author | paulson |
Wed, 15 Dec 1999 10:45:37 +0100 | |
changeset 8065 | 658e0d4e4ed9 |
parent 8055 | bb15396278fb |
child 8122 | b43ad07660b9 |
permissions | -rw-r--r-- |
7186 | 1 |
(* Title: HOL/UNITY/Lift_prog.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
7482 | 5 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
6 |
Arrays of processes. Many results are instances of those in Extend & Project. |
7186 | 7 |
*) |
8 |
||
9 |
||
10 |
(*** Basic properties ***) |
|
11 |
||
12 |
(** lift_set and drop_set **) |
|
13 |
||
14 |
Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
|
15 |
by Auto_tac; |
|
16 |
qed "lift_set_iff"; |
|
17 |
AddIffs [lift_set_iff]; |
|
18 |
||
7525 | 19 |
Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)"; |
20 |
by Auto_tac; |
|
21 |
qed "Int_lift_set"; |
|
22 |
||
23 |
Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)"; |
|
7186 | 24 |
by Auto_tac; |
7525 | 25 |
qed "Un_lift_set"; |
26 |
||
27 |
Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)"; |
|
28 |
by Auto_tac; |
|
29 |
qed "Diff_lift_set"; |
|
30 |
||
31 |
Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set]; |
|
7186 | 32 |
|
33 |
(** lift_act and drop_act **) |
|
34 |
||
7688 | 35 |
(*For compatibility with the original definition and perhaps simpler proofs*) |
36 |
Goalw [lift_act_def] |
|
37 |
"((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
|
38 |
by Auto_tac; |
|
39 |
by (rtac exI 1); |
|
40 |
by Auto_tac; |
|
41 |
qed "lift_act_eq"; |
|
42 |
AddIffs [lift_act_eq]; |
|
43 |
||
7186 | 44 |
(** lift_prog and drop_prog **) |
45 |
||
46 |
Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
|
47 |
by Auto_tac; |
|
48 |
qed "Init_lift_prog"; |
|
49 |
Addsimps [Init_lift_prog]; |
|
50 |
||
51 |
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
|
8041 | 52 |
by (auto_tac (claset() addIs [rev_image_eqI], simpset())); |
7186 | 53 |
qed "Acts_lift_prog"; |
54 |
Addsimps [Acts_lift_prog]; |
|
55 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
56 |
Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)"; |
7186 | 57 |
by Auto_tac; |
58 |
qed "Init_drop_prog"; |
|
59 |
Addsimps [Init_drop_prog]; |
|
60 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
61 |
Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)"; |
8041 | 62 |
by (auto_tac (claset() addIs [image_eqI], |
7688 | 63 |
simpset() addsimps [drop_prog_def])); |
7186 | 64 |
qed "Acts_drop_prog"; |
65 |
Addsimps [Acts_drop_prog]; |
|
66 |
||
7688 | 67 |
|
68 |
(*** sub ***) |
|
69 |
||
7947 | 70 |
Goal "sub i f = f i"; |
71 |
by (simp_tac (simpset() addsimps [sub_def]) 1); |
|
72 |
qed "sub_apply"; |
|
73 |
Addsimps [sub_apply]; |
|
7688 | 74 |
|
75 |
Goal "lift_set i {s. P s} = {s. P (sub i s)}"; |
|
76 |
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
77 |
qed "lift_set_sub"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
78 |
|
7688 | 79 |
Goal "{s. P (s i)} = lift_set i {s. P s}"; |
80 |
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
81 |
qed "Collect_eq_lift_set"; |
|
7186 | 82 |
|
7688 | 83 |
Goal "sub i -`` A = lift_set i A"; |
84 |
by (Force_tac 1); |
|
85 |
qed "sub_vimage"; |
|
86 |
Addsimps [sub_vimage]; |
|
87 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
88 |
(*For tidying the result of "export"*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
89 |
Goal "v o (%z. z i) = v o sub i"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
90 |
by (simp_tac (simpset() addsimps [sub_def]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
91 |
qed "fold_o_sub"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
92 |
|
7688 | 93 |
|
94 |
||
95 |
(*** lift_prog and the lattice operations ***) |
|
7186 | 96 |
|
97 |
Goal "lift_prog i SKIP = SKIP"; |
|
98 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
99 |
simpset() addsimps [SKIP_def, lift_prog_def])); |
|
100 |
qed "lift_prog_SKIP"; |
|
101 |
||
102 |
Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)"; |
|
103 |
by (rtac program_equalityI 1); |
|
7537 | 104 |
by Auto_tac; |
7186 | 105 |
qed "lift_prog_Join"; |
106 |
||
7525 | 107 |
Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))"; |
7186 | 108 |
by (rtac program_equalityI 1); |
7537 | 109 |
by Auto_tac; |
7186 | 110 |
qed "lift_prog_JN"; |
111 |
||
112 |
||
7525 | 113 |
(*** Equivalence with "extend" version ***) |
114 |
||
115 |
Goalw [lift_map_def] "good_map (lift_map i)"; |
|
116 |
by (rtac good_mapI 1); |
|
117 |
by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1); |
|
118 |
by Auto_tac; |
|
119 |
by (dres_inst_tac [("f", "%f. f i")] arg_cong 1); |
|
120 |
by Auto_tac; |
|
121 |
qed "good_map_lift_map"; |
|
122 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
123 |
fun lift_export th = |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
124 |
good_map_lift_map RS export th |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
125 |
|> simplify (simpset() addsimps [fold_o_sub]);; |
7525 | 126 |
|
127 |
Goal "fst (inv (lift_map i) g) = g i"; |
|
128 |
by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1); |
|
129 |
by (auto_tac (claset(), simpset() addsimps [lift_map_def])); |
|
130 |
qed "fst_inv_lift_map"; |
|
131 |
Addsimps [fst_inv_lift_map]; |
|
132 |
||
133 |
||
134 |
Goal "lift_set i A = extend_set (lift_map i) A"; |
|
135 |
by (auto_tac (claset(), |
|
136 |
simpset() addsimps [lift_export mem_extend_set_iff])); |
|
137 |
qed "lift_set_correct"; |
|
138 |
||
139 |
Goalw [drop_set_def, project_set_def, lift_map_def] |
|
140 |
"drop_set i A = project_set (lift_map i) A"; |
|
141 |
by Auto_tac; |
|
142 |
by (rtac image_eqI 2); |
|
143 |
by (rtac exI 1); |
|
144 |
by (stac (refl RS fun_upd_idem) 1); |
|
145 |
by Auto_tac; |
|
146 |
qed "drop_set_correct"; |
|
147 |
||
148 |
Goal "lift_act i = extend_act (lift_map i)"; |
|
149 |
by (rtac ext 1); |
|
150 |
by Auto_tac; |
|
151 |
by (forward_tac [lift_export extend_act_D] 2); |
|
7688 | 152 |
by (auto_tac (claset(), simpset() addsimps [extend_act_def])); |
7525 | 153 |
by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def])); |
154 |
by (rtac bexI 1); |
|
155 |
by (auto_tac (claset() addSIs [exI], simpset())); |
|
156 |
qed "lift_act_correct"; |
|
157 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7840
diff
changeset
|
158 |
Goal "drop_act i = project_act (lift_map i)"; |
7525 | 159 |
by (rtac ext 1); |
160 |
by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]); |
|
161 |
by Auto_tac; |
|
7688 | 162 |
by (REPEAT_FIRST (ares_tac [exI, conjI])); |
7525 | 163 |
by Auto_tac; |
7688 | 164 |
by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem))); |
7525 | 165 |
qed "drop_act_correct"; |
166 |
||
7688 | 167 |
Goal "lift_prog i = extend (lift_map i)"; |
168 |
by (rtac (program_equalityI RS ext) 1); |
|
7525 | 169 |
by (simp_tac (simpset() addsimps [lift_set_correct]) 1); |
170 |
by (simp_tac (simpset() |
|
171 |
addsimps [lift_export Acts_extend, |
|
172 |
lift_act_correct]) 1); |
|
173 |
qed "lift_prog_correct"; |
|
174 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
175 |
Goal "drop_prog i C = project (lift_map i) C"; |
7688 | 176 |
by (rtac (program_equalityI RS ext) 1); |
7525 | 177 |
by (simp_tac (simpset() addsimps [drop_set_correct]) 1); |
178 |
by (simp_tac (simpset() |
|
7547
a72a551b6d79
new proof of drop_prog_correct for new definition of project_act
paulson
parents:
7537
diff
changeset
|
179 |
addsimps [Acts_project, drop_act_correct]) 1); |
7525 | 180 |
qed "drop_prog_correct"; |
181 |
||
182 |
||
7688 | 183 |
(** Injectivity of lift_set, lift_act, lift_prog **) |
184 |
||
185 |
Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F"; |
|
186 |
by Auto_tac; |
|
187 |
qed "lift_set_inverse"; |
|
188 |
Addsimps [lift_set_inverse]; |
|
189 |
||
190 |
Goal "inj (lift_set i)"; |
|
191 |
by (rtac inj_on_inverseI 1); |
|
192 |
by (rtac lift_set_inverse 1); |
|
193 |
qed "inj_lift_set"; |
|
194 |
||
195 |
(*Because A and B could differ outside i, cannot generalize result to |
|
196 |
drop_set i (A Int B) = drop_set i A Int drop_set i B |
|
197 |
*) |
|
198 |
Goalw [lift_set_def, drop_set_def] |
|
199 |
"drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; |
|
200 |
by Auto_tac; |
|
201 |
qed "drop_set_Int_lift_set"; |
|
202 |
||
203 |
Goalw [lift_set_def, drop_set_def] |
|
204 |
"drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A"; |
|
205 |
by Auto_tac; |
|
206 |
qed "drop_set_Int_lift_set2"; |
|
207 |
||
208 |
Goalw [drop_set_def] |
|
209 |
"i : I ==> drop_set i (INT j:I. lift_set j A) = A"; |
|
210 |
by Auto_tac; |
|
211 |
qed "drop_set_INT"; |
|
212 |
||
213 |
Goal "lift_set i UNIV = UNIV"; |
|
214 |
by (simp_tac |
|
215 |
(simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1); |
|
216 |
qed "lift_set_UNIV_eq"; |
|
217 |
Addsimps [lift_set_UNIV_eq]; |
|
218 |
||
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7840
diff
changeset
|
219 |
(* |
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7840
diff
changeset
|
220 |
Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act"; |
7688 | 221 |
by (asm_full_simp_tac |
222 |
(simpset() addsimps [drop_set_correct, drop_act_correct, |
|
223 |
lift_act_correct, lift_export extend_act_inverse]) 1); |
|
224 |
qed "lift_act_inverse"; |
|
225 |
Addsimps [lift_act_inverse]; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7840
diff
changeset
|
226 |
*) |
7688 | 227 |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
228 |
Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F"; |
7688 | 229 |
by (asm_full_simp_tac |
230 |
(simpset() addsimps [drop_set_correct, drop_prog_correct, |
|
231 |
lift_prog_correct, lift_export extend_inverse]) 1); |
|
232 |
qed "lift_prog_inverse"; |
|
233 |
Addsimps [lift_prog_inverse]; |
|
234 |
||
235 |
Goal "inj (lift_prog i)"; |
|
236 |
by (simp_tac |
|
237 |
(simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1); |
|
238 |
qed "inj_lift_prog"; |
|
239 |
||
240 |
||
7525 | 241 |
(*** More Lemmas ***) |
242 |
||
243 |
Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)"; |
|
244 |
by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct, |
|
245 |
lift_export extend_act_Image]) 1); |
|
246 |
qed "lift_act_Image"; |
|
247 |
Addsimps [lift_act_Image]; |
|
248 |
||
249 |
||
250 |
||
7186 | 251 |
(*** Safety: co, stable, invariant ***) |
252 |
||
253 |
(** Safety and lift_prog **) |
|
254 |
||
255 |
Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \ |
|
256 |
\ (F : A co B)"; |
|
257 |
by (auto_tac (claset(), |
|
258 |
simpset() addsimps [constrains_def])); |
|
259 |
by (Force_tac 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
260 |
qed "lift_prog_constrains"; |
7186 | 261 |
|
262 |
Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
263 |
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
264 |
qed "lift_prog_stable"; |
7186 | 265 |
|
266 |
Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)"; |
|
267 |
by (auto_tac (claset(), |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
268 |
simpset() addsimps [invariant_def, lift_prog_stable])); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
269 |
qed "lift_prog_invariant"; |
7186 | 270 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
271 |
Goal "[| lift_prog i F : A co B |] \ |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
272 |
\ ==> F : (drop_set i A) co (drop_set i B)"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
273 |
by (asm_full_simp_tac |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
274 |
(simpset() addsimps [drop_set_correct, lift_prog_correct, |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
275 |
lift_export extend_constrains_project_set]) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
276 |
qed "lift_prog_constrains_drop_set"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7688
diff
changeset
|
277 |
|
7186 | 278 |
(*This one looks strange! Proof probably is by case analysis on i=j. |
279 |
If i~=j then lift_prog j (F j) does nothing to lift_set i, and the |
|
280 |
premise ensures A<=B.*) |
|
281 |
Goal "F i : A co B \ |
|
282 |
\ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)"; |
|
283 |
by (auto_tac (claset(), |
|
284 |
simpset() addsimps [constrains_def])); |
|
285 |
by (REPEAT (Blast_tac 1)); |
|
286 |
qed "constrains_imp_lift_prog_constrains"; |
|
287 |
||
288 |
||
289 |
(** Safety and drop_prog **) |
|
290 |
||
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
291 |
Goal "(drop_prog i C F : A co B) = \ |
7688 | 292 |
\ (F : (C Int lift_set i A) co (lift_set i B) & A <= B)"; |
293 |
by (simp_tac |
|
294 |
(simpset() addsimps [drop_prog_correct, |
|
295 |
lift_set_correct, lift_export project_constrains]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
296 |
qed "drop_prog_constrains"; |
7186 | 297 |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
298 |
Goal "(drop_prog i UNIV F : stable A) = (F : stable (lift_set i A))"; |
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
299 |
by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
300 |
qed "drop_prog_stable"; |
7186 | 301 |
|
302 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
303 |
(*** Weak safety primitives: Co, Stable ***) |
7186 | 304 |
|
305 |
(** Reachability **) |
|
306 |
||
307 |
Goal "reachable (lift_prog i F) = lift_set i (reachable F)"; |
|
7688 | 308 |
by (simp_tac |
309 |
(simpset() addsimps [lift_prog_correct, lift_set_correct, |
|
310 |
lift_export reachable_extend_eq]) 1); |
|
7186 | 311 |
qed "reachable_lift_prog"; |
312 |
||
313 |
Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
|
314 |
\ (F : A Co B)"; |
|
7947 | 315 |
by (simp_tac |
316 |
(simpset() addsimps [lift_prog_correct, lift_set_correct, |
|
317 |
lift_export extend_Constrains]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
318 |
qed "lift_prog_Constrains"; |
7186 | 319 |
|
320 |
Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
321 |
by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
322 |
qed "lift_prog_Stable"; |
7186 | 323 |
|
7688 | 324 |
Goal "[| reachable (lift_prog i F Join G) <= C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
325 |
\ F Join drop_prog i C G : A Co B |] \ |
7688 | 326 |
\ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)"; |
327 |
by (asm_full_simp_tac |
|
328 |
(simpset() addsimps [lift_prog_correct, drop_prog_correct, |
|
329 |
lift_set_correct, lift_export project_Constrains_D]) 1); |
|
7186 | 330 |
qed "drop_prog_Constrains_D"; |
331 |
||
332 |
Goalw [Stable_def] |
|
7688 | 333 |
"[| reachable (lift_prog i F Join G) <= C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
334 |
\ F Join drop_prog i C G : Stable A |] \ |
7688 | 335 |
\ ==> lift_prog i F Join G : Stable (lift_set i A)"; |
7186 | 336 |
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1); |
337 |
qed "drop_prog_Stable_D"; |
|
338 |
||
7688 | 339 |
Goal "[| reachable (lift_prog i F Join G) <= C; \ |
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
340 |
\ F Join drop_prog i C G : Always A |] \ |
7688 | 341 |
\ ==> lift_prog i F Join G : Always (lift_set i A)"; |
342 |
by (asm_full_simp_tac |
|
343 |
(simpset() addsimps [lift_prog_correct, drop_prog_correct, |
|
344 |
lift_set_correct, lift_export project_Always_D]) 1); |
|
345 |
qed "drop_prog_Always_D"; |
|
7186 | 346 |
|
7688 | 347 |
Goalw [Increasing_def] |
348 |
"[| reachable (lift_prog i F Join G) <= C; \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
349 |
\ F Join drop_prog i C G : Increasing func |] \ |
7688 | 350 |
\ ==> lift_prog i F Join G : Increasing (func o (sub i))"; |
7186 | 351 |
by Auto_tac; |
7688 | 352 |
by (stac Collect_eq_lift_set 1); |
353 |
by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); |
|
354 |
qed "project_Increasing_D"; |
|
7186 | 355 |
|
7361 | 356 |
|
7688 | 357 |
(*UNUSED*) |
358 |
Goal "UNIV <= drop_set i C \ |
|
7880
62fb24e28e5e
exchanged the first two args of "project" and "drop_prog"
paulson
parents:
7878
diff
changeset
|
359 |
\ ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)"; |
7688 | 360 |
by (asm_full_simp_tac |
361 |
(simpset() addsimps [lift_prog_correct, drop_prog_correct, |
|
362 |
drop_set_correct, lift_export project_extend_Join]) 1); |
|
363 |
qed "drop_prog_lift_prog_Join"; |
|
7186 | 364 |
|
365 |
||
7525 | 366 |
(*** Progress: transient, ensures ***) |
367 |
||
368 |
Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)"; |
|
369 |
by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct, |
|
370 |
lift_export extend_transient]) 1); |
|
371 |
qed "lift_prog_transient"; |
|
372 |
||
373 |
Goal "(lift_prog i F : transient (lift_set j A)) = \ |
|
374 |
\ (i=j & F : transient A | A={})"; |
|
375 |
by (case_tac "i=j" 1); |
|
376 |
by (auto_tac (claset(), simpset() addsimps [lift_prog_transient])); |
|
377 |
by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def])); |
|
378 |
by (Force_tac 1); |
|
379 |
qed "lift_prog_transient_eq_disj"; |
|
380 |
||
381 |
||
7186 | 382 |
(*** guarantees properties ***) |
383 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
384 |
Goal "lift_prog i F : preserves (v o sub j) = \ |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
385 |
\ (if i=j then F : preserves v else True)"; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
386 |
by (simp_tac (simpset() addsimps [lift_prog_correct, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
387 |
lift_export extend_preserves]) 1); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
388 |
by (auto_tac (claset(), |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
389 |
simpset() addsimps [preserves_def, extend_def, extend_act_def, |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
390 |
stable_def, constrains_def, lift_map_def])); |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
391 |
qed "lift_prog_preserves_sub"; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
392 |
|
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
393 |
Addsimps [lift_prog_preserves_sub]; |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
394 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
395 |
Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
396 |
by (asm_simp_tac |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
397 |
(simpset() addsimps [drop_prog_correct, fold_o_sub, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
398 |
lift_export project_preserves_I]) 1); |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
399 |
qed "drop_prog_preserves_I"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
400 |
|
8041 | 401 |
(*The raw version*) |
402 |
val [xguary,drop_prog,lift_prog] = |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
403 |
Goal "[| F : X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
404 |
\ !!G. lift_prog i F Join G : X' ==> F Join drop_prog i C G : X; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
405 |
\ !!G. [| F Join drop_prog i C G : Y; lift_prog i F Join G : X' |] \ |
8041 | 406 |
\ ==> lift_prog i F Join G : Y' |] \ |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
407 |
\ ==> lift_prog i F : X' guarantees[v o sub i] Y'"; |
8041 | 408 |
by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1); |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
409 |
by (etac drop_prog_preserves_I 1); |
8041 | 410 |
by (etac drop_prog 1); |
411 |
by (assume_tac 1); |
|
412 |
qed "drop_prog_guarantees_raw"; |
|
413 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
414 |
Goal "[| F : X guarantees[v] Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
415 |
\ projecting C (lift_map i) F X' X; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
416 |
\ extending w C (lift_map i) F Y' Y; \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
417 |
\ preserves w <= preserves (v o sub i) |] \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
418 |
\ ==> lift_prog i F : X' guarantees[w] Y'"; |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
419 |
by (asm_simp_tac |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
420 |
(simpset() addsimps [lift_prog_correct, fold_o_sub, |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
421 |
lift_export project_guarantees]) 1); |
7186 | 422 |
qed "drop_prog_guarantees"; |
423 |
||
424 |
||
425 |
(** Are these two useful?? **) |
|
426 |
||
427 |
(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not |
|
428 |
ensure that F has the form lift_prog i F for some F.*) |
|
429 |
Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}"; |
|
430 |
by Auto_tac; |
|
431 |
by (stac Collect_eq_lift_set 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
432 |
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1); |
7186 | 433 |
qed "image_lift_prog_Stable"; |
434 |
||
435 |
Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)"; |
|
436 |
by (simp_tac (simpset() addsimps [Increasing_def, |
|
437 |
inj_lift_prog RS image_INT]) 1); |
|
438 |
by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1); |
|
439 |
qed "image_lift_prog_Increasing"; |
|
440 |
||
441 |
||
442 |
(*** guarantees corollaries ***) |
|
443 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
444 |
Goal "F : UNIV guarantees[v] increasing func \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
445 |
\ ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)"; |
7688 | 446 |
by (dtac (lift_export extend_guar_increasing) 1); |
447 |
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
|
7186 | 448 |
qed "lift_prog_guar_increasing"; |
449 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
450 |
Goal "F : UNIV guarantees[v] Increasing func \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
451 |
\ ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)"; |
7688 | 452 |
by (dtac (lift_export extend_guar_Increasing) 1); |
453 |
by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
|
7186 | 454 |
qed "lift_prog_guar_Increasing"; |
455 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
456 |
Goal "F : Always A guarantees[v] Always B \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
457 |
\ ==> lift_prog i F : \ |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
458 |
\ Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)"; |
7688 | 459 |
by (asm_simp_tac |
460 |
(simpset() addsimps [lift_set_correct, lift_prog_correct, |
|
461 |
lift_export extend_guar_Always]) 1); |
|
462 |
qed "lift_prog_guar_Always"; |