Quelle  ProgressSets.thy   Sprache: Isabelle

(*  Title:      HOL/UNITY/ProgressSets.thy
    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)
*)

section‹Progress Sets›

theory ProgressSets imports Transformers begin

subsection ‹Complete Lattices and the Operator 🍋‹cl››

definition lattice :: "'a set set => bool" where
   🍋 ‹Meier calls them closure sets, but they are just complete lattices›
   "lattice L ==
         (∀M. M ⊆ L --> ∩M ∈ L) & (∀M. M ⊆ L --> ∪M ∈ L)"

definition cl :: "['a set set, 'a set] => 'a set" where
   🍋 ‹short for ``closure''›
   "cl L r == \{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|] ==> \M \ L"
by (simp add: lattice_def)

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

lemma UN_in_lattice:
     "[|lattice L; !!i. i\I ==> r i \ L|] ==> (\i\I. r i) \ L"
apply (blast intro: Union_in_lattice) 
done

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

lemma Un_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
  using Union_in_lattice [of "{x, y}" L] by simp

lemma Int_in_lattice: "[|x\L; y\L; lattice L|] ==> x\y \ L"
  using Inter_in_lattice [of "{x, y}" L] by simp

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 🍋‹cl L r› is the minimal
 element of 🍋‹L› that includes 🍋‹r›.›
lemma cl_in_lattice: "lattice L ==> cl L r \ L"
  by (simp add: lattice_def cl_def)

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 le_Inf_iff)

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: "(\i\I. cl L (r i)) \ cl L (\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 (\i\I. r i) = (\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 🍋‹wens_set F B›.›

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

definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where
   "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 🍋‹m› by 🍋‹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 🍋‹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: 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
   🍋‹T=UNIV› states that every progress set for the program 🍋‹F›
   and set 🍋‹B› includes the set 🍋‹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 🍋‹wens› case›
 apply (simp add: progress_induction_step) 
txt‹Disjunctive case›
apply (subgoal_tac "(\U\W. T \ U) \ C") 
 apply simp 
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\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\

definition relcl :: "'a set set => ('a * 'a) set" where
    🍋 ‹Derived relation from a lattice›
    "relcl L == {(x,y). y \ cl L {x}}"
  
definition latticeof :: "('a * 'a) set => 'a set set" where
    🍋 ‹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 (relcl L)"
by (simp add: refl_onI 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 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_on_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 "_ \ 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 r; trans r|] ==> relcl (latticeof r) = r"
by (simp add: relcl_def cl_latticeof)


subsubsection ‹Decoupling Theorems›

definition decoupled :: "['a program, 'a program] => bool" where
   "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\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\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\G \ stable B"
      and dec:     "decoupled F (F\G)"
  shows "F\G \ A leadsTo B"
proof -
  have prog: "{X. F\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\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 🍋‹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\G \ A leadsTo B"
proof -
  from prog have stable: "G' \ stable B"
    by (simp add: progress_set_def)
  have "F\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 🍋‹cl L› and assignment.›
definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where
   "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] 
                 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\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 🍋‹single_valued››
definition funof :: "[('a*'b)set, 'a] => 'b" where
   "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 still an ungodly mess*)
text‹From Meier's thesis, section 4.5.6\
lemma commutativity2_lemma:
  assumes dcommutes: 
      "\act s t. act \ Acts F \ s \ 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"
proof -
  { fix M and act and t
    assume 1: "B \ M" "act \ Acts F" "t \ cl L (T \ wp act M)"
    then have "\s. (s,t) \ relcl L \ s \ T \ wp act M"
      by (force simp add: cl_eq_Collect_relcl [OF lattice])
    then obtain s where 2: "(s, t) \ relcl L" "s \ T" "s \ wp act M"
      by blast
    then have 3: "\u\L. s \ u --> t \ u"
      apply (intro ballI impI) 
      apply (subst cl_ident [symmetric], assumption)
      apply (simp add: relcl_def)  
      apply (blast intro: cl_mono [THEN [2] rev_subsetD])
      done
    with 1 2 Fstable have 4: "funof act s \ T\M"
      by (force intro!: funof_in 
        simp add: wp_def stable_def constrains_def determ total)
    with 1 2 3 have 5: "s \ B | t \ B | (funof act s, funof act t) \ relcl L"
      by (intro dcommutes) assumption+ 
    with 1 2 3 4 have "t \ B | funof act t \ cl L (T\M)"
      by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
    with 1 2 3 4 5 have "t \ B | t \ wp act (cl L (T\M))"
      by (blast intro: funof_imp_wp determ) 
    with 2 3 have "t \ T \ (t \ B \ t \ wp act (cl L (T \ M)))"
      by (blast intro: TL cl_mono [THEN [2] rev_subsetD])
    then have"t \ T \ (B \ wp act (cl L (T \ M)))"
      by simp
  }
  then show "commutes F T B L" unfolding commutes_def by clarify
qed
  
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\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