author | paulson |
Wed, 03 Mar 1999 10:50:42 +0100 | |
changeset 6299 | 1a88db6e7c7e |
parent 6295 | 351b3c2b0d83 |
child 6451 | bc943acc5fda |
permissions | -rw-r--r-- |
5899 | 1 |
(* Title: HOL/UNITY/PPROD.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
*) |
|
6 |
||
6020 | 7 |
|
8 |
val rinst = read_instantiate_sg (sign_of thy); |
|
9 |
||
5899 | 10 |
(**** PPROD ****) |
11 |
||
12 |
(*** Basic properties ***) |
|
13 |
||
6020 | 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 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6020
diff
changeset
|
19 |
Goalw [lift_act_def] "lift_act i Id = Id"; |
5899 | 20 |
by Auto_tac; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6020
diff
changeset
|
21 |
qed "lift_act_Id"; |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6020
diff
changeset
|
22 |
Addsimps [lift_act_Id]; |
5899 | 23 |
|
6299 | 24 |
(*NEEDED????????????????????????????????????????????????????????????????*) |
25 |
Goal "Id : lift_act i `` Acts F"; |
|
26 |
by (auto_tac (claset() addSIs [lift_act_Id RS sym], |
|
27 |
simpset() addsimps [image_iff])); |
|
28 |
qed "Id_mem_lift_act"; |
|
29 |
||
30 |
Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
|
5972 | 31 |
by Auto_tac; |
32 |
qed "Init_lift_prog"; |
|
33 |
Addsimps [Init_lift_prog]; |
|
34 |
||
35 |
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6020
diff
changeset
|
36 |
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
5972 | 37 |
qed "Acts_lift_prog"; |
38 |
||
6020 | 39 |
Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))"; |
5972 | 40 |
by Auto_tac; |
41 |
qed "Init_PPROD"; |
|
42 |
Addsimps [Init_PPROD]; |
|
43 |
||
5899 | 44 |
Goalw [lift_act_def] |
45 |
"((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
|
46 |
by (Blast_tac 1); |
|
47 |
qed "lift_act_eq"; |
|
48 |
AddIffs [lift_act_eq]; |
|
49 |
||
6299 | 50 |
Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
5899 | 51 |
by (auto_tac (claset(), |
5972 | 52 |
simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN])); |
5899 | 53 |
qed "Acts_PPROD"; |
54 |
||
55 |
Goal "PPROD {} F = SKIP"; |
|
56 |
by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
|
57 |
qed "PPROD_empty"; |
|
58 |
||
6299 | 59 |
Goal "(PPI i: I. SKIP) = SKIP"; |
60 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
61 |
simpset() addsimps [Acts_lift_prog, SKIP_def, Acts_PPROD])); |
|
62 |
qed "PPROD_SKIP"; |
|
63 |
||
5899 | 64 |
Addsimps [PPROD_SKIP, PPROD_empty]; |
65 |
||
5972 | 66 |
Goalw [PPROD_def] |
67 |
"PPROD (insert i I) F = (lift_prog i (F i)) Join (PPROD I F)"; |
|
5899 | 68 |
by Auto_tac; |
69 |
qed "PPROD_insert"; |
|
70 |
||
5972 | 71 |
Goalw [PPROD_def] "i : I ==> component (lift_prog i (F i)) (PPROD I F)"; |
72 |
(*blast_tac doesn't use HO unification*) |
|
73 |
by (fast_tac (claset() addIs [component_JN]) 1); |
|
74 |
qed "component_PPROD"; |
|
5899 | 75 |
|
5972 | 76 |
|
77 |
(*** Safety: constrains, stable, invariant ***) |
|
78 |
||
79 |
(** 1st formulation of lifting **) |
|
5899 | 80 |
|
6020 | 81 |
Goal "(lift_prog i F : constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 82 |
\ (F : constrains A B)"; |
83 |
by (auto_tac (claset(), |
|
84 |
simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
85 |
by (Blast_tac 2); |
|
86 |
by (Force_tac 1); |
|
87 |
qed "lift_prog_constrains_eq"; |
|
88 |
||
6020 | 89 |
Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
5972 | 90 |
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1); |
91 |
qed "lift_prog_stable_eq"; |
|
92 |
||
93 |
(*This one looks strange! Proof probably is by case analysis on i=j.*) |
|
94 |
Goal "F i : constrains A B \ |
|
6020 | 95 |
\ ==> lift_prog j (F j) : constrains (lift_set i A) (lift_set i B)"; |
5972 | 96 |
by (auto_tac (claset(), |
97 |
simpset() addsimps [constrains_def, Acts_lift_prog])); |
|
98 |
by (REPEAT (Blast_tac 1)); |
|
99 |
qed "constrains_imp_lift_prog_constrains"; |
|
5899 | 100 |
|
101 |
Goal "i : I ==> \ |
|
6020 | 102 |
\ (PPROD I F : constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 103 |
\ (F i : constrains A B)"; |
104 |
by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
|
105 |
by (blast_tac (claset() addIs [lift_prog_constrains_eq RS iffD1, |
|
106 |
constrains_imp_lift_prog_constrains]) 1); |
|
5899 | 107 |
qed "PPROD_constrains"; |
108 |
||
6020 | 109 |
Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)"; |
5972 | 110 |
by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
111 |
qed "PPROD_stable"; |
|
112 |
||
113 |
||
114 |
(** 2nd formulation of lifting **) |
|
115 |
||
116 |
Goal "[| lift_prog i F : constrains AA BB |] \ |
|
5899 | 117 |
\ ==> F : constrains (Applyall AA i) (Applyall BB i)"; |
118 |
by (auto_tac (claset(), |
|
119 |
simpset() addsimps [Applyall_def, constrains_def, |
|
5972 | 120 |
Acts_lift_prog])); |
121 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
|
5899 | 122 |
simpset()) 1); |
5972 | 123 |
qed "lift_prog_constrains_projection"; |
124 |
||
125 |
Goal "[| PPROD I F : constrains AA BB; i: I |] \ |
|
126 |
\ ==> F i : constrains (Applyall AA i) (Applyall BB i)"; |
|
127 |
by (rtac lift_prog_constrains_projection 1); |
|
128 |
(*rotate this assumption to be last*) |
|
129 |
by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); |
|
130 |
by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
|
5899 | 131 |
qed "PPROD_constrains_projection"; |
132 |
||
133 |
||
5972 | 134 |
(** invariant **) |
135 |
||
6299 | 136 |
(*????????????????*) |
6020 | 137 |
Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)"; |
5972 | 138 |
by (auto_tac (claset(), |
139 |
simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
140 |
qed "invariant_imp_lift_prog_invariant"; |
|
5899 | 141 |
|
6299 | 142 |
(*????????????????*) |
6020 | 143 |
Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A"; |
5972 | 144 |
by (auto_tac (claset(), |
145 |
simpset() addsimps [invariant_def, lift_prog_stable_eq])); |
|
146 |
qed "lift_prog_invariant_imp_invariant"; |
|
147 |
||
148 |
(*NOT clear that the previous lemmas help in proving this one.*) |
|
6299 | 149 |
Goal "[| F i : invariant A; i : I |] \ |
150 |
\ ==> PPROD I F : invariant (lift_set i A)"; |
|
5972 | 151 |
by (auto_tac (claset(), |
152 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
153 |
qed "invariant_imp_PPROD_invariant"; |
|
154 |
||
155 |
(*The f0 premise ensures that the product is well-defined.*) |
|
6020 | 156 |
Goal "[| PPROD I F : invariant (lift_set i A); i : I; \ |
5972 | 157 |
\ f0: Init (PPROD I F) |] ==> F i : invariant A"; |
5899 | 158 |
by (auto_tac (claset(), |
159 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
5972 | 160 |
by (dres_inst_tac [("c", "f0(i:=x)")] subsetD 1); |
161 |
by Auto_tac; |
|
162 |
qed "PPROD_invariant_imp_invariant"; |
|
163 |
||
164 |
Goal "[| i : I; f0: Init (PPROD I F) |] \ |
|
6020 | 165 |
\ ==> (PPROD I F : invariant (lift_set i A)) = (F i : invariant A)"; |
5972 | 166 |
by (blast_tac (claset() addIs [invariant_imp_PPROD_invariant, |
167 |
PPROD_invariant_imp_invariant]) 1); |
|
5899 | 168 |
qed "PPROD_invariant"; |
169 |
||
5972 | 170 |
(*The f0 premise isn't needed if F is a constant program because then |
171 |
we get an initial state by replicating that of F*) |
|
172 |
Goal "i : I \ |
|
6020 | 173 |
\ ==> ((PPI x:I. F) : invariant (lift_set i A)) = (F : invariant A)"; |
5972 | 174 |
by (auto_tac (claset(), |
175 |
simpset() addsimps [invariant_def, PPROD_stable])); |
|
176 |
qed "PFUN_invariant"; |
|
177 |
||
5899 | 178 |
|
5972 | 179 |
(*** Substitution Axiom versions: Constrains, Stable ***) |
5899 | 180 |
|
5972 | 181 |
(** Reachability **) |
182 |
||
183 |
Goal "[| f : reachable (PPROD I F); i : I |] ==> f i : reachable (F i)"; |
|
5899 | 184 |
by (etac reachable.induct 1); |
185 |
by (auto_tac |
|
186 |
(claset() addIs reachable.intrs, |
|
187 |
simpset() addsimps [Acts_PPROD])); |
|
188 |
qed "reachable_PPROD"; |
|
189 |
||
5972 | 190 |
Goal "reachable (PPROD I F) <= {f. ALL i:I. f i : reachable (F i)}"; |
5899 | 191 |
by (force_tac (claset() addSDs [reachable_PPROD], simpset()) 1); |
192 |
qed "reachable_PPROD_subset1"; |
|
193 |
||
5972 | 194 |
Goal "[| i ~: I; A : reachable (F i) |] \ |
195 |
\ ==> ALL f. f : reachable (PPROD I F) \ |
|
196 |
\ --> f(i:=A) : reachable (lift_prog i (F i) Join PPROD I F)"; |
|
5899 | 197 |
by (etac reachable.induct 1); |
198 |
by (ALLGOALS Clarify_tac); |
|
199 |
by (etac reachable.induct 1); |
|
200 |
(*Init, Init case*) |
|
201 |
by (force_tac (claset() addIs reachable.intrs, |
|
5972 | 202 |
simpset() addsimps [Acts_lift_prog]) 1); |
5899 | 203 |
(*Init of F, action of PPROD F case*) |
5972 | 204 |
by (rtac reachable.Acts 1); |
5899 | 205 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 206 |
by (assume_tac 1); |
5899 | 207 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
208 |
(*induction over the 2nd "reachable" assumption*) |
|
209 |
by (eres_inst_tac [("xa","f")] reachable.induct 1); |
|
210 |
(*Init of PPROD F, action of F case*) |
|
211 |
by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
|
5972 | 212 |
by (force_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]) 1); |
5899 | 213 |
by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
214 |
by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
|
215 |
(*last case: an action of PPROD I F*) |
|
5972 | 216 |
by (rtac reachable.Acts 1); |
5899 | 217 |
by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
5972 | 218 |
by (assume_tac 1); |
5899 | 219 |
by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
220 |
qed_spec_mp "reachable_lift_Join_PPROD"; |
|
221 |
||
222 |
||
223 |
(*The index set must be finite: otherwise infinitely many copies of F can |
|
224 |
perform actions, and PPROD can never catch up in finite time.*) |
|
5972 | 225 |
Goal "finite I \ |
226 |
\ ==> {f. ALL i:I. f i : reachable (F i)} <= reachable (PPROD I F)"; |
|
5899 | 227 |
by (etac finite_induct 1); |
228 |
by (Simp_tac 1); |
|
229 |
by (force_tac (claset() addDs [reachable_lift_Join_PPROD], |
|
230 |
simpset() addsimps [PPROD_insert]) 1); |
|
231 |
qed "reachable_PPROD_subset2"; |
|
232 |
||
5972 | 233 |
Goal "finite I ==> \ |
234 |
\ reachable (PPROD I F) = {f. ALL i:I. f i : reachable (F i)}"; |
|
5899 | 235 |
by (REPEAT_FIRST (ares_tac [equalityI, |
236 |
reachable_PPROD_subset1, |
|
237 |
reachable_PPROD_subset2])); |
|
238 |
qed "reachable_PPROD_eq"; |
|
239 |
||
240 |
||
5972 | 241 |
(** Constrains **) |
5899 | 242 |
|
5972 | 243 |
Goal "[| F i : Constrains A B; i: I; finite I |] \ |
6020 | 244 |
\ ==> PPROD I F : Constrains (lift_set i A) (lift_set i B)"; |
5899 | 245 |
by (auto_tac |
246 |
(claset(), |
|
247 |
simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
|
248 |
reachable_PPROD_eq])); |
|
249 |
by (auto_tac (claset(), |
|
5972 | 250 |
simpset() addsimps [constrains_def, Acts_lift_prog, PPROD_def, |
5899 | 251 |
Acts_JN])); |
252 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
|
5972 | 253 |
qed "Constrains_imp_PPROD_Constrains"; |
254 |
||
6299 | 255 |
Goal "[| ALL i:I. f0 i : R i; i: I |] \ |
256 |
\ ==> Applyall ({f. (ALL i:I. f i : R i)} Int lift_set i A) i = R i Int A"; |
|
257 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
|
258 |
simpset() addsimps [Applyall_def, lift_set_def]) 1); |
|
5972 | 259 |
qed "Applyall_Int_depend"; |
260 |
||
261 |
(*Again, we need the f0 premise because otherwise Constrains holds trivially |
|
262 |
for PPROD I F.*) |
|
6020 | 263 |
Goal "[| PPROD I F : Constrains (lift_set i A) (lift_set i B); \ |
5972 | 264 |
\ i: I; finite I; f0: Init (PPROD I F) |] \ |
265 |
\ ==> F i : Constrains A B"; |
|
266 |
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
267 |
by (subgoal_tac "ALL i:I. f0 i : reachable (F i)" 1); |
|
268 |
by (blast_tac (claset() addIs [reachable.Init]) 2); |
|
269 |
by (dtac PPROD_constrains_projection 1); |
|
270 |
by (assume_tac 1); |
|
271 |
by (asm_full_simp_tac |
|
6299 | 272 |
(simpset() addsimps [Applyall_Int_depend, reachable_PPROD_eq]) 1); |
5972 | 273 |
qed "PPROD_Constrains_imp_Constrains"; |
5899 | 274 |
|
275 |
||
5972 | 276 |
Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
6020 | 277 |
\ ==> (PPROD I F : Constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 278 |
\ (F i : Constrains A B)"; |
279 |
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
|
280 |
PPROD_Constrains_imp_Constrains]) 1); |
|
281 |
qed "PPROD_Constrains"; |
|
282 |
||
283 |
Goal "[| i: I; finite I; f0: Init (PPROD I F) |] \ |
|
6020 | 284 |
\ ==> (PPROD I F : Stable (lift_set i A)) = (F i : Stable A)"; |
5972 | 285 |
by (asm_simp_tac (simpset() delsimps [Init_PPROD] |
286 |
addsimps [Stable_def, PPROD_Constrains]) 1); |
|
5899 | 287 |
qed "PPROD_Stable"; |
288 |
||
289 |
||
5972 | 290 |
(** PFUN (no dependence on i) doesn't require the f0 premise **) |
5899 | 291 |
|
6299 | 292 |
Goal "i: I \ |
293 |
\ ==> Applyall ({f. (ALL i:I. f i : R)} Int lift_set i A) i = R Int A"; |
|
5972 | 294 |
by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1); |
295 |
qed "Applyall_Int"; |
|
296 |
||
6020 | 297 |
Goal "[| (PPI x:I. F) : Constrains (lift_set i A) (lift_set i B); \ |
5972 | 298 |
\ i: I; finite I |] \ |
299 |
\ ==> F : Constrains A B"; |
|
300 |
by (full_simp_tac (simpset() addsimps [Constrains_def]) 1); |
|
301 |
by (dtac PPROD_constrains_projection 1); |
|
302 |
by (assume_tac 1); |
|
303 |
by (asm_full_simp_tac |
|
304 |
(simpset() addsimps [Applyall_Int, Collect_conj_eq RS sym, |
|
305 |
reachable_PPROD_eq]) 1); |
|
306 |
qed "PFUN_Constrains_imp_Constrains"; |
|
307 |
||
308 |
Goal "[| i: I; finite I |] \ |
|
6020 | 309 |
\ ==> ((PPI x:I. F) : Constrains (lift_set i A) (lift_set i B)) = \ |
5972 | 310 |
\ (F : Constrains A B)"; |
311 |
by (blast_tac (claset() addIs [Constrains_imp_PPROD_Constrains, |
|
312 |
PFUN_Constrains_imp_Constrains]) 1); |
|
313 |
qed "PFUN_Constrains"; |
|
314 |
||
315 |
Goal "[| i: I; finite I |] \ |
|
6020 | 316 |
\ ==> ((PPI x:I. F) : Stable (lift_set i A)) = (F : Stable A)"; |
5972 | 317 |
by (asm_simp_tac (simpset() addsimps [Stable_def, PFUN_Constrains]) 1); |
318 |
qed "PFUN_Stable"; |
|
319 |
||
320 |
||
321 |
||
322 |
(*** guarantees properties ***) |
|
323 |
||
324 |
||
325 |
Goal "drop_act i (lift_act i act) = act"; |
|
326 |
by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
|
327 |
simpset() addsimps [drop_act_def, lift_act_def]) 1); |
|
328 |
qed "lift_act_inverse"; |
|
329 |
Addsimps [lift_act_inverse]; |
|
330 |
||
331 |
||
332 |
Goal "(lift_prog i F) Join G = lift_prog i H \ |
|
333 |
\ ==> EX J. H = F Join J"; |
|
334 |
by (etac program_equalityE 1); |
|
335 |
by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join])); |
|
336 |
by (res_inst_tac [("x", |
|
337 |
"mk_program(Applyall(Init G) i, drop_act i `` Acts G)")] |
|
338 |
exI 1); |
|
339 |
by (rtac program_equalityI 1); |
|
340 |
(*Init*) |
|
341 |
by (simp_tac (simpset() addsimps [Applyall_def]) 1); |
|
342 |
(*Blast_tac can't do HO unification, needed to invent function states*) |
|
343 |
by (fast_tac (claset() addEs [equalityE]) 1); |
|
344 |
(*Now for the Actions*) |
|
345 |
by (dres_inst_tac [("f", "op `` (drop_act i)")] arg_cong 1); |
|
346 |
by (asm_full_simp_tac |
|
347 |
(simpset() addsimps [insert_absorb, Acts_Join, |
|
348 |
image_Un, image_compose RS sym, o_def]) 1); |
|
349 |
qed "lift_prog_Join_eq_lift_prog_D"; |
|
350 |
||
351 |
||
352 |
Goal "F : X guarantees Y \ |
|
353 |
\ ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)"; |
|
354 |
by (rtac guaranteesI 1); |
|
355 |
by Auto_tac; |
|
356 |
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
357 |
qed "lift_prog_guarantees"; |
|
358 |
||
359 |