src/HOL/IMP/Live.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 35802 362431732b5e child 39198 f967a16dfcdd permissions -rw-r--r--
 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" ``` wenzelm@32960 ` 96` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` `\c,t\ \\<^sub>c t''`] WhileTrue(6,8) ``` wenzelm@32960 ` 97` ``` by (auto simp:L_gen_kill) ``` nipkow@35802 ` 98` ``` then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@35802 ` 99` ``` then show ?case using WhileTrue(5,6) `\While b c,t''\ \\<^sub>c t'` by metis ``` nipkow@28583 ` 100` ``` qed auto } ``` nipkow@35802 ` 101` ```-- "a terser version" ``` nipkow@35802 ` 102` ``` { let ?w = "While b c" ``` nipkow@35802 ` 103` ``` have "\?w,s\ \\<^sub>c s' \ \?w,t\ \\<^sub>c t' \ ``` nipkow@35802 ` 104` ``` \ x \ L ?w A. s x = t x \ \x\A. s' x = t' x" ``` nipkow@35802 ` 105` ``` proof (induct ?w s s' arbitrary: t A pred:evalc) ``` nipkow@35802 ` 106` ``` case WhileFalse ``` nipkow@35802 ` 107` ``` have "\ b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@35802 ` 108` ``` then have "t' = t" using WhileFalse by auto ``` nipkow@35802 ` 109` ``` then show ?case using WhileFalse by simp ``` nipkow@35802 ` 110` ``` next ``` nipkow@35802 ` 111` ``` case (WhileTrue s s'' s') ``` nipkow@35802 ` 112` ``` have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@35802 ` 113` ``` then obtain t'' where "\c,t\ \\<^sub>c t''" and "\While b c,t''\ \\<^sub>c t'" ``` nipkow@35802 ` 114` ``` using WhileTrue(6,7) by auto ``` nipkow@35802 ` 115` ``` have "\x\Dep b \ A \ L c A. s'' x = t'' x" ``` nipkow@35802 ` 116` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` `\c,t\ \\<^sub>c t''`] WhileTrue(7) ``` nipkow@35802 ` 117` ``` by (auto simp:L_gen_kill) ``` nipkow@35802 ` 118` ``` then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@35802 ` 119` ``` then show ?case using WhileTrue(5) `\While b c,t''\ \\<^sub>c t'` by metis ``` nipkow@35802 ` 120` ``` qed } ``` nipkow@35802 ` 121` ``` from this[OF IH(3) IH(4,2)] show ?case by metis ``` nipkow@28583 ` 122` ```qed ``` nipkow@28583 ` 123` nipkow@28867 ` 124` nipkow@28867 ` 125` ```primrec bury :: "com \ loc set \ com" where ``` nipkow@28867 ` 126` ```"bury SKIP _ = SKIP" | ``` nipkow@28867 ` 127` ```"bury (x :== e) A = (if x:A then x:== e else SKIP)" | ``` nipkow@28867 ` 128` ```"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" | ``` nipkow@28867 ` 129` ```"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" | ``` nipkow@28867 ` 130` ```"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \ A \ L c A))" ``` nipkow@28867 ` 131` nipkow@28867 ` 132` ```theorem bury_sound: ``` nipkow@28867 ` 133` ``` "\ x \ L c A. s x = t x \ \c,s\ \\<^sub>c s' \ \bury c A,t\ \\<^sub>c t' \ ``` nipkow@28867 ` 134` ``` \x\A. s' x = t' x" ``` nipkow@28867 ` 135` ```proof (induct c arbitrary: A s t s' t') ``` nipkow@28867 ` 136` ``` case SKIP then show ?case by auto ``` nipkow@28867 ` 137` ```next ``` nipkow@28867 ` 138` ``` case (Assign x e) then show ?case ``` nipkow@28867 ` 139` ``` by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on) ``` nipkow@28867 ` 140` ```next ``` nipkow@28867 ` 141` ``` case (Semi c1 c2) ``` nipkow@28867 ` 142` ``` from Semi(4) obtain s'' where s1: "\c1,s\ \\<^sub>c s''" and s2: "\c2,s''\ \\<^sub>c s'" ``` nipkow@28867 ` 143` ``` by auto ``` nipkow@28867 ` 144` ``` 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 ` 145` ``` by auto ``` nipkow@28867 ` 146` ``` show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp ``` nipkow@28867 ` 147` ```next ``` nipkow@28867 ` 148` ``` case (Cond b c1 c2) ``` nipkow@28867 ` 149` ``` show ?case ``` nipkow@28867 ` 150` ``` proof cases ``` nipkow@28867 ` 151` ``` assume "b s" ``` nipkow@28867 ` 152` ``` hence s: "\c1,s\ \\<^sub>c s'" using Cond(4) by simp ``` nipkow@28867 ` 153` ``` have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28867 ` 154` ``` hence t: "\bury c1 A,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28867 ` 155` ``` show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28867 ` 156` ``` next ``` nipkow@28867 ` 157` ``` assume "\ b s" ``` nipkow@28867 ` 158` ``` hence s: "\c2,s\ \\<^sub>c s'" using Cond(4) by auto ``` nipkow@28867 ` 159` ``` have "\ b t" using `\ b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) ``` nipkow@28867 ` 160` ``` hence t: "\bury c2 A,t\ \\<^sub>c t'" using Cond(5) by auto ``` nipkow@28867 ` 161` ``` show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp ``` nipkow@28867 ` 162` ``` qed ``` nipkow@28867 ` 163` ```next ``` nipkow@28867 ` 164` ``` case (While b c) note IH = this ``` nipkow@28867 ` 165` ``` { fix cw ``` nipkow@28867 ` 166` ``` have "\cw,s\ \\<^sub>c s' \ cw = (While b c) \ \bury cw A,t\ \\<^sub>c t' \ ``` nipkow@28867 ` 167` ``` \ x \ L cw A. s x = t x \ \x\A. s' x = t' x" ``` nipkow@28867 ` 168` ``` proof (induct arbitrary: t A pred:evalc) ``` nipkow@28867 ` 169` ``` case WhileFalse ``` nipkow@28867 ` 170` ``` have "\ b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28867 ` 171` ``` then have "t' = t" using WhileFalse by auto ``` nipkow@28867 ` 172` ``` then show ?case using WhileFalse by auto ``` nipkow@28867 ` 173` ``` next ``` nipkow@28867 ` 174` ``` case (WhileTrue _ s _ s'' s') ``` nipkow@28867 ` 175` ``` have "\c,s\ \\<^sub>c s''" using WhileTrue(2,6) by simp ``` nipkow@28867 ` 176` ``` have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@28867 ` 177` ``` then obtain t'' where tt'': "\bury c (Dep b \ A \ L c A),t\ \\<^sub>c t''" ``` wenzelm@32960 ` 178` ``` and "\bury (While b c) A,t''\ \\<^sub>c t'" ``` nipkow@28867 ` 179` ``` using WhileTrue(6,7) by auto ``` nipkow@28867 ` 180` ``` have "\x\Dep b \ A \ L c A. s'' x = t'' x" ``` wenzelm@32960 ` 181` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` tt''] WhileTrue(6,8) ``` wenzelm@32960 ` 182` ``` by (auto simp:L_gen_kill) ``` nipkow@28867 ` 183` ``` moreover then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@28867 ` 184` ``` ultimately show ?case ``` wenzelm@32960 ` 185` ``` using WhileTrue(5,6) `\bury (While b c) A,t''\ \\<^sub>c t'` by metis ``` nipkow@28867 ` 186` ``` qed auto } ``` nipkow@35802 ` 187` ``` { let ?w = "While b c" ``` nipkow@35802 ` 188` ``` have "\?w,s\ \\<^sub>c s' \ \bury ?w A,t\ \\<^sub>c t' \ ``` nipkow@35802 ` 189` ``` \ x \ L ?w A. s x = t x \ \x\A. s' x = t' x" ``` nipkow@35802 ` 190` ``` proof (induct ?w s s' arbitrary: t A pred:evalc) ``` nipkow@35802 ` 191` ``` case WhileFalse ``` nipkow@35802 ` 192` ``` have "\ b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@35802 ` 193` ``` then have "t' = t" using WhileFalse by auto ``` nipkow@35802 ` 194` ``` then show ?case using WhileFalse by simp ``` nipkow@35802 ` 195` ``` next ``` nipkow@35802 ` 196` ``` case (WhileTrue s s'' s') ``` nipkow@35802 ` 197` ``` have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) ``` nipkow@35802 ` 198` ``` then obtain t'' where tt'': "\bury c (Dep b \ A \ L c A),t\ \\<^sub>c t''" ``` nipkow@35802 ` 199` ``` and "\bury (While b c) A,t''\ \\<^sub>c t'" ``` nipkow@35802 ` 200` ``` using WhileTrue(6,7) by auto ``` nipkow@35802 ` 201` ``` have "\x\Dep b \ A \ L c A. s'' x = t'' x" ``` nipkow@35802 ` 202` ``` using IH(1)[OF _ `\c,s\ \\<^sub>c s''` tt''] WhileTrue(7) ``` nipkow@35802 ` 203` ``` by (auto simp:L_gen_kill) ``` nipkow@35802 ` 204` ``` then have "\x\L (While b c) A. s'' x = t'' x" by auto ``` nipkow@35802 ` 205` ``` then show ?case ``` nipkow@35802 ` 206` ``` using WhileTrue(5) `\bury (While b c) A,t''\ \\<^sub>c t'` by metis ``` nipkow@35802 ` 207` ``` qed } ``` nipkow@35802 ` 208` ``` from this[OF IH(3) IH(4,2)] show ?case by metis ``` nipkow@28867 ` 209` ```qed ``` nipkow@28867 ` 210` nipkow@28867 ` 211` nipkow@28583 ` 212` `end`