author | paulson |
Tue, 04 Feb 2003 18:12:40 +0100 | |
changeset 13805 | 3786b2fd6808 |
parent 13798 | 4c1a53627500 |
child 13812 | 91713a1915ee |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/SubstAx |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6536 | 6 |
Weak LeadsTo relation (restricted to the set of reachable states) |
4776 | 7 |
*) |
8 |
||
13798 | 9 |
header{*Weak Progress*} |
10 |
||
13796 | 11 |
theory SubstAx = WFair + Constrains: |
4776 | 12 |
|
8041 | 13 |
constdefs |
13796 | 14 |
Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) |
13805 | 15 |
"A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8041
diff
changeset
|
16 |
|
13796 | 17 |
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) |
13805 | 18 |
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
4776 | 19 |
|
9685 | 20 |
syntax (xsymbols) |
13796 | 21 |
"op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60) |
22 |
||
23 |
||
24 |
(*Resembles the previous definition of LeadsTo*) |
|
25 |
lemma LeadsTo_eq_leadsTo: |
|
13805 | 26 |
"A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |
13796 | 27 |
apply (unfold LeadsTo_def) |
28 |
apply (blast dest: psp_stable2 intro: leadsTo_weaken) |
|
29 |
done |
|
30 |
||
31 |
||
13798 | 32 |
subsection{*Specialized laws for handling invariants*} |
13796 | 33 |
|
34 |
(** Conjoining an Always property **) |
|
35 |
||
36 |
lemma Always_LeadsTo_pre: |
|
13805 | 37 |
"F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')" |
38 |
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 |
|
39 |
Int_assoc [symmetric]) |
|
13796 | 40 |
|
41 |
lemma Always_LeadsTo_post: |
|
13805 | 42 |
"F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')" |
43 |
by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 |
|
44 |
Int_assoc [symmetric]) |
|
13796 | 45 |
|
13805 | 46 |
(* [| F \<in> Always C; F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *) |
13796 | 47 |
lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard] |
48 |
||
13805 | 49 |
(* [| F \<in> Always INV; F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *) |
13796 | 50 |
lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard] |
51 |
||
52 |
||
13798 | 53 |
subsection{*Introduction rules: Basis, Trans, Union*} |
13796 | 54 |
|
13805 | 55 |
lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B" |
13796 | 56 |
apply (simp add: LeadsTo_def) |
57 |
apply (blast intro: leadsTo_weaken_L) |
|
58 |
done |
|
59 |
||
60 |
lemma LeadsTo_Trans: |
|
13805 | 61 |
"[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C" |
13796 | 62 |
apply (simp add: LeadsTo_eq_leadsTo) |
63 |
apply (blast intro: leadsTo_Trans) |
|
64 |
done |
|
65 |
||
66 |
lemma LeadsTo_Union: |
|
13805 | 67 |
"(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B" |
13796 | 68 |
apply (simp add: LeadsTo_def) |
69 |
apply (subst Int_Union) |
|
70 |
apply (blast intro: leadsTo_UN) |
|
71 |
done |
|
72 |
||
73 |
||
13798 | 74 |
subsection{*Derived rules*} |
13796 | 75 |
|
13805 | 76 |
lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV" |
13796 | 77 |
by (simp add: LeadsTo_def) |
78 |
||
79 |
(*Useful with cancellation, disjunction*) |
|
80 |
lemma LeadsTo_Un_duplicate: |
|
13805 | 81 |
"F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'" |
13796 | 82 |
by (simp add: Un_ac) |
83 |
||
84 |
lemma LeadsTo_Un_duplicate2: |
|
13805 | 85 |
"F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)" |
13796 | 86 |
by (simp add: Un_ac) |
87 |
||
88 |
lemma LeadsTo_UN: |
|
13805 | 89 |
"(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B" |
13796 | 90 |
apply (simp only: Union_image_eq [symmetric]) |
91 |
apply (blast intro: LeadsTo_Union) |
|
92 |
done |
|
93 |
||
94 |
(*Binary union introduction rule*) |
|
95 |
lemma LeadsTo_Un: |
|
13805 | 96 |
"[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C" |
13796 | 97 |
apply (subst Un_eq_Union) |
98 |
apply (blast intro: LeadsTo_Union) |
|
99 |
done |
|
100 |
||
101 |
(*Lets us look at the starting state*) |
|
102 |
lemma single_LeadsTo_I: |
|
13805 | 103 |
"(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B" |
13796 | 104 |
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) |
105 |
||
13805 | 106 |
lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B" |
13796 | 107 |
apply (simp add: LeadsTo_def) |
108 |
apply (blast intro: subset_imp_leadsTo) |
|
109 |
done |
|
110 |
||
111 |
lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp] |
|
112 |
||
113 |
lemma LeadsTo_weaken_R [rule_format]: |
|
13805 | 114 |
"[| F \<in> A LeadsTo A'; A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'" |
115 |
apply (simp add: LeadsTo_def) |
|
13796 | 116 |
apply (blast intro: leadsTo_weaken_R) |
117 |
done |
|
118 |
||
119 |
lemma LeadsTo_weaken_L [rule_format]: |
|
13805 | 120 |
"[| F \<in> A LeadsTo A'; B \<subseteq> A |] |
121 |
==> F \<in> B LeadsTo A'" |
|
122 |
apply (simp add: LeadsTo_def) |
|
13796 | 123 |
apply (blast intro: leadsTo_weaken_L) |
124 |
done |
|
125 |
||
126 |
lemma LeadsTo_weaken: |
|
13805 | 127 |
"[| F \<in> A LeadsTo A'; |
128 |
B \<subseteq> A; A' \<subseteq> B' |] |
|
129 |
==> F \<in> B LeadsTo B'" |
|
13796 | 130 |
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans) |
131 |
||
132 |
lemma Always_LeadsTo_weaken: |
|
13805 | 133 |
"[| F \<in> Always C; F \<in> A LeadsTo A'; |
134 |
C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] |
|
135 |
==> F \<in> B LeadsTo B'" |
|
13796 | 136 |
by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD) |
137 |
||
138 |
(** Two theorems for "proof lattices" **) |
|
139 |
||
13805 | 140 |
lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B" |
13796 | 141 |
by (blast intro: LeadsTo_Un subset_imp_LeadsTo) |
142 |
||
143 |
lemma LeadsTo_Trans_Un: |
|
13805 | 144 |
"[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] |
145 |
==> F \<in> (A \<union> B) LeadsTo C" |
|
13796 | 146 |
by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans) |
147 |
||
148 |
||
149 |
(** Distributive laws **) |
|
150 |
||
151 |
lemma LeadsTo_Un_distrib: |
|
13805 | 152 |
"(F \<in> (A \<union> B) LeadsTo C) = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)" |
13796 | 153 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_L) |
154 |
||
155 |
lemma LeadsTo_UN_distrib: |
|
13805 | 156 |
"(F \<in> (\<Union>i \<in> I. A i) LeadsTo B) = (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)" |
13796 | 157 |
by (blast intro: LeadsTo_UN LeadsTo_weaken_L) |
158 |
||
159 |
lemma LeadsTo_Union_distrib: |
|
13805 | 160 |
"(F \<in> (Union S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)" |
13796 | 161 |
by (blast intro: LeadsTo_Union LeadsTo_weaken_L) |
162 |
||
163 |
||
164 |
(** More rules using the premise "Always INV" **) |
|
165 |
||
13805 | 166 |
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B" |
13796 | 167 |
by (simp add: Ensures_def LeadsTo_def leadsTo_Basis) |
168 |
||
169 |
lemma EnsuresI: |
|
13805 | 170 |
"[| F \<in> (A-B) Co (A \<union> B); F \<in> transient (A-B) |] |
171 |
==> F \<in> A Ensures B" |
|
13796 | 172 |
apply (simp add: Ensures_def Constrains_eq_constrains) |
173 |
apply (blast intro: ensuresI constrains_weaken transient_strengthen) |
|
174 |
done |
|
175 |
||
176 |
lemma Always_LeadsTo_Basis: |
|
13805 | 177 |
"[| F \<in> Always INV; |
178 |
F \<in> (INV \<inter> (A-A')) Co (A \<union> A'); |
|
179 |
F \<in> transient (INV \<inter> (A-A')) |] |
|
180 |
==> F \<in> A LeadsTo A'" |
|
13796 | 181 |
apply (rule Always_LeadsToI, assumption) |
182 |
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) |
|
183 |
done |
|
184 |
||
185 |
(*Set difference: maybe combine with leadsTo_weaken_L?? |
|
186 |
This is the most useful form of the "disjunction" rule*) |
|
187 |
lemma LeadsTo_Diff: |
|
13805 | 188 |
"[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] |
189 |
==> F \<in> A LeadsTo C" |
|
13796 | 190 |
by (blast intro: LeadsTo_Un LeadsTo_weaken) |
191 |
||
192 |
||
193 |
lemma LeadsTo_UN_UN: |
|
13805 | 194 |
"(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i)) |
195 |
==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)" |
|
13796 | 196 |
apply (simp only: Union_image_eq [symmetric]) |
197 |
apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) |
|
198 |
done |
|
199 |
||
200 |
||
201 |
(*Version with no index set*) |
|
202 |
lemma LeadsTo_UN_UN_noindex: |
|
13805 | 203 |
"(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
13796 | 204 |
by (blast intro: LeadsTo_UN_UN) |
205 |
||
206 |
(*Version with no index set*) |
|
207 |
lemma all_LeadsTo_UN_UN: |
|
13805 | 208 |
"\<forall>i. F \<in> (A i) LeadsTo (A' i) |
209 |
==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
|
13796 | 210 |
by (blast intro: LeadsTo_UN_UN) |
211 |
||
212 |
(*Binary union version*) |
|
213 |
lemma LeadsTo_Un_Un: |
|
13805 | 214 |
"[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] |
215 |
==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')" |
|
13796 | 216 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_R) |
217 |
||
218 |
||
219 |
(** The cancellation law **) |
|
220 |
||
221 |
lemma LeadsTo_cancel2: |
|
13805 | 222 |
"[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |] |
223 |
==> F \<in> A LeadsTo (A' \<union> B')" |
|
13796 | 224 |
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans) |
225 |
||
226 |
lemma LeadsTo_cancel_Diff2: |
|
13805 | 227 |
"[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |] |
228 |
==> F \<in> A LeadsTo (A' \<union> B')" |
|
13796 | 229 |
apply (rule LeadsTo_cancel2) |
230 |
prefer 2 apply assumption |
|
231 |
apply (simp_all (no_asm_simp)) |
|
232 |
done |
|
233 |
||
234 |
lemma LeadsTo_cancel1: |
|
13805 | 235 |
"[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |] |
236 |
==> F \<in> A LeadsTo (B' \<union> A')" |
|
13796 | 237 |
apply (simp add: Un_commute) |
238 |
apply (blast intro!: LeadsTo_cancel2) |
|
239 |
done |
|
240 |
||
241 |
lemma LeadsTo_cancel_Diff1: |
|
13805 | 242 |
"[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] |
243 |
==> F \<in> A LeadsTo (B' \<union> A')" |
|
13796 | 244 |
apply (rule LeadsTo_cancel1) |
245 |
prefer 2 apply assumption |
|
246 |
apply (simp_all (no_asm_simp)) |
|
247 |
done |
|
248 |
||
249 |
||
250 |
(** The impossibility law **) |
|
251 |
||
252 |
(*The set "A" may be non-empty, but it contains no reachable states*) |
|
13805 | 253 |
lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)" |
254 |
apply (simp add: LeadsTo_def Always_eq_includes_reachable) |
|
13796 | 255 |
apply (drule leadsTo_empty, auto) |
256 |
done |
|
257 |
||
258 |
||
259 |
(** PSP: Progress-Safety-Progress **) |
|
260 |
||
261 |
(*Special case of PSP: Misra's "stable conjunction"*) |
|
262 |
lemma PSP_Stable: |
|
13805 | 263 |
"[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
264 |
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)" |
|
265 |
apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) |
|
13796 | 266 |
apply (drule psp_stable, assumption) |
267 |
apply (simp add: Int_ac) |
|
268 |
done |
|
269 |
||
270 |
lemma PSP_Stable2: |
|
13805 | 271 |
"[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
272 |
==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')" |
|
13796 | 273 |
by (simp add: PSP_Stable Int_ac) |
274 |
||
275 |
lemma PSP: |
|
13805 | 276 |
"[| F \<in> A LeadsTo A'; F \<in> B Co B' |] |
277 |
==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))" |
|
278 |
apply (simp add: LeadsTo_def Constrains_eq_constrains) |
|
13796 | 279 |
apply (blast dest: psp intro: leadsTo_weaken) |
280 |
done |
|
281 |
||
282 |
lemma PSP2: |
|
13805 | 283 |
"[| F \<in> A LeadsTo A'; F \<in> B Co B' |] |
284 |
==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))" |
|
13796 | 285 |
by (simp add: PSP Int_ac) |
286 |
||
287 |
lemma PSP_Unless: |
|
13805 | 288 |
"[| F \<in> A LeadsTo A'; F \<in> B Unless B' |] |
289 |
==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')" |
|
13796 | 290 |
apply (unfold Unless_def) |
291 |
apply (drule PSP, assumption) |
|
292 |
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo) |
|
293 |
done |
|
294 |
||
295 |
||
296 |
lemma Stable_transient_Always_LeadsTo: |
|
13805 | 297 |
"[| F \<in> Stable A; F \<in> transient C; |
298 |
F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B" |
|
13796 | 299 |
apply (erule Always_LeadsTo_weaken) |
300 |
apply (rule LeadsTo_Diff) |
|
301 |
prefer 2 |
|
302 |
apply (erule |
|
303 |
transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2]) |
|
304 |
apply (blast intro: subset_imp_LeadsTo)+ |
|
305 |
done |
|
306 |
||
307 |
||
13798 | 308 |
subsection{*Induction rules*} |
13796 | 309 |
|
310 |
(** Meta or object quantifier ????? **) |
|
311 |
lemma LeadsTo_wf_induct: |
|
312 |
"[| wf r; |
|
13805 | 313 |
\<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo |
314 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
315 |
==> F \<in> A LeadsTo B" |
|
316 |
apply (simp add: LeadsTo_eq_leadsTo) |
|
13796 | 317 |
apply (erule leadsTo_wf_induct) |
318 |
apply (blast intro: leadsTo_weaken) |
|
319 |
done |
|
320 |
||
321 |
||
322 |
lemma Bounded_induct: |
|
323 |
"[| wf r; |
|
13805 | 324 |
\<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo |
325 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
326 |
==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)" |
|
13796 | 327 |
apply (erule LeadsTo_wf_induct, safe) |
13805 | 328 |
apply (case_tac "m \<in> I") |
13796 | 329 |
apply (blast intro: LeadsTo_weaken) |
330 |
apply (blast intro: subset_imp_LeadsTo) |
|
331 |
done |
|
332 |
||
333 |
||
334 |
lemma LessThan_induct: |
|
13805 | 335 |
"(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)) |
336 |
==> F \<in> A LeadsTo B" |
|
337 |
by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) |
|
13796 | 338 |
|
339 |
(*Integer version. Could generalize from 0 to any lower bound*) |
|
340 |
lemma integ_0_le_induct: |
|
13805 | 341 |
"[| F \<in> Always {s. (0::int) \<le> f s}; |
342 |
!! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo |
|
343 |
((A \<inter> {s. f s < z}) \<union> B) |] |
|
344 |
==> F \<in> A LeadsTo B" |
|
13796 | 345 |
apply (rule_tac f = "nat o f" in LessThan_induct) |
346 |
apply (simp add: vimage_def) |
|
347 |
apply (rule Always_LeadsTo_weaken, assumption+) |
|
348 |
apply (auto simp add: nat_eq_iff nat_less_iff) |
|
349 |
done |
|
350 |
||
351 |
lemma LessThan_bounded_induct: |
|
13805 | 352 |
"!!l::nat. \<forall>m \<in> greaterThan l. |
353 |
F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |
|
354 |
==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)" |
|
355 |
apply (simp only: Diff_eq [symmetric] vimage_Compl |
|
356 |
Compl_greaterThan [symmetric]) |
|
357 |
apply (rule wf_less_than [THEN Bounded_induct], simp) |
|
13796 | 358 |
done |
359 |
||
360 |
lemma GreaterThan_bounded_induct: |
|
13805 | 361 |
"!!l::nat. \<forall>m \<in> lessThan l. |
362 |
F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B) |
|
363 |
==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)" |
|
13796 | 364 |
apply (rule_tac f = f and f1 = "%k. l - k" |
365 |
in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct]) |
|
366 |
apply (simp add: inv_image_def Image_singleton, clarify) |
|
367 |
apply (case_tac "m<l") |
|
13805 | 368 |
apply (blast intro: LeadsTo_weaken_R diff_less_mono2) |
369 |
apply (blast intro: not_leE subset_imp_LeadsTo) |
|
13796 | 370 |
done |
371 |
||
372 |
||
13798 | 373 |
subsection{*Completion: Binary and General Finite versions*} |
13796 | 374 |
|
375 |
lemma Completion: |
|
13805 | 376 |
"[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C); |
377 |
F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) |] |
|
378 |
==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)" |
|
379 |
apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib) |
|
13796 | 380 |
apply (blast intro: completion leadsTo_weaken) |
381 |
done |
|
382 |
||
383 |
lemma Finite_completion_lemma: |
|
384 |
"finite I |
|
13805 | 385 |
==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) --> |
386 |
(\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) --> |
|
387 |
F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13796 | 388 |
apply (erule finite_induct, auto) |
389 |
apply (rule Completion) |
|
390 |
prefer 4 |
|
391 |
apply (simp only: INT_simps [symmetric]) |
|
392 |
apply (rule Constrains_INT, auto) |
|
393 |
done |
|
394 |
||
395 |
lemma Finite_completion: |
|
396 |
"[| finite I; |
|
13805 | 397 |
!!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C); |
398 |
!!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |] |
|
399 |
==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13796 | 400 |
by (blast intro: Finite_completion_lemma [THEN mp, THEN mp]) |
401 |
||
402 |
lemma Stable_completion: |
|
13805 | 403 |
"[| F \<in> A LeadsTo A'; F \<in> Stable A'; |
404 |
F \<in> B LeadsTo B'; F \<in> Stable B' |] |
|
405 |
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')" |
|
13796 | 406 |
apply (unfold Stable_def) |
407 |
apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R]) |
|
408 |
apply (force+) |
|
409 |
done |
|
410 |
||
411 |
lemma Finite_stable_completion: |
|
412 |
"[| finite I; |
|
13805 | 413 |
!!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i); |
414 |
!!i. i \<in> I ==> F \<in> Stable (A' i) |] |
|
415 |
==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)" |
|
13796 | 416 |
apply (unfold Stable_def) |
417 |
apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R]) |
|
13805 | 418 |
apply (simp_all, blast+) |
13796 | 419 |
done |
420 |
||
4776 | 421 |
end |