author | berghofe |
Mon, 26 Oct 2009 14:53:33 +0100 | |
changeset 33189 | 82a40677c1f8 |
parent 32960 | 69916a850301 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.thy |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27682
diff
changeset
|
3 |
Author: Sidi Ehmety |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
|
11190 | 5 |
From Chandy and Sanders, "Reasoning About Program Composition", |
6 |
Technical Report 2000-003, University of Florida, 2000. |
|
7 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27682
diff
changeset
|
8 |
Compatibility, weakest guarantees, etc. and Weakest existential |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27682
diff
changeset
|
9 |
property, from Charpentier and Chandy "Theorems about Composition", |
11190 | 10 |
Fifth International Conference on Mathematics of Program, 2000. |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
11 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
12 |
|
13798 | 13 |
header{*Guarantees Specifications*} |
14 |
||
27682 | 15 |
theory Guar |
16 |
imports Comp |
|
17 |
begin |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
18 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11190
diff
changeset
|
19 |
instance program :: (type) order |
27682 | 20 |
proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans) |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
21 |
|
14112 | 22 |
text{*Existential and Universal properties. I formalize the two-program |
23 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*} |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
24 |
|
14112 | 25 |
constdefs |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
26 |
|
13792 | 27 |
ex_prop :: "'a program set => bool" |
13819 | 28 |
"ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
29 |
|
13792 | 30 |
strict_ex_prop :: "'a program set => bool" |
13819 | 31 |
"strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
32 |
|
13792 | 33 |
uv_prop :: "'a program set => bool" |
13819 | 34 |
"uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
35 |
|
13792 | 36 |
strict_uv_prop :: "'a program set => bool" |
37 |
"strict_uv_prop X == |
|
13819 | 38 |
SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
39 |
|
14112 | 40 |
|
41 |
text{*Guarantees properties*} |
|
42 |
||
43 |
constdefs |
|
44 |
||
13792 | 45 |
guar :: "['a program set, 'a program set] => 'a program set" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
46 |
(infixl "guarantees" 55) (*higher than membership, lower than Co*) |
13819 | 47 |
"X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}" |
11190 | 48 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
49 |
|
11190 | 50 |
(* Weakest guarantees *) |
13792 | 51 |
wg :: "['a program, 'a program set] => 'a program set" |
13805 | 52 |
"wg F Y == Union({X. F \<in> X guarantees Y})" |
11190 | 53 |
|
54 |
(* Weakest existential property stronger than X *) |
|
55 |
wx :: "('a program) set => ('a program)set" |
|
13805 | 56 |
"wx X == Union({Y. Y \<subseteq> X & ex_prop Y})" |
11190 | 57 |
|
58 |
(*Ill-defined programs can arise through "Join"*) |
|
13792 | 59 |
welldef :: "'a program set" |
13805 | 60 |
"welldef == {F. Init F \<noteq> {}}" |
11190 | 61 |
|
13792 | 62 |
refines :: "['a program, 'a program, 'a program set] => bool" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
27682
diff
changeset
|
63 |
("(3_ refines _ wrt _)" [10,10,10] 10) |
11190 | 64 |
"G refines F wrt X == |
14112 | 65 |
\<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> |
13819 | 66 |
(G\<squnion>H \<in> welldef \<inter> X)" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
67 |
|
13792 | 68 |
iso_refines :: "['a program, 'a program, 'a program set] => bool" |
11190 | 69 |
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) |
70 |
"G iso_refines F wrt X == |
|
13805 | 71 |
F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
72 |
|
13792 | 73 |
|
74 |
lemma OK_insert_iff: |
|
75 |
"(OK (insert i I) F) = |
|
13805 | 76 |
(if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))" |
13792 | 77 |
by (auto intro: ok_sym simp add: OK_iff_ok) |
78 |
||
79 |
||
14112 | 80 |
subsection{*Existential Properties*} |
81 |
||
13798 | 82 |
lemma ex1 [rule_format]: |
13792 | 83 |
"[| ex_prop X; finite GG |] ==> |
13805 | 84 |
GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X" |
13792 | 85 |
apply (unfold ex_prop_def) |
86 |
apply (erule finite_induct) |
|
87 |
apply (auto simp add: OK_insert_iff Int_insert_left) |
|
88 |
done |
|
89 |
||
90 |
||
91 |
lemma ex2: |
|
13805 | 92 |
"\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X |
13792 | 93 |
==> ex_prop X" |
94 |
apply (unfold ex_prop_def, clarify) |
|
95 |
apply (drule_tac x = "{F,G}" in spec) |
|
96 |
apply (auto dest: ok_sym simp add: OK_iff_ok) |
|
97 |
done |
|
98 |
||
99 |
||
100 |
(*Chandy & Sanders take this as a definition*) |
|
101 |
lemma ex_prop_finite: |
|
102 |
"ex_prop X = |
|
13805 | 103 |
(\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)" |
13792 | 104 |
by (blast intro: ex1 ex2) |
105 |
||
106 |
||
107 |
(*Their "equivalent definition" given at the end of section 3*) |
|
108 |
lemma ex_prop_equiv: |
|
13805 | 109 |
"ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))" |
13792 | 110 |
apply auto |
14112 | 111 |
apply (unfold ex_prop_def component_of_def, safe, blast, blast) |
13792 | 112 |
apply (subst Join_commute) |
113 |
apply (drule ok_sym, blast) |
|
114 |
done |
|
115 |
||
116 |
||
14112 | 117 |
subsection{*Universal Properties*} |
118 |
||
13792 | 119 |
lemma uv1 [rule_format]: |
120 |
"[| uv_prop X; finite GG |] |
|
13805 | 121 |
==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X" |
13792 | 122 |
apply (unfold uv_prop_def) |
123 |
apply (erule finite_induct) |
|
124 |
apply (auto simp add: Int_insert_left OK_insert_iff) |
|
125 |
done |
|
126 |
||
127 |
lemma uv2: |
|
13805 | 128 |
"\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X |
13792 | 129 |
==> uv_prop X" |
130 |
apply (unfold uv_prop_def) |
|
131 |
apply (rule conjI) |
|
132 |
apply (drule_tac x = "{}" in spec) |
|
133 |
prefer 2 |
|
134 |
apply clarify |
|
135 |
apply (drule_tac x = "{F,G}" in spec) |
|
136 |
apply (auto dest: ok_sym simp add: OK_iff_ok) |
|
137 |
done |
|
138 |
||
139 |
(*Chandy & Sanders take this as a definition*) |
|
140 |
lemma uv_prop_finite: |
|
141 |
"uv_prop X = |
|
13805 | 142 |
(\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)" |
13792 | 143 |
by (blast intro: uv1 uv2) |
144 |
||
14112 | 145 |
subsection{*Guarantees*} |
13792 | 146 |
|
147 |
lemma guaranteesI: |
|
14112 | 148 |
"(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y" |
13792 | 149 |
by (simp add: guar_def component_def) |
150 |
||
151 |
lemma guaranteesD: |
|
14112 | 152 |
"[| F \<in> X guarantees Y; F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y" |
13792 | 153 |
by (unfold guar_def component_def, blast) |
154 |
||
155 |
(*This version of guaranteesD matches more easily in the conclusion |
|
13805 | 156 |
The major premise can no longer be F \<subseteq> H since we need to reason about G*) |
13792 | 157 |
lemma component_guaranteesD: |
14112 | 158 |
"[| F \<in> X guarantees Y; F\<squnion>G = H; H \<in> X; F ok G |] ==> H \<in> Y" |
13792 | 159 |
by (unfold guar_def, blast) |
160 |
||
161 |
lemma guarantees_weaken: |
|
13805 | 162 |
"[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'" |
13792 | 163 |
by (unfold guar_def, blast) |
164 |
||
13805 | 165 |
lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV" |
13792 | 166 |
by (unfold guar_def, blast) |
167 |
||
168 |
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
|
13805 | 169 |
lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y" |
13792 | 170 |
by (unfold guar_def, blast) |
171 |
||
172 |
(*Remark at end of section 4.1 *) |
|
173 |
||
174 |
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" |
|
175 |
apply (simp (no_asm_use) add: guar_def ex_prop_equiv) |
|
176 |
apply safe |
|
177 |
apply (drule_tac x = x in spec) |
|
178 |
apply (drule_tac [2] x = x in spec) |
|
179 |
apply (drule_tac [2] sym) |
|
180 |
apply (auto simp add: component_of_def) |
|
181 |
done |
|
182 |
||
183 |
lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" |
|
14112 | 184 |
by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym) |
13792 | 185 |
|
186 |
lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" |
|
187 |
apply (rule iffI) |
|
188 |
apply (rule ex_prop_imp) |
|
189 |
apply (auto simp add: guarantees_imp) |
|
190 |
done |
|
191 |
||
192 |
||
14112 | 193 |
subsection{*Distributive Laws. Re-Orient to Perform Miniscoping*} |
13792 | 194 |
|
195 |
lemma guarantees_UN_left: |
|
13805 | 196 |
"(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)" |
13792 | 197 |
by (unfold guar_def, blast) |
198 |
||
199 |
lemma guarantees_Un_left: |
|
13805 | 200 |
"(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)" |
13792 | 201 |
by (unfold guar_def, blast) |
202 |
||
203 |
lemma guarantees_INT_right: |
|
13805 | 204 |
"X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)" |
13792 | 205 |
by (unfold guar_def, blast) |
206 |
||
207 |
lemma guarantees_Int_right: |
|
13805 | 208 |
"Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)" |
13792 | 209 |
by (unfold guar_def, blast) |
210 |
||
211 |
lemma guarantees_Int_right_I: |
|
13805 | 212 |
"[| F \<in> Z guarantees X; F \<in> Z guarantees Y |] |
213 |
==> F \<in> Z guarantees (X \<inter> Y)" |
|
13792 | 214 |
by (simp add: guarantees_Int_right) |
215 |
||
216 |
lemma guarantees_INT_right_iff: |
|
13805 | 217 |
"(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))" |
13792 | 218 |
by (simp add: guarantees_INT_right) |
219 |
||
13805 | 220 |
lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))" |
13792 | 221 |
by (unfold guar_def, blast) |
222 |
||
223 |
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X" |
|
224 |
by (unfold guar_def, blast) |
|
225 |
||
226 |
(** The following two can be expressed using intersection and subset, which |
|
227 |
is more faithful to the text but looks cryptic. |
|
228 |
**) |
|
229 |
||
230 |
lemma combining1: |
|
13805 | 231 |
"[| F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z |] |
232 |
==> F \<in> (V \<inter> Y) guarantees Z" |
|
13792 | 233 |
by (unfold guar_def, blast) |
234 |
||
235 |
lemma combining2: |
|
13805 | 236 |
"[| F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z |] |
237 |
==> F \<in> V guarantees (X \<union> Z)" |
|
13792 | 238 |
by (unfold guar_def, blast) |
239 |
||
240 |
(** The following two follow Chandy-Sanders, but the use of object-quantifiers |
|
241 |
does not suit Isabelle... **) |
|
242 |
||
13805 | 243 |
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *) |
13792 | 244 |
lemma all_guarantees: |
13805 | 245 |
"\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)" |
13792 | 246 |
by (unfold guar_def, blast) |
247 |
||
13805 | 248 |
(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *) |
13792 | 249 |
lemma ex_guarantees: |
13805 | 250 |
"\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)" |
13792 | 251 |
by (unfold guar_def, blast) |
252 |
||
253 |
||
14112 | 254 |
subsection{*Guarantees: Additional Laws (by lcp)*} |
13792 | 255 |
|
256 |
lemma guarantees_Join_Int: |
|
13805 | 257 |
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] |
13819 | 258 |
==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)" |
14112 | 259 |
apply (simp add: guar_def, safe) |
260 |
apply (simp add: Join_assoc) |
|
13819 | 261 |
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") |
14112 | 262 |
apply (simp add: ok_commute) |
263 |
apply (simp add: Join_ac) |
|
13792 | 264 |
done |
265 |
||
266 |
lemma guarantees_Join_Un: |
|
13805 | 267 |
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] |
13819 | 268 |
==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)" |
14112 | 269 |
apply (simp add: guar_def, safe) |
270 |
apply (simp add: Join_assoc) |
|
13819 | 271 |
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") |
14112 | 272 |
apply (simp add: ok_commute) |
273 |
apply (simp add: Join_ac) |
|
13792 | 274 |
done |
275 |
||
276 |
lemma guarantees_JN_INT: |
|
13805 | 277 |
"[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |] |
278 |
==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)" |
|
13792 | 279 |
apply (unfold guar_def, auto) |
280 |
apply (drule bspec, assumption) |
|
281 |
apply (rename_tac "i") |
|
13819 | 282 |
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) |
13792 | 283 |
apply (auto intro: OK_imp_ok |
284 |
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) |
|
285 |
done |
|
286 |
||
287 |
lemma guarantees_JN_UN: |
|
13805 | 288 |
"[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |] |
289 |
==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)" |
|
13792 | 290 |
apply (unfold guar_def, auto) |
291 |
apply (drule bspec, assumption) |
|
292 |
apply (rename_tac "i") |
|
13819 | 293 |
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) |
13792 | 294 |
apply (auto intro: OK_imp_ok |
295 |
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) |
|
296 |
done |
|
297 |
||
298 |
||
14112 | 299 |
subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*} |
13792 | 300 |
|
301 |
lemma guarantees_Join_I1: |
|
13819 | 302 |
"[| F \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y" |
14112 | 303 |
by (simp add: guar_def Join_assoc) |
13792 | 304 |
|
14112 | 305 |
lemma guarantees_Join_I2: |
13819 | 306 |
"[| G \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y" |
13792 | 307 |
apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) |
308 |
apply (blast intro: guarantees_Join_I1) |
|
309 |
done |
|
310 |
||
311 |
lemma guarantees_JN_I: |
|
13805 | 312 |
"[| i \<in> I; F i \<in> X guarantees Y; OK I F |] |
313 |
==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y" |
|
13792 | 314 |
apply (unfold guar_def, clarify) |
13819 | 315 |
apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec) |
14112 | 316 |
apply (auto intro: OK_imp_ok |
317 |
simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) |
|
13792 | 318 |
done |
319 |
||
320 |
||
321 |
(*** well-definedness ***) |
|
322 |
||
13819 | 323 |
lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef" |
13792 | 324 |
by (unfold welldef_def, auto) |
325 |
||
13819 | 326 |
lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef" |
13792 | 327 |
by (unfold welldef_def, auto) |
328 |
||
329 |
(*** refinement ***) |
|
330 |
||
331 |
lemma refines_refl: "F refines F wrt X" |
|
332 |
by (unfold refines_def, blast) |
|
333 |
||
14112 | 334 |
(*We'd like transitivity, but how do we get it?*) |
335 |
lemma refines_trans: |
|
13792 | 336 |
"[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" |
14112 | 337 |
apply (simp add: refines_def) |
338 |
oops |
|
13792 | 339 |
|
340 |
||
341 |
lemma strict_ex_refine_lemma: |
|
342 |
"strict_ex_prop X |
|
13819 | 343 |
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) |
13805 | 344 |
= (F \<in> X --> G \<in> X)" |
13792 | 345 |
by (unfold strict_ex_prop_def, auto) |
346 |
||
347 |
lemma strict_ex_refine_lemma_v: |
|
348 |
"strict_ex_prop X |
|
13819 | 349 |
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = |
13805 | 350 |
(F \<in> welldef \<inter> X --> G \<in> X)" |
13792 | 351 |
apply (unfold strict_ex_prop_def, safe) |
352 |
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) |
|
353 |
apply (auto dest: Join_welldef_D1 Join_welldef_D2) |
|
354 |
done |
|
355 |
||
356 |
lemma ex_refinement_thm: |
|
357 |
"[| strict_ex_prop X; |
|
13819 | 358 |
\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |] |
13792 | 359 |
==> (G refines F wrt X) = (G iso_refines F wrt X)" |
360 |
apply (rule_tac x = SKIP in allE, assumption) |
|
361 |
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) |
|
362 |
done |
|
363 |
||
364 |
||
365 |
lemma strict_uv_refine_lemma: |
|
366 |
"strict_uv_prop X ==> |
|
13819 | 367 |
(\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)" |
13792 | 368 |
by (unfold strict_uv_prop_def, blast) |
369 |
||
370 |
lemma strict_uv_refine_lemma_v: |
|
371 |
"strict_uv_prop X |
|
13819 | 372 |
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = |
13805 | 373 |
(F \<in> welldef \<inter> X --> G \<in> X)" |
13792 | 374 |
apply (unfold strict_uv_prop_def, safe) |
375 |
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) |
|
376 |
apply (auto dest: Join_welldef_D1 Join_welldef_D2) |
|
377 |
done |
|
378 |
||
379 |
lemma uv_refinement_thm: |
|
380 |
"[| strict_uv_prop X; |
|
13819 | 381 |
\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> |
382 |
G\<squnion>H \<in> welldef |] |
|
13792 | 383 |
==> (G refines F wrt X) = (G iso_refines F wrt X)" |
384 |
apply (rule_tac x = SKIP in allE, assumption) |
|
385 |
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) |
|
386 |
done |
|
387 |
||
388 |
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) |
|
389 |
lemma guarantees_equiv: |
|
13805 | 390 |
"(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))" |
13792 | 391 |
by (unfold guar_def component_of_def, auto) |
392 |
||
14112 | 393 |
lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)" |
13792 | 394 |
by (unfold wg_def, auto) |
395 |
||
14112 | 396 |
lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)" |
13792 | 397 |
by (unfold wg_def guar_def, blast) |
398 |
||
14112 | 399 |
lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)" |
400 |
by (simp add: guarantees_equiv wg_def, blast) |
|
13792 | 401 |
|
13805 | 402 |
lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)" |
13792 | 403 |
by (simp add: wg_equiv) |
404 |
||
405 |
lemma wg_finite: |
|
13805 | 406 |
"\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F) |
407 |
--> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))" |
|
13792 | 408 |
apply clarify |
13805 | 409 |
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ") |
13792 | 410 |
apply (drule_tac X = X in component_of_wg, simp) |
411 |
apply (simp add: component_of_def) |
|
13805 | 412 |
apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI) |
13792 | 413 |
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) |
414 |
done |
|
415 |
||
13805 | 416 |
lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)" |
13792 | 417 |
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) |
418 |
apply blast |
|
419 |
done |
|
420 |
||
421 |
(** From Charpentier and Chandy "Theorems About Composition" **) |
|
422 |
(* Proposition 2 *) |
|
423 |
lemma wx_subset: "(wx X)<=X" |
|
424 |
by (unfold wx_def, auto) |
|
425 |
||
426 |
lemma wx_ex_prop: "ex_prop (wx X)" |
|
16647
c6d81ddebb0e
Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
berghofe
parents:
16417
diff
changeset
|
427 |
apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast) |
14112 | 428 |
apply force |
13792 | 429 |
done |
430 |
||
13805 | 431 |
lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X" |
14112 | 432 |
by (auto simp add: wx_def) |
13792 | 433 |
|
434 |
(* Proposition 6 *) |
|
13819 | 435 |
lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})" |
13792 | 436 |
apply (unfold ex_prop_def, safe) |
14112 | 437 |
apply (drule_tac x = "G\<squnion>Ga" in spec) |
438 |
apply (force simp add: ok_Join_iff1 Join_assoc) |
|
13819 | 439 |
apply (drule_tac x = "F\<squnion>Ga" in spec) |
14112 | 440 |
apply (simp add: ok_Join_iff1 ok_commute Join_ac) |
13792 | 441 |
done |
442 |
||
14112 | 443 |
text{* Equivalence with the other definition of wx *} |
13792 | 444 |
|
14112 | 445 |
lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}" |
13792 | 446 |
apply (unfold wx_def, safe) |
14112 | 447 |
apply (simp add: ex_prop_def, blast) |
13792 | 448 |
apply (simp (no_asm)) |
13819 | 449 |
apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe) |
13792 | 450 |
apply (rule_tac [2] wx'_ex_prop) |
14112 | 451 |
apply (drule_tac x = SKIP in spec)+ |
452 |
apply auto |
|
13792 | 453 |
done |
454 |
||
455 |
||
14112 | 456 |
text{* Propositions 7 to 11 are about this second definition of wx. |
457 |
They are the same as the ones proved for the first definition of wx, |
|
458 |
by equivalence *} |
|
13792 | 459 |
|
460 |
(* Proposition 12 *) |
|
461 |
(* Main result of the paper *) |
|
14112 | 462 |
lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)" |
463 |
by (simp add: guar_def wx_equiv) |
|
13792 | 464 |
|
465 |
||
466 |
(* Rules given in section 7 of Chandy and Sander's |
|
467 |
Reasoning About Program composition paper *) |
|
468 |
lemma stable_guarantees_Always: |
|
14112 | 469 |
"Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)" |
13792 | 470 |
apply (rule guaranteesI) |
14112 | 471 |
apply (simp add: Join_commute) |
13792 | 472 |
apply (rule stable_Join_Always1) |
14112 | 473 |
apply (simp_all add: invariant_def Join_stable) |
13792 | 474 |
done |
475 |
||
476 |
lemma constrains_guarantees_leadsTo: |
|
13805 | 477 |
"F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))" |
13792 | 478 |
apply (rule guaranteesI) |
479 |
apply (rule leadsTo_Basis') |
|
14112 | 480 |
apply (drule constrains_weaken_R) |
481 |
prefer 2 apply assumption |
|
482 |
apply blast |
|
13792 | 483 |
apply (blast intro: Join_transient_I1) |
484 |
done |
|
485 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
486 |
end |