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