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/WFair |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Weak Fairness versions of transient, ensures, leadsTo. |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
13798 | 11 |
header{*Progress under Weak Fairness*} |
12 |
||
13797 | 13 |
theory WFair = UNITY: |
4776 | 14 |
|
15 |
constdefs |
|
16 |
||
5155 | 17 |
(*This definition specifies weak fairness. The rest of the theory |
18 |
is generic to all forms of fairness.*) |
|
5648 | 19 |
transient :: "'a set => 'a program set" |
13805 | 20 |
"transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}" |
4776 | 21 |
|
13797 | 22 |
ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) |
13805 | 23 |
"A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)" |
8006 | 24 |
|
6536 | 25 |
|
26 |
consts |
|
27 |
||
28 |
(*LEADS-TO constant for the inductive definition*) |
|
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset
|
29 |
leads :: "'a program => ('a set * 'a set) set" |
5648 | 30 |
|
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset
|
31 |
|
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6536
diff
changeset
|
32 |
inductive "leads F" |
13797 | 33 |
intros |
4776 | 34 |
|
13805 | 35 |
Basis: "F \<in> A ensures B ==> (A,B) \<in> leads F" |
4776 | 36 |
|
13805 | 37 |
Trans: "[| (A,B) \<in> leads F; (B,C) \<in> leads F |] ==> (A,C) \<in> leads F" |
4776 | 38 |
|
13805 | 39 |
Union: "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F" |
4776 | 40 |
|
5155 | 41 |
|
8006 | 42 |
constdefs |
6536 | 43 |
|
8006 | 44 |
(*visible version of the LEADS-TO relation*) |
13797 | 45 |
leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) |
13805 | 46 |
"A leadsTo B == {F. (A,B) \<in> leads F}" |
5648 | 47 |
|
48 |
(*wlt F B is the largest set that leads to B*) |
|
49 |
wlt :: "['a program, 'a set] => 'a set" |
|
13805 | 50 |
"wlt F B == Union {A. F \<in> A leadsTo B}" |
4776 | 51 |
|
9685 | 52 |
syntax (xsymbols) |
13797 | 53 |
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60) |
54 |
||
55 |
||
13798 | 56 |
subsection{*transient*} |
13797 | 57 |
|
58 |
lemma stable_transient_empty: |
|
13805 | 59 |
"[| F \<in> stable A; F \<in> transient A |] ==> A = {}" |
13797 | 60 |
by (unfold stable_def constrains_def transient_def, blast) |
61 |
||
62 |
lemma transient_strengthen: |
|
13805 | 63 |
"[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B" |
13797 | 64 |
apply (unfold transient_def, clarify) |
65 |
apply (blast intro!: rev_bexI) |
|
66 |
done |
|
67 |
||
68 |
lemma transientI: |
|
13805 | 69 |
"[| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> F \<in> transient A" |
13797 | 70 |
by (unfold transient_def, blast) |
71 |
||
72 |
lemma transientE: |
|
13805 | 73 |
"[| F \<in> transient A; |
74 |
!!act. [| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> P |] |
|
13797 | 75 |
==> P" |
76 |
by (unfold transient_def, blast) |
|
77 |
||
78 |
lemma transient_UNIV [simp]: "transient UNIV = {}" |
|
79 |
by (unfold transient_def, blast) |
|
80 |
||
81 |
lemma transient_empty [simp]: "transient {} = UNIV" |
|
82 |
by (unfold transient_def, auto) |
|
83 |
||
84 |
||
13798 | 85 |
subsection{*ensures*} |
13797 | 86 |
|
87 |
lemma ensuresI: |
|
13805 | 88 |
"[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B" |
13797 | 89 |
by (unfold ensures_def, blast) |
90 |
||
91 |
lemma ensuresD: |
|
13805 | 92 |
"F \<in> A ensures B ==> F \<in> (A-B) co (A \<union> B) & F \<in> transient (A-B)" |
13797 | 93 |
by (unfold ensures_def, blast) |
94 |
||
95 |
lemma ensures_weaken_R: |
|
13805 | 96 |
"[| F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'" |
13797 | 97 |
apply (unfold ensures_def) |
98 |
apply (blast intro: constrains_weaken transient_strengthen) |
|
99 |
done |
|
100 |
||
101 |
(*The L-version (precondition strengthening) fails, but we have this*) |
|
102 |
lemma stable_ensures_Int: |
|
13805 | 103 |
"[| F \<in> stable C; F \<in> A ensures B |] |
104 |
==> F \<in> (C \<inter> A) ensures (C \<inter> B)" |
|
13797 | 105 |
apply (unfold ensures_def) |
106 |
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric]) |
|
107 |
prefer 2 apply (blast intro: transient_strengthen) |
|
108 |
apply (blast intro: stable_constrains_Int constrains_weaken) |
|
109 |
done |
|
110 |
||
111 |
lemma stable_transient_ensures: |
|
13805 | 112 |
"[| F \<in> stable A; F \<in> transient C; A \<subseteq> B \<union> C |] ==> F \<in> A ensures B" |
13797 | 113 |
apply (simp add: ensures_def stable_def) |
114 |
apply (blast intro: constrains_weaken transient_strengthen) |
|
115 |
done |
|
116 |
||
13805 | 117 |
lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)" |
13797 | 118 |
by (simp (no_asm) add: ensures_def unless_def) |
119 |
||
120 |
||
13798 | 121 |
subsection{*leadsTo*} |
13797 | 122 |
|
13805 | 123 |
lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B" |
13797 | 124 |
apply (unfold leadsTo_def) |
125 |
apply (blast intro: leads.Basis) |
|
126 |
done |
|
127 |
||
128 |
lemma leadsTo_Trans: |
|
13805 | 129 |
"[| F \<in> A leadsTo B; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C" |
13797 | 130 |
apply (unfold leadsTo_def) |
131 |
apply (blast intro: leads.Trans) |
|
132 |
done |
|
133 |
||
13805 | 134 |
lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)" |
13797 | 135 |
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) |
136 |
||
137 |
(*Useful with cancellation, disjunction*) |
|
13805 | 138 |
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'" |
13797 | 139 |
by (simp add: Un_ac) |
140 |
||
141 |
lemma leadsTo_Un_duplicate2: |
|
13805 | 142 |
"F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)" |
13797 | 143 |
by (simp add: Un_ac) |
144 |
||
145 |
(*The Union introduction rule as we should have liked to state it*) |
|
146 |
lemma leadsTo_Union: |
|
13805 | 147 |
"(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B" |
13797 | 148 |
apply (unfold leadsTo_def) |
149 |
apply (blast intro: leads.Union) |
|
150 |
done |
|
151 |
||
152 |
lemma leadsTo_Union_Int: |
|
13805 | 153 |
"(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B" |
13797 | 154 |
apply (unfold leadsTo_def) |
155 |
apply (simp only: Int_Union_Union) |
|
156 |
apply (blast intro: leads.Union) |
|
157 |
done |
|
158 |
||
159 |
lemma leadsTo_UN: |
|
13805 | 160 |
"(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B" |
13797 | 161 |
apply (subst Union_image_eq [symmetric]) |
162 |
apply (blast intro: leadsTo_Union) |
|
163 |
done |
|
164 |
||
165 |
(*Binary union introduction rule*) |
|
166 |
lemma leadsTo_Un: |
|
13805 | 167 |
"[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C" |
13797 | 168 |
apply (subst Un_eq_Union) |
169 |
apply (blast intro: leadsTo_Union) |
|
170 |
done |
|
171 |
||
172 |
lemma single_leadsTo_I: |
|
13805 | 173 |
"(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B" |
13797 | 174 |
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) |
175 |
||
176 |
||
177 |
(*The INDUCTION rule as we should have liked to state it*) |
|
178 |
lemma leadsTo_induct: |
|
13805 | 179 |
"[| F \<in> za leadsTo zb; |
180 |
!!A B. F \<in> A ensures B ==> P A B; |
|
181 |
!!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |] |
|
13797 | 182 |
==> P A C; |
13805 | 183 |
!!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B |
13797 | 184 |
|] ==> P za zb" |
185 |
apply (unfold leadsTo_def) |
|
186 |
apply (drule CollectD, erule leads.induct) |
|
187 |
apply (blast+) |
|
188 |
done |
|
189 |
||
190 |
||
13805 | 191 |
lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B" |
13797 | 192 |
by (unfold ensures_def constrains_def transient_def, blast) |
193 |
||
194 |
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard] |
|
195 |
||
196 |
lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard] |
|
197 |
||
198 |
lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp] |
|
199 |
||
200 |
lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp] |
|
201 |
||
202 |
||
203 |
||
204 |
(** Variant induction rule: on the preconditions for B **) |
|
205 |
||
206 |
(*Lemma is the weak version: can't see how to do it in one step*) |
|
207 |
lemma leadsTo_induct_pre_lemma: |
|
13805 | 208 |
"[| F \<in> za leadsTo zb; |
13797 | 209 |
P zb; |
13805 | 210 |
!!A B. [| F \<in> A ensures B; P B |] ==> P A; |
211 |
!!S. \<forall>A \<in> S. P A ==> P (Union S) |
|
13797 | 212 |
|] ==> P za" |
213 |
(*by induction on this formula*) |
|
214 |
apply (subgoal_tac "P zb --> P za") |
|
215 |
(*now solve first subgoal: this formula is sufficient*) |
|
216 |
apply (blast intro: leadsTo_refl) |
|
217 |
apply (erule leadsTo_induct) |
|
218 |
apply (blast+) |
|
219 |
done |
|
220 |
||
221 |
lemma leadsTo_induct_pre: |
|
13805 | 222 |
"[| F \<in> za leadsTo zb; |
13797 | 223 |
P zb; |
13805 | 224 |
!!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P B |] ==> P A; |
225 |
!!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S) |
|
13797 | 226 |
|] ==> P za" |
13805 | 227 |
apply (subgoal_tac "F \<in> za leadsTo zb & P za") |
13797 | 228 |
apply (erule conjunct2) |
229 |
apply (erule leadsTo_induct_pre_lemma) |
|
230 |
prefer 3 apply (blast intro: leadsTo_Union) |
|
231 |
prefer 2 apply (blast intro: leadsTo_Trans) |
|
232 |
apply (blast intro: leadsTo_refl) |
|
233 |
done |
|
234 |
||
235 |
||
13805 | 236 |
lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'" |
13797 | 237 |
by (blast intro: subset_imp_leadsTo leadsTo_Trans) |
238 |
||
13798 | 239 |
lemma leadsTo_weaken_L [rule_format]: |
13805 | 240 |
"[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'" |
13797 | 241 |
by (blast intro: leadsTo_Trans subset_imp_leadsTo) |
242 |
||
243 |
(*Distributes over binary unions*) |
|
244 |
lemma leadsTo_Un_distrib: |
|
13805 | 245 |
"F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)" |
13797 | 246 |
by (blast intro: leadsTo_Un leadsTo_weaken_L) |
247 |
||
248 |
lemma leadsTo_UN_distrib: |
|
13805 | 249 |
"F \<in> (\<Union>i \<in> I. A i) leadsTo B = (\<forall>i \<in> I. F \<in> (A i) leadsTo B)" |
13797 | 250 |
by (blast intro: leadsTo_UN leadsTo_weaken_L) |
251 |
||
252 |
lemma leadsTo_Union_distrib: |
|
13805 | 253 |
"F \<in> (Union S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)" |
13797 | 254 |
by (blast intro: leadsTo_Union leadsTo_weaken_L) |
255 |
||
256 |
||
257 |
lemma leadsTo_weaken: |
|
13805 | 258 |
"[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'" |
13797 | 259 |
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans) |
260 |
||
261 |
||
262 |
(*Set difference: maybe combine with leadsTo_weaken_L?*) |
|
263 |
lemma leadsTo_Diff: |
|
13805 | 264 |
"[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C" |
13797 | 265 |
by (blast intro: leadsTo_Un leadsTo_weaken) |
266 |
||
267 |
lemma leadsTo_UN_UN: |
|
13805 | 268 |
"(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i)) |
269 |
==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)" |
|
13797 | 270 |
apply (simp only: Union_image_eq [symmetric]) |
271 |
apply (blast intro: leadsTo_Union leadsTo_weaken_R) |
|
272 |
done |
|
273 |
||
274 |
(*Binary union version*) |
|
275 |
lemma leadsTo_Un_Un: |
|
13805 | 276 |
"[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |] |
277 |
==> F \<in> (A \<union> B) leadsTo (A' \<union> B')" |
|
13797 | 278 |
by (blast intro: leadsTo_Un leadsTo_weaken_R) |
279 |
||
280 |
||
281 |
(** The cancellation law **) |
|
282 |
||
283 |
lemma leadsTo_cancel2: |
|
13805 | 284 |
"[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |] |
285 |
==> F \<in> A leadsTo (A' \<union> B')" |
|
13797 | 286 |
by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans) |
287 |
||
288 |
lemma leadsTo_cancel_Diff2: |
|
13805 | 289 |
"[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |] |
290 |
==> F \<in> A leadsTo (A' \<union> B')" |
|
13797 | 291 |
apply (rule leadsTo_cancel2) |
292 |
prefer 2 apply assumption |
|
293 |
apply (simp_all (no_asm_simp)) |
|
294 |
done |
|
295 |
||
296 |
lemma leadsTo_cancel1: |
|
13805 | 297 |
"[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |] |
298 |
==> F \<in> A leadsTo (B' \<union> A')" |
|
13797 | 299 |
apply (simp add: Un_commute) |
300 |
apply (blast intro!: leadsTo_cancel2) |
|
301 |
done |
|
302 |
||
303 |
lemma leadsTo_cancel_Diff1: |
|
13805 | 304 |
"[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |] |
305 |
==> F \<in> A leadsTo (B' \<union> A')" |
|
13797 | 306 |
apply (rule leadsTo_cancel1) |
307 |
prefer 2 apply assumption |
|
308 |
apply (simp_all (no_asm_simp)) |
|
309 |
done |
|
310 |
||
311 |
||
312 |
||
313 |
(** The impossibility law **) |
|
314 |
||
13805 | 315 |
lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}" |
13797 | 316 |
apply (erule leadsTo_induct_pre) |
317 |
apply (simp_all add: ensures_def constrains_def transient_def, blast) |
|
318 |
done |
|
319 |
||
320 |
||
321 |
(** PSP: Progress-Safety-Progress **) |
|
322 |
||
323 |
(*Special case of PSP: Misra's "stable conjunction"*) |
|
324 |
lemma psp_stable: |
|
13805 | 325 |
"[| F \<in> A leadsTo A'; F \<in> stable B |] |
326 |
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)" |
|
13797 | 327 |
apply (unfold stable_def) |
328 |
apply (erule leadsTo_induct) |
|
329 |
prefer 3 apply (blast intro: leadsTo_Union_Int) |
|
330 |
prefer 2 apply (blast intro: leadsTo_Trans) |
|
331 |
apply (rule leadsTo_Basis) |
|
332 |
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric]) |
|
333 |
apply (blast intro: transient_strengthen constrains_Int) |
|
334 |
done |
|
335 |
||
336 |
lemma psp_stable2: |
|
13805 | 337 |
"[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')" |
13797 | 338 |
by (simp add: psp_stable Int_ac) |
339 |
||
340 |
lemma psp_ensures: |
|
13805 | 341 |
"[| F \<in> A ensures A'; F \<in> B co B' |] |
342 |
==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))" |
|
13797 | 343 |
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*) |
344 |
apply (blast intro: transient_strengthen) |
|
345 |
done |
|
346 |
||
347 |
lemma psp: |
|
13805 | 348 |
"[| F \<in> A leadsTo A'; F \<in> B co B' |] |
349 |
==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))" |
|
13797 | 350 |
apply (erule leadsTo_induct) |
351 |
prefer 3 apply (blast intro: leadsTo_Union_Int) |
|
352 |
txt{*Basis case*} |
|
353 |
apply (blast intro: psp_ensures) |
|
354 |
txt{*Transitivity case has a delicate argument involving "cancellation"*} |
|
355 |
apply (rule leadsTo_Un_duplicate2) |
|
356 |
apply (erule leadsTo_cancel_Diff1) |
|
357 |
apply (simp add: Int_Diff Diff_triv) |
|
358 |
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset) |
|
359 |
done |
|
360 |
||
361 |
lemma psp2: |
|
13805 | 362 |
"[| F \<in> A leadsTo A'; F \<in> B co B' |] |
363 |
==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))" |
|
13797 | 364 |
by (simp (no_asm_simp) add: psp Int_ac) |
365 |
||
366 |
lemma psp_unless: |
|
13805 | 367 |
"[| F \<in> A leadsTo A'; F \<in> B unless B' |] |
368 |
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')" |
|
13797 | 369 |
|
370 |
apply (unfold unless_def) |
|
371 |
apply (drule psp, assumption) |
|
372 |
apply (blast intro: leadsTo_weaken) |
|
373 |
done |
|
374 |
||
375 |
||
13798 | 376 |
subsection{*Proving the induction rules*} |
13797 | 377 |
|
378 |
(** The most general rule: r is any wf relation; f is any variant function **) |
|
379 |
||
380 |
lemma leadsTo_wf_induct_lemma: |
|
381 |
"[| wf r; |
|
13805 | 382 |
\<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo |
383 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
384 |
==> F \<in> (A \<inter> f-`{m}) leadsTo B" |
|
13797 | 385 |
apply (erule_tac a = m in wf_induct) |
13805 | 386 |
apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B") |
13797 | 387 |
apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate) |
388 |
apply (subst vimage_eq_UN) |
|
389 |
apply (simp only: UN_simps [symmetric]) |
|
390 |
apply (blast intro: leadsTo_UN) |
|
391 |
done |
|
392 |
||
393 |
||
394 |
(** Meta or object quantifier ? **) |
|
395 |
lemma leadsTo_wf_induct: |
|
396 |
"[| wf r; |
|
13805 | 397 |
\<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo |
398 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
399 |
==> F \<in> A leadsTo B" |
|
13797 | 400 |
apply (rule_tac t = A in subst) |
401 |
defer 1 |
|
402 |
apply (rule leadsTo_UN) |
|
403 |
apply (erule leadsTo_wf_induct_lemma) |
|
404 |
apply assumption |
|
405 |
apply fast (*Blast_tac: Function unknown's argument not a parameter*) |
|
406 |
done |
|
407 |
||
408 |
||
409 |
lemma bounded_induct: |
|
410 |
"[| wf r; |
|
13805 | 411 |
\<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo |
412 |
((A \<inter> f-`(r^-1 `` {m})) \<union> B) |] |
|
413 |
==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)" |
|
13797 | 414 |
apply (erule leadsTo_wf_induct, safe) |
13805 | 415 |
apply (case_tac "m \<in> I") |
13797 | 416 |
apply (blast intro: leadsTo_weaken) |
417 |
apply (blast intro: subset_imp_leadsTo) |
|
418 |
done |
|
419 |
||
420 |
||
13805 | 421 |
(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*) |
13797 | 422 |
lemma lessThan_induct: |
13805 | 423 |
"[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..m(}) \<union> B) |] |
424 |
==> F \<in> A leadsTo B" |
|
13797 | 425 |
apply (rule wf_less_than [THEN leadsTo_wf_induct]) |
426 |
apply (simp (no_asm_simp)) |
|
427 |
apply blast |
|
428 |
done |
|
429 |
||
430 |
lemma lessThan_bounded_induct: |
|
13805 | 431 |
"!!l::nat. [| \<forall>m \<in> greaterThan l. |
432 |
F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |] |
|
433 |
==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)" |
|
13797 | 434 |
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric]) |
435 |
apply (rule wf_less_than [THEN bounded_induct]) |
|
436 |
apply (simp (no_asm_simp)) |
|
437 |
done |
|
438 |
||
439 |
lemma greaterThan_bounded_induct: |
|
13805 | 440 |
"(!!l::nat. \<forall>m \<in> lessThan l. |
441 |
F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)) |
|
442 |
==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)" |
|
13797 | 443 |
apply (rule_tac f = f and f1 = "%k. l - k" |
444 |
in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct]) |
|
445 |
apply (simp (no_asm) add: inv_image_def Image_singleton) |
|
446 |
apply clarify |
|
447 |
apply (case_tac "m<l") |
|
13805 | 448 |
apply (blast intro: leadsTo_weaken_R diff_less_mono2) |
449 |
apply (blast intro: not_leE subset_imp_leadsTo) |
|
13797 | 450 |
done |
451 |
||
452 |
||
13798 | 453 |
subsection{*wlt*} |
13797 | 454 |
|
455 |
(*Misra's property W3*) |
|
13805 | 456 |
lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B" |
13797 | 457 |
apply (unfold wlt_def) |
458 |
apply (blast intro!: leadsTo_Union) |
|
459 |
done |
|
460 |
||
13805 | 461 |
lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B" |
13797 | 462 |
apply (unfold wlt_def) |
463 |
apply (blast intro!: leadsTo_Union) |
|
464 |
done |
|
465 |
||
466 |
(*Misra's property W2*) |
|
13805 | 467 |
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)" |
13797 | 468 |
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) |
469 |
||
470 |
(*Misra's property W4*) |
|
13805 | 471 |
lemma wlt_increasing: "B \<subseteq> wlt F B" |
13797 | 472 |
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) |
473 |
done |
|
474 |
||
475 |
||
476 |
(*Used in the Trans case below*) |
|
477 |
lemma lemma1: |
|
13805 | 478 |
"[| B \<subseteq> A2; |
479 |
F \<in> (A1 - B) co (A1 \<union> B); |
|
480 |
F \<in> (A2 - C) co (A2 \<union> C) |] |
|
481 |
==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)" |
|
13797 | 482 |
by (unfold constrains_def, clarify, blast) |
483 |
||
484 |
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
|
485 |
lemma leadsTo_123: |
|
13805 | 486 |
"F \<in> A leadsTo A' |
487 |
==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')" |
|
13797 | 488 |
apply (erule leadsTo_induct) |
489 |
(*Basis*) |
|
490 |
apply (blast dest: ensuresD) |
|
491 |
(*Trans*) |
|
492 |
apply clarify |
|
13805 | 493 |
apply (rule_tac x = "Ba \<union> Bb" in exI) |
13797 | 494 |
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) |
495 |
(*Union*) |
|
496 |
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) |
|
13805 | 497 |
apply (rule_tac x = "\<Union>A \<in> S. f A" in exI) |
13797 | 498 |
apply (auto intro: leadsTo_UN) |
499 |
(*Blast_tac says PROOF FAILED*) |
|
13805 | 500 |
apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B" |
13798 | 501 |
in constrains_UN [THEN constrains_weaken], auto) |
13797 | 502 |
done |
503 |
||
504 |
||
505 |
(*Misra's property W5*) |
|
13805 | 506 |
lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)" |
13798 | 507 |
proof - |
508 |
from wlt_leadsTo [of F B, THEN leadsTo_123] |
|
509 |
show ?thesis |
|
510 |
proof (elim exE conjE) |
|
511 |
(* assumes have to be in exactly the form as in the goal displayed at |
|
512 |
this point. Isar doesn't give you any automation. *) |
|
513 |
fix C |
|
514 |
assume wlt: "wlt F B \<subseteq> C" |
|
515 |
and lt: "F \<in> C leadsTo B" |
|
516 |
and co: "F \<in> C - B co C \<union> B" |
|
517 |
have eq: "C = wlt F B" |
|
518 |
proof - |
|
519 |
from lt and wlt show ?thesis |
|
520 |
by (blast dest: leadsTo_eq_subset_wlt [THEN iffD1]) |
|
521 |
qed |
|
522 |
from co show ?thesis by (simp add: eq wlt_increasing Un_absorb2) |
|
523 |
qed |
|
524 |
qed |
|
13797 | 525 |
|
526 |
||
13798 | 527 |
subsection{*Completion: Binary and General Finite versions*} |
13797 | 528 |
|
529 |
lemma completion_lemma : |
|
13805 | 530 |
"[| W = wlt F (B' \<union> C); |
531 |
F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C); |
|
532 |
F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) |] |
|
533 |
==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)" |
|
534 |
apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ") |
|
13797 | 535 |
prefer 2 |
536 |
apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, |
|
537 |
THEN constrains_weaken]) |
|
13805 | 538 |
apply (subgoal_tac "F \<in> (W-C) co W") |
13797 | 539 |
prefer 2 |
540 |
apply (simp add: wlt_increasing Un_assoc Un_absorb2) |
|
13805 | 541 |
apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ") |
13797 | 542 |
prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken]) |
543 |
(** LEVEL 6 **) |
|
13805 | 544 |
apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ") |
13797 | 545 |
prefer 2 |
546 |
apply (rule leadsTo_Un_duplicate2) |
|
547 |
apply (blast intro: leadsTo_Un_Un wlt_leadsTo |
|
548 |
[THEN psp2, THEN leadsTo_weaken] leadsTo_refl) |
|
549 |
apply (drule leadsTo_Diff) |
|
550 |
apply (blast intro: subset_imp_leadsTo) |
|
13805 | 551 |
apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W") |
13797 | 552 |
prefer 2 |
553 |
apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono]) |
|
554 |
apply (blast intro: leadsTo_Trans subset_imp_leadsTo) |
|
555 |
done |
|
556 |
||
557 |
lemmas completion = completion_lemma [OF refl] |
|
558 |
||
559 |
lemma finite_completion_lemma: |
|
13805 | 560 |
"finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) --> |
561 |
(\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) --> |
|
562 |
F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13797 | 563 |
apply (erule finite_induct, auto) |
564 |
apply (rule completion) |
|
565 |
prefer 4 |
|
566 |
apply (simp only: INT_simps [symmetric]) |
|
567 |
apply (rule constrains_INT, auto) |
|
568 |
done |
|
569 |
||
570 |
lemma finite_completion: |
|
571 |
"[| finite I; |
|
13805 | 572 |
!!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C); |
573 |
!!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |] |
|
574 |
==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)" |
|
13797 | 575 |
by (blast intro: finite_completion_lemma [THEN mp, THEN mp]) |
576 |
||
577 |
lemma stable_completion: |
|
13805 | 578 |
"[| F \<in> A leadsTo A'; F \<in> stable A'; |
579 |
F \<in> B leadsTo B'; F \<in> stable B' |] |
|
580 |
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')" |
|
13797 | 581 |
apply (unfold stable_def) |
582 |
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R]) |
|
583 |
apply (force+) |
|
584 |
done |
|
585 |
||
586 |
lemma finite_stable_completion: |
|
587 |
"[| finite I; |
|
13805 | 588 |
!!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i); |
589 |
!!i. i \<in> I ==> F \<in> stable (A' i) |] |
|
590 |
==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)" |
|
13797 | 591 |
apply (unfold stable_def) |
592 |
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R]) |
|
593 |
apply (simp_all (no_asm_simp)) |
|
594 |
apply blast+ |
|
595 |
done |
|
9685 | 596 |
|
4776 | 597 |
end |