author | haftmann |
Fri, 10 Dec 2010 16:10:50 +0100 | |
changeset 41107 | 8795cd75965e |
parent 35416 | d8d7d1b785af |
child 44106 | 0e018cbcc0de |
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 |
||
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 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" |
|
32139 | 45 |
apply (simp add: UN_eq) |
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" |
|
13853 | 51 |
apply (simp add: INT_eq) |
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" |
13853 | 56 |
apply (simp only: Un_eq_Union) |
13861 | 57 |
apply (blast intro: Union_in_lattice) |
13853 | 58 |
done |
59 |
||
13861 | 60 |
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L" |
13853 | 61 |
apply (simp only: Int_eq_Inter) |
13861 | 62 |
apply (blast intro: Inter_in_lattice) |
13853 | 63 |
done |
64 |
||
13861 | 65 |
lemma lattice_stable: "lattice {X. F \<in> stable X}" |
66 |
by (simp add: lattice_def stable_def constrains_def, blast) |
|
13853 | 67 |
|
13861 | 68 |
text{*The next three results state that @{term "cl L r"} is the minimal |
69 |
element of @{term L} that includes @{term r}.*} |
|
70 |
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L" |
|
71 |
apply (simp add: lattice_def cl_def) |
|
13853 | 72 |
apply (erule conjE) |
73 |
apply (drule spec, erule mp, blast) |
|
74 |
done |
|
75 |
||
13861 | 76 |
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" |
13853 | 77 |
by (force simp add: cl_def) |
78 |
||
79 |
text{*The next three lemmas constitute assertion (4.61)*} |
|
13861 | 80 |
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'" |
81 |
by (simp add: cl_def, blast) |
|
82 |
||
83 |
lemma subset_cl: "r \<subseteq> cl L r" |
|
84 |
by (simp add: cl_def, blast) |
|
85 |
||
13874 | 86 |
text{*A reformulation of @{thm subset_cl}*} |
87 |
lemma clI: "x \<in> r ==> x \<in> cl L r" |
|
88 |
by (simp add: cl_def, blast) |
|
89 |
||
90 |
text{*A reformulation of @{thm cl_least}*} |
|
91 |
lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B" |
|
92 |
by (force simp add: cl_def) |
|
93 |
||
13861 | 94 |
lemma cl_UN_subset: "(\<Union>i\<in>I. cl L (r i)) \<subseteq> cl L (\<Union>i\<in>I. r i)" |
13853 | 95 |
by (simp add: cl_def, blast) |
96 |
||
13861 | 97 |
lemma cl_Un: "lattice L ==> cl L (r\<union>s) = cl L r \<union> cl L s" |
98 |
apply (rule equalityI) |
|
99 |
prefer 2 |
|
100 |
apply (simp add: cl_def, blast) |
|
101 |
apply (rule cl_least) |
|
102 |
apply (blast intro: Un_in_lattice cl_in_lattice) |
|
103 |
apply (blast intro: subset_cl [THEN subsetD]) |
|
104 |
done |
|
13853 | 105 |
|
13861 | 106 |
lemma cl_UN: "lattice L ==> cl L (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl L (r i))" |
13853 | 107 |
apply (rule equalityI) |
13866 | 108 |
prefer 2 apply (simp add: cl_def, blast) |
13853 | 109 |
apply (rule cl_least) |
13861 | 110 |
apply (blast intro: UN_in_lattice cl_in_lattice) |
13853 | 111 |
apply (blast intro: subset_cl [THEN subsetD]) |
112 |
done |
|
113 |
||
13874 | 114 |
lemma cl_Int_subset: "cl L (r\<inter>s) \<subseteq> cl L r \<inter> cl L s" |
115 |
by (simp add: cl_def, blast) |
|
116 |
||
13861 | 117 |
lemma cl_idem [simp]: "cl L (cl L r) = cl L r" |
13853 | 118 |
by (simp add: cl_def, blast) |
119 |
||
13861 | 120 |
lemma cl_ident: "r\<in>L ==> cl L r = r" |
13853 | 121 |
by (force simp add: cl_def) |
122 |
||
13874 | 123 |
lemma cl_empty [simp]: "lattice L ==> cl L {} = {}" |
124 |
by (simp add: cl_ident empty_in_lattice) |
|
125 |
||
126 |
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV" |
|
127 |
by (simp add: cl_ident UNIV_in_lattice) |
|
128 |
||
13853 | 129 |
text{*Assertion (4.62)*} |
13861 | 130 |
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" |
13853 | 131 |
apply (rule iffI) |
132 |
apply (erule subst) |
|
13861 | 133 |
apply (erule cl_in_lattice) |
13853 | 134 |
apply (erule cl_ident) |
135 |
done |
|
136 |
||
13861 | 137 |
lemma cl_subset_in_lattice: "[|cl L r \<subseteq> r; lattice L|] ==> r\<in>L" |
138 |
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl) |
|
139 |
||
140 |
||
13866 | 141 |
subsection {*Progress Sets and the Main Lemma*} |
13888 | 142 |
text{*A progress set satisfies certain closure conditions and is a |
143 |
simple way of including the set @{term "wens_set F B"}.*} |
|
13866 | 144 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
145 |
definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where |
13861 | 146 |
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L --> |
147 |
T \<inter> (B \<union> wp act M) \<in> L" |
|
148 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
149 |
definition progress_set :: "['a program, 'a set, 'a set] => 'a set set set" where |
13861 | 150 |
"progress_set F T B == |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
151 |
{L. lattice L & B \<in> L & T \<in> L & closed F T B L}" |
13861 | 152 |
|
153 |
lemma closedD: |
|
154 |
"[|closed F T B L; act \<in> Acts F; B\<subseteq>M; T\<inter>M \<in> L|] |
|
14150 | 155 |
==> T \<inter> (B \<union> wp act M) \<in> L" |
13861 | 156 |
by (simp add: closed_def) |
157 |
||
13866 | 158 |
text{*Note: the formalization below replaces Meier's @{term q} by @{term B} |
159 |
and @{term m} by @{term X}. *} |
|
160 |
||
161 |
text{*Part of the proof of the claim at the bottom of page 97. It's |
|
162 |
proved separately because the argument requires a generalization over |
|
163 |
all @{term "act \<in> Acts F"}.*} |
|
13861 | 164 |
lemma lattice_awp_lemma: |
13866 | 165 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
166 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*} |
|
13861 | 167 |
and latt: "lattice C" |
13866 | 168 |
and TC: "T \<in> C" |
169 |
and BC: "B \<in> C" |
|
170 |
and clos: "closed F T B C" |
|
171 |
shows "T \<inter> (B \<union> awp F (X \<union> cl C (T\<inter>r))) \<in> C" |
|
13861 | 172 |
apply (simp del: INT_simps add: awp_def INT_extend_simps) |
173 |
apply (rule INT_in_lattice [OF latt]) |
|
174 |
apply (erule closedD [OF clos]) |
|
13866 | 175 |
apply (simp add: subset_trans [OF BsubX Un_upper1]) |
176 |
apply (subgoal_tac "T \<inter> (X \<union> cl C (T\<inter>r)) = (T\<inter>X) \<union> cl C (T\<inter>r)") |
|
13874 | 177 |
prefer 2 apply (blast intro: TC clD) |
13861 | 178 |
apply (erule ssubst) |
13866 | 179 |
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) |
13861 | 180 |
done |
181 |
||
13866 | 182 |
text{*Remainder of the proof of the claim at the bottom of page 97.*} |
13861 | 183 |
lemma lattice_lemma: |
13866 | 184 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
185 |
and BsubX: "B \<subseteq> X" --{*holds in inductive step*} |
|
13861 | 186 |
and act: "act \<in> Acts F" |
187 |
and latt: "lattice C" |
|
13866 | 188 |
and TC: "T \<in> C" |
189 |
and BC: "B \<in> C" |
|
190 |
and clos: "closed F T B C" |
|
191 |
shows "T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X) \<in> C" |
|
192 |
apply (subgoal_tac "T \<inter> (B \<union> wp act X) \<in> C") |
|
193 |
prefer 2 apply (simp add: closedD [OF clos] act BsubX TXC) |
|
13861 | 194 |
apply (drule Int_in_lattice |
13866 | 195 |
[OF _ lattice_awp_lemma [OF TXC BsubX latt TC BC clos, of r] |
13861 | 196 |
latt]) |
197 |
apply (subgoal_tac |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32693
diff
changeset
|
198 |
"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
|
199 |
T \<inter> (B \<union> wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)))") |
13861 | 200 |
prefer 2 apply blast |
201 |
apply simp |
|
13866 | 202 |
apply (drule Un_in_lattice [OF _ TXC latt]) |
13861 | 203 |
apply (subgoal_tac |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32693
diff
changeset
|
204 |
"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
|
205 |
T \<inter> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>r)) \<union> X)") |
13866 | 206 |
apply simp |
207 |
apply (blast intro: BsubX [THEN subsetD]) |
|
13861 | 208 |
done |
209 |
||
210 |
||
13866 | 211 |
text{*Induction step for the main lemma*} |
13861 | 212 |
lemma progress_induction_step: |
13866 | 213 |
assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*} |
13861 | 214 |
and act: "act \<in> Acts F" |
13866 | 215 |
and Xwens: "X \<in> wens_set F B" |
13861 | 216 |
and latt: "lattice C" |
13866 | 217 |
and TC: "T \<in> C" |
218 |
and BC: "B \<in> C" |
|
219 |
and clos: "closed F T B C" |
|
13861 | 220 |
and Fstable: "F \<in> stable T" |
13866 | 221 |
shows "T \<inter> wens F act X \<in> C" |
13861 | 222 |
proof - |
13866 | 223 |
from Xwens have BsubX: "B \<subseteq> X" |
224 |
by (rule wens_set_imp_subset) |
|
225 |
let ?r = "wens F act X" |
|
226 |
have "?r \<subseteq> (wp act X \<inter> awp F (X\<union>?r)) \<union> X" |
|
227 |
by (simp add: wens_unfold [symmetric]) |
|
228 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X\<union>?r)) \<union> X)" |
|
229 |
by blast |
|
230 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (T \<inter> (X\<union>?r))) \<union> X)" |
|
231 |
by (simp add: awp_Int_eq Fstable stable_imp_awp_ident, blast) |
|
232 |
then have "T\<inter>?r \<subseteq> T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" |
|
233 |
by (blast intro: awp_mono [THEN [2] rev_subsetD] subset_cl [THEN subsetD]) |
|
234 |
then have "cl C (T\<inter>?r) \<subseteq> |
|
235 |
cl C (T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X))" |
|
236 |
by (rule cl_mono) |
|
237 |
then have "cl C (T\<inter>?r) \<subseteq> |
|
238 |
T \<inter> ((wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X)" |
|
239 |
by (simp add: cl_ident lattice_lemma [OF TXC BsubX act latt TC BC clos]) |
|
240 |
then have "cl C (T\<inter>?r) \<subseteq> (wp act X \<inter> awp F (X \<union> cl C (T\<inter>?r))) \<union> X" |
|
241 |
by blast |
|
242 |
then have "cl C (T\<inter>?r) \<subseteq> ?r" |
|
243 |
by (blast intro!: subset_wens) |
|
244 |
then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r" |
|
32693 | 245 |
by (simp add: cl_ident TC |
13866 | 246 |
subset_trans [OF cl_mono [OF Int_lower1]]) |
247 |
show ?thesis |
|
248 |
by (rule cl_subset_in_lattice [OF cl_subset latt]) |
|
13861 | 249 |
qed |
250 |
||
13888 | 251 |
text{*Proved on page 96 of Meier's thesis. The special case when |
252 |
@{term "T=UNIV"} states that every progress set for the program @{term F} |
|
253 |
and set @{term B} includes the set @{term "wens_set F B"}.*} |
|
13861 | 254 |
lemma progress_set_lemma: |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
255 |
"[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C" |
13861 | 256 |
apply (simp add: progress_set_def, clarify) |
257 |
apply (erule wens_set.induct) |
|
258 |
txt{*Base*} |
|
259 |
apply (simp add: Int_in_lattice) |
|
260 |
txt{*The difficult @{term wens} case*} |
|
261 |
apply (simp add: progress_induction_step) |
|
262 |
txt{*Disjunctive case*} |
|
263 |
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") |
|
264 |
apply (simp add: Int_Union) |
|
265 |
apply (blast intro: UN_in_lattice) |
|
266 |
done |
|
267 |
||
13866 | 268 |
|
269 |
subsection {*The Progress Set Union Theorem*} |
|
270 |
||
271 |
lemma closed_mono: |
|
272 |
assumes BB': "B \<subseteq> B'" |
|
273 |
and TBwp: "T \<inter> (B \<union> wp act M) \<in> C" |
|
274 |
and B'C: "B' \<in> C" |
|
275 |
and TC: "T \<in> C" |
|
276 |
and latt: "lattice C" |
|
277 |
shows "T \<inter> (B' \<union> wp act M) \<in> C" |
|
278 |
proof - |
|
279 |
from TBwp have "(T\<inter>B) \<union> (T \<inter> wp act M) \<in> C" |
|
280 |
by (simp add: Int_Un_distrib) |
|
281 |
then have TBBC: "(T\<inter>B') \<union> ((T\<inter>B) \<union> (T \<inter> wp act M)) \<in> C" |
|
282 |
by (blast intro: Int_in_lattice Un_in_lattice TC B'C latt) |
|
283 |
show ?thesis |
|
284 |
by (rule eqelem_imp_iff [THEN iffD1, OF _ TBBC], |
|
285 |
blast intro: BB' [THEN subsetD]) |
|
286 |
qed |
|
287 |
||
288 |
||
289 |
lemma progress_set_mono: |
|
290 |
assumes BB': "B \<subseteq> B'" |
|
291 |
shows |
|
292 |
"[| B' \<in> C; C \<in> progress_set F T B|] |
|
293 |
==> C \<in> progress_set F T B'" |
|
294 |
by (simp add: progress_set_def closed_def closed_mono [OF BB'] |
|
295 |
subset_trans [OF BB']) |
|
296 |
||
297 |
theorem progress_set_Union: |
|
13874 | 298 |
assumes leadsTo: "F \<in> A leadsTo B'" |
299 |
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
|
300 |
and Fstable: "F \<in> stable T" |
13866 | 301 |
and BB': "B \<subseteq> B'" |
302 |
and B'C: "B' \<in> C" |
|
303 |
and Gco: "!!X. X\<in>C ==> G \<in> X-B co X" |
|
304 |
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
|
305 |
apply (insert prog Fstable) |
13866 | 306 |
apply (rule leadsTo_Join [OF leadsTo]) |
307 |
apply (force simp add: progress_set_def awp_iff_stable [symmetric]) |
|
308 |
apply (simp add: awp_iff_constrains) |
|
309 |
apply (drule progress_set_mono [OF BB' B'C]) |
|
310 |
apply (blast intro: progress_set_lemma Gco constrains_weaken_L |
|
311 |
BB' [THEN subsetD]) |
|
312 |
done |
|
313 |
||
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
314 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
315 |
subsection {*Some Progress Sets*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
316 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13866
diff
changeset
|
317 |
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
|
318 |
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
|
319 |
|
13874 | 320 |
|
321 |
||
13885 | 322 |
subsubsection {*Lattices and Relations*} |
13874 | 323 |
text{*From Meier's thesis, section 4.5.3*} |
324 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
325 |
definition relcl :: "'a set set => ('a * 'a) set" where |
13885 | 326 |
-- {*Derived relation from a lattice*} |
13874 | 327 |
"relcl L == {(x,y). y \<in> cl L {x}}" |
13885 | 328 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
329 |
definition latticeof :: "('a * 'a) set => 'a set set" where |
13885 | 330 |
-- {*Derived lattice from a relation: the set of upwards-closed sets*} |
331 |
"latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}" |
|
332 |
||
13874 | 333 |
|
334 |
lemma relcl_refl: "(a,a) \<in> relcl L" |
|
335 |
by (simp add: relcl_def subset_cl [THEN subsetD]) |
|
336 |
||
337 |
lemma relcl_trans: |
|
338 |
"[| (a,b) \<in> relcl L; (b,c) \<in> relcl L; lattice L |] ==> (a,c) \<in> relcl L" |
|
339 |
apply (simp add: relcl_def) |
|
340 |
apply (blast intro: clD cl_in_lattice) |
|
341 |
done |
|
342 |
||
30198 | 343 |
lemma refl_relcl: "lattice L ==> refl (relcl L)" |
344 |
by (simp add: refl_onI relcl_def subset_cl [THEN subsetD]) |
|
13874 | 345 |
|
346 |
lemma trans_relcl: "lattice L ==> trans (relcl L)" |
|
347 |
by (blast intro: relcl_trans transI) |
|
348 |
||
13885 | 349 |
lemma lattice_latticeof: "lattice (latticeof r)" |
350 |
by (auto simp add: lattice_def latticeof_def) |
|
351 |
||
352 |
lemma lattice_singletonI: |
|
353 |
"[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L" |
|
354 |
apply (cut_tac UN_singleton [of X]) |
|
355 |
apply (erule subst) |
|
356 |
apply (simp only: UN_in_lattice) |
|
357 |
done |
|
358 |
||
359 |
text{*Equation (4.71) of Meier's thesis. He gives no proof.*} |
|
360 |
lemma cl_latticeof: |
|
30198 | 361 |
"[|refl r; trans r|] |
13885 | 362 |
==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" |
363 |
apply (rule equalityI) |
|
364 |
apply (rule cl_least) |
|
365 |
apply (simp (no_asm_use) add: latticeof_def trans_def, blast) |
|
30198 | 366 |
apply (simp add: latticeof_def refl_on_def, blast) |
13885 | 367 |
apply (simp add: latticeof_def, clarify) |
368 |
apply (unfold cl_def, blast) |
|
369 |
done |
|
370 |
||
371 |
text{*Related to (4.71).*} |
|
13874 | 372 |
lemma cl_eq_Collect_relcl: |
373 |
"lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" |
|
13885 | 374 |
apply (cut_tac UN_singleton [of X]) |
375 |
apply (erule subst) |
|
13874 | 376 |
apply (force simp only: relcl_def cl_UN) |
377 |
done |
|
378 |
||
13885 | 379 |
text{*Meier's theorem of section 4.5.3*} |
380 |
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L" |
|
381 |
apply (rule equalityI) |
|
382 |
prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) |
|
383 |
apply (rename_tac X) |
|
384 |
apply (rule cl_subset_in_lattice) |
|
385 |
prefer 2 apply assumption |
|
386 |
apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2]) |
|
387 |
apply (drule equalityD1) |
|
388 |
apply (rule subset_trans) |
|
389 |
prefer 2 apply assumption |
|
390 |
apply (thin_tac "?U \<subseteq> X") |
|
391 |
apply (cut_tac A=X in UN_singleton) |
|
392 |
apply (erule subst) |
|
393 |
apply (simp only: cl_UN lattice_latticeof |
|
394 |
cl_latticeof [OF refl_relcl trans_relcl]) |
|
395 |
apply (simp add: relcl_def) |
|
396 |
done |
|
397 |
||
398 |
theorem relcl_latticeof_eq: |
|
30198 | 399 |
"[|refl r; trans r|] ==> relcl (latticeof r) = r" |
23767 | 400 |
by (simp add: relcl_def cl_latticeof) |
13885 | 401 |
|
13874 | 402 |
|
403 |
subsubsection {*Decoupling Theorems*} |
|
404 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
405 |
definition decoupled :: "['a program, 'a program] => bool" where |
13874 | 406 |
"decoupled F G == |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32693
diff
changeset
|
407 |
\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)" |
13874 | 408 |
|
409 |
||
410 |
text{*Rao's Decoupling Theorem*} |
|
411 |
lemma stableco: "F \<in> stable A ==> F \<in> A-B co A" |
|
412 |
by (simp add: stable_def constrains_def, blast) |
|
413 |
||
414 |
theorem decoupling: |
|
415 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
416 |
and Gstable: "G \<in> stable B" |
|
417 |
and dec: "decoupled F G" |
|
418 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
419 |
proof - |
|
420 |
have prog: "{X. G \<in> stable X} \<in> progress_set F UNIV B" |
|
421 |
by (simp add: progress_set_def lattice_stable Gstable closed_def |
|
422 |
stable_Un [OF Gstable] dec [unfolded decoupled_def]) |
|
423 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
424 |
by (rule progress_set_Union [OF leadsTo prog], |
|
425 |
simp_all add: Gstable stableco) |
|
426 |
thus ?thesis by simp |
|
427 |
qed |
|
428 |
||
429 |
||
430 |
text{*Rao's Weak Decoupling Theorem*} |
|
431 |
theorem weak_decoupling: |
|
432 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
433 |
and stable: "F\<squnion>G \<in> stable B" |
|
434 |
and dec: "decoupled F (F\<squnion>G)" |
|
435 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
436 |
proof - |
|
437 |
have prog: "{X. F\<squnion>G \<in> stable X} \<in> progress_set F UNIV B" |
|
438 |
by (simp del: Join_stable |
|
439 |
add: progress_set_def lattice_stable stable closed_def |
|
440 |
stable_Un [OF stable] dec [unfolded decoupled_def]) |
|
441 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
442 |
by (rule progress_set_Union [OF leadsTo prog], |
|
443 |
simp_all del: Join_stable add: stable, |
|
444 |
simp add: stableco) |
|
445 |
thus ?thesis by simp |
|
446 |
qed |
|
447 |
||
448 |
text{*The ``Decoupling via @{term G'} Union Theorem''*} |
|
449 |
theorem decoupling_via_aux: |
|
450 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
451 |
and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B" |
|
452 |
and GG': "G \<le> G'" |
|
453 |
--{*Beware! This is the converse of the refinement relation!*} |
|
454 |
shows "F\<squnion>G \<in> A leadsTo B" |
|
455 |
proof - |
|
456 |
from prog have stable: "G' \<in> stable B" |
|
457 |
by (simp add: progress_set_def) |
|
458 |
have "F\<squnion>G \<in> (UNIV\<inter>A) leadsTo B" |
|
459 |
by (rule progress_set_Union [OF leadsTo prog], |
|
460 |
simp_all add: stable stableco component_stable [OF GG']) |
|
461 |
thus ?thesis by simp |
|
462 |
qed |
|
463 |
||
464 |
||
465 |
subsection{*Composition Theorems Based on Monotonicity and Commutativity*} |
|
466 |
||
13888 | 467 |
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
|
468 |
definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where |
13874 | 469 |
"commutes F T B L == |
470 |
\<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> |
|
471 |
cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))" |
|
472 |
||
473 |
||
13888 | 474 |
text{*From Meier's thesis, section 4.5.6*} |
13885 | 475 |
lemma commutativity1_lemma: |
13874 | 476 |
assumes commutes: "commutes F T B L" |
477 |
and lattice: "lattice L" |
|
478 |
and BL: "B \<in> L" |
|
479 |
and TL: "T \<in> L" |
|
480 |
shows "closed F T B L" |
|
481 |
apply (simp add: closed_def, clarify) |
|
482 |
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice]) |
|
32693 | 483 |
apply (simp add: Int_Un_distrib cl_Un [OF lattice] |
13874 | 484 |
cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1) |
485 |
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") |
|
486 |
prefer 2 |
|
15102 | 487 |
apply (cut_tac commutes, simp add: commutes_def) |
13874 | 488 |
apply (erule subset_trans) |
489 |
apply (simp add: cl_ident) |
|
490 |
apply (blast intro: rev_subsetD [OF _ wp_mono]) |
|
491 |
done |
|
492 |
||
13888 | 493 |
text{*Version packaged with @{thm progress_set_Union}*} |
13885 | 494 |
lemma commutativity1: |
495 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
496 |
and lattice: "lattice L" |
|
497 |
and BL: "B \<in> L" |
|
498 |
and TL: "T \<in> L" |
|
499 |
and Fstable: "F \<in> stable T" |
|
500 |
and Gco: "!!X. X\<in>L ==> G \<in> X-B co X" |
|
501 |
and commutes: "commutes F T B L" |
|
502 |
shows "F\<squnion>G \<in> T\<inter>A leadsTo B" |
|
503 |
by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco], |
|
504 |
simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) |
|
505 |
||
506 |
||
507 |
||
13874 | 508 |
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
|
509 |
definition funof :: "[('a*'b)set, 'a] => 'b" where |
13874 | 510 |
"funof r == (\<lambda>x. THE y. (x,y) \<in> r)" |
511 |
||
512 |
lemma funof_eq: "[|single_valued r; (x,y) \<in> r|] ==> funof r x = y" |
|
513 |
by (simp add: funof_def single_valued_def, blast) |
|
514 |
||
515 |
lemma funof_Pair_in: |
|
516 |
"[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r" |
|
517 |
by (force simp add: funof_eq) |
|
518 |
||
519 |
lemma funof_in: |
|
520 |
"[|r``{x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" |
|
521 |
by (force simp add: funof_eq) |
|
522 |
||
523 |
lemma funof_imp_wp: "[|funof act t \<in> A; single_valued act|] ==> t \<in> wp act A" |
|
524 |
by (force simp add: in_wp_iff funof_eq) |
|
525 |
||
526 |
||
527 |
subsubsection{*Commutativity of Functions and Relation*} |
|
528 |
text{*Thesis, page 109*} |
|
529 |
||
32604 | 530 |
(*FIXME: this proof is still an ungodly mess*) |
13888 | 531 |
text{*From Meier's thesis, section 4.5.6*} |
13885 | 532 |
lemma commutativity2_lemma: |
13874 | 533 |
assumes dcommutes: |
534 |
"\<forall>act \<in> Acts F. |
|
535 |
\<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> |
|
536 |
s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" |
|
537 |
and determ: "!!act. act \<in> Acts F ==> single_valued act" |
|
538 |
and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" |
|
539 |
and lattice: "lattice L" |
|
540 |
and BL: "B \<in> L" |
|
541 |
and TL: "T \<in> L" |
|
542 |
and Fstable: "F \<in> stable T" |
|
543 |
shows "commutes F T B L" |
|
32604 | 544 |
apply (simp add: commutes_def del: Int_subset_iff le_inf_iff, clarify) |
545 |
proof - |
|
546 |
fix M and act and t |
|
547 |
assume 1: "B \<subseteq> M" "act \<in> Acts F" "t \<in> cl L (T \<inter> wp act M)" |
|
548 |
then have "\<exists>s. (s,t) \<in> relcl L \<and> s \<in> T \<inter> wp act M" |
|
549 |
by (force simp add: cl_eq_Collect_relcl [OF lattice]) |
|
550 |
then obtain s where 2: "(s, t) \<in> relcl L" "s \<in> T" "s \<in> wp act M" |
|
551 |
by blast |
|
552 |
then have 3: "\<forall>u\<in>L. s \<in> u --> t \<in> u" |
|
553 |
apply (intro ballI impI) |
|
554 |
apply (subst cl_ident [symmetric], assumption) |
|
555 |
apply (simp add: relcl_def) |
|
556 |
apply (blast intro: cl_mono [THEN [2] rev_subsetD]) |
|
557 |
done |
|
558 |
with 1 2 Fstable have 4: "funof act s \<in> T\<inter>M" |
|
559 |
by (force intro!: funof_in |
|
560 |
simp add: wp_def stable_def constrains_def determ total) |
|
561 |
with 1 2 3 have 5: "s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" |
|
562 |
by (intro dcommutes [rule_format]) assumption+ |
|
563 |
with 1 2 3 4 have "t \<in> B | funof act t \<in> cl L (T\<inter>M)" |
|
564 |
by (simp add: relcl_def) (blast intro: BL cl_mono [THEN [2] rev_subsetD]) |
|
565 |
with 1 2 3 4 5 have "t \<in> B | t \<in> wp act (cl L (T\<inter>M))" |
|
566 |
by (blast intro: funof_imp_wp determ) |
|
567 |
with 2 3 have "t \<in> T \<and> (t \<in> B \<or> t \<in> wp act (cl L (T \<inter> M)))" |
|
568 |
by (blast intro: TL cl_mono [THEN [2] rev_subsetD]) |
|
569 |
then show "t \<in> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))" |
|
570 |
by simp |
|
571 |
qed |
|
572 |
||
13888 | 573 |
text{*Version packaged with @{thm progress_set_Union}*} |
13885 | 574 |
lemma commutativity2: |
575 |
assumes leadsTo: "F \<in> A leadsTo B" |
|
576 |
and dcommutes: |
|
577 |
"\<forall>act \<in> Acts F. |
|
578 |
\<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> |
|
579 |
s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L" |
|
580 |
and determ: "!!act. act \<in> Acts F ==> single_valued act" |
|
581 |
and total: "!!act. act \<in> Acts F ==> Domain act = UNIV" |
|
582 |
and lattice: "lattice L" |
|
583 |
and BL: "B \<in> L" |
|
584 |
and TL: "T \<in> L" |
|
585 |
and Fstable: "F \<in> stable T" |
|
586 |
and Gco: "!!X. X\<in>L ==> G \<in> X-B co X" |
|
587 |
shows "F\<squnion>G \<in> T\<inter>A leadsTo B" |
|
588 |
apply (rule commutativity1 [OF leadsTo lattice]) |
|
589 |
apply (simp_all add: Gco commutativity2_lemma dcommutes determ total |
|
590 |
lattice BL TL Fstable) |
|
591 |
done |
|
592 |
||
593 |
||
13888 | 594 |
subsection {*Monotonicity*} |
14150 | 595 |
text{*From Meier's thesis, section 4.5.7, page 110*} |
13888 | 596 |
(*to be continued?*) |
597 |
||
13853 | 598 |
end |