src/HOL/IMP/Live.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 28867 3d9873c4c409 child 32960 69916a850301 permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
 nipkow@28583 ` 1` ```theory Live imports Natural ``` nipkow@28583 ` 2` ```begin ``` nipkow@28583 ` 3` nipkow@28583 ` 4` ```text{* Which variables/locations does an expression depend on? ``` nipkow@28583 ` 5` ```Any set of variables that completely determine the value of the expression, ``` nipkow@28583 ` 6` ```in the worst case all locations: *} ``` nipkow@28583 ` 7` nipkow@28583 ` 8` ```consts Dep :: "((loc \ 'a) \ 'b) \ loc set" ``` nipkow@28583 ` 9` ```specification (Dep) ``` nipkow@28583 ` 10` ```dep_on: "(\x\Dep e. s x = t x) \ e s = e t" ``` nipkow@28583 ` 11` ```by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric]) ``` nipkow@28583 ` 12` nipkow@28583 ` 13` ```text{* The following definition of @{const Dep} looks very tempting ``` nipkow@28583 ` 14` ```@{prop"Dep e = {a. EX s t. (ALL x. x\a \ s x = t x) \ e s \ e t}"} ``` nipkow@28583 ` 15` ```but does not work in case @{text e} depends on an infinite set of variables. ``` nipkow@28583 ` 16` ```For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set! ``` nipkow@28583 ` 17` nipkow@28583 ` 18` ```If we had a concrete representation of expressions, we would simply write ``` nipkow@28583 ` 19` ```a recursive free-variables function. ``` nipkow@28583 ` 20` ```*} ``` nipkow@28583 ` 21` nipkow@28583 ` 22` ```primrec L :: "com \ loc set \ loc set" where ``` nipkow@28583 ` 23` ```"L SKIP A = A" | ``` nipkow@28583 ` 24` ```"L (x :== e) A = A-{x} \ Dep e" | ``` nipkow@28583 ` 25` ```"L (c1; c2) A = (L c1 \ L c2) A" | ``` nipkow@28583 ` 26` ```"L (IF b THEN c1 ELSE c2) A = Dep b \ L c1 A \ L c2 A" | ``` nipkow@28583 ` 27` ```"L (WHILE b DO c) A = Dep b \ A \ L c A" ``` nipkow@28583 ` 28` nipkow@28583 ` 29` ```primrec "kill" :: "com \ loc set" where ``` nipkow@28583 ` 30` ```"kill SKIP = {}" | ``` nipkow@28583 ` 31` ```"kill (x :== e) = {x}" | ``` nipkow@28583 ` 32` ```"kill (c1; c2) = kill c1 \ kill c2" | ``` nipkow@28583 ` 33` ```"kill (IF b THEN c1 ELSE c2) = Dep b \ kill c1 \ kill c2" | ``` nipkow@28583 ` 34` ```"kill (WHILE b DO c) = {}" ``` nipkow@28583 ` 35` nipkow@28583 ` 36` ```primrec gen :: "com \ loc set" where ``` nipkow@28583 ` 37` ```"gen SKIP = {}" | ``` nipkow@28583 ` 38` ```"gen (x :== e) = Dep e" | ``` nipkow@28583 ` 39` ```"gen (c1; c2) = gen c1 \ (gen c2-kill c1)" | ``` nipkow@28583 ` 40` ```"gen (IF b THEN c1 ELSE c2) = Dep b \ gen c1 \ gen c2" | ``` nipkow@28583 ` 41` ```"gen (WHILE b DO c) = Dep b \ gen c" ``` nipkow@28583 ` 42` nipkow@28583 ` 43` ```lemma L_gen_kill: "L c A = gen c \ (A - kill c)" ``` nipkow@28583 ` 44` ```by(induct c arbitrary:A) auto ``` nipkow@28583 ` 45` nipkow@28583 ` 46` ```lemma L_idemp: "L c (L c A) \ L c A" ``` nipkow@28583 ` 47` ```by(fastsimp simp add:L_gen_kill) ``` nipkow@28583 ` 48` nipkow@28583 ` 49` ```theorem L_sound: "\ x \ L c A. s x = t x \ \c,s\ \\<^sub>c s' \ \c,t\ \\<^sub>c t' \ ``` nipkow@28583 ` 50` ``` \x\A. s' x = t' x" ``` nipkow@28583 ` 51` ```proof (induct c arbitrary: A s t s' t') ``` nipkow@28583 ` 52` ``` case SKIP then show ?case by auto ``` nipkow@28583 ` 53` ```next ``` nipkow@28583 ` 54` ``` case (Assign x e) then show ?case ``` nipkow@28583 ` 55` ``` by (auto simp:update_def ball_Un dest!: dep_on) ``` nipkow@28583 ` 56` ```next ``` nipkow@28583 ` 57` ``` case (Semi c1 c2) ``` nipkow@28583 ` 58` ``` from Semi(4) obtain s'' where s1: "\c1,s\ \\<^sub>c s''" and s2: "\c2,s''\ \\<^sub>c s'" ``` nipkow@28583 ` 59` ``` by auto ``` nipkow@28583 ` 60` ``` from Semi(5) obtain t'' where t1: "\c1,t\ \\<^sub>c t''" and t2: "\c2,t''\ \\<^sub>c t'" ``` nipkow@28583 ` 61` ``` by auto ``` nipkow@28583 ` 62` ``` show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp ``` nipkow@28583 ` 63` ```next ``` nipkow@28583 ` 64` ``` case (Cond b c1 c2) ``` nipkow@28583 ` 65` ``` show ?case ``` nipkow@28583 ` 66` ``` proof cases ``` nipkow@28583 ` 67` ``` assume "b s" ``` nipkow@28583 ` 68` ``` hence s: "\c1,s\ \\<^sub>c s'" using Cond(4) by simp ``` nipkow@28583 ` 69` ``` have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28583 ` 70` ``` hence t: "\c1,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28583 ` 71` ``` show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28583 ` 72` ``` next ``` nipkow@28583 ` 73` ``` assume "\ b s" ``` nipkow@28583 ` 74` ``` hence s: "\c2,s\ \\<^sub>c s'" using Cond(4) by auto ``` nipkow@28583 ` 75` ``` have "\ b t" using `\ b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28583 ` 76` ``` hence t: "\c2,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28583 ` 77` ``` show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28583 ` 78` ``` qed ``` nipkow@28583 ` 79` ```next ``` nipkow@28583 ` 80` ``` case (While b c) note IH = this ``` nipkow@28583 ` 81` ``` { fix cw ``` nipkow@28583 ` 82` ``` have "\cw,s\ \\<^sub>c s' \ cw = (While b c) \ \cw,t\ \\<^sub>c t' \ ``` nipkow@28583 ` 83` ``` \ x \ L cw A. s x = t x \ \x\A. s' x = t' x" ``` nipkow@28583 ` 84` ``` proof (induct arbitrary: t A pred:evalc) ``` nipkow@28583 ` 85` ``` case WhileFalse ``` nipkow@28583 ` 86` ``` have "\ b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28583 ` 87` ``` then have "t' = t" using WhileFalse by auto ``` nipkow@28583 ` 88` ``` then show ?case using WhileFalse by auto ``` nipkow@28583 ` 89` ``` next ``` nipkow@28583 ` 90` ``` case (WhileTrue _ s _ s'' s') ``` nipkow@28583 ` 91` ``` have "\c,s\ \\<^sub>c s''" using WhileTrue(2,6) by simp ``` nipkow@28583 ` 92` ``` have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28583 ` 93` ``` then obtain t'' where "\c,t\ \\<^sub>c t''" and "\While b c,t''\ \\<^sub>c t'" ``` nipkow@28583 ` 94` ``` using WhileTrue(6,7) by auto ``` nipkow@28867 ` 95` ``` have "\x\Dep b \ A \ L c A. s'' x = t'' x" ``` nipkow@28867 ` 96` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` `\c,t\ \\<^sub>c t''`] WhileTrue(6,8) ``` nipkow@28867 ` 97` ``` by (auto simp:L_gen_kill) ``` nipkow@28867 ` 98` ``` moreover then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@28867 ` 99` ``` ultimately show ?case using WhileTrue(5,6) `\While b c,t''\ \\<^sub>c t'` by metis ``` nipkow@28583 ` 100` ``` qed auto } ``` nipkow@28583 ` 101` ``` from this[OF IH(3) _ IH(4,2)] show ?case by metis ``` nipkow@28583 ` 102` ```qed ``` nipkow@28583 ` 103` nipkow@28867 ` 104` nipkow@28867 ` 105` ```primrec bury :: "com \ loc set \ com" where ``` nipkow@28867 ` 106` ```"bury SKIP _ = SKIP" | ``` nipkow@28867 ` 107` ```"bury (x :== e) A = (if x:A then x:== e else SKIP)" | ``` nipkow@28867 ` 108` ```"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" | ``` nipkow@28867 ` 109` ```"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" | ``` nipkow@28867 ` 110` ```"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \ A \ L c A))" ``` nipkow@28867 ` 111` nipkow@28867 ` 112` ```theorem bury_sound: ``` nipkow@28867 ` 113` ``` "\ x \ L c A. s x = t x \ \c,s\ \\<^sub>c s' \ \bury c A,t\ \\<^sub>c t' \ ``` nipkow@28867 ` 114` ``` \x\A. s' x = t' x" ``` nipkow@28867 ` 115` ```proof (induct c arbitrary: A s t s' t') ``` nipkow@28867 ` 116` ``` case SKIP then show ?case by auto ``` nipkow@28867 ` 117` ```next ``` nipkow@28867 ` 118` ``` case (Assign x e) then show ?case ``` nipkow@28867 ` 119` ``` by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on) ``` nipkow@28867 ` 120` ```next ``` nipkow@28867 ` 121` ``` case (Semi c1 c2) ``` nipkow@28867 ` 122` ``` from Semi(4) obtain s'' where s1: "\c1,s\ \\<^sub>c s''" and s2: "\c2,s''\ \\<^sub>c s'" ``` nipkow@28867 ` 123` ``` by auto ``` nipkow@28867 ` 124` ``` from Semi(5) obtain t'' where t1: "\bury c1 (L c2 A),t\ \\<^sub>c t''" and t2: "\bury c2 A,t''\ \\<^sub>c t'" ``` nipkow@28867 ` 125` ``` by auto ``` nipkow@28867 ` 126` ``` show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp ``` nipkow@28867 ` 127` ```next ``` nipkow@28867 ` 128` ``` case (Cond b c1 c2) ``` nipkow@28867 ` 129` ``` show ?case ``` nipkow@28867 ` 130` ``` proof cases ``` nipkow@28867 ` 131` ``` assume "b s" ``` nipkow@28867 ` 132` ``` hence s: "\c1,s\ \\<^sub>c s'" using Cond(4) by simp ``` nipkow@28867 ` 133` ``` have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28867 ` 134` ``` hence t: "\bury c1 A,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28867 ` 135` ``` show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28867 ` 136` ``` next ``` nipkow@28867 ` 137` ``` assume "\ b s" ``` nipkow@28867 ` 138` ``` hence s: "\c2,s\ \\<^sub>c s'" using Cond(4) by auto ``` nipkow@28867 ` 139` ``` have "\ b t" using `\ b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28867 ` 140` ``` hence t: "\bury c2 A,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28867 ` 141` ``` show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28867 ` 142` ``` qed ``` nipkow@28867 ` 143` ```next ``` nipkow@28867 ` 144` ``` case (While b c) note IH = this ``` nipkow@28867 ` 145` ``` { fix cw ``` nipkow@28867 ` 146` ``` have "\cw,s\ \\<^sub>c s' \ cw = (While b c) \ \bury cw A,t\ \\<^sub>c t' \ ``` nipkow@28867 ` 147` ``` \ x \ L cw A. s x = t x \ \x\A. s' x = t' x" ``` nipkow@28867 ` 148` ``` proof (induct arbitrary: t A pred:evalc) ``` nipkow@28867 ` 149` ``` case WhileFalse ``` nipkow@28867 ` 150` ``` have "\ b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28867 ` 151` ``` then have "t' = t" using WhileFalse by auto ``` nipkow@28867 ` 152` ``` then show ?case using WhileFalse by auto ``` nipkow@28867 ` 153` ``` next ``` nipkow@28867 ` 154` ``` case (WhileTrue _ s _ s'' s') ``` nipkow@28867 ` 155` ``` have "\c,s\ \\<^sub>c s''" using WhileTrue(2,6) by simp ``` nipkow@28867 ` 156` ``` have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28867 ` 157` ``` then obtain t'' where tt'': "\bury c (Dep b \ A \ L c A),t\ \\<^sub>c t''" ``` nipkow@28867 ` 158` ``` and "\bury (While b c) A,t''\ \\<^sub>c t'" ``` nipkow@28867 ` 159` ``` using WhileTrue(6,7) by auto ``` nipkow@28867 ` 160` ``` have "\x\Dep b \ A \ L c A. s'' x = t'' x" ``` nipkow@28867 ` 161` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` tt''] WhileTrue(6,8) ``` nipkow@28867 ` 162` ``` by (auto simp:L_gen_kill) ``` nipkow@28867 ` 163` ``` moreover then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@28867 ` 164` ``` ultimately show ?case ``` nipkow@28867 ` 165` ``` using WhileTrue(5,6) `\bury (While b c) A,t''\ \\<^sub>c t'` by metis ``` nipkow@28867 ` 166` ``` qed auto } ``` nipkow@28867 ` 167` ``` from this[OF IH(3) _ IH(4,2)] show ?case by metis ``` nipkow@28867 ` 168` ```qed ``` nipkow@28867 ` 169` nipkow@28867 ` 170` nipkow@28583 ` 171` `end`