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