1(* 2 Author: Norbert Schirmer 3 Maintainer: Norbert Schirmer, norbert.schirmer at web de 4 License: LGPL 5*) 6 7(* Title: HoarePartial.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 Total Correctness Hoare Logic\<close> 30 31theory HoareTotalProps imports SmallStep HoareTotalDef HoarePartialProps begin 32 33subsection \<open>Soundness\<close> 34 35lemma hoaret_sound: 36 assumes hoare: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 37 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 38using hoare 39proof (induct) 40 case (Skip \<Theta> F P A) 41 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Skip P,A" 42 proof (rule cvalidtI) 43 fix s t 44 assume "\<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow> t" "s \<in> P" 45 thus "t \<in> Normal ` P \<union> Abrupt ` A" 46 by cases auto 47 next 48 fix s show "\<Gamma>\<turnstile>Skip \<down> Normal s" 49 by (rule terminates.intros) 50 qed 51next 52 case (Basic \<Theta> F f P A) 53 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. f s \<in> P} (Basic f) P,A" 54 proof (rule cvalidtI) 55 fix s t 56 assume "\<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow> t" "s \<in> {s. f s \<in> P}" 57 thus "t \<in> Normal ` P \<union> Abrupt ` A" 58 by cases auto 59 next 60 fix s show "\<Gamma>\<turnstile>Basic f \<down> Normal s" 61 by (rule terminates.intros) 62 qed 63next 64 case (Spec \<Theta> F r Q A) 65 show "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^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" 66 proof (rule cvalidtI) 67 fix s t 68 assume "\<Gamma>\<turnstile>\<langle>Spec r ,Normal s\<rangle> \<Rightarrow> t" 69 "s \<in> {s. (\<forall>t. (s, t) \<in> r \<longrightarrow> t \<in> Q) \<and> (\<exists>t. (s, t) \<in> r)}" 70 thus "t \<in> Normal ` Q \<union> Abrupt ` A" 71 by cases auto 72 next 73 fix s show "\<Gamma>\<turnstile>Spec r \<down> Normal s" 74 by (rule terminates.intros) 75 qed 76next 77 case (Seq \<Theta> F P c1 R A c2 Q) 78 have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c1 R,A" by fact 79 have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> R c2 Q,A" by fact 80 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Seq c1 c2 Q,A" 81 proof (rule cvalidtI) 82 fix s t 83 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 84 assume exec: "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow> t" 85 assume P: "s \<in> P" 86 assume t_notin_F: "t \<notin> Fault ` F" 87 from exec P obtain r where 88 exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> r" and exec_c2: "\<Gamma>\<turnstile>\<langle>c2,r\<rangle> \<Rightarrow> t" 89 by cases auto 90 with t_notin_F have "r \<notin> Fault ` F" 91 by (auto dest: Fault_end) 92 from valid_c1 ctxt exec_c1 P this 93 have r: "r \<in> Normal ` R \<union> Abrupt ` A" 94 by (rule cvalidt_postD) 95 show "t\<in>Normal ` Q \<union> Abrupt ` A" 96 proof (cases r) 97 case (Normal r') 98 with exec_c2 r 99 show "t\<in>Normal ` Q \<union> Abrupt ` A" 100 apply - 101 apply (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F]) 102 apply auto 103 done 104 next 105 case (Abrupt r') 106 with exec_c2 have "t=Abrupt r'" 107 by (auto elim: exec_elim_cases) 108 with Abrupt r show ?thesis 109 by auto 110 next 111 case Fault with r show ?thesis by blast 112 next 113 case Stuck with r show ?thesis by blast 114 qed 115 next 116 fix s 117 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 118 assume P: "s\<in>P" 119 show "\<Gamma>\<turnstile>Seq c1 c2 \<down> Normal s" 120 proof - 121 from valid_c1 ctxt P 122 have "\<Gamma>\<turnstile>c1\<down> Normal s" 123 by (rule cvalidt_termD) 124 moreover 125 { 126 fix r assume exec_c1: "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> r" 127 have "\<Gamma>\<turnstile>c2 \<down> r" 128 proof (cases r) 129 case (Normal r') 130 with cvalidt_postD [OF valid_c1 ctxt exec_c1 P] 131 have r: "r\<in>Normal ` R" 132 by auto 133 with cvalidt_termD [OF valid_c2 ctxt] exec_c1 134 show "\<Gamma>\<turnstile>c2 \<down> r" 135 by auto 136 qed auto 137 } 138 ultimately show ?thesis 139 by (iprover intro: terminates.intros) 140 qed 141 qed 142next 143 case (Cond \<Theta> F P b c1 Q A c2) 144 have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> b) c1 Q,A" by fact 145 have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> - b) c2 Q,A" by fact 146 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Cond b c1 c2 Q,A" 147 proof (rule cvalidtI) 148 fix s t 149 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 150 assume exec: "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow> t" 151 assume P: "s \<in> P" 152 assume t_notin_F: "t \<notin> Fault ` F" 153 show "t \<in> Normal ` Q \<union> Abrupt ` A" 154 proof (cases "s\<in>b") 155 case True 156 with exec have "\<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow> t" 157 by cases auto 158 with P True 159 show ?thesis 160 by - (rule cvalidt_postD [OF valid_c1 ctxt _ _ t_notin_F],auto) 161 next 162 case False 163 with exec P have "\<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow> t" 164 by cases auto 165 with P False 166 show ?thesis 167 by - (rule cvalidt_postD [OF valid_c2 ctxt _ _ t_notin_F],auto) 168 qed 169 next 170 fix s 171 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 172 assume P: "s \<in> P" 173 thus "\<Gamma>\<turnstile>Cond b c1 c2 \<down> Normal s" 174 using cvalidt_termD [OF valid_c1 ctxt] cvalidt_termD [OF valid_c2 ctxt] 175 by (cases "s \<in> b") (auto intro: terminates.intros) 176 qed 177next 178 case (While r \<Theta> F P b c A) 179 assume wf: "wf r" 180 have valid_c: "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> P \<inter> b) c ({t. (t, \<sigma>) \<in> r} \<inter> P),A" 181 using While.hyps by iprover 182 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (While b c) (P \<inter> - b),A" 183 proof (rule cvalidtI) 184 fix s t 185 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 186 assume wprems: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t" "s \<in> P" "t \<notin> Fault ` F" 187 from wf 188 have "\<And>t. \<lbrakk>\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t; s \<in> P; t \<notin> Fault ` F\<rbrakk> 189 \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" 190 proof (induct) 191 fix s t 192 assume hyp: 193 "\<And>s' t. \<lbrakk>(s',s)\<in>r; \<Gamma>\<turnstile>\<langle>While b c,Normal s'\<rangle> \<Rightarrow> t; s' \<in> P; t \<notin> Fault ` F\<rbrakk> 194 \<Longrightarrow> t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" 195 assume exec: "\<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow> t" 196 assume P: "s \<in> P" 197 assume t_notin_F: "t \<notin> Fault ` F" 198 from exec 199 show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" 200 proof (cases) 201 fix s' 202 assume b: "s\<in>b" 203 assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> s'" 204 assume exec_w: "\<Gamma>\<turnstile>\<langle>While b c,s'\<rangle> \<Rightarrow> t" 205 from exec_w t_notin_F have "s' \<notin> Fault ` F" 206 by (auto dest: Fault_end) 207 from exec_c P b valid_c ctxt this 208 have s': "s' \<in> Normal ` ({s'. (s', s) \<in> r} \<inter> P) \<union> Abrupt ` A" 209 by (auto simp add: cvalidt_def validt_def valid_def) 210 show ?thesis 211 proof (cases s') 212 case Normal 213 with exec_w s' t_notin_F 214 show ?thesis 215 by - (rule hyp,auto) 216 next 217 case Abrupt 218 with exec_w have "t=s'" 219 by (auto dest: Abrupt_end) 220 with Abrupt s' show ?thesis 221 by blast 222 next 223 case Fault 224 with exec_w have "t=s'" 225 by (auto dest: Fault_end) 226 with Fault s' show ?thesis 227 by blast 228 next 229 case Stuck 230 with exec_w have "t=s'" 231 by (auto dest: Stuck_end) 232 with Stuck s' show ?thesis 233 by blast 234 qed 235 next 236 assume "s\<notin>b" "t=Normal s" with P show ?thesis by simp 237 qed 238 qed 239 with wprems show "t \<in> Normal ` (P \<inter> - b) \<union> Abrupt ` A" by blast 240 next 241 fix s 242 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 243 assume "s \<in> P" 244 with wf 245 show "\<Gamma>\<turnstile>While b c \<down> Normal s" 246 proof (induct) 247 fix s 248 assume hyp: "\<And>s'. \<lbrakk>(s',s)\<in>r; s' \<in> P\<rbrakk> 249 \<Longrightarrow> \<Gamma>\<turnstile>While b c \<down> Normal s'" 250 assume P: "s \<in> P" 251 show "\<Gamma>\<turnstile>While b c \<down> Normal s" 252 proof (cases "s \<in> b") 253 case False with P show ?thesis 254 by (blast intro: terminates.intros) 255 next 256 case True 257 with valid_c P ctxt 258 have "\<Gamma>\<turnstile>c \<down> Normal s" 259 by (simp add: cvalidt_def validt_def) 260 moreover 261 { 262 fix s' 263 assume exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> s'" 264 have "\<Gamma>\<turnstile>While b c \<down> s'" 265 proof (cases s') 266 case (Normal s'') 267 with exec_c P True valid_c ctxt 268 have s': "s' \<in> Normal ` ({s'. (s', s) \<in> r} \<inter> P)" 269 by (fastforce simp add: cvalidt_def validt_def valid_def) 270 then show ?thesis 271 by (blast intro: hyp) 272 qed auto 273 } 274 ultimately 275 show ?thesis 276 by (blast intro: terminates.intros) 277 qed 278 qed 279 qed 280next 281 case (Guard \<Theta> F g P c Q A f) 282 have valid_c: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact 283 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) Guard f g c Q,A" 284 proof (rule cvalidtI) 285 fix s t 286 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 287 assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t" 288 assume t_notin_F: "t \<notin> Fault ` F" 289 assume P:"s \<in> (g \<inter> P)" 290 from exec P have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 291 by cases auto 292 from valid_c ctxt this P t_notin_F 293 show "t \<in> Normal ` Q \<union> Abrupt ` A" 294 by (rule cvalidt_postD) 295 next 296 fix s 297 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 298 assume P:"s \<in> (g \<inter> P)" 299 thus "\<Gamma>\<turnstile>Guard f g c \<down> Normal s" 300 by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt]) 301 qed 302next 303 case (Guarantee f F \<Theta> g P c Q A) 304 have valid_c: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) c Q,A" by fact 305 have f_F: "f \<in> F" by fact 306 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Guard f g c Q,A" 307 proof (rule cvalidtI) 308 fix s t 309 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 310 assume exec: "\<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t" 311 assume t_notin_F: "t \<notin> Fault ` F" 312 assume P:"s \<in> P" 313 from exec f_F t_notin_F have g: "s \<in> g" 314 by cases auto 315 with P have P': "s \<in> g \<inter> P" 316 by blast 317 from exec g have "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 318 by cases auto 319 from valid_c ctxt this P' t_notin_F 320 show "t \<in> Normal ` Q \<union> Abrupt ` A" 321 by (rule cvalidt_postD) 322 next 323 fix s 324 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 325 assume P:"s \<in> P" 326 thus "\<Gamma>\<turnstile>Guard f g c \<down> Normal s" 327 by (auto intro: terminates.intros cvalidt_termD [OF valid_c ctxt]) 328 qed 329next 330 case (CallRec P p Q A Specs r Specs_wf \<Theta> F) 331 have p: "(P,p,Q,A) \<in> Specs" by fact 332 have wf: "wf r" by fact 333 have Specs_wf: 334 "Specs_wf = (\<lambda>p \<tau>. (\<lambda>(P,q,Q,A). (P \<inter> {s. ((s, q),\<tau>,p) \<in> r},q,Q,A)) ` Specs)" by fact 335 from CallRec.hyps 336 have valid_body: 337 "\<forall>(P, p, Q, A)\<in>Specs. p \<in> dom \<Gamma> \<and> 338 (\<forall>\<tau>. \<Gamma>,\<Theta> \<union> Specs_wf p \<tau>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) the (\<Gamma> p) Q,A)" by auto 339 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 340 proof - 341 { 342 fix \<tau>p 343 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 344 from wf 345 have "\<And>\<tau> p P Q A. \<lbrakk>\<tau>p = (\<tau>,p); (P,p,Q,A) \<in> Specs\<rbrakk> \<Longrightarrow> 346 \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> (p))) Q,A" 347 proof (induct \<tau>p rule: wf_induct [rule_format, consumes 1, case_names WF]) 348 case (WF \<tau>p \<tau> p P Q A) 349 have \<tau>p: "\<tau>p = (\<tau>, p)" by fact 350 have p: "(P, p, Q, A) \<in> Specs" by fact 351 { 352 fix q P' Q' A' 353 assume q: "(P',q,Q',A') \<in> Specs" 354 have "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}) (Call q) Q',A'" 355 proof (rule validtI) 356 fix s t 357 assume exec_q: 358 "\<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow> t" 359 assume Pre: "s \<in> P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}" 360 assume t_notin_F: "t \<notin> Fault ` F" 361 from Pre q \<tau>p 362 have valid_bdy: 363 "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P') the (\<Gamma> q) Q',A'" 364 by - (rule WF.hyps, auto) 365 from Pre q 366 have Pre': "s \<in> {s} \<inter> P'" 367 by auto 368 from exec_q show "t \<in> Normal ` Q' \<union> Abrupt ` A'" 369 proof (cases) 370 fix bdy 371 assume bdy: "\<Gamma> q = Some bdy" 372 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t" 373 from valid_bdy [simplified bdy option.sel] t_notin_F exec_bdy Pre' 374 have "t \<in> Normal ` Q' \<union> Abrupt ` A'" 375 by (auto simp add: validt_def valid_def) 376 with Pre q 377 show ?thesis 378 by auto 379 next 380 assume "\<Gamma> q = None" 381 with q valid_body have False by auto 382 thus ?thesis .. 383 qed 384 next 385 fix s 386 assume Pre: "s \<in> P' \<inter> {s. ((s,q), \<tau>,p) \<in> r}" 387 from Pre q \<tau>p 388 have valid_bdy: 389 "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s} \<inter> P') (the (\<Gamma> q)) Q',A'" 390 by - (rule WF.hyps, auto) 391 from Pre q 392 have Pre': "s \<in> {s} \<inter> P'" 393 by auto 394 from valid_bdy ctxt Pre' 395 have "\<Gamma>\<turnstile>the (\<Gamma> q) \<down> Normal s" 396 by (auto simp add: validt_def) 397 with valid_body q 398 show "\<Gamma>\<turnstile>Call q\<down> Normal s" 399 by (fastforce intro: terminates.Call) 400 qed 401 } 402 hence "\<forall>(P, p, Q, A)\<in>Specs_wf p \<tau>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Call p Q,A" 403 by (auto simp add: cvalidt_def Specs_wf) 404 with ctxt have "\<forall>(P, p, Q, A)\<in>\<Theta> \<union> Specs_wf p \<tau>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Call p Q,A" 405 by auto 406 with p valid_body 407 show "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A" 408 by (simp add: cvalidt_def) blast 409 qed 410 } 411 note lem = this 412 have valid_body': 413 "\<And>\<tau>. \<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A \<Longrightarrow> 414 \<forall>(P,p,Q,A)\<in>Specs. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> P) (the (\<Gamma> p)) Q,A" 415 by (auto intro: lem) 416 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 417 proof (rule cvalidtI) 418 fix s t 419 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 420 assume exec_call: "\<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow> t" 421 assume P: "s \<in> P" 422 assume t_notin_F: "t \<notin> Fault ` F" 423 from exec_call show "t \<in> Normal ` Q \<union> Abrupt ` A" 424 proof (cases) 425 fix bdy 426 assume bdy: "\<Gamma> p = Some bdy" 427 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal s\<rangle> \<Rightarrow> t" 428 from exec_body bdy p P t_notin_F 429 valid_body' [of "s", OF ctxt] 430 ctxt 431 have "t \<in> Normal ` Q \<union> Abrupt ` A" 432 apply (simp only: cvalidt_def validt_def valid_def) 433 apply (drule (1) bspec) 434 apply auto 435 done 436 with p P 437 show ?thesis 438 by simp 439 next 440 assume "\<Gamma> p = None" 441 with p valid_body have False by auto 442 thus ?thesis by simp 443 qed 444 next 445 fix s 446 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 447 assume P: "s \<in> P" 448 show "\<Gamma>\<turnstile>Call p \<down> Normal s" 449 proof - 450 from ctxt P p valid_body' [of "s",OF ctxt] 451 have "\<Gamma>\<turnstile>(the (\<Gamma> p)) \<down> Normal s" 452 by (auto simp add: cvalidt_def validt_def) 453 with valid_body p show ?thesis 454 by (fastforce intro: terminates.Call) 455 qed 456 qed 457 qed 458next 459 case (DynCom P \<Theta> F c Q A) 460 hence valid_c: "\<forall>s\<in>P. \<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (c s) Q,A" by simp 461 show "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P DynCom c Q,A" 462 proof (rule cvalidtI) 463 fix s t 464 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 465 assume exec: "\<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow> t" 466 assume P: "s \<in> P" 467 assume t_notin_F: "t \<notin> Fault ` F" 468 from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" 469 proof (cases) 470 assume "\<Gamma>\<turnstile>\<langle>c s,Normal s\<rangle> \<Rightarrow> t" 471 from cvalidt_postD [OF valid_c [rule_format, OF P] ctxt this P t_notin_F] 472 show ?thesis . 473 qed 474 next 475 fix s 476 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 477 assume P: "s \<in> P" 478 show "\<Gamma>\<turnstile>DynCom c \<down> Normal s" 479 proof - 480 from cvalidt_termD [OF valid_c [rule_format, OF P] ctxt P] 481 have "\<Gamma>\<turnstile>c s \<down> Normal s" . 482 thus ?thesis 483 by (rule terminates.intros) 484 qed 485 qed 486next 487 case (Throw \<Theta> F A Q) 488 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> A Throw Q,A" 489 proof (rule cvalidtI) 490 fix s t 491 assume "\<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow> t" "s \<in> A" 492 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 493 by cases simp 494 next 495 fix s 496 show "\<Gamma>\<turnstile>Throw \<down> Normal s" 497 by (rule terminates.intros) 498 qed 499next 500 case (Catch \<Theta> F P c\<^sub>1 Q R c\<^sub>2 A) 501 have valid_c1: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,R" by fact 502 have valid_c2: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> R c\<^sub>2 Q,A" by fact 503 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A" 504 proof (rule cvalidtI) 505 fix s t 506 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 507 assume exec: "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t" 508 assume P: "s \<in> P" 509 assume t_notin_F: "t \<notin> Fault ` F" 510 from exec show "t \<in> Normal ` Q \<union> Abrupt ` A" 511 proof (cases) 512 fix s' 513 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt s'" 514 assume exec_c2: "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s'\<rangle> \<Rightarrow> t" 515 from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] 516 have "Abrupt s' \<in> Abrupt ` R" 517 by auto 518 with cvalidt_postD [OF valid_c2 ctxt] exec_c2 t_notin_F 519 show ?thesis 520 by fastforce 521 next 522 assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" 523 assume notAbr: "\<not> isAbr t" 524 from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] t_notin_F 525 have "t \<in> Normal ` Q \<union> Abrupt ` R" . 526 with notAbr 527 show ?thesis 528 by auto 529 qed 530 next 531 fix s 532 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 533 assume P: "s \<in> P" 534 show "\<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s" 535 proof - 536 from valid_c1 ctxt P 537 have "\<Gamma>\<turnstile>c\<^sub>1\<down> Normal s" 538 by (rule cvalidt_termD) 539 moreover 540 { 541 fix r assume exec_c1: "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt r" 542 from cvalidt_postD [OF valid_c1 ctxt exec_c1 P] 543 have r: "Abrupt r\<in>Normal ` Q \<union> Abrupt ` R" 544 by auto 545 hence "Abrupt r\<in>Abrupt ` R" by fast 546 with cvalidt_termD [OF valid_c2 ctxt] exec_c1 547 have "\<Gamma>\<turnstile>c\<^sub>2 \<down> Normal r" 548 by fast 549 } 550 ultimately show ?thesis 551 by (iprover intro: terminates.intros) 552 qed 553 qed 554next 555 case (Conseq P \<Theta> F c Q A) 556 hence adapt: 557 "\<forall>s \<in> P. (\<exists>P' Q' A'. (\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A') \<and> s \<in> P'\<and> Q' \<subseteq> Q \<and> A' \<subseteq> A)" by blast 558 show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 559 proof (rule cvalidtI) 560 fix s t 561 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 562 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 563 assume P: "s \<in> P" 564 assume t_notin_F: "t \<notin> Fault ` F" 565 show "t \<in> Normal ` Q \<union> Abrupt ` A" 566 proof - 567 from adapt [rule_format, OF P] 568 obtain P' and Q' and A' where 569 valid_P'_Q': "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A'" 570 and weaken: "s \<in> P'" "Q' \<subseteq> Q" "A'\<subseteq> A" 571 by blast 572 from exec valid_P'_Q' ctxt t_notin_F 573 have P'_Q': "Normal s \<in> Normal ` P' \<longrightarrow> 574 t \<in> Normal ` Q' \<union> Abrupt ` A'" 575 by (unfold cvalidt_def validt_def valid_def) blast 576 hence "s \<in> P' \<longrightarrow> t \<in> Normal ` Q' \<union> Abrupt ` A'" 577 by blast 578 with weaken 579 show ?thesis 580 by blast 581 qed 582 next 583 fix s 584 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 585 assume P: "s \<in> P" 586 show "\<Gamma>\<turnstile>c \<down> Normal s" 587 proof - 588 from P adapt 589 obtain P' and Q' and A' where 590 "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P' c Q',A'" 591 "s \<in> P'" 592 by blast 593 with ctxt 594 show ?thesis 595 by (simp add: cvalidt_def validt_def) 596 qed 597 qed 598next 599 case (Asm P p Q A \<Theta> F) 600 assume "(P, p, Q, A) \<in> \<Theta>" 601 then show "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 602 by (auto simp add: cvalidt_def ) 603next 604 case ExFalso thus ?case by iprover 605qed 606 607lemma hoaret_sound': 608"\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 609 apply (drule hoaret_sound) 610 apply (simp add: cvalidt_def) 611 done 612 613theorem total_to_partial: 614 assumes total: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" shows "\<Gamma>,{}\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 615proof - 616 from total have "\<Gamma>,{}\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 617 by (rule hoaret_sound) 618 hence "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 619 by (simp add: cvalidt_def validt_def cvalid_def) 620 thus ?thesis 621 by (rule hoare_complete) 622qed 623 624subsection \<open>Completeness\<close> 625 626lemma MGT_valid: 627"\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s} c 628 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 629proof (rule validtI) 630 fix s t 631 assume "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 632 "s \<in> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s}" 633 "t \<notin> Fault ` F" 634 thus "t \<in> Normal ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t} \<union> 635 Abrupt ` {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 636 apply (cases t) 637 apply (auto simp add: final_notin_def) 638 done 639next 640 fix s 641 assume "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c\<down>Normal s}" 642 thus "\<Gamma>\<turnstile>c\<down>Normal s" 643 by blast 644qed 645 646text \<open>The consequence rule where the existential @{term Z} is instantiated 647to @{term s}. Usefull in proof of \<open>MGT_lemma\<close>.\<close> 648lemma ConseqMGT: 649 assumes modif: "\<forall>Z::'a. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z::'a assn) c (Q' Z),(A' Z)" 650 assumes impl: "\<And>s. s \<in> P \<Longrightarrow> s \<in> P' s \<and> (\<forall>t. t \<in> Q' s \<longrightarrow> t \<in> Q) \<and> 651 (\<forall>t. t \<in> A' s \<longrightarrow> t \<in> A)" 652 shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 653using impl 654by - (rule conseq [OF modif],blast) 655 656lemma MGT_implies_complete: 657 assumes MGT: "\<forall>Z. \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 658 \<Gamma>\<turnstile>c\<down>Normal s} 659 c 660 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 661 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 662 assumes valid: "\<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 663 shows "\<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 664 using MGT 665 apply (rule ConseqMGT) 666 apply (insert valid) 667 apply (auto simp add: validt_def valid_def intro!: final_notinI) 668 done 669 670lemma conseq_extract_state_indep_prop: 671 assumes state_indep_prop:"\<forall>s \<in> P. R" 672 assumes to_show: "R \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 673 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 674 apply (rule Conseq) 675 apply (clarify) 676 apply (rule_tac x="P" in exI) 677 apply (rule_tac x="Q" in exI) 678 apply (rule_tac x="A" in exI) 679 using state_indep_prop to_show 680 by blast 681 682lemma MGT_lemma: 683 assumes MGT_Calls: 684 "\<forall>p \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 685 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 686 \<Gamma>\<turnstile>(Call p)\<down>Normal s} 687 (Call p) 688 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 689 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 690 shows "\<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 691 \<Gamma>\<turnstile>c\<down>Normal s} 692 c 693 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 694proof (induct c) 695 case Skip 696 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 697 \<Gamma>\<turnstile>Skip \<down> Normal s} 698 Skip 699 {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 700 by (rule hoaret.Skip [THEN conseqPre]) 701 (auto elim: exec_elim_cases simp add: final_notin_def 702 intro: exec.intros terminates.intros) 703next 704 case (Basic f) 705 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 706 \<Gamma>\<turnstile>Basic f \<down> Normal s} 707 Basic f 708 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t}, 709 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 710 by (rule hoaret.Basic [THEN conseqPre]) 711 (auto elim: exec_elim_cases simp add: final_notin_def 712 intro: exec.intros terminates.intros) 713next 714 case (Spec r) 715 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 716 \<Gamma>\<turnstile>Spec r \<down> Normal s} 717 Spec r 718 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t}, 719 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 720 apply (rule hoaret.Spec [THEN conseqPre]) 721 apply (clarsimp simp add: final_notin_def) 722 apply (case_tac "\<exists>t. (Z,t) \<in> r") 723 apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) 724 done 725next 726 case (Seq c1 c2) 727 have hyp_c1: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 728 \<Gamma>\<turnstile>c1\<down>Normal s} 729 c1 730 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 731 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 732 using Seq.hyps by iprover 733 have hyp_c2: "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 734 \<Gamma>\<turnstile>c2\<down>Normal s} 735 c2 736 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 737 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 738 using Seq.hyps by iprover 739 from hyp_c1 740 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 741 \<Gamma>\<turnstile>Seq c1 c2\<down>Normal s} c1 742 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 743 \<Gamma>\<turnstile>c2\<down>Normal t}, 744 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 745 by (rule ConseqMGT) 746 (auto dest: Seq_NoFaultStuckD1 [simplified] Seq_NoFaultStuckD2 [simplified] 747 elim: terminates_Normal_elim_cases 748 intro: exec.intros) 749 thus "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 750 \<Gamma>\<turnstile>Seq c1 c2\<down>Normal s} 751 Seq c1 c2 752 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 753 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 754 proof (rule hoaret.Seq ) 755 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> 756 \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>c2 \<down> Normal t} 757 c2 758 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 759 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 760 proof (rule ConseqMGT [OF hyp_c2],safe) 761 fix r t 762 assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Normal t" 763 then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t" 764 by (rule exec.intros) 765 next 766 fix r t 767 assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal r" "\<Gamma>\<turnstile>\<langle>c2,Normal r\<rangle> \<Rightarrow> Abrupt t" 768 then show "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 769 by (rule exec.intros) 770 qed 771 qed 772next 773 case (Cond b c1 c2) 774 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 775 \<Gamma>\<turnstile>c1\<down>Normal s} 776 c1 777 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 778 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 779 using Cond.hyps by iprover 780 hence "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 781 \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s}\<inter>b) 782 c1 783 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 784 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 785 by (rule ConseqMGT) 786 (fastforce simp add: final_notin_def intro: exec.CondTrue 787 elim: terminates_Normal_elim_cases) 788 moreover 789 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 790 \<Gamma>\<turnstile>c2\<down>Normal s} 791 c2 792 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 793 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 794 using Cond.hyps by iprover 795 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 796 \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s}\<inter>-b) 797 c2 798 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 799 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 800 by (rule ConseqMGT) 801 (fastforce simp add: final_notin_def intro: exec.CondFalse 802 elim: terminates_Normal_elim_cases) 803 ultimately 804 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 805 \<Gamma>\<turnstile>(Cond b c1 c2)\<down>Normal s} 806 (Cond b c1 c2) 807 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 808 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 809 by (rule hoaret.Cond) 810next 811 case (While b c) 812 let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*" 813 let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and> 814 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 815 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 816 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 817 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 818 \<Gamma>\<turnstile>(While b c)\<down>Normal t}" 819 let ?A = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 820 let ?r = "{(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and> 821 \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" 822 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 823 \<Gamma>\<turnstile>(While b c)\<down>Normal s} 824 (While b c) 825 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}, 826 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 827 proof (rule ConseqMGT [where ?P'="\<lambda> Z. ?P' Z" 828 and ?Q'="\<lambda> Z. ?P' Z \<inter> - b"]) 829 have wf_r: "wf ?r" by (rule wf_terminates_while) 830 show "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A Z)" 831 proof (rule allI, rule hoaret.While [OF wf_r]) 832 fix Z 833 from While 834 have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 835 \<Gamma>\<turnstile>c\<down>Normal s} 836 c 837 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 838 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover 839 show "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> ?P' Z \<inter> b) c 840 ({t. (t, \<sigma>) \<in> ?r} \<inter> ?P' Z),(?A Z)" 841 proof (rule allI, rule ConseqMGT [OF hyp_c]) 842 fix \<sigma> s 843 assume "s\<in> {\<sigma>} \<inter> 844 {t. (Z, t) \<in> ?unroll \<and> 845 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 846 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 847 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 848 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 849 \<Gamma>\<turnstile>(While b c)\<down>Normal t} 850 \<inter> b" 851 then obtain 852 s_eq_\<sigma>: "s=\<sigma>" and 853 Z_s_unroll: "(Z,s) \<in> ?unroll" and 854 noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 855 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 856 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 857 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and 858 while_term: "\<Gamma>\<turnstile>(While b c)\<down>Normal s" and 859 s_in_b: "s\<in>b" 860 by blast 861 show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 862 \<Gamma>\<turnstile>c\<down>Normal t} \<and> 863 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow> 864 t \<in> {t. (t,\<sigma>) \<in> ?r} \<inter> 865 {t. (Z, t) \<in> ?unroll \<and> 866 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 867 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 868 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 869 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 870 \<Gamma>\<turnstile>(While b c)\<down>Normal t}) \<and> 871 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow> 872 t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})" 873 (is "?C1 \<and> ?C2 \<and> ?C3") 874 proof (intro conjI) 875 from Z_s_unroll noabort s_in_b while_term show ?C1 876 by (blast elim: terminates_Normal_elim_cases) 877 next 878 { 879 fix t 880 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t" 881 with s_eq_\<sigma> while_term s_in_b have "(t,\<sigma>) \<in> ?r" 882 by blast 883 moreover 884 from Z_s_unroll s_t s_in_b 885 have "(Z, t) \<in> ?unroll" 886 by (blast intro: rtrancl_into_rtrancl) 887 moreover from while_term s_t s_in_b 888 have "\<Gamma>\<turnstile>(While b c)\<down>Normal t" 889 by (blast elim: terminates_Normal_elim_cases) 890 moreover note noabort 891 ultimately 892 have "(t,\<sigma>) \<in> ?r \<and> (Z, t) \<in> ?unroll \<and> 893 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 894 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 895 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 896 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 897 \<Gamma>\<turnstile>(While b c)\<down>Normal t" 898 by iprover 899 } 900 then show ?C2 by blast 901 next 902 { 903 fix t 904 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t" 905 from Z_s_unroll noabort s_t s_in_b 906 have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t" 907 by blast 908 } thus ?C3 by simp 909 qed 910 qed 911 qed 912 next 913 fix s 914 assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 915 \<Gamma>\<turnstile>While b c \<down> Normal s}" 916 hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 917 by auto 918 show "s \<in> ?P' s \<and> 919 (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow> 920 t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and> 921 (\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z)" 922 proof (intro conjI) 923 { 924 fix e 925 assume "(Z,e) \<in> ?unroll" "e \<in> b" 926 from this WhileNoFault 927 have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 928 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 929 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e") 930 proof (induct rule: converse_rtrancl_induct [consumes 1]) 931 assume e_in_b: "e \<in> b" 932 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 933 with e_in_b WhileNoFault 934 have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 935 by (auto simp add: final_notin_def intro: exec.intros) 936 moreover 937 { 938 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 939 with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u" 940 by (blast intro: exec.intros) 941 } 942 ultimately 943 show "?Prop e e" 944 by iprover 945 next 946 fix Z r 947 assume e_in_b: "e\<in>b" 948 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 949 assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk> 950 \<Longrightarrow> ?Prop r e" 951 assume Z_r: 952 "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}" 953 with WhileNoFault 954 have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 955 by (auto simp add: final_notin_def intro: exec.intros) 956 from hyp [OF e_in_b this] obtain 957 cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and 958 Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow> 959 \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" 960 by simp 961 962 { 963 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 964 with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp 965 moreover from Z_r obtain 966 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 967 by simp 968 ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u" 969 by (blast intro: exec.intros) 970 } 971 with cNoFault show "?Prop Z e" 972 by iprover 973 qed 974 } 975 with P show "s \<in> ?P' s" 976 by blast 977 next 978 { 979 fix t 980 assume "termination": "t \<notin> b" 981 assume "(Z, t) \<in> ?unroll" 982 hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 983 proof (induct rule: converse_rtrancl_induct [consumes 1]) 984 from "termination" 985 show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t" 986 by (blast intro: exec.WhileFalse) 987 next 988 fix Z r 989 assume first_body: 990 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" 991 assume "(r, t) \<in> ?unroll" 992 assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t" 993 show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 994 proof - 995 from first_body obtain 996 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 997 by fast 998 moreover 999 from rest_loop have 1000 "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t" 1001 by fast 1002 ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 1003 by (rule exec.WhileTrue) 1004 qed 1005 qed 1006 } 1007 with P 1008 show "(\<forall>t. t\<in>(?P' s \<inter> - b) 1009 \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})" 1010 by blast 1011 next 1012 from P show "\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z" 1013 by simp 1014 qed 1015 qed 1016next 1017 case (Call p) 1018 from noStuck_Call 1019 have "\<forall>s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1020 \<Gamma>\<turnstile>Call p\<down> Normal s}. 1021 p \<in> dom \<Gamma>" 1022 by (fastforce simp add: final_notin_def) 1023 then show ?case 1024 proof (rule conseq_extract_state_indep_prop) 1025 assume p_defined: "p \<in> dom \<Gamma>" 1026 with MGT_Calls show 1027 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> 1028 \<Gamma>\<turnstile>\<langle>Call p ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<and> 1029 \<Gamma>\<turnstile>Call p\<down>Normal s} 1030 (Call p) 1031 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 1032 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1033 by (auto) 1034 qed 1035next 1036 case (DynCom c) 1037 have hyp: 1038 "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1039 \<Gamma>\<turnstile>c s'\<down>Normal s} c s' 1040 {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1041 using DynCom by simp 1042 have hyp': 1043 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s = Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1044 \<Gamma>\<turnstile>DynCom c\<down>Normal s} 1045 (c Z) 1046 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1047 by (rule ConseqMGT [OF hyp]) 1048 (fastforce simp add: final_notin_def intro: exec.intros 1049 elim: terminates_Normal_elim_cases) 1050 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1051 \<Gamma>\<turnstile>DynCom c\<down>Normal s} 1052 DynCom c 1053 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1054 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1055 apply (rule hoaret.DynCom) 1056 apply (clarsimp) 1057 apply (rule hyp' [simplified]) 1058 done 1059next 1060 case (Guard f g c) 1061 have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1062 \<Gamma>\<turnstile>c\<down>Normal s} 1063 c 1064 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1065 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1066 using Guard by iprover 1067 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1068 \<Gamma>\<turnstile>Guard f g c\<down> Normal s} 1069 Guard f g c 1070 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, 1071 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1072 proof (cases "f \<in> F") 1073 case True 1074 from hyp_c 1075 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>(g \<inter> {s. s=Z \<and> 1076 \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck}\<union> Fault ` (-F))\<and> 1077 \<Gamma>\<turnstile>Guard f g c\<down> Normal s}) 1078 c 1079 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1080 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1081 apply (rule ConseqMGT) 1082 apply (insert True) 1083 apply (auto simp add: final_notin_def intro: exec.intros 1084 elim: terminates_Normal_elim_cases) 1085 done 1086 from True this 1087 show ?thesis 1088 by (rule conseqPre [OF Guarantee]) auto 1089 next 1090 case False 1091 from hyp_c 1092 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F \<^esub>(g \<inter> {s. s \<in> g \<and> s=Z \<and> 1093 \<Gamma>\<turnstile>\<langle>Guard f g c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck}\<union> Fault ` (-F))\<and> 1094 \<Gamma>\<turnstile>Guard f g c\<down> Normal s} ) 1095 c 1096 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1097 {t. \<Gamma>\<turnstile>\<langle>Guard f g c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1098 apply (rule ConseqMGT) 1099 apply clarify 1100 apply (frule Guard_noFaultStuckD [OF _ False]) 1101 apply (auto simp add: final_notin_def intro: exec.intros 1102 elim: terminates_Normal_elim_cases) 1103 done 1104 then show ?thesis 1105 apply (rule conseqPre [OF hoaret.Guard]) 1106 apply clarify 1107 apply (frule Guard_noFaultStuckD [OF _ False]) 1108 apply auto 1109 done 1110 qed 1111next 1112 case Throw 1113 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1114 \<Gamma>\<turnstile>Throw \<down> Normal s} 1115 Throw 1116 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t}, 1117 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1118 by (rule conseqPre [OF hoaret.Throw]) 1119 (blast intro: exec.intros terminates.intros) 1120next 1121 case (Catch c\<^sub>1 c\<^sub>2) 1122 have "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1123 \<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s} 1124 c\<^sub>1 1125 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t}, 1126 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1127 using Catch.hyps by iprover 1128 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and> 1129 \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s} 1130 c\<^sub>1 1131 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1132 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal t \<and> 1133 \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))}" 1134 by (rule ConseqMGT) 1135 (fastforce intro: exec.intros terminates.intros 1136 elim: terminates_Normal_elim_cases 1137 simp add: final_notin_def) 1138 moreover 1139 have 1140 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1141 \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s} c\<^sub>2 1142 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1143 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1144 using Catch.hyps by iprover 1145 hence "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>Abrupt s \<and> \<Gamma>\<turnstile>c\<^sub>2 \<down> Normal s \<and> 1146 \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))} 1147 c\<^sub>2 1148 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1149 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1150 by (rule ConseqMGT) 1151 (fastforce intro: exec.intros terminates.intros 1152 simp add: noFault_def') 1153 ultimately 1154 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and> 1155 \<Gamma>\<turnstile>Catch c\<^sub>1 c\<^sub>2 \<down> Normal s} 1156 Catch c\<^sub>1 c\<^sub>2 1157 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1158 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1159 by (rule hoaret.Catch ) 1160qed 1161 1162 1163lemma Call_lemma': 1164 assumes Call_hyp: 1165 "\<forall>q\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1166 \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>} 1167 (Call q) 1168 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, 1169 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1170 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 1171 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1172 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')} 1173 c 1174 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1175 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1176proof (induct c) 1177 case Skip 1178 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Skip,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1179 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1180 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Skip \<in> redexes c')} 1181 Skip 1182 {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Normal t}, 1183 {t. \<Gamma>\<turnstile>\<langle>Skip,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1184 by (rule hoaret.Skip [THEN conseqPre]) (blast intro: exec.Skip) 1185next 1186 case (Basic f) 1187 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Basic f,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1188 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1189 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1190 Basic f \<in> redexes c')} 1191 Basic f 1192 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Normal t}, 1193 {t. \<Gamma>\<turnstile>\<langle>Basic f,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1194 by (rule hoaret.Basic [THEN conseqPre]) (blast intro: exec.Basic) 1195next 1196 case (Spec r) 1197 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Spec r,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1198 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1199 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1200 Spec r \<in> redexes c')} 1201 Spec r 1202 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Normal t}, 1203 {t. \<Gamma>\<turnstile>\<langle>Spec r,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1204 apply (rule hoaret.Spec [THEN conseqPre]) 1205 apply (clarsimp) 1206 apply (case_tac "\<exists>t. (Z,t) \<in> r") 1207 apply (auto elim: exec_elim_cases simp add: final_notin_def intro: exec.intros) 1208 done 1209next 1210 case (Seq c1 c2) 1211 have hyp_c1: 1212 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1213 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1214 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c1 \<in> redexes c')} 1215 c1 1216 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 1217 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1218 using Seq.hyps by iprover 1219 have hyp_c2: 1220 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1221 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1222 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c2 \<in> redexes c')} 1223 c2 1224 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1225 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1226 using Seq.hyps (2) by iprover 1227 have c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1228 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1229 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1230 Seq c1 c2 \<in> redexes c')} 1231 c1 1232 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t \<and> 1233 \<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1234 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1235 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> 1236 c2 \<in> redexes c')}, 1237 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1238 proof (rule ConseqMGT [OF hyp_c1],clarify,safe) 1239 assume "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1240 thus "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1241 by (blast dest: Seq_NoFaultStuckD1) 1242 next 1243 fix c' 1244 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1245 assume red: "Seq c1 c2 \<in> redexes c'" 1246 from redexes_subset [OF red] steps_c' 1247 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c1 \<in> redexes c'" 1248 by (auto iff: root_in_redexes) 1249 next 1250 fix t 1251 assume "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1252 "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t" 1253 thus "\<Gamma>\<turnstile>\<langle>c2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1254 by (blast dest: Seq_NoFaultStuckD2) 1255 next 1256 fix c' t 1257 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1258 assume red: "Seq c1 c2 \<in> redexes c'" 1259 assume exec_c1: "\<Gamma>\<turnstile> \<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t" 1260 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> c2 \<in> redexes c'" 1261 proof - 1262 note steps_c' 1263 also 1264 from exec_impl_steps_Normal [OF exec_c1] 1265 have "\<Gamma>\<turnstile> (c1, Normal Z) \<rightarrow>\<^sup>* (Skip, Normal t)". 1266 from steps_redexes_Seq [OF this red] 1267 obtain c'' where 1268 steps_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow>\<^sup>* (c'', Normal t)" and 1269 Skip: "Seq Skip c2 \<in> redexes c''" 1270 by blast 1271 note steps_c'' 1272 also 1273 have step_Skip: "\<Gamma>\<turnstile> (Seq Skip c2,Normal t) \<rightarrow> (c2,Normal t)" 1274 by (rule step.SeqSkip) 1275 from step_redexes [OF step_Skip Skip] 1276 obtain c''' where 1277 step_c''': "\<Gamma>\<turnstile> (c'', Normal t) \<rightarrow> (c''', Normal t)" and 1278 c2: "c2 \<in> redexes c'''" 1279 by blast 1280 note step_c''' 1281 finally show ?thesis 1282 using c2 1283 by blast 1284 qed 1285 next 1286 fix t 1287 assume "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1288 thus "\<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1289 by (blast intro: exec.intros) 1290 qed 1291 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1292 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1293 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Seq c1 c2 \<in> redexes c')} 1294 Seq c1 c2 1295 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1296 {t. \<Gamma>\<turnstile>\<langle>Seq c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1297 by (rule hoaret.Seq [OF c1 ConseqMGT [OF hyp_c2]]) 1298 (blast intro: exec.intros) 1299next 1300 case (Cond b c1 c2) 1301 have hyp_c1: 1302 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1303 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1304 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c1 \<in> redexes c')} 1305 c1 1306 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t}, 1307 {t. \<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1308 using Cond.hyps by iprover 1309 have 1310 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1311 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1312 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1313 Cond b c1 c2 \<in> redexes c')} 1314 \<inter> b) 1315 c1 1316 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1317 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1318 proof (rule ConseqMGT [OF hyp_c1],safe) 1319 assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1320 thus "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1321 by (auto simp add: final_notin_def intro: exec.CondTrue) 1322 next 1323 fix c' 1324 assume b: "Z \<in> b" 1325 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1326 assume redex_c': "Cond b c1 c2 \<in> redexes c'" 1327 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c1 \<in> redexes c'" 1328 proof - 1329 note steps_c' 1330 also 1331 from b 1332 have "\<Gamma>\<turnstile>(Cond b c1 c2, Normal Z) \<rightarrow> (c1, Normal Z)" 1333 by (rule step.CondTrue) 1334 from step_redexes [OF this redex_c'] obtain c'' where 1335 step_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and 1336 c1: "c1 \<in> redexes c''" 1337 by blast 1338 note step_c'' 1339 finally show ?thesis 1340 using c1 1341 by blast 1342 qed 1343 next 1344 fix t assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Normal t" 1345 thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t" 1346 by (blast intro: exec.CondTrue) 1347 next 1348 fix t assume "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c1,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1349 thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1350 by (blast intro: exec.CondTrue) 1351 qed 1352 moreover 1353 have hyp_c2: 1354 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1355 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1356 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c2 \<in> redexes c')} 1357 c2 1358 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1359 {t. \<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1360 using Cond.hyps by iprover 1361 have 1362 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1363 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1364 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal s) \<and> 1365 Cond b c1 c2 \<in> redexes c')} 1366 \<inter> -b) 1367 c2 1368 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1369 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1370 proof (rule ConseqMGT [OF hyp_c2],safe) 1371 assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1372 thus "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1373 by (auto simp add: final_notin_def intro: exec.CondFalse) 1374 next 1375 fix c' 1376 assume b: "Z \<notin> b" 1377 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1378 assume redex_c': "Cond b c1 c2 \<in> redexes c'" 1379 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c2 \<in> redexes c'" 1380 proof - 1381 note steps_c' 1382 also 1383 from b 1384 have "\<Gamma>\<turnstile>(Cond b c1 c2, Normal Z) \<rightarrow> (c2, Normal Z)" 1385 by (rule step.CondFalse) 1386 from step_redexes [OF this redex_c'] obtain c'' where 1387 step_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and 1388 c1: "c2 \<in> redexes c''" 1389 by blast 1390 note step_c'' 1391 finally show ?thesis 1392 using c1 1393 by blast 1394 qed 1395 next 1396 fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Normal t" 1397 thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t" 1398 by (blast intro: exec.CondFalse) 1399 next 1400 fix t assume "Z \<notin> b" "\<Gamma>\<turnstile>\<langle>c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1401 thus "\<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1402 by (blast intro: exec.CondFalse) 1403 qed 1404 ultimately 1405 show 1406 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1407 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1408 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1409 Cond b c1 c2 \<in> redexes c')} 1410 (Cond b c1 c2) 1411 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1412 {t. \<Gamma>\<turnstile>\<langle>Cond b c1 c2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1413 by (rule hoaret.Cond) 1414next 1415 case (While b c) 1416 let ?unroll = "({(s,t). s\<in>b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t})\<^sup>*" 1417 let ?P' = "\<lambda>Z. {t. (Z,t)\<in>?unroll \<and> 1418 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 1419 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1420 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1421 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 1422 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1423 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ 1424 (c',Normal t) \<and> While b c \<in> redexes c')}" 1425 let ?A = "\<lambda>Z. {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1426 let ?r = "{(t,s). \<Gamma>\<turnstile>(While b c)\<down>Normal s \<and> s\<in>b \<and> 1427 \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" 1428 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> 1429 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1430 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1431 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and> While b c \<in> redexes c')} 1432 (While b c) 1433 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1434 {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1435 proof (rule ConseqMGT [where ?P'="\<lambda> Z. ?P' Z" 1436 and ?Q'="\<lambda> Z. ?P' Z \<inter> - b"]) 1437 have wf_r: "wf ?r" by (rule wf_terminates_while) 1438 show "\<forall> Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) (While b c) (?P' Z \<inter> - b),(?A Z)" 1439 proof (rule allI, rule hoaret.While [OF wf_r]) 1440 fix Z 1441 from While 1442 have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> 1443 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1444 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1445 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')} 1446 c 1447 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1448 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" by iprover 1449 show "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> ?P' Z \<inter> b) c 1450 ({t. (t, \<sigma>) \<in> ?r} \<inter> ?P' Z),(?A Z)" 1451 proof (rule allI, rule ConseqMGT [OF hyp_c]) 1452 fix \<tau> s 1453 assume asm: "s\<in> {\<tau>} \<inter> 1454 {t. (Z, t) \<in> ?unroll \<and> 1455 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 1456 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1457 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1458 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 1459 \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> 1460 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ 1461 (c',Normal t) \<and> While b c \<in> redexes c')} 1462 \<inter> b" 1463 then obtain c' where 1464 s_eq_\<tau>: "s=\<tau>" and 1465 Z_s_unroll: "(Z,s) \<in> ?unroll" and 1466 noabort:"\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 1467 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1468 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1469 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" and 1470 termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" and 1471 reach: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s)" and 1472 red_c': "While b c \<in> redexes c'" and 1473 s_in_b: "s\<in>b" 1474 by blast 1475 obtain c'' where 1476 reach_c: "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal s)" 1477 "Seq c (While b c) \<in> redexes c''" 1478 proof - 1479 note reach 1480 also from s_in_b 1481 have "\<Gamma>\<turnstile>(While b c,Normal s) \<rightarrow> (Seq c (While b c),Normal s)" 1482 by (rule step.WhileTrue) 1483 from step_redexes [OF this red_c'] obtain c'' where 1484 step: "\<Gamma>\<turnstile> (c', Normal s) \<rightarrow> (c'', Normal s)" and 1485 red_c'': "Seq c (While b c) \<in> redexes c''" 1486 by blast 1487 note step 1488 finally 1489 show ?thesis 1490 using red_c'' 1491 by (blast intro: that) 1492 qed 1493 from reach termi 1494 have "\<Gamma>\<turnstile>c' \<down> Normal s" 1495 by (rule steps_preserves_termination') 1496 from redexes_preserves_termination [OF this red_c'] 1497 have termi_while: "\<Gamma>\<turnstile>While b c \<down> Normal s" . 1498 show "s \<in> {t. t = s \<and> \<Gamma>\<turnstile>\<langle>c,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1499 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1500 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c \<in> redexes c')} \<and> 1501 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t} \<longrightarrow> 1502 t \<in> {t. (t,\<tau>) \<in> ?r} \<inter> 1503 {t. (Z, t) \<in> ?unroll \<and> 1504 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 1505 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1506 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1507 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 1508 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1509 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> 1510 While b c \<in> redexes c')}) \<and> 1511 (\<forall>t. t \<in> {t. \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t} \<longrightarrow> 1512 t \<in> {t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t})" 1513 (is "?C1 \<and> ?C2 \<and> ?C3") 1514 proof (intro conjI) 1515 from Z_s_unroll noabort s_in_b termi reach_c show ?C1 1516 apply clarsimp 1517 apply (drule redexes_subset) 1518 apply simp 1519 apply (blast intro: root_in_redexes) 1520 done 1521 next 1522 { 1523 fix t 1524 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t" 1525 with s_eq_\<tau> termi_while s_in_b have "(t,\<tau>) \<in> ?r" 1526 by blast 1527 moreover 1528 from Z_s_unroll s_t s_in_b 1529 have "(Z, t) \<in> ?unroll" 1530 by (blast intro: rtrancl_into_rtrancl) 1531 moreover 1532 obtain c'' where 1533 reach_c'': "\<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c'',Normal t)" 1534 "(While b c) \<in> redexes c''" 1535 proof - 1536 note reach_c (1) 1537 also from s_in_b 1538 have "\<Gamma>\<turnstile>(While b c,Normal s)\<rightarrow> (Seq c (While b c),Normal s)" 1539 by (rule step.WhileTrue) 1540 have "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>+ 1541 (While b c, Normal t)" 1542 proof - 1543 from exec_impl_steps_Normal [OF s_t] 1544 have "\<Gamma>\<turnstile> (c, Normal s) \<rightarrow>\<^sup>* (Skip, Normal t)". 1545 hence "\<Gamma>\<turnstile> (Seq c (While b c), Normal s) \<rightarrow>\<^sup>* 1546 (Seq Skip (While b c), Normal t)" 1547 by (rule SeqSteps) auto 1548 moreover 1549 have "\<Gamma>\<turnstile>(Seq Skip (While b c), Normal t)\<rightarrow>(While b c, Normal t)" 1550 by (rule step.SeqSkip) 1551 ultimately show ?thesis by (rule rtranclp_into_tranclp1) 1552 qed 1553 from steps_redexes' [OF this reach_c (2)] 1554 obtain c''' where 1555 step: "\<Gamma>\<turnstile> (c'', Normal s) \<rightarrow>\<^sup>+ (c''', Normal t)" and 1556 red_c'': "While b c \<in> redexes c'''" 1557 by blast 1558 note step 1559 finally 1560 show ?thesis 1561 using red_c'' 1562 by (blast intro: that) 1563 qed 1564 moreover note noabort termi 1565 ultimately 1566 have "(t,\<tau>) \<in> ?r \<and> (Z, t) \<in> ?unroll \<and> 1567 (\<forall>e. (Z,e)\<in>?unroll \<longrightarrow> e\<in>b 1568 \<longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1569 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1570 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)) \<and> 1571 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1572 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> 1573 While b c \<in> redexes c')" 1574 by iprover 1575 } 1576 then show ?C2 by blast 1577 next 1578 { 1579 fix t 1580 assume s_t: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t" 1581 from Z_s_unroll noabort s_t s_in_b 1582 have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1583 by blast 1584 } thus ?C3 by simp 1585 qed 1586 qed 1587 qed 1588 next 1589 fix s 1590 assume P: "s \<in> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>While b c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1591 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1592 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1593 While b c \<in> redexes c')}" 1594 hence WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1595 by auto 1596 show "s \<in> ?P' s \<and> 1597 (\<forall>t. t\<in>(?P' s \<inter> - b)\<longrightarrow> 1598 t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t})\<and> 1599 (\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z)" 1600 proof (intro conjI) 1601 { 1602 fix e 1603 assume "(Z,e) \<in> ?unroll" "e \<in> b" 1604 from this WhileNoFault 1605 have "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1606 (\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>Abrupt u \<longrightarrow> 1607 \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u)" (is "?Prop Z e") 1608 proof (induct rule: converse_rtrancl_induct [consumes 1]) 1609 assume e_in_b: "e \<in> b" 1610 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1611 with e_in_b WhileNoFault 1612 have cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1613 by (auto simp add: final_notin_def intro: exec.intros) 1614 moreover 1615 { 1616 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 1617 with e_in_b have "\<Gamma>\<turnstile>\<langle>While b c,Normal e\<rangle> \<Rightarrow> Abrupt u" 1618 by (blast intro: exec.intros) 1619 } 1620 ultimately 1621 show "?Prop e e" 1622 by iprover 1623 next 1624 fix Z r 1625 assume e_in_b: "e\<in>b" 1626 assume WhileNoFault: "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1627 assume hyp: "\<lbrakk>e\<in>b;\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))\<rbrakk> 1628 \<Longrightarrow> ?Prop r e" 1629 assume Z_r: 1630 "(Z, r) \<in> {(Z, r). Z \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r}" 1631 with WhileNoFault 1632 have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1633 by (auto simp add: final_notin_def intro: exec.intros) 1634 from hyp [OF e_in_b this] obtain 1635 cNoFault: "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" and 1636 Abrupt_r: "\<forall>u. \<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u \<longrightarrow> 1637 \<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" 1638 by simp 1639 1640 { 1641 fix u assume "\<Gamma>\<turnstile>\<langle>c,Normal e\<rangle> \<Rightarrow> Abrupt u" 1642 with Abrupt_r have "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Abrupt u" by simp 1643 moreover from Z_r obtain 1644 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 1645 by simp 1646 ultimately have "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Abrupt u" 1647 by (blast intro: exec.intros) 1648 } 1649 with cNoFault show "?Prop Z e" 1650 by iprover 1651 qed 1652 } 1653 with P show "s \<in> ?P' s" 1654 by blast 1655 next 1656 { 1657 fix t 1658 assume "termination": "t \<notin> b" 1659 assume "(Z, t) \<in> ?unroll" 1660 hence "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 1661 proof (induct rule: converse_rtrancl_induct [consumes 1]) 1662 from "termination" 1663 show "\<Gamma>\<turnstile>\<langle>While b c,Normal t\<rangle> \<Rightarrow> Normal t" 1664 by (blast intro: exec.WhileFalse) 1665 next 1666 fix Z r 1667 assume first_body: 1668 "(Z, r) \<in> {(s, t). s \<in> b \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> Normal t}" 1669 assume "(r, t) \<in> ?unroll" 1670 assume rest_loop: "\<Gamma>\<turnstile>\<langle>While b c, Normal r\<rangle> \<Rightarrow> Normal t" 1671 show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 1672 proof - 1673 from first_body obtain 1674 "Z \<in> b" "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal r" 1675 by fast 1676 moreover 1677 from rest_loop have 1678 "\<Gamma>\<turnstile>\<langle>While b c,Normal r\<rangle> \<Rightarrow> Normal t" 1679 by fast 1680 ultimately show "\<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t" 1681 by (rule exec.WhileTrue) 1682 qed 1683 qed 1684 } 1685 with P 1686 show "\<forall>t. t\<in>(?P' s \<inter> - b) 1687 \<longrightarrow>t\<in>{t. \<Gamma>\<turnstile>\<langle>While b c,Normal Z\<rangle> \<Rightarrow> Normal t}" 1688 by blast 1689 next 1690 from P show "\<forall>t. t\<in>?A s \<longrightarrow> t\<in>?A Z" 1691 by simp 1692 qed 1693 qed 1694next 1695 case (Call q) 1696 let ?P = "{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1697 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1698 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Call q \<in> redexes c')}" 1699 from noStuck_Call 1700 have "\<forall>s \<in> ?P. q \<in> dom \<Gamma>" 1701 by (fastforce simp add: final_notin_def) 1702 then show ?case 1703 proof (rule conseq_extract_state_indep_prop) 1704 assume q_defined: "q \<in> dom \<Gamma>" 1705 from Call_hyp have 1706 "\<forall>q\<in>dom \<Gamma>. \<forall>Z. 1707 \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub>{s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1708 \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>} 1709 (Call q) 1710 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, 1711 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1712 by (simp add: exec_Call_body' noFaultStuck_Call_body' [simplified] 1713 terminates_Normal_Call_body) 1714 from Call_hyp q_defined have Call_hyp': 1715 "\<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1716 \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>} 1717 (Call q) 1718 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, 1719 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1720 by auto 1721 show 1722 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ?P 1723 (Call q) 1724 {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Normal t}, 1725 {t. \<Gamma>\<turnstile>\<langle>Call q ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1726 proof (rule ConseqMGT [OF Call_hyp'],safe) 1727 fix c' 1728 assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" 1729 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1730 assume red_c': "Call q \<in> redexes c'" 1731 show "\<Gamma>\<turnstile>Call q \<down> Normal Z" 1732 proof - 1733 from steps_preserves_termination' [OF steps_c' termi] 1734 have "\<Gamma>\<turnstile>c' \<down> Normal Z" . 1735 from redexes_preserves_termination [OF this red_c'] 1736 show ?thesis . 1737 qed 1738 next 1739 fix c' 1740 assume termi: "\<Gamma>\<turnstile>Call p \<down> Normal \<sigma>" 1741 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1742 assume red_c': "Call q \<in> redexes c'" 1743 from redex_redexes [OF this] 1744 have "redex c' = Call q" 1745 by auto 1746 with termi steps_c' 1747 show "((Z, q), \<sigma>, p) \<in> termi_call_steps \<Gamma>" 1748 by (auto simp add: termi_call_steps_def) 1749 qed 1750 qed 1751next 1752 case (DynCom c) 1753 have hyp: 1754 "\<And>s'. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> 1755 {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>c s',Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1756 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1757 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c s' \<in> redexes c')} 1758 (c s') 1759 {t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c s',Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1760 using DynCom by simp 1761 have hyp': 1762 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>DynCom c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1763 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1764 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> DynCom c \<in> redexes c')} 1765 (c Z) 1766 {t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1767 proof (rule ConseqMGT [OF hyp],safe) 1768 assume "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1769 then show "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1770 by (fastforce simp add: final_notin_def intro: exec.intros) 1771 next 1772 fix c' 1773 assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1774 assume c': "DynCom c \<in> redexes c'" 1775 have "\<Gamma>\<turnstile> (DynCom c, Normal Z) \<rightarrow> (c Z,Normal Z)" 1776 by (rule step.DynCom) 1777 from step_redexes [OF this c'] obtain c'' where 1778 step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c Z \<in> redexes c''" 1779 by blast 1780 note steps also note step 1781 finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c Z \<in> redexes c'" 1782 using c'' by blast 1783 next 1784 fix t 1785 assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Normal t" 1786 thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Normal t" 1787 by (auto intro: exec.intros) 1788 next 1789 fix t 1790 assume "\<Gamma>\<turnstile>\<langle>c Z,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1791 thus "\<Gamma>\<turnstile>\<langle>DynCom c,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1792 by (auto intro: exec.intros) 1793 qed 1794 show ?case 1795 apply (rule hoaret.DynCom) 1796 apply safe 1797 apply (rule hyp') 1798 done 1799next 1800 case (Guard f g c) 1801 have hyp_c: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> 1802 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1803 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1804 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c \<in> redexes c')} 1805 c 1806 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t}, 1807 {t. \<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1808 using Guard.hyps by iprover 1809 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1810 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1811 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Guard f g c \<in> redexes c')} 1812 Guard f g c 1813 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, 1814 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1815 proof (cases "f \<in> F") 1816 case True 1817 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and> 1818 \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1819 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1820 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1821 Guard f g c \<in> redexes c')}) 1822 c 1823 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, 1824 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1825 proof (rule ConseqMGT [OF hyp_c], safe) 1826 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" "Z\<in>g" 1827 thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1828 by (auto simp add: final_notin_def intro: exec.intros) 1829 next 1830 fix c' 1831 assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1832 assume c': "Guard f g c \<in> redexes c'" 1833 assume "Z \<in> g" 1834 from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)" 1835 by (rule step.Guard) 1836 from step_redexes [OF this c'] obtain c'' where 1837 step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c \<in> redexes c''" 1838 by blast 1839 note steps also note step 1840 finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c \<in> redexes c'" 1841 using c'' by blast 1842 next 1843 fix t 1844 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1845 "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t" "Z \<in> g" 1846 thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t" 1847 by (auto simp add: final_notin_def intro: exec.intros ) 1848 next 1849 fix t 1850 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1851 "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t" "Z \<in> g" 1852 thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1853 by (auto simp add: final_notin_def intro: exec.intros ) 1854 qed 1855 from True this show ?thesis 1856 by (rule conseqPre [OF Guarantee]) auto 1857 next 1858 case False 1859 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> {s. s=Z \<and> 1860 \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1861 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1862 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1863 Guard f g c \<in> redexes c')}) 1864 c 1865 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t}, 1866 {t. \<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1867 proof (rule ConseqMGT [OF hyp_c], safe) 1868 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1869 thus "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1870 using False 1871 by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros) 1872 next 1873 fix c' 1874 assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1875 assume c': "Guard f g c \<in> redexes c'" 1876 1877 assume "Z \<in> g" 1878 from this have "\<Gamma>\<turnstile>(Guard f g c,Normal Z) \<rightarrow> (c,Normal Z)" 1879 by (rule step.Guard) 1880 from step_redexes [OF this c'] obtain c'' where 1881 step: "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow> (c'', Normal Z)" and c'': "c \<in> redexes c''" 1882 by blast 1883 note steps also note step 1884 finally show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c \<in> redexes c'" 1885 using c'' by blast 1886 next 1887 fix t 1888 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1889 "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Normal t" 1890 thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Normal t" 1891 using False 1892 by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros ) 1893 next 1894 fix t 1895 assume "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1896 "\<Gamma>\<turnstile>\<langle>c,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1897 thus "\<Gamma>\<turnstile>\<langle>Guard f g c ,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1898 using False 1899 by (cases "Z\<in> g") (auto simp add: final_notin_def intro: exec.intros ) 1900 qed 1901 then show ?thesis 1902 apply (rule conseqPre [OF hoaret.Guard]) 1903 apply clarify 1904 apply (frule Guard_noFaultStuckD [OF _ False]) 1905 apply auto 1906 done 1907 qed 1908next 1909 case Throw 1910 show "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1911 \<Gamma>\<turnstile>Call p\<down>Normal \<sigma> \<and> 1912 (\<exists>c'. \<Gamma>\<turnstile>(Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> Throw \<in> redexes c')} 1913 Throw 1914 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Normal t}, 1915 {t. \<Gamma>\<turnstile>\<langle>Throw,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1916 by (rule conseqPre [OF hoaret.Throw]) 1917 (blast intro: exec.intros terminates.intros) 1918next 1919 case (Catch c\<^sub>1 c\<^sub>2) 1920 have hyp_c1: 1921 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1922 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1923 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> 1924 c\<^sub>1 \<in> redexes c')} 1925 c\<^sub>1 1926 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1927 using Catch.hyps by iprover 1928 have hyp_c2: 1929 "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s= Z \<and> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 1930 \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> 1931 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal s) \<and> c\<^sub>2 \<in> redexes c')} 1932 c\<^sub>2 1933 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 1934 using Catch.hyps by iprover 1935 have 1936 "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^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)) \<and> 1937 \<Gamma>\<turnstile>Call p\<down> Normal \<sigma> \<and> 1938 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>)\<rightarrow>\<^sup>+(c',Normal s) \<and> 1939 Catch c\<^sub>1 c\<^sub>2 \<in> redexes c')} 1940 c\<^sub>1 1941 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 1942 {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> 1943 \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault`(-F)) \<and> \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 1944 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c\<^sub>2 \<in> redexes c')}" 1945 proof (rule ConseqMGT [OF hyp_c1],clarify,safe) 1946 assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1947 thus "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1948 by (fastforce simp add: final_notin_def intro: exec.intros) 1949 next 1950 fix c' 1951 assume steps: "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1952 assume c': "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'" 1953 from steps redexes_subset [OF this] 1954 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z) \<and> c\<^sub>1 \<in> redexes c'" 1955 by (auto iff: root_in_redexes) 1956 next 1957 fix t 1958 assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Normal t" 1959 thus "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t" 1960 by (auto intro: exec.intros) 1961 next 1962 fix t 1963 assume "\<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1964 "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1965 thus "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F))" 1966 by (auto simp add: final_notin_def intro: exec.intros) 1967 next 1968 fix c' t 1969 assume steps_c': "\<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal Z)" 1970 assume red: "Catch c\<^sub>1 c\<^sub>2 \<in> redexes c'" 1971 assume exec_c\<^sub>1: "\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t" 1972 show "\<exists>c'. \<Gamma>\<turnstile> (Call p, Normal \<sigma>) \<rightarrow>\<^sup>+ (c', Normal t) \<and> c\<^sub>2 \<in> redexes c'" 1973 proof - 1974 note steps_c' 1975 also 1976 from exec_impl_steps_Normal_Abrupt [OF exec_c\<^sub>1] 1977 have "\<Gamma>\<turnstile> (c\<^sub>1, Normal Z) \<rightarrow>\<^sup>* (Throw, Normal t)". 1978 from steps_redexes_Catch [OF this red] 1979 obtain c'' where 1980 steps_c'': "\<Gamma>\<turnstile> (c', Normal Z) \<rightarrow>\<^sup>* (c'', Normal t)" and 1981 Catch: "Catch Throw c\<^sub>2 \<in> redexes c''" 1982 by blast 1983 note steps_c'' 1984 also 1985 have step_Catch: "\<Gamma>\<turnstile> (Catch Throw c\<^sub>2,Normal t) \<rightarrow> (c\<^sub>2,Normal t)" 1986 by (rule step.CatchThrow) 1987 from step_redexes [OF step_Catch Catch] 1988 obtain c''' where 1989 step_c''': "\<Gamma>\<turnstile> (c'', Normal t) \<rightarrow> (c''', Normal t)" and 1990 c2: "c\<^sub>2 \<in> redexes c'''" 1991 by blast 1992 note step_c''' 1993 finally show ?thesis 1994 using c2 1995 by blast 1996 qed 1997 qed 1998 moreover 1999 have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {t. \<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal Z\<rangle> \<Rightarrow> Abrupt t \<and> 2000 \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal t\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2001 \<Gamma>\<turnstile>Call p \<down> Normal \<sigma> \<and> 2002 (\<exists>c'. \<Gamma>\<turnstile>(Call p,Normal \<sigma>) \<rightarrow>\<^sup>+ (c',Normal t) \<and> c\<^sub>2 \<in> redexes c')} 2003 c\<^sub>2 2004 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Normal t}, 2005 {t. \<Gamma>\<turnstile>\<langle>Catch c\<^sub>1 c\<^sub>2,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2006 by (rule ConseqMGT [OF hyp_c2]) (fastforce intro: exec.intros) 2007 ultimately show ?case 2008 by (rule hoaret.Catch) 2009qed 2010 2011 2012text \<open>To prove a procedure implementation correct it suffices to assume 2013 only the procedure specifications of procedures that actually 2014 occur during evaluation of the body. 2015\<close> 2016 2017lemma Call_lemma: 2018 assumes A: 2019 "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 2020 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2021 \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>} 2022 (Call q) 2023 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, 2024 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2025 assumes pdef: "p \<in> dom \<Gamma>" 2026 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 2027 ({\<sigma>} \<inter> {s. s=Z \<and>\<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2028 \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s}) 2029 the (\<Gamma> p) 2030 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t}, 2031 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2032apply (rule conseqPre) 2033apply (rule Call_lemma' [OF A]) 2034using pdef 2035apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF step.Call] root_in_redexes) 2036done 2037 2038lemma Call_lemma_switch_Call_body: 2039 assumes 2040 call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 2041 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2042 \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>} 2043 (Call q) 2044 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, 2045 {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2046 assumes p_defined: "p \<in> dom \<Gamma>" 2047 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> 2048 ({\<sigma>} \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2049 \<Gamma>\<turnstile>Call p\<down>Normal s}) 2050 the (\<Gamma> p) 2051 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2052 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2053apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined]) 2054apply (rule conseqPre) 2055apply (rule Call_lemma') 2056apply (rule call) 2057using p_defined 2058apply (fastforce intro: terminates.intros tranclp.r_into_trancl [of "(step \<Gamma>)", OF step.Call] 2059root_in_redexes) 2060done 2061 2062lemma MGT_Call: 2063"\<forall>p \<in> dom \<Gamma>. \<forall>Z. 2064 \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2065 \<Gamma>\<turnstile>(Call p)\<down>Normal s} 2066 (Call p) 2067 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2068 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2069apply (intro ballI allI) 2070apply (rule CallRec' [where Procs="dom \<Gamma>" and 2071 P="\<lambda>p Z. {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2072 \<Gamma>\<turnstile>Call p\<down>Normal s}" and 2073 Q="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" and 2074 A="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" and 2075 r="termi_call_steps \<Gamma>" 2076 ]) 2077apply simp 2078apply simp 2079apply (rule wf_termi_call_steps) 2080apply (intro ballI allI) 2081apply simp 2082apply (rule Call_lemma_switch_Call_body [rule_format, simplified]) 2083apply (rule hoaret.Asm) 2084apply fastforce 2085apply assumption 2086done 2087 2088 2089lemma CollInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}" 2090 by auto 2091 2092lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) = (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {f (x p Z)})" 2093 by (auto iff: not_None_eq) 2094 2095 2096text \<open>Another proof of \<open>MGT_Call\<close>, maybe a little more readable\<close> 2097lemma 2098"\<forall>p \<in> dom \<Gamma>. \<forall>Z. 2099 \<Gamma>,{} \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2100 \<Gamma>\<turnstile>(Call p)\<down>Normal s} 2101 (Call p) 2102 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2103 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2104proof - 2105 { 2106 fix p Z \<sigma> 2107 assume defined: "p \<in> dom \<Gamma>" 2108 define Specs where "Specs = (\<Union>p\<in>dom \<Gamma>. \<Union>Z. 2109 {({s. s=Z \<and> 2110 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2111 \<Gamma>\<turnstile>Call p\<down>Normal s}, 2112 p, 2113 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2114 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})" 2115 define Specs_wf where "Specs_wf p \<sigma> = (\<lambda>(P,q,Q,A). 2116 (P \<inter> {s. ((s,q),\<sigma>,p) \<in> termi_call_steps \<Gamma>}, q, Q, A)) ` Specs" for p \<sigma> 2117 have "\<Gamma>,Specs_wf p \<sigma> 2118 \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter> 2119 {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2120 \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s}) 2121 (the (\<Gamma> p)) 2122 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t}, 2123 {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2124 apply (rule Call_lemma [rule_format, OF _ defined]) 2125 apply (rule hoaret.Asm) 2126 apply (clarsimp simp add: Specs_wf_def Specs_def image_Un_conv) 2127 apply (rule_tac x=q in bexI) 2128 apply (rule_tac x=Z in exI) 2129 apply (clarsimp simp add: CollInt_iff) 2130 apply auto 2131 done 2132 hence "\<Gamma>,Specs_wf p \<sigma> 2133 \<turnstile>\<^sub>t\<^bsub>/F\<^esub>({\<sigma>} \<inter> 2134 {s. s = Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2135 \<Gamma>\<turnstile>Call p\<down>Normal s}) 2136 (the (\<Gamma> p)) 2137 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2138 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" 2139 by (simp only: exec_Call_body' [OF defined] 2140 noFaultStuck_Call_body' [OF defined] 2141 terminates_Normal_Call_body [OF defined]) 2142 } note bdy=this 2143 show ?thesis 2144 apply (intro ballI allI) 2145 apply (rule hoaret.CallRec [where Specs="(\<Union>p\<in>dom \<Gamma>. \<Union>Z. 2146 {({s. s=Z \<and> 2147 \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and> 2148 \<Gamma>\<turnstile>Call p\<down>Normal s}, 2149 p, 2150 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}, 2151 {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t})})", 2152 OF _ wf_termi_call_steps [of \<Gamma>] refl]) 2153 apply fastforce 2154 apply clarify 2155 apply (rule conjI) 2156 apply fastforce 2157 apply (rule allI) 2158 apply (simp (no_asm_use) only : Un_empty_left) 2159 apply (rule bdy) 2160 apply auto 2161 done 2162qed 2163 2164 2165theorem hoaret_complete: "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A \<Longrightarrow> \<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2166 by (iprover intro: MGT_implies_complete MGT_lemma [OF MGT_Call]) 2167 2168lemma hoaret_complete': 2169 assumes cvalid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2170 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2171proof (cases "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A") 2172 case True 2173 hence "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2174 by (rule hoaret_complete) 2175 thus "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2176 by (rule hoaret_augment_context) simp 2177next 2178 case False 2179 with cvalid 2180 show ?thesis 2181 by (rule ExFalso) 2182qed 2183 2184subsection \<open>And Now: Some Useful Rules\<close> 2185 2186subsubsection \<open>Modify Return\<close> 2187 2188lemma ProcModifyReturn_sound: 2189 assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c Q,A" 2190 assumes valid_modif: 2191 "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)" 2192 assumes res_modif: 2193 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 2194 assumes ret_modifAbr: 2195 "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 2196 shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 2197proof (rule cvalidtI) 2198 fix s t 2199 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2200 hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2201 by (auto simp add: validt_def) 2202 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 2203 by (auto intro: valid_augment_Faults) 2204 assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> \<Rightarrow> t" 2205 assume P: "s \<in> P" 2206 assume t_notin_F: "t \<notin> Fault ` F" 2207 from exec 2208 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2209 proof (cases rule: exec_call_Normal_elim) 2210 fix bdy t' 2211 assume bdy: "\<Gamma> p = Some bdy" 2212 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2213 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" 2214 from exec_body bdy 2215 have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2216 by (auto simp add: intro: exec.intros) 2217 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2218 have "t' \<in> Modif (init s)" 2219 by auto 2220 with res_modif have "Normal (return' s t') = Normal (return s t')" 2221 by simp 2222 with exec_body exec_c bdy 2223 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2224 by (auto intro: exec_call) 2225 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2226 show ?thesis 2227 by simp 2228 next 2229 fix bdy t' 2230 assume bdy: "\<Gamma> p = Some bdy" 2231 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2232 assume t: "t = Abrupt (return s t')" 2233 also from exec_body bdy 2234 have "\<Gamma>\<turnstile>\<langle>(Call p),Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2235 by (auto simp add: intro: exec.intros) 2236 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2237 have "t' \<in> ModifAbr (init s)" 2238 by auto 2239 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 2240 by simp 2241 finally have "t = Abrupt (return' s t')" . 2242 with exec_body bdy 2243 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2244 by (auto intro: exec_callAbrupt) 2245 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2246 show ?thesis 2247 by simp 2248 next 2249 fix bdy f 2250 assume bdy: "\<Gamma> p = Some bdy" 2251 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and 2252 t: "t = Fault f" 2253 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t" 2254 by (auto intro: exec_callFault) 2255 from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F 2256 show ?thesis 2257 by simp 2258 next 2259 fix bdy 2260 assume bdy: "\<Gamma> p = Some bdy" 2261 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" 2262 "t = Stuck" 2263 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t" 2264 by (auto intro: exec_callStuck) 2265 from valid_call ctxt this P t_notin_F 2266 show ?thesis 2267 by (rule cvalidt_postD) 2268 next 2269 assume "\<Gamma> p = None" "t=Stuck" 2270 hence "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t" 2271 by (auto intro: exec_callUndefined) 2272 from valid_call ctxt this P t_notin_F 2273 show ?thesis 2274 by (rule cvalidt_postD) 2275 qed 2276next 2277 fix s 2278 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2279 hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2280 by (auto simp add: validt_def) 2281 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 2282 by (auto intro: valid_augment_Faults) 2283 assume P: "s \<in> P" 2284 from valid_call ctxt P 2285 have call: "\<Gamma>\<turnstile>call init p return' c\<down> Normal s" 2286 by (rule cvalidt_termD) 2287 show "\<Gamma>\<turnstile>call init p return c \<down> Normal s" 2288 proof (cases "p \<in> dom \<Gamma>") 2289 case True 2290 with call obtain bdy where 2291 bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and 2292 termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> 2293 \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" 2294 by cases auto 2295 { 2296 fix t 2297 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t" 2298 hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" 2299 proof - 2300 from exec_bdy bdy 2301 have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t" 2302 by (auto simp add: intro: exec.intros) 2303 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2304 res_modif 2305 have "return' s t = return s t" 2306 by auto 2307 with termi_c exec_bdy show ?thesis by auto 2308 qed 2309 } 2310 with bdy termi_bdy 2311 show ?thesis 2312 by (iprover intro: terminates_call) 2313 next 2314 case False 2315 thus ?thesis 2316 by (auto intro: terminates_callUndefined) 2317 qed 2318qed 2319 2320lemma ProcModifyReturn: 2321 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 2322 assumes res_modif: 2323 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 2324 assumes ret_modifAbr: 2325 "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)" 2326 assumes modifies_spec: 2327 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)" 2328 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 2329apply (rule hoaret_complete') 2330apply (rule ProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr, 2331 OF _ _ res_modif ret_modifAbr]) 2332apply (rule hoaret_sound [OF spec]) 2333using modifies_spec 2334apply (blast intro: hoare_sound) 2335done 2336 2337lemma ProcModifyReturnSameFaults_sound: 2338 assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P call init p return' c Q,A" 2339 assumes valid_modif: 2340 "\<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)" 2341 assumes res_modif: 2342 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 2343 assumes ret_modifAbr: 2344 "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 2345 shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 2346proof (rule cvalidtI) 2347 fix s t 2348 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2349 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2350 by (auto simp add: validt_def) 2351 assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> \<Rightarrow> t" 2352 assume P: "s \<in> P" 2353 assume t_notin_F: "t \<notin> Fault ` F" 2354 from exec 2355 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2356 proof (cases rule: exec_call_Normal_elim) 2357 fix bdy t' 2358 assume bdy: "\<Gamma> p = Some bdy" 2359 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2360 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" 2361 from exec_body bdy 2362 have "\<Gamma>\<turnstile>\<langle>(Call p) ,Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2363 by (auto simp add: intro: exec.intros) 2364 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2365 have "t' \<in> Modif (init s)" 2366 by auto 2367 with res_modif have "Normal (return' s t') = Normal (return s t')" 2368 by simp 2369 with exec_body exec_c bdy 2370 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2371 by (auto intro: exec_call) 2372 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2373 show ?thesis 2374 by simp 2375 next 2376 fix bdy t' 2377 assume bdy: "\<Gamma> p = Some bdy" 2378 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2379 assume t: "t = Abrupt (return s t')" 2380 also 2381 from exec_body bdy 2382 have "\<Gamma>\<turnstile>\<langle>Call p ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2383 by (auto simp add: intro: exec.intros) 2384 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2385 have "t' \<in> ModifAbr (init s)" 2386 by auto 2387 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 2388 by simp 2389 finally have "t = Abrupt (return' s t')" . 2390 with exec_body bdy 2391 have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2392 by (auto intro: exec_callAbrupt) 2393 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2394 show ?thesis 2395 by simp 2396 next 2397 fix bdy f 2398 assume bdy: "\<Gamma> p = Some bdy" 2399 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and 2400 t: "t = Fault f" 2401 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> \<Rightarrow> t" 2402 by (auto intro: exec_callFault) 2403 from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F 2404 show ?thesis 2405 by simp 2406 next 2407 fix bdy 2408 assume bdy: "\<Gamma> p = Some bdy" 2409 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" 2410 "t = Stuck" 2411 with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2412 by (auto intro: exec_callStuck) 2413 from valid_call ctxt this P t_notin_F 2414 show ?thesis 2415 by (rule cvalidt_postD) 2416 next 2417 assume "\<Gamma> p = None" "t=Stuck" 2418 hence "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> \<Rightarrow> t" 2419 by (auto intro: exec_callUndefined) 2420 from valid_call ctxt this P t_notin_F 2421 show ?thesis 2422 by (rule cvalidt_postD) 2423 qed 2424next 2425 fix s 2426 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2427 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2428 by (auto simp add: validt_def) 2429 assume P: "s \<in> P" 2430 from valid_call ctxt P 2431 have call: "\<Gamma>\<turnstile>call init p return' c\<down> Normal s" 2432 by (rule cvalidt_termD) 2433 show "\<Gamma>\<turnstile>call init p return c \<down> Normal s" 2434 proof (cases "p \<in> dom \<Gamma>") 2435 case True 2436 with call obtain bdy where 2437 bdy: "\<Gamma> p = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and 2438 termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> 2439 \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" 2440 by cases auto 2441 { 2442 fix t 2443 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t" 2444 hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" 2445 proof - 2446 from exec_bdy bdy 2447 have "\<Gamma>\<turnstile>\<langle>(Call p ),Normal (init s)\<rangle> \<Rightarrow> Normal t" 2448 by (auto simp add: intro: exec.intros) 2449 from cvalidD [OF valid_modif [rule_format, of "init s"] ctxt' this] P 2450 res_modif 2451 have "return' s t = return s t" 2452 by auto 2453 with termi_c exec_bdy show ?thesis by auto 2454 qed 2455 } 2456 with bdy termi_bdy 2457 show ?thesis 2458 by (iprover intro: terminates_call) 2459 next 2460 case False 2461 thus ?thesis 2462 by (auto intro: terminates_callUndefined) 2463 qed 2464qed 2465 2466lemma ProcModifyReturnSameFaults: 2467 assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A" 2468 assumes res_modif: 2469 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)" 2470 assumes ret_modifAbr: 2471 "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)" 2472 assumes modifies_spec: 2473 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call p) (Modif \<sigma>),(ModifAbr \<sigma>)" 2474 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A" 2475apply (rule hoaret_complete') 2476apply (rule ProcModifyReturnSameFaults_sound [where Modif=Modif and ModifAbr=ModifAbr, 2477 OF _ _ res_modif ret_modifAbr]) 2478apply (rule hoaret_sound [OF spec]) 2479using modifies_spec 2480apply (blast intro: hoare_sound) 2481done 2482 2483 2484subsubsection \<open>DynCall\<close> 2485 2486 2487lemma dynProcModifyReturn_sound: 2488assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 2489assumes valid_modif: 2490 "\<forall>s\<in>P. \<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)" 2491assumes ret_modif: 2492 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 2493assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 2494shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 2495proof (rule cvalidtI) 2496 fix s t 2497 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2498 hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2499 by (auto simp add: validt_def) 2500 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 2501 by (auto intro: valid_augment_Faults) 2502 assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> \<Rightarrow> t" 2503 assume t_notin_F: "t \<notin> Fault ` F" 2504 assume P: "s \<in> P" 2505 with valid_modif 2506 have valid_modif': 2507 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)" 2508 by blast 2509 from exec 2510 have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> \<Rightarrow> t" 2511 by (cases rule: exec_dynCall_Normal_elim) 2512 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 2513 proof (cases rule: exec_call_Normal_elim) 2514 fix bdy t' 2515 assume bdy: "\<Gamma> (p s) = Some bdy" 2516 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2517 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" 2518 from exec_body bdy 2519 have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2520 by (auto simp add: intro: exec.Call) 2521 from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P 2522 have "t' \<in> Modif (init s)" 2523 by auto 2524 with ret_modif have "Normal (return' s t') = 2525 Normal (return s t')" 2526 by simp 2527 with exec_body exec_c bdy 2528 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t" 2529 by (auto intro: exec_call) 2530 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2531 by (rule exec_dynCall) 2532 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2533 show ?thesis 2534 by simp 2535 next 2536 fix bdy t' 2537 assume bdy: "\<Gamma> (p s) = Some bdy" 2538 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2539 assume t: "t = Abrupt (return s t')" 2540 also from exec_body bdy 2541 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2542 by (auto simp add: intro: exec.intros) 2543 from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P 2544 have "t' \<in> ModifAbr (init s)" 2545 by auto 2546 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 2547 by simp 2548 finally have "t = Abrupt (return' s t')" . 2549 with exec_body bdy 2550 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t" 2551 by (auto intro: exec_callAbrupt) 2552 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2553 by (rule exec_dynCall) 2554 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2555 show ?thesis 2556 by simp 2557 next 2558 fix bdy f 2559 assume bdy: "\<Gamma> (p s) = Some bdy" 2560 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and 2561 t: "t = Fault f" 2562 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2563 by (auto intro: exec_callFault) 2564 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2565 by (rule exec_dynCall) 2566 from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F 2567 show ?thesis 2568 by blast 2569 next 2570 fix bdy 2571 assume bdy: "\<Gamma> (p s) = Some bdy" 2572 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" 2573 "t = Stuck" 2574 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2575 by (auto intro: exec_callStuck) 2576 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2577 by (rule exec_dynCall) 2578 from valid_call ctxt this P t_notin_F 2579 show ?thesis 2580 by (rule cvalidt_postD) 2581 next 2582 fix bdy 2583 assume "\<Gamma> (p s) = None" "t=Stuck" 2584 hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2585 by (auto intro: exec_callUndefined) 2586 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2587 by (rule exec_dynCall) 2588 from valid_call ctxt this P t_notin_F 2589 show ?thesis 2590 by (rule cvalidt_postD) 2591 qed 2592next 2593 fix s 2594 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2595 hence "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2596 by (auto simp add: validt_def) 2597 then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/UNIV\<^esub> P (Call p) Q,A" 2598 by (auto intro: valid_augment_Faults) 2599 assume P: "s \<in> P" 2600 from valid_call ctxt P 2601 have "\<Gamma>\<turnstile>dynCall init p return' c\<down> Normal s" 2602 by (rule cvalidt_termD) 2603 hence call: "\<Gamma>\<turnstile>call init (p s) return' c\<down> Normal s" 2604 by cases 2605 have "\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s" 2606 proof (cases "p s \<in> dom \<Gamma>") 2607 case True 2608 with call obtain bdy where 2609 bdy: "\<Gamma> (p s) = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and 2610 termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> 2611 \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" 2612 by cases auto 2613 { 2614 fix t 2615 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t" 2616 hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" 2617 proof - 2618 from exec_bdy bdy 2619 have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t" 2620 by (auto simp add: intro: exec.intros) 2621 from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P 2622 ret_modif 2623 have "return' s t = return s t" 2624 by auto 2625 with termi_c exec_bdy show ?thesis by auto 2626 qed 2627 } 2628 with bdy termi_bdy 2629 show ?thesis 2630 by (iprover intro: terminates_call) 2631 next 2632 case False 2633 thus ?thesis 2634 by (auto intro: terminates_callUndefined) 2635 qed 2636 thus "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s" 2637 by (iprover intro: terminates_dynCall) 2638qed 2639 2640lemma dynProcModifyReturn: 2641assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 2642assumes ret_modif: 2643 "\<forall>s t. t \<in> Modif (init s) 2644 \<longrightarrow> return' s t = return s t" 2645assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) 2646 \<longrightarrow> return' s t = return s t" 2647assumes modif: 2648 "\<forall>s \<in> P. \<forall>\<sigma>. 2649 \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 2650shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 2651apply (rule hoaret_complete') 2652apply (rule dynProcModifyReturn_sound 2653 [where Modif=Modif and ModifAbr=ModifAbr, 2654 OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr]) 2655apply (intro ballI allI) 2656apply (rule hoare_sound [OF modif [rule_format]]) 2657apply assumption 2658done 2659 2660lemma dynProcModifyReturnSameFaults_sound: 2661assumes valid_call: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 2662assumes valid_modif: 2663 "\<forall>s\<in>P. \<forall>\<sigma>. \<Gamma>,\<Theta> \<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 2664assumes ret_modif: 2665 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 2666assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 2667shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 2668proof (rule cvalidtI) 2669 fix s t 2670 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2671 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2672 by (auto simp add: validt_def) 2673 assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> \<Rightarrow> t" 2674 assume t_notin_F: "t \<notin> Fault ` F" 2675 assume P: "s \<in> P" 2676 with valid_modif 2677 have valid_modif': 2678 "\<forall>\<sigma>. \<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),(ModifAbr \<sigma>)" 2679 by blast 2680 from exec 2681 have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> \<Rightarrow> t" 2682 by (cases rule: exec_dynCall_Normal_elim) 2683 then show "t \<in> Normal ` Q \<union> Abrupt ` A" 2684 proof (cases rule: exec_call_Normal_elim) 2685 fix bdy t' 2686 assume bdy: "\<Gamma> (p s) = Some bdy" 2687 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2688 assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t" 2689 from exec_body bdy 2690 have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t'" 2691 by (auto simp add: intro: exec.intros) 2692 from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P 2693 have "t' \<in> Modif (init s)" 2694 by auto 2695 with ret_modif have "Normal (return' s t') = 2696 Normal (return s t')" 2697 by simp 2698 with exec_body exec_c bdy 2699 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t" 2700 by (auto intro: exec_call) 2701 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2702 by (rule exec_dynCall) 2703 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2704 show ?thesis 2705 by simp 2706 next 2707 fix bdy t' 2708 assume bdy: "\<Gamma> (p s) = Some bdy" 2709 assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2710 assume t: "t = Abrupt (return s t')" 2711 also from exec_body bdy 2712 have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> \<Rightarrow> Abrupt t'" 2713 by (auto simp add: intro: exec.intros) 2714 from cvalidD [OF valid_modif' [rule_format, of "init s"] ctxt' this] P 2715 have "t' \<in> ModifAbr (init s)" 2716 by auto 2717 with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')" 2718 by simp 2719 finally have "t = Abrupt (return' s t')" . 2720 with exec_body bdy 2721 have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> \<Rightarrow> t" 2722 by (auto intro: exec_callAbrupt) 2723 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2724 by (rule exec_dynCall) 2725 from cvalidt_postD [OF valid_call ctxt this] P t_notin_F 2726 show ?thesis 2727 by simp 2728 next 2729 fix bdy f 2730 assume bdy: "\<Gamma> (p s) = Some bdy" 2731 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f" and 2732 t: "t = Fault f" 2733 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2734 by (auto intro: exec_callFault) 2735 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2736 by (rule exec_dynCall) 2737 from cvalidt_postD [OF valid_call ctxt this P] t t_notin_F 2738 show ?thesis 2739 by simp 2740 next 2741 fix bdy 2742 assume bdy: "\<Gamma> (p s) = Some bdy" 2743 assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck" 2744 "t = Stuck" 2745 with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2746 by (auto intro: exec_callStuck) 2747 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2748 by (rule exec_dynCall) 2749 from valid_call ctxt this P t_notin_F 2750 show ?thesis 2751 by (rule cvalidt_postD) 2752 next 2753 fix bdy 2754 assume "\<Gamma> (p s) = None" "t=Stuck" 2755 hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> \<Rightarrow> t" 2756 by (auto intro: exec_callUndefined) 2757 hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> \<Rightarrow> t" 2758 by (rule exec_dynCall) 2759 from valid_call ctxt this P t_notin_F 2760 show ?thesis 2761 by (rule cvalidt_postD) 2762 qed 2763next 2764 fix s 2765 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2766 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2767 by (auto simp add: validt_def) 2768 assume P: "s \<in> P" 2769 from valid_call ctxt P 2770 have "\<Gamma>\<turnstile>dynCall init p return' c\<down> Normal s" 2771 by (rule cvalidt_termD) 2772 hence call: "\<Gamma>\<turnstile>call init (p s) return' c\<down> Normal s" 2773 by cases 2774 have "\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s" 2775 proof (cases "p s \<in> dom \<Gamma>") 2776 case True 2777 with call obtain bdy where 2778 bdy: "\<Gamma> (p s) = Some bdy" and termi_bdy: "\<Gamma>\<turnstile>bdy \<down> Normal (init s)" and 2779 termi_c: "\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> 2780 \<Gamma>\<turnstile>c s t \<down> Normal (return' s t)" 2781 by cases auto 2782 { 2783 fix t 2784 assume exec_bdy: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t" 2785 hence "\<Gamma>\<turnstile>c s t \<down> Normal (return s t)" 2786 proof - 2787 from exec_bdy bdy 2788 have "\<Gamma>\<turnstile>\<langle>Call (p s),Normal (init s)\<rangle> \<Rightarrow> Normal t" 2789 by (auto simp add: intro: exec.intros) 2790 from cvalidD [OF valid_modif [rule_format, of s "init s"] ctxt' this] P 2791 ret_modif 2792 have "return' s t = return s t" 2793 by auto 2794 with termi_c exec_bdy show ?thesis by auto 2795 qed 2796 } 2797 with bdy termi_bdy 2798 show ?thesis 2799 by (iprover intro: terminates_call) 2800 next 2801 case False 2802 thus ?thesis 2803 by (auto intro: terminates_callUndefined) 2804 qed 2805 thus "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s" 2806 by (iprover intro: terminates_dynCall) 2807qed 2808 2809lemma dynProcModifyReturnSameFaults: 2810assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return' c Q,A" 2811assumes ret_modif: 2812 "\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t" 2813assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t" 2814assumes modif: 2815 "\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)" 2816shows "\<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A" 2817apply (rule hoaret_complete') 2818apply (rule dynProcModifyReturnSameFaults_sound 2819 [where Modif=Modif and ModifAbr=ModifAbr, 2820 OF hoaret_sound [OF dyn_call] _ ret_modif ret_modifAbr]) 2821apply (intro ballI allI) 2822apply (rule hoare_sound [OF modif [rule_format]]) 2823apply assumption 2824done 2825 2826subsubsection \<open>Conjunction of Postcondition\<close> 2827 2828lemma PostConjI_sound: 2829 assumes valid_Q: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2830 assumes valid_R: "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B" 2831 shows "\<Gamma>,\<Theta> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 2832proof (rule cvalidtI) 2833 fix s t 2834 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2835 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 2836 assume P: "s \<in> P" 2837 assume t_notin_F: "t \<notin> Fault ` F" 2838 from valid_Q ctxt exec P t_notin_F have "t \<in> Normal ` Q \<union> Abrupt ` A" 2839 by (rule cvalidt_postD) 2840 moreover 2841 from valid_R ctxt exec P t_notin_F have "t \<in> Normal ` R \<union> Abrupt ` B" 2842 by (rule cvalidt_postD) 2843 ultimately show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> B)" 2844 by blast 2845next 2846 fix s 2847 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2848 assume P: "s \<in> P" 2849 from valid_Q ctxt P 2850 show "\<Gamma>\<turnstile>c \<down> Normal s" 2851 by (rule cvalidt_termD) 2852qed 2853 2854lemma PostConjI: 2855 assumes deriv_Q: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2856 assumes deriv_R: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c R,B" 2857 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> B)" 2858apply (rule hoaret_complete') 2859apply (rule PostConjI_sound) 2860apply (rule hoaret_sound [OF deriv_Q]) 2861apply (rule hoaret_sound [OF deriv_R]) 2862done 2863 2864 2865lemma Merge_PostConj_sound: 2866 assumes validF: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2867 assumes validG: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/G\<^esub> P' c R,X" 2868 assumes F_G: "F \<subseteq> G" 2869 assumes P_P': "P \<subseteq> P'" 2870 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)" 2871proof (rule cvalidtI) 2872 fix s t 2873 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2874 with F_G have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/G\<^esub> P (Call p) Q,A" 2875 by (auto intro: validt_augment_Faults) 2876 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 2877 assume P: "s \<in> P" 2878 with P_P' have P': "s \<in> P'" 2879 by auto 2880 assume t_noFault: "t \<notin> Fault ` F" 2881 show "t \<in> Normal ` (Q \<inter> R) \<union> Abrupt ` (A \<inter> X)" 2882 proof - 2883 from cvalidt_postD [OF validF [rule_format] ctxt exec P t_noFault] 2884 have t: "t \<in> Normal ` Q \<union> Abrupt ` A". 2885 then have "t \<notin> Fault ` G" 2886 by auto 2887 from cvalidt_postD [OF validG [rule_format] ctxt' exec P' this] 2888 have "t \<in> Normal ` R \<union> Abrupt ` X" . 2889 with t show ?thesis by auto 2890 qed 2891next 2892 fix s 2893 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2894 assume P: "s \<in> P" 2895 from validF ctxt P 2896 show "\<Gamma>\<turnstile>c \<down> Normal s" 2897 by (rule cvalidt_termD) 2898qed 2899 2900 2901 2902lemma Merge_PostConj: 2903 assumes validF: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2904 assumes validG: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/G\<^esub> P' c R,X" 2905 assumes F_G: "F \<subseteq> G" 2906 assumes P_P': "P \<subseteq> P'" 2907 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c (Q \<inter> R),(A \<inter> X)" 2908apply (rule hoaret_complete') 2909apply (rule Merge_PostConj_sound [OF _ _ F_G P_P']) 2910using validF apply (blast intro:hoaret_sound) 2911using validG apply (blast intro:hoaret_sound) 2912done 2913 2914 2915subsubsection \<open>Guards and Guarantees\<close> 2916 2917lemma SplitGuards_sound: 2918 assumes valid_c1: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" 2919 assumes valid_c2: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV" 2920 assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c" 2921 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2922proof (rule cvalidtI) 2923 fix s t 2924 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2925 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^bsub>/F\<^esub> P (Call p) Q,A" 2926 by (auto simp add: validt_def) 2927 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 2928 assume P: "s \<in> P" 2929 assume t_notin_F: "t \<notin> Fault ` F" 2930 show "t \<in> Normal ` Q \<union> Abrupt ` A" 2931 proof (cases t) 2932 case Normal 2933 with inter_guards_exec_noFault [OF c exec] 2934 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp 2935 from valid_c1 ctxt this P t_notin_F 2936 show ?thesis 2937 by (rule cvalidt_postD) 2938 next 2939 case Abrupt 2940 with inter_guards_exec_noFault [OF c exec] 2941 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp 2942 from valid_c1 ctxt this P t_notin_F 2943 show ?thesis 2944 by (rule cvalidt_postD) 2945 next 2946 case (Fault f) 2947 assume t: "t=Fault f" 2948 with exec inter_guards_exec_Fault [OF c] 2949 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault f \<or> \<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault f" 2950 by auto 2951 then show ?thesis 2952 proof (cases rule: disjE [consumes 1]) 2953 assume "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault f" 2954 from cvalidt_postD [OF valid_c1 ctxt this P] t t_notin_F 2955 show ?thesis 2956 by blast 2957 next 2958 assume "\<Gamma>\<turnstile>\<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault f" 2959 from cvalidD [OF valid_c2 ctxt' this P] t t_notin_F 2960 show ?thesis 2961 by blast 2962 qed 2963 next 2964 case Stuck 2965 with inter_guards_exec_noFault [OF c exec] 2966 have "\<Gamma>\<turnstile>\<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t" by simp 2967 from valid_c1 ctxt this P t_notin_F 2968 show ?thesis 2969 by (rule cvalidt_postD) 2970 qed 2971next 2972 fix s 2973 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 2974 assume P: "s \<in> P" 2975 show "\<Gamma>\<turnstile>c \<down> Normal s" 2976 proof - 2977 from valid_c1 ctxt P 2978 have "\<Gamma>\<turnstile>c\<^sub>1 \<down> Normal s" 2979 by (rule cvalidt_termD) 2980 with c show ?thesis 2981 by (rule inter_guards_terminates) 2982 qed 2983qed 2984 2985lemma SplitGuards: 2986 assumes c: "(c\<^sub>1 \<inter>\<^sub>g c\<^sub>2) = Some c" 2987 assumes deriv_c1: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c\<^sub>1 Q,A" 2988 assumes deriv_c2: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>2 UNIV,UNIV" 2989 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2990apply (rule hoaret_complete') 2991apply (rule SplitGuards_sound [OF _ _ c]) 2992apply (rule hoaret_sound [OF deriv_c1]) 2993apply (rule hoare_sound [OF deriv_c2]) 2994done 2995 2996lemma CombineStrip_sound: 2997 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 2998 assumes valid_strip: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV" 2999 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3000proof (rule cvalidtI) 3001 fix s t 3002 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3003 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> P (Call p) Q,A" 3004 by (auto simp add: validt_def) 3005 from ctxt have ctxt'': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3006 by (auto intro: valid_augment_Faults simp add: validt_def) 3007 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3008 assume P: "s \<in> P" 3009 assume t_noFault: "t \<notin> Fault ` {}" 3010 show "t \<in> Normal ` Q \<union> Abrupt ` A" 3011 proof (cases t) 3012 case (Normal t') 3013 from cvalidt_postD [OF valid ctxt'' exec P] Normal 3014 show ?thesis 3015 by auto 3016 next 3017 case (Abrupt t') 3018 from cvalidt_postD [OF valid ctxt'' exec P] Abrupt 3019 show ?thesis 3020 by auto 3021 next 3022 case (Fault f) 3023 show ?thesis 3024 proof (cases "f \<in> F") 3025 case True 3026 hence "f \<notin> -F" by simp 3027 with exec Fault 3028 have "\<Gamma>\<turnstile>\<langle>strip_guards (-F) c,Normal s\<rangle> \<Rightarrow> Fault f" 3029 by (auto intro: exec_to_exec_strip_guards_Fault) 3030 from cvalidD [OF valid_strip ctxt' this P] Fault 3031 have False 3032 by auto 3033 thus ?thesis .. 3034 next 3035 case False 3036 with cvalidt_postD [OF valid ctxt'' exec P] Fault 3037 show ?thesis 3038 by auto 3039 qed 3040 next 3041 case Stuck 3042 from cvalidt_postD [OF valid ctxt'' exec P] Stuck 3043 show ?thesis 3044 by auto 3045 qed 3046next 3047 fix s 3048 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3049 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3050 by (auto intro: valid_augment_Faults simp add: validt_def) 3051 assume P: "s \<in> P" 3052 show "\<Gamma>\<turnstile>c \<down> Normal s" 3053 proof - 3054 from valid ctxt' P 3055 show "\<Gamma>\<turnstile>c \<down> Normal s" 3056 by (rule cvalidt_termD) 3057 qed 3058qed 3059 3060lemma CombineStrip: 3061 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3062 assumes deriv_strip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/{}\<^esub> P (strip_guards (-F) c) UNIV,UNIV" 3063 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3064apply (rule hoaret_complete') 3065apply (rule CombineStrip_sound) 3066apply (iprover intro: hoaret_sound [OF deriv]) 3067apply (iprover intro: hoare_sound [OF deriv_strip]) 3068done 3069 3070lemma GuardsFlip_sound: 3071 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3072 assumes validFlip: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV" 3073 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3074proof (rule cvalidtI) 3075 fix s t 3076 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3077 from ctxt have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3078 by (auto intro: valid_augment_Faults simp add: validt_def) 3079 from ctxt have ctxtFlip: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^bsub>/-F\<^esub> P (Call p) Q,A" 3080 by (auto intro: valid_augment_Faults simp add: validt_def) 3081 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3082 assume P: "s \<in> P" 3083 assume t_noFault: "t \<notin> Fault ` {}" 3084 show "t \<in> Normal ` Q \<union> Abrupt ` A" 3085 proof (cases t) 3086 case (Normal t') 3087 from cvalidt_postD [OF valid ctxt' exec P] Normal 3088 show ?thesis 3089 by auto 3090 next 3091 case (Abrupt t') 3092 from cvalidt_postD [OF valid ctxt' exec P] Abrupt 3093 show ?thesis 3094 by auto 3095 next 3096 case (Fault f) 3097 show ?thesis 3098 proof (cases "f \<in> F") 3099 case True 3100 hence "f \<notin> -F" by simp 3101 with cvalidD [OF validFlip ctxtFlip exec P] Fault 3102 have False 3103 by auto 3104 thus ?thesis .. 3105 next 3106 case False 3107 with cvalidt_postD [OF valid ctxt' exec P] Fault 3108 show ?thesis 3109 by auto 3110 qed 3111 next 3112 case Stuck 3113 from cvalidt_postD [OF valid ctxt' exec P] Stuck 3114 show ?thesis 3115 by auto 3116 qed 3117next 3118 fix s 3119 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3120 hence ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3121 by (auto intro: valid_augment_Faults simp add: validt_def) 3122 assume P: "s \<in> P" 3123 show "\<Gamma>\<turnstile>c \<down> Normal s" 3124 proof - 3125 from valid ctxt' P 3126 show "\<Gamma>\<turnstile>c \<down> Normal s" 3127 by (rule cvalidt_termD) 3128 qed 3129qed 3130 3131 3132lemma GuardsFlip: 3133 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3134 assumes derivFlip: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/-F\<^esub> P c UNIV,UNIV" 3135 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3136apply (rule hoaret_complete') 3137apply (rule GuardsFlip_sound) 3138apply (iprover intro: hoaret_sound [OF deriv]) 3139apply (iprover intro: hoare_sound [OF derivFlip]) 3140done 3141 3142lemma MarkGuardsI_sound: 3143 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3144 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 3145proof (rule cvalidtI) 3146 fix s t 3147 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3148 assume exec: "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> t" 3149 from exec_mark_guards_to_exec [OF exec] obtain t' where 3150 exec_c: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t'" and 3151 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 3152 by blast 3153 assume P: "s \<in> P" 3154 assume t_noFault: "t \<notin> Fault ` {}" 3155 show "t \<in> Normal ` Q \<union> Abrupt ` A" 3156 proof - 3157 from cvalidt_postD [OF valid [rule_format] ctxt exec_c P] 3158 have "t' \<in> Normal ` Q \<union> Abrupt ` A" 3159 by blast 3160 with t'_noFault 3161 show ?thesis 3162 by auto 3163 qed 3164next 3165 fix s 3166 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3167 assume P: "s \<in> P" 3168 from cvalidt_termD [OF valid ctxt P] 3169 have "\<Gamma>\<turnstile>c \<down> Normal s". 3170 thus "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s" 3171 by (rule terminates_to_terminates_mark_guards) 3172qed 3173 3174lemma MarkGuardsI: 3175 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3176 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 3177apply (rule hoaret_complete') 3178apply (rule MarkGuardsI_sound) 3179apply (iprover intro: hoaret_sound [OF deriv]) 3180done 3181 3182 3183lemma MarkGuardsD_sound: 3184 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 3185 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3186proof (rule cvalidtI) 3187 fix s t 3188 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3189 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3190 assume P: "s \<in> P" 3191 assume t_noFault: "t \<notin> Fault ` {}" 3192 show "t \<in> Normal ` Q \<union> Abrupt ` A" 3193 proof (cases "isFault t") 3194 case True 3195 with exec_to_exec_mark_guards_Fault exec 3196 obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> Fault f'" 3197 by (fastforce elim: isFaultE) 3198 from cvalidt_postD [OF valid [rule_format] ctxt this P] 3199 have False 3200 by auto 3201 thus ?thesis .. 3202 next 3203 case False 3204 from exec_to_exec_mark_guards [OF exec False] 3205 obtain f' where "\<Gamma>\<turnstile>\<langle>mark_guards f c,Normal s\<rangle> \<Rightarrow> t" 3206 by auto 3207 from cvalidt_postD [OF valid [rule_format] ctxt this P] 3208 show ?thesis 3209 by auto 3210 qed 3211next 3212 fix s 3213 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3214 assume P: "s \<in> P" 3215 from cvalidt_termD [OF valid ctxt P] 3216 have "\<Gamma>\<turnstile>mark_guards f c \<down> Normal s". 3217 thus "\<Gamma>\<turnstile>c \<down> Normal s" 3218 by (rule terminates_mark_guards_to_terminates) 3219qed 3220 3221lemma MarkGuardsD: 3222 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P mark_guards f c Q,A" 3223 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3224apply (rule hoaret_complete') 3225apply (rule MarkGuardsD_sound) 3226apply (iprover intro: hoaret_sound [OF deriv]) 3227done 3228 3229lemma MergeGuardsI_sound: 3230 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3231 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A" 3232proof (rule cvalidtI) 3233 fix s t 3234 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3235 assume exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> \<Rightarrow> t" 3236 from exec_merge_guards_to_exec [OF exec_merge] 3237 have exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" . 3238 assume P: "s \<in> P" 3239 assume t_notin_F: "t \<notin> Fault ` F" 3240 from cvalidt_postD [OF valid [rule_format] ctxt exec P t_notin_F] 3241 show "t \<in> Normal ` Q \<union> Abrupt ` A". 3242next 3243 fix s 3244 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3245 assume P: "s \<in> P" 3246 from cvalidt_termD [OF valid ctxt P] 3247 have "\<Gamma>\<turnstile>c \<down> Normal s". 3248 thus "\<Gamma>\<turnstile>merge_guards c \<down> Normal s" 3249 by (rule terminates_to_terminates_merge_guards) 3250qed 3251 3252lemma MergeGuardsI: 3253 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3254 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A" 3255apply (rule hoaret_complete') 3256apply (rule MergeGuardsI_sound) 3257apply (iprover intro: hoaret_sound [OF deriv]) 3258done 3259 3260lemma MergeGuardsD_sound: 3261 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A" 3262 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3263proof (rule cvalidtI) 3264 fix s t 3265 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3266 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3267 from exec_to_exec_merge_guards [OF exec] 3268 have exec_merge: "\<Gamma>\<turnstile>\<langle>merge_guards c,Normal s\<rangle> \<Rightarrow> t". 3269 assume P: "s \<in> P" 3270 assume t_notin_F: "t \<notin> Fault ` F" 3271 from cvalidt_postD [OF valid [rule_format] ctxt exec_merge P t_notin_F] 3272 show "t \<in> Normal ` Q \<union> Abrupt ` A". 3273next 3274 fix s 3275 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3276 assume P: "s \<in> P" 3277 from cvalidt_termD [OF valid ctxt P] 3278 have "\<Gamma>\<turnstile>merge_guards c \<down> Normal s". 3279 thus "\<Gamma>\<turnstile>c \<down> Normal s" 3280 by (rule terminates_merge_guards_to_terminates) 3281qed 3282 3283lemma MergeGuardsD: 3284 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A" 3285 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3286apply (rule hoaret_complete') 3287apply (rule MergeGuardsD_sound) 3288apply (iprover intro: hoaret_sound [OF deriv]) 3289done 3290 3291 3292lemma SubsetGuards_sound: 3293 assumes c_c': "c \<subseteq>\<^sub>g c'" 3294 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c' Q,A" 3295 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3296proof (rule cvalidtI) 3297 fix s t 3298 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3299 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3300 from exec_to_exec_subseteq_guards [OF c_c' exec] obtain t' where 3301 exec_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> \<Rightarrow> t'" and 3302 t'_noFault: "\<not> isFault t' \<longrightarrow> t' = t" 3303 by blast 3304 assume P: "s \<in> P" 3305 assume t_noFault: "t \<notin> Fault ` {}" 3306 from cvalidt_postD [OF valid [rule_format] ctxt exec_c' P] t'_noFault t_noFault 3307 show "t \<in> Normal ` Q \<union> Abrupt ` A" 3308 by auto 3309next 3310 fix s 3311 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/{}\<^esub> P (Call p) Q,A" 3312 assume P: "s \<in> P" 3313 from cvalidt_termD [OF valid ctxt P] 3314 have termi_c': "\<Gamma>\<turnstile>c' \<down> Normal s". 3315 from cvalidt_postD [OF valid ctxt _ P] 3316 have noFault_c': "\<Gamma>\<turnstile>\<langle>c',Normal s\<rangle> \<Rightarrow>\<notin>Fault ` UNIV" 3317 by (auto simp add: final_notin_def) 3318 from termi_c' c_c' noFault_c' 3319 show "\<Gamma>\<turnstile>c \<down> Normal s" 3320 by (rule terminates_fewer_guards) 3321qed 3322 3323lemma SubsetGuards: 3324 assumes c_c': "c \<subseteq>\<^sub>g c'" 3325 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c' Q,A" 3326 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/{}\<^esub> P c Q,A" 3327apply (rule hoaret_complete') 3328apply (rule SubsetGuards_sound [OF c_c']) 3329apply (iprover intro: hoaret_sound [OF deriv]) 3330done 3331 3332lemma NormalizeD_sound: 3333 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A" 3334 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3335proof (rule cvalidtI) 3336 fix s t 3337 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3338 assume exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3339 hence exec_norm: "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> \<Rightarrow> t" 3340 by (rule exec_to_exec_normalize) 3341 assume P: "s \<in> P" 3342 assume noFault: "t \<notin> Fault ` F" 3343 from cvalidt_postD [OF valid [rule_format] ctxt exec_norm P noFault] 3344 show "t \<in> Normal ` Q \<union> Abrupt ` A". 3345next 3346 fix s 3347 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3348 assume P: "s \<in> P" 3349 from cvalidt_termD [OF valid ctxt P] 3350 have "\<Gamma>\<turnstile>normalize c \<down> Normal s". 3351 thus "\<Gamma>\<turnstile>c \<down> Normal s" 3352 by (rule terminates_normalize_to_terminates) 3353qed 3354 3355lemma NormalizeD: 3356 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A" 3357 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3358apply (rule hoaret_complete') 3359apply (rule NormalizeD_sound) 3360apply (iprover intro: hoaret_sound [OF deriv]) 3361done 3362 3363lemma NormalizeI_sound: 3364 assumes valid: "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3365 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A" 3366proof (rule cvalidtI) 3367 fix s t 3368 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3369 assume "\<Gamma>\<turnstile>\<langle>normalize c,Normal s\<rangle> \<Rightarrow> t" 3370 hence exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t" 3371 by (rule exec_normalize_to_exec) 3372 assume P: "s \<in> P" 3373 assume noFault: "t \<notin> Fault ` F" 3374 from cvalidt_postD [OF valid [rule_format] ctxt exec P noFault] 3375 show "t \<in> Normal ` Q \<union> Abrupt ` A". 3376next 3377 fix s 3378 assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P (Call p) Q,A" 3379 assume P: "s \<in> P" 3380 from cvalidt_termD [OF valid ctxt P] 3381 have "\<Gamma>\<turnstile> c \<down> Normal s". 3382 thus "\<Gamma>\<turnstile>normalize c \<down> Normal s" 3383 by (rule terminates_to_terminates_normalize) 3384qed 3385 3386lemma NormalizeI: 3387 assumes deriv: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3388 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (normalize c) Q,A" 3389apply (rule hoaret_complete') 3390apply (rule NormalizeI_sound) 3391apply (iprover intro: hoaret_sound [OF deriv]) 3392done 3393 3394subsubsection \<open>Restricting the Procedure Environment\<close> 3395 3396lemma validt_restrict_to_validt: 3397assumes validt_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3398shows "\<Gamma>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3399proof - 3400 from validt_c 3401 have valid_c: "\<Gamma>|\<^bsub>M\<^esub>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" by (simp add: validt_def) 3402 hence "\<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" by (rule valid_restrict_to_valid) 3403 moreover 3404 { 3405 fix s 3406 assume P: "s \<in> P" 3407 have "\<Gamma>\<turnstile>c\<down>Normal s" 3408 proof - 3409 from P validt_c have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>c\<down>Normal s" 3410 by (auto simp add: validt_def) 3411 moreover 3412 from P valid_c 3413 have "\<Gamma>|\<^bsub>M\<^esub>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck}" 3414 by (auto simp add: valid_def final_notin_def) 3415 ultimately show ?thesis 3416 by (rule terminates_restrict_to_terminates) 3417 qed 3418 } 3419 ultimately show ?thesis 3420 by (auto simp add: validt_def) 3421qed 3422 3423 3424lemma augment_procs: 3425assumes deriv_c: "\<Gamma>|\<^bsub>M\<^esub>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3426shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3427 apply (rule hoaret_complete) 3428 apply (rule validt_restrict_to_validt) 3429 apply (insert hoaret_sound [OF deriv_c]) 3430 by (simp add: cvalidt_def) 3431 3432subsubsection \<open>Miscellaneous\<close> 3433 3434lemma augment_Faults: 3435assumes deriv_c: "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3436assumes F: "F \<subseteq> F'" 3437shows "\<Gamma>,{}\<turnstile>\<^sub>t\<^bsub>/F'\<^esub> P c Q,A" 3438 apply (rule hoaret_complete) 3439 apply (rule validt_augment_Faults [OF _ F]) 3440 apply (insert hoaret_sound [OF deriv_c]) 3441 by (simp add: cvalidt_def) 3442 3443lemma TerminationPartial_sound: 3444 assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" 3445 assumes partial_corr: "\<Gamma>,\<Theta>\<Turnstile>\<^bsub>/F\<^esub> P c Q,A" 3446 shows "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3447using "termination" partial_corr 3448by (auto simp add: cvalidt_def validt_def cvalid_def) 3449 3450lemma TerminationPartial: 3451 assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 3452 assumes "termination": "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" 3453 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3454 apply (rule hoaret_complete') 3455 apply (rule TerminationPartial_sound [OF "termination"]) 3456 apply (rule hoare_sound [OF partial_deriv]) 3457 done 3458 3459lemma TerminationPartialStrip: 3460 assumes partial_deriv: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 3461 assumes "termination": "\<forall>s \<in> P. strip F' \<Gamma>\<turnstile>strip_guards F' c\<down>Normal s" 3462 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3463proof - 3464 from "termination" have "\<forall>s \<in> P. \<Gamma>\<turnstile>c\<down>Normal s" 3465 by (auto intro: terminates_strip_guards_to_terminates 3466 terminates_strip_to_terminates) 3467 with partial_deriv 3468 show ?thesis 3469 by (rule TerminationPartial) 3470qed 3471 3472lemma SplitTotalPartial: 3473 assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q',A'" 3474 assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 3475 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3476proof - 3477 from hoaret_sound [OF termi] hoare_sound [OF part] 3478 have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3479 by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def) 3480 thus ?thesis 3481 by (rule hoaret_complete') 3482qed 3483 3484lemma SplitTotalPartial': 3485 assumes termi: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/UNIV\<^esub> P c Q',A'" 3486 assumes part: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A" 3487 shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3488proof - 3489 from hoaret_sound [OF termi] hoare_sound [OF part] 3490 have "\<Gamma>,\<Theta>\<Turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A" 3491 by (fastforce simp add: cvalidt_def validt_def cvalid_def valid_def) 3492 thus ?thesis 3493 by (rule hoaret_complete') 3494qed 3495 3496end 3497