# 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)
case Tip
show ?case by simp
next
case (Node tr1 a tr2)
show ?case
apply simp
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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.