*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Turning intervals into lists: upt and upto*From*: Thomas Sewell <tals4 at cam.ac.uk>*Date*: Mon, 19 Jul 2021 09:47:25 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <617d104c-47c9-3e37-80b6-300ab3ca830c@in.tum.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> <617d104c-47c9-3e37-80b6-300ab3ca830c@in.tum.de>*User-agent*: Roundcube Webmail/1.4.11

I've worked with upt a bit, and I generally override the default simplification direction for the reasons mentioned already. Often it's useful to work with an upt+map variant, for instance: "i < j ⟹ upt i j = i # map Suc (upt i (j - 1))" The above will work with an induction on j, assuming the map is compatible with what you're doing. The library already contains map_upt_Suc for cases where the map was explicitly present. Anyway, my points is, while there might be a lot of proofs about upt, many of them might manually set the rewrite/simp pattern, and might need less maintenance. I note that a grep for 'del:.*upt.simps' in the l4.verified repository gives me 160+ hits. That might be daunting or not. Best regards, Thomas. On 2021-07-17 16:53, Tobias Nipkow wrote:

Yes, "[i..<j] = (if i < j then i # [Suc i..<j] else [])" does not terminate (hence my "something like") and two conditional rules are probably the best option. But updating the proofs could be daunting... 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 typeclass.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 theend,but many functions consume lists from the front. Thus this simp ruleisfrequently removed. Something like the following one should workbetter(I hope): "[i..<j] = (if i < j then i # [Suc i..<j] else [])"I agree with the observation that the default simp rule aboveobstructsproofs that would require unfolding from the lower bound rather thantheupper bound. But the alternative formulation has no syntactic circuitbreaker like Suc and would hence unfold infinitely. Maybe aconditionalformulation would help: ‹i < j ==> [i..<j] = i # [Suc i..<j]› But this all would require further thinking. Cheers, Florian

**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

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

- Previous by Date: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Date: [isabelle] Postdoctoral Opening at the University of Minnesota
- Previous by Thread: Re: [isabelle] Turning intervals into lists: upt and upto
- Next by Thread: [isabelle] Fwd: Postdoc position: Formal methods in control (Munich, Germany), ref 9y22x
- 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