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"+ −
+ −
+ −