Theory ProgressSets
section‹Progress Sets›
theory ProgressSets imports Transformers begin
subsection ‹Complete Lattices and the Operator \<^term>‹cl››
definition lattice :: "'a set set => bool" where
"lattice L ==
(∀M. M ⊆ L --> ⋂M ∈ L) & (∀M. M ⊆ L --> ⋃M ∈ L)"
definition cl :: "['a set set, 'a set] => 'a set" where
"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 \<^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"
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 \<^term>‹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 \<^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"
and BsubX: "B ⊆ X"
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"
and BsubX: "B ⊆ X"
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"
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
\<^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 "(⋃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
"relcl L == {(x,y). y ∈ cl L {x}}"
definition latticeof :: "('a * 'a) set => 'a set set" where
"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 \<^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'"
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 \<^term>‹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 \<^term>‹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›
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›
end