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

[Tobias Nipkow]

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 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.


Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or 
renaming that "compact" in the most appropriate way.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Sebastien Gouezel]

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 comment in the library 
around there mentioning subsequences, that could be found by grepping 
the library (I found out that grepping the library or the AFP for 
mathematical keywords is often the most efficient way to locate facts or 
definitions related to a given concept).



It's "Topological_Spaces.compact" and that should definitely work.


Yes, it works. Strangely, topological_space.compact is recognized as 
valid syntax (contrary, say, to metric_space.compact), that's why I 
didn't spot my mistake.


Thanks!
Sebastien

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Manuel Eberl]

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 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.

> 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 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.

Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Sebastien Gouezel]

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.

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.


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). For instance, the fact that a 
sequence of functions which converges in L^2 has a subsequence which 
converges everywhere, is extremely powerful. Having to type

topological_spaces.subseq all the time would be very cumbersome, on
the other hand using something like subsequence would be perfectly
OK (and I am strongly in favour of keeping it).

By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly

theory Foo
  imports Analysis
begin

lemma infdist_compact_attained:
  assumes "compact C" "C ≠ {}"
  shows "∃c∈C. infdist x C = dist x c"
proof -
  have "∃c∈C. ∀d∈C. dist x c ≤ dist x d"
by (rule continuous_attains_inf[OF assms], intro continuous_intros)
  then show ?thesis unfolding infdist_def using `C ≠ {}`
by (metis antisym bdd_below_infdist cINF_lower le_cINF_iff)
qed

end


But if one imports Probability instead of Analysis, then compact
becomes the one from Complete_Partial_Order2 (which, I think, is
much less commonly used than the compactness for topological
spaces). Strangely enough, even replacing compact with
topological_space.compact does not solve the issue.

Sebastien Gouezel

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

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 with that problem.

At the moment I don’t regard it as heavily used, but I guess it depends on what 
one is working on at any one time.

I would rather have qualified names than completely arbitrary variations of the 
name.

Larry

> On 30 Jun 2017, at 15:57, Manuel Eberl  wrote:
> 
> 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.
> 
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [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  > 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

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

[Tobias Nipkow]

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 > 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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Manuel Eberl]

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 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 >> > 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

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

[Tobias Nipkow]

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 > 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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 Eberl wrote:

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 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 subsequence. This name is now hidden by the definition in
Sublist, in particular when I import HOL-Probability.

Can this name clash be eliminated before the next release such that I
don't have to write Topological_Spaces.subseq everywhere?

Thanks,
Andreas

On 26/05/17 08:16, Tobias Nipkow wrote:

Thank you for your research. I am perfectly happy with "sublist" (for
the contiguous case) and "subseq" (for the general case) and think we
should adopt it.

[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
nat set ⇒ 'a list" (in List) to something else, eg sublist_index)

Tobias

On 25/05/2017 21:13, Jasmin Blanchette wrote:



On 25.05.2017, at 20:41, Tobias Nipkow  wrote:

I don't think that sublist, subsequence and substring really have
much of a bias in either direction, except possibly substring, but
the latter does indeed sound too specialized.


Wikipedia has a clear bias (and I did not edit it, nor did I look it
up before writing my previous email):

 https://en.wikipedia.org/wiki/Subsequence
 https://en.wikipedia.org/wiki/Substring

Popular algorithm sbooks like Cormen et al. follow the same
definition of subsequence. Standard expressions like "longest
increasing subsequence" depend on this semantics.

As for sublist, all the examples I see by Googling either "sublist",
"is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
Scala, etc., have the contiguous semantics. Including this page:

 http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html

I'm not saying we should rename the Isabelle concepts, just that
Isabelle is the odd (wo)man out.

Jasmin




___
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




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Efficient code for Discrete.log

[Manuel Eberl]

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 believe there is already a more efficient way 
> to compute log2.
> 
> In your implementation, consider your intlog2_aux which roughly requires y 
> iterations if log2(x) = y,
> since you always just add 1 to the accumulator.
> 
> For some of my applications this implementation is not efficient enough, 
> which was the reason to develop Sqrt_Babylonian/Log_Impl.thy,
> which is much faster since it only needs log2(y) iterations: 
> in log_main the accumulator is roughly doubled in every iteration.
> 
> To test, try to compute "log_2 (3 ^ n)” for some reasonably large n.
> 
> Cheers,
> René
> 
> PS: Unfortunately, Sqrt_Babylonian.log_floor and log_ceiling are not 
> connected to Discrete.log.
> 
>> Am 29.06.2017 um 15:29 schrieb Manuel Eberl :
>>
>> Hallo,
>>
>> I'm considering adding efficient code for Discrete.log (the dual logarithm 
>> on natural numbers). PolyML does provide an IntInf.log2 function that seems 
>> reasonably efficient so that one can set up code printing. However, I am 
>> struggling with one detail:
>>
>> Where would the code that does this actually reside? I cannot really put it 
>> into Discrete.thy, because then that would have to import 
>> Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but then 
>> that would have to import Discrete, which does not sound right to me either.
>>
>> I attached what I have so far.
>>
>> Manuel
>>
>> ___
>> 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

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

[Andreas Lochbihler]

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.

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 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 subsequence. This name is now hidden by the definition in
Sublist, in particular when I import HOL-Probability.

Can this name clash be eliminated before the next release such that I
don't have to write Topological_Spaces.subseq everywhere?

Thanks,
Andreas

On 26/05/17 08:16, Tobias Nipkow wrote:

Thank you for your research. I am perfectly happy with "sublist" (for
the contiguous case) and "subseq" (for the general case) and think we
should adopt it.

[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
nat set ⇒ 'a list" (in List) to something else, eg sublist_index)

Tobias

On 25/05/2017 21:13, Jasmin Blanchette wrote:



On 25.05.2017, at 20:41, Tobias Nipkow  wrote:

I don't think that sublist, subsequence and substring really have
much of a bias in either direction, except possibly substring, but
the latter does indeed sound too specialized.


Wikipedia has a clear bias (and I did not edit it, nor did I look it
up before writing my previous email):

 https://en.wikipedia.org/wiki/Subsequence
 https://en.wikipedia.org/wiki/Substring

Popular algorithm sbooks like Cormen et al. follow the same
definition of subsequence. Standard expressions like "longest
increasing subsequence" depend on this semantics.

As for sublist, all the examples I see by Googling either "sublist",
"is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
Scala, etc., have the contiguous semantics. Including this page:

 http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html

I'm not saying we should rename the Isabelle concepts, just that
Isabelle is the odd (wo)man out.

Jasmin




___
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