Re: [isabelle] [Noob] Proof on trees
Very nice explanation Bertram. Thanks a lot!
Em 28/05/2016 22:04, "Bertram Felgenhauer via Cl-isabelle-users" <
cl-isabelle-users at lists.cam.ac.uk> escreveu:
> 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
> case (Node tr1 a tr2)
> show ?case
> apply simp
> apply (simp add: Node.IH)
> I would prove the symmetric version of the lemma which avoids these
> lemma dfs2_dfs1_conv: "dfs2 t xs = dfs1 t @ xs"
> by (induct t arbitrary: xs) auto
This archive was generated by a fusion of
Pipermail (Mailman edition) and