More on progress sets
authorpaulson
Fri Mar 21 18:16:18 2003 +0100 (2003-03-21)
changeset 138740da2141606c6
parent 13873 f9f49a1ec0f2
child 13875 12997e3ddd8d
More on progress sets
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Transformers.thy
     1.1 --- a/src/HOL/UNITY/Comp.thy	Fri Mar 21 18:15:56 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Fri Mar 21 18:16:18 2003 +0100
     1.3 @@ -110,6 +110,9 @@
     1.4  lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
     1.5  by (auto simp add: constrains_def component_eq_subset)
     1.6  
     1.7 +lemma component_stable: "[| F \<le> G; G \<in> stable A |] ==> F \<in> stable A"
     1.8 +by (auto simp add: stable_def component_constrains)
     1.9 +
    1.10  (*Used in Guar.thy to show that programs are partially ordered*)
    1.11  lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
    1.12  
     2.1 --- a/src/HOL/UNITY/ProgressSets.thy	Fri Mar 21 18:15:56 2003 +0100
     2.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Fri Mar 21 18:16:18 2003 +0100
     2.3 @@ -85,6 +85,14 @@
     2.4  lemma subset_cl: "r \<subseteq> cl L r"
     2.5  by (simp add: cl_def, blast)
     2.6  
     2.7 +text{*A reformulation of @{thm subset_cl}*}
     2.8 +lemma clI: "x \<in> r ==> x \<in> cl L r"
     2.9 +by (simp add: cl_def, blast)
    2.10 +
    2.11 +text{*A reformulation of @{thm cl_least}*}
    2.12 +lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
    2.13 +by (force simp add: cl_def)
    2.14 +
    2.15  lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)"
    2.16  by (simp add: cl_def, blast)
    2.17  
    2.18 @@ -105,12 +113,21 @@
    2.19  apply (blast intro: subset_cl [THEN subsetD])  
    2.20  done
    2.21  
    2.22 +lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s"
    2.23 +by (simp add: cl_def, blast)
    2.24 +
    2.25  lemma cl_idem [simp]: "cl L (cl L r) = cl L r"
    2.26  by (simp add: cl_def, blast)
    2.27  
    2.28  lemma cl_ident: "r\<in>L ==> cl L r = r" 
    2.29  by (force simp add: cl_def)
    2.30  
    2.31 +lemma cl_empty [simp]: "lattice L ==> cl L {} = {}"
    2.32 +by (simp add: cl_ident empty_in_lattice)
    2.33 +
    2.34 +lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
    2.35 +by (simp add: cl_ident UNIV_in_lattice)
    2.36 +
    2.37  text{*Assertion (4.62)*}
    2.38  lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
    2.39  apply (rule iffI) 
    2.40 @@ -158,7 +175,7 @@
    2.41  apply (erule closedD [OF clos]) 
    2.42  apply (simp add: subset_trans [OF BsubX Un_upper1]) 
    2.43  apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)")
    2.44 - prefer 2 apply (blast intro: TC rev_subsetD [OF _ cl_least]) 
    2.45 + prefer 2 apply (blast intro: TC clD) 
    2.46  apply (erule ssubst) 
    2.47  apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
    2.48  done
    2.49 @@ -277,12 +294,12 @@
    2.50                   subset_trans [OF BB']) 
    2.51  
    2.52  theorem progress_set_Union:
    2.53 -  assumes prog: "C \<in> progress_set F T B"
    2.54 +  assumes leadsTo: "F \<in> A leadsTo B'"
    2.55 +      and prog: "C \<in> progress_set F T B"
    2.56        and Fstable: "F \<in> stable T"
    2.57        and BB':  "B \<subseteq> B'"
    2.58        and B'C:  "B' \<in> C"
    2.59        and Gco: "!!X. X\<in>C ==> G \<in> X-B co X"
    2.60 -      and leadsTo: "F \<in> A leadsTo B'"
    2.61    shows "F\<squnion>G \<in> T\<inter>A leadsTo B'"
    2.62  apply (insert prog Fstable) 
    2.63  apply (rule leadsTo_Join [OF leadsTo]) 
    2.64 @@ -299,4 +316,192 @@
    2.65  lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
    2.66  by (simp add: progress_set_def lattice_def closed_def)
    2.67  
    2.68 +
    2.69 +
    2.70 +subsubsection {*Derived Relation from a Lattice*}
    2.71 +text{*From Meier's thesis, section 4.5.3*}
    2.72 +
    2.73 +constdefs
    2.74 +  relcl :: "'a set set => ('a * 'a) set"
    2.75 +    "relcl L == {(x,y). y \<in> cl L {x}}"
    2.76 +
    2.77 +lemma relcl_refl: "(a,a) \<in> relcl L"
    2.78 +by (simp add: relcl_def subset_cl [THEN subsetD])
    2.79 +
    2.80 +lemma relcl_trans:
    2.81 +     "[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L"
    2.82 +apply (simp add: relcl_def)
    2.83 +apply (blast intro: clD cl_in_lattice)
    2.84 +done
    2.85 +
    2.86 +lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
    2.87 +by (simp add: reflI relcl_def subset_cl [THEN subsetD])
    2.88 +
    2.89 +lemma trans_relcl: "lattice L ==> trans (relcl L)"
    2.90 +by (blast intro: relcl_trans transI)
    2.91 +
    2.92 +text{*Related to equation (4.71) of Meier's thesis*}
    2.93 +lemma cl_eq_Collect_relcl:
    2.94 +     "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 
    2.95 +apply (cut_tac UN_singleton [of X, symmetric]) 
    2.96 +apply (erule ssubst) 
    2.97 +apply (force simp only: relcl_def cl_UN)
    2.98 +done
    2.99 +
   2.100 +
   2.101 +subsubsection {*Decoupling Theorems*}
   2.102 +
   2.103 +constdefs
   2.104 +  decoupled :: "['a program, 'a program] => bool"
   2.105 +   "decoupled F G ==
   2.106 +	\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
   2.107 +
   2.108 +
   2.109 +text{*Rao's Decoupling Theorem*}
   2.110 +lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
   2.111 +by (simp add: stable_def constrains_def, blast) 
   2.112 +
   2.113 +theorem decoupling:
   2.114 +  assumes leadsTo: "F \<in> A leadsTo B"
   2.115 +      and Gstable: "G \<in> stable B"
   2.116 +      and dec:     "decoupled F G"
   2.117 +  shows "F\<squnion>G \<in> A leadsTo B"
   2.118 +proof -
   2.119 +  have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B"
   2.120 +    by (simp add: progress_set_def lattice_stable Gstable closed_def
   2.121 +                  stable_Un [OF Gstable] dec [unfolded decoupled_def]) 
   2.122 +  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
   2.123 +    by (rule progress_set_Union [OF leadsTo prog],
   2.124 +        simp_all add: Gstable stableco)
   2.125 +  thus ?thesis by simp
   2.126 +qed
   2.127 +
   2.128 +
   2.129 +text{*Rao's Weak Decoupling Theorem*}
   2.130 +theorem weak_decoupling:
   2.131 +  assumes leadsTo: "F \<in> A leadsTo B"
   2.132 +      and stable: "F\<squnion>G \<in> stable B"
   2.133 +      and dec:     "decoupled F (F\<squnion>G)"
   2.134 +  shows "F\<squnion>G \<in> A leadsTo B"
   2.135 +proof -
   2.136 +  have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" 
   2.137 +    by (simp del: Join_stable
   2.138 +             add: progress_set_def lattice_stable stable closed_def
   2.139 +                  stable_Un [OF stable] dec [unfolded decoupled_def])
   2.140 +  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
   2.141 +    by (rule progress_set_Union [OF leadsTo prog],
   2.142 +        simp_all del: Join_stable add: stable,
   2.143 +        simp add: stableco) 
   2.144 +  thus ?thesis by simp
   2.145 +qed
   2.146 +
   2.147 +text{*The ``Decoupling via @{term G'} Union Theorem''*}
   2.148 +theorem decoupling_via_aux:
   2.149 +  assumes leadsTo: "F \<in> A leadsTo B"
   2.150 +      and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
   2.151 +      and GG':  "G \<le> G'"  
   2.152 +               --{*Beware!  This is the converse of the refinement relation!*}
   2.153 +  shows "F\<squnion>G \<in> A leadsTo B"
   2.154 +proof -
   2.155 +  from prog have stable: "G' \<in> stable B"
   2.156 +    by (simp add: progress_set_def)
   2.157 +  have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 
   2.158 +    by (rule progress_set_Union [OF leadsTo prog],
   2.159 +        simp_all add: stable stableco component_stable [OF GG'])
   2.160 +  thus ?thesis by simp
   2.161 +qed
   2.162 +
   2.163 +
   2.164 +subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
   2.165 +
   2.166 +constdefs 
   2.167 +  commutes :: "['a program, 'a set, 'a set,  'a set set] => bool"
   2.168 +   "commutes F T B L ==
   2.169 +       \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 
   2.170 +           cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
   2.171 +
   2.172 +
   2.173 +lemma commutativity1:
   2.174 +  assumes commutes: "commutes F T B L" 
   2.175 +      and lattice:  "lattice L"
   2.176 +      and BL: "B \<in> L"
   2.177 +      and TL: "T \<in> L"
   2.178 +  shows "closed F T B L"
   2.179 +apply (simp add: closed_def, clarify)
   2.180 +apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
   2.181 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
   2.182 +                 cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
   2.183 +apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
   2.184 + prefer 2 
   2.185 + apply (simp add: commutes [unfolded commutes_def]) 
   2.186 +apply (erule subset_trans) 
   2.187 +apply (simp add: cl_ident)
   2.188 +apply (blast intro: rev_subsetD [OF _ wp_mono]) 
   2.189 +done
   2.190 +
   2.191 +text{*Possibly move to Relation.thy, after @{term single_valued}*}
   2.192 +constdefs
   2.193 +  funof :: "[('a*'b)set, 'a] => 'b"
   2.194 +   "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
   2.195 +
   2.196 +lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y"
   2.197 +by (simp add: funof_def single_valued_def, blast)
   2.198 +
   2.199 +lemma funof_Pair_in:
   2.200 +     "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
   2.201 +by (force simp add: funof_eq) 
   2.202 +
   2.203 +lemma funof_in:
   2.204 +     "[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 
   2.205 +by (force simp add: funof_eq)
   2.206 + 
   2.207 +lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A"
   2.208 +by (force simp add: in_wp_iff funof_eq)
   2.209 +
   2.210 +
   2.211 +subsubsection{*Commutativity of Functions and Relation*}
   2.212 +text{*Thesis, page 109*}
   2.213 +
   2.214 +(*FIXME: this proof is an unGodly mess*)
   2.215 +lemma commutativity2:
   2.216 +  assumes dcommutes: 
   2.217 +        "\<forall>act \<in> Acts F. 
   2.218 +         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
   2.219 +                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
   2.220 +      and determ: "!!act. act \<in> Acts F ==> single_valued act"
   2.221 +      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
   2.222 +      and lattice:  "lattice L"
   2.223 +      and BL: "B \<in> L"
   2.224 +      and TL: "T \<in> L"
   2.225 +      and Fstable: "F \<in> stable T"
   2.226 +  shows  "commutes F T B L"
   2.227 +apply (simp add: commutes_def, clarify)  
   2.228 +apply (rename_tac t)
   2.229 +apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
   2.230 + prefer 2 apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp) 
   2.231 +apply clarify 
   2.232 +apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") 
   2.233 + prefer 2 
   2.234 + apply (intro ballI impI) 
   2.235 + apply (subst cl_ident [symmetric], assumption)
   2.236 + apply (simp add: relcl_def)  
   2.237 + apply (blast intro: cl_mono [THEN [2] rev_subsetD])  
   2.238 +apply (subgoal_tac "funof act s \<in> T\<inter>M") 
   2.239 + prefer 2 
   2.240 + apply (cut_tac Fstable) 
   2.241 + apply (force intro!: funof_in 
   2.242 +              simp add: wp_def stable_def constrains_def determ total) 
   2.243 +apply (subgoal_tac "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L")
   2.244 + prefer 2
   2.245 + apply (rule dcommutes [rule_format], assumption+) 
   2.246 +apply (subgoal_tac "t \<in> B | funof act t \<in> cl L (T\<inter>M)")
   2.247 + prefer 2 
   2.248 + apply (simp add: relcl_def)
   2.249 + apply (blast intro: BL cl_mono [THEN [2] rev_subsetD])  
   2.250 +apply (subgoal_tac "t \<in> B | t \<in> wp act (cl L (T\<inter>M))")
   2.251 + prefer 2
   2.252 + apply (blast intro: funof_imp_wp determ) 
   2.253 +apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])  
   2.254 +done
   2.255 +
   2.256  end
     3.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Mar 21 18:15:56 2003 +0100
     3.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Mar 21 18:16:18 2003 +0100
     3.3 @@ -38,6 +38,10 @@
     3.4  theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
     3.5  by (force simp add: wp_def) 
     3.6  
     3.7 +text{*This lemma is a good deal more intuitive than the definition!*}
     3.8 +lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
     3.9 +by (simp add: wp_def, blast)
    3.10 +
    3.11  lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    3.12  by (force simp add: wp_def) 
    3.13  
    3.14 @@ -70,6 +74,9 @@
    3.15  apply (simp add: awp_iff_stable) 
    3.16  done
    3.17  
    3.18 +lemma wp_mono: "(A \<subseteq> B) ==> wp act A \<subseteq> wp act B"
    3.19 +by (simp add: wp_def, blast)
    3.20 +
    3.21  lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    3.22  by (simp add: awp_def wp_def, blast)
    3.23