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