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