--- a/thys/Chap03.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,295 +0,0 @@
-theory Chap03
-imports Main
-begin
-
-(* 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 "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)"
-value "value2 (Var 11) (\<lambda>x. 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"
-
-lemma "value2 (And (Var 10) (Var 11)) en2 = True"
-apply(simp)
-done
-
-datatype ifex = 
-  CIF bool 
-| VIF nat 
-| IF ifex ifex ifex
-
-primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
-"valif (CIF b)    env = b" |
-"valif (VIF x)    env = env x" |
-"valif (IF b t e) env = (if valif b env then valif t env else valif e env)"
-
-abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)"
-abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)"
-abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)"
-
-value "valif (CIF False) (\<lambda>x. False)"
-value "valif (VIF 11) (\<lambda>x. True)"
-value "valif (IF (CIF False) (CIF True) (CIF True))"
-
-primrec bool2if :: "boolex \<Rightarrow> ifex" where
-"bool2if (Const b)  = CIF b" |
-"bool2if (Var x)    = VIF x" |
-"bool2if (Neg b)    = IF (bool2if b) (CIF False) (CIF True)" |
-"bool2if (And b c)  = IF (bool2if b) (bool2if c) (CIF False)"
-
-lemma "valif (bool2if b) env = value2 b env"
-apply(induct_tac b)
-apply(auto)
-done
-
-primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
-"normif (CIF b)     t e = IF (CIF b) t e" |
-"normif (VIF x)     t e = IF (VIF x) t e" |
-"normif (IF b t e)  u f = normif b (normif t u f) (normif e u f)"
-
-primrec norm :: "ifex \<Rightarrow> ifex" where
-"norm (CIF b)     = CIF b" |
-"norm (VIF x)     = VIF x" |
-"norm (IF b t e)  = normif b (norm t) (norm e)"  
-
-(***************   CHAPTER-3   ********************************)
-
-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"
-
-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"
-
-lemma abc [simp]: "add1 m 0 = m"
-apply(induction m)
-apply(simp)
-apply(simp)
-done
-
-lemma abc2: "\<forall>m. add1 m n = m + n"
-apply(induction n)
-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
-
-thm abc3
-
-lemma abc4: "add1 m n = add2 m n"
-apply(induction n arbitrary: m)
-apply(simp)
-apply(simp add: abc3)
-done
-
-find_theorems "_ \<and> _ "
-
-(* added anottest *)
-
-lemma abc5: "add2 m n = m + n"
-apply(induction n)
-apply(simp)
-apply(simp)
-done
-
-
-(* 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)"
-
-value "value (Cex a) (\<lambda>x. True)"
-
-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
-
-(* 3.4 Advanced Datatypes  *)
-
-datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" 
-                | Sum "'a aexp" "'a aexp"
-                | Diff "'a aexp" "'a aexp"
-                | Var 'a
-                | Num nat
-and      'a bexp = Less "'a aexp" "'a aexp"
-                | And "'a bexp" "'a bexp"
-                | Neg "'a bexp"
-                
-(*  Total Recursive Functions: Fun  *)
-(*  3.5.1 Definition    *)
-
-fun fib :: "nat \<Rightarrow> nat" where
-"fib 0 = 0" |
-"fib (Suc 0) = 1" |
-"fib (Suc(Suc x)) = fib x + fib (Suc x)"
-
-value "fib (Suc(Suc(Suc(Suc(Suc 0)))))"
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep a [] = []" |
-"sep a [x] = [x]" |
-"sep a (x#y#zs) = x # a # sep a (y#zs)"
-
-fun last :: "'a list \<Rightarrow> 'a" where
-"last [x] = x" |
-"last (_#y#zs) = last (y#zs)"
-
-fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
-"sep1 _ xs = xs"
-
-fun swap12:: "'a list \<Rightarrow> 'a list" where
-"swap12 (x#y#zs) = y#x#zs" |
-"swap12 zs = zs"
-