--- a/thys/Pr.thy	Mon Jul 06 20:44:30 2015 +0100
+++ b/thys/Pr.thy	Thu Dec 17 13:14:36 2015 +0000
@@ -2,6 +2,68 @@
 imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"
 begin
 
+fun 
+  add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
+where
+  "add 0 n = n" |
+  "add (Suc m) n = Suc (add m n)"
+
+fun 
+  doub :: "nat \<Rightarrow> nat" 
+where
+  "doub 0 = 0" |
+  "doub n = n + n"
+
+lemma add_lem:
+  "add m n = m + n"
+apply(induct m arbitrary: )
+apply(auto)
+done
+
+fun 
+  count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
+where
+  "count n Nil = 0" |
+  "count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)"
+
+value "count 3 [1,2,3,3,4,3,5]"
+
+fun 
+  count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 
+where
+"count2 n Nil = 0" |
+"count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)"
+
+value "count2 (2::nat) [2,2,3::nat]"
+
+lemma
+  "count2 x xs \<le> length xs"
+apply(induct xs)
+apply(simp)
+apply(simp)
+apply(auto)
+done
+
+fun 
+  sum :: "nat \<Rightarrow> nat"
+where
+  "sum 0 = 0"
+| "sum (Suc n) = (Suc n) + sum n"
+
+lemma
+  "sum n = (n * (Suc n)) div 2"
+apply(induct n)
+apply(auto)
+done
+
+
+lemma
+  "doub n = add n n"
+apply(induct n)
+apply(simp)
+apply(simp add: add_lem)
+done
+
 lemma 
   fixes a b::nat
   shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"