*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Turning intervals into lists: upt and upto*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 17 Jul 2021 17:53:02 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mail-out2.in.tum.de) smtp.remote-ip=131.159.0.36; spf=pass smtp.mailfrom=in.tum.de; arc=none*In-reply-to*: <d31b11be-dda7-2c5a-dee1-d5fd9f978968@informatik.tu-muenchen.de>*References*: <3ac3a0b4-9f77-c1f9-5bc3-3c969286736b@in.tum.de> <afd219e8-7114-396f-10e0-f79543e376ee@in.tum.de> <d31b11be-dda7-2c5a-dee1-d5fd9f978968@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:78.0) Gecko/20100101 Thunderbird/78.12.0

Tobias On 17/07/2021 10:57, Florian Haftmann wrote:

Hi all,I always like to balance ease of notation and proof automation. I would have no objection against generalising [_.._] to some type class.5 years ago I posted sth. on the mailing list: https://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg06715.html I think it is still a valid starting point for further discussion.If you really want to improve the situation, you could iron out a different problem. This is a defining equation and simp rule: "[i..<(Suc j)] = (if i ≤ j then [i..<j] @ [j] else [])" Unfortunately it leads to lists where elements are appended at the end, but many functions consume lists from the front. Thus this simp rule is frequently removed. Something like the following one should work better (I hope): "[i..<j] = (if i < j then i # [Suc i..<j] else [])"I agree with the observation that the default simp rule above obstructs proofs that would require unfolding from the lower bound rather than the upper bound. But the alternative formulation has no syntactic circuit breaker like Suc and would hence unfold infinitely. Maybe a conditional formulation would help: ‹i < j ==> [i..<j] = i # [Suc i..<j]› But this all would require further thinking. Cheers, Florian

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Turning intervals into lists: upt and upto***From:*Thomas Sewell

**References**:**[isabelle] Turning intervals into lists: upt and upto***From:*Manuel Eberl

**Re: [isabelle] Turning intervals into lists: upt and upto***From:*Tobias Nipkow

**Re: [isabelle] Turning intervals into lists: upt and upto***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Date: Re: [isabelle] Turning intervals into lists: upt and upto
- Previous by Thread: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Thread: Re: [isabelle] Turning intervals into lists: upt and upto
- Cl-isabelle-users July 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list