# HG changeset patch # User paulson # Date 1048266978 -3600 # Node ID 0da2141606c621456030544ba061c07d81ab8147 # Parent f9f49a1ec0f29d9eba16339cf7cbff0559ab9cfd More on progress sets diff -r f9f49a1ec0f2 -r 0da2141606c6 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Fri Mar 21 18:15:56 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Fri Mar 21 18:16:18 2003 +0100 @@ -110,6 +110,9 @@ lemma component_constrains: "[| F \ G; G \ A co B |] ==> F \ A co B" by (auto simp add: constrains_def component_eq_subset) +lemma component_stable: "[| F \ G; G \ stable A |] ==> F \ stable A" +by (auto simp add: stable_def component_constrains) + (*Used in Guar.thy to show that programs are partially ordered*) lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq] diff -r f9f49a1ec0f2 -r 0da2141606c6 src/HOL/UNITY/ProgressSets.thy --- a/src/HOL/UNITY/ProgressSets.thy Fri Mar 21 18:15:56 2003 +0100 +++ b/src/HOL/UNITY/ProgressSets.thy Fri Mar 21 18:16:18 2003 +0100 @@ -85,6 +85,14 @@ 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: "(\i\I. cl L (r i)) \ cl L (\i\I. r i)" by (simp add: cl_def, blast) @@ -105,12 +113,21 @@ 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) @@ -158,7 +175,7 @@ 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 rev_subsetD [OF _ cl_least]) + prefer 2 apply (blast intro: TC clD) apply (erule ssubst) apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) done @@ -277,12 +294,12 @@ subset_trans [OF BB']) theorem progress_set_Union: - assumes prog: "C \ progress_set F T B" + 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" - and leadsTo: "F \ A leadsTo B'" shows "F\G \ T\A leadsTo B'" apply (insert prog Fstable) apply (rule leadsTo_Join [OF leadsTo]) @@ -299,4 +316,192 @@ lemma UNIV_in_progress_set: "UNIV \ progress_set F T B" by (simp add: progress_set_def lattice_def closed_def) + + +subsubsection {*Derived Relation from a Lattice*} +text{*From Meier's thesis, section 4.5.3*} + +constdefs + relcl :: "'a set set => ('a * 'a) set" + "relcl L == {(x,y). y \ cl L {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) + +text{*Related to equation (4.71) of Meier's thesis*} +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, symmetric]) +apply (erule ssubst) +apply (force simp only: relcl_def cl_UN) +done + + +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\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'" + --{*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*} + +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)))" + + +lemma commutativity1: + 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 (simp add: commutes [unfolded commutes_def]) +apply (erule subset_trans) +apply (simp add: cl_ident) +apply (blast intro: rev_subsetD [OF _ wp_mono]) +done + +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*) +lemma commutativity2: + 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, 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) +apply 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 + end diff -r f9f49a1ec0f2 -r 0da2141606c6 src/HOL/UNITY/Transformers.thy --- a/src/HOL/UNITY/Transformers.thy Fri Mar 21 18:15:56 2003 +0100 +++ b/src/HOL/UNITY/Transformers.thy Fri Mar 21 18:16:18 2003 +0100 @@ -38,6 +38,10 @@ theorem wp_iff: "(A <= wp act B) = (act `` A <= B)" by (force simp add: wp_def) +text{*This lemma is a good deal more intuitive than the definition!*} +lemma in_wp_iff: "(a \ wp act B) = (\x. (a,x) \ act --> x \ B)" +by (simp add: wp_def, blast) + lemma Compl_Domain_subset_wp: "- (Domain act) \ wp act B" by (force simp add: wp_def) @@ -70,6 +74,9 @@ apply (simp add: awp_iff_stable) done +lemma wp_mono: "(A \ B) ==> wp act A \ wp act B" +by (simp add: wp_def, blast) + lemma awp_mono: "(A \ B) ==> awp F A \ awp F B" by (simp add: awp_def wp_def, blast)