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

[Makarius]

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 lengthy names is tedious.

Just for typing it there is semantic completion in the Prover IDE. For
constants in the term language, it requires trailing "_" to say that it
is really meant to be a constant and not a variable.

To actually complete such long name components as "subseq" in
"Topological_Spaces.subseq", I have now made a tiny change in
Isabelle/f50e6e31a0ee. Also note that the completion history reorders
frequently used completions later on, so the long list of completion
items becomes practically usable.


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

That introduces some extra complexity in the theory source, apart from
input methods. Nonetheless, the 'alias' command from
Isabelle/df85956228c2 can in principle do that: it merely exposes an
important Isabelle/ML interface from recent years as Isar command.

I did not do this earlier, because aliases have the potential for extra
confusion of names in a theory, but proper name space operations are
better than simulating that with 'notation' / 'no_notation'. (Alphabetic
syntax tokens should be kept at a minimum anyway: they are subtracted
from the identifier syntax category.)


Makarius
___
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]

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



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



___
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

[Florian Haftmann]

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

Am 30.06.2017 um 20:41 schrieb 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
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital 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

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

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

[Manuel Eberl]

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

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

[Andreas Lochbihler]

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