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

On 30/06/17 16:39, Manuel Eberl wrote: > > 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

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

See now Isabelle/4c999b5d78e2. Andreas On 30/06/17 21:31, Tobias Nipkow wrote: On 30/06/2017 20:41, Manuel Eberl wrote: By the way, I recently encountered a similar (and even more nasty) name clash, with compact. The following works perfectly It's "Topological_Spaces.compact" and that

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

Hi all, Yes, it absolutely makes sense to change the situation with compact. It is a standard notion in order theory, so my suggestion is to make it qualified with ccpo, just like admissible and fixp are. I can take care of that. Andreas On 30/06/17 21:31, Tobias Nipkow wrote: On

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

Just for the record: * Topological_Spaces.subseq has already been present before 2007 in HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7) * strict_mono has entered in 2009, see abefe1dfadbb Hence we have the typical situation that a generalized constant subsumes a more ancient unconsciously. Cheers,

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

On 30/06/2017 20:41, Manuel Eberl wrote: By the way, I recently encountered a similar (and even more nasty) name clash, with compact. The following works perfectly It's "Topological_Spaces.compact" and that should definitely work. We should probably make the one from Complete_Partial_Order2

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

Le 30/06/2017 à 20:41, Manuel Eberl a écrit : So what about the suggestion of just writing "strict_mono" instead? Besides, you can always introduce local abbreviations for things with "notation" and delete them with "no_notation" afterwards. strict_mono would be perfectly OK if there is a

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

On 2017-06-30 20:33, Sebastien Gouezel wrote: > I used subseq quite heavily in my ergodic theory developments. From > a mathematician point of view, taking subsequences of sequences > from nat to nat is very common and very useful in analysis (much > more than taking subsequences of lists). So

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

Le 30/06/2017 à 16:57, Manuel Eberl a écrit : 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.

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

As I recall, this constant originally comes from HOL Light and is used in a couple of proofs. And it occurs to me that it might be a good way of dealing with HOL Light’s generalisation of summations and limits to sets of natural numbers. As I ported the PNT, I used two other methods of dealing

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

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

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

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

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

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

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

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

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

Indeed we do. Larry > On 28 Jun 2017, at 18:49, Manuel Eberl 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

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

Another possibility is to call one of them is_subseq. Tobias On 30/06/2017 08:17, Andreas Lochbihler wrote: Hi Manuel, Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly strict_subseq to strict_subsequence or ssubsequence? Andreas On 28/06/17 19:49, Manuel

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

Hi Manuel, Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly strict_subseq to strict_subsequence or ssubsequence? Andreas On 28/06/17 19:49, Manuel Eberl wrote: Yes, I noticed that as well. I decided to leave it that way since, well, we do have qualified names.

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

Yes, I noticed that as well. I decided to leave it that way since, well, we do have qualified names. If anybody has better suggestions, I am open to implementing them. Manuel On 2017-06-28 17:05, Andreas Lochbihler wrote: > Dear all, > > While porting some of my theories to the current

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

Dear all, While porting some of my theories to the current development version, I've just noticed that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad effect: The name subseq is already used in Topological_Spaces to formalise the concept of a