--- a/thys/MyFirst.thy~	Mon Oct 06 14:22:13 2014 +0100
+++ b/thys/MyFirst.thy~	Mon Oct 06 15:24:41 2014 +0100
@@ -50,10 +50,23 @@
 
 value "add 2 3"
 
-lemma add_04: "add m (add n k) = add k (add m n)"
-apply(induct)
-apply(auto)
-oops
+(**commutative-associative**)
+lemma add_04: "add m (add n k) = add (add m n) k"
+apply(induct m)
+apply(simp_all)
+done
+
+lemma add_zero: "add n 0 = n"
+sorry
+
+lemma add_Suc: "add m (Suc n) = Suc (add m n)"
+sorry
+
+lemma add_comm: "add m n = add n m"
+apply(induct m)
+apply(simp add: add_zero)
+apply(simp add: add_Suc)
+done
 
 fun dub :: "nat \<Rightarrow> nat" where
 "dub 0 = 0" |
@@ -91,14 +104,22 @@
 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
-"mull m 1 = m" |
-"mull m n = 0" 
+(**"mull m 1 = m" | **)
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
 
+(**Define a function that counts the
+number of occurrences of an element in a list **)
 (**
 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
 "count  "
 **)
 
+fun sum :: "nat \<Rightarrow> nat" where
+"sum n = 0 + \<dots> + n"
+(* prove n = n * (n + 1) div 2  *)
+
 
 
 
@@ -108,3 +129,4 @@
 
 
 
+