*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] [Noob] Proof on trees*From*: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Sun, 29 May 2016 03:04:22 +0200*In-reply-to*: <CAAPnxw10Tb1-6J8+PhV6iv6r3gARX10Wcx+qaJhkmX58csuF8A@mail.gmail.com>*References*: <CAJ+TeoenCK-idZ5AnAxD2sinE2YqUw=3zX=5PNfpBm3EhqoLzg@mail.gmail.com> <f95cc660-a1b0-ffb1-bb5a-ebbc6523d149@danielhorne.co.uk> <CAAPnxw10Tb1-6J8+PhV6iv6r3gARX10Wcx+qaJhkmX58csuF8A@mail.gmail.com>*Reply-to*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*User-agent*: Mutt/1.6.0 (2016-04-01)

Alfio Martini wrote: > Hi Daniel, > , > I am especially also interested in knowing why the structured proofs goes > thorugh using just the simplifier and the script fails to succeed. When faced with proving "dfs1 (Node tr1 a tr2) @ xs = dfs2 (Node tr1 a tr2) xs" the simplifier first unfolds the left-hand side to "(dfs1 tr1 @ a # dfs1 tr2) @ xs" At this point, there are two possibilities: a) use the induction hypothesis and rewrite that term further to "dfs2 tr1 (a # dfs1 tr2) @ xs" at which point the simplifier gets stuck; in fact it's hard to make progress from here because the xs is outside of the call "dfs2 tr1 ...", but the right-hand side will expand to "dfs2 tr1 (a # dfs2 tr2 xs)" with the xs inside of the "dfs2 tr1 ..." call. b) use the associativity of append and its definition to obtain "dfs1 tr1 @ a # dfs1 tr2 @ xs" and only then apply the induction hypothesis which results in "dfs2 tr1 (a # dfs2 tr2 xs)" Unfortunately, if the induction hypothesis is available for simplification, the simplifier prefers a) and the proof fails. The following works, but looks fragile: lemma "dfs1 tr @ xs = dfs2 tr xs" proof (induction tr arbitrary: xs) case Tip show ?case by simp next case (Node tr1 a tr2) show ?case apply simp apply (simp add: Node.IH) done qed I would prove the symmetric version of the lemma which avoids these complications: lemma dfs2_dfs1_conv: "dfs2 t xs = dfs1 t @ xs" by (induct t arbitrary: xs) auto Cheers, Bertram

**Follow-Ups**:**Re: [isabelle] [Noob] Proof on trees***From:*Alfio Martini

**References**:**[isabelle] [Noob] Proof on trees***From:*Rustom Mody

**Re: [isabelle] [Noob] Proof on trees***From:*Daniel Horne

**Re: [isabelle] [Noob] Proof on trees***From:*Alfio Martini

- Previous by Date: Re: [isabelle] [Noob] Proof on trees
- Next by Date: Re: [isabelle] [Noob] Proof on trees
- Previous by Thread: Re: [isabelle] [Noob] Proof on trees
- Next by Thread: Re: [isabelle] [Noob] Proof on trees
- Cl-isabelle-users May 2016 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