4 

     5 datatype 

     6   'a tree = Tip | 

     7   Node " 'a tree" 'a " 'a tree"

     8 

     9 fun mirror :: " 'a tree \<Rightarrow> 'a tree" where

    10   "mirror Tip = Tip" |

    11   "mirror (Node l a r) = Node (mirror r) a (mirror l)"

    12 

    13 lemma "mirror(mirror t) = t"

    14   apply(induction t)

    15   apply(auto)

    16   done

    17 

    18 datatype 'a option = None | Some 'a

    19 

    20 fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where

    21   "lookup [] x = None" |

    22   "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"

    23 

    24 definition sq :: "nat \<Rightarrow> nat" where

    25   "sq n = n * n"

    26  

    27 abbreviation sq' :: "nat \<Rightarrow> nat" where

    28   "sq' n \<equiv> n * n"

    29 

    30 fun div2 :: "nat \<Rightarrow> nat" where

    31   "div2 0 = 0" |

    32   "div2 (Suc 0) = 0" |

    33   "div2 (Suc(Suc n)) = Suc(div2 n)"

    34 

    35 lemma "div2(n) = n div 2"

    36 apply(induction n rule: div2.induct)

    37 apply(auto)

    38 done

    39 

    40 value "div2 8"

    41 

    42