theory MyTreeimports Mainbegindatatype '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) donedatatype 'a option = None | Some 'afun 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)donevalue "div2 8"