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