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