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 <ebe...@in.tum.de >>>>> <mailto:ebe...@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-...@in.tum.de >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>>> >>>> >>> >>> >>> >>> _______________________________________________ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >> >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
