theory Tree = Main:

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

lemma "Tip ~= Node l x r"
apply auto
done

lemma "(0::nat) \<le> (case t of Tip \<Rightarrow> 0 | Node l x r \<Rightarrow> x+1)"
apply(case_tac t)
apply auto
done

consts
  mirror :: "'a tree => 'a tree"

primrec
"mirror Tip = Tip"
"mirror (Node l x r) = Node (mirror r) x (mirror l)"

lemma [simp]: "mirror(mirror t) = t"
apply(induct_tac t)
apply auto
done

end