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