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] Efficient code for Discrete.log

Thanks for the hint! I'll try to use that then. However, the main goal was to use PolyML's native log2 function anyway, which is likely much faster than anything we can implement in Isabelle. Manuel On 2017-06-29 20:12, Thiemann, Rene wrote: > Hi Manual, > > thanks for your efforts, but I

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.