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