author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 45605 | a89b4bc311a5 |
child 60773 | d09c66a0ea10 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/SubstAx.thy |
4776 | 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 |
||
58889 | 8 |
section{*Weak Progress*} |
13798 | 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' *) |
45605 | 45 |
lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1] |
13796 | 46 |
|
13805 | 47 |
(* [| F \<in> Always INV; F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *) |
45605 | 48 |
lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2] |
13796 | 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" |
44106 | 88 |
apply (unfold SUP_def) |
13796 | 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" |
44106 | 95 |
using LeadsTo_UN [of "{A, B}" F id C] by auto |
13796 | 96 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
97 |
text{*Lets us look at the starting state*} |
13796 | 98 |
lemma single_LeadsTo_I: |
13805 | 99 |
"(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B" |
13796 | 100 |
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) |
101 |
||
13805 | 102 |
lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B" |
13796 | 103 |
apply (simp add: LeadsTo_def) |
104 |
apply (blast intro: subset_imp_leadsTo) |
|
105 |
done |
|
106 |
||
45605 | 107 |
lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp] |
13796 | 108 |
|
45477 | 109 |
lemma LeadsTo_weaken_R: |
13805 | 110 |
"[| F \<in> A LeadsTo A'; A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'" |
111 |
apply (simp add: LeadsTo_def) |
|
13796 | 112 |
apply (blast intro: leadsTo_weaken_R) |
113 |
done |
|
114 |
||
45477 | 115 |
lemma LeadsTo_weaken_L: |
13805 | 116 |
"[| F \<in> A LeadsTo A'; B \<subseteq> A |] |
117 |
==> F \<in> B LeadsTo A'" |
|
118 |
apply (simp add: LeadsTo_def) |
|
13796 | 119 |
apply (blast intro: leadsTo_weaken_L) |
120 |
done |
|
121 |
||
122 |
lemma LeadsTo_weaken: |
|
13805 | 123 |
"[| F \<in> A LeadsTo A'; |
124 |
B \<subseteq> A; A' \<subseteq> B' |] |
|
125 |
==> F \<in> B LeadsTo B'" |
|
13796 | 126 |
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans) |
127 |
||
128 |
lemma Always_LeadsTo_weaken: |
|
13805 | 129 |
"[| F \<in> Always C; F \<in> A LeadsTo A'; |
130 |
C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] |
|
131 |
==> F \<in> B LeadsTo B'" |
|
13796 | 132 |
by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD) |
133 |
||
134 |
(** Two theorems for "proof lattices" **) |
|
135 |
||
13805 | 136 |
lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B" |
13796 | 137 |
by (blast intro: LeadsTo_Un subset_imp_LeadsTo) |
138 |
||
139 |
lemma LeadsTo_Trans_Un: |
|
13805 | 140 |
"[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] |
141 |
==> F \<in> (A \<union> B) LeadsTo C" |
|
13796 | 142 |
by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans) |
143 |
||
144 |
||
145 |
(** Distributive laws **) |
|
146 |
||
147 |
lemma LeadsTo_Un_distrib: |
|
13805 | 148 |
"(F \<in> (A \<union> B) LeadsTo C) = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)" |
13796 | 149 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_L) |
150 |
||
151 |
lemma LeadsTo_UN_distrib: |
|
13805 | 152 |
"(F \<in> (\<Union>i \<in> I. A i) LeadsTo B) = (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)" |
13796 | 153 |
by (blast intro: LeadsTo_UN LeadsTo_weaken_L) |
154 |
||
155 |
lemma LeadsTo_Union_distrib: |
|
13805 | 156 |
"(F \<in> (Union S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)" |
13796 | 157 |
by (blast intro: LeadsTo_Union LeadsTo_weaken_L) |
158 |
||
159 |
||
160 |
(** More rules using the premise "Always INV" **) |
|
161 |
||
13805 | 162 |
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B" |
13796 | 163 |
by (simp add: Ensures_def LeadsTo_def leadsTo_Basis) |
164 |
||
165 |
lemma EnsuresI: |
|
13805 | 166 |
"[| F \<in> (A-B) Co (A \<union> B); F \<in> transient (A-B) |] |
167 |
==> F \<in> A Ensures B" |
|
13796 | 168 |
apply (simp add: Ensures_def Constrains_eq_constrains) |
169 |
apply (blast intro: ensuresI constrains_weaken transient_strengthen) |
|
170 |
done |
|
171 |
||
172 |
lemma Always_LeadsTo_Basis: |
|
13805 | 173 |
"[| F \<in> Always INV; |
174 |
F \<in> (INV \<inter> (A-A')) Co (A \<union> A'); |
|
175 |
F \<in> transient (INV \<inter> (A-A')) |] |
|
176 |
==> F \<in> A LeadsTo A'" |
|
13796 | 177 |
apply (rule Always_LeadsToI, assumption) |
178 |
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) |
|
179 |
done |
|
180 |
||
14150 | 181 |
text{*Set difference: maybe combine with @{text leadsTo_weaken_L}?? |
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
182 |
This is the most useful form of the "disjunction" rule*} |
13796 | 183 |
lemma LeadsTo_Diff: |
13805 | 184 |
"[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] |
185 |
==> F \<in> A LeadsTo C" |
|
13796 | 186 |
by (blast intro: LeadsTo_Un LeadsTo_weaken) |
187 |
||
188 |
||
189 |
lemma LeadsTo_UN_UN: |
|
13805 | 190 |
"(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i)) |
191 |
==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)" |
|
13796 | 192 |
apply (simp only: Union_image_eq [symmetric]) |
193 |
apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) |
|
194 |
done |
|
195 |
||
196 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
197 |
text{*Version with no index set*} |
13796 | 198 |
lemma LeadsTo_UN_UN_noindex: |
13805 | 199 |
"(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
13796 | 200 |
by (blast intro: LeadsTo_UN_UN) |
201 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
202 |
text{*Version with no index set*} |
13796 | 203 |
lemma all_LeadsTo_UN_UN: |
13805 | 204 |
"\<forall>i. F \<in> (A i) LeadsTo (A' i) |
205 |
==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
|
13796 | 206 |
by (blast intro: LeadsTo_UN_UN) |
207 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
208 |
text{*Binary union version*} |
13796 | 209 |
lemma LeadsTo_Un_Un: |
13805 | 210 |
"[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] |
211 |
==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')" |
|
13796 | 212 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_R) |
213 |
||
214 |
||
215 |
(** The cancellation law **) |
|
216 |
||
217 |
lemma LeadsTo_cancel2: |
|
13805 | 218 |
"[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |] |
219 |
==> F \<in> A LeadsTo (A' \<union> B')" |
|
13796 | 220 |
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans) |
221 |
||
222 |
lemma LeadsTo_cancel_Diff2: |
|
13805 | 223 |
"[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |] |
224 |
==> F \<in> A LeadsTo (A' \<union> B')" |
|
13796 | 225 |
apply (rule LeadsTo_cancel2) |
226 |
prefer 2 apply assumption |
|
227 |
apply (simp_all (no_asm_simp)) |
|
228 |
done |
|
229 |
||
230 |
lemma LeadsTo_cancel1: |
|
13805 | 231 |
"[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |] |
232 |
==> F \<in> A LeadsTo (B' \<union> A')" |
|
13796 | 233 |
apply (simp add: Un_commute) |
234 |
apply (blast intro!: LeadsTo_cancel2) |
|
235 |
done |
|
236 |
||
237 |
lemma LeadsTo_cancel_Diff1: |
|
13805 | 238 |
"[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] |
239 |
==> F \<in> A LeadsTo (B' \<union> A')" |
|
13796 | 240 |
apply (rule LeadsTo_cancel1) |
241 |
prefer 2 apply assumption |
|
242 |
apply (simp_all (no_asm_simp)) |
|
243 |
done |
|
244 |
||
245 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
246 |
text{*The impossibility law*} |
13796 | 247 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
248 |
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
|
249 |
lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)" |
13805 | 250 |
apply (simp add: LeadsTo_def Always_eq_includes_reachable) |
13796 | 251 |
apply (drule leadsTo_empty, auto) |
252 |
done |
|
253 |
||
254 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
255 |
subsection{*PSP: Progress-Safety-Progress*} |
13796 | 256 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
257 |
text{*Special case of PSP: Misra's "stable conjunction"*} |
13796 | 258 |
lemma PSP_Stable: |
13805 | 259 |
"[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
260 |
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)" |
|
261 |
apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) |
|
13796 | 262 |
apply (drule psp_stable, assumption) |
263 |
apply (simp add: Int_ac) |
|
264 |
done |
|
265 |
||
266 |
lemma PSP_Stable2: |
|
13805 | 267 |
"[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
268 |
==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')" |
|
13796 | 269 |
by (simp add: PSP_Stable Int_ac) |
270 |
||
271 |
lemma PSP: |
|
13805 | 272 |
"[| F \<in> A LeadsTo A'; F \<in> B Co B' |] |
273 |
==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))" |
|
274 |
apply (simp add: LeadsTo_def Constrains_eq_constrains) |
|
13796 | 275 |
apply (blast dest: psp intro: leadsTo_weaken) |
276 |
done |
|
277 |
||
278 |
lemma PSP2: |
|
13805 | 279 |
"[| F \<in> A LeadsTo A'; F \<in> B Co B' |] |
280 |
==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))" |
|
13796 | 281 |
by (simp add: PSP Int_ac) |
282 |
||
283 |
lemma PSP_Unless: |
|
13805 | 284 |
"[| F \<in> A LeadsTo A'; F \<in> B Unless B' |] |
285 |
==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')" |
|
13796 | 286 |
apply (unfold Unless_def) |
287 |
apply (drule PSP, assumption) |
|
288 |
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo) |
|
289 |
done |
|
290 |
||
291 |
||
292 |
lemma Stable_transient_Always_LeadsTo: |
|
13805 | 293 |
"[| F \<in> Stable A; F \<in> transient C; |
294 |
F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B" |
|
13796 | 295 |
apply (erule Always_LeadsTo_weaken) |
296 |
apply (rule LeadsTo_Diff) |
|
297 |
prefer 2 |
|
298 |
apply (erule |
|
299 |
transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2]) |
|
300 |
apply (blast intro: subset_imp_LeadsTo)+ |
|
301 |
done |
|
302 |
||
303 |
||
13798 | 304 |
subsection{*Induction rules*} |
13796 | 305 |
|
306 |
(** Meta or object quantifier ????? **) |
|
307 |
lemma LeadsTo_wf_induct: |
|
308 |
"[| wf r; |
|
13805 | 309 |
\<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo |
310 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
311 |
==> F \<in> A LeadsTo B" |
|
312 |
apply (simp add: LeadsTo_eq_leadsTo) |
|
13796 | 313 |
apply (erule leadsTo_wf_induct) |
314 |
apply (blast intro: leadsTo_weaken) |
|
315 |
done |
|
316 |
||
317 |
||
318 |
lemma Bounded_induct: |
|
319 |
"[| wf r; |
|
13805 | 320 |
\<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo |
321 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
322 |
==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)" |
|
13796 | 323 |
apply (erule LeadsTo_wf_induct, safe) |
13805 | 324 |
apply (case_tac "m \<in> I") |
13796 | 325 |
apply (blast intro: LeadsTo_weaken) |
326 |
apply (blast intro: subset_imp_LeadsTo) |
|
327 |
done |
|
328 |
||
329 |
||
330 |
lemma LessThan_induct: |
|
13805 | 331 |
"(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)) |
332 |
==> F \<in> A LeadsTo B" |
|
333 |
by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) |
|
13796 | 334 |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13805
diff
changeset
|
335 |
text{*Integer version. Could generalize from 0 to any lower bound*} |
13796 | 336 |
lemma integ_0_le_induct: |
13805 | 337 |
"[| F \<in> Always {s. (0::int) \<le> f s}; |
338 |
!! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo |
|
339 |
((A \<inter> {s. f s < z}) \<union> B) |] |
|
340 |
==> F \<in> A LeadsTo B" |
|
13796 | 341 |
apply (rule_tac f = "nat o f" in LessThan_induct) |
342 |
apply (simp add: vimage_def) |
|
343 |
apply (rule Always_LeadsTo_weaken, assumption+) |
|
344 |
apply (auto simp add: nat_eq_iff nat_less_iff) |
|
345 |
done |
|
346 |
||
347 |
lemma LessThan_bounded_induct: |
|
13805 | 348 |
"!!l::nat. \<forall>m \<in> greaterThan l. |
349 |
F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |
|
350 |
==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)" |
|
351 |
apply (simp only: Diff_eq [symmetric] vimage_Compl |
|
352 |
Compl_greaterThan [symmetric]) |
|
353 |
apply (rule wf_less_than [THEN Bounded_induct], simp) |
|
13796 | 354 |
done |
355 |
||
356 |
lemma GreaterThan_bounded_induct: |
|
13805 | 357 |
"!!l::nat. \<forall>m \<in> lessThan l. |
358 |
F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B) |
|
359 |
==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)" |
|
13796 | 360 |
apply (rule_tac f = f and f1 = "%k. l - k" |
361 |
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
|
362 |
apply (simp add: Image_singleton, clarify) |
13796 | 363 |
apply (case_tac "m<l") |
13805 | 364 |
apply (blast intro: LeadsTo_weaken_R diff_less_mono2) |
365 |
apply (blast intro: not_leE subset_imp_LeadsTo) |
|
13796 | 366 |
done |
367 |
||
368 |
||
13798 | 369 |
subsection{*Completion: Binary and General Finite versions*} |
13796 | 370 |
|
371 |
lemma Completion: |
|
13805 | 372 |
"[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C); |
373 |
F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) |] |
|
374 |
==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)" |
|
375 |
apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib) |
|
13796 | 376 |
apply (blast intro: completion leadsTo_weaken) |
377 |
done |
|
378 |
||
379 |
lemma Finite_completion_lemma: |
|
380 |
"finite I |
|
13805 | 381 |
==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) --> |
382 |
(\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) --> |
|
383 |
F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13796 | 384 |
apply (erule finite_induct, auto) |
385 |
apply (rule Completion) |
|
386 |
prefer 4 |
|
387 |
apply (simp only: INT_simps [symmetric]) |
|
388 |
apply (rule Constrains_INT, auto) |
|
389 |
done |
|
390 |
||
391 |
lemma Finite_completion: |
|
392 |
"[| finite I; |
|
13805 | 393 |
!!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C); |
394 |
!!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |] |
|
395 |
==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13796 | 396 |
by (blast intro: Finite_completion_lemma [THEN mp, THEN mp]) |
397 |
||
398 |
lemma Stable_completion: |
|
13805 | 399 |
"[| F \<in> A LeadsTo A'; F \<in> Stable A'; |
400 |
F \<in> B LeadsTo B'; F \<in> Stable B' |] |
|
401 |
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')" |
|
13796 | 402 |
apply (unfold Stable_def) |
403 |
apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R]) |
|
404 |
apply (force+) |
|
405 |
done |
|
406 |
||
407 |
lemma Finite_stable_completion: |
|
408 |
"[| finite I; |
|
13805 | 409 |
!!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i); |
410 |
!!i. i \<in> I ==> F \<in> Stable (A' i) |] |
|
411 |
==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)" |
|
13796 | 412 |
apply (unfold Stable_def) |
413 |
apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R]) |
|
13805 | 414 |
apply (simp_all, blast+) |
13796 | 415 |
done |
416 |
||
4776 | 417 |
end |