90 case (WhileTrue _ s _ s'' s') |
90 case (WhileTrue _ s _ s'' s') |
91 have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp |
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) |
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'" |
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 |
94 using WhileTrue(6,7) by auto |
95 note IH1 = IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] |
95 have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
96 have L1: "\<forall>x\<in>A. s'' x = t'' x" using IH1 WhileTrue(6,8) |
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(simp add: ball_Un) (metis) |
97 by (auto simp:L_gen_kill) |
98 have L2: "\<forall>x\<in>Dep b. s'' x = t'' x" |
98 moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
99 using IH1 WhileTrue(6,8) by (auto simp:L_gen_kill) |
99 ultimately show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
100 have L3: "\<forall>x\<in>L c A. s'' x = t'' x" |
|
101 using IH1 L_idemp[of c A] WhileTrue(6,8) by auto |
|
102 have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" using L1 L2 L3 by auto |
|
103 then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
104 qed auto } |
100 qed auto } |
105 from this[OF IH(3) _ IH(4,2)] show ?case by metis |
101 from this[OF IH(3) _ IH(4,2)] show ?case by metis |
106 qed |
102 qed |
107 |
103 |
|
104 |
|
105 primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where |
|
106 "bury SKIP _ = SKIP" | |
|
107 "bury (x :== e) A = (if x:A then x:== e else SKIP)" | |
|
108 "bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" | |
|
109 "bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" | |
|
110 "bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))" |
|
111 |
|
112 theorem bury_sound: |
|
113 "\<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> |
|
114 \<forall>x\<in>A. s' x = t' x" |
|
115 proof (induct c arbitrary: A s t s' t') |
|
116 case SKIP then show ?case by auto |
|
117 next |
|
118 case (Assign x e) then show ?case |
|
119 by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on) |
|
120 next |
|
121 case (Semi c1 c2) |
|
122 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'" |
|
123 by auto |
|
124 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'" |
|
125 by auto |
|
126 show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp |
|
127 next |
|
128 case (Cond b c1 c2) |
|
129 show ?case |
|
130 proof cases |
|
131 assume "b s" |
|
132 hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp |
|
133 have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
134 hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
135 show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp |
|
136 next |
|
137 assume "\<not> b s" |
|
138 hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto |
|
139 have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
140 hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
141 show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp |
|
142 qed |
|
143 next |
|
144 case (While b c) note IH = this |
|
145 { fix cw |
|
146 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> |
|
147 \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x" |
|
148 proof (induct arbitrary: t A pred:evalc) |
|
149 case WhileFalse |
|
150 have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) |
|
151 then have "t' = t" using WhileFalse by auto |
|
152 then show ?case using WhileFalse by auto |
|
153 next |
|
154 case (WhileTrue _ s _ s'' s') |
|
155 have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp |
|
156 have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) |
|
157 then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''" |
|
158 and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
159 using WhileTrue(6,7) by auto |
|
160 have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
161 using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8) |
|
162 by (auto simp:L_gen_kill) |
|
163 moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
|
164 ultimately show ?case |
|
165 using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
166 qed auto } |
|
167 from this[OF IH(3) _ IH(4,2)] show ?case by metis |
|
168 qed |
|
169 |
|
170 |
108 end |
171 end |