[isabelle-dev] [isabelle] Good name for "sublist" predicates
eberlm at in.tum.de
Fri Jun 30 16:57:25 CEST 2017
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
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?
>> 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.
>> 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.
>>> On 30/06/2017 16:14, Lawrence Paulson wrote:
>>>> Indeed we do.
>>>>> 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,
>>>>> we do have qualified names.
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev