author  berghofe 
Fri, 01 Jul 2005 14:16:32 +0200  
changeset 16647  c6d81ddebb0e 
parent 16417  9bc16273c2d4 
child 27682  25aceefd4786 
permissions  rwrr 
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 
ID: $Id$ 
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

4 
Copyright 1999 University of Cambridge 
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

5 

11190  6 
From Chandy and Sanders, "Reasoning About Program Composition", 
7 
Technical Report 2000003, University of Florida, 2000. 

8 

9 
Revised by Sidi Ehmety on January 2001 

10 

11 
Added: Compatibility, weakest guarantees, etc. 

12 

13 
and Weakest existential property, 

14 
from Charpentier and Chandy "Theorems about Composition", 

15 
Fifth International Conference on Mathematics of Program, 2000. 

16 

7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

17 
*) 
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

18 

13798  19 
header{*Guarantees Specifications*} 
20 

16417  21 
theory Guar imports Comp begin 
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

22 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11190
diff
changeset

23 
instance program :: (type) order 
13792  24 
by (intro_classes, 
25 
(assumption  rule component_refl component_trans component_antisym 

26 
program_less_le)+) 

27 

7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

28 

14112  29 
text{*Existential and Universal properties. I formalize the twoprogram 
30 
case, proving equivalence with Chandy and Sanders's nary definitions*} 

7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

31 

14112  32 
constdefs 
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

33 

13792  34 
ex_prop :: "'a program set => bool" 
13819  35 
"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

36 

13792  37 
strict_ex_prop :: "'a program set => bool" 
13819  38 
"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

39 

13792  40 
uv_prop :: "'a program set => bool" 
13819  41 
"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

42 

13792  43 
strict_uv_prop :: "'a program set => bool" 
44 
"strict_uv_prop X == 

13819  45 
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

46 

14112  47 

48 
text{*Guarantees properties*} 

49 

50 
constdefs 

51 

13792  52 
guar :: "['a program set, 'a program set] => 'a program set" 
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset

53 
(infixl "guarantees" 55) (*higher than membership, lower than Co*) 
13819  54 
"X guarantees Y == {F. \<forall>G. F ok G > F\<squnion>G \<in> X > F\<squnion>G \<in> Y}" 
11190  55 

7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

56 

11190  57 
(* Weakest guarantees *) 
13792  58 
wg :: "['a program, 'a program set] => 'a program set" 
13805  59 
"wg F Y == Union({X. F \<in> X guarantees Y})" 
11190  60 

61 
(* Weakest existential property stronger than X *) 

62 
wx :: "('a program) set => ('a program)set" 

13805  63 
"wx X == Union({Y. Y \<subseteq> X & ex_prop Y})" 
11190  64 

65 
(*Illdefined programs can arise through "Join"*) 

13792  66 
welldef :: "'a program set" 
13805  67 
"welldef == {F. Init F \<noteq> {}}" 
11190  68 

13792  69 
refines :: "['a program, 'a program, 'a program set] => bool" 
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

70 
("(3_ refines _ wrt _)" [10,10,10] 10) 
11190  71 
"G refines F wrt X == 
14112  72 
\<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) > 
13819  73 
(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

74 

13792  75 
iso_refines :: "['a program, 'a program, 'a program set] => bool" 
11190  76 
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) 
77 
"G iso_refines F wrt X == 

13805  78 
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

79 

13792  80 

81 
lemma OK_insert_iff: 

82 
"(OK (insert i I) F) = 

13805  83 
(if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))" 
13792  84 
by (auto intro: ok_sym simp add: OK_iff_ok) 
85 

86 

14112  87 
subsection{*Existential Properties*} 
88 

13798  89 
lemma ex1 [rule_format]: 
13792  90 
"[ ex_prop X; finite GG ] ==> 
13805  91 
GG \<inter> X \<noteq> {}> OK GG (%G. G) > (\<Squnion>G \<in> GG. G) \<in> X" 
13792  92 
apply (unfold ex_prop_def) 
93 
apply (erule finite_induct) 

94 
apply (auto simp add: OK_insert_iff Int_insert_left) 

95 
done 

96 

97 

98 
lemma ex2: 

13805  99 
"\<forall>GG. finite GG & GG \<inter> X \<noteq> {} > OK GG (%G. G) >(\<Squnion>G \<in> GG. G):X 
13792  100 
==> ex_prop X" 
101 
apply (unfold ex_prop_def, clarify) 

102 
apply (drule_tac x = "{F,G}" in spec) 

103 
apply (auto dest: ok_sym simp add: OK_iff_ok) 

104 
done 

105 

106 

107 
(*Chandy & Sanders take this as a definition*) 

108 
lemma ex_prop_finite: 

109 
"ex_prop X = 

13805  110 
(\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)> (\<Squnion>G \<in> GG. G) \<in> X)" 
13792  111 
by (blast intro: ex1 ex2) 
112 

113 

114 
(*Their "equivalent definition" given at the end of section 3*) 

115 
lemma ex_prop_equiv: 

13805  116 
"ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) > H \<in> X))" 
13792  117 
apply auto 
14112  118 
apply (unfold ex_prop_def component_of_def, safe, blast, blast) 
13792  119 
apply (subst Join_commute) 
120 
apply (drule ok_sym, blast) 

121 
done 

122 

123 

14112  124 
subsection{*Universal Properties*} 
125 

13792  126 
lemma uv1 [rule_format]: 
127 
"[ uv_prop X; finite GG ] 

13805  128 
==> GG \<subseteq> X & OK GG (%G. G) > (\<Squnion>G \<in> GG. G) \<in> X" 
13792  129 
apply (unfold uv_prop_def) 
130 
apply (erule finite_induct) 

131 
apply (auto simp add: Int_insert_left OK_insert_iff) 

132 
done 

133 

134 
lemma uv2: 

13805  135 
"\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) > (\<Squnion>G \<in> GG. G) \<in> X 
13792  136 
==> uv_prop X" 
137 
apply (unfold uv_prop_def) 

138 
apply (rule conjI) 

139 
apply (drule_tac x = "{}" in spec) 

140 
prefer 2 

141 
apply clarify 

142 
apply (drule_tac x = "{F,G}" in spec) 

143 
apply (auto dest: ok_sym simp add: OK_iff_ok) 

144 
done 

145 

146 
(*Chandy & Sanders take this as a definition*) 

147 
lemma uv_prop_finite: 

148 
"uv_prop X = 

13805  149 
(\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) > (\<Squnion>G \<in> GG. G): X)" 
13792  150 
by (blast intro: uv1 uv2) 
151 

14112  152 
subsection{*Guarantees*} 
13792  153 

154 
lemma guaranteesI: 

14112  155 
"(!!G. [ F ok G; F\<squnion>G \<in> X ] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y" 
13792  156 
by (simp add: guar_def component_def) 
157 

158 
lemma guaranteesD: 

14112  159 
"[ F \<in> X guarantees Y; F ok G; F\<squnion>G \<in> X ] ==> F\<squnion>G \<in> Y" 
13792  160 
by (unfold guar_def component_def, blast) 
161 

162 
(*This version of guaranteesD matches more easily in the conclusion 

13805  163 
The major premise can no longer be F \<subseteq> H since we need to reason about G*) 
13792  164 
lemma component_guaranteesD: 
14112  165 
"[ F \<in> X guarantees Y; F\<squnion>G = H; H \<in> X; F ok G ] ==> H \<in> Y" 
13792  166 
by (unfold guar_def, blast) 
167 

168 
lemma guarantees_weaken: 

13805  169 
"[ F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' ] ==> F \<in> Y guarantees Y'" 
13792  170 
by (unfold guar_def, blast) 
171 

13805  172 
lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV" 
13792  173 
by (unfold guar_def, blast) 
174 

175 
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) 

13805  176 
lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y" 
13792  177 
by (unfold guar_def, blast) 
178 

179 
(*Remark at end of section 4.1 *) 

180 

181 
lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" 

182 
apply (simp (no_asm_use) add: guar_def ex_prop_equiv) 

183 
apply safe 

184 
apply (drule_tac x = x in spec) 

185 
apply (drule_tac [2] x = x in spec) 

186 
apply (drule_tac [2] sym) 

187 
apply (auto simp add: component_of_def) 

188 
done 

189 

190 
lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" 

14112  191 
by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym) 
13792  192 

193 
lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" 

194 
apply (rule iffI) 

195 
apply (rule ex_prop_imp) 

196 
apply (auto simp add: guarantees_imp) 

197 
done 

198 

199 

14112  200 
subsection{*Distributive Laws. ReOrient to Perform Miniscoping*} 
13792  201 

202 
lemma guarantees_UN_left: 

13805  203 
"(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)" 
13792  204 
by (unfold guar_def, blast) 
205 

206 
lemma guarantees_Un_left: 

13805  207 
"(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)" 
13792  208 
by (unfold guar_def, blast) 
209 

210 
lemma guarantees_INT_right: 

13805  211 
"X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)" 
13792  212 
by (unfold guar_def, blast) 
213 

214 
lemma guarantees_Int_right: 

13805  215 
"Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)" 
13792  216 
by (unfold guar_def, blast) 
217 

218 
lemma guarantees_Int_right_I: 

13805  219 
"[ F \<in> Z guarantees X; F \<in> Z guarantees Y ] 
220 
==> F \<in> Z guarantees (X \<inter> Y)" 

13792  221 
by (simp add: guarantees_Int_right) 
222 

223 
lemma guarantees_INT_right_iff: 

13805  224 
"(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))" 
13792  225 
by (simp add: guarantees_INT_right) 
226 

13805  227 
lemma shunting: "(X guarantees Y) = (UNIV guarantees (X \<union> Y))" 
13792  228 
by (unfold guar_def, blast) 
229 

230 
lemma contrapositive: "(X guarantees Y) = Y guarantees X" 

231 
by (unfold guar_def, blast) 

232 

233 
(** The following two can be expressed using intersection and subset, which 

234 
is more faithful to the text but looks cryptic. 

235 
**) 

236 

237 
lemma combining1: 

13805  238 
"[ F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z ] 
239 
==> F \<in> (V \<inter> Y) guarantees Z" 

13792  240 
by (unfold guar_def, blast) 
241 

242 
lemma combining2: 

13805  243 
"[ F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z ] 
244 
==> F \<in> V guarantees (X \<union> Z)" 

13792  245 
by (unfold guar_def, blast) 
246 

247 
(** The following two follow ChandySanders, but the use of objectquantifiers 

248 
does not suit Isabelle... **) 

249 

13805  250 
(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *) 
13792  251 
lemma all_guarantees: 
13805  252 
"\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)" 
13792  253 
by (unfold guar_def, blast) 
254 

13805  255 
(*Premises should be [ F \<in> X guarantees Y i; i \<in> I ] *) 
13792  256 
lemma ex_guarantees: 
13805  257 
"\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)" 
13792  258 
by (unfold guar_def, blast) 
259 

260 

14112  261 
subsection{*Guarantees: Additional Laws (by lcp)*} 
13792  262 

263 
lemma guarantees_Join_Int: 

13805  264 
"[ F \<in> U guarantees V; G \<in> X guarantees Y; F ok G ] 
13819  265 
==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)" 
14112  266 
apply (simp add: guar_def, safe) 
267 
apply (simp add: Join_assoc) 

13819  268 
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") 
14112  269 
apply (simp add: ok_commute) 
270 
apply (simp add: Join_ac) 

13792  271 
done 
272 

273 
lemma guarantees_Join_Un: 

13805  274 
"[ F \<in> U guarantees V; G \<in> X guarantees Y; F ok G ] 
13819  275 
==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)" 
14112  276 
apply (simp add: guar_def, safe) 
277 
apply (simp add: Join_assoc) 

13819  278 
apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ") 
14112  279 
apply (simp add: ok_commute) 
280 
apply (simp add: Join_ac) 

13792  281 
done 
282 

283 
lemma guarantees_JN_INT: 

13805  284 
"[ \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F ] 
285 
==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)" 

13792  286 
apply (unfold guar_def, auto) 
287 
apply (drule bspec, assumption) 

288 
apply (rename_tac "i") 

13819  289 
apply (drule_tac x = "JOIN (I{i}) F\<squnion>G" in spec) 
13792  290 
apply (auto intro: OK_imp_ok 
291 
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 

292 
done 

293 

294 
lemma guarantees_JN_UN: 

13805  295 
"[ \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F ] 
296 
==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)" 

13792  297 
apply (unfold guar_def, auto) 
298 
apply (drule bspec, assumption) 

299 
apply (rename_tac "i") 

13819  300 
apply (drule_tac x = "JOIN (I{i}) F\<squnion>G" in spec) 
13792  301 
apply (auto intro: OK_imp_ok 
302 
simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) 

303 
done 

304 

305 

14112  306 
subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*} 
13792  307 

308 
lemma guarantees_Join_I1: 

13819  309 
"[ F \<in> X guarantees Y; F ok G ] ==> F\<squnion>G \<in> X guarantees Y" 
14112  310 
by (simp add: guar_def Join_assoc) 
13792  311 

14112  312 
lemma guarantees_Join_I2: 
13819  313 
"[ G \<in> X guarantees Y; F ok G ] ==> F\<squnion>G \<in> X guarantees Y" 
13792  314 
apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) 
315 
apply (blast intro: guarantees_Join_I1) 

316 
done 

317 

318 
lemma guarantees_JN_I: 

13805  319 
"[ i \<in> I; F i \<in> X guarantees Y; OK I F ] 
320 
==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y" 

13792  321 
apply (unfold guar_def, clarify) 
13819  322 
apply (drule_tac x = "JOIN (I{i}) F\<squnion>G" in spec) 
14112  323 
apply (auto intro: OK_imp_ok 
324 
simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) 

13792  325 
done 
326 

327 

328 
(*** welldefinedness ***) 

329 

13819  330 
lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef" 
13792  331 
by (unfold welldef_def, auto) 
332 

13819  333 
lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef" 
13792  334 
by (unfold welldef_def, auto) 
335 

336 
(*** refinement ***) 

337 

338 
lemma refines_refl: "F refines F wrt X" 

339 
by (unfold refines_def, blast) 

340 

14112  341 
(*We'd like transitivity, but how do we get it?*) 
342 
lemma refines_trans: 

13792  343 
"[ H refines G wrt X; G refines F wrt X ] ==> H refines F wrt X" 
14112  344 
apply (simp add: refines_def) 
345 
oops 

13792  346 

347 

348 
lemma strict_ex_refine_lemma: 

349 
"strict_ex_prop X 

13819  350 
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X > G\<squnion>H \<in> X) 
13805  351 
= (F \<in> X > G \<in> X)" 
13792  352 
by (unfold strict_ex_prop_def, auto) 
353 

354 
lemma strict_ex_refine_lemma_v: 

355 
"strict_ex_prop X 

13819  356 
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X > G\<squnion>H \<in> X) = 
13805  357 
(F \<in> welldef \<inter> X > G \<in> X)" 
13792  358 
apply (unfold strict_ex_prop_def, safe) 
359 
apply (erule_tac x = SKIP and P = "%H. ?PP H > ?RR H" in allE) 

360 
apply (auto dest: Join_welldef_D1 Join_welldef_D2) 

361 
done 

362 

363 
lemma ex_refinement_thm: 

364 
"[ strict_ex_prop X; 

13819  365 
\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X > G\<squnion>H \<in> welldef ] 
13792  366 
==> (G refines F wrt X) = (G iso_refines F wrt X)" 
367 
apply (rule_tac x = SKIP in allE, assumption) 

368 
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) 

369 
done 

370 

371 

372 
lemma strict_uv_refine_lemma: 

373 
"strict_uv_prop X ==> 

13819  374 
(\<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  375 
by (unfold strict_uv_prop_def, blast) 
376 

377 
lemma strict_uv_refine_lemma_v: 

378 
"strict_uv_prop X 

13819  379 
==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X > G\<squnion>H \<in> X) = 
13805  380 
(F \<in> welldef \<inter> X > G \<in> X)" 
13792  381 
apply (unfold strict_uv_prop_def, safe) 
382 
apply (erule_tac x = SKIP and P = "%H. ?PP H > ?RR H" in allE) 

383 
apply (auto dest: Join_welldef_D1 Join_welldef_D2) 

384 
done 

385 

386 
lemma uv_refinement_thm: 

387 
"[ strict_uv_prop X; 

13819  388 
\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X > 
389 
G\<squnion>H \<in> welldef ] 

13792  390 
==> (G refines F wrt X) = (G iso_refines F wrt X)" 
391 
apply (rule_tac x = SKIP in allE, assumption) 

392 
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) 

393 
done 

394 

395 
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) 

396 
lemma guarantees_equiv: 

13805  397 
"(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))" 
13792  398 
by (unfold guar_def component_of_def, auto) 
399 

14112  400 
lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)" 
13792  401 
by (unfold wg_def, auto) 
402 

14112  403 
lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)" 
13792  404 
by (unfold wg_def guar_def, blast) 
405 

14112  406 
lemma wg_equiv: "(H \<in> wg F X) = (F component_of H > H \<in> X)" 
407 
by (simp add: guarantees_equiv wg_def, blast) 

13792  408 

13805  409 
lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)" 
13792  410 
by (simp add: wg_equiv) 
411 

412 
lemma wg_finite: 

13805  413 
"\<forall>FF. finite FF & FF \<inter> X \<noteq> {} > OK FF (%F. F) 
414 
> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))" 

13792  415 
apply clarify 
13805  416 
apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ") 
13792  417 
apply (drule_tac X = X in component_of_wg, simp) 
418 
apply (simp add: component_of_def) 

13805  419 
apply (rule_tac x = "\<Squnion>F \<in> (FF{F}) . F" in exI) 
13792  420 
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) 
421 
done 

422 

13805  423 
lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)" 
13792  424 
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) 
425 
apply blast 

426 
done 

427 

428 
(** From Charpentier and Chandy "Theorems About Composition" **) 

429 
(* Proposition 2 *) 

430 
lemma wx_subset: "(wx X)<=X" 

431 
by (unfold wx_def, auto) 

432 

433 
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

434 
apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast) 
14112  435 
apply force 
13792  436 
done 
437 

13805  438 
lemma wx_weakest: "\<forall>Z. Z<= X > ex_prop Z > Z \<subseteq> wx X" 
14112  439 
by (auto simp add: wx_def) 
13792  440 

441 
(* Proposition 6 *) 

13819  442 
lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G > F\<squnion>G \<in> X})" 
13792  443 
apply (unfold ex_prop_def, safe) 
14112  444 
apply (drule_tac x = "G\<squnion>Ga" in spec) 
445 
apply (force simp add: ok_Join_iff1 Join_assoc) 

13819  446 
apply (drule_tac x = "F\<squnion>Ga" in spec) 
14112  447 
apply (simp add: ok_Join_iff1 ok_commute Join_ac) 
13792  448 
done 
449 

14112  450 
text{* Equivalence with the other definition of wx *} 
13792  451 

14112  452 
lemma wx_equiv: "wx X = {F. \<forall>G. F ok G > (F\<squnion>G) \<in> X}" 
13792  453 
apply (unfold wx_def, safe) 
14112  454 
apply (simp add: ex_prop_def, blast) 
13792  455 
apply (simp (no_asm)) 
13819  456 
apply (rule_tac x = "{F. \<forall>G. F ok G > F\<squnion>G \<in> X}" in exI, safe) 
13792  457 
apply (rule_tac [2] wx'_ex_prop) 
14112  458 
apply (drule_tac x = SKIP in spec)+ 
459 
apply auto 

13792  460 
done 
461 

462 

14112  463 
text{* Propositions 7 to 11 are about this second definition of wx. 
464 
They are the same as the ones proved for the first definition of wx, 

465 
by equivalence *} 

13792  466 

467 
(* Proposition 12 *) 

468 
(* Main result of the paper *) 

14112  469 
lemma guarantees_wx_eq: "(X guarantees Y) = wx(X \<union> Y)" 
470 
by (simp add: guar_def wx_equiv) 

13792  471 

472 

473 
(* Rules given in section 7 of Chandy and Sander's 

474 
Reasoning About Program composition paper *) 

475 
lemma stable_guarantees_Always: 

14112  476 
"Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)" 
13792  477 
apply (rule guaranteesI) 
14112  478 
apply (simp add: Join_commute) 
13792  479 
apply (rule stable_Join_Always1) 
14112  480 
apply (simp_all add: invariant_def Join_stable) 
13792  481 
done 
482 

483 
lemma constrains_guarantees_leadsTo: 

13805  484 
"F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (BA))" 
13792  485 
apply (rule guaranteesI) 
486 
apply (rule leadsTo_Basis') 

14112  487 
apply (drule constrains_weaken_R) 
488 
prefer 2 apply assumption 

489 
apply blast 

13792  490 
apply (blast intro: Join_transient_I1) 
491 
done 

492 

7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset

493 
end 