author | wenzelm |
Tue, 13 Mar 2012 23:33:35 +0100 | |
changeset 46912 | e0cd5c4df8e6 |
parent 46911 | 6d2a2f0e904e |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26806
diff
changeset
|
1 |
(* Title: HOL/UNITY/ELT.thy |
8044 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1999 University of Cambridge |
|
4 |
||
5 |
leadsTo strengthened with a specification of the allowable sets transient parts |
|
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
6 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
7 |
TRY INSTEAD (to get rid of the {} and to gain strong induction) |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
8 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
9 |
elt :: "['a set set, 'a program, 'a set] => ('a set) set" |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
10 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
11 |
inductive "elt CC F B" |
13790 | 12 |
intros |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
13 |
|
13790 | 14 |
Weaken: "A <= B ==> A : elt CC F B" |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
15 |
|
13790 | 16 |
ETrans: "[| F : A ensures A'; A-A' : CC; A' : elt CC F B |] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26806
diff
changeset
|
17 |
==> A : elt CC F B" |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
18 |
|
13790 | 19 |
Union: "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B" |
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
20 |
|
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8072
diff
changeset
|
21 |
monos Pow_mono |
8044 | 22 |
*) |
23 |
||
13798 | 24 |
header{*Progress Under Allowable Sets*} |
25 |
||
16417 | 26 |
theory ELT imports Project begin |
8044 | 27 |
|
23767 | 28 |
inductive_set |
8044 | 29 |
(*LEADS-TO constant for the inductive definition*) |
30 |
elt :: "['a set set, 'a program] => ('a set * 'a set) set" |
|
23767 | 31 |
for CC :: "'a set set" and F :: "'a program" |
32 |
where |
|
8044 | 33 |
|
13790 | 34 |
Basis: "[| F : A ensures B; A-B : (insert {} CC) |] ==> (A,B) : elt CC F" |
8044 | 35 |
|
23767 | 36 |
| Trans: "[| (A,B) : elt CC F; (B,C) : elt CC F |] ==> (A,C) : elt CC F" |
8044 | 37 |
|
23767 | 38 |
| Union: "ALL A: S. (A,B) : elt CC F ==> (Union S, B) : elt CC F" |
8044 | 39 |
|
40 |
||
36866 | 41 |
definition |
8128 | 42 |
(*the set of all sets determined by f alone*) |
43 |
givenBy :: "['a => 'b] => 'a set set" |
|
36866 | 44 |
where "givenBy f = range (%B. f-` B)" |
8044 | 45 |
|
36866 | 46 |
definition |
8044 | 47 |
(*visible version of the LEADS-TO relation*) |
48 |
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
|
49 |
("(3_/ leadsTo[_]/ _)" [80,0,80] 80) |
|
36866 | 50 |
where "leadsETo A CC B = {F. (A,B) : elt CC F}" |
8044 | 51 |
|
36866 | 52 |
definition |
8044 | 53 |
LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
54 |
("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) |
|
36866 | 55 |
where "LeadsETo A CC B = |
10834 | 56 |
{F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}" |
8044 | 57 |
|
13790 | 58 |
|
59 |
(*** givenBy ***) |
|
60 |
||
61 |
lemma givenBy_id [simp]: "givenBy id = UNIV" |
|
62 |
by (unfold givenBy_def, auto) |
|
63 |
||
64 |
lemma givenBy_eq_all: "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}" |
|
65 |
apply (unfold givenBy_def, safe) |
|
66 |
apply (rule_tac [2] x = "v ` ?u" in image_eqI, auto) |
|
67 |
done |
|
68 |
||
69 |
lemma givenByI: "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v" |
|
70 |
by (subst givenBy_eq_all, blast) |
|
71 |
||
72 |
lemma givenByD: "[| A: givenBy v; x:A; v x = v y |] ==> y: A" |
|
73 |
by (unfold givenBy_def, auto) |
|
74 |
||
75 |
lemma empty_mem_givenBy [iff]: "{} : givenBy v" |
|
76 |
by (blast intro!: givenByI) |
|
77 |
||
78 |
lemma givenBy_imp_eq_Collect: "A: givenBy v ==> EX P. A = {s. P(v s)}" |
|
79 |
apply (rule_tac x = "%n. EX s. v s = n & s : A" in exI) |
|
80 |
apply (simp (no_asm_use) add: givenBy_eq_all) |
|
81 |
apply blast |
|
82 |
done |
|
83 |
||
84 |
lemma Collect_mem_givenBy: "{s. P(v s)} : givenBy v" |
|
85 |
by (unfold givenBy_def, best) |
|
86 |
||
87 |
lemma givenBy_eq_Collect: "givenBy v = {A. EX P. A = {s. P(v s)}}" |
|
88 |
by (blast intro: Collect_mem_givenBy givenBy_imp_eq_Collect) |
|
89 |
||
90 |
(*preserving v preserves properties given by v*) |
|
91 |
lemma preserves_givenBy_imp_stable: |
|
92 |
"[| F : preserves v; D : givenBy v |] ==> F : stable D" |
|
13798 | 93 |
by (force simp add: preserves_subset_stable [THEN subsetD] givenBy_eq_Collect) |
13790 | 94 |
|
95 |
lemma givenBy_o_subset: "givenBy (w o v) <= givenBy v" |
|
96 |
apply (simp (no_asm) add: givenBy_eq_Collect) |
|
97 |
apply best |
|
98 |
done |
|
99 |
||
100 |
lemma givenBy_DiffI: |
|
101 |
"[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v" |
|
102 |
apply (simp (no_asm_use) add: givenBy_eq_Collect) |
|
103 |
apply safe |
|
104 |
apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI) |
|
26806 | 105 |
unfolding set_diff_eq |
26349 | 106 |
apply auto |
13790 | 107 |
done |
108 |
||
109 |
||
110 |
(** Standard leadsTo rules **) |
|
111 |
||
112 |
lemma leadsETo_Basis [intro]: |
|
113 |
"[| F: A ensures B; A-B: insert {} CC |] ==> F : A leadsTo[CC] B" |
|
114 |
apply (unfold leadsETo_def) |
|
115 |
apply (blast intro: elt.Basis) |
|
116 |
done |
|
117 |
||
118 |
lemma leadsETo_Trans: |
|
119 |
"[| F : A leadsTo[CC] B; F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C" |
|
120 |
apply (unfold leadsETo_def) |
|
121 |
apply (blast intro: elt.Trans) |
|
122 |
done |
|
123 |
||
124 |
||
125 |
(*Useful with cancellation, disjunction*) |
|
126 |
lemma leadsETo_Un_duplicate: |
|
127 |
"F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'" |
|
13819 | 128 |
by (simp add: Un_ac) |
13790 | 129 |
|
130 |
lemma leadsETo_Un_duplicate2: |
|
131 |
"F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)" |
|
132 |
by (simp add: Un_ac) |
|
133 |
||
134 |
(*The Union introduction rule as we should have liked to state it*) |
|
135 |
lemma leadsETo_Union: |
|
136 |
"(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B" |
|
137 |
apply (unfold leadsETo_def) |
|
138 |
apply (blast intro: elt.Union) |
|
139 |
done |
|
140 |
||
141 |
lemma leadsETo_UN: |
|
142 |
"(!!i. i : I ==> F : (A i) leadsTo[CC] B) |
|
143 |
==> F : (UN i:I. A i) leadsTo[CC] B" |
|
144 |
apply (subst Union_image_eq [symmetric]) |
|
145 |
apply (blast intro: leadsETo_Union) |
|
146 |
done |
|
147 |
||
148 |
(*The INDUCTION rule as we should have liked to state it*) |
|
149 |
lemma leadsETo_induct: |
|
150 |
"[| F : za leadsTo[CC] zb; |
|
151 |
!!A B. [| F : A ensures B; A-B : insert {} CC |] ==> P A B; |
|
152 |
!!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |] |
|
153 |
==> P A C; |
|
154 |
!!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B |
|
155 |
|] ==> P za zb" |
|
156 |
apply (unfold leadsETo_def) |
|
157 |
apply (drule CollectD) |
|
158 |
apply (erule elt.induct, blast+) |
|
159 |
done |
|
160 |
||
161 |
||
162 |
(** New facts involving leadsETo **) |
|
163 |
||
164 |
lemma leadsETo_mono: "CC' <= CC ==> (A leadsTo[CC'] B) <= (A leadsTo[CC] B)" |
|
165 |
apply safe |
|
166 |
apply (erule leadsETo_induct) |
|
167 |
prefer 3 apply (blast intro: leadsETo_Union) |
|
168 |
prefer 2 apply (blast intro: leadsETo_Trans) |
|
46577 | 169 |
apply blast |
13790 | 170 |
done |
171 |
||
172 |
lemma leadsETo_Trans_Un: |
|
173 |
"[| F : A leadsTo[CC] B; F : B leadsTo[DD] C |] |
|
174 |
==> F : A leadsTo[CC Un DD] C" |
|
175 |
by (blast intro: leadsETo_mono [THEN subsetD] leadsETo_Trans) |
|
176 |
||
177 |
lemma leadsETo_Union_Int: |
|
178 |
"(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) |
|
179 |
==> F : (Union S Int C) leadsTo[CC] B" |
|
180 |
apply (unfold leadsETo_def) |
|
181 |
apply (simp only: Int_Union_Union) |
|
182 |
apply (blast intro: elt.Union) |
|
183 |
done |
|
184 |
||
185 |
(*Binary union introduction rule*) |
|
186 |
lemma leadsETo_Un: |
|
187 |
"[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |] |
|
188 |
==> F : (A Un B) leadsTo[CC] C" |
|
44106 | 189 |
using leadsETo_Union [of "{A, B}" F CC C] by auto |
13790 | 190 |
|
191 |
lemma single_leadsETo_I: |
|
192 |
"(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B" |
|
13819 | 193 |
by (subst UN_singleton [symmetric], rule leadsETo_UN, blast) |
13790 | 194 |
|
195 |
||
196 |
lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B" |
|
13819 | 197 |
by (simp add: subset_imp_ensures [THEN leadsETo_Basis] |
198 |
Diff_eq_empty_iff [THEN iffD2]) |
|
13790 | 199 |
|
200 |
lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp] |
|
201 |
||
202 |
||
203 |
||
204 |
(** Weakening laws **) |
|
205 |
||
206 |
lemma leadsETo_weaken_R: |
|
207 |
"[| F : A leadsTo[CC] A'; A'<=B' |] ==> F : A leadsTo[CC] B'" |
|
13819 | 208 |
by (blast intro: subset_imp_leadsETo leadsETo_Trans) |
13790 | 209 |
|
46911 | 210 |
lemma leadsETo_weaken_L: |
13790 | 211 |
"[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'" |
13819 | 212 |
by (blast intro: leadsETo_Trans subset_imp_leadsETo) |
13790 | 213 |
|
214 |
(*Distributes over binary unions*) |
|
215 |
lemma leadsETo_Un_distrib: |
|
216 |
"F : (A Un B) leadsTo[CC] C = |
|
217 |
(F : A leadsTo[CC] C & F : B leadsTo[CC] C)" |
|
13819 | 218 |
by (blast intro: leadsETo_Un leadsETo_weaken_L) |
13790 | 219 |
|
220 |
lemma leadsETo_UN_distrib: |
|
221 |
"F : (UN i:I. A i) leadsTo[CC] B = |
|
222 |
(ALL i : I. F : (A i) leadsTo[CC] B)" |
|
13819 | 223 |
by (blast intro: leadsETo_UN leadsETo_weaken_L) |
13790 | 224 |
|
225 |
lemma leadsETo_Union_distrib: |
|
226 |
"F : (Union S) leadsTo[CC] B = (ALL A : S. F : A leadsTo[CC] B)" |
|
13819 | 227 |
by (blast intro: leadsETo_Union leadsETo_weaken_L) |
13790 | 228 |
|
229 |
lemma leadsETo_weaken: |
|
230 |
"[| F : A leadsTo[CC'] A'; B<=A; A'<=B'; CC' <= CC |] |
|
231 |
==> F : B leadsTo[CC] B'" |
|
232 |
apply (drule leadsETo_mono [THEN subsetD], assumption) |
|
13819 | 233 |
apply (blast del: subsetCE |
234 |
intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans) |
|
13790 | 235 |
done |
236 |
||
237 |
lemma leadsETo_givenBy: |
|
238 |
"[| F : A leadsTo[CC] A'; CC <= givenBy v |] |
|
239 |
==> F : A leadsTo[givenBy v] A'" |
|
46577 | 240 |
by (blast intro: leadsETo_weaken) |
13790 | 241 |
|
242 |
||
243 |
(*Set difference*) |
|
244 |
lemma leadsETo_Diff: |
|
245 |
"[| F : (A-B) leadsTo[CC] C; F : B leadsTo[CC] C |] |
|
246 |
==> F : A leadsTo[CC] C" |
|
247 |
by (blast intro: leadsETo_Un leadsETo_weaken) |
|
248 |
||
249 |
||
250 |
(*Binary union version*) |
|
251 |
lemma leadsETo_Un_Un: |
|
252 |
"[| F : A leadsTo[CC] A'; F : B leadsTo[CC] B' |] |
|
253 |
==> F : (A Un B) leadsTo[CC] (A' Un B')" |
|
254 |
by (blast intro: leadsETo_Un leadsETo_weaken_R) |
|
255 |
||
256 |
||
257 |
(** The cancellation law **) |
|
258 |
||
259 |
lemma leadsETo_cancel2: |
|
260 |
"[| F : A leadsTo[CC] (A' Un B); F : B leadsTo[CC] B' |] |
|
261 |
==> F : A leadsTo[CC] (A' Un B')" |
|
262 |
by (blast intro: leadsETo_Un_Un subset_imp_leadsETo leadsETo_Trans) |
|
263 |
||
264 |
lemma leadsETo_cancel1: |
|
265 |
"[| F : A leadsTo[CC] (B Un A'); F : B leadsTo[CC] B' |] |
|
266 |
==> F : A leadsTo[CC] (B' Un A')" |
|
267 |
apply (simp add: Un_commute) |
|
268 |
apply (blast intro!: leadsETo_cancel2) |
|
269 |
done |
|
270 |
||
271 |
lemma leadsETo_cancel_Diff1: |
|
272 |
"[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |] |
|
273 |
==> F : A leadsTo[CC] (B' Un A')" |
|
274 |
apply (rule leadsETo_cancel1) |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
275 |
prefer 2 apply assumption |
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
276 |
apply simp_all |
13790 | 277 |
done |
278 |
||
279 |
||
280 |
(** PSP: Progress-Safety-Progress **) |
|
281 |
||
282 |
(*Special case of PSP: Misra's "stable conjunction"*) |
|
283 |
lemma e_psp_stable: |
|
284 |
"[| F : A leadsTo[CC] A'; F : stable B; ALL C:CC. C Int B : CC |] |
|
285 |
==> F : (A Int B) leadsTo[CC] (A' Int B)" |
|
286 |
apply (unfold stable_def) |
|
287 |
apply (erule leadsETo_induct) |
|
288 |
prefer 3 apply (blast intro: leadsETo_Union_Int) |
|
289 |
prefer 2 apply (blast intro: leadsETo_Trans) |
|
290 |
apply (rule leadsETo_Basis) |
|
291 |
prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric]) |
|
13819 | 292 |
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] |
293 |
Int_Un_distrib2 [symmetric]) |
|
13790 | 294 |
apply (blast intro: transient_strengthen constrains_Int) |
295 |
done |
|
296 |
||
297 |
lemma e_psp_stable2: |
|
298 |
"[| F : A leadsTo[CC] A'; F : stable B; ALL C:CC. C Int B : CC |] |
|
299 |
==> F : (B Int A) leadsTo[CC] (B Int A')" |
|
300 |
by (simp (no_asm_simp) add: e_psp_stable Int_ac) |
|
301 |
||
302 |
lemma e_psp: |
|
303 |
"[| F : A leadsTo[CC] A'; F : B co B'; |
|
304 |
ALL C:CC. C Int B Int B' : CC |] |
|
305 |
==> F : (A Int B') leadsTo[CC] ((A' Int B) Un (B' - B))" |
|
306 |
apply (erule leadsETo_induct) |
|
307 |
prefer 3 apply (blast intro: leadsETo_Union_Int) |
|
308 |
(*Transitivity case has a delicate argument involving "cancellation"*) |
|
309 |
apply (rule_tac [2] leadsETo_Un_duplicate2) |
|
310 |
apply (erule_tac [2] leadsETo_cancel_Diff1) |
|
311 |
prefer 2 |
|
312 |
apply (simp add: Int_Diff Diff_triv) |
|
313 |
apply (blast intro: leadsETo_weaken_L dest: constrains_imp_subset) |
|
314 |
(*Basis case*) |
|
315 |
apply (rule leadsETo_Basis) |
|
316 |
apply (blast intro: psp_ensures) |
|
317 |
apply (subgoal_tac "A Int B' - (Ba Int B Un (B' - B)) = (A - Ba) Int B Int B'") |
|
318 |
apply auto |
|
319 |
done |
|
320 |
||
321 |
lemma e_psp2: |
|
322 |
"[| F : A leadsTo[CC] A'; F : B co B'; |
|
323 |
ALL C:CC. C Int B Int B' : CC |] |
|
324 |
==> F : (B' Int A) leadsTo[CC] ((B Int A') Un (B' - B))" |
|
325 |
by (simp add: e_psp Int_ac) |
|
326 |
||
327 |
||
328 |
(*** Special properties involving the parameter [CC] ***) |
|
329 |
||
330 |
(*??IS THIS NEEDED?? or is it just an example of what's provable??*) |
|
331 |
lemma gen_leadsETo_imp_Join_leadsETo: |
|
332 |
"[| F: (A leadsTo[givenBy v] B); G : preserves v; |
|
13819 | 333 |
F\<squnion>G : stable C |] |
334 |
==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)" |
|
13790 | 335 |
apply (erule leadsETo_induct) |
336 |
prefer 3 |
|
337 |
apply (subst Int_Union) |
|
338 |
apply (blast intro: leadsETo_UN) |
|
339 |
prefer 2 |
|
340 |
apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans) |
|
341 |
apply (rule leadsETo_Basis) |
|
13819 | 342 |
apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] |
46577 | 343 |
Int_Diff ensures_def givenBy_eq_Collect) |
13790 | 344 |
prefer 3 apply (blast intro: transient_strengthen) |
345 |
apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD]) |
|
346 |
apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD]) |
|
347 |
apply (unfold stable_def) |
|
348 |
apply (blast intro: constrains_Int [THEN constrains_weaken])+ |
|
349 |
done |
|
350 |
||
351 |
(**** Relationship with traditional "leadsTo", strong & weak ****) |
|
352 |
||
353 |
(** strong **) |
|
354 |
||
355 |
lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)" |
|
356 |
apply safe |
|
357 |
apply (erule leadsETo_induct) |
|
13819 | 358 |
prefer 3 apply (blast intro: leadsTo_Union) |
359 |
prefer 2 apply (blast intro: leadsTo_Trans, blast) |
|
13790 | 360 |
done |
361 |
||
362 |
lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)" |
|
363 |
apply safe |
|
364 |
apply (erule leadsETo_subset_leadsTo [THEN subsetD]) |
|
365 |
(*right-to-left case*) |
|
366 |
apply (erule leadsTo_induct) |
|
13819 | 367 |
prefer 3 apply (blast intro: leadsETo_Union) |
368 |
prefer 2 apply (blast intro: leadsETo_Trans, blast) |
|
13790 | 369 |
done |
370 |
||
371 |
(**** weak ****) |
|
372 |
||
373 |
lemma LeadsETo_eq_leadsETo: |
|
374 |
"A LeadsTo[CC] B = |
|
375 |
{F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] |
|
376 |
(reachable F Int B)}" |
|
377 |
apply (unfold LeadsETo_def) |
|
378 |
apply (blast dest: e_psp_stable2 intro: leadsETo_weaken) |
|
379 |
done |
|
380 |
||
381 |
(*** Introduction rules: Basis, Trans, Union ***) |
|
382 |
||
383 |
lemma LeadsETo_Trans: |
|
384 |
"[| F : A LeadsTo[CC] B; F : B LeadsTo[CC] C |] |
|
385 |
==> F : A LeadsTo[CC] C" |
|
386 |
apply (simp add: LeadsETo_eq_leadsETo) |
|
387 |
apply (blast intro: leadsETo_Trans) |
|
388 |
done |
|
389 |
||
390 |
lemma LeadsETo_Union: |
|
391 |
"(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B" |
|
392 |
apply (simp add: LeadsETo_def) |
|
393 |
apply (subst Int_Union) |
|
394 |
apply (blast intro: leadsETo_UN) |
|
395 |
done |
|
396 |
||
397 |
lemma LeadsETo_UN: |
|
398 |
"(!!i. i : I ==> F : (A i) LeadsTo[CC] B) |
|
399 |
==> F : (UN i:I. A i) LeadsTo[CC] B" |
|
400 |
apply (simp only: Union_image_eq [symmetric]) |
|
401 |
apply (blast intro: LeadsETo_Union) |
|
402 |
done |
|
403 |
||
404 |
(*Binary union introduction rule*) |
|
405 |
lemma LeadsETo_Un: |
|
406 |
"[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |] |
|
407 |
==> F : (A Un B) LeadsTo[CC] C" |
|
44106 | 408 |
using LeadsETo_Union [of "{A, B}" F CC C] by auto |
13790 | 409 |
|
410 |
(*Lets us look at the starting state*) |
|
411 |
lemma single_LeadsETo_I: |
|
412 |
"(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B" |
|
13819 | 413 |
by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast) |
13790 | 414 |
|
415 |
lemma subset_imp_LeadsETo: |
|
416 |
"A <= B ==> F : A LeadsTo[CC] B" |
|
417 |
apply (simp (no_asm) add: LeadsETo_def) |
|
418 |
apply (blast intro: subset_imp_leadsETo) |
|
419 |
done |
|
420 |
||
45605 | 421 |
lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo] |
13790 | 422 |
|
46911 | 423 |
lemma LeadsETo_weaken_R: |
13790 | 424 |
"[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'" |
46911 | 425 |
apply (simp add: LeadsETo_def) |
13790 | 426 |
apply (blast intro: leadsETo_weaken_R) |
427 |
done |
|
428 |
||
46911 | 429 |
lemma LeadsETo_weaken_L: |
13790 | 430 |
"[| F : A LeadsTo[CC] A'; B <= A |] ==> F : B LeadsTo[CC] A'" |
46911 | 431 |
apply (simp add: LeadsETo_def) |
13790 | 432 |
apply (blast intro: leadsETo_weaken_L) |
433 |
done |
|
434 |
||
435 |
lemma LeadsETo_weaken: |
|
436 |
"[| F : A LeadsTo[CC'] A'; |
|
437 |
B <= A; A' <= B'; CC' <= CC |] |
|
438 |
==> F : B LeadsTo[CC] B'" |
|
439 |
apply (simp (no_asm_use) add: LeadsETo_def) |
|
440 |
apply (blast intro: leadsETo_weaken) |
|
441 |
done |
|
442 |
||
443 |
lemma LeadsETo_subset_LeadsTo: "(A LeadsTo[CC] B) <= (A LeadsTo B)" |
|
444 |
apply (unfold LeadsETo_def LeadsTo_def) |
|
445 |
apply (blast intro: leadsETo_subset_leadsTo [THEN subsetD]) |
|
446 |
done |
|
447 |
||
448 |
(*Postcondition can be strengthened to (reachable F Int B) *) |
|
449 |
lemma reachable_ensures: |
|
450 |
"F : A ensures B ==> F : (reachable F Int A) ensures B" |
|
451 |
apply (rule stable_ensures_Int [THEN ensures_weaken_R], auto) |
|
452 |
done |
|
453 |
||
454 |
lemma lel_lemma: |
|
455 |
"F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B" |
|
456 |
apply (erule leadsTo_induct) |
|
46577 | 457 |
apply (blast intro: reachable_ensures) |
13790 | 458 |
apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L) |
459 |
apply (subst Int_Union) |
|
460 |
apply (blast intro: leadsETo_UN) |
|
461 |
done |
|
462 |
||
463 |
lemma LeadsETo_UNIV_eq_LeadsTo: "(A LeadsTo[UNIV] B) = (A LeadsTo B)" |
|
464 |
apply safe |
|
465 |
apply (erule LeadsETo_subset_LeadsTo [THEN subsetD]) |
|
466 |
(*right-to-left case*) |
|
467 |
apply (unfold LeadsETo_def LeadsTo_def) |
|
13836 | 468 |
apply (blast intro: lel_lemma [THEN leadsETo_weaken]) |
13790 | 469 |
done |
470 |
||
471 |
||
472 |
(**** EXTEND/PROJECT PROPERTIES ****) |
|
473 |
||
46912 | 474 |
context Extend |
475 |
begin |
|
476 |
||
477 |
lemma givenBy_o_eq_extend_set: |
|
13819 | 478 |
"givenBy (v o f) = extend_set h ` (givenBy v)" |
13836 | 479 |
apply (simp add: givenBy_eq_Collect) |
480 |
apply (rule equalityI, best) |
|
481 |
apply blast |
|
482 |
done |
|
13790 | 483 |
|
46912 | 484 |
lemma givenBy_eq_extend_set: "givenBy f = range (extend_set h)" |
13836 | 485 |
by (simp add: givenBy_eq_Collect, best) |
13790 | 486 |
|
46912 | 487 |
lemma extend_set_givenBy_I: |
13790 | 488 |
"D : givenBy v ==> extend_set h D : givenBy (v o f)" |
13836 | 489 |
apply (simp (no_asm_use) add: givenBy_eq_all, blast) |
13790 | 490 |
done |
491 |
||
46912 | 492 |
lemma leadsETo_imp_extend_leadsETo: |
13790 | 493 |
"F : A leadsTo[CC] B |
494 |
==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] |
|
495 |
(extend_set h B)" |
|
496 |
apply (erule leadsETo_induct) |
|
46577 | 497 |
apply (force intro: subset_imp_ensures |
13790 | 498 |
simp add: extend_ensures extend_set_Diff_distrib [symmetric]) |
499 |
apply (blast intro: leadsETo_Trans) |
|
500 |
apply (simp add: leadsETo_UN extend_set_Union) |
|
501 |
done |
|
502 |
||
503 |
||
504 |
(*This version's stronger in the "ensures" precondition |
|
505 |
BUT there's no ensures_weaken_L*) |
|
46912 | 506 |
lemma Join_project_ensures_strong: |
13790 | 507 |
"[| project h C G ~: transient (project_set h C Int (A-B)) | |
508 |
project_set h C Int (A - B) = {}; |
|
13819 | 509 |
extend h F\<squnion>G : stable C; |
510 |
F\<squnion>project h C G : (project_set h C Int A) ensures B |] |
|
511 |
==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)" |
|
13790 | 512 |
apply (subst Int_extend_set_lemma [symmetric]) |
513 |
apply (rule Join_project_ensures) |
|
514 |
apply (auto simp add: Int_Diff) |
|
515 |
done |
|
516 |
||
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
517 |
(*NOT WORKING. MODIFY AS IN Project.thy |
46912 | 518 |
lemma pld_lemma: |
13819 | 519 |
"[| extend h F\<squnion>G : stable C; |
520 |
F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B; |
|
13790 | 521 |
G : preserves (v o f) |] |
13819 | 522 |
==> extend h F\<squnion>G : |
13790 | 523 |
(C Int extend_set h (project_set h C Int A)) |
524 |
leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)" |
|
525 |
apply (erule leadsETo_induct) |
|
526 |
prefer 3 |
|
527 |
apply (simp del: UN_simps add: Int_UN_distrib leadsETo_UN extend_set_Union) |
|
528 |
prefer 2 |
|
529 |
apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans) |
|
530 |
txt{*Base case is hard*} |
|
531 |
apply auto |
|
532 |
apply (force intro: leadsETo_Basis subset_imp_ensures) |
|
533 |
apply (rule leadsETo_Basis) |
|
534 |
prefer 2 |
|
535 |
apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric]) |
|
536 |
apply (rule Join_project_ensures_strong) |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
537 |
apply (auto intro: project_stable_project_set simp add: Int_left_absorb) |
13790 | 538 |
apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set) |
539 |
done |
|
540 |
||
46912 | 541 |
lemma project_leadsETo_D_lemma: |
13819 | 542 |
"[| extend h F\<squnion>G : stable C; |
543 |
F\<squnion>project h C G : |
|
13790 | 544 |
(project_set h C Int A) |
545 |
leadsTo[(%D. project_set h C Int D)`givenBy v] B; |
|
546 |
G : preserves (v o f) |] |
|
13819 | 547 |
==> extend h F\<squnion>G : (C Int extend_set h A) |
13790 | 548 |
leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)" |
549 |
apply (rule pld_lemma [THEN leadsETo_weaken]) |
|
550 |
apply (auto simp add: split_extended_all) |
|
551 |
done |
|
552 |
||
46912 | 553 |
lemma project_leadsETo_D: |
13819 | 554 |
"[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B; |
13790 | 555 |
G : preserves (v o f) |] |
13819 | 556 |
==> extend h F\<squnion>G : (extend_set h A) |
13790 | 557 |
leadsTo[givenBy (v o f)] (extend_set h B)" |
558 |
apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) |
|
559 |
apply (erule leadsETo_givenBy) |
|
560 |
apply (rule givenBy_o_eq_extend_set [THEN equalityD2]) |
|
561 |
done |
|
562 |
||
46912 | 563 |
lemma project_LeadsETo_D: |
13819 | 564 |
"[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G |
13790 | 565 |
: A LeadsTo[givenBy v] B; |
566 |
G : preserves (v o f) |] |
|
13819 | 567 |
==> extend h F\<squnion>G : |
13790 | 568 |
(extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)" |
569 |
apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma]) |
|
570 |
apply (auto simp add: LeadsETo_def) |
|
571 |
apply (erule leadsETo_mono [THEN [2] rev_subsetD]) |
|
572 |
apply (blast intro: extend_set_givenBy_I) |
|
573 |
apply (simp add: project_set_reachable_extend_eq [symmetric]) |
|
574 |
done |
|
575 |
||
46912 | 576 |
lemma extending_leadsETo: |
13790 | 577 |
"(ALL G. extend h F ok G --> G : preserves (v o f)) |
578 |
==> extending (%G. UNIV) h F |
|
579 |
(extend_set h A leadsTo[givenBy (v o f)] extend_set h B) |
|
580 |
(A leadsTo[givenBy v] B)" |
|
581 |
apply (unfold extending_def) |
|
582 |
apply (auto simp add: project_leadsETo_D) |
|
583 |
done |
|
584 |
||
46912 | 585 |
lemma extending_LeadsETo: |
13790 | 586 |
"(ALL G. extend h F ok G --> G : preserves (v o f)) |
13819 | 587 |
==> extending (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 588 |
(extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) |
589 |
(A LeadsTo[givenBy v] B)" |
|
590 |
apply (unfold extending_def) |
|
591 |
apply (blast intro: project_LeadsETo_D) |
|
592 |
done |
|
13812
91713a1915ee
converting HOL/UNITY to use unconditional fairness
paulson
parents:
13798
diff
changeset
|
593 |
*) |
13790 | 594 |
|
595 |
||
596 |
(*** leadsETo in the precondition ***) |
|
597 |
||
598 |
(*Lemma for the Trans case*) |
|
46912 | 599 |
lemma pli_lemma: |
13819 | 600 |
"[| extend h F\<squnion>G : stable C; |
601 |
F\<squnion>project h C G |
|
13790 | 602 |
: project_set h C Int project_set h A leadsTo project_set h B |] |
13819 | 603 |
==> F\<squnion>project h C G |
13790 | 604 |
: project_set h C Int project_set h A leadsTo |
605 |
project_set h C Int project_set h B" |
|
606 |
apply (rule psp_stable2 [THEN leadsTo_weaken_L]) |
|
607 |
apply (auto simp add: project_stable_project_set extend_stable_project_set) |
|
608 |
done |
|
609 |
||
46912 | 610 |
lemma project_leadsETo_I_lemma: |
13819 | 611 |
"[| extend h F\<squnion>G : stable C; |
612 |
extend h F\<squnion>G : |
|
13790 | 613 |
(C Int A) leadsTo[(%D. C Int D)`givenBy f] B |] |
13819 | 614 |
==> F\<squnion>project h C G |
13790 | 615 |
: (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)" |
616 |
apply (erule leadsETo_induct) |
|
617 |
prefer 3 |
|
618 |
apply (simp only: Int_UN_distrib project_set_Union) |
|
619 |
apply (blast intro: leadsTo_UN) |
|
620 |
prefer 2 apply (blast intro: leadsTo_Trans pli_lemma) |
|
621 |
apply (simp add: givenBy_eq_extend_set) |
|
622 |
apply (rule leadsTo_Basis) |
|
623 |
apply (blast intro: ensures_extend_set_imp_project_ensures) |
|
624 |
done |
|
625 |
||
46912 | 626 |
lemma project_leadsETo_I: |
13819 | 627 |
"extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B) |
628 |
==> F\<squnion>project h UNIV G : A leadsTo B" |
|
13790 | 629 |
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto) |
630 |
done |
|
631 |
||
46912 | 632 |
lemma project_LeadsETo_I: |
13819 | 633 |
"extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) |
634 |
==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G |
|
13790 | 635 |
: A LeadsTo B" |
636 |
apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def) |
|
637 |
apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken]) |
|
638 |
apply (auto simp add: project_set_reachable_extend_eq [symmetric]) |
|
639 |
done |
|
640 |
||
46912 | 641 |
lemma projecting_leadsTo: |
13790 | 642 |
"projecting (%G. UNIV) h F |
643 |
(extend_set h A leadsTo[givenBy f] extend_set h B) |
|
644 |
(A leadsTo B)" |
|
645 |
apply (unfold projecting_def) |
|
646 |
apply (force dest: project_leadsETo_I) |
|
647 |
done |
|
648 |
||
46912 | 649 |
lemma projecting_LeadsTo: |
13819 | 650 |
"projecting (%G. reachable (extend h F\<squnion>G)) h F |
13790 | 651 |
(extend_set h A LeadsTo[givenBy f] extend_set h B) |
652 |
(A LeadsTo B)" |
|
653 |
apply (unfold projecting_def) |
|
654 |
apply (force dest: project_LeadsETo_I) |
|
655 |
done |
|
656 |
||
8044 | 657 |
end |
46912 | 658 |
|
659 |
end |