[isabelle-dev] [isabelle] Good name for "sublist" predicates

[Tobias Nipkow]

On 30/06/2017 16:39, Manuel Eberl wrote:
> I do understand that argument, but I am not sure if Topological_Spaces.subseq is 
> really used /that/ often. Actually, going one step further, it is nothing more 
> than "strict_mono" restricted to "nat ⇒ nat", so one may well argue that it is 
> superfluous anyway.

If we can get rid of it all together, surely that is the best option?

Tobias

> The possibility of renaming one of them to "subsequence" or "is_subseq" is, in 
> my opinion, not a satisfactory solution, since we would then /still/ have two 
> completely different constants with essentially the same name, just with an 
> arbitrary artificial difference. We might as well call one of them subseq'.
> 
> The advantage of qualified names is that they really allow us to add 
> disambiguating context to ambiguous names when necessary, e.g. something like 
> "List.subseq" and "Topological_Spaces.subseq". Still, as I said, I do understand 
> that typing such lengthy names is tedious.
> 
> I currently see the following possible solutions:
> 
> – find another good name for one of the two things currently named "subseq" and 
> rename it
> – introduce an arbitrary distinction like "subsequence" or "is_subseq"
> – move "subseq" to List.thy and make it qualified, so that one must write 
> "List.subseq"
> – remove Topological_Spaces.subseq entirely, replacing it by strict_mono
> – leave everything as it is
> 
> Incidentally, I wonder if it is possible to locally prefer one of the two 
> constants, i.e. say that, in the following block, I want "subseq" to mean 
> "Topological_Spaces.subseq". That might also mitigate the problem of long 
> qualified names.
> 
> Manuel
> 
> 
> 
> On 2017-06-30 16:23, Tobias Nipkow wrote:
>> In theory that solves the problem, but the point is that 
>> Topological_Spaces.subseq is impractical for a frequently used symbol. It 
>> would be nice if non-quaified names could be found for this case.
>>
>> Tobias
>>
>> On 30/06/2017 16:14, Lawrence Paulson wrote:
>>> Indeed we do.
>>> Larry
>>>
>>>> On 28 Jun 2017, at 18:49, Manuel Eberl <eberlm at in.tum.de 
>>>> <mailto:eberlm at in.tum.de>> wrote:
>>>>
>>>> Yes, I noticed that as well. I decided to leave it that way since, well,
>>>> we do have qualified names.
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170630/5ad19d73/attachment.bin>