--- a/thys/Chap03.thy	Mon Jan 26 15:41:16 2015 +0000
+++ b/thys/Chap03.thy	Mon Jan 26 15:54:27 2015 +0000
@@ -84,6 +84,10 @@
 "add1 m 0 = m" |
 "add1 m (Suc n) = add1 (Suc m) n"
 
+primrec add2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add2 m 0 = m" |
+"add2 m (Suc n) = Suc (add2 m n)"
+
 value "add1 1 3"
 value "1 + 3"
 
@@ -93,11 +97,41 @@
 apply(simp)
 done
 
-lemma abc2 "add1 m n = m+n"
+lemma abc2: "\<forall>m. add1 m n = m + n"
 apply(induction n)
-apply(auto)
+apply(simp)
+apply(simp del: add1.simps)
+apply(simp (no_asm) only: add1.simps)
+apply(simp only: )
+apply(simp)
+done
+
+thm abc2
+
+lemma abc3: "add1 m n = m + n"
+apply(induction n arbitrary: m)
+apply(simp)
+apply(simp del: add1.simps)
+apply(simp (no_asm) only: add1.simps)
+apply(simp only: )
+done
 
-oops
+thm abc3
+
+lemma abc4: "add1 m n = add2 m n"
+apply(induction n arbitrary: m)
+apply(simp)
+apply(simp add: abc3)
+done
+
+(* added test *)
+
+lemma abc5: "add2 m n = m + n"
+apply(induction n)
+apply(simp)
+apply(simp)
+done
+
 
 (* 3.3 Case Study: Compiling Expressions  *)
 
@@ -159,9 +193,22 @@
 "value2 (And b c)  env = (value2 b env \<and> value2 c env)"
 
 value "Const true"
-value "Suc(Suc(0))"
+value "Var (Suc(0))"
+
+
+
+value "value2 (Const False) (\<lambda>x. False)"
+value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"
 
-'b::Const = "true"
+definition
+  "en1 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
+  
+abbreviation
+  "en2 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
+  
+value "value2 (And (Var 10) (Var 11)) en2"
 
-value "value2 (Const true) (env = true)"
+lemma "value2 (And (Var 10) (Var 11)) en2 = True"
+apply(simp)
+done