1 theory Chap03

     2 imports Main

     3 begin

     4 

     5 (* 2.5.6 Case Study: Boolean Expressions *)

     6 

     7 datatype boolex = Const bool | Var nat | Neg boolex

     8 | And boolex boolex

     9 

    10 primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where

    11 "value2 (Const b)  env = b" |

    12 "value2 (Var x)    env = env x" |

    13 "value2 (Neg b)    env = (\<not> value2 b env)" |

    14 "value2 (And b c)  env = (value2 b env \<and> value2 c env)"

    15 

    16 value "Const true"

    17 value "Var (Suc(0))"

    18 value "value2 (Const False) (\<lambda>x. False)"

    19 value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"

    20 value "value2 (Var 11) (\<lambda>x. True )"

    21 

    22 definition

    23   "en1 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"

    24   

    25 abbreviation

    26   "en2 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"

    27   

    28 value "value2 (And (Var 10) (Var 11)) en2"

    29 

    30 lemma "value2 (And (Var 10) (Var 11)) en2 = True"

    31 apply(simp)

    32 done

    33 

    34 datatype ifex = 

    35   CIF bool 

    36 | VIF nat 

    37 | IF ifex ifex ifex

    38 

    39 primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where

    40 "valif (CIF b)    env = b" |

    41 "valif (VIF x)    env = env x" |

    42 "valif (IF b t e) env = (if valif b env then valif t env else valif e env)"

    43 

    44 abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)"

    45 abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)"

    46 abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)"

    47 

    48 value "valif (CIF False) (\<lambda>x. False)"

    49 value "valif (VIF 11) (\<lambda>x. True)"

    50 value "valif (IF (CIF False) (CIF True) (CIF True))"

    51 

    52 primrec bool2if :: "boolex \<Rightarrow> ifex" where

    53 "bool2if (Const b)  = CIF b" |

    54 "bool2if (Var x)    = VIF x" |

    55 "bool2if (Neg b)    = IF (bool2if b) (CIF False) (CIF True)" |

    56 "bool2if (And b c)  = IF (bool2if b) (bool2if c) (CIF False)"

    57 

    58 lemma "valif (bool2if b) env = value2 b env"

    59 apply(induct_tac b)

    60 apply(auto)

    61 done

    62 

    63 primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where

    64 "normif (CIF b)     t e = IF (CIF b) t e" |

    65 "normif (VIF x)     t e = IF (VIF x) t e" |

    66 "normif (IF b t e)  u f = normif b (normif t u f) (normif e u f)"

    67 

    68 primrec norm :: "ifex \<Rightarrow> ifex" where

    69 "norm (CIF b)     = CIF b" |

    70 "norm (VIF x)     = VIF x" |

    71 "norm (IF b t e)  = normif b (norm t) (norm e)"  

    72 

    73 (***************   CHAPTER-3   ********************************)

    74 

    75 lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"

    76 apply simp

    77 done

    78 

    79 lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"

    80 apply (simp (no_asm))

    81 done

    82 

    83 definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where

    84 "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"

    85 

    86 lemma "xor A (\<not>A)"

    87 apply(simp only: xor_def)

    88 apply(simp add: xor_def)

    89 done

    90 

    91 lemma "(let xs = [] in xs@ys@xs) = ys"

    92 apply(simp only: Let_def)

    93 apply(simp add: Let_def)

    94 done

    95 

    96 (* 3.1.8 Conditioal Simplification Rules  *)

    97 

    98 lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"

    99 using [[simp_trace=true]]

   100 apply(case_tac xs)

   101 apply(simp)

   102 apply(simp)

   103 done

   104 

   105 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"

   106 apply(case_tac xs)

   107 using [[simp_trace=true]]

   108 apply(simp)

   109 apply(simp)

   110 done

   111 

   112 (* 3.1.9 Automatic Case Splits  *)

   113 

   114 lemma "\<forall> xs. if xs = [] then rev xs = [] else rev xs \<noteq> []"

   115 apply(split split_if)

   116 apply(simp)

   117 done

   118 

   119 lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"

   120 apply(split list.split)

   121 apply(simp split: list.split)

   122 done

   123 

   124 lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"

   125 apply(split split_if_asm)

   126 apply(simp)

   127 apply(auto)

   128 done

   129 

   130 (* 3.2 Induction Heuristics  *)

   131 

   132 primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   133 "itrev [] ys = ys" |

   134 "itrev (x#xs) ys = itrev xs (x#ys)"

   135 

   136 lemma "itrev xs [] = rev xs"

   137 apply(induct_tac xs)

   138 apply(simp)

   139 apply(auto)

   140 oops

   141 

   142 lemma "itrev xs ys = rev xs @ ys"

   143 apply(induct_tac xs)

   144 apply(simp_all)

   145 oops

   146 

   147 lemma "\<forall> ys. itrev xs ys = rev xs @ ys"

   148 apply(induct_tac xs)

   149 apply(simp)

   150 apply(simp)

   151 done

   152 

   153 primrec add1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   154 "add1 m 0 = m" |

   155 "add1 m (Suc n) = add1 (Suc m) n"

   156 

   157 primrec add2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   158 "add2 m 0 = m" |

   159 "add2 m (Suc n) = Suc (add2 m n)"

   160 

   161 value "add1 1 3"

   162 value "1 + 3"

   163 

   164 lemma abc [simp]: "add1 m 0 = m"

   165 apply(induction m)

   166 apply(simp)

   167 apply(simp)

   168 done

   169 

   170 lemma abc2: "\<forall>m. add1 m n = m + n"

   171 apply(induction n)

   172 apply(simp)

   173 apply(simp del: add1.simps)

   174 apply(simp (no_asm) only: add1.simps)

   175 apply(simp only: )

   176 apply(simp)

   177 done

   178 

   179 thm abc2

   180 

   181 lemma abc3: "add1 m n = m + n"

   182 apply(induction n arbitrary: m)

   183 apply(simp)

   184 apply(simp del: add1.simps)

   185 apply(simp (no_asm) only: add1.simps)

   186 apply(simp only: )

   187 done

   188 

   189 thm abc3

   190 

   191 lemma abc4: "add1 m n = add2 m n"

   192 apply(induction n arbitrary: m)

   193 apply(simp)

   194 apply(simp add: abc3)

   195 done

   196 

   197 find_theorems "_ \<and> _ "

   198 

   199 (* added anottest *)

   200 

   201 lemma abc5: "add2 m n = m + n"

   202 apply(induction n)

   203 apply(simp)

   204 apply(simp)

   205 done

   206 

   207 

   208 (* 3.3 Case Study: Compiling Expressions  *)

   209 

   210 type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"

   211 datatype ('a, 'v)expr = 

   212   Cex 'v

   213 | Vex 'a

   214 | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"

   215 

   216 primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where

   217 "value (Cex v) env = v" |

   218 "value (Vex a) env = env a" |

   219 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"

   220 

   221 value "value (Cex a) (\<lambda>x. True)"

   222 

   223 datatype ('a,'v)instr = 

   224   Const 'v

   225 | Load 'a

   226 | Apply "'v binop"

   227 

   228 primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" where

   229 "exec [] s vs = vs" |

   230 "exec (i#is) s vs = (case i of

   231     Const v \<Rightarrow> exec is s (v#vs)

   232   | Load a \<Rightarrow> exec is s ((s a)#vs)

   233   | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"

   234   

   235 primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where

   236 "compile (Cex v) = [Const v]" |

   237 "compile (Vex a) = [Load a]" |

   238 "compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"

   239 

   240 theorem "exec (compile e) s [] = [value e s]"

   241 (*the theorem needs to be generalized*)

   242 oops

   243 

   244 (*more generalized theorem*)

   245 theorem "\<forall> vs. exec (compile e) s vs = (value e s) # vs"

   246 apply(induct_tac e)

   247 apply(simp)

   248 apply(simp)

   249 oops

   250 

   251 lemma exec_app[simp]: "\<forall> vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"

   252 apply(induct_tac xs)

   253 apply(simp)

   254 apply(simp)

   255 apply(simp split: instr.split)

   256 done

   257 

   258 (* 3.4 Advanced Datatypes  *)

   259 

   260 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" 

   261                 | Sum "'a aexp" "'a aexp"

   262                 | Diff "'a aexp" "'a aexp"

   263                 | Var 'a

   264                 | Num nat

   265 and      'a bexp = Less "'a aexp" "'a aexp"

   266                 | And "'a bexp" "'a bexp"

   267                 | Neg "'a bexp"

   268                 

   269 (*  Total Recursive Functions: Fun  *)

   270 (*  3.5.1 Definition    *)

   271 

   272 fun fib :: "nat \<Rightarrow> nat" where

   273 "fib 0 = 0" |

   274 "fib (Suc 0) = 1" |

   275 "fib (Suc(Suc x)) = fib x + fib (Suc x)"

   276 

   277 value "fib (Suc(Suc(Suc(Suc(Suc 0)))))"

   278 

   279 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   280 "sep a [] = []" |

   281 "sep a [x] = [x]" |

   282 "sep a (x#y#zs) = x # a # sep a (y#zs)"

   283 

   284 fun last :: "'a list \<Rightarrow> 'a" where

   285 "last [x] = x" |

   286 "last (_#y#zs) = last (y#zs)"

   287 

   288 fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   289 "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |

   290 "sep1 _ xs = xs"

   291 

   292 fun swap12:: "'a list \<Rightarrow> 'a list" where

   293 "swap12 (x#y#zs) = y#x#zs" |

   294 "swap12 zs = zs"

   295