src/HOL/IMP/Fold.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 44070 cebb7abb54b1 child 44850 a6095c96a89b permissions -rw-r--r--
remove lemma stupid_ext
 kleing@44070 ` 1` ```header "Constant Folding" ``` kleing@44070 ` 2` kleing@44070 ` 3` ```theory Fold imports Sem_Equiv begin ``` kleing@44070 ` 4` kleing@44070 ` 5` ```section "Simple folding of arithmetic expressions" ``` kleing@44070 ` 6` kleing@44070 ` 7` ```types ``` kleing@44070 ` 8` ``` tab = "name \ val option" ``` kleing@44070 ` 9` kleing@44070 ` 10` ```(* maybe better as the composition of substitution and the existing simp_const(0) *) ``` kleing@44070 ` 11` ```fun simp_const :: "aexp \ tab \ aexp" where ``` kleing@44070 ` 12` ```"simp_const (N n) _ = N n" | ``` kleing@44070 ` 13` ```"simp_const (V x) t = (case t x of None \ V x | Some k \ N k)" | ``` kleing@44070 ` 14` ```"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of ``` kleing@44070 ` 15` ``` (N n1, N n2) \ N(n1+n2) | (e1',e2') \ Plus e1' e2')" ``` kleing@44070 ` 16` kleing@44070 ` 17` ```definition "approx t s \ (ALL x k. t x = Some k \ s x = k)" ``` kleing@44070 ` 18` kleing@44070 ` 19` ```theorem aval_simp_const[simp]: ``` kleing@44070 ` 20` ```assumes "approx t s" ``` kleing@44070 ` 21` ```shows "aval (simp_const a t) s = aval a s" ``` kleing@44070 ` 22` ``` using assms ``` kleing@44070 ` 23` ``` by (induct a) (auto simp: approx_def split: aexp.split option.split) ``` kleing@44070 ` 24` kleing@44070 ` 25` ```theorem aval_simp_const_N: ``` kleing@44070 ` 26` ```assumes "approx t s" ``` kleing@44070 ` 27` ```shows "simp_const a t = N n \ aval a s = n" ``` kleing@44070 ` 28` ``` using assms ``` kleing@44070 ` 29` ``` by (induct a arbitrary: n) ``` kleing@44070 ` 30` ``` (auto simp: approx_def split: aexp.splits option.splits) ``` kleing@44070 ` 31` kleing@44070 ` 32` ```definition ``` kleing@44070 ` 33` ``` "merge t1 t2 = (\m. if t1 m = t2 m then t1 m else None)" ``` kleing@44070 ` 34` kleing@44070 ` 35` ```primrec lnames :: "com \ name set" where ``` kleing@44070 ` 36` ```"lnames SKIP = {}" | ``` kleing@44070 ` 37` ```"lnames (x ::= a) = {x}" | ``` kleing@44070 ` 38` ```"lnames (c1; c2) = lnames c1 \ lnames c2" | ``` kleing@44070 ` 39` ```"lnames (IF b THEN c1 ELSE c2) = lnames c1 \ lnames c2" | ``` kleing@44070 ` 40` ```"lnames (WHILE b DO c) = lnames c" ``` kleing@44070 ` 41` kleing@44070 ` 42` ```primrec "defs" :: "com \ tab \ tab" where ``` kleing@44070 ` 43` ```"defs SKIP t = t" | ``` kleing@44070 ` 44` ```"defs (x ::= a) t = ``` kleing@44070 ` 45` ``` (case simp_const a t of N k \ t(x \ k) | _ \ t(x:=None))" | ``` kleing@44070 ` 46` ```"defs (c1;c2) t = (defs c2 o defs c1) t" | ``` kleing@44070 ` 47` ```"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" | ``` kleing@44070 ` 48` ```"defs (WHILE b DO c) t = t |` (-lnames c)" ``` kleing@44070 ` 49` kleing@44070 ` 50` ```primrec fold where ``` kleing@44070 ` 51` ```"fold SKIP _ = SKIP" | ``` kleing@44070 ` 52` ```"fold (x ::= a) t = (x ::= (simp_const a t))" | ``` kleing@44070 ` 53` ```"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" | ``` kleing@44070 ` 54` ```"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" | ``` kleing@44070 ` 55` ```"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))" ``` kleing@44070 ` 56` kleing@44070 ` 57` ```lemma approx_merge: ``` kleing@44070 ` 58` ``` "approx t1 s \ approx t2 s \ approx (merge t1 t2) s" ``` kleing@44070 ` 59` ``` by (fastsimp simp: merge_def approx_def) ``` kleing@44070 ` 60` kleing@44070 ` 61` ```lemma approx_map_le: ``` kleing@44070 ` 62` ``` "approx t2 s \ t1 \\<^sub>m t2 \ approx t1 s" ``` kleing@44070 ` 63` ``` by (clarsimp simp: approx_def map_le_def dom_def) ``` kleing@44070 ` 64` kleing@44070 ` 65` ```lemma restrict_map_le [intro!, simp]: "t |` S \\<^sub>m t" ``` kleing@44070 ` 66` ``` by (clarsimp simp: restrict_map_def map_le_def) ``` kleing@44070 ` 67` kleing@44070 ` 68` ```lemma merge_restrict: ``` kleing@44070 ` 69` ``` assumes "t1 |` S = t |` S" ``` kleing@44070 ` 70` ``` assumes "t2 |` S = t |` S" ``` kleing@44070 ` 71` ``` shows "merge t1 t2 |` S = t |` S" ``` kleing@44070 ` 72` ```proof - ``` kleing@44070 ` 73` ``` from assms ``` kleing@44070 ` 74` ``` have "\x. (t1 |` S) x = (t |` S) x" ``` kleing@44070 ` 75` ``` and "\x. (t2 |` S) x = (t |` S) x" by auto ``` kleing@44070 ` 76` ``` thus ?thesis ``` kleing@44070 ` 77` ``` by (auto simp: merge_def restrict_map_def ``` kleing@44070 ` 78` ``` split: if_splits intro: ext) ``` kleing@44070 ` 79` ```qed ``` kleing@44070 ` 80` kleing@44070 ` 81` kleing@44070 ` 82` ```lemma defs_restrict: ``` kleing@44070 ` 83` ``` "defs c t |` (- lnames c) = t |` (- lnames c)" ``` kleing@44070 ` 84` ```proof (induct c arbitrary: t) ``` kleing@44070 ` 85` ``` case (Semi c1 c2) ``` kleing@44070 ` 86` ``` hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" ``` kleing@44070 ` 87` ``` by simp ``` kleing@44070 ` 88` ``` hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = ``` kleing@44070 ` 89` ``` t |` (- lnames c1) |` (-lnames c2)" by simp ``` kleing@44070 ` 90` ``` moreover ``` kleing@44070 ` 91` ``` from Semi ``` kleing@44070 ` 92` ``` have "defs c2 (defs c1 t) |` (- lnames c2) = ``` kleing@44070 ` 93` ``` defs c1 t |` (- lnames c2)" ``` kleing@44070 ` 94` ``` by simp ``` kleing@44070 ` 95` ``` hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) = ``` kleing@44070 ` 96` ``` defs c1 t |` (- lnames c2) |` (- lnames c1)" ``` kleing@44070 ` 97` ``` by simp ``` kleing@44070 ` 98` ``` ultimately ``` kleing@44070 ` 99` ``` show ?case by (clarsimp simp: Int_commute) ``` kleing@44070 ` 100` ```next ``` kleing@44070 ` 101` ``` case (If b c1 c2) ``` kleing@44070 ` 102` ``` hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp ``` kleing@44070 ` 103` ``` hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = ``` kleing@44070 ` 104` ``` t |` (- lnames c1) |` (-lnames c2)" by simp ``` kleing@44070 ` 105` ``` moreover ``` kleing@44070 ` 106` ``` from If ``` kleing@44070 ` 107` ``` have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp ``` kleing@44070 ` 108` ``` hence "defs c2 t |` (- lnames c2) |` (-lnames c1) = ``` kleing@44070 ` 109` ``` t |` (- lnames c2) |` (-lnames c1)" by simp ``` kleing@44070 ` 110` ``` ultimately ``` kleing@44070 ` 111` ``` show ?case by (auto simp: Int_commute intro: merge_restrict) ``` kleing@44070 ` 112` ```qed (auto split: aexp.split) ``` kleing@44070 ` 113` kleing@44070 ` 114` kleing@44070 ` 115` ```lemma big_step_pres_approx: ``` kleing@44070 ` 116` ``` "(c,s) \ s' \ approx t s \ approx (defs c t) s'" ``` kleing@44070 ` 117` ```proof (induct arbitrary: t rule: big_step_induct) ``` kleing@44070 ` 118` ``` case Skip thus ?case by simp ``` kleing@44070 ` 119` ```next ``` kleing@44070 ` 120` ``` case Assign ``` kleing@44070 ` 121` ``` thus ?case ``` kleing@44070 ` 122` ``` by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) ``` kleing@44070 ` 123` ```next ``` kleing@44070 ` 124` ``` case (Semi c1 s1 s2 c2 s3) ``` kleing@44070 ` 125` ``` have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems]) ``` kleing@44070 ` 126` ``` hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4)) ``` kleing@44070 ` 127` ``` thus ?case by simp ``` kleing@44070 ` 128` ```next ``` kleing@44070 ` 129` ``` case (IfTrue b s c1 s') ``` kleing@44070 ` 130` ``` hence "approx (defs c1 t) s'" by simp ``` kleing@44070 ` 131` ``` thus ?case by (simp add: approx_merge) ``` kleing@44070 ` 132` ```next ``` kleing@44070 ` 133` ``` case (IfFalse b s c2 s') ``` kleing@44070 ` 134` ``` hence "approx (defs c2 t) s'" by simp ``` kleing@44070 ` 135` ``` thus ?case by (simp add: approx_merge) ``` kleing@44070 ` 136` ```next ``` kleing@44070 ` 137` ``` case WhileFalse ``` kleing@44070 ` 138` ``` thus ?case by (simp add: approx_def restrict_map_def) ``` kleing@44070 ` 139` ```next ``` kleing@44070 ` 140` ``` case (WhileTrue b s1 c s2 s3) ``` kleing@44070 ` 141` ``` hence "approx (defs c t) s2" by simp ``` kleing@44070 ` 142` ``` with WhileTrue ``` kleing@44070 ` 143` ``` have "approx (defs c t |` (-lnames c)) s3" by simp ``` kleing@44070 ` 144` ``` thus ?case by (simp add: defs_restrict) ``` kleing@44070 ` 145` ```qed ``` kleing@44070 ` 146` kleing@44070 ` 147` ```corollary approx_defs_inv [simp]: ``` kleing@44070 ` 148` ``` "\ {approx t} c {approx (defs c t)}" ``` kleing@44070 ` 149` ``` by (simp add: hoare_valid_def big_step_pres_approx) ``` kleing@44070 ` 150` kleing@44070 ` 151` kleing@44070 ` 152` ```lemma big_step_pres_approx_restrict: ``` kleing@44070 ` 153` ``` "(c,s) \ s' \ approx (t |` (-lnames c)) s \ approx (t |` (-lnames c)) s'" ``` kleing@44070 ` 154` ```proof (induct arbitrary: t rule: big_step_induct) ``` kleing@44070 ` 155` ``` case Assign ``` kleing@44070 ` 156` ``` thus ?case by (clarsimp simp: approx_def) ``` kleing@44070 ` 157` ```next ``` kleing@44070 ` 158` ``` case (Semi c1 s1 s2 c2 s3) ``` kleing@44070 ` 159` ``` hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" ``` kleing@44070 ` 160` ``` by (simp add: Int_commute) ``` kleing@44070 ` 161` ``` hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2" ``` kleing@44070 ` 162` ``` by (rule Semi) ``` kleing@44070 ` 163` ``` hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2" ``` kleing@44070 ` 164` ``` by (simp add: Int_commute) ``` kleing@44070 ` 165` ``` hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3" ``` kleing@44070 ` 166` ``` by (rule Semi) ``` kleing@44070 ` 167` ``` thus ?case by simp ``` kleing@44070 ` 168` ```next ``` kleing@44070 ` 169` ``` case (IfTrue b s c1 s' c2) ``` kleing@44070 ` 170` ``` hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" ``` kleing@44070 ` 171` ``` by (simp add: Int_commute) ``` kleing@44070 ` 172` ``` hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'" ``` kleing@44070 ` 173` ``` by (rule IfTrue) ``` kleing@44070 ` 174` ``` thus ?case by (simp add: Int_commute) ``` kleing@44070 ` 175` ```next ``` kleing@44070 ` 176` ``` case (IfFalse b s c2 s' c1) ``` kleing@44070 ` 177` ``` hence "approx (t |` (-lnames c1) |` (-lnames c2)) s" ``` kleing@44070 ` 178` ``` by simp ``` kleing@44070 ` 179` ``` hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'" ``` kleing@44070 ` 180` ``` by (rule IfFalse) ``` kleing@44070 ` 181` ``` thus ?case by simp ``` kleing@44070 ` 182` ```qed auto ``` kleing@44070 ` 183` kleing@44070 ` 184` kleing@44070 ` 185` ```lemma approx_restrict_inv: ``` kleing@44070 ` 186` ``` "\ {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}" ``` kleing@44070 ` 187` ``` by (simp add: hoare_valid_def big_step_pres_approx_restrict) ``` kleing@44070 ` 188` kleing@44070 ` 189` ```declare assign_simp [simp] ``` kleing@44070 ` 190` kleing@44070 ` 191` ```lemma approx_eq: ``` kleing@44070 ` 192` ``` "approx t \ c \ fold c t" ``` kleing@44070 ` 193` ```proof (induct c arbitrary: t) ``` kleing@44070 ` 194` ``` case SKIP show ?case by simp ``` kleing@44070 ` 195` ```next ``` kleing@44070 ` 196` ``` case Assign ``` kleing@44070 ` 197` ``` show ?case by (simp add: equiv_up_to_def) ``` kleing@44070 ` 198` ```next ``` kleing@44070 ` 199` ``` case Semi ``` kleing@44070 ` 200` ``` thus ?case by (auto intro!: equiv_up_to_semi) ``` kleing@44070 ` 201` ```next ``` kleing@44070 ` 202` ``` case If ``` kleing@44070 ` 203` ``` thus ?case by (auto intro!: equiv_up_to_if_weak) ``` kleing@44070 ` 204` ```next ``` kleing@44070 ` 205` ``` case (While b c) ``` kleing@44070 ` 206` ``` hence "approx (t |` (- lnames c)) \ ``` kleing@44070 ` 207` ``` WHILE b DO c \ WHILE b DO fold c (t |` (- lnames c))" ``` kleing@44070 ` 208` ``` by (auto intro: equiv_up_to_while_weak approx_restrict_inv) ``` kleing@44070 ` 209` ``` thus ?case ``` kleing@44070 ` 210` ``` by (auto intro: equiv_up_to_weaken approx_map_le) ``` kleing@44070 ` 211` ```qed ``` kleing@44070 ` 212` ``` ``` kleing@44070 ` 213` kleing@44070 ` 214` ```lemma approx_empty [simp]: ``` kleing@44070 ` 215` ``` "approx empty = (\_. True)" ``` kleing@44070 ` 216` ``` by (auto intro!: ext simp: approx_def) ``` kleing@44070 ` 217` kleing@44070 ` 218` ```lemma equiv_sym: ``` kleing@44070 ` 219` ``` "c \ c' \ c' \ c" ``` kleing@44070 ` 220` ``` by (auto simp add: equiv_def) ``` kleing@44070 ` 221` kleing@44070 ` 222` ```theorem constant_folding_equiv: ``` kleing@44070 ` 223` ``` "fold c empty \ c" ``` kleing@44070 ` 224` ``` using approx_eq [of empty c] ``` kleing@44070 ` 225` ``` by (simp add: equiv_up_to_True equiv_sym) ``` kleing@44070 ` 226` kleing@44070 ` 227` kleing@44070 ` 228` kleing@44070 ` 229` ```section {* More ambitious folding including boolean expressions *} ``` kleing@44070 ` 230` kleing@44070 ` 231` kleing@44070 ` 232` ```fun bsimp_const :: "bexp \ tab \ bexp" where ``` kleing@44070 ` 233` ```"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" | ``` kleing@44070 ` 234` ```"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" | ``` kleing@44070 ` 235` ```"bsimp_const (Not b) t = not(bsimp_const b t)" | ``` kleing@44070 ` 236` ```"bsimp_const (B bv) _ = B bv" ``` kleing@44070 ` 237` kleing@44070 ` 238` ```theorem bvalsimp_const [simp]: ``` kleing@44070 ` 239` ``` assumes "approx t s" ``` kleing@44070 ` 240` ``` shows "bval (bsimp_const b t) s = bval b s" ``` kleing@44070 ` 241` ``` using assms by (induct b) auto ``` kleing@44070 ` 242` kleing@44070 ` 243` ```lemma not_B [simp]: "not (B v) = B (\v)" ``` kleing@44070 ` 244` ``` by (cases v) auto ``` kleing@44070 ` 245` kleing@44070 ` 246` ```lemma not_B_eq [simp]: "(not b = B v) = (b = B (\v))" ``` kleing@44070 ` 247` ``` by (cases b) auto ``` kleing@44070 ` 248` kleing@44070 ` 249` ```lemma and_B_eq: ``` kleing@44070 ` 250` ``` "(and a b = B v) = (a = B False \ \v \ ``` kleing@44070 ` 251` ``` b = B False \ \v \ ``` kleing@44070 ` 252` ``` (\v1 v2. a = B v1 \ b = B v2 \ v = v1 \ v2))" ``` kleing@44070 ` 253` ``` by (rule and.induct) auto ``` kleing@44070 ` 254` kleing@44070 ` 255` ```lemma less_B_eq [simp]: ``` kleing@44070 ` 256` ``` "(less a b = B v) = (\n1 n2. a = N n1 \ b = N n2 \ v = (n1 < n2))" ``` kleing@44070 ` 257` ``` by (rule less.induct) auto ``` kleing@44070 ` 258` ``` ``` kleing@44070 ` 259` ```theorem bvalsimp_const_B: ``` kleing@44070 ` 260` ```assumes "approx t s" ``` kleing@44070 ` 261` ```shows "bsimp_const b t = B v \ bval b s = v" ``` kleing@44070 ` 262` ``` using assms ``` kleing@44070 ` 263` ``` by (induct b arbitrary: v) ``` kleing@44070 ` 264` ``` (auto simp: approx_def and_B_eq aval_simp_const_N ``` kleing@44070 ` 265` ``` split: bexp.splits bool.splits) ``` kleing@44070 ` 266` kleing@44070 ` 267` kleing@44070 ` 268` ```primrec "bdefs" :: "com \ tab \ tab" where ``` kleing@44070 ` 269` ```"bdefs SKIP t = t" | ``` kleing@44070 ` 270` ```"bdefs (x ::= a) t = ``` kleing@44070 ` 271` ``` (case simp_const a t of N k \ t(x \ k) | _ \ t(x:=None))" | ``` kleing@44070 ` 272` ```"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" | ``` kleing@44070 ` 273` ```"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of ``` kleing@44070 ` 274` ``` B True \ bdefs c1 t ``` kleing@44070 ` 275` ``` | B False \ bdefs c2 t ``` kleing@44070 ` 276` ``` | _ \ merge (bdefs c1 t) (bdefs c2 t))" | ``` kleing@44070 ` 277` ```"bdefs (WHILE b DO c) t = t |` (-lnames c)" ``` kleing@44070 ` 278` kleing@44070 ` 279` kleing@44070 ` 280` ```primrec bfold where ``` kleing@44070 ` 281` ```"bfold SKIP _ = SKIP" | ``` kleing@44070 ` 282` ```"bfold (x ::= a) t = (x ::= (simp_const a t))" | ``` kleing@44070 ` 283` ```"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" | ``` kleing@44070 ` 284` ```"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of ``` kleing@44070 ` 285` ``` B True \ bfold c1 t ``` kleing@44070 ` 286` ``` | B False \ bfold c2 t ``` kleing@44070 ` 287` ``` | _ \ IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" | ``` kleing@44070 ` 288` ```"bfold (WHILE b DO c) t = (case bsimp_const b t of ``` kleing@44070 ` 289` ``` B False \ SKIP ``` kleing@44070 ` 290` ``` | _ \ WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))" ``` kleing@44070 ` 291` kleing@44070 ` 292` kleing@44070 ` 293` ```lemma bdefs_restrict: ``` kleing@44070 ` 294` ``` "bdefs c t |` (- lnames c) = t |` (- lnames c)" ``` kleing@44070 ` 295` ```proof (induct c arbitrary: t) ``` kleing@44070 ` 296` ``` case (Semi c1 c2) ``` kleing@44070 ` 297` ``` hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" ``` kleing@44070 ` 298` ``` by simp ``` kleing@44070 ` 299` ``` hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = ``` kleing@44070 ` 300` ``` t |` (- lnames c1) |` (-lnames c2)" by simp ``` kleing@44070 ` 301` ``` moreover ``` kleing@44070 ` 302` ``` from Semi ``` kleing@44070 ` 303` ``` have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = ``` kleing@44070 ` 304` ``` bdefs c1 t |` (- lnames c2)" ``` kleing@44070 ` 305` ``` by simp ``` kleing@44070 ` 306` ``` hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) = ``` kleing@44070 ` 307` ``` bdefs c1 t |` (- lnames c2) |` (- lnames c1)" ``` kleing@44070 ` 308` ``` by simp ``` kleing@44070 ` 309` ``` ultimately ``` kleing@44070 ` 310` ``` show ?case by (clarsimp simp: Int_commute) ``` kleing@44070 ` 311` ```next ``` kleing@44070 ` 312` ``` case (If b c1 c2) ``` kleing@44070 ` 313` ``` hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp ``` kleing@44070 ` 314` ``` hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = ``` kleing@44070 ` 315` ``` t |` (- lnames c1) |` (-lnames c2)" by simp ``` kleing@44070 ` 316` ``` moreover ``` kleing@44070 ` 317` ``` from If ``` kleing@44070 ` 318` ``` have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp ``` kleing@44070 ` 319` ``` hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) = ``` kleing@44070 ` 320` ``` t |` (- lnames c2) |` (-lnames c1)" by simp ``` kleing@44070 ` 321` ``` ultimately ``` kleing@44070 ` 322` ``` show ?case ``` kleing@44070 ` 323` ``` by (auto simp: Int_commute intro: merge_restrict ``` kleing@44070 ` 324` ``` split: bexp.splits bool.splits) ``` kleing@44070 ` 325` ```qed (auto split: aexp.split bexp.split bool.split) ``` kleing@44070 ` 326` kleing@44070 ` 327` kleing@44070 ` 328` ```lemma big_step_pres_approx_b: ``` kleing@44070 ` 329` ``` "(c,s) \ s' \ approx t s \ approx (bdefs c t) s'" ``` kleing@44070 ` 330` ```proof (induct arbitrary: t rule: big_step_induct) ``` kleing@44070 ` 331` ``` case Skip thus ?case by simp ``` kleing@44070 ` 332` ```next ``` kleing@44070 ` 333` ``` case Assign ``` kleing@44070 ` 334` ``` thus ?case ``` kleing@44070 ` 335` ``` by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split) ``` kleing@44070 ` 336` ```next ``` kleing@44070 ` 337` ``` case (Semi c1 s1 s2 c2 s3) ``` kleing@44070 ` 338` ``` have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems]) ``` kleing@44070 ` 339` ``` hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4)) ``` kleing@44070 ` 340` ``` thus ?case by simp ``` kleing@44070 ` 341` ```next ``` kleing@44070 ` 342` ``` case (IfTrue b s c1 s') ``` kleing@44070 ` 343` ``` hence "approx (bdefs c1 t) s'" by simp ``` kleing@44070 ` 344` ``` thus ?case using `bval b s` `approx t s` ``` kleing@44070 ` 345` ``` by (clarsimp simp: approx_merge bvalsimp_const_B ``` kleing@44070 ` 346` ``` split: bexp.splits bool.splits) ``` kleing@44070 ` 347` ```next ``` kleing@44070 ` 348` ``` case (IfFalse b s c2 s') ``` kleing@44070 ` 349` ``` hence "approx (bdefs c2 t) s'" by simp ``` kleing@44070 ` 350` ``` thus ?case using `\bval b s` `approx t s` ``` kleing@44070 ` 351` ``` by (clarsimp simp: approx_merge bvalsimp_const_B ``` kleing@44070 ` 352` ``` split: bexp.splits bool.splits) ``` kleing@44070 ` 353` ```next ``` kleing@44070 ` 354` ``` case WhileFalse ``` kleing@44070 ` 355` ``` thus ?case ``` kleing@44070 ` 356` ``` by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def ``` kleing@44070 ` 357` ``` split: bexp.splits bool.splits) ``` kleing@44070 ` 358` ```next ``` kleing@44070 ` 359` ``` case (WhileTrue b s1 c s2 s3) ``` kleing@44070 ` 360` ``` hence "approx (bdefs c t) s2" by simp ``` kleing@44070 ` 361` ``` with WhileTrue ``` kleing@44070 ` 362` ``` have "approx (bdefs c t |` (- lnames c)) s3" ``` kleing@44070 ` 363` ``` by simp ``` kleing@44070 ` 364` ``` thus ?case ``` kleing@44070 ` 365` ``` by (simp add: bdefs_restrict) ``` kleing@44070 ` 366` ```qed ``` kleing@44070 ` 367` kleing@44070 ` 368` ```corollary approx_bdefs_inv [simp]: ``` kleing@44070 ` 369` ``` "\ {approx t} c {approx (bdefs c t)}" ``` kleing@44070 ` 370` ``` by (simp add: hoare_valid_def big_step_pres_approx_b) ``` kleing@44070 ` 371` kleing@44070 ` 372` ```lemma bfold_equiv: ``` kleing@44070 ` 373` ``` "approx t \ c \ bfold c t" ``` kleing@44070 ` 374` ```proof (induct c arbitrary: t) ``` kleing@44070 ` 375` ``` case SKIP show ?case by simp ``` kleing@44070 ` 376` ```next ``` kleing@44070 ` 377` ``` case Assign ``` kleing@44070 ` 378` ``` thus ?case by (simp add: equiv_up_to_def) ``` kleing@44070 ` 379` ```next ``` kleing@44070 ` 380` ``` case Semi ``` kleing@44070 ` 381` ``` thus ?case by (auto intro!: equiv_up_to_semi) ``` kleing@44070 ` 382` ```next ``` kleing@44070 ` 383` ``` case (If b c1 c2) ``` kleing@44070 ` 384` ``` hence "approx t \ IF b THEN c1 ELSE c2 \ ``` kleing@44070 ` 385` ``` IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t" ``` kleing@44070 ` 386` ``` by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) ``` kleing@44070 ` 387` ``` thus ?case using If ``` kleing@44070 ` 388` ``` by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits ``` kleing@44070 ` 389` ``` intro: equiv_up_to_trans) ``` kleing@44070 ` 390` ``` next ``` kleing@44070 ` 391` ``` case (While b c) ``` kleing@44070 ` 392` ``` hence "approx (t |` (- lnames c)) \ ``` kleing@44070 ` 393` ``` WHILE b DO c \ ``` kleing@44070 ` 394` ``` WHILE bsimp_const b (t |` (- lnames c)) ``` kleing@44070 ` 395` ``` DO bfold c (t |` (- lnames c))" (is "_ \ ?W \ ?W'") ``` kleing@44070 ` 396` ``` by (auto intro: equiv_up_to_while_weak approx_restrict_inv ``` kleing@44070 ` 397` ``` simp: bequiv_up_to_def) ``` kleing@44070 ` 398` ``` hence "approx t \ ?W \ ?W'" ``` kleing@44070 ` 399` ``` by (auto intro: equiv_up_to_weaken approx_map_le) ``` kleing@44070 ` 400` ``` thus ?case ``` kleing@44070 ` 401` ``` by (auto split: bexp.splits bool.splits ``` kleing@44070 ` 402` ``` intro: equiv_up_to_while_False ``` kleing@44070 ` 403` ``` simp: bvalsimp_const_B) ``` kleing@44070 ` 404` ```qed ``` kleing@44070 ` 405` kleing@44070 ` 406` kleing@44070 ` 407` ```theorem constant_bfolding_equiv: ``` kleing@44070 ` 408` ``` "bfold c empty \ c" ``` kleing@44070 ` 409` ``` using bfold_equiv [of empty c] ``` kleing@44070 ` 410` ``` by (simp add: equiv_up_to_True equiv_sym) ``` kleing@44070 ` 411` kleing@44070 ` 412` kleing@44070 ` 413` ```end ```