author  haftmann 
Sun, 16 Mar 2014 18:09:04 +0100  
changeset 56166  9a241bc276cd 
parent 51488  3c886fe611b8 
child 58889  5b7a9633cfa8 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

1 
(* Title: HOL/UNITY/ProgressSets.thy 
13853  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 
Copyright 2003 University of Cambridge 

4 

5 
Progress Sets. From 

6 

7 
David Meier and Beverly Sanders, 

8 
Composing Leadsto Properties 

9 
Theoretical Computer Science 243:12 (2000), 339361. 

13861  10 

11 
David Meier, 

12 
Progress Properties in Program Refinement and Parallel Composition 

13 
Swiss Federal Institute of Technology Zurich (1997) 

13853  14 
*) 
15 

16 
header{*Progress Sets*} 

17 

16417  18 
theory ProgressSets imports Transformers begin 
13853  19 

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

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

22 
definition lattice :: "'a set set => bool" where 
13861  23 
{*Meier calls them closure sets, but they are just complete lattices*} 
24 
"lattice L == 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

25 
(\<forall>M. M \<subseteq> L > \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L > \<Union>M \<in> L)" 
13853  26 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

27 
definition cl :: "['a set set, 'a set] => 'a set" where 
13853  28 
{*short for ``closure''*} 
13861  29 
"cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}" 
13853  30 

13861  31 
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L" 
32 
by (force simp add: lattice_def) 

13853  33 

13861  34 
lemma empty_in_lattice: "lattice L ==> {} \<in> L" 
35 
by (force simp add: lattice_def) 

13853  36 

13861  37 
lemma Union_in_lattice: "[M \<subseteq> L; lattice L] ==> \<Union>M \<in> L" 
38 
by (simp add: lattice_def) 

13853  39 

13861  40 
lemma Inter_in_lattice: "[M \<subseteq> L; lattice L] ==> \<Inter>M \<in> L" 
41 
by (simp add: lattice_def) 

13853  42 

13861  43 
lemma UN_in_lattice: 
44 
"[lattice L; !!i. i\<in>I ==> r i \<in> L] ==> (\<Union>i\<in>I. r i) \<in> L" 

44106  45 
apply (unfold SUP_def) 
13861  46 
apply (blast intro: Union_in_lattice) 
13853  47 
done 
48 

13861  49 
lemma INT_in_lattice: 
50 
"[lattice L; !!i. i\<in>I ==> r i \<in> L] ==> (\<Inter>i\<in>I. r i) \<in> L" 

44106  51 
apply (unfold INF_def) 
13861  52 
apply (blast intro: Inter_in_lattice) 
13853  53 
done 
54 

13861  55 
lemma Un_in_lattice: "[x\<in>L; y\<in>L; lattice L] ==> x\<union>y \<in> L" 
44106  56 
using Union_in_lattice [of "{x, y}" L] by simp 
13853  57 

13861  58 
lemma Int_in_lattice: "[x\<in>L; y\<in>L; lattice L] ==> x\<inter>y \<in> L" 
44106  59 
using Inter_in_lattice [of "{x, y}" L] by simp 
13853  60 

13861  61 
lemma lattice_stable: "lattice {X. F \<in> stable X}" 
62 
by (simp add: lattice_def stable_def constrains_def, blast) 

13853  63 

13861  64 
text{*The next three results state that @{term "cl L r"} is the minimal 
65 
element of @{term L} that includes @{term r}.*} 

66 
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L" 

67 
apply (simp add: lattice_def cl_def) 

13853  68 
apply (erule conjE) 
69 
apply (drule spec, erule mp, blast) 

70 
done 

71 

13861  72 
lemma cl_least: "[c\<in>L; r\<subseteq>c] ==> cl L r \<subseteq> c" 
13853  73 
by (force simp add: cl_def) 
74 

75 
text{*The next three lemmas constitute assertion (4.61)*} 

13861  76 
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'" 
77 
by (simp add: cl_def, blast) 

78 

79 
lemma subset_cl: "r \<subseteq> cl L r" 

44918  80 
by (simp add: cl_def le_Inf_iff) 
13861  81 

13874  82 
text{*A reformulation of @{thm subset_cl}*} 
83 
lemma clI: "x \<in> r ==> x \<in> cl L r" 

84 
by (simp add: cl_def, blast) 

85 

86 
text{*A reformulation of @{thm cl_least}*} 

87 
lemma clD: "[c \<in> cl L r; B \<in> L; r \<subseteq> B] ==> c \<in> B" 

88 
by (force simp add: cl_def) 

89 

13861  90 
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)" 
13853  91 
by (simp add: cl_def, blast) 
92 

13861  93 
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s" 
94 
apply (rule equalityI) 

95 
prefer 2 

96 
apply (simp add: cl_def, blast) 

97 
apply (rule cl_least) 

98 
apply (blast intro: Un_in_lattice cl_in_lattice) 

99 
apply (blast intro: subset_cl [THEN subsetD]) 

100 
done 

13853  101 

13861  102 
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))" 
13853  103 
apply (rule equalityI) 
13866  104 
prefer 2 apply (simp add: cl_def, blast) 
13853  105 
apply (rule cl_least) 
13861  106 
apply (blast intro: UN_in_lattice cl_in_lattice) 
13853  107 
apply (blast intro: subset_cl [THEN subsetD]) 
108 
done 

109 

13874  110 
lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s" 
111 
by (simp add: cl_def, blast) 

112 

13861  113 
lemma cl_idem [simp]: "cl L (cl L r) = cl L r" 
13853  114 
by (simp add: cl_def, blast) 
115 

13861  116 
lemma cl_ident: "r\<in>L ==> cl L r = r" 
13853  117 
by (force simp add: cl_def) 
118 

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

121 

122 
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV" 

123 
by (simp add: cl_ident UNIV_in_lattice) 

124 

13853  125 
text{*Assertion (4.62)*} 
13861  126 
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
13853  127 
apply (rule iffI) 
128 
apply (erule subst) 

13861  129 
apply (erule cl_in_lattice) 
13853  130 
apply (erule cl_ident) 
131 
done 

132 

13861  133 
lemma cl_subset_in_lattice: "[cl L r \<subseteq> r; lattice L] ==> r\<in>L" 
134 
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl) 

135 

136 

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

13866  140 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

141 
definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where 
13861  142 
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L > 
143 
T \<inter> (B \<union> wp act M) \<in> L" 

144 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

145 
definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where 
13861  146 
"progress_set F T B == 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

147 
{L. lattice L & B \<in> L & T \<in> L & closed F T B L}" 
13861  148 

149 
lemma closedD: 

150 
"[closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L] 

14150  151 
==> T \<inter> (B \<union> wp act M) \<in> L" 
13861  152 
by (simp add: closed_def) 
153 

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

156 

157 
text{*Part of the proof of the claim at the bottom of page 97. It's 

158 
proved separately because the argument requires a generalization over 

159 
all @{term "act \<in> Acts F"}.*} 

13861  160 
lemma lattice_awp_lemma: 
13866  161 
assumes TXC: "T\<inter>X \<in> C" {*induction hypothesis in theorem below*} 
162 
and BsubX: "B \<subseteq> X" {*holds in inductive step*} 

13861  163 
and latt: "lattice C" 
13866  164 
and TC: "T \<in> C" 
165 
and BC: "B \<in> C" 

166 
and clos: "closed F T B C" 

167 
shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C" 

13861  168 
apply (simp del: INT_simps add: awp_def INT_extend_simps) 
169 
apply (rule INT_in_lattice [OF latt]) 

170 
apply (erule closedD [OF clos]) 

13866  171 
apply (simp add: subset_trans [OF BsubX Un_upper1]) 
172 
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)") 

13874  173 
prefer 2 apply (blast intro: TC clD) 
13861  174 
apply (erule ssubst) 
13866  175 
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
13861  176 
done 
177 

13866  178 
text{*Remainder of the proof of the claim at the bottom of page 97.*} 
13861  179 
lemma lattice_lemma: 
13866  180 
assumes TXC: "T\<inter>X \<in> C" {*induction hypothesis in theorem below*} 
181 
and BsubX: "B \<subseteq> X" {*holds in inductive step*} 

13861  182 
and act: "act \<in> Acts F" 
183 
and latt: "lattice C" 

13866  184 
and TC: "T \<in> C" 
185 
and BC: "B \<in> C" 

186 
and clos: "closed F T B C" 

187 
shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C" 

188 
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C") 

189 
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC) 

13861  190 
apply (drule Int_in_lattice 
13866  191 
[OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r] 
13861  192 
latt]) 
193 
apply (subgoal_tac 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

194 
"T \<inter> (B \<union> wp act X) \<inter> (T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r)))) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

195 
T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") 
13861  196 
prefer 2 apply blast 
197 
apply simp 

13866  198 
apply (drule Un_in_lattice [OF _ TXC latt]) 
13861  199 
apply (subgoal_tac 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

200 
"T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r))) \<union> T\<inter>X = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

201 
T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)") 
13866  202 
apply simp 
203 
apply (blast intro: BsubX [THEN subsetD]) 

13861  204 
done 
205 

206 

13866  207 
text{*Induction step for the main lemma*} 
13861  208 
lemma progress_induction_step: 
13866  209 
assumes TXC: "T\<inter>X \<in> C" {*induction hypothesis in theorem below*} 
13861  210 
and act: "act \<in> Acts F" 
13866  211 
and Xwens: "X \<in> wens_set F B" 
13861  212 
and latt: "lattice C" 
13866  213 
and TC: "T \<in> C" 
214 
and BC: "B \<in> C" 

215 
and clos: "closed F T B C" 

13861  216 
and Fstable: "F \<in> stable T" 
13866  217 
shows "T \<inter> wens F act X \<in> C" 
13861  218 
proof  
13866  219 
from Xwens have BsubX: "B \<subseteq> X" 
220 
by (rule wens_set_imp_subset) 

221 
let ?r = "wens F act X" 

222 
have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X" 

223 
by (simp add: wens_unfold [symmetric]) 

224 
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)" 

225 
by blast 

226 
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)" 

227 
by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) 

228 
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" 

229 
by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD]) 

230 
then have "cl C (T\<inter>?r) \<subseteq> 

231 
cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))" 

232 
by (rule cl_mono) 

233 
then have "cl C (T\<inter>?r) \<subseteq> 

234 
T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" 

235 
by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos]) 

236 
then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X" 

237 
by blast 

238 
then have "cl C (T\<inter>?r) \<subseteq> ?r" 

239 
by (blast intro!: subset_wens) 

240 
then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r" 

32693  241 
by (simp add: cl_ident TC 
13866  242 
subset_trans [OF cl_mono [OF Int_lower1]]) 
243 
show ?thesis 

244 
by (rule cl_subset_in_lattice [OF cl_subset latt]) 

13861  245 
qed 
246 

13888  247 
text{*Proved on page 96 of Meier's thesis. The special case when 
248 
@{term "T=UNIV"} states that every progress set for the program @{term F} 

249 
and set @{term B} includes the set @{term "wens_set F B"}.*} 

13861  250 
lemma progress_set_lemma: 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

251 
"[C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T] ==> T\<inter>r \<in> C" 
13861  252 
apply (simp add: progress_set_def, clarify) 
253 
apply (erule wens_set.induct) 

254 
txt{*Base*} 

255 
apply (simp add: Int_in_lattice) 

256 
txt{*The difficult @{term wens} case*} 

257 
apply (simp add: progress_induction_step) 

258 
txt{*Disjunctive case*} 

259 
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 

56166  260 
apply simp 
13861  261 
apply (blast intro: UN_in_lattice) 
262 
done 

263 

13866  264 

265 
subsection {*The Progress Set Union Theorem*} 

266 

267 
lemma closed_mono: 

268 
assumes BB': "B \<subseteq> B'" 

269 
and TBwp: "T \<inter> (B \<union> wp act M) \<in> C" 

270 
and B'C: "B' \<in> C" 

271 
and TC: "T \<in> C" 

272 
and latt: "lattice C" 

273 
shows "T \<inter> (B' \<union> wp act M) \<in> C" 

274 
proof  

275 
from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C" 

276 
by (simp add: Int_Un_distrib) 

277 
then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C" 

278 
by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) 

279 
show ?thesis 

280 
by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], 

281 
blast intro: BB' [THEN subsetD]) 

282 
qed 

283 

284 

285 
lemma progress_set_mono: 

286 
assumes BB': "B \<subseteq> B'" 

287 
shows 

288 
"[ B' \<in> C; C \<in> progress_set F T B] 

289 
==> C \<in> progress_set F T B'" 

290 
by (simp add: progress_set_def closed_def closed_mono [OF BB'] 

291 
subset_trans [OF BB']) 

292 

293 
theorem progress_set_Union: 

13874  294 
assumes leadsTo: "F \<in> A leadsTo B'" 
295 
and prog: "C \<in> progress_set F T B" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

296 
and Fstable: "F \<in> stable T" 
13866  297 
and BB': "B \<subseteq> B'" 
298 
and B'C: "B' \<in> C" 

299 
and Gco: "!!X. X\<in>C ==> G \<in> XB co X" 

300 
shows "F\<squnion>G \<in> T\<inter>A leadsTo B'" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

301 
apply (insert prog Fstable) 
13866  302 
apply (rule leadsTo_Join [OF leadsTo]) 
303 
apply (force simp add: progress_set_def awp_iff_stable [symmetric]) 

304 
apply (simp add: awp_iff_constrains) 

305 
apply (drule progress_set_mono [OF BB' B'C]) 

306 
apply (blast intro: progress_set_lemma Gco constrains_weaken_L 

307 
BB' [THEN subsetD]) 

308 
done 

309 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

310 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

311 
subsection {*Some Progress Sets*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

312 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

313 
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

314 
by (simp add: progress_set_def lattice_def closed_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset

315 

13874  316 

317 

13885  318 
subsubsection {*Lattices and Relations*} 
13874  319 
text{*From Meier's thesis, section 4.5.3*} 
320 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

321 
definition relcl :: "'a set set => ('a * 'a) set" where 
13885  322 
 {*Derived relation from a lattice*} 
13874  323 
"relcl L == {(x,y). y \<in> cl L {x}}" 
13885  324 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

325 
definition latticeof :: "('a * 'a) set => 'a set set" where 
13885  326 
 {*Derived lattice from a relation: the set of upwardsclosed sets*} 
327 
"latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r > t \<in> X}" 

328 

13874  329 

330 
lemma relcl_refl: "(a,a) \<in> relcl L" 

331 
by (simp add: relcl_def subset_cl [THEN subsetD]) 

332 

333 
lemma relcl_trans: 

334 
"[ (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L ] ==> (a,c) \<in> relcl L" 

335 
apply (simp add: relcl_def) 

336 
apply (blast intro: clD cl_in_lattice) 

337 
done 

338 

30198  339 
lemma refl_relcl: "lattice L ==> refl (relcl L)" 
340 
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD]) 

13874  341 

342 
lemma trans_relcl: "lattice L ==> trans (relcl L)" 

343 
by (blast intro: relcl_trans transI) 

344 

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

347 

348 
lemma lattice_singletonI: 

349 
"[lattice L; !!s. s \<in> X ==> {s} \<in> L] ==> X \<in> L" 

350 
apply (cut_tac UN_singleton [of X]) 

351 
apply (erule subst) 

352 
apply (simp only: UN_in_lattice) 

353 
done 

354 

355 
text{*Equation (4.71) of Meier's thesis. He gives no proof.*} 

356 
lemma cl_latticeof: 

30198  357 
"[refl r; trans r] 
13885  358 
==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
359 
apply (rule equalityI) 

360 
apply (rule cl_least) 

361 
apply (simp (no_asm_use) add: latticeof_def trans_def, blast) 

30198  362 
apply (simp add: latticeof_def refl_on_def, blast) 
13885  363 
apply (simp add: latticeof_def, clarify) 
364 
apply (unfold cl_def, blast) 

365 
done 

366 

367 
text{*Related to (4.71).*} 

13874  368 
lemma cl_eq_Collect_relcl: 
369 
"lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 

13885  370 
apply (cut_tac UN_singleton [of X]) 
371 
apply (erule subst) 

13874  372 
apply (force simp only: relcl_def cl_UN) 
373 
done 

374 

13885  375 
text{*Meier's theorem of section 4.5.3*} 
376 
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L" 

377 
apply (rule equalityI) 

378 
prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 

379 
apply (rename_tac X) 

380 
apply (rule cl_subset_in_lattice) 

381 
prefer 2 apply assumption 

382 
apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2]) 

383 
apply (drule equalityD1) 

384 
apply (rule subset_trans) 

385 
prefer 2 apply assumption 

386 
apply (thin_tac "?U \<subseteq> X") 

387 
apply (cut_tac A=X in UN_singleton) 

388 
apply (erule subst) 

389 
apply (simp only: cl_UN lattice_latticeof 

390 
cl_latticeof [OF refl_relcl trans_relcl]) 

391 
apply (simp add: relcl_def) 

392 
done 

393 

394 
theorem relcl_latticeof_eq: 

30198  395 
"[refl r; trans r] ==> relcl (latticeof r) = r" 
23767  396 
by (simp add: relcl_def cl_latticeof) 
13885  397 

13874  398 

399 
subsubsection {*Decoupling Theorems*} 

400 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

401 
definition decoupled :: "['a program, 'a program] => bool" where 
13874  402 
"decoupled F G == 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32693
diff
changeset

403 
\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B > G \<in> stable (wp act B)" 
13874  404 

405 

406 
text{*Rao's Decoupling Theorem*} 

407 
lemma stableco: "F \<in> stable A ==> F \<in> AB co A" 

408 
by (simp add: stable_def constrains_def, blast) 

409 

410 
theorem decoupling: 

411 
assumes leadsTo: "F \<in> A leadsTo B" 

412 
and Gstable: "G \<in> stable B" 

413 
and dec: "decoupled F G" 

414 
shows "F\<squnion>G \<in> A leadsTo B" 

415 
proof  

416 
have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B" 

417 
by (simp add: progress_set_def lattice_stable Gstable closed_def 

418 
stable_Un [OF Gstable] dec [unfolded decoupled_def]) 

419 
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 

420 
by (rule progress_set_Union [OF leadsTo prog], 

421 
simp_all add: Gstable stableco) 

422 
thus ?thesis by simp 

423 
qed 

424 

425 

426 
text{*Rao's Weak Decoupling Theorem*} 

427 
theorem weak_decoupling: 

428 
assumes leadsTo: "F \<in> A leadsTo B" 

429 
and stable: "F\<squnion>G \<in> stable B" 

430 
and dec: "decoupled F (F\<squnion>G)" 

431 
shows "F\<squnion>G \<in> A leadsTo B" 

432 
proof  

433 
have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" 

434 
by (simp del: Join_stable 

435 
add: progress_set_def lattice_stable stable closed_def 

436 
stable_Un [OF stable] dec [unfolded decoupled_def]) 

437 
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 

438 
by (rule progress_set_Union [OF leadsTo prog], 

439 
simp_all del: Join_stable add: stable, 

440 
simp add: stableco) 

441 
thus ?thesis by simp 

442 
qed 

443 

444 
text{*The ``Decoupling via @{term G'} Union Theorem''*} 

445 
theorem decoupling_via_aux: 

446 
assumes leadsTo: "F \<in> A leadsTo B" 

447 
and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B" 

448 
and GG': "G \<le> G'" 

449 
{*Beware! This is the converse of the refinement relation!*} 

450 
shows "F\<squnion>G \<in> A leadsTo B" 

451 
proof  

452 
from prog have stable: "G' \<in> stable B" 

453 
by (simp add: progress_set_def) 

454 
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" 

455 
by (rule progress_set_Union [OF leadsTo prog], 

456 
simp_all add: stable stableco component_stable [OF GG']) 

457 
thus ?thesis by simp 

458 
qed 

459 

460 

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

462 

13888  463 
subsubsection{*Commutativity of @{term "cl L"} and assignment.*} 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

464 
definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where 
13874  465 
"commutes F T B L == 
466 
\<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M > 

467 
cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" 

468 

469 

13888  470 
text{*From Meier's thesis, section 4.5.6*} 
13885  471 
lemma commutativity1_lemma: 
13874  472 
assumes commutes: "commutes F T B L" 
473 
and lattice: "lattice L" 

474 
and BL: "B \<in> L" 

475 
and TL: "T \<in> L" 

476 
shows "closed F T B L" 

477 
apply (simp add: closed_def, clarify) 

478 
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice]) 

32693  479 
apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
13874  480 
cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1) 
481 
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 

482 
prefer 2 

15102  483 
apply (cut_tac commutes, simp add: commutes_def) 
13874  484 
apply (erule subset_trans) 
485 
apply (simp add: cl_ident) 

486 
apply (blast intro: rev_subsetD [OF _ wp_mono]) 

487 
done 

488 

13888  489 
text{*Version packaged with @{thm progress_set_Union}*} 
13885  490 
lemma commutativity1: 
491 
assumes leadsTo: "F \<in> A leadsTo B" 

492 
and lattice: "lattice L" 

493 
and BL: "B \<in> L" 

494 
and TL: "T \<in> L" 

495 
and Fstable: "F \<in> stable T" 

496 
and Gco: "!!X. X\<in>L ==> G \<in> XB co X" 

497 
and commutes: "commutes F T B L" 

498 
shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 

499 
by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco], 

500 
simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) 

501 

502 

503 

13874  504 
text{*Possibly move to Relation.thy, after @{term single_valued}*} 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

505 
definition funof :: "[('a*'b)set, 'a] => 'b" where 
13874  506 
"funof r == (\<lambda>x. THE y. (x,y) \<in> r)" 
507 

508 
lemma funof_eq: "[single_valued r; (x,y) \<in> r] ==> funof r x = y" 

509 
by (simp add: funof_def single_valued_def, blast) 

510 

511 
lemma funof_Pair_in: 

512 
"[single_valued r; x \<in> Domain r] ==> (x, funof r x) \<in> r" 

513 
by (force simp add: funof_eq) 

514 

515 
lemma funof_in: 

516 
"[r``{x} \<subseteq> A; single_valued r; x \<in> Domain r] ==> funof r x \<in> A" 

517 
by (force simp add: funof_eq) 

518 

519 
lemma funof_imp_wp: "[funof act t \<in> A; single_valued act] ==> t \<in> wp act A" 

520 
by (force simp add: in_wp_iff funof_eq) 

521 

522 

523 
subsubsection{*Commutativity of Functions and Relation*} 

524 
text{*Thesis, page 109*} 

525 

32604  526 
(*FIXME: this proof is still an ungodly mess*) 
13888  527 
text{*From Meier's thesis, section 4.5.6*} 
13885  528 
lemma commutativity2_lemma: 
13874  529 
assumes dcommutes: 
45477  530 
"\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow> 
531 
s \<in> B  t \<in> B  (funof act s, funof act t) \<in> relcl L" 

532 
and determ: "!!act. act \<in> Acts F ==> single_valued act" 

533 
and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" 

534 
and lattice: "lattice L" 

535 
and BL: "B \<in> L" 

536 
and TL: "T \<in> L" 

537 
and Fstable: "F \<in> stable T" 

13874  538 
shows "commutes F T B L" 
32604  539 
proof  
51488  540 
{ fix M and act and t 
541 
assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" 

542 
then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" 

543 
by (force simp add: cl_eq_Collect_relcl [OF lattice]) 

544 
then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" 

545 
by blast 

546 
then have 3: "\<forall>u\<in>L. s \<in> u > t \<in> u" 

547 
apply (intro ballI impI) 

548 
apply (subst cl_ident [symmetric], assumption) 

549 
apply (simp add: relcl_def) 

550 
apply (blast intro: cl_mono [THEN [2] rev_subsetD]) 

551 
done 

552 
with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" 

553 
by (force intro!: funof_in 

554 
simp add: wp_def stable_def constrains_def determ total) 

555 
with 1 2 3 have 5: "s \<in> B  t \<in> B  (funof act s, funof act t) \<in> relcl L" 

556 
by (intro dcommutes) assumption+ 

557 
with 1 2 3 4 have "t \<in> B  funof act t \<in> cl L (T\<inter>M)" 

558 
by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) 

559 
with 1 2 3 4 5 have "t \<in> B  t \<in> wp act (cl L (T\<inter>M))" 

560 
by (blast intro: funof_imp_wp determ) 

561 
with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" 

562 
by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) 

563 
then have"t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" 

564 
by simp 

565 
} 

566 
then show "commutes F T B L" unfolding commutes_def by clarify 

32604  567 
qed 
568 

13888  569 
text{*Version packaged with @{thm progress_set_Union}*} 
13885  570 
lemma commutativity2: 
571 
assumes leadsTo: "F \<in> A leadsTo B" 

572 
and dcommutes: 

573 
"\<forall>act \<in> Acts F. 

574 
\<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L > 

575 
s \<in> B  t \<in> B  (funof act s, funof act t) \<in> relcl L" 

576 
and determ: "!!act. act \<in> Acts F ==> single_valued act" 

577 
and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" 

578 
and lattice: "lattice L" 

579 
and BL: "B \<in> L" 

580 
and TL: "T \<in> L" 

581 
and Fstable: "F \<in> stable T" 

582 
and Gco: "!!X. X\<in>L ==> G \<in> XB co X" 

583 
shows "F\<squnion>G \<in> T\<inter>A leadsTo B" 

584 
apply (rule commutativity1 [OF leadsTo lattice]) 

585 
apply (simp_all add: Gco commutativity2_lemma dcommutes determ total 

586 
lattice BL TL Fstable) 

587 
done 

588 

589 

13888  590 
subsection {*Monotonicity*} 
14150  591 
text{*From Meier's thesis, section 4.5.7, page 110*} 
13888  592 
(*to be continued?*) 
593 

13853  594 
end 