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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170630/6c42202f/attachment.bin>