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"