src/HOL/IMP/Live.thy
 author nipkow Tue Oct 14 13:23:31 2008 +0200 (2008-10-14) changeset 28583 9bb9791bdc18 child 28867 3d9873c4c409 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@28583 ` 95` ``` note IH1 = IH(1)[OF _ `\c,s\ \\<^sub>c s''` `\c,t\ \\<^sub>c t''`] ``` nipkow@28583 ` 96` ``` have L1: "\x\A. s'' x = t'' x" using IH1 WhileTrue(6,8) ``` nipkow@28583 ` 97` ``` by(simp add: ball_Un) (metis) ``` nipkow@28583 ` 98` ``` have L2: "\x\Dep b. s'' x = t'' x" ``` nipkow@28583 ` 99` ``` using IH1 WhileTrue(6,8) by (auto simp:L_gen_kill) ``` nipkow@28583 ` 100` ``` have L3: "\x\L c A. s'' x = t'' x" ``` nipkow@28583 ` 101` ``` using IH1 L_idemp[of c A] WhileTrue(6,8) by auto ``` nipkow@28583 ` 102` ``` have "\x\L (While b c) A. s'' x = t'' x" using L1 L2 L3 by auto ``` nipkow@28583 ` 103` ``` then show ?case using WhileTrue(5,6) `\While b c,t''\ \\<^sub>c t'` by metis ``` nipkow@28583 ` 104` ``` qed auto } ``` nipkow@28583 ` 105` ``` from this[OF IH(3) _ IH(4,2)] show ?case by metis ``` nipkow@28583 ` 106` ```qed ``` nipkow@28583 ` 107` nipkow@28583 ` 108` `end`