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--
```     1 theory Live imports Natural
```
```     2 begin
```
```     3
```
```     4 text{* Which variables/locations does an expression depend on?
```
```     5 Any set of variables that completely determine the value of the expression,
```
```     6 in the worst case all locations: *}
```
```     7
```
```     8 consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
```
```     9 specification (Dep)
```
```    10 dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
```
```    11 by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric])
```
```    12
```
```    13 text{* The following definition of @{const Dep} looks very tempting
```
```    14 @{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
```
```    15 but does not work in case @{text e} depends on an infinite set of variables.
```
```    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!
```
```    17
```
```    18 If we had a concrete representation of expressions, we would simply write
```
```    19 a recursive free-variables function.
```
```    20 *}
```
```    21
```
```    22 primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
```
```    23 "L SKIP A = A" |
```
```    24 "L (x :== e) A = A-{x} \<union> Dep e" |
```
```    25 "L (c1; c2) A = (L c1 \<circ> L c2) A" |
```
```    26 "L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
```
```    27 "L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
```
```    28
```
```    29 primrec "kill" :: "com \<Rightarrow> loc set" where
```
```    30 "kill SKIP = {}" |
```
```    31 "kill (x :== e) = {x}" |
```
```    32 "kill (c1; c2) = kill c1 \<union> kill c2" |
```
```    33 "kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter>  kill c2" |
```
```    34 "kill (WHILE b DO c) = {}"
```
```    35
```
```    36 primrec gen :: "com \<Rightarrow> loc set" where
```
```    37 "gen SKIP = {}" |
```
```    38 "gen (x :== e) = Dep e" |
```
```    39 "gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
```
```    40 "gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
```
```    41 "gen (WHILE b DO c) = Dep b \<union> gen c"
```
```    42
```
```    43 lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
```
```    44 by(induct c arbitrary:A) auto
```
```    45
```
```    46 lemma L_idemp: "L c (L c A) \<subseteq> L c A"
```
```    47 by(fastsimp simp add:L_gen_kill)
```
```    48
```
```    49 theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```    50  \<forall>x\<in>A. s' x = t' x"
```
```    51 proof (induct c arbitrary: A s t s' t')
```
```    52   case SKIP then show ?case by auto
```
```    53 next
```
```    54   case (Assign x e) then show ?case
```
```    55     by (auto simp:update_def ball_Un dest!: dep_on)
```
```    56 next
```
```    57   case (Semi c1 c2)
```
```    58   from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
```
```    59     by auto
```
```    60   from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```    61     by auto
```
```    62   show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
```
```    63 next
```
```    64   case (Cond b c1 c2)
```
```    65   show ?case
```
```    66   proof cases
```
```    67     assume "b s"
```
```    68     hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
```
```    69     have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
```
```    70     hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
```
```    71     show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
```
```    72   next
```
```    73     assume "\<not> b s"
```
```    74     hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
```
```    75     have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
```
```    76     hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
```
```    77     show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
```
```    78   qed
```
```    79 next
```
```    80   case (While b c) note IH = this
```
```    81   { fix cw
```
```    82     have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```    83           \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
```
```    84     proof (induct arbitrary: t A pred:evalc)
```
```    85       case WhileFalse
```
```    86       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
```
```    87       then have "t' = t" using WhileFalse by auto
```
```    88       then show ?case using WhileFalse by auto
```
```    89     next
```
```    90       case (WhileTrue _ s _ s'' s')
```
```    91       have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
```
```    92       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
```
```    93       then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```    94         using WhileTrue(6,7) by auto
```
```    95       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
```
```    96         using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
```
```    97         by (auto simp:L_gen_kill)
```
```    98       then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
```
```    99       then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
```
```   100     qed auto }
```
```   101 -- "a terser version"
```
```   102   { let ?w = "While b c"
```
```   103     have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>?w,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```   104           \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
```
```   105     proof (induct ?w s s' arbitrary: t A pred:evalc)
```
```   106       case WhileFalse
```
```   107       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
```
```   108       then have "t' = t" using WhileFalse by auto
```
```   109       then show ?case using WhileFalse by simp
```
```   110     next
```
```   111       case (WhileTrue s s'' s')
```
```   112       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
```
```   113       then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```   114         using WhileTrue(6,7) by auto
```
```   115       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
```
```   116         using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(7)
```
```   117         by (auto simp:L_gen_kill)
```
```   118       then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
```
```   119       then show ?case using WhileTrue(5) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
```
```   120     qed }
```
```   121   from this[OF IH(3) IH(4,2)] show ?case by metis
```
```   122 qed
```
```   123
```
```   124
```
```   125 primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
```
```   126 "bury SKIP _ = SKIP" |
```
```   127 "bury (x :== e) A = (if x:A then x:== e else SKIP)" |
```
```   128 "bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
```
```   129 "bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
```
```   130 "bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
```
```   131
```
```   132 theorem bury_sound:
```
```   133   "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```   134    \<forall>x\<in>A. s' x = t' x"
```
```   135 proof (induct c arbitrary: A s t s' t')
```
```   136   case SKIP then show ?case by auto
```
```   137 next
```
```   138   case (Assign x e) then show ?case
```
```   139     by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
```
```   140 next
```
```   141   case (Semi c1 c2)
```
```   142   from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
```
```   143     by auto
```
```   144   from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```   145     by auto
```
```   146   show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
```
```   147 next
```
```   148   case (Cond b c1 c2)
```
```   149   show ?case
```
```   150   proof cases
```
```   151     assume "b s"
```
```   152     hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
```
```   153     have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
```
```   154     hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
```
```   155     show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
```
```   156   next
```
```   157     assume "\<not> b s"
```
```   158     hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
```
```   159     have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
```
```   160     hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
```
```   161     show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
```
```   162   qed
```
```   163 next
```
```   164   case (While b c) note IH = this
```
```   165   { fix cw
```
```   166     have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```   167           \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
```
```   168     proof (induct arbitrary: t A pred:evalc)
```
```   169       case WhileFalse
```
```   170       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
```
```   171       then have "t' = t" using WhileFalse by auto
```
```   172       then show ?case using WhileFalse by auto
```
```   173     next
```
```   174       case (WhileTrue _ s _ s'' s')
```
```   175       have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
```
```   176       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
```
```   177       then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
```
```   178         and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```   179         using WhileTrue(6,7) by auto
```
```   180       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
```
```   181         using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
```
```   182         by (auto simp:L_gen_kill)
```
```   183       moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
```
```   184       ultimately show ?case
```
```   185         using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
```
```   186     qed auto }
```
```   187   { let ?w = "While b c"
```
```   188     have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury ?w A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
```
```   189           \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
```
```   190     proof (induct ?w s s' arbitrary: t A pred:evalc)
```
```   191       case WhileFalse
```
```   192       have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
```
```   193       then have "t' = t" using WhileFalse by auto
```
```   194       then show ?case using WhileFalse by simp
```
```   195     next
```
```   196       case (WhileTrue s s'' s')
```
```   197       have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
```
```   198       then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
```
```   199         and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
```
```   200         using WhileTrue(6,7) by auto
```
```   201       have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
```
```   202         using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(7)
```
```   203         by (auto simp:L_gen_kill)
```
```   204       then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
```
```   205       then show ?case
```
```   206         using WhileTrue(5) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
```
```   207     qed }
```
```   208   from this[OF IH(3) IH(4,2)] show ?case by metis
```
```   209 qed
```
```   210
```
```   211
```
`   212 end`