--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Chap03.thy	Mon Jan 26 15:41:16 2015 +0000
@@ -0,0 +1,167 @@
+theory Chap03
+imports Main
+begin
+
+lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
+apply simp
+done
+
+lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"
+apply (simp (no_asm))
+done
+
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
+
+lemma "xor A (\<not>A)"
+apply(simp only: xor_def)
+apply(simp add: xor_def)
+done
+
+lemma "(let xs = [] in xs@ys@xs) = ys"
+apply(simp only: Let_def)
+apply(simp add: Let_def)
+done
+
+(* 3.1.8 Conditioal Simplification Rules  *)
+
+lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
+using [[simp_trace=true]]
+apply(case_tac xs)
+apply(simp)
+apply(simp)
+done
+
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"
+apply(case_tac xs)
+using [[simp_trace=true]]
+apply(simp)
+apply(simp)
+done
+
+(* 3.1.9 Automatic Case Splits  *)
+
+lemma "\<forall> xs. if xs = [] then rev xs = [] else rev xs \<noteq> []"
+apply(split split_if)
+apply(simp)
+done
+
+lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"
+apply(split list.split)
+apply(simp split: list.split)
+done
+
+lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
+apply(split split_if_asm)
+apply(simp)
+apply(auto)
+done
+
+(* 3.2 Induction Heuristics  *)
+
+primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "itrev xs [] = rev xs"
+apply(induct_tac xs)
+apply(simp)
+apply(auto)
+oops
+
+lemma "itrev xs ys = rev xs @ ys"
+apply(induct_tac xs)
+apply(simp_all)
+oops
+
+lemma "\<forall> ys. itrev xs ys = rev xs @ ys"
+apply(induct_tac xs)
+apply(simp)
+apply(simp)
+done
+
+primrec add1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add1 m 0 = m" |
+"add1 m (Suc n) = add1 (Suc m) n"
+
+value "add1 1 3"
+value "1 + 3"
+
+lemma abc [simp]: "add1 m 0 = m"
+apply(induction m)
+apply(simp)
+apply(simp)
+done
+
+lemma abc2 "add1 m n = m+n"
+apply(induction n)
+apply(auto)
+
+oops
+
+(* 3.3 Case Study: Compiling Expressions  *)
+
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
+datatype ('a, 'v)expr = 
+  Cex 'v
+| Vex 'a
+| Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
+
+primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where
+"value (Cex v) env = v" |
+"value (Vex a) env = env a" |
+"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
+
+datatype ('a,'v)instr = 
+  Const 'v
+| Load 'a
+| Apply "'v binop"
+
+primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" where
+"exec [] s vs = vs" |
+"exec (i#is) s vs = (case i of
+    Const v \<Rightarrow> exec is s (v#vs)
+  | Load a \<Rightarrow> exec is s ((s a)#vs)
+  | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
+  
+primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where
+"compile (Cex v) = [Const v]" |
+"compile (Vex a) = [Load a]" |
+"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
+
+theorem "exec (compile e) s [] = [value e s]"
+(*the theorem needs to be generalized*)
+oops
+
+(*more generalized theorem*)
+theorem "\<forall> vs. exec (compile e) s vs = (value e s) # vs"
+apply(induct_tac e)
+apply(simp)
+apply(simp)
+oops
+
+lemma exec_app[simp]: "\<forall> vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
+apply(induct_tac xs)
+apply(simp)
+apply(simp)
+apply(simp split: instr.split)
+done
+
+(* 2.5.6 Case Study: Boolean Expressions *)
+
+datatype boolex = Const bool | Var nat | Neg boolex
+| And boolex boolex
+
+primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"value2 (Const b)  env = b" |
+"value2 (Var x)    env = env x" |
+"value2 (Neg b)    env = (\<not> value2 b env)" |
+"value2 (And b c)  env = (value2 b env \<and> value2 c env)"
+
+value "Const true"
+value "Suc(Suc(0))"
+
+'b::Const = "true"
+
+value "value2 (Const true) (env = true)"
+