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