theory Demo = Main:


typedecl varname
typedecl varname2

types nat_pair = "nat \<times> nat"
types nat_triple = "nat \<times> nat \<times> nat"

term "(1, (2, 3)) :: nat_triple"
term "(1, ((2, 3)::nat_pair)) :: nat_triple"

(*
term "((1, 2)::nat_pair, 3) :: nat_triple"
*)
constdefs
  f :: "[nat, nat] \<Rightarrow> nat"
  "f x  == \<lambda> y. x + y + 2"

(*
lemma "f 2 = z"
apply (simp add: f_def)
done
*)
(*
term "((1, 2), 3) :: nat_triple"
*)

term "(x::varname) = (y::varname)"

(*
term "(x::varname) = (y::varname2)"
*)

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

lemma "Tip \<noteq> 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"

consts
  lookup :: "['k, ('k \<times> 'v) list] \<Rightarrow> 'v option"

primrec
  "lookup k [] = None"
  "lookup k (x#xs) = 
      (if (fst x) = k then Some (snd x) else lookup k xs)"

lemma "lookup (2::nat) [(1, 2), (2, 4), (3, 6)] = z"
apply simp
oops

lemma "lookup (4::nat) [(1, 2), (2, 4), (3, 6)] = z"
apply simp
oops


end