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