author | haftmann |
Tue, 22 Dec 2015 15:39:01 +0100 | |
changeset 61914 | 16bfe0a6702d |
parent 59807 | 22bc39064290 |
child 62343 | 24106dc44def |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 Leads-to Properties |
|
9 |
Theoretical Computer Science 243:1-2 (2000), 339-361. |
|
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 |
||
58889 | 16 |
section{*Progress Sets*} |
13853 | 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 tab-width;
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 tab-width;
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 tab-width;
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 tab-width;
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 tab-width;
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> X-B 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 upwards-closed 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 |
|
59807 | 386 |
apply (thin_tac "_ \<subseteq> X") |
13885 | 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 tab-width;
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> A-B 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> X-B 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> X-B 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 |