1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: HoarePartialProps.thy 8 Author: Norbert Schirmer, TU Muenchen 9 10Copyright (C) 2004-2008 Norbert Schirmer 11Some rights reserved, TU Muenchen 12 13This library is free software; you can redistribute it and/or modify 14it under the terms of the GNU Lesser General Public License as 15published by the Free Software Foundation; either version 2.1 of the 16License, or (at your option) any later version. 17 18This library is distributed in the hope that it will be useful, but 19WITHOUT ANY WARRANTY; without even the implied warranty of 20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 21Lesser General Public License for more details. 22 23You should have received a copy of the GNU Lesser General Public 24License along with this library; if not, write to the Free Software 25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 26USA 27*) 28 29section \<open>Properties of Partial Correctness Hoare Logic\<close> 30 31theory HoarePartialProps imports HoarePartialDef begin 32 33subsection \<open>Soundness\<close> 34 35lemma hoare_cnvalid: 36 assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 37 shows "\<And>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 38using hoare 39proof (induct) 40 case (Skip \<Theta> F P A) 41 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Skip P,A" 42 proof (rule cnvalidI) 43 fix s t 44 assume "\<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> P" 45 thus "t \<in> Normal ` P \<union> Abrupt ` A" 46 by cases auto 47 qed 48next 49 case (Basic \<Theta> F f P A) 50 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> {s. f s \<in> P} (Basic f) P,A" 51 proof (rule cnvalidI) 52 fix s t 53 assume "\<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> {s. f s \<in> P}" 54 thus "t \<in> Normal ` P \<union> Abrupt ` A" 55 by cases auto 56 qed 57next 58 case (Spec \<Theta> F r Q A) 59 show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)} Spec r Q,A" 60 proof (rule cnvalidI) 61 fix s t 62 assume exec: "\<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> =n\<Rightarrow> t" 63 assume P: "s \<in> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)}" 64 from exec P 65 show "t \<in> Normal ` Q \<union> Abrupt ` A" 66 by cases auto 67 qed 68next 69 case (Seq \<Theta> F P c1 R A c2 Q) 70 have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c1 R,A" by fact 71 have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> R c2 Q,A" by fact 72 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Seq c1 c2 Q,A" 73 proof (rule cnvalidI) 74 fix s t 75 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 76 assume exec: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> =n\<Rightarrow> t" 77 assume t_notin_F: "t \<notin> Fault ` F" 78 assume P: "s \<in> P" 79 from exec P obtain r where 80 exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> =n\<Rightarrow> r" and exec_c2: "\<Gamma>\<turnstile>\<langle>c2,r\<rangle> =n\<Rightarrow> t" 81 by cases auto 82 with t_notin_F have "r \<notin> Fault ` F" 83 by (auto dest: execn_Fault_end) 84 with valid_c1 ctxt exec_c1 P 85 have r: "r\<in>Normal ` R \<union> Abrupt ` A" 86 by (rule cnvalidD) 87 show "t\<in>Normal ` Q \<union> Abrupt ` A" 88 proof (cases r) 89 case (Normal r') 90 with exec_c2 r 91 show "t\<in>Normal ` Q \<union> Abrupt ` A" 92 apply - 93 apply (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F]) 94 apply auto 95 done 96 next 97 case (Abrupt r') 98 with exec_c2 have "t=Abrupt r'" 99 by (auto elim: execn_elim_cases) 100 with Abrupt r show ?thesis 101 by auto 102 next 103 case Fault with r show ?thesis by blast 104 next 105 case Stuck with r show ?thesis by blast 106 qed 107 qed 108next 109 case (Cond \<Theta> F P b c1 Q A c2) 110 have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> b) c1 Q,A" by fact 111 have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> - b) c2 Q,A" by fact 112 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Cond b c1 c2 Q,A" 113 proof (rule cnvalidI) 114 fix s t 115 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 116 assume exec: "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> =n\<Rightarrow> t" 117 assume P: "s \<in> P" 118 assume t_notin_F: "t \<notin> Fault ` F" 119 show "t \<in> Normal ` Q \<union> Abrupt ` A" 120 proof (cases "s\<in>b") 121 case True 122 with exec have "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> =n\<Rightarrow> t" 123 by cases auto 124 with P True 125 show ?thesis 126 by - (rule cnvalidD [OF valid_c1 ctxt _ _ t_notin_F],auto) 127 next 128 case False 129 with exec P have "\<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> =n\<Rightarrow> t" 130 by cases auto 131 with P False 132 show ?thesis 133 by - (rule cnvalidD [OF valid_c2 ctxt _ _ t_notin_F],auto) 134 qed 135 qed 136next 137 case (While \<Theta> F P b c A n) 138 have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (P \<inter> b) c P,A" by fact 139 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P While b c (P \<inter> - b),A" 140 proof (rule cnvalidI) 141 fix s t 142 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 143 assume exec: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> =n\<Rightarrow> t" 144 assume P: "s \<in> P" 145 assume t_notin_F: "t \<notin> Fault ` F" 146 show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" 147 proof (cases "s \<in> b") 148 case True 149 { 150 fix d::"('b,'a,'c) com" fix s t 151 assume exec: "\<Gamma>\<turnstile>\<langle>d,s\<rangle> =n\<Rightarrow> t" 152 assume d: "d=While b c" 153 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 154 from exec d ctxt 155 have "\<lbrakk>s \<in> Normal ` P; t \<notin> Fault ` F\<rbrakk> 156 \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt`A" 157 proof (induct) 158 case (WhileTrue s b' c' n r t) 159 have t_notin_F: "t \<notin> Fault ` F" by fact 160 have eqs: "While b' c' = While b c" by fact 161 note valid_c 162 moreover have ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact 163 moreover from WhileTrue 164 obtain "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> r" and 165 "\<Gamma>\<turnstile>\<langle>While b c,r\<rangle> =n\<Rightarrow> t" and 166 "Normal s \<in> Normal `(P \<inter> b)" by auto 167 moreover with t_notin_F have "r \<notin> Fault ` F" 168 by (auto dest: execn_Fault_end) 169 ultimately 170 have r: "r \<in> Normal ` P \<union> Abrupt ` A" 171 by - (rule cnvalidD,auto) 172 from this _ ctxt 173 show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A " 174 proof (cases r) 175 case (Normal r') 176 with r ctxt eqs t_notin_F 177 show ?thesis 178 by - (rule WhileTrue.hyps,auto) 179 next 180 case (Abrupt r') 181 have "\<Gamma>\<turnstile>\<langle>While b' c',r\<rangle> =n\<Rightarrow> t" by fact 182 with Abrupt have "t=r" 183 by (auto dest: execn_Abrupt_end) 184 with r Abrupt show ?thesis 185 by blast 186 next 187 case Fault with r show ?thesis by blast 188 next 189 case Stuck with r show ?thesis by blast 190 qed 191 qed auto 192 } 193 with exec ctxt P t_notin_F 194 show ?thesis 195 by auto 196 next 197 case False 198 with exec P have "t=Normal s" 199 by cases auto 200 with P False 201 show ?thesis 202 by auto 203 qed 204 qed 205next 206 case (Guard \<Theta> F g P c Q A f) 207 have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact 208 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) Guard f g c Q,A" 209 proof (rule cnvalidI) 210 fix s t 211 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 212 assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> =n\<Rightarrow> t" 213 assume t_notin_F: "t \<notin> Fault ` F" 214 assume P:"s \<in> (g \<inter> P)" 215 from exec P have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 216 by cases auto 217 from valid_c ctxt this P t_notin_F 218 show "t \<in> Normal ` Q \<union> Abrupt ` A" 219 by (rule cnvalidD) 220 qed 221next 222 case (Guarantee f F \<Theta> g P c Q A) 223 have valid_c: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact 224 have f_F: "f \<in> F" by fact 225 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Guard f g c Q,A" 226 proof (rule cnvalidI) 227 fix s t 228 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 229 assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> =n\<Rightarrow> t" 230 assume t_notin_F: "t \<notin> Fault ` F" 231 assume P:"s \<in> P" 232 from exec f_F t_notin_F have g: "s \<in> g" 233 by cases auto 234 with P have P': "s \<in> g \<inter> P" 235 by blast 236 from exec P g have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 237 by cases auto 238 from valid_c ctxt this P' t_notin_F 239 show "t \<in> Normal ` Q \<union> Abrupt ` A" 240 by (rule cnvalidD) 241 qed 242next 243 case (CallRec P p Q A Specs \<Theta> F) 244 have p: "(P,p,Q,A) \<in> Specs" by fact 245 have valid_body: 246 "\<forall>(P,p,Q,A) \<in> Specs. p \<in> dom \<Gamma> \<and> (\<forall>n. \<Gamma>,\<Theta> \<union> Specs \<Turnstile>n:\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A)" 247 using CallRec.hyps by blast 248 show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P Call p Q,A" 249 proof - 250 { 251 fix n 252 have "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A 253 \<Longrightarrow> \<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 254 proof (induct n) 255 case 0 256 show "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>0:\<^bsub>/F\<^esub> P (Call p) Q,A" 257 by (fastforce elim!: execn_elim_cases simp add: nvalid_def) 258 next 259 case (Suc m) 260 have hyp: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A 261 \<Longrightarrow> \<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact 262 have "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A" by fact 263 hence ctxt_m: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A" 264 by (fastforce simp add: nvalid_def intro: execn_Suc) 265 hence valid_Proc: 266 "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma>\<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A" 267 by (rule hyp) 268 let ?\<Theta>'= "\<Theta> \<union> Specs" 269 from valid_Proc ctxt_m 270 have "\<forall>(P, p, Q, A)\<in>?\<Theta>'. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (Call p) Q,A" 271 by fastforce 272 with valid_body 273 have valid_body_m: 274 "\<forall>(P,p,Q,A) \<in>Specs. \<forall>n. \<Gamma> \<Turnstile>m:\<^bsub>/F\<^esub> P (the (\<Gamma> p)) Q,A" 275 by (fastforce simp add: cnvalid_def) 276 show "\<forall>(P,p,Q,A) \<in>Specs. \<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A" 277 proof (clarify) 278 fix P p Q A assume p: "(P,p,Q,A) \<in> Specs" 279 show "\<Gamma> \<Turnstile>Suc m:\<^bsub>/F\<^esub> P (Call p) Q,A" 280 proof (rule nvalidI) 281 fix s t 282 assume exec_call: 283 "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> =Suc m\<Rightarrow> t" 284 assume Pre: "s \<in> P" 285 assume t_notin_F: "t \<notin> Fault ` F" 286 from exec_call 287 show "t \<in> Normal ` Q \<union> Abrupt ` A" 288 proof (cases) 289 fix bdy m' 290 assume m: "Suc m = Suc m'" 291 assume bdy: "\<Gamma> p = Some bdy" 292 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> =m'\<Rightarrow> t" 293 from Pre valid_body_m exec_body bdy m p t_notin_F 294 show ?thesis 295 by (fastforce simp add: nvalid_def) 296 next 297 assume "\<Gamma> p = None" 298 with valid_body p have False by auto 299 thus ?thesis .. 300 qed 301 qed 302 qed 303 qed 304 } 305 with p show ?thesis 306 by (fastforce simp add: cnvalid_def) 307 qed 308next 309 case (DynCom P \<Theta> F c Q A) 310 hence valid_c: "\<forall>s\<in>P. (\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (c s) Q,A)" by auto 311 show "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P DynCom c Q,A" 312 proof (rule cnvalidI) 313 fix s t 314 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 315 assume exec: "\<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> =n\<Rightarrow> t" 316 assume P: "s \<in> P" 317 assume t_notin_Fault: "t \<notin> Fault ` F" 318 from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" 319 proof (cases) 320 assume "\<Gamma>\<turnstile>\<langle>c s,Normal s\<rangle> =n\<Rightarrow> t" 321 from cnvalidD [OF valid_c [rule_format, OF P] ctxt this P t_notin_Fault] 322 show ?thesis . 323 qed 324 qed 325next 326 case (Throw \<Theta> F A Q) 327 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> A Throw Q,A" 328 proof (rule cnvalidI) 329 fix s t 330 assume "\<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> =n\<Rightarrow> t" "s \<in> A" 331 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 332 by cases simp 333 qed 334next 335 case (Catch \<Theta> F P c\<^sub>1 Q R c\<^sub>2 A) 336 have valid_c1: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>1 Q,R" by fact 337 have valid_c2: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> R c\<^sub>2 Q,A" by fact 338 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A" 339 proof (rule cnvalidI) 340 fix s t 341 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 342 assume exec: "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> t" 343 assume P: "s \<in> P" 344 assume t_notin_Fault: "t \<notin> Fault ` F" 345 from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" 346 proof (cases) 347 fix s' 348 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Abrupt s'" 349 assume exec_c2: "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s'\<rangle> =n\<Rightarrow> t" 350 from cnvalidD [OF valid_c1 ctxt exec_c1 P ] 351 have "Abrupt s' \<in> Abrupt ` R" 352 by auto 353 with cnvalidD [OF valid_c2 ctxt _ _ t_notin_Fault] exec_c2 354 show ?thesis 355 by fastforce 356 next 357 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" 358 assume notAbr: "\<not> isAbr t" 359 from cnvalidD [OF valid_c1 ctxt exec_c1 P t_notin_Fault] 360 have "t \<in> Normal ` Q \<union> Abrupt ` R" . 361 with notAbr 362 show ?thesis 363 by auto 364 qed 365 qed 366next 367 case (Conseq P \<Theta> F c Q A) 368 hence adapt: "\<forall>s \<in> P. (\<exists>P' Q' A'. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A' \<and> 369 s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)" 370 by blast 371 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 372 proof (rule cnvalidI) 373 fix s t 374 assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 375 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 376 assume P: "s \<in> P" 377 assume t_notin_F: "t \<notin> Fault ` F" 378 show "t \<in> Normal ` Q \<union> Abrupt ` A" 379 proof - 380 from P adapt obtain P' Q' A' Z where 381 spec: "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A'" and 382 P': "s \<in> P'" and strengthen: "Q' \<subseteq> Q \<and> A' \<subseteq> A" 383 by auto 384 from spec [rule_format] ctxt exec P' t_notin_F 385 have "t \<in> Normal ` Q' \<union> Abrupt ` A'" 386 by (rule cnvalidD) 387 with strengthen show ?thesis 388 by blast 389 qed 390 qed 391next 392 case (Asm P p Q A \<Theta> F) 393 have asm: "(P, p, Q, A) \<in> \<Theta>" by fact 394 show "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 395 proof (rule cnvalidI) 396 fix s t 397 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 398 assume exec: "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> =n\<Rightarrow> t" 399 from asm ctxt have "\<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P Call p Q,A" by auto 400 moreover 401 assume "s \<in> P" "t \<notin> Fault ` F" 402 ultimately 403 show "t \<in> Normal ` Q \<union> Abrupt ` A" 404 using exec 405 by (auto simp add: nvalid_def) 406 qed 407next 408 case ExFalso thus ?case by iprover 409qed 410 411theorem hoare_sound: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 412 by (iprover intro: cnvalid_to_cvalid hoare_cnvalid) 413 414subsection \<open>Completeness\<close> 415 416lemma MGT_valid: 417"\<Gamma>\<Turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 418 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 419proof (rule validI) 420 fix s t 421 assume "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 422 "s \<in> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}" 423 "t \<notin> Fault ` F" 424 thus "t \<in> Normal ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t} \<union> 425 Abrupt ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 426 by (cases t) (auto simp add: final_notin_def) 427qed 428 429text \<open>The consequence rule where the existential @{term Z} is instantiated 430to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close> 431lemma ConseqMGT: 432 assumes modif: "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" 433 assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and> 434 (\<forall>t. t \<in> A' s \<longrightarrow> t \<in> A)" 435 shows "\<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> P c Q,A" 436using impl 437by - (rule conseq [OF modif],blast) 438 439 440lemma Seq_NoFaultStuckD1: 441 assumes noabort: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` F)" 442 shows "\<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` F)" 443proof (rule final_notinI) 444 fix t 445 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow> t" 446 show "t \<notin> {Stuck} \<union> Fault ` F" 447 proof 448 assume "t \<in> {Stuck} \<union> Fault ` F" 449 moreover 450 { 451 assume "t = Stuck" 452 with exec_c1 453 have "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow> Stuck" 454 by (auto intro: exec_Seq') 455 with noabort have False 456 by (auto simp add: final_notin_def) 457 hence False .. 458 } 459 moreover 460 { 461 assume "t \<in> Fault ` F" 462 then obtain f where 463 t: "t=Fault f" and f: "f \<in> F" 464 by auto 465 from t exec_c1 466 have "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow> Fault f" 467 by (auto intro: exec_Seq') 468 with noabort f have False 469 by (auto simp add: final_notin_def) 470 hence False .. 471 } 472 ultimately show False by auto 473 qed 474qed 475 476lemma Seq_NoFaultStuckD2: 477 assumes noabort: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` F)" 478 shows "\<forall>t. \<Gamma>\<turnstile>\<langle>c1,s\<rangle> \<Rightarrow> t \<longrightarrow> t\<notin> ({Stuck} \<union> Fault ` F) \<longrightarrow> 479 \<Gamma>\<turnstile>\<langle>c2,t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` F)" 480using noabort 481by (auto simp add: final_notin_def intro: exec_Seq') 482 483 484lemma MGT_implies_complete: 485 assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 486 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 487 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 488 assumes valid: "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 489 shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A" 490 using MGT 491 apply (rule ConseqMGT) 492 apply (insert valid) 493 apply (auto simp add: valid_def intro!: final_notinI) 494 done 495 496text \<open>Equipped only with the classic consequence rule @{thm "conseqPrePost"} 497 we can only derive this syntactically more involved version 498 of completeness. But semantically it is equivalent to the "real" one 499 (see below)\<close> 500lemma MGT_implies_complete': 501 assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> 502 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 503 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 504 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 505 assumes valid: "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 506 shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}" 507 using MGT [rule_format, of Z] 508 apply (rule conseqPrePost) 509 apply (insert valid) 510 apply (fastforce simp add: valid_def final_notin_def) 511 apply (fastforce simp add: valid_def) 512 apply (fastforce simp add: valid_def) 513 done 514 515text \<open>Semantic equivalence of both kind of formulations\<close> 516lemma valid_involved_to_valid: 517 assumes valid: 518 "\<forall>Z. \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}" 519 shows "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 520 using valid 521 apply (simp add: valid_def) 522 apply clarsimp 523 apply (erule_tac x="x" in allE) 524 apply (erule_tac x="Normal x" in allE) 525 apply (erule_tac x=t in allE) 526 apply fastforce 527 done 528 529text \<open>The sophisticated consequence rule allow us to do this 530 semantical transformation on the hoare-level, too. 531 The magic is, that it allow us to 532 choose the instance of @{term Z} under the assumption of an state @{term "s \<in> P"}\<close> 533lemma 534 assumes deriv: 535 "\<forall>Z. \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}" 536 shows "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A" 537 apply (rule ConseqMGT [OF deriv]) 538 apply auto 539 done 540 541lemma valid_to_valid_involved: 542 "\<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> 543 \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}" 544by (simp add: valid_def Collect_conv_if) 545 546lemma 547 assumes deriv: "\<Gamma>,{} \<turnstile>\<^bsub>/F\<^esub> P c Q,A" 548 shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> s \<in> P} c {t. Z \<in> P \<longrightarrow> t \<in> Q},{t. Z \<in> P \<longrightarrow> t \<in> A}" 549 apply (rule conseqPrePost [OF deriv]) 550 apply auto 551 done 552 553lemma conseq_extract_state_indep_prop: 554 assumes state_indep_prop:"\<forall>s \<in> P. R" 555 assumes to_show: "R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 556 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 557 apply (rule Conseq) 558 apply (clarify) 559 apply (rule_tac x="P" in exI) 560 apply (rule_tac x="Q" in exI) 561 apply (rule_tac x="A" in exI) 562 using state_indep_prop to_show 563 by blast 564 565 566lemma MGT_lemma: 567 assumes MGT_Calls: 568 "\<forall>p\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^bsub>/F\<^esub> 569 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 570 (Call p) 571 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 572 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 573 shows "\<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 574 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 575proof (induct c) 576 case Skip 577 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Skip 578 {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 579 by (rule hoarep.Skip [THEN conseqPre]) 580 (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) 581next 582 case (Basic f) 583 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Basic f 584 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t}, 585 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 586 by (rule hoarep.Basic [THEN conseqPre]) 587 (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) 588next 589 case (Spec r) 590 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Spec r 591 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t}, 592 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 593 apply (rule hoarep.Spec [THEN conseqPre]) 594 apply (clarsimp simp add: final_notin_def) 595 apply (case_tac "\<exists>t. (Z,t) \<in> r") 596 apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) 597 done 598next 599 case (Seq c1 c2) 600 have hyp_c1: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1 601 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 602 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 603 using Seq.hyps by iprover 604 have hyp_c2: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c2 605 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 606 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 607 using Seq.hyps by iprover 608 from hyp_c1 609 have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1 610 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> 611 \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}, 612 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 613 by (rule ConseqMGT) 614 (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified] 615 intro: exec.Seq) 616 thus "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 617 Seq c1 c2 618 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 619 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 620 proof (rule hoarep.Seq ) 621 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> 622 \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 623 c2 624 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 625 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 626 proof (rule ConseqMGT [OF hyp_c2],safe) 627 fix r t 628 assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Normal t" 629 then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t" 630 by (iprover intro: exec.intros) 631 next 632 fix r t 633 assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Abrupt t" 634 then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 635 by (iprover intro: exec.intros) 636 qed 637 qed 638next 639 case (Cond b c1 c2) 640 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c1 641 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 642 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 643 using Cond.hyps by iprover 644 hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}\<inter>b) 645 c1 646 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 647 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 648 by (rule ConseqMGT) 649 (fastforce intro: exec.CondTrue simp add: final_notin_def) 650 moreover 651 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c2 652 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 653 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 654 using Cond.hyps by iprover 655 hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}\<inter>-b) 656 c2 657 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 658 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 659 by (rule ConseqMGT) 660 (fastforce intro: exec.CondFalse simp add: final_notin_def) 661 ultimately 662 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 663 Cond b c1 c2 664 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 665 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 666 by (rule hoarep.Cond) 667next 668 case (While b c) 669 let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*" 670 let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and> 671 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 672 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 673 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 674 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))}" 675 let ?A' = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 676 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 677 While b c 678 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}, 679 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 680 proof (rule ConseqMGT [where ?P'="?P'" 681 and ?Q'="\<lambda>Z. ?P' Z \<inter> - b" and ?A'="?A'"]) 682 show "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A' Z)" 683 proof (rule allI, rule hoarep.While) 684 fix Z 685 from While 686 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 687 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 688 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover 689 then show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?P' Z \<inter> b) c (?P' Z),(?A' Z)" 690 proof (rule ConseqMGT) 691 fix s 692 assume "s\<in> {t. (Z, t) \<in> ?unroll \<and> 693 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 694 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 695 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 696 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))} 697 \<inter> b" 698 then obtain 699 Z_s_unroll: "(Z,s) \<in> ?unroll" and 700 noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 701 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 702 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 703 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and 704 s_in_b: "s\<in>b" 705 by blast 706 show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} \<and> 707 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow> 708 t \<in> {t. (Z, t) \<in> ?unroll \<and> 709 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 710 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 711 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 712 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))}) \<and> 713 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow> 714 t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})" 715 (is "?C1 \<and> ?C2 \<and> ?C3") 716 proof (intro conjI) 717 from Z_s_unroll noabort s_in_b show ?C1 by blast 718 next 719 { 720 fix t 721 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t" 722 moreover 723 from Z_s_unroll s_t s_in_b 724 have "(Z, t) \<in> ?unroll" 725 by (blast intro: rtrancl_into_rtrancl) 726 moreover note noabort 727 ultimately 728 have "(Z, t) \<in> ?unroll \<and> 729 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 730 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 731 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 732 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u))" 733 by iprover 734 } 735 then show ?C2 by blast 736 next 737 { 738 fix t 739 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t" 740 from Z_s_unroll noabort s_t s_in_b 741 have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t" 742 by blast 743 } thus ?C3 by simp 744 qed 745 qed 746 qed 747 next 748 fix s 749 assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}" 750 hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 751 by auto 752 show "s \<in> ?P' s \<and> 753 (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow> 754 t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and> 755 (\<forall>t. t\<in>?A' s \<longrightarrow> t\<in>?A' Z)" 756 proof (intro conjI) 757 { 758 fix e 759 assume "(Z,e) \<in> ?unroll" "e \<in> b" 760 from this WhileNoFault 761 have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 762 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 763 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e") 764 proof (induct rule: converse_rtrancl_induct [consumes 1]) 765 assume e_in_b: "e \<in> b" 766 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 767 with e_in_b WhileNoFault 768 have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 769 by (auto simp add: final_notin_def intro: exec.intros) 770 moreover 771 { 772 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 773 with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u" 774 by (blast intro: exec.intros) 775 } 776 ultimately 777 show "?Prop e e" 778 by iprover 779 next 780 fix Z r 781 assume e_in_b: "e\<in>b" 782 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 783 assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk> 784 \<Longrightarrow> ?Prop r e" 785 assume Z_r: 786 "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}" 787 with WhileNoFault 788 have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 789 by (auto simp add: final_notin_def intro: exec.intros) 790 from hyp [OF e_in_b this] obtain 791 cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and 792 Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow> 793 \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" 794 by simp 795 796 { 797 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 798 with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp 799 moreover from Z_r obtain 800 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 801 by simp 802 ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u" 803 by (blast intro: exec.intros) 804 } 805 with cNoFault show "?Prop Z e" 806 by iprover 807 qed 808 } 809 with P show "s \<in> ?P' s" 810 by blast 811 next 812 { 813 fix t 814 assume "termination": "t \<notin> b" 815 assume "(Z, t) \<in> ?unroll" 816 hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 817 proof (induct rule: converse_rtrancl_induct [consumes 1]) 818 from "termination" 819 show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t" 820 by (blast intro: exec.WhileFalse) 821 next 822 fix Z r 823 assume first_body: 824 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" 825 assume "(r, t) \<in> ?unroll" 826 assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t" 827 show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 828 proof - 829 from first_body obtain 830 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 831 by fast 832 moreover 833 from rest_loop have 834 "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t" 835 by fast 836 ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 837 by (rule exec.WhileTrue) 838 qed 839 qed 840 } 841 with P 842 show "(\<forall>t. t\<in>(?P' s \<inter> - b) 843 \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})" 844 by blast 845 next 846 from P show "\<forall>t. t\<in>?A' s \<longrightarrow> t\<in>?A' Z" by simp 847 qed 848 qed 849next 850 case (Call p) 851 let ?P = "{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}" 852 from noStuck_Call have "\<forall>s \<in> ?P. p \<in> dom \<Gamma>" 853 by (fastforce simp add: final_notin_def ) 854 then show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ?P (Call p) 855 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 856 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 857 proof (rule conseq_extract_state_indep_prop) 858 assume p_definied: "p \<in> dom \<Gamma>" 859 with MGT_Calls show 860 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> 861 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 862 (Call p) 863 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 864 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 865 by (auto) 866 qed 867next 868 case (DynCom c) 869 have hyp: 870 "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c s' 871 {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}" 872 using DynCom by simp 873 have hyp': 874 "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c Z 875 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 876 by (rule ConseqMGT [OF hyp]) 877 (fastforce simp add: final_notin_def intro: exec.intros) 878 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 879 DynCom c 880 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t}, 881 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 882 apply (rule hoarep.DynCom) 883 apply (clarsimp) 884 apply (rule hyp' [simplified]) 885 done 886next 887 case (Guard f g c) 888 have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c 889 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 890 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 891 using Guard by iprover 892 show ?case 893 proof (cases "f \<in> F") 894 case True 895 from hyp_c 896 have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>(g \<inter> {s. s = Z \<and> 897 \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (- F))}) 898 c 899 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t}, 900 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 901 apply (rule ConseqMGT) 902 apply (insert True) 903 apply (auto simp add: final_notin_def intro: exec.intros) 904 done 905 from True this 906 show ?thesis 907 by (rule conseqPre [OF Guarantee]) auto 908 next 909 case False 910 from hyp_c 911 have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> 912 (g \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}) 913 c 914 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t}, 915 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 916 apply (rule ConseqMGT) 917 apply clarify 918 apply (frule Guard_noFaultStuckD [OF _ False]) 919 apply (auto simp add: final_notin_def intro: exec.intros) 920 done 921 then show ?thesis 922 apply (rule conseqPre [OF hoarep.Guard]) 923 apply clarify 924 apply (frule Guard_noFaultStuckD [OF _ False]) 925 apply auto 926 done 927 qed 928next 929 case Throw 930 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} Throw 931 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t}, 932 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 933 by (rule conseqPre [OF hoarep.Throw]) (blast intro: exec.intros) 934next 935 case (Catch c\<^sub>1 c\<^sub>2) 936 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>1 937 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t}, 938 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 939 using Catch.hyps by iprover 940 hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>1 941 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 942 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> 943 \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}" 944 by (rule ConseqMGT) 945 (fastforce intro: exec.intros simp add: final_notin_def) 946 moreover 947 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} c\<^sub>2 948 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 949 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 950 using Catch.hyps by iprover 951 hence "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>Abrupt s \<and> 952 \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 953 c\<^sub>2 954 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 955 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 956 by (rule ConseqMGT) 957 (fastforce intro: exec.intros simp add: final_notin_def) 958 ultimately 959 show "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 960 Catch c\<^sub>1 c\<^sub>2 961 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 962 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 963 by (rule hoarep.Catch) 964qed 965 966lemma MGT_Calls: 967 "\<forall>p\<in>dom \<Gamma>. \<forall>Z. 968 \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 969 (Call p) 970 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 971 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 972proof - 973 { 974 fix p Z 975 assume defined: "p \<in> dom \<Gamma>" 976 have 977 "\<Gamma>,(\<Union>p\<in>dom \<Gamma>. \<Union>Z. 978 {({s. s=Z \<and> 979 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}, 980 p, 981 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 982 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})}) 983 \<turnstile>\<^bsub>/F\<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 984 (the (\<Gamma> p)) 985 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 986 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 987 (is "\<Gamma>,?\<Theta> \<turnstile>\<^bsub>/F\<^esub> (?Pre p Z) (the (\<Gamma> p)) (?Post p Z),(?Abr p Z)") 988 proof - 989 have MGT_Calls: 990 "\<forall>p\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,?\<Theta> \<turnstile>\<^bsub>/F\<^esub> 991 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 992 (Call p) 993 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 994 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 995 by (intro ballI allI, rule HoarePartialDef.Asm,auto) 996 have "\<forall>Z. \<Gamma>,?\<Theta>\<turnstile>\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p) ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault`(-F))} 997 (the (\<Gamma> p)) 998 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t}, 999 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1000 by (iprover intro: MGT_lemma [OF MGT_Calls]) 1001 thus "\<Gamma>,?\<Theta>\<turnstile>\<^bsub>/F\<^esub> (?Pre p Z) (the (\<Gamma> p)) (?Post p Z),(?Abr p Z)" 1002 apply (rule ConseqMGT) 1003 apply (clarify,safe) 1004 proof - 1005 assume "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1006 with defined show "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1007 by (fastforce simp add: final_notin_def 1008 intro: exec.intros) 1009 next 1010 fix t 1011 assume "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t" 1012 with defined 1013 show "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>Normal t" 1014 by (auto intro: exec.Call) 1015 next 1016 fix t 1017 assume "\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t" 1018 with defined 1019 show "\<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow>Abrupt t" 1020 by (auto intro: exec.Call) 1021 qed 1022 qed 1023 } 1024 then show ?thesis 1025 apply - 1026 apply (intro ballI allI) 1027 apply (rule CallRec' [where Procs="dom \<Gamma>" and 1028 P="\<lambda>p Z. {s. s=Z \<and> 1029 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}"and 1030 Q="\<lambda>p Z. 1031 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" and 1032 A="\<lambda>p Z. 1033 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"] ) 1034 apply simp+ 1035 done 1036qed 1037 1038theorem hoare_complete: "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1039 by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Calls]) 1040 1041lemma hoare_complete': 1042 assumes cvalid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1043 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1044proof (cases "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A") 1045 case True 1046 hence "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1047 by (rule hoare_complete) 1048 thus "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F \<^esub>P c Q,A" 1049 by (rule hoare_augment_context) simp 1050next 1051 case False 1052 with cvalid 1053 show ?thesis 1054 by (rule ExFalso) 1055qed 1056 1057 1058lemma hoare_strip_\<Gamma>: 1059 assumes deriv: "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 1060 assumes F': "F' \<subseteq> -F" 1061 shows "strip F' \<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P p Q,A" 1062proof (rule hoare_complete) 1063 from hoare_sound [OF deriv] have "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P p Q,A" 1064 by (simp add: cvalid_def) 1065 from this F' 1066 show "strip F' \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P p Q,A" 1067 by (rule valid_to_valid_strip) 1068qed 1069 1070 1071subsection \<open>And Now: Some Useful Rules\<close> 1072 1073subsubsection \<open>Consequence\<close> 1074 1075 1076lemma LiberalConseq_sound: 1077fixes F::"'f set" 1078assumes cons: "\<forall>s \<in> P. \<forall>(t::('s,'f) xstate). \<exists>P' Q' A'. (\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A') \<and> 1079 ((s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A') 1080 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)" 1081shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A " 1082proof (rule cnvalidI) 1083 fix s t 1084 assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1085 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1086 assume P: "s \<in> P" 1087 assume t_notin_F: "t \<notin> Fault ` F" 1088 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1089 proof - 1090 from P cons obtain P' Q' A' where 1091 spec: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P' c Q',A'" and 1092 adapt: "(s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A') 1093 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A" 1094 apply - 1095 apply (drule (1) bspec) 1096 apply (erule_tac x=t in allE) 1097 apply (elim exE conjE) 1098 apply iprover 1099 done 1100 from exec spec ctxt t_notin_F 1101 have "s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A'" 1102 by (simp add: cnvalid_def nvalid_def) 1103 with adapt show ?thesis 1104 by simp 1105 qed 1106qed 1107 1108lemma LiberalConseq: 1109fixes F:: "'f set" 1110assumes cons: "\<forall>s \<in> P. \<forall>(t::('s,'f) xstate). \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> 1111 ((s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A') 1112 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)" 1113shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A " 1114apply (rule hoare_complete') 1115apply (rule allI) 1116apply (rule LiberalConseq_sound) 1117using cons 1118apply (clarify) 1119apply (drule (1) bspec) 1120apply (erule_tac x=t in allE) 1121apply clarify 1122apply (rule_tac x=P' in exI) 1123apply (rule_tac x=Q' in exI) 1124apply (rule_tac x=A' in exI) 1125apply (rule conjI) 1126apply (blast intro: hoare_cnvalid) 1127apply assumption 1128done 1129 1130lemma "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> Q \<and> A' \<subseteq> A 1131 \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1132 apply (rule LiberalConseq) 1133 apply (rule ballI) 1134 apply (drule (1) bspec) 1135 apply clarify 1136 apply (rule_tac x=P' in exI) 1137 apply (rule_tac x=Q' in exI) 1138 apply (rule_tac x=A' in exI) 1139 apply auto 1140 done 1141 1142lemma 1143fixes F:: "'f set" 1144assumes cons: "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> 1145 (\<forall>(t::('s,'f) xstate). (s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A') 1146 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)" 1147shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A " 1148 apply (rule Conseq) 1149 apply (rule ballI) 1150 apply (insert cons) 1151 apply (drule (1) bspec) 1152 apply clarify 1153 apply (rule_tac x=P' in exI) 1154 apply (rule_tac x=Q' in exI) 1155 apply (rule_tac x=A' in exI) 1156 apply (rule conjI) 1157 apply assumption 1158 (* no way to get s \<in> P' *) 1159 oops 1160 1161lemma LiberalConseq': 1162fixes F:: "'f set" 1163assumes cons: "\<forall>s \<in> P. \<exists>P' Q' A'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' c Q',A' \<and> 1164 (\<forall>(t::('s,'f) xstate). (s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A') 1165 \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)" 1166shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A " 1167apply (rule LiberalConseq) 1168apply (rule ballI) 1169apply (rule allI) 1170apply (insert cons) 1171apply (drule (1) bspec) 1172apply clarify 1173apply (rule_tac x=P' in exI) 1174apply (rule_tac x=Q' in exI) 1175apply (rule_tac x=A' in exI) 1176apply iprover 1177done 1178 1179lemma LiberalConseq'': 1180fixes F:: "'f set" 1181assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" 1182assumes cons: "\<forall>s (t::('s,'f) xstate). 1183 (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in> Normal ` Q' Z \<union> Abrupt ` A' Z) 1184 \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Normal ` Q \<union> Abrupt ` A)" 1185shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A " 1186apply (rule LiberalConseq) 1187apply (rule ballI) 1188apply (rule allI) 1189apply (insert cons) 1190apply (erule_tac x=s in allE) 1191apply (erule_tac x=t in allE) 1192apply (case_tac "t \<in> Normal ` Q \<union> Abrupt ` A") 1193apply (insert spec) 1194apply iprover 1195apply auto 1196done 1197 1198primrec procs:: "('s,'p,'f) com \<Rightarrow> 'p set" 1199where 1200"procs Skip = {}" | 1201"procs (Basic f) = {}" | 1202"procs (Seq c\<^sub>1 c\<^sub>2) = (procs c\<^sub>1 \<union> procs c\<^sub>2)" | 1203"procs (Cond b c\<^sub>1 c\<^sub>2) = (procs c\<^sub>1 \<union> procs c\<^sub>2)" | 1204"procs (While b c) = procs c" | 1205"procs (Call p) = {p}" | 1206"procs (DynCom c) = (\<Union>s. procs (c s))" | 1207"procs (Guard f g c) = procs c" | 1208"procs Throw = {}" | 1209"procs (Catch c\<^sub>1 c\<^sub>2) = (procs c\<^sub>1 \<union> procs c\<^sub>2)" 1210 1211primrec noSpec:: "('s,'p,'f) com \<Rightarrow> bool" 1212where 1213"noSpec Skip = True" | 1214"noSpec (Basic f) = True" | 1215"noSpec (Spec r) = False" | 1216"noSpec (Seq c\<^sub>1 c\<^sub>2) = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)" | 1217"noSpec (Cond b c\<^sub>1 c\<^sub>2) = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)" | 1218"noSpec (While b c) = noSpec c" | 1219"noSpec (Call p) = True" | 1220"noSpec (DynCom c) = (\<forall>s. noSpec (c s))" | 1221"noSpec (Guard f g c) = noSpec c" | 1222"noSpec Throw = True" | 1223"noSpec (Catch c\<^sub>1 c\<^sub>2) = (noSpec c\<^sub>1 \<and> noSpec c\<^sub>2)" 1224 1225lemma exec_noSpec_no_Stuck: 1226 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" 1227 assumes noSpec_c: "noSpec c" 1228 assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))" 1229 assumes procs_subset: "procs c \<subseteq> dom \<Gamma>" 1230 assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>" 1231 assumes s_no_Stuck: "s\<noteq>Stuck" 1232 shows "t\<noteq>Stuck" 1233using exec noSpec_c procs_subset s_no_Stuck proof induct 1234 case (Call p bdy s t) with noSpec_\<Gamma> procs_subset_\<Gamma> show ?case 1235 by (auto dest!: bspec [of _ _ p]) 1236next 1237 case (DynCom c s t) then show ?case 1238 by auto blast 1239qed auto 1240 1241lemma execn_noSpec_no_Stuck: 1242 assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> =n\<Rightarrow> t" 1243 assumes noSpec_c: "noSpec c" 1244 assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))" 1245 assumes procs_subset: "procs c \<subseteq> dom \<Gamma>" 1246 assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>" 1247 assumes s_no_Stuck: "s\<noteq>Stuck" 1248 shows "t\<noteq>Stuck" 1249using exec noSpec_c procs_subset s_no_Stuck proof induct 1250 case (Call p bdy n s t) with noSpec_\<Gamma> procs_subset_\<Gamma> show ?case 1251 by (auto dest!: bspec [of _ _ p]) 1252next 1253 case (DynCom c s t) then show ?case 1254 by auto blast 1255qed auto 1256 1257lemma LiberalConseq_noguards_nothrows_sound: 1258assumes spec: "\<forall>Z. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" 1259assumes cons: "\<forall>s t. (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in> Q' Z ) 1260 \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Q )" 1261assumes noguards_c: "noguards c" 1262assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))" 1263assumes nothrows_c: "nothrows c" 1264assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))" 1265assumes noSpec_c: "noSpec c" 1266assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))" 1267assumes procs_subset: "procs c \<subseteq> dom \<Gamma>" 1268assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>" 1269shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A " 1270proof (rule cnvalidI) 1271 fix s t 1272 assume ctxt:"\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1273 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1274 assume P: "s \<in> P" 1275 assume t_notin_F: "t \<notin> Fault ` F" 1276 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1277 proof - 1278 from execn_noguards_no_Fault [OF exec noguards_c noguards_\<Gamma>] 1279 execn_nothrows_no_Abrupt [OF exec nothrows_c nothrows_\<Gamma> ] 1280 execn_noSpec_no_Stuck [OF exec 1281 noSpec_c noSpec_\<Gamma> procs_subset 1282 procs_subset_\<Gamma>] 1283 obtain t' where t: "t=Normal t'" 1284 by (cases t) auto 1285 with exec spec ctxt 1286 have "(\<forall>Z. s \<in> P' Z \<longrightarrow> t' \<in> Q' Z)" 1287 by (unfold cnvalid_def nvalid_def) blast 1288 with cons P t show ?thesis 1289 by simp 1290 qed 1291qed 1292 1293 1294lemma LiberalConseq_noguards_nothrows: 1295assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) c (Q' Z),(A' Z)" 1296assumes cons: "\<forall>s t. (\<forall>Z. s \<in> P' Z \<longrightarrow> t \<in> Q' Z ) 1297 \<longrightarrow> (s \<in> P \<longrightarrow> t \<in> Q )" 1298assumes noguards_c: "noguards c" 1299assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))" 1300assumes nothrows_c: "nothrows c" 1301assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))" 1302assumes noSpec_c: "noSpec c" 1303assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))" 1304assumes procs_subset: "procs c \<subseteq> dom \<Gamma>" 1305assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>" 1306shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A " 1307apply (rule hoare_complete') 1308apply (rule allI) 1309apply (rule LiberalConseq_noguards_nothrows_sound 1310 [OF _ cons noguards_c noguards_\<Gamma> nothrows_c nothrows_\<Gamma> 1311 noSpec_c noSpec_\<Gamma> 1312 procs_subset procs_subset_\<Gamma>]) 1313apply (insert spec) 1314apply (intro allI) 1315apply (erule_tac x=Z in allE) 1316by (rule hoare_cnvalid) 1317 1318lemma 1319assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=fst Z \<and> P s (snd Z)} c {t. Q (fst Z) (snd Z) t},{}" 1320assumes noguards_c: "noguards c" 1321assumes noguards_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noguards (the (\<Gamma> p))" 1322assumes nothrows_c: "nothrows c" 1323assumes nothrows_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. nothrows (the (\<Gamma> p))" 1324assumes noSpec_c: "noSpec c" 1325assumes noSpec_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. noSpec (the (\<Gamma> p))" 1326assumes procs_subset: "procs c \<subseteq> dom \<Gamma>" 1327assumes procs_subset_\<Gamma>: "\<forall>p \<in> dom \<Gamma>. procs (the (\<Gamma> p)) \<subseteq> dom \<Gamma>" 1328shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>{s. s=\<sigma>} c {t. \<forall>l. P \<sigma> l \<longrightarrow> Q \<sigma> l t},{}" 1329apply (rule allI) 1330apply (rule LiberalConseq_noguards_nothrows 1331 [OF spec _ noguards_c noguards_\<Gamma> nothrows_c nothrows_\<Gamma> 1332 noSpec_c noSpec_\<Gamma> 1333 procs_subset procs_subset_\<Gamma>]) 1334apply auto 1335done 1336 1337subsubsection \<open>Modify Return\<close> 1338 1339lemma ProcModifyReturn_sound: 1340 assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A" 1341 assumes valid_modif: 1342 "\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)" 1343 assumes ret_modif: 1344 "\<forall>s t. t \<in> Modif (init s) 1345 \<longrightarrow> return' s t = return s t" 1346 assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 1347 \<longrightarrow> return' s t = return s t" 1348 shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A" 1349proof (rule cnvalidI) 1350 fix s t 1351 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1352 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 1353 by (auto intro: nvalid_augment_Faults) 1354 assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t" 1355 assume P: "s \<in> P" 1356 assume t_notin_F: "t \<notin> Fault ` F" 1357 from exec 1358 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1359 proof (cases rule: execn_call_Normal_elim) 1360 fix bdy m t' 1361 assume bdy: "\<Gamma> p = Some bdy" 1362 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'" 1363 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t" 1364 assume n: "n = Suc m" 1365 from exec_body n bdy 1366 have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'" 1367 by (auto simp add: intro: execn.Call) 1368 from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P 1369 have "t' \<in> Modif (init s)" 1370 by auto 1371 with ret_modif have "Normal (return' s t') = 1372 Normal (return s t')" 1373 by simp 1374 with exec_body exec_c bdy n 1375 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1376 by (auto intro: execn_call) 1377 from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F 1378 show ?thesis 1379 by simp 1380 next 1381 fix bdy m t' 1382 assume bdy: "\<Gamma> p = Some bdy" 1383 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'" 1384 assume n: "n = Suc m" 1385 assume t: "t = Abrupt (return s t')" 1386 also from exec_body n bdy 1387 have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'" 1388 by (auto simp add: intro: execn.intros) 1389 from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P 1390 have "t' \<in> ModifAbr (init s)" 1391 by auto 1392 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 1393 by simp 1394 finally have "t = Abrupt (return' s t')" . 1395 with exec_body bdy n 1396 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1397 by (auto intro: execn_callAbrupt) 1398 from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F 1399 show ?thesis 1400 by simp 1401 next 1402 fix bdy m f 1403 assume bdy: "\<Gamma> p = Some bdy" 1404 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" 1405 "t = Fault f" 1406 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1407 by (auto intro: execn_callFault) 1408 from valid_call [rule_format] ctxt this P t_notin_F 1409 show ?thesis 1410 by (rule cnvalidD) 1411 next 1412 fix bdy m 1413 assume bdy: "\<Gamma> p = Some bdy" 1414 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m" 1415 "t = Stuck" 1416 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1417 by (auto intro: execn_callStuck) 1418 from valid_call [rule_format] ctxt this P t_notin_F 1419 show ?thesis 1420 by (rule cnvalidD) 1421 next 1422 fix m 1423 assume "\<Gamma> p = None" 1424 and "n = Suc m" "t = Stuck" 1425 then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1426 by (auto intro: execn_callUndefined) 1427 from valid_call [rule_format] ctxt this P t_notin_F 1428 show ?thesis 1429 by (rule cnvalidD) 1430 qed 1431qed 1432 1433 1434lemma ProcModifyReturn: 1435 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 1436 assumes result_conform: 1437 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 1438 assumes return_conform: 1439 "\<forall>s t. t \<in> ModifAbr (init s) 1440 \<longrightarrow> (return' s t) = (return s t)" 1441 assumes modifies_spec: 1442 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)" 1443 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A" 1444apply (rule hoare_complete') 1445apply (rule allI) 1446apply (rule ProcModifyReturn_sound 1447 [where Modif=Modif and ModifAbr=ModifAbr, 1448 OF _ _ result_conform return_conform] ) 1449using spec 1450apply (blast intro: hoare_cnvalid) 1451using modifies_spec 1452apply (blast intro: hoare_cnvalid) 1453done 1454 1455lemma ProcModifyReturnSameFaults_sound: 1456 assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A" 1457 assumes valid_modif: 1458 "\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)" 1459 assumes ret_modif: 1460 "\<forall>s t. t \<in> Modif (init s) 1461 \<longrightarrow> return' s t = return s t" 1462 assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 1463 \<longrightarrow> return' s t = return s t" 1464 shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A" 1465proof (rule cnvalidI) 1466 fix s t 1467 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1468 assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t" 1469 assume P: "s \<in> P" 1470 assume t_notin_F: "t \<notin> Fault ` F" 1471 from exec 1472 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1473 proof (cases rule: execn_call_Normal_elim) 1474 fix bdy m t' 1475 assume bdy: "\<Gamma> p = Some bdy" 1476 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'" 1477 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t" 1478 assume n: "n = Suc m" 1479 from exec_body n bdy 1480 have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'" 1481 by (auto simp add: intro: execn.intros) 1482 from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P 1483 have "t' \<in> Modif (init s)" 1484 by auto 1485 with ret_modif have "Normal (return' s t') = 1486 Normal (return s t')" 1487 by simp 1488 with exec_body exec_c bdy n 1489 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1490 by (auto intro: execn_call) 1491 from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F 1492 show ?thesis 1493 by simp 1494 next 1495 fix bdy m t' 1496 assume bdy: "\<Gamma> p = Some bdy" 1497 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'" 1498 assume n: "n = Suc m" 1499 assume t: "t = Abrupt (return s t')" 1500 also 1501 from exec_body n bdy 1502 have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'" 1503 by (auto simp add: intro: execn.intros) 1504 from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P 1505 have "t' \<in> ModifAbr (init s)" 1506 by auto 1507 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 1508 by simp 1509 finally have "t = Abrupt (return' s t')" . 1510 with exec_body bdy n 1511 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1512 by (auto intro: execn_callAbrupt) 1513 from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F 1514 show ?thesis 1515 by simp 1516 next 1517 fix bdy m f 1518 assume bdy: "\<Gamma> p = Some bdy" 1519 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" and 1520 t: "t = Fault f" 1521 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1522 by (auto intro: execn_callFault) 1523 from cnvalidD [OF valid_call [rule_format] ctxt this P] t t_notin_F 1524 show ?thesis 1525 by simp 1526 next 1527 fix bdy m 1528 assume bdy: "\<Gamma> p = Some bdy" 1529 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m" 1530 "t = Stuck" 1531 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1532 by (auto intro: execn_callStuck) 1533 from valid_call [rule_format] ctxt this P t_notin_F 1534 show ?thesis 1535 by (rule cnvalidD) 1536 next 1537 fix m 1538 assume "\<Gamma> p = None" 1539 and "n = Suc m" "t = Stuck" 1540 then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1541 by (auto intro: execn_callUndefined) 1542 from valid_call [rule_format] ctxt this P t_notin_F 1543 show ?thesis 1544 by (rule cnvalidD) 1545 qed 1546qed 1547 1548 1549lemma ProcModifyReturnSameFaults: 1550 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 1551 assumes result_conform: 1552 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 1553 assumes return_conform: 1554 "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)" 1555 assumes modifies_spec: 1556 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)" 1557 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A" 1558apply (rule hoare_complete') 1559apply (rule allI) 1560apply (rule ProcModifyReturnSameFaults_sound 1561 [where Modif=Modif and ModifAbr=ModifAbr, 1562 OF _ _ result_conform return_conform]) 1563using spec 1564apply (blast intro: hoare_cnvalid) 1565using modifies_spec 1566apply (blast intro: hoare_cnvalid) 1567done 1568 1569subsubsection \<open>DynCall\<close> 1570 1571lemma dynProcModifyReturn_sound: 1572assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 1573assumes valid_modif: 1574 "\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n. 1575 \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1576assumes ret_modif: 1577 "\<forall>s t. t \<in> Modif (init s) 1578 \<longrightarrow> return' s t = return s t" 1579assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 1580 \<longrightarrow> return' s t = return s t" 1581shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1582proof (rule cnvalidI) 1583 fix s t 1584 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1585 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 1586 by (auto intro: nvalid_augment_Faults) 1587 assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t" 1588 assume t_notin_F: "t \<notin> Fault ` F" 1589 assume P: "s \<in> P" 1590 with valid_modif 1591 have valid_modif': "\<forall>\<sigma>. \<forall>n. 1592 \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1593 by blast 1594 from exec 1595 have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t" 1596 by (cases rule: execn_dynCall_Normal_elim) 1597 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 1598 proof (cases rule: execn_call_Normal_elim) 1599 fix bdy m t' 1600 assume bdy: "\<Gamma> (p s) = Some bdy" 1601 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'" 1602 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t" 1603 assume n: "n = Suc m" 1604 from exec_body n bdy 1605 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'" 1606 by (auto simp add: intro: execn.intros) 1607 from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P 1608 have "t' \<in> Modif (init s)" 1609 by auto 1610 with ret_modif have "Normal (return' s t') = Normal (return s t')" 1611 by simp 1612 with exec_body exec_c bdy n 1613 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t" 1614 by (auto intro: execn_call) 1615 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1616 by (rule execn_dynCall) 1617 from cnvalidD [OF valid_call ctxt this] P t_notin_F 1618 show ?thesis 1619 by simp 1620 next 1621 fix bdy m t' 1622 assume bdy: "\<Gamma> (p s) = Some bdy" 1623 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'" 1624 assume n: "n = Suc m" 1625 assume t: "t = Abrupt (return s t')" 1626 also from exec_body n bdy 1627 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'" 1628 by (auto simp add: intro: execn.intros) 1629 from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P 1630 have "t' \<in> ModifAbr (init s)" 1631 by auto 1632 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 1633 by simp 1634 finally have "t = Abrupt (return' s t')" . 1635 with exec_body bdy n 1636 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t" 1637 by (auto intro: execn_callAbrupt) 1638 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1639 by (rule execn_dynCall) 1640 from cnvalidD [OF valid_call ctxt this] P t_notin_F 1641 show ?thesis 1642 by simp 1643 next 1644 fix bdy m f 1645 assume bdy: "\<Gamma> (p s) = Some bdy" 1646 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" 1647 "t = Fault f" 1648 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1649 by (auto intro: execn_callFault) 1650 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1651 by (rule execn_dynCall) 1652 from valid_call ctxt this P t_notin_F 1653 show ?thesis 1654 by (rule cnvalidD) 1655 next 1656 fix bdy m 1657 assume bdy: "\<Gamma> (p s) = Some bdy" 1658 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m" 1659 "t = Stuck" 1660 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1661 by (auto intro: execn_callStuck) 1662 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1663 by (rule execn_dynCall) 1664 from valid_call ctxt this P t_notin_F 1665 show ?thesis 1666 by (rule cnvalidD) 1667 next 1668 fix m 1669 assume "\<Gamma> (p s) = None" 1670 and "n = Suc m" "t = Stuck" 1671 hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1672 by (auto intro: execn_callUndefined) 1673 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1674 by (rule execn_dynCall) 1675 from valid_call ctxt this P t_notin_F 1676 show ?thesis 1677 by (rule cnvalidD) 1678 qed 1679qed 1680 1681lemma dynProcModifyReturn: 1682assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 1683assumes ret_modif: 1684 "\<forall>s t. t \<in> Modif (init s) 1685 \<longrightarrow> return' s t = return s t" 1686assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 1687 \<longrightarrow> return' s t = return s t" 1688assumes modif: 1689 "\<forall>s \<in> P. \<forall>\<sigma>. 1690 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1691shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1692apply (rule hoare_complete') 1693apply (rule allI) 1694apply (rule dynProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr, 1695 OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr]) 1696apply (intro ballI allI) 1697apply (rule hoare_cnvalid [OF modif [rule_format]]) 1698apply assumption 1699done 1700 1701lemma dynProcModifyReturnSameFaults_sound: 1702assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 1703assumes valid_modif: 1704 "\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n. 1705 \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1706assumes ret_modif: 1707 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 1708assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 1709shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1710proof (rule cnvalidI) 1711 fix s t 1712 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1713 assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t" 1714 assume t_notin_F: "t \<notin> Fault ` F" 1715 assume P: "s \<in> P" 1716 with valid_modif 1717 have valid_modif': "\<forall>\<sigma>. \<forall>n. 1718 \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1719 by blast 1720 from exec 1721 have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t" 1722 by (cases rule: execn_dynCall_Normal_elim) 1723 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 1724 proof (cases rule: execn_call_Normal_elim) 1725 fix bdy m t' 1726 assume bdy: "\<Gamma> (p s) = Some bdy" 1727 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'" 1728 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t" 1729 assume n: "n = Suc m" 1730 from exec_body n bdy 1731 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Normal t'" 1732 by (auto simp add: intro: execn.Call) 1733 from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P 1734 have "t' \<in> Modif (init s)" 1735 by auto 1736 with ret_modif have "Normal (return' s t') = Normal (return s t')" 1737 by simp 1738 with exec_body exec_c bdy n 1739 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t" 1740 by (auto intro: execn_call) 1741 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1742 by (rule execn_dynCall) 1743 from cnvalidD [OF valid_call ctxt this] P t_notin_F 1744 show ?thesis 1745 by simp 1746 next 1747 fix bdy m t' 1748 assume bdy: "\<Gamma> (p s) = Some bdy" 1749 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'" 1750 assume n: "n = Suc m" 1751 assume t: "t = Abrupt (return s t')" 1752 also from exec_body n bdy 1753 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'" 1754 by (auto simp add: intro: execn.intros) 1755 from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P 1756 have "t' \<in> ModifAbr (init s)" 1757 by auto 1758 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 1759 by simp 1760 finally have "t = Abrupt (return' s t')" . 1761 with exec_body bdy n 1762 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t" 1763 by (auto intro: execn_callAbrupt) 1764 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1765 by (rule execn_dynCall) 1766 from cnvalidD [OF valid_call ctxt this] P t_notin_F 1767 show ?thesis 1768 by simp 1769 next 1770 fix bdy m f 1771 assume bdy: "\<Gamma> (p s) = Some bdy" 1772 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" and 1773 t: "t = Fault f" 1774 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1775 by (auto intro: execn_callFault) 1776 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1777 by (rule execn_dynCall) 1778 from cnvalidD [OF valid_call ctxt this P] t t_notin_F 1779 show ?thesis 1780 by simp 1781 next 1782 fix bdy m 1783 assume bdy: "\<Gamma> (p s) = Some bdy" 1784 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m" 1785 "t = Stuck" 1786 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1787 by (auto intro: execn_callStuck) 1788 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1789 by (rule execn_dynCall) 1790 from valid_call ctxt this P t_notin_F 1791 show ?thesis 1792 by (rule cnvalidD) 1793 next 1794 fix m 1795 assume "\<Gamma> (p s) = None" 1796 and "n = Suc m" "t = Stuck" 1797 hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t" 1798 by (auto intro: execn_callUndefined) 1799 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t" 1800 by (rule execn_dynCall) 1801 from valid_call ctxt this P t_notin_F 1802 show ?thesis 1803 by (rule cnvalidD) 1804 qed 1805qed 1806 1807lemma dynProcModifyReturnSameFaults: 1808assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 1809assumes ret_modif: 1810 "\<forall>s t. t \<in> Modif (init s) 1811 \<longrightarrow> return' s t = return s t" 1812assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 1813 \<longrightarrow> return' s t = return s t" 1814assumes modif: 1815 "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 1816shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 1817apply (rule hoare_complete') 1818apply (rule allI) 1819apply (rule dynProcModifyReturnSameFaults_sound 1820 [where Modif=Modif and ModifAbr=ModifAbr, 1821 OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr]) 1822apply (intro ballI allI) 1823apply (rule hoare_cnvalid [OF modif [rule_format]]) 1824apply assumption 1825done 1826 1827 1828subsubsection \<open>Conjunction of Postcondition\<close> 1829 1830lemma PostConjI_sound: 1831assumes valid_Q: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1832assumes valid_R: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c R,B" 1833shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 1834proof (rule cnvalidI) 1835 fix s t 1836 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1837 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1838 assume P: "s \<in> P" 1839 assume t_notin_F: "t \<notin> Fault ` F" 1840 from valid_Q [rule_format] ctxt exec P t_notin_F have "t \<in> Normal ` Q \<union> Abrupt ` A" 1841 by (rule cnvalidD) 1842 moreover 1843 from valid_R [rule_format] ctxt exec P t_notin_F have "t \<in> Normal ` R \<union> Abrupt ` B" 1844 by (rule cnvalidD) 1845 ultimately show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> B)" 1846 by blast 1847qed 1848 1849lemma PostConjI: 1850 assumes deriv_Q: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1851 assumes deriv_R: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c R,B" 1852 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 1853apply (rule hoare_complete') 1854apply (rule allI) 1855apply (rule PostConjI_sound) 1856using deriv_Q 1857apply (blast intro: hoare_cnvalid) 1858using deriv_R 1859apply (blast intro: hoare_cnvalid) 1860done 1861 1862lemma Merge_PostConj_sound: 1863 assumes validF: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1864 assumes validG: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/G\<^esub> P' c R,X" 1865 assumes F_G: "F \<subseteq> G" 1866 assumes P_P': "P \<subseteq> P'" 1867 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)" 1868proof (rule cnvalidI) 1869 fix s t 1870 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1871 with F_G have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/G\<^esub> P (Call p) Q,A" 1872 by (auto intro: nvalid_augment_Faults) 1873 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1874 assume P: "s \<in> P" 1875 with P_P' have P': "s \<in> P'" 1876 by auto 1877 assume t_noFault: "t \<notin> Fault ` F" 1878 show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)" 1879 proof - 1880 from cnvalidD [OF validF [rule_format] ctxt exec P t_noFault] 1881 have *: "t \<in> Normal ` Q \<union> Abrupt ` A". 1882 then have "t \<notin> Fault ` G" 1883 by auto 1884 from cnvalidD [OF validG [rule_format] ctxt' exec P' this] 1885 have "t \<in> Normal ` R \<union> Abrupt ` X" . 1886 with * show ?thesis by auto 1887 qed 1888qed 1889 1890lemma Merge_PostConj: 1891 assumes validF: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1892 assumes validG: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/G\<^esub> P' c R,X" 1893 assumes F_G: "F \<subseteq> G" 1894 assumes P_P': "P \<subseteq> P'" 1895 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)" 1896apply (rule hoare_complete') 1897apply (rule allI) 1898apply (rule Merge_PostConj_sound [OF _ _ F_G P_P']) 1899using validF apply (blast intro:hoare_cnvalid) 1900using validG apply (blast intro:hoare_cnvalid) 1901done 1902 1903subsubsection \<open>Weaken Context\<close> 1904 1905 1906lemma WeakenContext_sound: 1907 assumes valid_c: "\<forall>n. \<Gamma>,\<Theta>'\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1908 assumes valid_ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>'. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1909 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1910proof (rule cnvalidI) 1911 fix s t 1912 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1913 with valid_ctxt 1914 have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>'. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1915 by (simp add: cnvalid_def) 1916 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1917 assume P: "s \<in> P" 1918 assume t_notin_F: "t \<notin> Fault ` F" 1919 from valid_c [rule_format] ctxt' exec P t_notin_F 1920 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1921 by (rule cnvalidD) 1922qed 1923 1924lemma WeakenContext: 1925 assumes deriv_c: "\<Gamma>,\<Theta>'\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1926 assumes deriv_ctxt: "\<forall>(P,p,Q,A)\<in>\<Theta>'. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 1927 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1928apply (rule hoare_complete') 1929apply (rule allI) 1930apply (rule WeakenContext_sound) 1931using deriv_c 1932apply (blast intro: hoare_cnvalid) 1933using deriv_ctxt 1934apply (blast intro: hoare_cnvalid) 1935done 1936 1937subsubsection \<open>Guards and Guarantees\<close> 1938 1939lemma SplitGuards_sound: 1940assumes valid_c1: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" 1941assumes valid_c2: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV" 1942assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c" 1943shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 1944proof (rule cnvalidI) 1945 fix s t 1946 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 1947 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 1948 assume P: "s \<in> P" 1949 assume t_notin_F: "t \<notin> Fault ` F" 1950 show "t \<in> Normal ` Q \<union> Abrupt ` A" 1951 proof (cases t) 1952 case Normal 1953 with inter_guards_execn_noFault [OF c exec] 1954 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp 1955 from valid_c1 [rule_format] ctxt this P t_notin_F 1956 show ?thesis 1957 by (rule cnvalidD) 1958 next 1959 case Abrupt 1960 with inter_guards_execn_noFault [OF c exec] 1961 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp 1962 from valid_c1 [rule_format] ctxt this P t_notin_F 1963 show ?thesis 1964 by (rule cnvalidD) 1965 next 1966 case (Fault f) 1967 with exec inter_guards_execn_Fault [OF c] 1968 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Fault f \<or> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> Fault f" 1969 by auto 1970 then show ?thesis 1971 proof (cases rule: disjE [consumes 1]) 1972 assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> Fault f" 1973 from Fault cnvalidD [OF valid_c1 [rule_format] ctxt this P] t_notin_F 1974 show ?thesis 1975 by blast 1976 next 1977 assume "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> =n\<Rightarrow> Fault f" 1978 from Fault cnvalidD [OF valid_c2 [rule_format] ctxt this P] t_notin_F 1979 show ?thesis 1980 by blast 1981 qed 1982 next 1983 case Stuck 1984 with inter_guards_execn_noFault [OF c exec] 1985 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> =n\<Rightarrow> t" by simp 1986 from valid_c1 [rule_format] ctxt this P t_notin_F 1987 show ?thesis 1988 by (rule cnvalidD) 1989 qed 1990qed 1991 1992lemma SplitGuards: 1993 assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c" 1994 assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" 1995 assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV" 1996 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 1997apply (rule hoare_complete') 1998apply (rule allI) 1999apply (rule SplitGuards_sound [OF _ _ c]) 2000using deriv_c1 2001apply (blast intro: hoare_cnvalid) 2002using deriv_c2 2003apply (blast intro: hoare_cnvalid) 2004done 2005 2006lemma CombineStrip_sound: 2007 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2008 assumes valid_strip: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV" 2009 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A" 2010proof (rule cnvalidI) 2011 fix s t 2012 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A" 2013 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2014 by (auto intro: nvalid_augment_Faults) 2015 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2016 assume P: "s \<in> P" 2017 assume t_noFault: "t \<notin> Fault ` {}" 2018 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2019 proof (cases t) 2020 case (Normal t') 2021 from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal 2022 show ?thesis 2023 by auto 2024 next 2025 case (Abrupt t') 2026 from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt 2027 show ?thesis 2028 by auto 2029 next 2030 case (Fault f) 2031 show ?thesis 2032 proof (cases "f \<in> F") 2033 case True 2034 hence "f \<notin> -F" by simp 2035 with exec Fault 2036 have "\<Gamma>\<turnstile>\<langle>strip_guards (-F) c,Normal s\<rangle> =n\<Rightarrow> Fault f" 2037 by (auto intro: execn_to_execn_strip_guards_Fault) 2038 from cnvalidD [OF valid_strip [rule_format] ctxt this P] Fault 2039 have False 2040 by auto 2041 thus ?thesis .. 2042 next 2043 case False 2044 with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault 2045 show ?thesis 2046 by auto 2047 qed 2048 next 2049 case Stuck 2050 from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck 2051 show ?thesis 2052 by auto 2053 qed 2054qed 2055 2056lemma CombineStrip: 2057 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2058 assumes deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV" 2059 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 2060apply (rule hoare_complete') 2061apply (rule allI) 2062apply (rule CombineStrip_sound) 2063apply (iprover intro: hoare_cnvalid [OF deriv]) 2064apply (iprover intro: hoare_cnvalid [OF deriv_strip]) 2065done 2066 2067lemma GuardsFlip_sound: 2068 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2069 assumes validFlip: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/-F\<^esub> P c UNIV,UNIV" 2070 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A" 2071proof (rule cnvalidI) 2072 fix s t 2073 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A" 2074 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2075 by (auto intro: nvalid_augment_Faults) 2076 from ctxt have ctxtFlip: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/-F\<^esub> P (Call p) Q,A" 2077 by (auto intro: nvalid_augment_Faults) 2078 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2079 assume P: "s \<in> P" 2080 assume t_noFault: "t \<notin> Fault ` {}" 2081 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2082 proof (cases t) 2083 case (Normal t') 2084 from cnvalidD [OF valid [rule_format] ctxt' exec P] Normal 2085 show ?thesis 2086 by auto 2087 next 2088 case (Abrupt t') 2089 from cnvalidD [OF valid [rule_format] ctxt' exec P] Abrupt 2090 show ?thesis 2091 by auto 2092 next 2093 case (Fault f) 2094 show ?thesis 2095 proof (cases "f \<in> F") 2096 case True 2097 hence "f \<notin> -F" by simp 2098 with cnvalidD [OF validFlip [rule_format] ctxtFlip exec P] Fault 2099 have False 2100 by auto 2101 thus ?thesis .. 2102 next 2103 case False 2104 with cnvalidD [OF valid [rule_format] ctxt' exec P] Fault 2105 show ?thesis 2106 by auto 2107 qed 2108 next 2109 case Stuck 2110 from cnvalidD [OF valid [rule_format] ctxt' exec P] Stuck 2111 show ?thesis 2112 by auto 2113 qed 2114qed 2115 2116lemma GuardsFlip: 2117 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2118 assumes derivFlip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV" 2119 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 2120apply (rule hoare_complete') 2121apply (rule allI) 2122apply (rule GuardsFlip_sound) 2123apply (iprover intro: hoare_cnvalid [OF deriv]) 2124apply (iprover intro: hoare_cnvalid [OF derivFlip]) 2125done 2126 2127lemma MarkGuardsI_sound: 2128 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A" 2129 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 2130proof (rule cnvalidI) 2131 fix s t 2132 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A" 2133 assume exec: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> t" 2134 from execn_mark_guards_to_execn [OF exec] obtain t' where 2135 exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t'" and 2136 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 2137 by blast 2138 assume P: "s \<in> P" 2139 assume t_noFault: "t \<notin> Fault ` {}" 2140 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2141 proof - 2142 from cnvalidD [OF valid [rule_format] ctxt exec_c P] 2143 have "t' \<in> Normal ` Q \<union> Abrupt ` A" 2144 by blast 2145 with t'_noFault 2146 show ?thesis 2147 by auto 2148 qed 2149qed 2150 2151lemma MarkGuardsI: 2152 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 2153 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 2154apply (rule hoare_complete') 2155apply (rule allI) 2156apply (rule MarkGuardsI_sound) 2157apply (iprover intro: hoare_cnvalid [OF deriv]) 2158done 2159 2160lemma MarkGuardsD_sound: 2161 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 2162 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A" 2163proof (rule cnvalidI) 2164 fix s t 2165 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A" 2166 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2167 assume P: "s \<in> P" 2168 assume t_noFault: "t \<notin> Fault ` {}" 2169 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2170 proof (cases "isFault t") 2171 case True 2172 with execn_to_execn_mark_guards_Fault [OF exec ] 2173 obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> Fault f'" 2174 by (fastforce elim: isFaultE) 2175 from cnvalidD [OF valid [rule_format] ctxt this P] 2176 have False 2177 by auto 2178 thus ?thesis .. 2179 next 2180 case False 2181 from execn_to_execn_mark_guards [OF exec False] 2182 obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> =n\<Rightarrow> t" 2183 by auto 2184 from cnvalidD [OF valid [rule_format] ctxt this P] 2185 show ?thesis 2186 by auto 2187 qed 2188qed 2189 2190lemma MarkGuardsD: 2191 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 2192 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 2193apply (rule hoare_complete') 2194apply (rule allI) 2195apply (rule MarkGuardsD_sound) 2196apply (iprover intro: hoare_cnvalid [OF deriv]) 2197done 2198 2199lemma MergeGuardsI_sound: 2200 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2201 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P merge_guards c Q,A" 2202proof (rule cnvalidI) 2203 fix s t 2204 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2205 assume exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> =n\<Rightarrow> t" 2206 from execn_merge_guards_to_execn [OF exec_merge] 2207 have exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" . 2208 assume P: "s \<in> P" 2209 assume t_notin_F: "t \<notin> Fault ` F" 2210 from cnvalidD [OF valid [rule_format] ctxt exec P t_notin_F] 2211 show "t \<in> Normal ` Q \<union> Abrupt ` A". 2212qed 2213 2214lemma MergeGuardsI: 2215 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2216 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P merge_guards c Q,A" 2217apply (rule hoare_complete') 2218apply (rule allI) 2219apply (rule MergeGuardsI_sound) 2220apply (iprover intro: hoare_cnvalid [OF deriv]) 2221done 2222 2223lemma MergeGuardsD_sound: 2224 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P merge_guards c Q,A" 2225 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2226proof (rule cnvalidI) 2227 fix s t 2228 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2229 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2230 from execn_to_execn_merge_guards [OF exec] 2231 have exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> =n\<Rightarrow> t". 2232 assume P: "s \<in> P" 2233 assume t_notin_F: "t \<notin> Fault ` F" 2234 from cnvalidD [OF valid [rule_format] ctxt exec_merge P t_notin_F] 2235 show "t \<in> Normal ` Q \<union> Abrupt ` A". 2236qed 2237 2238lemma MergeGuardsD: 2239 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P merge_guards c Q,A" 2240 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2241apply (rule hoare_complete') 2242apply (rule allI) 2243apply (rule MergeGuardsD_sound) 2244apply (iprover intro: hoare_cnvalid [OF deriv]) 2245done 2246 2247 2248lemma SubsetGuards_sound: 2249 assumes c_c': "c \<subseteq>\<^sub>g c'" 2250 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c' Q,A" 2251 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/{}\<^esub> P c Q,A" 2252proof (rule cnvalidI) 2253 fix s t 2254 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/{}\<^esub> P (Call p) Q,A" 2255 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2256 from execn_to_execn_subseteq_guards [OF c_c' exec] obtain t' where 2257 exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> =n\<Rightarrow> t'" and 2258 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 2259 by blast 2260 assume P: "s \<in> P" 2261 assume t_noFault: "t \<notin> Fault ` {}" 2262 from cnvalidD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault 2263 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2264 by auto 2265qed 2266 2267lemma SubsetGuards: 2268 assumes c_c': "c \<subseteq>\<^sub>g c'" 2269 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c' Q,A" 2270 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P c Q,A" 2271apply (rule hoare_complete') 2272apply (rule allI) 2273apply (rule SubsetGuards_sound [OF c_c']) 2274apply (iprover intro: hoare_cnvalid [OF deriv]) 2275done 2276 2277lemma NormalizeD_sound: 2278 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (normalize c) Q,A" 2279 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2280proof (rule cnvalidI) 2281 fix s t 2282 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2283 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2284 hence exec_norm: "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> =n\<Rightarrow> t" 2285 by (rule execn_to_execn_normalize) 2286 assume P: "s \<in> P" 2287 assume noFault: "t \<notin> Fault ` F" 2288 from cnvalidD [OF valid [rule_format] ctxt exec_norm P noFault] 2289 show "t \<in> Normal ` Q \<union> Abrupt ` A". 2290qed 2291 2292lemma NormalizeD: 2293 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (normalize c) Q,A" 2294 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2295apply (rule hoare_complete') 2296apply (rule allI) 2297apply (rule NormalizeD_sound) 2298apply (iprover intro: hoare_cnvalid [OF deriv]) 2299done 2300 2301lemma NormalizeI_sound: 2302 assumes valid: "\<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2303 shows "\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> P (normalize c) Q,A" 2304proof (rule cnvalidI) 2305 fix s t 2306 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A" 2307 assume "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> =n\<Rightarrow> t" 2308 hence exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2309 by (rule execn_normalize_to_execn) 2310 assume P: "s \<in> P" 2311 assume noFault: "t \<notin> Fault ` F" 2312 from cnvalidD [OF valid [rule_format] ctxt exec P noFault] 2313 show "t \<in> Normal ` Q \<union> Abrupt ` A". 2314qed 2315 2316lemma NormalizeI: 2317 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2318 shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (normalize c) Q,A" 2319apply (rule hoare_complete') 2320apply (rule allI) 2321apply (rule NormalizeI_sound) 2322apply (iprover intro: hoare_cnvalid [OF deriv]) 2323done 2324 2325 2326subsubsection \<open>Restricting the Procedure Environment\<close> 2327 2328lemma nvalid_restrict_to_nvalid: 2329assumes valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2330shows "\<Gamma>\<Turnstile>n:\<^bsub>/F\<^esub> P c Q,A" 2331proof (rule nvalidI) 2332 fix s t 2333 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t" 2334 assume P: "s \<in> P" 2335 assume t_notin_F: "t \<notin> Fault ` F" 2336 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2337 proof - 2338 from execn_to_execn_restrict [OF exec] 2339 obtain t' where 2340 exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t'" and 2341 t_Fault: "\<forall>f. t = Fault f \<longrightarrow> t' \<in> {Fault f, Stuck}" and 2342 t'_notStuck: "t'\<noteq>Stuck \<longrightarrow> t'=t" 2343 by blast 2344 from t_Fault t_notin_F t'_notStuck have "t' \<notin> Fault ` F" 2345 by (cases t') auto 2346 with valid_c exec_res P 2347 have "t' \<in> Normal ` Q \<union> Abrupt ` A" 2348 by (auto simp add: nvalid_def) 2349 with t'_notStuck 2350 show ?thesis 2351 by auto 2352 qed 2353qed 2354 2355lemma valid_restrict_to_valid: 2356assumes valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 2357shows "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 2358proof (rule validI) 2359 fix s t 2360 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 2361 assume P: "s \<in> P" 2362 assume t_notin_F: "t \<notin> Fault ` F" 2363 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2364 proof - 2365 from exec_to_exec_restrict [OF exec] 2366 obtain t' where 2367 exec_res: "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t'" and 2368 t_Fault: "\<forall>f. t = Fault f \<longrightarrow> t' \<in> {Fault f, Stuck}" and 2369 t'_notStuck: "t'\<noteq>Stuck \<longrightarrow> t'=t" 2370 by blast 2371 from t_Fault t_notin_F t'_notStuck have "t' \<notin> Fault ` F" 2372 by (cases t') auto 2373 with valid_c exec_res P 2374 have "t' \<in> Normal ` Q \<union> Abrupt ` A" 2375 by (auto simp add: valid_def) 2376 with t'_notStuck 2377 show ?thesis 2378 by auto 2379 qed 2380qed 2381 2382lemma augment_procs: 2383assumes deriv_c: "\<Gamma>|\<^bsub>M\<^esub>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2384shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2385 apply (rule hoare_complete) 2386 apply (rule valid_restrict_to_valid) 2387 apply (insert hoare_sound [OF deriv_c]) 2388 by (simp add: cvalid_def) 2389 2390lemma augment_Faults: 2391assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 2392assumes F: "F \<subseteq> F'" 2393shows "\<Gamma>,{}\<turnstile>\<^bsub>/F'\<^esub> P c Q,A" 2394 apply (rule hoare_complete) 2395 apply (rule valid_augment_Faults [OF _ F]) 2396 apply (insert hoare_sound [OF deriv_c]) 2397 by (simp add: cvalid_def) 2398 2399end 2400