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

[Manuel Eberl]

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.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170630/b6cf5d67/attachment-0002.html>