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

[Manuel Eberl]

I agree about 90%, I think, but one could argue that "subseq" contains
additional meta-information: the semantic meaning is that it is a
strictly monotonic function, but the idea behind it is that it describes
a sub-sequence of some other sequence.

Still, I for one think this is not really worth the trouble of keeping
an entirely separate constant around, especially because "subseq h" does
not make much sense: "h" itself is not a subsequence of anything, "f ∘
h" is a sub-sequence of "f".

It would be interesting to know what other users of Complex_Main think
about that.

Manuel


On 2017-06-30 16:52, Tobias Nipkow wrote:
>
> 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
>>
>>
>
>
>
> _______________________________________________
> 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/6529bc1d/attachment-0002.html>