theory MyTheory = Main: datatype 'a btree = Leaf | Branch 'a "'a btree" "'a btree" consts mirror :: "'a btree \ 'a btree" primrec "mirror Leaf = Leaf" "mirror (Branch elt t1 t2) = Branch elt (mirror t2) (mirror t1)" consts flatten :: "'a btree \ 'a list" primrec "flatten Leaf = []" "flatten (Branch elt t1 t2) = (flatten t1) @ (Cons elt (flatten t2))" lemma flat : "\t. flatten (mirror t) = rev (flatten t)" apply (rule allI) apply (induct_tac t) apply auto done lemma mir_mir : "mirror (mirror t) = t" apply (induct t) apply auto done