# Theory WFair

Up to index of Isabelle/HOL/UNITY

theory WFair
imports UNITY
begin

    (*  Title:      HOL/UNITY/WFair
        ID:         $Id: WFair.thy,v 1.25 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Conditional Fairness versions of transient, ensures, leadsTo.

    From Misra, "A Logic for Concurrent Programming", 1994
    *)

    header{*Progress*}

    theory WFair imports UNITY begin

    text{*The original version of this theory was based on weak fairness.  (Thus,
    the entire UNITY development embodied this assumption, until February 2003.)
    Weak fairness states that if a command is enabled continuously, then it is
    eventually executed.  Ernie Cohen suggested that I instead adopt unconditional
    fairness: every command is executed infinitely often.

    In fact, Misra's paper on "Progress" seems to be ambiguous about the correct
    interpretation, and says that the two forms of fairness are equivalent.  They
    differ only on their treatment of partial transitions, which under
    unconditional fairness behave magically.  That is because if there are partial
    transitions then there may be no fair executions, making all leads-to
    properties hold vacuously.

    Unconditional fairness has some great advantages.  By distinguishing partial
    transitions from total ones that are the identity on part of their domain, it
    is more expressive.  Also, by simplifying the definition of the transient
    property, it simplifies many proofs.  A drawback is that some laws only hold
    under the assumption that all transitions are total.  The best-known of these
    is the impossibility law for leads-to.
    *}

    constdefs

      --{*This definition specifies conditional fairness.  The rest of the theory
          is generic to all forms of fairness.  To get weak fairness, conjoin
          the inclusion below with @{term "A ⊆ Domain act"}, which specifies
          that the action is enabled over all of @{term A}.*}
      transient :: "'a set => 'a program set"
        "transient A == {F. ∃act∈Acts F. act``A ⊆ -A}"

      ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
        "A ensures B == (A-B co A ∪ B) ∩ transient (A-B)"

    consts

      leads :: "'a program => ('a set * 'a set) set"
        --{*LEADS-TO constant for the inductive definition*}

    inductive "leads F"
      intros

        Basis:  "F ∈ A ensures B ==> (A,B) ∈ leads F"

        Trans:  "[| (A,B) ∈ leads F;  (B,C) ∈ leads F |] ==> (A,C) ∈ leads F"

        Union:  "∀A ∈ S. (A,B) ∈ leads F ==> (Union S, B) ∈ leads F"

    constdefs

      leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
         --{*visible version of the LEADS-TO relation*}
        "A leadsTo B == {F. (A,B) ∈ leads F}"

      wlt :: "['a program, 'a set] => 'a set"
         --{*predicate transformer: the largest set that leads to @{term B}*}
        "wlt F B == Union {A. F ∈ A leadsTo B}"

    syntax (xsymbols)
      "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)

    subsection{*transient*}

    lemma stable_transient:
        "[| F ∈ stable A; F ∈ transient A |] ==> ∃act∈Acts F. A ⊆ - (Domain act)"
    apply (simp add: stable_def constrains_def transient_def, clarify)
    apply (rule rev_bexI, auto)
    done

    lemma stable_transient_empty:
        "[| F ∈ stable A; F ∈ transient A; all_total F |] ==> A = {}"
    apply (drule stable_transient, assumption)
    apply (simp add: all_total_def)
    done

    lemma transient_strengthen:
        "[| F ∈ transient A; B ⊆ A |] ==> F ∈ transient B"
    apply (unfold transient_def, clarify)
    apply (blast intro!: rev_bexI)
    done

    lemma transientI:
        "[| act: Acts F;  act``A ⊆ -A |] ==> F ∈ transient A"
    by (unfold transient_def, blast)

    lemma transientE:
        "[| F ∈ transient A;
            !!act. [| act: Acts F;  act``A ⊆ -A |] ==> P |]
         ==> P"
    by (unfold transient_def, blast)

    lemma transient_empty [simp]: "transient {} = UNIV"
    by (unfold transient_def, auto)

    text{*This equation recovers the notion of weak fairness.  A totalized
          program satisfies a transient assertion just if the original program
          contains a suitable action that is also enabled.*}
    lemma totalize_transient_iff:
       "(totalize F ∈ transient A) = (∃act∈Acts F. A ⊆ Domain act & act``A ⊆ -A)"
    apply (simp add: totalize_def totalize_act_def transient_def
                     Un_Image Un_subset_iff, safe)
    apply (blast intro!: rev_bexI)+
    done

    lemma totalize_transientI:
        "[| act: Acts F;  A ⊆ Domain act;  act``A ⊆ -A |]
         ==> totalize F ∈ transient A"
    by (simp add: totalize_transient_iff, blast)

    subsection{*ensures*}

    lemma ensuresI:
        "[| F ∈ (A-B) co (A ∪ B); F ∈ transient (A-B) |] ==> F ∈ A ensures B"
    by (unfold ensures_def, blast)

    lemma ensuresD:
        "F ∈ A ensures B ==> F ∈ (A-B) co (A ∪ B) & F ∈ transient (A-B)"
    by (unfold ensures_def, blast)

    lemma ensures_weaken_R:
        "[| F ∈ A ensures A'; A'<=B' |] ==> F ∈ A ensures B'"
    apply (unfold ensures_def)
    apply (blast intro: constrains_weaken transient_strengthen)
    done

    text{*The L-version (precondition strengthening) fails, but we have this*}
    lemma stable_ensures_Int:
        "[| F ∈ stable C;  F ∈ A ensures B |]
        ==> F ∈ (C ∩ A) ensures (C ∩ B)"
    apply (unfold ensures_def)
    apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
    prefer 2 apply (blast intro: transient_strengthen)
    apply (blast intro: stable_constrains_Int constrains_weaken)
    done

    lemma stable_transient_ensures:
         "[| F ∈ stable A;  F ∈ transient C;  A ⊆ B ∪ C |] ==> F ∈ A ensures B"
    apply (simp add: ensures_def stable_def)
    apply (blast intro: constrains_weaken transient_strengthen)
    done

    lemma ensures_eq: "(A ensures B) = (A unless B) ∩ transient (A-B)"
    by (simp (no_asm) add: ensures_def unless_def)

    subsection{*leadsTo*}

    lemma leadsTo_Basis [intro]: "F ∈ A ensures B ==> F ∈ A leadsTo B"
    apply (unfold leadsTo_def)
    apply (blast intro: leads.Basis)
    done

    lemma leadsTo_Trans:
         "[| F ∈ A leadsTo B;  F ∈ B leadsTo C |] ==> F ∈ A leadsTo C"
    apply (unfold leadsTo_def)
    apply (blast intro: leads.Trans)
    done

    lemma leadsTo_Basis':
         "[| F ∈ A co A ∪ B; F ∈ transient A |] ==> F ∈ A leadsTo B"
    apply (drule_tac B = "A-B" in constrains_weaken_L)
    apply (drule_tac [2] B = "A-B" in transient_strengthen)
    apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
    apply (blast+)
    done

    lemma transient_imp_leadsTo: "F ∈ transient A ==> F ∈ A leadsTo (-A)"
    by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)

    text{*Useful with cancellation, disjunction*}
    lemma leadsTo_Un_duplicate: "F ∈ A leadsTo (A' ∪ A') ==> F ∈ A leadsTo A'"
    by (simp add: Un_ac)

    lemma leadsTo_Un_duplicate2:
         "F ∈ A leadsTo (A' ∪ C ∪ C) ==> F ∈ A leadsTo (A' ∪ C)"
    by (simp add: Un_ac)

    text{*The Union introduction rule as we should have liked to state it*}
    lemma leadsTo_Union:
        "(!!A. A ∈ S ==> F ∈ A leadsTo B) ==> F ∈ (Union S) leadsTo B"
    apply (unfold leadsTo_def)
    apply (blast intro: leads.Union)
    done

    lemma leadsTo_Union_Int:
     "(!!A. A ∈ S ==> F ∈ (A ∩ C) leadsTo B) ==> F ∈ (Union S ∩ C) leadsTo B"
    apply (unfold leadsTo_def)
    apply (simp only: Int_Union_Union)
    apply (blast intro: leads.Union)
    done

    lemma leadsTo_UN:
        "(!!i. i ∈ I ==> F ∈ (A i) leadsTo B) ==> F ∈ (\<Union>i ∈ I. A i) leadsTo B"
    apply (subst Union_image_eq [symmetric])
    apply (blast intro: leadsTo_Union)
    done

    text{*Binary union introduction rule*}
    lemma leadsTo_Un:
         "[| F ∈ A leadsTo C; F ∈ B leadsTo C |] ==> F ∈ (A ∪ B) leadsTo C"
    apply (subst Un_eq_Union)
    apply (blast intro: leadsTo_Union)
    done

    lemma single_leadsTo_I:
         "(!!x. x ∈ A ==> F ∈ {x} leadsTo B) ==> F ∈ A leadsTo B"
    by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)

    text{*The INDUCTION rule as we should have liked to state it*}
    lemma leadsTo_induct:
      "[| F ∈ za leadsTo zb;
          !!A B. F ∈ A ensures B ==> P A B;
          !!A B C. [| F ∈ A leadsTo B; P A B; F ∈ B leadsTo C; P B C |]
                   ==> P A C;
          !!B S. ∀A ∈ S. F ∈ A leadsTo B & P A B ==> P (Union S) B
       |] ==> P za zb"
    apply (unfold leadsTo_def)
    apply (drule CollectD, erule leads.induct)
    apply (blast+)
    done

    lemma subset_imp_ensures: "A ⊆ B ==> F ∈ A ensures B"
    by (unfold ensures_def constrains_def transient_def, blast)

    lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]

    lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]

    lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]

    lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]

    (** Variant induction rule: on the preconditions for B **)

    text{*Lemma is the weak version: can't see how to do it in one step*}
    lemma leadsTo_induct_pre_lemma:
      "[| F ∈ za leadsTo zb;
          P zb;
          !!A B. [| F ∈ A ensures B;  P B |] ==> P A;
          !!S. ∀A ∈ S. P A ==> P (Union S)
       |] ==> P za"
    txt{*by induction on this formula*}
    apply (subgoal_tac "P zb --> P za")
    txt{*now solve first subgoal: this formula is sufficient*}
    apply (blast intro: leadsTo_refl)
    apply (erule leadsTo_induct)
    apply (blast+)
    done

    lemma leadsTo_induct_pre:
      "[| F ∈ za leadsTo zb;
          P zb;
          !!A B. [| F ∈ A ensures B;  F ∈ B leadsTo zb;  P B |] ==> P A;
          !!S. ∀A ∈ S. F ∈ A leadsTo zb & P A ==> P (Union S)
       |] ==> P za"
    apply (subgoal_tac "F ∈ za leadsTo zb & P za")
    apply (erule conjunct2)
    apply (erule leadsTo_induct_pre_lemma)
    prefer 3 apply (blast intro: leadsTo_Union)
    prefer 2 apply (blast intro: leadsTo_Trans)
    apply (blast intro: leadsTo_refl)
    done

    lemma leadsTo_weaken_R: "[| F ∈ A leadsTo A'; A'<=B' |] ==> F ∈ A leadsTo B'"
    by (blast intro: subset_imp_leadsTo leadsTo_Trans)

    lemma leadsTo_weaken_L [rule_format]:
         "[| F ∈ A leadsTo A'; B ⊆ A |] ==> F ∈ B leadsTo A'"
    by (blast intro: leadsTo_Trans subset_imp_leadsTo)

    text{*Distributes over binary unions*}
    lemma leadsTo_Un_distrib:
         "F ∈ (A ∪ B) leadsTo C  =  (F ∈ A leadsTo C & F ∈ B leadsTo C)"
    by (blast intro: leadsTo_Un leadsTo_weaken_L)

    lemma leadsTo_UN_distrib:
         "F ∈ (\<Union>i ∈ I. A i) leadsTo B  =  (∀i ∈ I. F ∈ (A i) leadsTo B)"
    by (blast intro: leadsTo_UN leadsTo_weaken_L)

    lemma leadsTo_Union_distrib:
         "F ∈ (Union S) leadsTo B  =  (∀A ∈ S. F ∈ A leadsTo B)"
    by (blast intro: leadsTo_Union leadsTo_weaken_L)

    lemma leadsTo_weaken:
         "[| F ∈ A leadsTo A'; B ⊆ A; A'<=B' |] ==> F ∈ B leadsTo B'"
    by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)

    text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
    lemma leadsTo_Diff:
         "[| F ∈ (A-B) leadsTo C; F ∈ B leadsTo C |]   ==> F ∈ A leadsTo C"
    by (blast intro: leadsTo_Un leadsTo_weaken)

    lemma leadsTo_UN_UN:
       "(!! i. i ∈ I ==> F ∈ (A i) leadsTo (A' i))
        ==> F ∈ (\<Union>i ∈ I. A i) leadsTo (\<Union>i ∈ I. A' i)"
    apply (simp only: Union_image_eq [symmetric])
    apply (blast intro: leadsTo_Union leadsTo_weaken_R)
    done

    text{*Binary union version*}
    lemma leadsTo_Un_Un:
         "[| F ∈ A leadsTo A'; F ∈ B leadsTo B' |]
          ==> F ∈ (A ∪ B) leadsTo (A' ∪ B')"
    by (blast intro: leadsTo_Un leadsTo_weaken_R)

    (** The cancellation law **)

    lemma leadsTo_cancel2:
         "[| F ∈ A leadsTo (A' ∪ B); F ∈ B leadsTo B' |]
          ==> F ∈ A leadsTo (A' ∪ B')"
    by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)

    lemma leadsTo_cancel_Diff2:
         "[| F ∈ A leadsTo (A' ∪ B); F ∈ (B-A') leadsTo B' |]
          ==> F ∈ A leadsTo (A' ∪ B')"
    apply (rule leadsTo_cancel2)
    prefer 2 apply assumption
    apply (simp_all (no_asm_simp))
    done

    lemma leadsTo_cancel1:
         "[| F ∈ A leadsTo (B ∪ A'); F ∈ B leadsTo B' |]
        ==> F ∈ A leadsTo (B' ∪ A')"
    apply (simp add: Un_commute)
    apply (blast intro!: leadsTo_cancel2)
    done

    lemma leadsTo_cancel_Diff1:
         "[| F ∈ A leadsTo (B ∪ A'); F ∈ (B-A') leadsTo B' |]
        ==> F ∈ A leadsTo (B' ∪ A')"
    apply (rule leadsTo_cancel1)
    prefer 2 apply assumption
    apply (simp_all (no_asm_simp))
    done

    text{*The impossibility law*}
    lemma leadsTo_empty: "[|F ∈ A leadsTo {}; all_total F|] ==> A={}"
    apply (erule leadsTo_induct_pre)
    apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
    apply (drule bspec, assumption)+
    apply blast
    done

    subsection{*PSP: Progress-Safety-Progress*}

    text{*Special case of PSP: Misra's "stable conjunction"*}
    lemma psp_stable:
       "[| F ∈ A leadsTo A'; F ∈ stable B |]
        ==> F ∈ (A ∩ B) leadsTo (A' ∩ B)"
    apply (unfold stable_def)
    apply (erule leadsTo_induct)
    prefer 3 apply (blast intro: leadsTo_Union_Int)
    prefer 2 apply (blast intro: leadsTo_Trans)
    apply (rule leadsTo_Basis)
    apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
    apply (blast intro: transient_strengthen constrains_Int)
    done

    lemma psp_stable2:
       "[| F ∈ A leadsTo A'; F ∈ stable B |] ==> F ∈ (B ∩ A) leadsTo (B ∩ A')"
    by (simp add: psp_stable Int_ac)

    lemma psp_ensures:
       "[| F ∈ A ensures A'; F ∈ B co B' |]
        ==> F ∈ (A ∩ B') ensures ((A' ∩ B) ∪ (B' - B))"
    apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
    apply (blast intro: transient_strengthen)
    done

    lemma psp:
         "[| F ∈ A leadsTo A'; F ∈ B co B' |]
          ==> F ∈ (A ∩ B') leadsTo ((A' ∩ B) ∪ (B' - B))"
    apply (erule leadsTo_induct)
      prefer 3 apply (blast intro: leadsTo_Union_Int)
     txt{*Basis case*}
     apply (blast intro: psp_ensures)
    txt{*Transitivity case has a delicate argument involving "cancellation"*}
    apply (rule leadsTo_Un_duplicate2)
    apply (erule leadsTo_cancel_Diff1)
    apply (simp add: Int_Diff Diff_triv)
    apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
    done

    lemma psp2:
         "[| F ∈ A leadsTo A'; F ∈ B co B' |]
        ==> F ∈ (B' ∩ A) leadsTo ((B ∩ A') ∪ (B' - B))"
    by (simp (no_asm_simp) add: psp Int_ac)

    lemma psp_unless:
       "[| F ∈ A leadsTo A';  F ∈ B unless B' |]
        ==> F ∈ (A ∩ B) leadsTo ((A' ∩ B) ∪ B')"

    apply (unfold unless_def)
    apply (drule psp, assumption)
    apply (blast intro: leadsTo_weaken)
    done

    subsection{*Proving the induction rules*}

    (** The most general rule: r is any wf relation; f is any variant function **)

    lemma leadsTo_wf_induct_lemma:
         "[| wf r;
             ∀m. F ∈ (A ∩ f-`{m}) leadsTo
                        ((A ∩ f-`(r^-1 `` {m})) ∪ B) |]
          ==> F ∈ (A ∩ f-`{m}) leadsTo B"
    apply (erule_tac a = m in wf_induct)
    apply (subgoal_tac "F ∈ (A ∩ (f -` (r^-1 `` {x}))) leadsTo B")
     apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
    apply (subst vimage_eq_UN)
    apply (simp only: UN_simps [symmetric])
    apply (blast intro: leadsTo_UN)
    done

    (** Meta or object quantifier ? **)
    lemma leadsTo_wf_induct:
         "[| wf r;
             ∀m. F ∈ (A ∩ f-`{m}) leadsTo
                        ((A ∩ f-`(r^-1 `` {m})) ∪ B) |]
          ==> F ∈ A leadsTo B"
    apply (rule_tac t = A in subst)
     defer 1
     apply (rule leadsTo_UN)
     apply (erule leadsTo_wf_induct_lemma)
     apply assumption
    apply fast (*Blast_tac: Function unknown's argument not a parameter*)
    done

    lemma bounded_induct:
         "[| wf r;
             ∀m ∈ I. F ∈ (A ∩ f-`{m}) leadsTo
                          ((A ∩ f-`(r^-1 `` {m})) ∪ B) |]
          ==> F ∈ A leadsTo ((A - (f-`I)) ∪ B)"
    apply (erule leadsTo_wf_induct, safe)
    apply (case_tac "m ∈ I")
    apply (blast intro: leadsTo_weaken)
    apply (blast intro: subset_imp_leadsTo)
    done

    (*Alternative proof is via the lemma F ∈ (A ∩ f-`(lessThan m)) leadsTo B*)
    lemma lessThan_induct:
         "[| !!m::nat. F ∈ (A ∩ f-`{m}) leadsTo ((A ∩ f-`{..<m}) ∪ B) |]
          ==> F ∈ A leadsTo B"
    apply (rule wf_less_than [THEN leadsTo_wf_induct])
    apply (simp (no_asm_simp))
    apply blast
    done

    lemma lessThan_bounded_induct:
         "!!l::nat. [| ∀m ∈ greaterThan l.
                F ∈ (A ∩ f-`{m}) leadsTo ((A ∩ f-`(lessThan m)) ∪ B) |]
          ==> F ∈ A leadsTo ((A ∩ (f-`(atMost l))) ∪ B)"
    apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
    apply (rule wf_less_than [THEN bounded_induct])
    apply (simp (no_asm_simp))
    done

    lemma greaterThan_bounded_induct:
         "(!!l::nat. ∀m ∈ lessThan l.
                     F ∈ (A ∩ f-`{m}) leadsTo ((A ∩ f-`(greaterThan m)) ∪ B))
          ==> F ∈ A leadsTo ((A ∩ (f-`(atLeast l))) ∪ B)"
    apply (rule_tac f = f and f1 = "%k. l - k"
           in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
    apply (simp (no_asm) add: inv_image_def Image_singleton)
    apply clarify
    apply (case_tac "m<l")
     apply (blast intro: leadsTo_weaken_R diff_less_mono2)
    apply (blast intro: not_leE subset_imp_leadsTo)
    done

    subsection{*wlt*}

    text{*Misra's property W3*}
    lemma wlt_leadsTo: "F ∈ (wlt F B) leadsTo B"
    apply (unfold wlt_def)
    apply (blast intro!: leadsTo_Union)
    done

    lemma leadsTo_subset: "F ∈ A leadsTo B ==> A ⊆ wlt F B"
    apply (unfold wlt_def)
    apply (blast intro!: leadsTo_Union)
    done

    text{*Misra's property W2*}
    lemma leadsTo_eq_subset_wlt: "F ∈ A leadsTo B = (A ⊆ wlt F B)"
    by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])

    text{*Misra's property W4*}
    lemma wlt_increasing: "B ⊆ wlt F B"
    apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
    done

    text{*Used in the Trans case below*}
    lemma lemma1:
       "[| B ⊆ A2;
           F ∈ (A1 - B) co (A1 ∪ B);
           F ∈ (A2 - C) co (A2 ∪ C) |]
        ==> F ∈ (A1 ∪ A2 - C) co (A1 ∪ A2 ∪ C)"
    by (unfold constrains_def, clarify,  blast)

    text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
    lemma leadsTo_123:
         "F ∈ A leadsTo A'
          ==> ∃B. A ⊆ B & F ∈ B leadsTo A' & F ∈ (B-A') co (B ∪ A')"
    apply (erule leadsTo_induct)
      txt{*Basis*}
      apply (blast dest: ensuresD)
     txt{*Trans*}
     apply clarify
     apply (rule_tac x = "Ba ∪ Bb" in exI)
     apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
    txt{*Union*}
    apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
    apply (rule_tac x = "\<Union>A ∈ S. f A" in exI)
    apply (auto intro: leadsTo_UN)
    (*Blast_tac says PROOF FAILED*)
    apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i ∪ B"
           in constrains_UN [THEN constrains_weaken], auto)
    done

    text{*Misra's property W5*}
    lemma wlt_constrains_wlt: "F ∈ (wlt F B - B) co (wlt F B)"
    proof -
      from wlt_leadsTo [of F B, THEN leadsTo_123]
      show ?thesis
      proof (elim exE conjE)
    (* assumes have to be in exactly the form as in the goal displayed at
       this point.  Isar doesn't give you any automation. *)
        fix C
        assume wlt: "wlt F B ⊆ C"
           and lt:  "F ∈ C leadsTo B"
           and co:  "F ∈ C - B co C ∪ B"
        have eq: "C = wlt F B"
        proof -
          from lt and wlt show ?thesis
               by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1])
        qed
        from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2)
      qed
    qed

    subsection{*Completion: Binary and General Finite versions*}

    lemma completion_lemma :
         "[| W = wlt F (B' ∪ C);
           F ∈ A leadsTo (A' ∪ C);  F ∈ A' co (A' ∪ C);
           F ∈ B leadsTo (B' ∪ C);  F ∈ B' co (B' ∪ C) |]
        ==> F ∈ (A ∩ B) leadsTo ((A' ∩ B') ∪ C)"
    apply (subgoal_tac "F ∈ (W-C) co (W ∪ B' ∪ C) ")
     prefer 2
     apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un,
                                             THEN constrains_weaken])
    apply (subgoal_tac "F ∈ (W-C) co W")
     prefer 2
     apply (simp add: wlt_increasing Un_assoc Un_absorb2)
    apply (subgoal_tac "F ∈ (A ∩ W - C) leadsTo (A' ∩ W ∪ C) ")
     prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
    (** LEVEL 6 **)
    apply (subgoal_tac "F ∈ (A' ∩ W ∪ C) leadsTo (A' ∩ B' ∪ C) ")
     prefer 2
     apply (rule leadsTo_Un_duplicate2)
     apply (blast intro: leadsTo_Un_Un wlt_leadsTo
                             [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
    apply (drule leadsTo_Diff)
    apply (blast intro: subset_imp_leadsTo)
    apply (subgoal_tac "A ∩ B ⊆ A ∩ W")
     prefer 2
     apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
    apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
    done

    lemmas completion = completion_lemma [OF refl]

    lemma finite_completion_lemma:
         "finite I ==> (∀i ∈ I. F ∈ (A i) leadsTo (A' i ∪ C)) -->
                       (∀i ∈ I. F ∈ (A' i) co (A' i ∪ C)) -->
                       F ∈ (\<Inter>i ∈ I. A i) leadsTo ((\<Inter>i ∈ I. A' i) ∪ C)"
    apply (erule finite_induct, auto)
    apply (rule completion)
       prefer 4
       apply (simp only: INT_simps [symmetric])
       apply (rule constrains_INT, auto)
    done

    lemma finite_completion:
         "[| finite I;
             !!i. i ∈ I ==> F ∈ (A i) leadsTo (A' i ∪ C);
             !!i. i ∈ I ==> F ∈ (A' i) co (A' i ∪ C) |]
          ==> F ∈ (\<Inter>i ∈ I. A i) leadsTo ((\<Inter>i ∈ I. A' i) ∪ C)"
    by (blast intro: finite_completion_lemma [THEN mp, THEN mp])

    lemma stable_completion:
         "[| F ∈ A leadsTo A';  F ∈ stable A';
             F ∈ B leadsTo B';  F ∈ stable B' |]
        ==> F ∈ (A ∩ B) leadsTo (A' ∩ B')"
    apply (unfold stable_def)
    apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
    apply (force+)
    done

    lemma finite_stable_completion:
         "[| finite I;
             !!i. i ∈ I ==> F ∈ (A i) leadsTo (A' i);
             !!i. i ∈ I ==> F ∈ stable (A' i) |]
          ==> F ∈ (\<Inter>i ∈ I. A i) leadsTo (\<Inter>i ∈ I. A' i)"
    apply (unfold stable_def)
    apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
    apply (simp_all (no_asm_simp))
    apply blast+
    done

    end

### transient

lemma stable_transient:

      [| F ∈ stable A; F ∈ transient A |] ==> ∃act∈Acts F. A ⊆ - Domain act

lemma stable_transient_empty:

      [| F ∈ stable A; F ∈ transient A; all_total F |] ==> A = {}

lemma transient_strengthen:

      [| F ∈ transient A; B ⊆ A |] ==> F ∈ transient B

lemma transientI:

      [| act ∈ Acts F; act `` A ⊆ - A |] ==> F ∈ transient A

lemma transientE:

      [| F ∈ transient A; !!act. [| act ∈ Acts F; act `` A ⊆ - A |] ==> P |] ==> P

lemma transient_empty:

      transient {} = UNIV

lemma totalize_transient_iff:

      (totalize F ∈ transient A) = (∃act∈Acts F. A ⊆ Domain act ∧ act `` A ⊆ - A)

lemma totalize_transientI:

      [| act ∈ Acts F; A ⊆ Domain act; act `` A ⊆ - A |] ==> totalize F ∈ transient A

### ensures

lemma ensuresI:

      [| F ∈ A - B co A ∪ B; F ∈ transient (A - B) |] ==> F ∈ A ensures B

lemma ensuresD:

      F ∈ A ensures B ==> F ∈ A - B co A ∪ B ∧ F ∈ transient (A - B)

lemma ensures_weaken_R:

      [| F ∈ A ensures A'; A' ⊆ B' |] ==> F ∈ A ensures B'

lemma stable_ensures_Int:

      [| F ∈ stable C; F ∈ A ensures B |] ==> F ∈ C ∩ A ensures C ∩ B

lemma stable_transient_ensures:

      [| F ∈ stable A; F ∈ transient C; A ⊆ B ∪ C |] ==> F ∈ A ensures B

lemma ensures_eq:

      A ensures B = (A unless B) ∩ transient (A - B)

### leadsTo

lemma leadsTo_Basis:

      F ∈ A ensures B ==> F ∈ A leadsTo B

lemma leadsTo_Trans:

      [| F ∈ A leadsTo B; F ∈ B leadsTo C |] ==> F ∈ A leadsTo C

lemma leadsTo_Basis':

      [| F ∈ A co A ∪ B; F ∈ transient A |] ==> F ∈ A leadsTo B

lemma transient_imp_leadsTo:

      F ∈ transient A ==> F ∈ A leadsTo - A

lemma leadsTo_Un_duplicate:

      F ∈ A leadsTo A' ∪ A' ==> F ∈ A leadsTo A'

lemma leadsTo_Un_duplicate2:

      F ∈ A leadsTo A' ∪ C ∪ C ==> F ∈ A leadsTo A' ∪ C

lemma leadsTo_Union:

      (!!A. A ∈ S ==> F ∈ A leadsTo B) ==> F ∈ Union S leadsTo B

lemma leadsTo_Union_Int:

      (!!A. A ∈ S ==> F ∈ A ∩ C leadsTo B) ==> F ∈ Union S ∩ C leadsTo B

lemma leadsTo_UN:

      (!!i. i ∈ I ==> F ∈ A i leadsTo B) ==> F ∈ (UN i:I. A i) leadsTo B

lemma leadsTo_Un:

      [| F ∈ A leadsTo C; F ∈ B leadsTo C |] ==> F ∈ A ∪ B leadsTo C

lemma single_leadsTo_I:

      (!!x. x ∈ A ==> F ∈ {x} leadsTo B) ==> F ∈ A leadsTo B

lemma leadsTo_induct:

      [| F ∈ za leadsTo zb; !!A B. F ∈ A ensures B ==> P A B;
         !!A B C. [| F ∈ A leadsTo B; P A B; F ∈ B leadsTo C; P B C |] ==> P A C;
         !!B S. ∀A∈S. F ∈ A leadsTo B ∧ P A B ==> P (Union S) B |]
      ==> P za zb

lemma subset_imp_ensures:

      A ⊆ B ==> F ∈ A ensures B

lemmas subset_imp_leadsTo:

      A ⊆ B ==> F ∈ A leadsTo B

lemmas subset_imp_leadsTo:

      A ⊆ B ==> F ∈ A leadsTo B

lemmas leadsTo_refl:

      F ∈ A leadsTo A

lemmas leadsTo_refl:

      F ∈ A leadsTo A

lemmas empty_leadsTo:

      F ∈ {} leadsTo B

lemmas empty_leadsTo:

      F ∈ {} leadsTo B

lemmas leadsTo_UNIV:

      F ∈ A leadsTo UNIV

lemmas leadsTo_UNIV:

      F ∈ A leadsTo UNIV

lemma leadsTo_induct_pre_lemma:

      [| F ∈ za leadsTo zb; P zb; !!A B. [| F ∈ A ensures B; P B |] ==> P A;
         !!S. ∀A∈S. P A ==> P (Union S) |]
      ==> P za

lemma leadsTo_induct_pre:

      [| F ∈ za leadsTo zb; P zb;
         !!A B. [| F ∈ A ensures B; F ∈ B leadsTo zb; P B |] ==> P A;
         !!S. ∀A∈S. F ∈ A leadsTo zb ∧ P A ==> P (Union S) |]
      ==> P za

lemma leadsTo_weaken_R:

      [| F ∈ A leadsTo A'; A' ⊆ B' |] ==> F ∈ A leadsTo B'

lemma leadsTo_weaken_L:

      [| F ∈ A leadsTo A'; B ⊆ A |] ==> F ∈ B leadsTo A'

lemma leadsTo_Un_distrib:

      (F ∈ A ∪ B leadsTo C) = (F ∈ A leadsTo C ∧ F ∈ B leadsTo C)

lemma leadsTo_UN_distrib:

      (F ∈ (UN i:I. A i) leadsTo B) = (∀i∈I. F ∈ A i leadsTo B)

lemma leadsTo_Union_distrib:

      (F ∈ Union S leadsTo B) = (∀A∈S. F ∈ A leadsTo B)

lemma leadsTo_weaken:

      [| F ∈ A leadsTo A'; B ⊆ A; A' ⊆ B' |] ==> F ∈ B leadsTo B'

lemma leadsTo_Diff:

      [| F ∈ A - B leadsTo C; F ∈ B leadsTo C |] ==> F ∈ A leadsTo C

lemma leadsTo_UN_UN:

      (!!i. i ∈ I ==> F ∈ A i leadsTo A' i)
      ==> F ∈ (UN i:I. A i) leadsTo (UN i:I. A' i)

lemma leadsTo_Un_Un:

      [| F ∈ A leadsTo A'; F ∈ B leadsTo B' |] ==> F ∈ A ∪ B leadsTo A' ∪ B'

lemma leadsTo_cancel2:

      [| F ∈ A leadsTo A' ∪ B; F ∈ B leadsTo B' |] ==> F ∈ A leadsTo A' ∪ B'

lemma leadsTo_cancel_Diff2:

      [| F ∈ A leadsTo A' ∪ B; F ∈ B - A' leadsTo B' |] ==> F ∈ A leadsTo A' ∪ B'

lemma leadsTo_cancel1:

      [| F ∈ A leadsTo B ∪ A'; F ∈ B leadsTo B' |] ==> F ∈ A leadsTo B' ∪ A'

lemma leadsTo_cancel_Diff1:

      [| F ∈ A leadsTo B ∪ A'; F ∈ B - A' leadsTo B' |] ==> F ∈ A leadsTo B' ∪ A'

lemma leadsTo_empty:

      [| F ∈ A leadsTo {}; all_total F |] ==> A = {}

### PSP: Progress-Safety-Progress

lemma psp_stable:

      [| F ∈ A leadsTo A'; F ∈ stable B |] ==> F ∈ A ∩ B leadsTo A' ∩ B

lemma psp_stable2:

      [| F ∈ A leadsTo A'; F ∈ stable B |] ==> F ∈ B ∩ A leadsTo B ∩ A'

lemma psp_ensures:

      [| F ∈ A ensures A'; F ∈ B co B' |] ==> F ∈ A ∩ B' ensures A' ∩ B ∪ (B' - B)

lemma psp:

      [| F ∈ A leadsTo A'; F ∈ B co B' |] ==> F ∈ A ∩ B' leadsTo A' ∩ B ∪ (B' - B)

lemma psp2:

      [| F ∈ A leadsTo A'; F ∈ B co B' |] ==> F ∈ B' ∩ A leadsTo B ∩ A' ∪ (B' - B)

lemma psp_unless:

      [| F ∈ A leadsTo A'; F ∈ B unless B' |] ==> F ∈ A ∩ B leadsTo A' ∩ B ∪ B'

### Proving the induction rules

lemma leadsTo_wf_induct_lemma:

      [| wf r; ∀m. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` r^-1 `` {m} ∪ B |]
      ==> F ∈ A ∩ f -` {m} leadsTo B

lemma leadsTo_wf_induct:

      [| wf r; ∀m. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` r^-1 `` {m} ∪ B |]
      ==> F ∈ A leadsTo B

lemma bounded_induct:

      [| wf r; ∀m∈I. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` r^-1 `` {m} ∪ B |]
      ==> F ∈ A leadsTo A - f -` I ∪ B

lemma lessThan_induct:

      (!!m. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` {..<m} ∪ B) ==> F ∈ A leadsTo B

lemma lessThan_bounded_induct:

      ∀m∈{l<..}. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` {..<m} ∪ B
      ==> F ∈ A leadsTo A ∩ f -` {..l} ∪ B

lemma greaterThan_bounded_induct:

      (!!l. ∀m∈{..<l}. F ∈ A ∩ f -` {m} leadsTo A ∩ f -` {m<..} ∪ B)
      ==> F ∈ A leadsTo A ∩ f -` {l..} ∪ B

### wlt

lemma wlt_leadsTo:

      F ∈ wlt F B leadsTo B

lemma leadsTo_subset:

      F ∈ A leadsTo B ==> A ⊆ wlt F B

lemma leadsTo_eq_subset_wlt:

      (F ∈ A leadsTo B) = (A ⊆ wlt F B)

lemma wlt_increasing:

      B ⊆ wlt F B

lemma lemma1:

      [| B ⊆ A2.0; F ∈ A1.0 - B co A1.0 ∪ B; F ∈ A2.0 - C co A2.0 ∪ C |]
      ==> F ∈ A1.0 ∪ A2.0 - C co A1.0 ∪ A2.0 ∪ C

lemma leadsTo_123:

      F ∈ A leadsTo A' ==> ∃B≥A. F ∈ B leadsTo A' ∧ F ∈ B - A' co B ∪ A'

lemma wlt_constrains_wlt:

      F ∈ wlt F B - B co wlt F B

### Completion: Binary and General Finite versions

lemma completion_lemma:

      [| W = wlt F (B' ∪ C); F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C;
         F ∈ B leadsTo B' ∪ C; F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemmas completion:

      [| F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C; F ∈ B leadsTo B' ∪ C;
         F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemmas completion:

      [| F ∈ A leadsTo A' ∪ C; F ∈ A' co A' ∪ C; F ∈ B leadsTo B' ∪ C;
         F ∈ B' co B' ∪ C |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B' ∪ C

lemma finite_completion_lemma:

      finite I
      ==> (∀i∈I. F ∈ A i leadsTo A' i ∪ C) -->
          (∀i∈I. F ∈ A' i co A' i ∪ C) -->
          F ∈ (INT i:I. A i) leadsTo (INT i:I. A' i) ∪ C

lemma finite_completion:

      [| finite I; !!i. i ∈ I ==> F ∈ A i leadsTo A' i ∪ C;
         !!i. i ∈ I ==> F ∈ A' i co A' i ∪ C |]
      ==> F ∈ (INT i:I. A i) leadsTo (INT i:I. A' i) ∪ C

lemma stable_completion:

      [| F ∈ A leadsTo A'; F ∈ stable A'; F ∈ B leadsTo B'; F ∈ stable B' |]
      ==> F ∈ A ∩ B leadsTo A' ∩ B'

lemma finite_stable_completion:

      [| finite I; !!i. i ∈ I ==> F ∈ A i leadsTo A' i;
         !!i. i ∈ I ==> F ∈ stable (A' i) |]
      ==> F ∈ (INT i:I. A i) leadsTo (INT i:I. A' i)