# Theory ProgressSets

Up to index of Isabelle/HOL/UNITY

theory ProgressSets
imports Transformers
begin

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

    Progress Sets.  From

        David Meier and Beverly Sanders,
        Composing Leads-to Properties
        Theoretical Computer Science 243:1-2 (2000), 339-361.

        David Meier,
        Progress Properties in Program Refinement and Parallel Composition
        Swiss Federal Institute of Technology Zurich (1997)
    *)

    header{*Progress Sets*}

    theory ProgressSets imports Transformers begin

    subsection {*Complete Lattices and the Operator @{term cl}*}

    constdefs
      lattice :: "'a set set => bool"
       --{*Meier calls them closure sets, but they are just complete lattices*}
       "lattice L ==
             (∀M. M ⊆ L --> \<Inter>M ∈ L) & (∀M. M ⊆ L --> \<Union>M ∈ L)"

      cl :: "['a set set, 'a set] => 'a set"
       --{*short for ``closure''*}
       "cl L r == \<Inter>{x. x∈L & r ⊆ x}"

    lemma UNIV_in_lattice: "lattice L ==> UNIV ∈ L"
    by (force simp add: lattice_def)

    lemma empty_in_lattice: "lattice L ==> {} ∈ L"
    by (force simp add: lattice_def)

    lemma Union_in_lattice: "[|M ⊆ L; lattice L|] ==> \<Union>M ∈ L"
    by (simp add: lattice_def)

    lemma Inter_in_lattice: "[|M ⊆ L; lattice L|] ==> \<Inter>M ∈ L"
    by (simp add: lattice_def)

    lemma UN_in_lattice:
         "[|lattice L; !!i. i∈I ==> r i ∈ L|] ==> (\<Union>i∈I. r i) ∈ L"
    apply (simp add: Set.UN_eq)
    apply (blast intro: Union_in_lattice)
    done

    lemma INT_in_lattice:
         "[|lattice L; !!i. i∈I ==> r i ∈ L|] ==> (\<Inter>i∈I. r i)  ∈ L"
    apply (simp add: INT_eq)
    apply (blast intro: Inter_in_lattice)
    done

    lemma Un_in_lattice: "[|x∈L; y∈L; lattice L|] ==> x∪y ∈ L"
    apply (simp only: Un_eq_Union)
    apply (blast intro: Union_in_lattice)
    done

    lemma Int_in_lattice: "[|x∈L; y∈L; lattice L|] ==> x∩y ∈ L"
    apply (simp only: Int_eq_Inter)
    apply (blast intro: Inter_in_lattice)
    done

    lemma lattice_stable: "lattice {X. F ∈ stable X}"
    by (simp add: lattice_def stable_def constrains_def, blast)

    text{*The next three results state that @{term "cl L r"} is the minimal
     element of @{term L} that includes @{term r}.*}
    lemma cl_in_lattice: "lattice L ==> cl L r ∈ L"
    apply (simp add: lattice_def cl_def)
    apply (erule conjE)
    apply (drule spec, erule mp, blast)
    done

    lemma cl_least: "[|c∈L; r⊆c|] ==> cl L r ⊆ c"
    by (force simp add: cl_def)

    text{*The next three lemmas constitute assertion (4.61)*}
    lemma cl_mono: "r ⊆ r' ==> cl L r ⊆ cl L r'"
    by (simp add: cl_def, blast)

    lemma subset_cl: "r ⊆ cl L r"
    by (simp add: cl_def, blast)

    text{*A reformulation of @{thm subset_cl}*}
    lemma clI: "x ∈ r ==> x ∈ cl L r"
    by (simp add: cl_def, blast)

    text{*A reformulation of @{thm cl_least}*}
    lemma clD: "[|c ∈ cl L r; B ∈ L; r ⊆ B|] ==> c ∈ B"
    by (force simp add: cl_def)

    lemma cl_UN_subset: "(\<Union>i∈I. cl L (r i)) ⊆ cl L (\<Union>i∈I. r i)"
    by (simp add: cl_def, blast)

    lemma cl_Un: "lattice L ==> cl L (r∪s) = cl L r ∪ cl L s"
    apply (rule equalityI)
     prefer 2
      apply (simp add: cl_def, blast)
    apply (rule cl_least)
     apply (blast intro: Un_in_lattice cl_in_lattice)
    apply (blast intro: subset_cl [THEN subsetD])
    done

    lemma cl_UN: "lattice L ==> cl L (\<Union>i∈I. r i) = (\<Union>i∈I. cl L (r i))"
    apply (rule equalityI)
     prefer 2 apply (simp add: cl_def, blast)
    apply (rule cl_least)
     apply (blast intro: UN_in_lattice cl_in_lattice)
    apply (blast intro: subset_cl [THEN subsetD])
    done

    lemma cl_Int_subset: "cl L (r∩s) ⊆ cl L r ∩ cl L s"
    by (simp add: cl_def, blast)

    lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
    by (simp add: cl_def, blast)

    lemma cl_ident: "r∈L ==> cl L r = r"
    by (force simp add: cl_def)

    lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
    by (simp add: cl_ident empty_in_lattice)

    lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
    by (simp add: cl_ident UNIV_in_lattice)

    text{*Assertion (4.62)*}
    lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r∈L)"
    apply (rule iffI)
     apply (erule subst)
     apply (erule cl_in_lattice)
    apply (erule cl_ident)
    done

    lemma cl_subset_in_lattice: "[|cl L r ⊆ r; lattice L|] ==> r∈L"
    by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)

    subsection {*Progress Sets and the Main Lemma*}
    text{*A progress set satisfies certain closure conditions and is a
    simple way of including the set @{term "wens_set F B"}.*}

    constdefs
      closed :: "['a program, 'a set, 'a set,  'a set set] => bool"
       "closed F T B L == ∀M. ∀act ∈ Acts F. B⊆M & T∩M ∈ L -->
                                  T ∩ (B ∪ wp act M) ∈ L"

      progress_set :: "['a program, 'a set, 'a set] => 'a set set set"
       "progress_set F T B ==
          {L. lattice L & B ∈ L & T ∈ L & closed F T B L}"

    lemma closedD:
       "[|closed F T B L; act ∈ Acts F; B⊆M; T∩M ∈ L|]
        ==> T ∩ (B ∪ wp act M) ∈ L"
    by (simp add: closed_def)

    text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
    and @{term m} by @{term X}. *}

    text{*Part of the proof of the claim at the bottom of page 97.  It's
    proved separately because the argument requires a generalization over
    all @{term "act ∈ Acts F"}.*}
    lemma lattice_awp_lemma:
      assumes TXC:  "T∩X ∈ C" --{*induction hypothesis in theorem below*}
          and BsubX:  "B ⊆ X"   --{*holds in inductive step*}
          and latt: "lattice C"
          and TC:   "T ∈ C"
          and BC:   "B ∈ C"
          and clos: "closed F T B C"
        shows "T ∩ (B ∪ awp F (X ∪ cl C (T∩r))) ∈ C"
    apply (simp del: INT_simps add: awp_def INT_extend_simps)
    apply (rule INT_in_lattice [OF latt])
    apply (erule closedD [OF clos])
    apply (simp add: subset_trans [OF BsubX Un_upper1])
    apply (subgoal_tac "T ∩ (X ∪ cl C (T∩r)) = (T∩X) ∪ cl C (T∩r)")
     prefer 2 apply (blast intro: TC clD)
    apply (erule ssubst)
    apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
    done

    text{*Remainder of the proof of the claim at the bottom of page 97.*}
    lemma lattice_lemma:
      assumes TXC:  "T∩X ∈ C" --{*induction hypothesis in theorem below*}
          and BsubX:  "B ⊆ X"   --{*holds in inductive step*}
          and act:  "act ∈ Acts F"
          and latt: "lattice C"
          and TC:   "T ∈ C"
          and BC:   "B ∈ C"
          and clos: "closed F T B C"
        shows "T ∩ (wp act X ∩ awp F (X ∪ cl C (T∩r)) ∪ X) ∈ C"
    apply (subgoal_tac "T ∩ (B ∪ wp act X) ∈ C")
     prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC)
    apply (drule Int_in_lattice
                  [OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r]
                        latt])
    apply (subgoal_tac
             "T ∩ (B ∪ wp act X) ∩ (T ∩ (B ∪ awp F (X ∪ cl C (T∩r)))) =
              T ∩ (B ∪ wp act X ∩ awp F (X ∪ cl C (T∩r)))")
     prefer 2 apply blast
    apply simp
    apply (drule Un_in_lattice [OF _ TXC latt])
    apply (subgoal_tac
             "T ∩ (B ∪ wp act X ∩ awp F (X ∪ cl C (T∩r))) ∪ T∩X =
              T ∩ (wp act X ∩ awp F (X ∪ cl C (T∩r)) ∪ X)")
     apply simp
    apply (blast intro: BsubX [THEN subsetD])
    done

    text{*Induction step for the main lemma*}
    lemma progress_induction_step:
      assumes TXC:  "T∩X ∈ C" --{*induction hypothesis in theorem below*}
          and act:  "act ∈ Acts F"
          and Xwens: "X ∈ wens_set F B"
          and latt: "lattice C"
          and  TC:  "T ∈ C"
          and  BC:  "B ∈ C"
          and clos: "closed F T B C"
          and Fstable: "F ∈ stable T"
      shows "T ∩ wens F act X ∈ C"
    proof -
      from Xwens have BsubX: "B ⊆ X"
        by (rule wens_set_imp_subset)
      let ?r = "wens F act X"
      have "?r ⊆ (wp act X ∩ awp F (X∪?r)) ∪ X"
        by (simp add: wens_unfold [symmetric])
      then have "T∩?r ⊆ T ∩ ((wp act X ∩ awp F (X∪?r)) ∪ X)"
        by blast
      then have "T∩?r ⊆ T ∩ ((wp act X ∩ awp F (T ∩ (X∪?r))) ∪ X)"
        by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast)
      then have "T∩?r ⊆ T ∩ ((wp act X ∩ awp F (X ∪ cl C (T∩?r))) ∪ X)"
        by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD])
      then have "cl C (T∩?r) ⊆
                 cl C (T ∩ ((wp act X ∩ awp F (X ∪ cl C (T∩?r))) ∪ X))"
        by (rule cl_mono)
      then have "cl C (T∩?r) ⊆
                 T ∩ ((wp act X ∩ awp F (X ∪ cl C (T∩?r))) ∪ X)"
        by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos])
      then have "cl C (T∩?r) ⊆ (wp act X ∩ awp F (X ∪ cl C (T∩?r))) ∪ X"
        by blast
      then have "cl C (T∩?r) ⊆ ?r"
        by (blast intro!: subset_wens)
      then have cl_subset: "cl C (T∩?r) ⊆ T∩?r"
        by (simp add: Int_subset_iff cl_ident TC
                      subset_trans [OF cl_mono [OF Int_lower1]])
      show ?thesis
        by (rule cl_subset_in_lattice [OF cl_subset latt])
    qed

    text{*Proved on page 96 of Meier's thesis.  The special case when
       @{term "T=UNIV"} states that every progress set for the program @{term F}
       and set @{term B} includes the set @{term "wens_set F B"}.*}
    lemma progress_set_lemma:
         "[|C ∈ progress_set F T B; r ∈ wens_set F B; F ∈ stable T|] ==> T∩r ∈ C"
    apply (simp add: progress_set_def, clarify)
    apply (erule wens_set.induct)
      txt{*Base*}
      apply (simp add: Int_in_lattice)
     txt{*The difficult @{term wens} case*}
     apply (simp add: progress_induction_step)
    txt{*Disjunctive case*}
    apply (subgoal_tac "(\<Union>U∈W. T ∩ U) ∈ C")
     apply (simp add: Int_Union)
    apply (blast intro: UN_in_lattice)
    done

    subsection {*The Progress Set Union Theorem*}

    lemma closed_mono:
      assumes BB':  "B ⊆ B'"
          and TBwp: "T ∩ (B ∪ wp act M) ∈ C"
          and B'C:  "B' ∈ C"
          and TC:   "T ∈ C"
          and latt: "lattice C"
      shows "T ∩ (B' ∪ wp act M) ∈ C"
    proof -
      from TBwp have "(T∩B) ∪ (T ∩ wp act M) ∈ C"
        by (simp add: Int_Un_distrib)
      then have TBBC: "(T∩B') ∪ ((T∩B) ∪ (T ∩ wp act M)) ∈ C"
        by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt)
      show ?thesis
        by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC],
            blast intro: BB' [THEN subsetD])
    qed

    lemma progress_set_mono:
        assumes BB':  "B ⊆ B'"
        shows
         "[| B' ∈ C;  C ∈ progress_set F T B|]
          ==> C ∈ progress_set F T B'"
    by (simp add: progress_set_def closed_def closed_mono [OF BB']
                     subset_trans [OF BB'])

    theorem progress_set_Union:
      assumes leadsTo: "F ∈ A leadsTo B'"
          and prog: "C ∈ progress_set F T B"
          and Fstable: "F ∈ stable T"
          and BB':  "B ⊆ B'"
          and B'C:  "B' ∈ C"
          and Gco: "!!X. X∈C ==> G ∈ X-B co X"
      shows "F\<squnion>G ∈ T∩A leadsTo B'"
    apply (insert prog Fstable)
    apply (rule leadsTo_Join [OF leadsTo])
      apply (force simp add: progress_set_def awp_iff_stable [symmetric])
    apply (simp add: awp_iff_constrains)
    apply (drule progress_set_mono [OF BB' B'C])
    apply (blast intro: progress_set_lemma Gco constrains_weaken_L
                        BB' [THEN subsetD])
    done

    subsection {*Some Progress Sets*}

    lemma UNIV_in_progress_set: "UNIV ∈ progress_set F T B"
    by (simp add: progress_set_def lattice_def closed_def)

    subsubsection {*Lattices and Relations*}
    text{*From Meier's thesis, section 4.5.3*}

    constdefs
      relcl :: "'a set set => ('a * 'a) set"
        -- {*Derived relation from a lattice*}
        "relcl L == {(x,y). y ∈ cl L {x}}"

      latticeof :: "('a * 'a) set => 'a set set"
        -- {*Derived lattice from a relation: the set of upwards-closed sets*}
        "latticeof r == {X. ∀s t. s ∈ X & (s,t) ∈ r --> t ∈ X}"

    lemma relcl_refl: "(a,a) ∈ relcl L"
    by (simp add: relcl_def subset_cl [THEN subsetD])

    lemma relcl_trans:
         "[| (a,b) ∈ relcl L; (b,c) ∈ relcl L; lattice L |] ==> (a,c) ∈ relcl L"
    apply (simp add: relcl_def)
    apply (blast intro: clD cl_in_lattice)
    done

    lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
    by (simp add: reflI relcl_def subset_cl [THEN subsetD])

    lemma trans_relcl: "lattice L ==> trans (relcl L)"
    by (blast intro: relcl_trans transI)

    lemma lattice_latticeof: "lattice (latticeof r)"
    by (auto simp add: lattice_def latticeof_def)

    lemma lattice_singletonI:
         "[|lattice L; !!s. s ∈ X ==> {s} ∈ L|] ==> X ∈ L"
    apply (cut_tac UN_singleton [of X])
    apply (erule subst)
    apply (simp only: UN_in_lattice)
    done

    text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
    lemma cl_latticeof:
         "[|refl UNIV r; trans r|]
          ==> cl (latticeof r) X = {t. ∃s. s∈X & (s,t) ∈ r}"
    apply (rule equalityI)
     apply (rule cl_least)
      apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
     apply (simp add: latticeof_def refl_def, blast)
    apply (simp add: latticeof_def, clarify)
    apply (unfold cl_def, blast)
    done

    text{*Related to (4.71).*}
    lemma cl_eq_Collect_relcl:
         "lattice L ==> cl L X = {t. ∃s. s∈X & (s,t) ∈ relcl L}"
    apply (cut_tac UN_singleton [of X])
    apply (erule subst)
    apply (force simp only: relcl_def cl_UN)
    done

    text{*Meier's theorem of section 4.5.3*}
    theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
    apply (rule equalityI)
     prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify)
    apply (rename_tac X)
    apply (rule cl_subset_in_lattice)
     prefer 2 apply assumption
    apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
    apply (drule equalityD1)
    apply (rule subset_trans)
     prefer 2 apply assumption
    apply (thin_tac "?U ⊆ X")
    apply (cut_tac A=X in UN_singleton)
    apply (erule subst)
    apply (simp only: cl_UN lattice_latticeof
                      cl_latticeof [OF refl_relcl trans_relcl])
    apply (simp add: relcl_def)
    done

    theorem relcl_latticeof_eq:
         "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
    by (simp add: relcl_def cl_latticeof, blast)

    subsubsection {*Decoupling Theorems*}

    constdefs
      decoupled :: "['a program, 'a program] => bool"
       "decoupled F G ==
            ∀act ∈ Acts F. ∀B. G ∈ stable B --> G ∈ stable (wp act B)"

    text{*Rao's Decoupling Theorem*}
    lemma stableco: "F ∈ stable A ==> F ∈ A-B co A"
    by (simp add: stable_def constrains_def, blast)

    theorem decoupling:
      assumes leadsTo: "F ∈ A leadsTo B"
          and Gstable: "G ∈ stable B"
          and dec:     "decoupled F G"
      shows "F\<squnion>G ∈ A leadsTo B"
    proof -
      have prog: "{X. G ∈ stable X} ∈ progress_set F UNIV B"
        by (simp add: progress_set_def lattice_stable Gstable closed_def
                      stable_Un [OF Gstable] dec [unfolded decoupled_def])
      have "F\<squnion>G ∈ (UNIV∩A) leadsTo B"
        by (rule progress_set_Union [OF leadsTo prog],
            simp_all add: Gstable stableco)
      thus ?thesis by simp
    qed

    text{*Rao's Weak Decoupling Theorem*}
    theorem weak_decoupling:
      assumes leadsTo: "F ∈ A leadsTo B"
          and stable: "F\<squnion>G ∈ stable B"
          and dec:     "decoupled F (F\<squnion>G)"
      shows "F\<squnion>G ∈ A leadsTo B"
    proof -
      have prog: "{X. F\<squnion>G ∈ stable X} ∈ progress_set F UNIV B"
        by (simp del: Join_stable
                 add: progress_set_def lattice_stable stable closed_def
                      stable_Un [OF stable] dec [unfolded decoupled_def])
      have "F\<squnion>G ∈ (UNIV∩A) leadsTo B"
        by (rule progress_set_Union [OF leadsTo prog],
            simp_all del: Join_stable add: stable,
            simp add: stableco)
      thus ?thesis by simp
    qed

    text{*The ``Decoupling via @{term G'} Union Theorem''*}
    theorem decoupling_via_aux:
      assumes leadsTo: "F ∈ A leadsTo B"
          and prog: "{X. G' ∈ stable X} ∈ progress_set F UNIV B"
          and GG':  "G ≤ G'"
                   --{*Beware!  This is the converse of the refinement relation!*}
      shows "F\<squnion>G ∈ A leadsTo B"
    proof -
      from prog have stable: "G' ∈ stable B"
        by (simp add: progress_set_def)
      have "F\<squnion>G ∈ (UNIV∩A) leadsTo B"
        by (rule progress_set_Union [OF leadsTo prog],
            simp_all add: stable stableco component_stable [OF GG'])
      thus ?thesis by simp
    qed

    subsection{*Composition Theorems Based on Monotonicity and Commutativity*}

    subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
    constdefs
      commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
       "commutes F T B L ==
           ∀M. ∀act ∈ Acts F. B ⊆ M -->
               cl L (T ∩ wp act M) ⊆ T ∩ (B ∪ wp act (cl L (T∩M)))"

    text{*From Meier's thesis, section 4.5.6*}
    lemma commutativity1_lemma:
      assumes commutes: "commutes F T B L"
          and lattice:  "lattice L"
          and BL: "B ∈ L"
          and TL: "T ∈ L"
      shows "closed F T B L"
    apply (simp add: closed_def, clarify)
    apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
    apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
                     cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
    apply (subgoal_tac "cl L (T ∩ wp act M) ⊆ T ∩ (B ∪ wp act (cl L (T ∩ M)))")
     prefer 2
     apply (cut_tac commutes, simp add: commutes_def)
    apply (erule subset_trans)
    apply (simp add: cl_ident)
    apply (blast intro: rev_subsetD [OF _ wp_mono])
    done

    text{*Version packaged with @{thm progress_set_Union}*}
    lemma commutativity1:
      assumes leadsTo: "F ∈ A leadsTo B"
          and lattice:  "lattice L"
          and BL: "B ∈ L"
          and TL: "T ∈ L"
          and Fstable: "F ∈ stable T"
          and Gco: "!!X. X∈L ==> G ∈ X-B co X"
          and commutes: "commutes F T B L"
      shows "F\<squnion>G ∈ T∩A leadsTo B"
    by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
        simp add: progress_set_def commutativity1_lemma commutes lattice BL TL)

    text{*Possibly move to Relation.thy, after @{term single_valued}*}
    constdefs
      funof :: "[('a*'b)set, 'a] => 'b"
       "funof r == (λx. THE y. (x,y) ∈ r)"

    lemma funof_eq: "[|single_valued r; (x,y) ∈ r|] ==> funof r x = y"
    by (simp add: funof_def single_valued_def, blast)

    lemma funof_Pair_in:
         "[|single_valued r; x ∈ Domain r|] ==> (x, funof r x) ∈ r"
    by (force simp add: funof_eq)

    lemma funof_in:
         "[|r``{x} ⊆ A; single_valued r; x ∈ Domain r|] ==> funof r x ∈ A"
    by (force simp add: funof_eq)

    lemma funof_imp_wp: "[|funof act t ∈ A; single_valued act|] ==> t ∈ wp act A"
    by (force simp add: in_wp_iff funof_eq)

    subsubsection{*Commutativity of Functions and Relation*}
    text{*Thesis, page 109*}

    (*FIXME: this proof is an ungodly mess*)
    text{*From Meier's thesis, section 4.5.6*}
    lemma commutativity2_lemma:
      assumes dcommutes:
            "∀act ∈ Acts F.
             ∀s ∈ T. ∀t. (s,t) ∈ relcl L -->
                          s ∈ B | t ∈ B | (funof act s, funof act t) ∈ relcl L"
          and determ: "!!act. act ∈ Acts F ==> single_valued act"
          and total: "!!act. act ∈ Acts F ==> Domain act = UNIV"
          and lattice:  "lattice L"
          and BL: "B ∈ L"
          and TL: "T ∈ L"
          and Fstable: "F ∈ stable T"
      shows  "commutes F T B L"
    apply (simp add: commutes_def del: Int_subset_iff, clarify)
    apply (rename_tac t)
    apply (subgoal_tac "∃s. (s,t) ∈ relcl L & s ∈ T ∩ wp act M")
     prefer 2
     apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify)
    apply (subgoal_tac "∀u∈L. s ∈ u --> t ∈ u")
     prefer 2
     apply (intro ballI impI)
     apply (subst cl_ident [symmetric], assumption)
     apply (simp add: relcl_def)
     apply (blast intro: cl_mono [THEN [2] rev_subsetD])
    apply (subgoal_tac "funof act s ∈ T∩M")
     prefer 2
     apply (cut_tac Fstable)
     apply (force intro!: funof_in
                  simp add: wp_def stable_def constrains_def determ total)
    apply (subgoal_tac "s ∈ B | t ∈ B | (funof act s, funof act t) ∈ relcl L")
     prefer 2
     apply (rule dcommutes [rule_format], assumption+)
    apply (subgoal_tac "t ∈ B | funof act t ∈ cl L (T∩M)")
     prefer 2
     apply (simp add: relcl_def)
     apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])
    apply (subgoal_tac "t ∈ B | t ∈ wp act (cl L (T∩M))")
     prefer 2
     apply (blast intro: funof_imp_wp determ)
    apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])
    done

    text{*Version packaged with @{thm progress_set_Union}*}
    lemma commutativity2:
      assumes leadsTo: "F ∈ A leadsTo B"
          and dcommutes:
            "∀act ∈ Acts F.
             ∀s ∈ T. ∀t. (s,t) ∈ relcl L -->
                          s ∈ B | t ∈ B | (funof act s, funof act t) ∈ relcl L"
          and determ: "!!act. act ∈ Acts F ==> single_valued act"
          and total: "!!act. act ∈ Acts F ==> Domain act = UNIV"
          and lattice:  "lattice L"
          and BL: "B ∈ L"
          and TL: "T ∈ L"
          and Fstable: "F ∈ stable T"
          and Gco: "!!X. X∈L ==> G ∈ X-B co X"
      shows "F\<squnion>G ∈ T∩A leadsTo B"
    apply (rule commutativity1 [OF leadsTo lattice])
    apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
                         lattice BL TL Fstable)
    done

    subsection {*Monotonicity*}
    text{*From Meier's thesis, section 4.5.7, page 110*}
    (*to be continued?*)

    end

### Complete Lattices and the Operator @{term cl}

lemma UNIV_in_lattice:

      ProgressSets.lattice L ==> UNIV ∈ L

lemma empty_in_lattice:

      ProgressSets.lattice L ==> {} ∈ L

lemma Union_in_lattice:

      [| M ⊆ L; ProgressSets.lattice L |] ==> Union M ∈ L

lemma Inter_in_lattice:

      [| M ⊆ L; ProgressSets.lattice L |] ==> Inter M ∈ L

lemma UN_in_lattice:

      [| ProgressSets.lattice L; !!i. i ∈ I ==> r i ∈ L |] ==> (UN i:I. r i) ∈ L

lemma INT_in_lattice:

      [| ProgressSets.lattice L; !!i. i ∈ I ==> r i ∈ L |] ==> (INT i:I. r i) ∈ L

lemma Un_in_lattice:

      [| x ∈ L; y ∈ L; ProgressSets.lattice L |] ==> x ∪ y ∈ L

lemma Int_in_lattice:

      [| x ∈ L; y ∈ L; ProgressSets.lattice L |] ==> x ∩ y ∈ L

lemma lattice_stable:

      ProgressSets.lattice {X. F ∈ stable X}

lemma cl_in_lattice:

      ProgressSets.lattice L ==> cl L r ∈ L

lemma cl_least:

      [| c ∈ L; r ⊆ c |] ==> cl L r ⊆ c

lemma cl_mono:

      r ⊆ r' ==> cl L r ⊆ cl L r'

lemma subset_cl:

      r ⊆ cl L r

lemma clI:

      x ∈ r ==> x ∈ cl L r

lemma clD:

      [| c ∈ cl L r; B ∈ L; r ⊆ B |] ==> c ∈ B

lemma cl_UN_subset:

      (UN i:I. cl L (r i)) ⊆ cl L (UN i:I. r i)

lemma cl_Un:

      ProgressSets.lattice L ==> cl L (r ∪ s) = cl L r ∪ cl L s

lemma cl_UN:

      ProgressSets.lattice L ==> cl L (UN i:I. r i) = (UN i:I. cl L (r i))

lemma cl_Int_subset:

      cl L (r ∩ s) ⊆ cl L r ∩ cl L s

lemma cl_idem:

      cl L (cl L r) = cl L r

lemma cl_ident:

      r ∈ L ==> cl L r = r

lemma cl_empty:

      ProgressSets.lattice L ==> cl L {} = {}

lemma cl_UNIV:

      ProgressSets.lattice L ==> cl L UNIV = UNIV

lemma cl_ident_iff:

      ProgressSets.lattice L ==> (cl L r = r) = (r ∈ L)

lemma cl_subset_in_lattice:

      [| cl L r ⊆ r; ProgressSets.lattice L |] ==> r ∈ L

### Progress Sets and the Main Lemma

lemma closedD:

      [| closed F T B L; act ∈ Acts F; B ⊆ M; T ∩ M ∈ L |] ==> T ∩ (B ∪ wp act M) ∈ L

lemma lattice_awp_lemma:

      [| T ∩ X ∈ C; B ⊆ X; ProgressSets.lattice C; T ∈ C; B ∈ C; closed F T B C |]
      ==> T ∩ (B ∪ awp F (X ∪ cl C (T ∩ r))) ∈ C

lemma lattice_lemma:

      [| T ∩ X ∈ C; B ⊆ X; act ∈ Acts F; ProgressSets.lattice C; T ∈ C; B ∈ C;
         closed F T B C |]
      ==> T ∩ (wp act X ∩ awp F (X ∪ cl C (T ∩ r)) ∪ X) ∈ C

lemma progress_induction_step:

      [| T ∩ X ∈ C; act ∈ Acts F; X ∈ wens_set F B; ProgressSets.lattice C; T ∈ C;
         B ∈ C; closed F T B C; F ∈ stable T |]
      ==> T ∩ wens F act X ∈ C

lemma progress_set_lemma:

      [| C ∈ progress_set F T B; r ∈ wens_set F B; F ∈ stable T |] ==> T ∩ r ∈ C

### The Progress Set Union Theorem

lemma closed_mono:

      [| B ⊆ B'; T ∩ (B ∪ wp act M) ∈ C; B' ∈ C; T ∈ C; ProgressSets.lattice C |]
      ==> T ∩ (B' ∪ wp act M) ∈ C

lemma progress_set_mono:

      [| B ⊆ B'; B' ∈ C; C ∈ progress_set F T B |] ==> C ∈ progress_set F T B'

theorem progress_set_Union:

      [| F ∈ A leadsTo B'; C ∈ progress_set F T B; F ∈ stable T; B ⊆ B'; B' ∈ C;
         !!X. X ∈ C ==> G ∈ X - B co X |]
      ==> F Join G ∈ T ∩ A leadsTo B'

### Some Progress Sets

lemma UNIV_in_progress_set:

      UNIV ∈ progress_set F T B

#### Lattices and Relations

lemma relcl_refl:

      (a, a) ∈ relcl L

lemma relcl_trans:

      [| (a, b) ∈ relcl L; (b, c) ∈ relcl L; ProgressSets.lattice L |]
      ==> (a, c) ∈ relcl L

lemma refl_relcl:

      ProgressSets.lattice L ==> reflexive (relcl L)

lemma trans_relcl:

      ProgressSets.lattice L ==> trans (relcl L)

lemma lattice_latticeof:

      ProgressSets.lattice (latticeof r)

lemma lattice_singletonI:

      [| ProgressSets.lattice L; !!s. s ∈ X ==> {s} ∈ L |] ==> X ∈ L

lemma cl_latticeof:

      [| reflexive r; trans r |] ==> cl (latticeof r) X = {t. ∃s. s ∈ X ∧ (s, t) ∈ r}

lemma cl_eq_Collect_relcl:

      ProgressSets.lattice L ==> cl L X = {t. ∃s. s ∈ X ∧ (s, t) ∈ relcl L}

theorem latticeof_relcl_eq:

      ProgressSets.lattice L ==> latticeof (relcl L) = L

theorem relcl_latticeof_eq:

      [| reflexive r; trans r |] ==> relcl (latticeof r) = r

#### Decoupling Theorems

lemma stableco:

      F ∈ stable A ==> F ∈ A - B co A

theorem decoupling:

      [| F ∈ A leadsTo B; G ∈ stable B; decoupled F G |] ==> F Join G ∈ A leadsTo B

theorem weak_decoupling:

      [| F ∈ A leadsTo B; F Join G ∈ stable B; decoupled F (F Join G) |]
      ==> F Join G ∈ A leadsTo B

theorem decoupling_via_aux:

      [| F ∈ A leadsTo B; {X. G' ∈ stable X} ∈ progress_set F UNIV B; G ≤ G' |]
      ==> F Join G ∈ A leadsTo B

### Composition Theorems Based on Monotonicity and Commutativity

#### Commutativity of @{term "cl L"} and assignment.

lemma commutativity1_lemma:

      [| commutes F T B L; ProgressSets.lattice L; B ∈ L; T ∈ L |] ==> closed F T B L

lemma commutativity1:

      [| F ∈ A leadsTo B; ProgressSets.lattice L; B ∈ L; T ∈ L; F ∈ stable T;
         !!X. X ∈ L ==> G ∈ X - B co X; commutes F T B L |]
      ==> F Join G ∈ T ∩ A leadsTo B

lemma funof_eq:

      [| single_valued r; (x, y) ∈ r |] ==> funof r x = y

lemma funof_Pair_in:

      [| single_valued r; x ∈ Domain r |] ==> (x, funof r x) ∈ r

lemma funof_in:

      [| r `` {x} ⊆ A; single_valued r; x ∈ Domain r |] ==> funof r x ∈ A

lemma funof_imp_wp:

      [| funof act t ∈ A; single_valued act |] ==> t ∈ wp act A

#### Commutativity of Functions and Relation

lemma commutativity2_lemma:

      [| ∀act∈Acts F.
            ∀s∈T. ∀t. (s, t) ∈ relcl L -->
                      s ∈ B ∨ t ∈ B ∨ (funof act s, funof act t) ∈ relcl L;
         !!act. act ∈ Acts F ==> single_valued act;
         !!act. act ∈ Acts F ==> Domain act = UNIV; ProgressSets.lattice L; B ∈ L;
         T ∈ L; F ∈ stable T |]
      ==> commutes F T B L

lemma commutativity2:

      [| F ∈ A leadsTo B;
         ∀act∈Acts F.
            ∀s∈T. ∀t. (s, t) ∈ relcl L -->
                      s ∈ B ∨ t ∈ B ∨ (funof act s, funof act t) ∈ relcl L;
         !!act. act ∈ Acts F ==> single_valued act;
         !!act. act ∈ Acts F ==> Domain act = UNIV; ProgressSets.lattice L; B ∈ L;
         T ∈ L; F ∈ stable T; !!X. X ∈ L ==> G ∈ X - B co X |]
      ==> F Join G ∈ T ∩ A leadsTo B

### Monotonicity