1 theory Chap03

     2 imports Main

     3 begin

     4 

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

     6 apply simp

     7 done

     8 

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

    10 apply (simp (no_asm))

    11 done

    12 

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

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

    15 

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

    17 apply(simp only: xor_def)

    18 apply(simp add: xor_def)

    19 done

    20 

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

    22 apply(simp only: Let_def)

    23 apply(simp add: Let_def)

    24 done

    25 

    26 (* 3.1.8 Conditioal Simplification Rules  *)

    27 

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

    29 using [[simp_trace=true]]

    30 apply(case_tac xs)

    31 apply(simp)

    32 apply(simp)

    33 done

    34 

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

    36 apply(case_tac xs)

    37 using [[simp_trace=true]]

    38 apply(simp)

    39 apply(simp)

    40 done

    41 

    42 (* 3.1.9 Automatic Case Splits  *)

    43 

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

    45 apply(split split_if)

    46 apply(simp)

    47 done

    48 

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

    50 apply(split list.split)

    51 apply(simp split: list.split)

    52 done

    53 

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

    55 apply(split split_if_asm)

    56 apply(simp)

    57 apply(auto)

    58 done

    59 

    60 (* 3.2 Induction Heuristics  *)

    61 

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

    63 "itrev [] ys = ys" |

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

    65 

    66 lemma "itrev xs [] = rev xs"

    67 apply(induct_tac xs)

    68 apply(simp)

    69 apply(auto)

    70 oops

    71 

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

    73 apply(induct_tac xs)

    74 apply(simp_all)

    75 oops

    76 

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

    78 apply(induct_tac xs)

    79 apply(simp)

    80 apply(simp)

    81 done

    82 

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

    84 "add1 m 0 = m" |

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

    86 

    87 value "add1 1 3"

    88 value "1 + 3"

    89 

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

    91 apply(induction m)

    92 apply(simp)

    93 apply(simp)

    94 done

    95 

    96 lemma abc2 "add1 m n = m+n"

    97 apply(induction n)

    98 apply(auto)

    99 

   100 oops

   101 

   102 (* 3.3 Case Study: Compiling Expressions  *)

   103 

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

   105 datatype ('a, 'v)expr = 

   106   Cex 'v

   107 | Vex 'a

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

   109 

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

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

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

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

   114 

   115 datatype ('a,'v)instr = 

   116   Const 'v

   117 | Load 'a

   118 | Apply "'v binop"

   119 

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

   121 "exec [] s vs = vs" |

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

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

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

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

   126   

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

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

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

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

   131 

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

   133 (*the theorem needs to be generalized*)

   134 oops

   135 

   136 (*more generalized theorem*)

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

   138 apply(induct_tac e)

   139 apply(simp)

   140 apply(simp)

   141 oops

   142 

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

   144 apply(induct_tac xs)

   145 apply(simp)

   146 apply(simp)

   147 apply(simp split: instr.split)

   148 done

   149 

   150 (* 2.5.6 Case Study: Boolean Expressions *)

   151 

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

   153 | And boolex boolex

   154 

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

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

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

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

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

   160 

   161 value "Const true"

   162 value "Suc(Suc(0))"

   163 

   164 'b::Const = "true"

   165 

   166 value "value2 (Const true) (env = true)"

   167