theory Demo = 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"
       prime :: "nat \<Rightarrow> bool"

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

defs
prime_def:
  "prime p == !m. m dvd p --> m=1 | m=p"

constdefs
 xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
"xor x y \<equiv> \<not>(x=y)"

lemma "xor x (\<not>x)"
apply(unfold xor_def)
apply auto
done

types autonr       =  nat
      'a self      =  "'a => 'a"
      ('a,'b)alist =  "('a * 'b) list"

end