theory Ex3_2_2
imports Main Ex2_5_1
begin
primrec flatten2 :: "tree \ nat list \ nat list" where
"flatten2 Tip ls = ls" |
"flatten2 (Node l x r) ls = flatten2 l (x # (flatten2 r ls))"
lemma helper: "flatten2 t ls = (flatten t) @ ls"
apply (induct t arbitrary: ls)
apply auto
done
lemma "flatten2 t [] = flatten t"
using helper apply simp
done
end