theory MyTree
imports Main
begin

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

fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
  "mirror Tip = Tip" |
  "mirror (Node l a r) = Node (mirror r) a (mirror l)"

lemma "mirror(mirror t) = t"
  apply(induction t)
  apply(auto)
  done

datatype 'a option = None | Some 'a

fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
  "lookup [] x = None" |
  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"

definition sq :: "nat \<Rightarrow> nat" where
  "sq n = n * n"
 
abbreviation sq' :: "nat \<Rightarrow> nat" where
  "sq' n \<equiv> n * n"

fun div2 :: "nat \<Rightarrow> nat" where
  "div2 0 = 0" |
  "div2 (Suc 0) = 0" |
  "div2 (Suc(Suc n)) = Suc(div2 n)"

lemma "div2(n) = n div 2"
apply(induction n rule: div2.induct)
apply(auto)
done

value "div2 8"