Re: [isabelle] [Noob] Proof on trees
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)
show ?case by simp
case (Node tr1 a tr2)
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