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