src/HOL/UNITY/WFair.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 37936 1e4c5015a72e
child 44106 0e018cbcc0de
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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 apply (subst Un_eq_Union)
   215 apply (blast intro: leadsTo_Union)
   216 done
   217 
   218 lemma single_leadsTo_I: 
   219      "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
   220 by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
   221 
   222 
   223 text{*The INDUCTION rule as we should have liked to state it*}
   224 lemma leadsTo_induct: 
   225   "[| F \<in> za leadsTo zb;   
   226       !!A B. F \<in> A ensures B ==> P A B;  
   227       !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]  
   228                ==> P A C;  
   229       !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B  
   230    |] ==> P za zb"
   231 apply (unfold leadsTo_def)
   232 apply (drule CollectD, erule leads.induct)
   233 apply (blast+)
   234 done
   235 
   236 
   237 lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
   238 by (unfold ensures_def constrains_def transient_def, blast)
   239 
   240 lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
   241 
   242 lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
   243 
   244 lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
   245 
   246 lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
   247 
   248 
   249 
   250 (** Variant induction rule: on the preconditions for B **)
   251 
   252 text{*Lemma is the weak version: can't see how to do it in one step*}
   253 lemma leadsTo_induct_pre_lemma: 
   254   "[| F \<in> za leadsTo zb;   
   255       P zb;  
   256       !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
   257       !!S. \<forall>A \<in> S. P A ==> P (Union S)  
   258    |] ==> P za"
   259 txt{*by induction on this formula*}
   260 apply (subgoal_tac "P zb --> P za")
   261 txt{*now solve first subgoal: this formula is sufficient*}
   262 apply (blast intro: leadsTo_refl)
   263 apply (erule leadsTo_induct)
   264 apply (blast+)
   265 done
   266 
   267 lemma leadsTo_induct_pre: 
   268   "[| F \<in> za leadsTo zb;   
   269       P zb;  
   270       !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P B |] ==> P A;  
   271       !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)  
   272    |] ==> P za"
   273 apply (subgoal_tac "F \<in> za leadsTo zb & P za")
   274 apply (erule conjunct2)
   275 apply (erule leadsTo_induct_pre_lemma)
   276 prefer 3 apply (blast intro: leadsTo_Union)
   277 prefer 2 apply (blast intro: leadsTo_Trans)
   278 apply (blast intro: leadsTo_refl)
   279 done
   280 
   281 
   282 lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
   283 by (blast intro: subset_imp_leadsTo leadsTo_Trans)
   284 
   285 lemma leadsTo_weaken_L [rule_format]:
   286      "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
   287 by (blast intro: leadsTo_Trans subset_imp_leadsTo)
   288 
   289 text{*Distributes over binary unions*}
   290 lemma leadsTo_Un_distrib:
   291      "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
   292 by (blast intro: leadsTo_Un leadsTo_weaken_L)
   293 
   294 lemma leadsTo_UN_distrib:
   295      "F \<in> (\<Union>i \<in> I. A i) leadsTo B  =  (\<forall>i \<in> I. F \<in> (A i) leadsTo B)"
   296 by (blast intro: leadsTo_UN leadsTo_weaken_L)
   297 
   298 lemma leadsTo_Union_distrib:
   299      "F \<in> (Union S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
   300 by (blast intro: leadsTo_Union leadsTo_weaken_L)
   301 
   302 
   303 lemma leadsTo_weaken:
   304      "[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'"
   305 by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
   306 
   307 
   308 text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
   309 lemma leadsTo_Diff:
   310      "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
   311 by (blast intro: leadsTo_Un leadsTo_weaken)
   312 
   313 lemma leadsTo_UN_UN:
   314    "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))  
   315     ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
   316 apply (simp only: Union_image_eq [symmetric])
   317 apply (blast intro: leadsTo_Union leadsTo_weaken_R)
   318 done
   319 
   320 text{*Binary union version*}
   321 lemma leadsTo_Un_Un:
   322      "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]  
   323       ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
   324 by (blast intro: leadsTo_Un leadsTo_weaken_R)
   325 
   326 
   327 (** The cancellation law **)
   328 
   329 lemma leadsTo_cancel2:
   330      "[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |]  
   331       ==> F \<in> A leadsTo (A' \<union> B')"
   332 by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
   333 
   334 lemma leadsTo_cancel_Diff2:
   335      "[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |]  
   336       ==> F \<in> A leadsTo (A' \<union> B')"
   337 apply (rule leadsTo_cancel2)
   338 prefer 2 apply assumption
   339 apply (simp_all (no_asm_simp))
   340 done
   341 
   342 lemma leadsTo_cancel1:
   343      "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |]  
   344     ==> F \<in> A leadsTo (B' \<union> A')"
   345 apply (simp add: Un_commute)
   346 apply (blast intro!: leadsTo_cancel2)
   347 done
   348 
   349 lemma leadsTo_cancel_Diff1:
   350      "[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |]  
   351     ==> F \<in> A leadsTo (B' \<union> A')"
   352 apply (rule leadsTo_cancel1)
   353 prefer 2 apply assumption
   354 apply (simp_all (no_asm_simp))
   355 done
   356 
   357 
   358 text{*The impossibility law*}
   359 lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
   360 apply (erule leadsTo_induct_pre)
   361 apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
   362 apply (drule bspec, assumption)+
   363 apply blast
   364 done
   365 
   366 subsection{*PSP: Progress-Safety-Progress*}
   367 
   368 text{*Special case of PSP: Misra's "stable conjunction"*}
   369 lemma psp_stable: 
   370    "[| F \<in> A leadsTo A'; F \<in> stable B |]  
   371     ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
   372 apply (unfold stable_def)
   373 apply (erule leadsTo_induct)
   374 prefer 3 apply (blast intro: leadsTo_Union_Int)
   375 prefer 2 apply (blast intro: leadsTo_Trans)
   376 apply (rule leadsTo_Basis)
   377 apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
   378 apply (blast intro: transient_strengthen constrains_Int)
   379 done
   380 
   381 lemma psp_stable2: 
   382    "[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')"
   383 by (simp add: psp_stable Int_ac)
   384 
   385 lemma psp_ensures: 
   386    "[| F \<in> A ensures A'; F \<in> B co B' |]  
   387     ==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
   388 apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
   389 apply (blast intro: transient_strengthen)
   390 done
   391 
   392 lemma psp:
   393      "[| F \<in> A leadsTo A'; F \<in> B co B' |]  
   394       ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
   395 apply (erule leadsTo_induct)
   396   prefer 3 apply (blast intro: leadsTo_Union_Int)
   397  txt{*Basis case*}
   398  apply (blast intro: psp_ensures)
   399 txt{*Transitivity case has a delicate argument involving "cancellation"*}
   400 apply (rule leadsTo_Un_duplicate2)
   401 apply (erule leadsTo_cancel_Diff1)
   402 apply (simp add: Int_Diff Diff_triv)
   403 apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
   404 done
   405 
   406 lemma psp2:
   407      "[| F \<in> A leadsTo A'; F \<in> B co B' |]  
   408     ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
   409 by (simp (no_asm_simp) add: psp Int_ac)
   410 
   411 lemma psp_unless: 
   412    "[| F \<in> A leadsTo A';  F \<in> B unless B' |]  
   413     ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
   414 
   415 apply (unfold unless_def)
   416 apply (drule psp, assumption)
   417 apply (blast intro: leadsTo_weaken)
   418 done
   419 
   420 
   421 subsection{*Proving the induction rules*}
   422 
   423 (** The most general rule: r is any wf relation; f is any variant function **)
   424 
   425 lemma leadsTo_wf_induct_lemma:
   426      "[| wf r;      
   427          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
   428                     ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   429       ==> F \<in> (A \<inter> f-`{m}) leadsTo B"
   430 apply (erule_tac a = m in wf_induct)
   431 apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B")
   432  apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
   433 apply (subst vimage_eq_UN)
   434 apply (simp only: UN_simps [symmetric])
   435 apply (blast intro: leadsTo_UN)
   436 done
   437 
   438 
   439 (** Meta or object quantifier ? **)
   440 lemma leadsTo_wf_induct:
   441      "[| wf r;      
   442          \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
   443                     ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   444       ==> F \<in> A leadsTo B"
   445 apply (rule_tac t = A in subst)
   446  defer 1
   447  apply (rule leadsTo_UN)
   448  apply (erule leadsTo_wf_induct_lemma)
   449  apply assumption
   450 apply fast (*Blast_tac: Function unknown's argument not a parameter*)
   451 done
   452 
   453 
   454 lemma bounded_induct:
   455      "[| wf r;      
   456          \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo                    
   457                       ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   458       ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)"
   459 apply (erule leadsTo_wf_induct, safe)
   460 apply (case_tac "m \<in> I")
   461 apply (blast intro: leadsTo_weaken)
   462 apply (blast intro: subset_imp_leadsTo)
   463 done
   464 
   465 
   466 (*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
   467 lemma lessThan_induct: 
   468      "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..<m}) \<union> B) |]  
   469       ==> F \<in> A leadsTo B"
   470 apply (rule wf_less_than [THEN leadsTo_wf_induct])
   471 apply (simp (no_asm_simp))
   472 apply blast
   473 done
   474 
   475 lemma lessThan_bounded_induct:
   476      "!!l::nat. [| \<forall>m \<in> greaterThan l.     
   477             F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |]  
   478       ==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
   479 apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
   480 apply (rule wf_less_than [THEN bounded_induct])
   481 apply (simp (no_asm_simp))
   482 done
   483 
   484 lemma greaterThan_bounded_induct:
   485      "(!!l::nat. \<forall>m \<in> lessThan l.     
   486                  F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B))
   487       ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
   488 apply (rule_tac f = f and f1 = "%k. l - k" 
   489        in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
   490 apply (simp (no_asm) add:Image_singleton)
   491 apply clarify
   492 apply (case_tac "m<l")
   493  apply (blast intro: leadsTo_weaken_R diff_less_mono2)
   494 apply (blast intro: not_leE subset_imp_leadsTo)
   495 done
   496 
   497 
   498 subsection{*wlt*}
   499 
   500 text{*Misra's property W3*}
   501 lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
   502 apply (unfold wlt_def)
   503 apply (blast intro!: leadsTo_Union)
   504 done
   505 
   506 lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B"
   507 apply (unfold wlt_def)
   508 apply (blast intro!: leadsTo_Union)
   509 done
   510 
   511 text{*Misra's property W2*}
   512 lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
   513 by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
   514 
   515 text{*Misra's property W4*}
   516 lemma wlt_increasing: "B \<subseteq> wlt F B"
   517 apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
   518 done
   519 
   520 
   521 text{*Used in the Trans case below*}
   522 lemma lemma1: 
   523    "[| B \<subseteq> A2;   
   524        F \<in> (A1 - B) co (A1 \<union> B);  
   525        F \<in> (A2 - C) co (A2 \<union> C) |]  
   526     ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
   527 by (unfold constrains_def, clarify,  blast)
   528 
   529 text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
   530 lemma leadsTo_123:
   531      "F \<in> A leadsTo A'  
   532       ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
   533 apply (erule leadsTo_induct)
   534   txt{*Basis*}
   535   apply (blast dest: ensuresD)
   536  txt{*Trans*}
   537  apply clarify
   538  apply (rule_tac x = "Ba \<union> Bb" in exI)
   539  apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
   540 txt{*Union*}
   541 apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
   542 apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
   543 apply (auto intro: leadsTo_UN)
   544 (*Blast_tac says PROOF FAILED*)
   545 apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B" 
   546        in constrains_UN [THEN constrains_weaken], auto) 
   547 done
   548 
   549 
   550 text{*Misra's property W5*}
   551 lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
   552 proof -
   553   from wlt_leadsTo [of F B, THEN leadsTo_123]
   554   show ?thesis
   555   proof (elim exE conjE)
   556 (* assumes have to be in exactly the form as in the goal displayed at
   557    this point.  Isar doesn't give you any automation. *)
   558     fix C
   559     assume wlt: "wlt F B \<subseteq> C"
   560        and lt:  "F \<in> C leadsTo B"
   561        and co:  "F \<in> C - B co C \<union> B"
   562     have eq: "C = wlt F B"
   563     proof -
   564       from lt and wlt show ?thesis 
   565            by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
   566     qed
   567     from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
   568   qed
   569 qed
   570 
   571 
   572 subsection{*Completion: Binary and General Finite versions*}
   573 
   574 lemma completion_lemma :
   575      "[| W = wlt F (B' \<union> C);      
   576        F \<in> A leadsTo (A' \<union> C);  F \<in> A' co (A' \<union> C);    
   577        F \<in> B leadsTo (B' \<union> C);  F \<in> B' co (B' \<union> C) |]  
   578     ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
   579 apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ")
   580  prefer 2
   581  apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 
   582                                          THEN constrains_weaken])
   583 apply (subgoal_tac "F \<in> (W-C) co W")
   584  prefer 2
   585  apply (simp add: wlt_increasing Un_assoc Un_absorb2)
   586 apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
   587  prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
   588 (** LEVEL 6 **)
   589 apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
   590  prefer 2
   591  apply (rule leadsTo_Un_duplicate2)
   592  apply (blast intro: leadsTo_Un_Un wlt_leadsTo
   593                          [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
   594 apply (drule leadsTo_Diff)
   595 apply (blast intro: subset_imp_leadsTo)
   596 apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")
   597  prefer 2
   598  apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
   599 apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
   600 done
   601 
   602 lemmas completion = completion_lemma [OF refl]
   603 
   604 lemma finite_completion_lemma:
   605      "finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) -->   
   606                    (\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) -->  
   607                    F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   608 apply (erule finite_induct, auto)
   609 apply (rule completion)
   610    prefer 4
   611    apply (simp only: INT_simps [symmetric])
   612    apply (rule constrains_INT, auto)
   613 done
   614 
   615 lemma finite_completion: 
   616      "[| finite I;   
   617          !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C);  
   618          !!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |]    
   619       ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   620 by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
   621 
   622 lemma stable_completion: 
   623      "[| F \<in> A leadsTo A';  F \<in> stable A';    
   624          F \<in> B leadsTo B';  F \<in> stable B' |]  
   625     ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
   626 apply (unfold stable_def)
   627 apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
   628 apply (force+)
   629 done
   630 
   631 lemma finite_stable_completion: 
   632      "[| finite I;   
   633          !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i);  
   634          !!i. i \<in> I ==> F \<in> stable (A' i) |]    
   635       ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)"
   636 apply (unfold stable_def)
   637 apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
   638 apply (simp_all (no_asm_simp))
   639 apply blast+
   640 done
   641 
   642 end