4 

     5 fun 

     6   add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

     7 where

     8   "add 0 n = n" |

     9   "add (Suc m) n = Suc (add m n)"

    10 

    11 fun 

    12   doub :: "nat \<Rightarrow> nat" 

    13 where

    14   "doub 0 = 0" |

    15   "doub n = n + n"

    16 

    17 lemma add_lem:

    18   "add m n = m + n"

    19 apply(induct m arbitrary: )

    20 apply(auto)

    21 done

    22 

    23 fun 

    24   count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"

    25 where

    26   "count n Nil = 0" |

    27   "count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)"

    28 

    29 value "count 3 [1,2,3,3,4,3,5]"

    30 

    31 fun 

    32   count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 

    33 where

    34 "count2 n Nil = 0" |

    35 "count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)"

    36 

    37 value "count2 (2::nat) [2,2,3::nat]"

    38 

    39 lemma

    40   "count2 x xs \<le> length xs"

    41 apply(induct xs)

    42 apply(simp)

    43 apply(simp)

    44 apply(auto)

    45 done

    46 

    47 fun 

    48   sum :: "nat \<Rightarrow> nat"

    49 where

    50   "sum 0 = 0"

    51 | "sum (Suc n) = (Suc n) + sum n"

    52 

    53 lemma

    54   "sum n = (n * (Suc n)) div 2"

    55 apply(induct n)

    56 apply(auto)

    57 done

    58 

    59 

    60 lemma

    61   "doub n = add n n"

    62 apply(induct n)

    63 apply(simp)

    64 apply(simp add: add_lem)

    65 done