1(* Title: HOL/UNITY/WFair.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1998 University of Cambridge 4 5Conditional Fairness versions of transient, ensures, leadsTo. 6 7From Misra, "A Logic for Concurrent Programming", 1994 8*) 9 10section\<open>Progress\<close> 11 12theory WFair imports UNITY begin 13 14text\<open>The original version of this theory was based on weak fairness. (Thus, 15the entire UNITY development embodied this assumption, until February 2003.) 16Weak fairness states that if a command is enabled continuously, then it is 17eventually executed. Ernie Cohen suggested that I instead adopt unconditional 18fairness: every command is executed infinitely often. 19 20In fact, Misra's paper on "Progress" seems to be ambiguous about the correct 21interpretation, and says that the two forms of fairness are equivalent. They 22differ only on their treatment of partial transitions, which under 23unconditional fairness behave magically. That is because if there are partial 24transitions then there may be no fair executions, making all leads-to 25properties hold vacuously. 26 27Unconditional fairness has some great advantages. By distinguishing partial 28transitions from total ones that are the identity on part of their domain, it 29is more expressive. Also, by simplifying the definition of the transient 30property, it simplifies many proofs. A drawback is that some laws only hold 31under the assumption that all transitions are total. The best-known of these 32is the impossibility law for leads-to. 33\<close> 34 35definition 36 37 \<comment> \<open>This definition specifies conditional fairness. The rest of the theory 38 is generic to all forms of fairness. To get weak fairness, conjoin 39 the inclusion below with \<^term>\<open>A \<subseteq> Domain act\<close>, which specifies 40 that the action is enabled over all of \<^term>\<open>A\<close>.\<close> 41 transient :: "'a set => 'a program set" where 42 "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}" 43 44definition 45 ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) where 46 "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)" 47 48 49inductive_set 50 leads :: "'a program => ('a set * 'a set) set" 51 \<comment> \<open>LEADS-TO constant for the inductive definition\<close> 52 for F :: "'a program" 53 where 54 55 Basis: "F \<in> A ensures B ==> (A,B) \<in> leads F" 56 57 | Trans: "[| (A,B) \<in> leads F; (B,C) \<in> leads F |] ==> (A,C) \<in> leads F" 58 59 | Union: "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F" 60 61 62definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) where 63 \<comment> \<open>visible version of the LEADS-TO relation\<close> 64 "A leadsTo B == {F. (A,B) \<in> leads F}" 65 66definition wlt :: "['a program, 'a set] => 'a set" where 67 \<comment> \<open>predicate transformer: the largest set that leads to \<^term>\<open>B\<close>\<close> 68 "wlt F B == \<Union>{A. F \<in> A leadsTo B}" 69 70notation leadsTo (infixl "\<longmapsto>" 60) 71 72 73subsection\<open>transient\<close> 74 75lemma stable_transient: 76 "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)" 77apply (simp add: stable_def constrains_def transient_def, clarify) 78apply (rule rev_bexI, auto) 79done 80 81lemma stable_transient_empty: 82 "[| F \<in> stable A; F \<in> transient A; all_total F |] ==> A = {}" 83apply (drule stable_transient, assumption) 84apply (simp add: all_total_def) 85done 86 87lemma transient_strengthen: 88 "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B" 89apply (unfold transient_def, clarify) 90apply (blast intro!: rev_bexI) 91done 92 93lemma transientI: 94 "[| act \<in> Acts F; act``A \<subseteq> -A |] ==> F \<in> transient A" 95by (unfold transient_def, blast) 96 97lemma transientE: 98 "[| F \<in> transient A; 99 \<And>act. [| act \<in> Acts F; act``A \<subseteq> -A |] ==> P |] 100 ==> P" 101by (unfold transient_def, blast) 102 103lemma transient_empty [simp]: "transient {} = UNIV" 104by (unfold transient_def, auto) 105 106 107text\<open>This equation recovers the notion of weak fairness. A totalized 108 program satisfies a transient assertion just if the original program 109 contains a suitable action that is also enabled.\<close> 110lemma totalize_transient_iff: 111 "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)" 112apply (simp add: totalize_def totalize_act_def transient_def 113 Un_Image, safe) 114apply (blast intro!: rev_bexI)+ 115done 116 117lemma totalize_transientI: 118 "[| act \<in> Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] 119 ==> totalize F \<in> transient A" 120by (simp add: totalize_transient_iff, blast) 121 122subsection\<open>ensures\<close> 123 124lemma ensuresI: 125 "[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B" 126by (unfold ensures_def, blast) 127 128lemma ensuresD: 129 "F \<in> A ensures B ==> F \<in> (A-B) co (A \<union> B) & F \<in> transient (A-B)" 130by (unfold ensures_def, blast) 131 132lemma ensures_weaken_R: 133 "[| F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'" 134apply (unfold ensures_def) 135apply (blast intro: constrains_weaken transient_strengthen) 136done 137 138text\<open>The L-version (precondition strengthening) fails, but we have this\<close> 139lemma stable_ensures_Int: 140 "[| F \<in> stable C; F \<in> A ensures B |] 141 ==> F \<in> (C \<inter> A) ensures (C \<inter> B)" 142apply (unfold ensures_def) 143apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) 144prefer 2 apply (blast intro: transient_strengthen) 145apply (blast intro: stable_constrains_Int constrains_weaken) 146done 147 148lemma stable_transient_ensures: 149 "[| F \<in> stable A; F \<in> transient C; A \<subseteq> B \<union> C |] ==> F \<in> A ensures B" 150apply (simp add: ensures_def stable_def) 151apply (blast intro: constrains_weaken transient_strengthen) 152done 153 154lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)" 155by (simp (no_asm) add: ensures_def unless_def) 156 157 158subsection\<open>leadsTo\<close> 159 160lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B" 161apply (unfold leadsTo_def) 162apply (blast intro: leads.Basis) 163done 164 165lemma leadsTo_Trans: 166 "[| F \<in> A leadsTo B; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C" 167apply (unfold leadsTo_def) 168apply (blast intro: leads.Trans) 169done 170 171lemma leadsTo_Basis': 172 "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B" 173apply (drule_tac B = "A-B" in constrains_weaken_L) 174apply (drule_tac [2] B = "A-B" in transient_strengthen) 175apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) 176apply (blast+) 177done 178 179lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)" 180by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) 181 182text\<open>Useful with cancellation, disjunction\<close> 183lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'" 184by (simp add: Un_ac) 185 186lemma leadsTo_Un_duplicate2: 187 "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)" 188by (simp add: Un_ac) 189 190text\<open>The Union introduction rule as we should have liked to state it\<close> 191lemma leadsTo_Union: 192 "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B" 193apply (unfold leadsTo_def) 194apply (blast intro: leads.Union) 195done 196 197lemma leadsTo_Union_Int: 198 "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (\<Union>S \<inter> C) leadsTo B" 199apply (unfold leadsTo_def) 200apply (simp only: Int_Union_Union) 201apply (blast intro: leads.Union) 202done 203 204lemma leadsTo_UN: 205 "(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B" 206apply (blast intro: leadsTo_Union) 207done 208 209text\<open>Binary union introduction rule\<close> 210lemma leadsTo_Un: 211 "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C" 212 using leadsTo_Union [of "{A, B}" F C] by auto 213 214lemma single_leadsTo_I: 215 "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B" 216by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) 217 218 219text\<open>The INDUCTION rule as we should have liked to state it\<close> 220lemma leadsTo_induct: 221 "[| F \<in> za leadsTo zb; 222 !!A B. F \<in> A ensures B ==> P A B; 223 !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |] 224 ==> P A C; 225 !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (\<Union>S) B 226 |] ==> P za zb" 227apply (unfold leadsTo_def) 228apply (drule CollectD, erule leads.induct) 229apply (blast+) 230done 231 232 233lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B" 234by (unfold ensures_def constrains_def transient_def, blast) 235 236lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis] 237 238lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo] 239 240lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, simp] 241 242lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, simp] 243 244 245 246(** Variant induction rule: on the preconditions for B **) 247 248text\<open>Lemma is the weak version: can't see how to do it in one step\<close> 249lemma leadsTo_induct_pre_lemma: 250 "[| F \<in> za leadsTo zb; 251 P zb; 252 !!A B. [| F \<in> A ensures B; P B |] ==> P A; 253 !!S. \<forall>A \<in> S. P A ==> P (\<Union>S) 254 |] ==> P za" 255txt\<open>by induction on this formula\<close> 256apply (subgoal_tac "P zb --> P za") 257txt\<open>now solve first subgoal: this formula is sufficient\<close> 258apply (blast intro: leadsTo_refl) 259apply (erule leadsTo_induct) 260apply (blast+) 261done 262 263lemma leadsTo_induct_pre: 264 "[| F \<in> za leadsTo zb; 265 P zb; 266 !!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P B |] ==> P A; 267 !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (\<Union>S) 268 |] ==> P za" 269apply (subgoal_tac "F \<in> za leadsTo zb & P za") 270apply (erule conjunct2) 271apply (erule leadsTo_induct_pre_lemma) 272prefer 3 apply (blast intro: leadsTo_Union) 273prefer 2 apply (blast intro: leadsTo_Trans) 274apply (blast intro: leadsTo_refl) 275done 276 277 278lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'" 279by (blast intro: subset_imp_leadsTo leadsTo_Trans) 280 281lemma leadsTo_weaken_L: 282 "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'" 283by (blast intro: leadsTo_Trans subset_imp_leadsTo) 284 285text\<open>Distributes over binary unions\<close> 286lemma leadsTo_Un_distrib: 287 "F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)" 288by (blast intro: leadsTo_Un leadsTo_weaken_L) 289 290lemma leadsTo_UN_distrib: 291 "F \<in> (\<Union>i \<in> I. A i) leadsTo B = (\<forall>i \<in> I. F \<in> (A i) leadsTo B)" 292by (blast intro: leadsTo_UN leadsTo_weaken_L) 293 294lemma leadsTo_Union_distrib: 295 "F \<in> (\<Union>S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)" 296by (blast intro: leadsTo_Union leadsTo_weaken_L) 297 298 299lemma leadsTo_weaken: 300 "[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'" 301by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans) 302 303 304text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close> 305lemma leadsTo_Diff: 306 "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C" 307by (blast intro: leadsTo_Un leadsTo_weaken) 308 309lemma leadsTo_UN_UN: 310 "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i)) 311 ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)" 312apply (blast intro: leadsTo_Union leadsTo_weaken_R) 313done 314 315text\<open>Binary union version\<close> 316lemma leadsTo_Un_Un: 317 "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |] 318 ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')" 319by (blast intro: leadsTo_Un leadsTo_weaken_R) 320 321 322(** The cancellation law **) 323 324lemma leadsTo_cancel2: 325 "[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |] 326 ==> F \<in> A leadsTo (A' \<union> B')" 327by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans) 328 329lemma leadsTo_cancel_Diff2: 330 "[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |] 331 ==> F \<in> A leadsTo (A' \<union> B')" 332apply (rule leadsTo_cancel2) 333prefer 2 apply assumption 334apply (simp_all (no_asm_simp)) 335done 336 337lemma leadsTo_cancel1: 338 "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |] 339 ==> F \<in> A leadsTo (B' \<union> A')" 340apply (simp add: Un_commute) 341apply (blast intro!: leadsTo_cancel2) 342done 343 344lemma leadsTo_cancel_Diff1: 345 "[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |] 346 ==> F \<in> A leadsTo (B' \<union> A')" 347apply (rule leadsTo_cancel1) 348prefer 2 apply assumption 349apply (simp_all (no_asm_simp)) 350done 351 352 353text\<open>The impossibility law\<close> 354lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}" 355apply (erule leadsTo_induct_pre) 356apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify) 357apply (drule bspec, assumption)+ 358apply blast 359done 360 361subsection\<open>PSP: Progress-Safety-Progress\<close> 362 363text\<open>Special case of PSP: Misra's "stable conjunction"\<close> 364lemma psp_stable: 365 "[| F \<in> A leadsTo A'; F \<in> stable B |] 366 ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)" 367apply (unfold stable_def) 368apply (erule leadsTo_induct) 369prefer 3 apply (blast intro: leadsTo_Union_Int) 370prefer 2 apply (blast intro: leadsTo_Trans) 371apply (rule leadsTo_Basis) 372apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric]) 373apply (blast intro: transient_strengthen constrains_Int) 374done 375 376lemma psp_stable2: 377 "[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')" 378by (simp add: psp_stable Int_ac) 379 380lemma psp_ensures: 381 "[| F \<in> A ensures A'; F \<in> B co B' |] 382 ==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))" 383apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*) 384apply (blast intro: transient_strengthen) 385done 386 387lemma psp: 388 "[| F \<in> A leadsTo A'; F \<in> B co B' |] 389 ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))" 390apply (erule leadsTo_induct) 391 prefer 3 apply (blast intro: leadsTo_Union_Int) 392 txt\<open>Basis case\<close> 393 apply (blast intro: psp_ensures) 394txt\<open>Transitivity case has a delicate argument involving "cancellation"\<close> 395apply (rule leadsTo_Un_duplicate2) 396apply (erule leadsTo_cancel_Diff1) 397apply (simp add: Int_Diff Diff_triv) 398apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset) 399done 400 401lemma psp2: 402 "[| F \<in> A leadsTo A'; F \<in> B co B' |] 403 ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))" 404by (simp (no_asm_simp) add: psp Int_ac) 405 406lemma psp_unless: 407 "[| F \<in> A leadsTo A'; F \<in> B unless B' |] 408 ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')" 409 410apply (unfold unless_def) 411apply (drule psp, assumption) 412apply (blast intro: leadsTo_weaken) 413done 414 415 416subsection\<open>Proving the induction rules\<close> 417 418(** The most general rule: r is any wf relation; f is any variant function **) 419 420lemma leadsTo_wf_induct_lemma: 421 "[| wf r; 422 \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo 423 ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |] 424 ==> F \<in> (A \<inter> f-`{m}) leadsTo B" 425apply (erule_tac a = m in wf_induct) 426apply (subgoal_tac "F \<in> (A \<inter> (f -` (r\<inverse> `` {x}))) leadsTo B") 427 apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) 428apply (subst vimage_eq_UN) 429apply (simp only: UN_simps [symmetric]) 430apply (blast intro: leadsTo_UN) 431done 432 433 434(** Meta or object quantifier ? **) 435lemma leadsTo_wf_induct: 436 "[| wf r; 437 \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo 438 ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |] 439 ==> F \<in> A leadsTo B" 440apply (rule_tac t = A in subst) 441 defer 1 442 apply (rule leadsTo_UN) 443 apply (erule leadsTo_wf_induct_lemma) 444 apply assumption 445apply fast (*Blast_tac: Function unknown's argument not a parameter*) 446done 447 448 449lemma bounded_induct: 450 "[| wf r; 451 \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo 452 ((A \<inter> f-`(r\<inverse> `` {m})) \<union> B) |] 453 ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)" 454apply (erule leadsTo_wf_induct, safe) 455apply (case_tac "m \<in> I") 456apply (blast intro: leadsTo_weaken) 457apply (blast intro: subset_imp_leadsTo) 458done 459 460 461(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*) 462lemma lessThan_induct: 463 "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..<m}) \<union> B) |] 464 ==> F \<in> A leadsTo B" 465apply (rule wf_less_than [THEN leadsTo_wf_induct]) 466apply (simp (no_asm_simp)) 467apply blast 468done 469 470lemma lessThan_bounded_induct: 471 "!!l::nat. [| \<forall>m \<in> greaterThan l. 472 F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |] 473 ==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)" 474apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) 475apply (rule wf_less_than [THEN bounded_induct]) 476apply (simp (no_asm_simp)) 477done 478 479lemma greaterThan_bounded_induct: 480 "(!!l::nat. \<forall>m \<in> lessThan l. 481 F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)) 482 ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)" 483apply (rule_tac f = f and f1 = "%k. l - k" 484 in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct]) 485apply (simp (no_asm) add:Image_singleton) 486apply clarify 487apply (case_tac "m<l") 488 apply (blast intro: leadsTo_weaken_R diff_less_mono2) 489apply (blast intro: not_le_imp_less subset_imp_leadsTo) 490done 491 492 493subsection\<open>wlt\<close> 494 495text\<open>Misra's property W3\<close> 496lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B" 497apply (unfold wlt_def) 498apply (blast intro!: leadsTo_Union) 499done 500 501lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B" 502apply (unfold wlt_def) 503apply (blast intro!: leadsTo_Union) 504done 505 506text\<open>Misra's property W2\<close> 507lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)" 508by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) 509 510text\<open>Misra's property W4\<close> 511lemma wlt_increasing: "B \<subseteq> wlt F B" 512apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) 513done 514 515 516text\<open>Used in the Trans case below\<close> 517lemma lemma1: 518 "[| B \<subseteq> A2; 519 F \<in> (A1 - B) co (A1 \<union> B); 520 F \<in> (A2 - C) co (A2 \<union> C) |] 521 ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)" 522by (unfold constrains_def, clarify, blast) 523 524text\<open>Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"\<close> 525lemma leadsTo_123: 526 "F \<in> A leadsTo A' 527 ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')" 528apply (erule leadsTo_induct) 529 txt\<open>Basis\<close> 530 apply (blast dest: ensuresD) 531 txt\<open>Trans\<close> 532 apply clarify 533 apply (rule_tac x = "Ba \<union> Bb" in exI) 534 apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) 535txt\<open>Union\<close> 536apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) 537apply (rule_tac x = "\<Union>A \<in> S. f A" in exI) 538apply (auto intro: leadsTo_UN) 539(*Blast_tac says PROOF FAILED*) 540apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B" 541 in constrains_UN [THEN constrains_weaken], auto) 542done 543 544 545text\<open>Misra's property W5\<close> 546lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)" 547proof - 548 from wlt_leadsTo [of F B, THEN leadsTo_123] 549 show ?thesis 550 proof (elim exE conjE) 551(* assumes have to be in exactly the form as in the goal displayed at 552 this point. Isar doesn't give you any automation. *) 553 fix C 554 assume wlt: "wlt F B \<subseteq> C" 555 and lt: "F \<in> C leadsTo B" 556 and co: "F \<in> C - B co C \<union> B" 557 have eq: "C = wlt F B" 558 proof - 559 from lt and wlt show ?thesis 560 by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1]) 561 qed 562 from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2) 563 qed 564qed 565 566 567subsection\<open>Completion: Binary and General Finite versions\<close> 568 569lemma completion_lemma : 570 "[| W = wlt F (B' \<union> C); 571 F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C); 572 F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) |] 573 ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)" 574apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ") 575 prefer 2 576 apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 577 THEN constrains_weaken]) 578apply (subgoal_tac "F \<in> (W-C) co W") 579 prefer 2 580 apply (simp add: wlt_increasing Un_assoc Un_absorb2) 581apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ") 582 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) 583(** LEVEL 6 **) 584apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ") 585 prefer 2 586 apply (rule leadsTo_Un_duplicate2) 587 apply (blast intro: leadsTo_Un_Un wlt_leadsTo 588 [THEN psp2, THEN leadsTo_weaken] leadsTo_refl) 589apply (drule leadsTo_Diff) 590apply (blast intro: subset_imp_leadsTo) 591apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W") 592 prefer 2 593 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) 594apply (blast intro: leadsTo_Trans subset_imp_leadsTo) 595done 596 597lemmas completion = completion_lemma [OF refl] 598 599lemma finite_completion_lemma: 600 "finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) --> 601 (\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) --> 602 F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 603apply (erule finite_induct, auto) 604apply (rule completion) 605 prefer 4 606 apply (simp only: INT_simps [symmetric]) 607 apply (rule constrains_INT, auto) 608done 609 610lemma finite_completion: 611 "[| finite I; 612 !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C); 613 !!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |] 614 ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" 615by (blast intro: finite_completion_lemma [THEN mp, THEN mp]) 616 617lemma stable_completion: 618 "[| F \<in> A leadsTo A'; F \<in> stable A'; 619 F \<in> B leadsTo B'; F \<in> stable B' |] 620 ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')" 621apply (unfold stable_def) 622apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R]) 623apply (force+) 624done 625 626lemma finite_stable_completion: 627 "[| finite I; 628 !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i); 629 !!i. i \<in> I ==> F \<in> stable (A' i) |] 630 ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)" 631apply (unfold stable_def) 632apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R]) 633apply (simp_all (no_asm_simp)) 634apply blast+ 635done 636 637end 638