--- 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,11 +50,31 @@
 
 value "add 2 3"
 
+
 (**commutative-associative**)
-lemma add_04: "add m (add n k) = add k (add m n)"
-apply(induct)
-apply(auto)
-oops
+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
+
+lemma add_odd: "add m (add n k) = add k (add m n)"
+apply(subst add_04)
+apply(subst (2) add_comm)
+apply(simp)
+done
+
 
 fun dub :: "nat \<Rightarrow> nat" where
 "dub 0 = 0" |
@@ -89,9 +109,54 @@
 value "trip 1"
 value "trip 2"
 
+fun sum :: "nat \<Rightarrow> nat" where
+  "sum 0 = 0"
+| "sum (Suc n) = (Suc n) + sum n"
+
+function sum1 :: "nat \<Rightarrow> nat" where
+  "sum1 0 = 0"
+| "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"
+apply(auto)
+done
+
+termination sum1
+by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)
+
+lemma "sum n = sum1 n"
+apply(induct n)
+apply(auto)
+done
+
+lemma "sum n = (\<Sum>i \<le> n. i)"
+apply(induct n)
+apply(simp_all)
+done
+
 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "mull 0 0 = 0" |
 "mull m 0 = 0" |
+"mull m 1 = m" | 
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
+apply(pat_completeness)
+apply(auto)
+
+done
+
+  "mull 0 n = 0"
+| "mull (Suc m) n = add n (mull m n)" 
+
+lemma test: "mull m n = m * n"
+sorry
+
+fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "poww 0 n = 1"
+| "poww (Suc m) n = mull n (poww m n)" 
+
+
+"mull 0 0 = 0" |
+"mull m 0 = 0" |
 (**"mull m 1 = m" | **)
 (**"mull m (1::nat) = m" | **)
 (**"mull m (suc(0)) = m" | **)
@@ -104,8 +169,7 @@
 "count  "
 **)
 
-fun sum :: "nat \<Rightarrow> nat" where
-"sum n = 0 + \<dots> + n"
+
 (* prove n = n * (n + 1) div 2  *)