9 |
9 |
10 (**** PPROD ****) |
10 (**** PPROD ****) |
11 |
11 |
12 (*** Basic properties ***) |
12 (*** Basic properties ***) |
13 |
13 |
|
14 (** lift_set and drop_set **) |
|
15 |
14 Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
16 Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
15 by Auto_tac; |
17 by Auto_tac; |
16 qed "lift_set_iff"; |
18 qed "lift_set_iff"; |
17 AddIffs [lift_set_iff]; |
19 AddIffs [lift_set_iff]; |
18 |
20 |
19 Goalw [lift_set_def] "lift_set i (A Int B) = lift_set i A Int lift_set i B"; |
21 Goalw [lift_set_def] "lift_set i (A Int B) = lift_set i A Int lift_set i B"; |
20 by Auto_tac; |
22 by Auto_tac; |
21 qed "lift_set_Int"; |
23 qed "lift_set_Int"; |
22 |
24 |
|
25 (*USED?? converse fails*) |
|
26 Goalw [drop_set_def] "f : A ==> f i : drop_set i A"; |
|
27 by Auto_tac; |
|
28 qed "drop_set_I"; |
|
29 |
|
30 (** lift_act and drop_act **) |
|
31 |
23 Goalw [lift_act_def] "lift_act i Id = Id"; |
32 Goalw [lift_act_def] "lift_act i Id = Id"; |
24 by Auto_tac; |
33 by Auto_tac; |
25 qed "lift_act_Id"; |
34 qed "lift_act_Id"; |
26 Addsimps [lift_act_Id]; |
35 Addsimps [lift_act_Id]; |
|
36 |
|
37 Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act"; |
|
38 by (auto_tac (claset() addSIs [image_eqI], simpset())); |
|
39 qed "drop_act_I"; |
|
40 |
|
41 Goalw [drop_act_def] "drop_act i Id = Id"; |
|
42 by Auto_tac; |
|
43 by (res_inst_tac [("x", "((%u. x), (%u. x))")] image_eqI 1); |
|
44 by Auto_tac; |
|
45 qed "drop_act_Id"; |
|
46 Addsimps [drop_act_Id]; |
|
47 |
|
48 (** lift_prog and drop_prog **) |
27 |
49 |
28 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
50 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
29 by Auto_tac; |
51 by Auto_tac; |
30 qed "Init_lift_prog"; |
52 qed "Init_lift_prog"; |
31 Addsimps [Init_lift_prog]; |
53 Addsimps [Init_lift_prog]; |
32 |
54 |
33 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
55 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
34 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
56 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
35 qed "Acts_lift_prog"; |
57 qed "Acts_lift_prog"; |
|
58 Addsimps [Acts_lift_prog]; |
|
59 |
|
60 Goalw [drop_prog_def] "Init (drop_prog i F) = drop_set i (Init F)"; |
|
61 by Auto_tac; |
|
62 qed "Init_drop_prog"; |
|
63 Addsimps [Init_drop_prog]; |
|
64 |
|
65 Goalw [drop_prog_def] "Acts (drop_prog i F) = drop_act i `` Acts F"; |
|
66 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
|
67 qed "Acts_drop_prog"; |
|
68 Addsimps [Acts_drop_prog]; |
|
69 |
|
70 Goal "F component G ==> lift_prog i F component lift_prog i G"; |
|
71 by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
|
72 by Auto_tac; |
|
73 qed "lift_prog_mono"; |
|
74 |
|
75 Goal "F component G ==> drop_prog i F component drop_prog i G"; |
|
76 by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1); |
|
77 by Auto_tac; |
|
78 qed "drop_prog_mono"; |
|
79 |
|
80 Goal "lift_prog i SKIP = SKIP"; |
|
81 by (auto_tac (claset() addSIs [program_equalityI], |
|
82 simpset() addsimps [SKIP_def, lift_prog_def])); |
|
83 qed "lift_prog_SKIP"; |
|
84 |
|
85 Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)"; |
|
86 by (rtac program_equalityI 1); |
|
87 by (auto_tac (claset(), simpset() addsimps [Acts_Join])); |
|
88 qed "lift_prog_Join"; |
|
89 |
|
90 Goal "lift_prog i (JOIN I F) = (JN j:I. lift_prog i (F j))"; |
|
91 by (rtac program_equalityI 1); |
|
92 by (auto_tac (claset(), simpset() addsimps [Acts_JN])); |
|
93 qed "lift_prog_JN"; |
|
94 |
|
95 Goal "drop_prog i SKIP = SKIP"; |
|
96 by (auto_tac (claset() addSIs [program_equalityI], |
|
97 simpset() addsimps [SKIP_def, drop_set_def, drop_prog_def])); |
|
98 qed "drop_prog_SKIP"; |
36 |
99 |
37 |
100 |
38 (** Injectivity of lift_set, lift_act, lift_prog **) |
101 (** Injectivity of lift_set, lift_act, lift_prog **) |
39 |
102 |
40 Goalw [inj_on_def] "inj (lift_set i)"; |
103 Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F"; |
41 by (simp_tac (simpset() addsimps [lift_set_def]) 1); |
104 by Auto_tac; |
42 by (fast_tac (claset() addEs [equalityE]) 1); |
105 qed "lift_set_inverse"; |
|
106 Addsimps [lift_set_inverse]; |
|
107 |
|
108 Goal "inj (lift_set i)"; |
|
109 by (rtac inj_on_inverseI 1); |
|
110 by (rtac lift_set_inverse 1); |
43 qed "inj_lift_set"; |
111 qed "inj_lift_set"; |
44 |
112 |
45 Goalw [lift_act_def] "lift_act i x <= lift_act i y ==> x <= y"; |
113 Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act"; |
46 by Auto_tac; |
114 by Auto_tac; |
47 by (dres_inst_tac [("c", "((%s. a), (%s. a)(i:=b))")] subsetD 1); |
115 by (REPEAT_FIRST (resolve_tac [exI, conjI])); |
48 by Auto_tac; |
116 by Auto_tac; |
49 by (dres_inst_tac [("x", "i")] fun_cong 1); |
117 qed "lift_act_inverse"; |
50 by Auto_tac; |
118 Addsimps [lift_act_inverse]; |
51 val lemma = result(); |
119 |
52 |
120 Goal "inj (lift_act i)"; |
53 Goalw [inj_on_def] "inj (lift_act i)"; |
121 by (rtac inj_on_inverseI 1); |
54 by (blast_tac (claset() addEs [equalityE] |
122 by (rtac lift_act_inverse 1); |
55 addDs [lemma]) 1); |
|
56 qed "inj_lift_act"; |
123 qed "inj_lift_act"; |
57 |
124 |
58 Goal "insert Id (lift_act i `` Acts F) = (lift_act i `` Acts F)"; |
125 Goal "drop_prog i (lift_prog i F) = F"; |
59 by (rtac (image_eqI RS insert_absorb) 1); |
126 by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1); |
60 by (rtac Id_in_Acts 2); |
127 by (rtac program_equalityI 1); |
61 by (rtac (lift_act_Id RS sym) 1); |
128 by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2); |
62 qed "insert_Id_lift_act_eq"; |
129 by (Simp_tac 1); |
63 |
130 qed "lift_prog_inverse"; |
64 Goalw [inj_on_def] "inj (lift_prog i)"; |
131 Addsimps [lift_prog_inverse]; |
65 by (simp_tac (simpset() addsimps [lift_prog_def]) 1); |
132 |
66 by Auto_tac; |
133 Goal "inj (lift_prog i)"; |
67 by (etac program_equalityE 1); |
134 by (rtac inj_on_inverseI 1); |
68 by (full_simp_tac |
135 by (rtac lift_prog_inverse 1); |
69 (simpset() addsimps [insert_Id_lift_act_eq, inj_lift_set RS inj_eq, |
|
70 inj_lift_act RS inj_image_eq_iff]) 1); |
|
71 by (blast_tac (claset() addSIs [program_equalityI]) 1); |
|
72 qed "inj_lift_prog"; |
136 qed "inj_lift_prog"; |
73 |
|
74 |
137 |
75 |
138 |
76 (** PPROD **) |
139 (** PPROD **) |
77 |
140 |
78 Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))"; |
141 Goalw [PPROD_def] "Init (PPROD I F) = (INT i:I. lift_set i (Init (F i)))"; |
86 qed "lift_act_eq"; |
149 qed "lift_act_eq"; |
87 AddIffs [lift_act_eq]; |
150 AddIffs [lift_act_eq]; |
88 |
151 |
89 Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
152 Goal "Acts (PPROD I F) = insert Id (UN i:I. lift_act i `` Acts (F i))"; |
90 by (auto_tac (claset(), |
153 by (auto_tac (claset(), |
91 simpset() addsimps [PPROD_def, Acts_lift_prog, Acts_JN])); |
154 simpset() addsimps [PPROD_def, Acts_JN])); |
92 qed "Acts_PPROD"; |
155 qed "Acts_PPROD"; |
93 |
156 |
94 Goal "PPROD {} F = SKIP"; |
157 Goal "PPROD {} F = SKIP"; |
95 by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
158 by (simp_tac (simpset() addsimps [PPROD_def]) 1); |
96 qed "PPROD_empty"; |
159 qed "PPROD_empty"; |
97 |
160 |
98 Goal "(PPI i: I. SKIP) = SKIP"; |
161 Goal "(PPI i: I. SKIP) = SKIP"; |
99 by (auto_tac (claset() addSIs [program_equalityI], |
162 by (simp_tac (simpset() addsimps [PPROD_def,lift_prog_SKIP,JN_constant]) 1); |
100 simpset() addsimps [Acts_lift_prog, SKIP_def, Acts_PPROD])); |
|
101 qed "PPROD_SKIP"; |
163 qed "PPROD_SKIP"; |
102 |
164 |
103 Addsimps [PPROD_SKIP, PPROD_empty]; |
165 Addsimps [PPROD_SKIP, PPROD_empty]; |
104 |
166 |
105 Goalw [PPROD_def] |
167 Goalw [PPROD_def] |
113 qed "component_PPROD"; |
175 qed "component_PPROD"; |
114 |
176 |
115 |
177 |
116 (*** Safety: co, stable, invariant ***) |
178 (*** Safety: co, stable, invariant ***) |
117 |
179 |
118 (** 1st formulation of lifting **) |
180 (** Safety and lift_prog **) |
119 |
181 |
120 Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \ |
182 Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \ |
121 \ (F : A co B)"; |
183 \ (F : A co B)"; |
122 by (auto_tac (claset(), |
184 by (auto_tac (claset(), |
123 simpset() addsimps [constrains_def, Acts_lift_prog])); |
185 simpset() addsimps [constrains_def])); |
124 by (Blast_tac 2); |
186 by (Blast_tac 2); |
125 by (Force_tac 1); |
187 by (Force_tac 1); |
126 qed "lift_prog_constrains_eq"; |
188 qed "lift_prog_constrains_eq"; |
127 |
189 |
128 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
190 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
129 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1); |
191 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains_eq]) 1); |
130 qed "lift_prog_stable_eq"; |
192 qed "lift_prog_stable_eq"; |
131 |
193 |
132 (*This one looks strange! Proof probably is by case analysis on i=j.*) |
194 (*This one looks strange! Proof probably is by case analysis on i=j. |
|
195 If i~=j then lift_prog j (F j) does nothing to lift_set i, and the |
|
196 premise ensures A<=B.*) |
133 Goal "F i : A co B \ |
197 Goal "F i : A co B \ |
134 \ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)"; |
198 \ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)"; |
135 by (auto_tac (claset(), |
199 by (auto_tac (claset(), |
136 simpset() addsimps [constrains_def, Acts_lift_prog])); |
200 simpset() addsimps [constrains_def])); |
137 by (REPEAT (Blast_tac 1)); |
201 by (REPEAT (Blast_tac 1)); |
138 qed "constrains_imp_lift_prog_constrains"; |
202 qed "constrains_imp_lift_prog_constrains"; |
|
203 |
|
204 (** safety properties for program unit j hold trivially of unit i **) |
|
205 Goalw [constrains_def] |
|
206 "[| i~=j; A<= B|] ==> lift_prog i F : (lift_set j A) co (lift_set j B)"; |
|
207 by Auto_tac; |
|
208 qed "neq_imp_lift_prog_constrains"; |
|
209 |
|
210 Goalw [stable_def] |
|
211 "i~=j ==> lift_prog i F : stable (lift_set j A)"; |
|
212 by (blast_tac (claset() addIs [neq_imp_lift_prog_constrains]) 1); |
|
213 qed "neq_imp_lift_prog_stable"; |
|
214 |
|
215 bind_thm ("neq_imp_lift_prog_Constrains", |
|
216 neq_imp_lift_prog_constrains RS constrains_imp_Constrains); |
|
217 |
|
218 bind_thm ("neq_imp_lift_prog_Stable", |
|
219 neq_imp_lift_prog_stable RS stable_imp_Stable); |
|
220 |
|
221 |
|
222 (** Safety and PPROD **) |
139 |
223 |
140 Goal "i : I ==> \ |
224 Goal "i : I ==> \ |
141 \ (PPROD I F : (lift_set i A) co (lift_set i B)) = \ |
225 \ (PPROD I F : (lift_set i A) co (lift_set i B)) = \ |
142 \ (F i : A co B)"; |
226 \ (F i : A co B)"; |
143 by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
227 by (asm_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
148 Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)"; |
232 Goal "i : I ==> (PPROD I F : stable (lift_set i A)) = (F i : stable A)"; |
149 by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
233 by (asm_simp_tac (simpset() addsimps [stable_def, PPROD_constrains]) 1); |
150 qed "PPROD_stable"; |
234 qed "PPROD_stable"; |
151 |
235 |
152 |
236 |
153 (** 2nd formulation of lifting **) |
237 (** Safety, lift_prog + drop_set **) |
154 |
238 |
155 Goal "[| lift_prog i F : AA co BB |] \ |
239 Goal "[| lift_prog i F : AA co BB |] \ |
156 \ ==> F : (Applyall AA i) co (Applyall BB i)"; |
240 \ ==> F : (drop_set i AA) co (drop_set i BB)"; |
157 by (auto_tac (claset(), |
241 by (auto_tac (claset(), |
158 simpset() addsimps [Applyall_def, constrains_def, |
242 simpset() addsimps [constrains_def, drop_set_def])); |
159 Acts_lift_prog])); |
|
160 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
243 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
161 simpset()) 1); |
244 simpset()) 1); |
162 qed "lift_prog_constrains_projection"; |
245 qed "lift_prog_constrains_projection"; |
163 |
246 |
164 Goal "[| PPROD I F : AA co BB; i: I |] \ |
247 Goal "[| PPROD I F : AA co BB; i: I |] \ |
165 \ ==> F i : (Applyall AA i) co (Applyall BB i)"; |
248 \ ==> F i : (drop_set i AA) co (drop_set i BB)"; |
166 by (rtac lift_prog_constrains_projection 1); |
249 by (rtac lift_prog_constrains_projection 1); |
167 (*rotate this assumption to be last*) |
250 (*rotate this assumption to be last*) |
168 by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); |
251 by (dres_inst_tac [("psi", "PPROD I F : ?C")] asm_rl 1); |
169 by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
252 by (asm_full_simp_tac (simpset() addsimps [PPROD_def, constrains_JN]) 1); |
170 qed "PPROD_constrains_projection"; |
253 qed "PPROD_constrains_projection"; |
215 (** for lift_prog **) |
298 (** for lift_prog **) |
216 |
299 |
217 Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)"; |
300 Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)"; |
218 by (etac reachable.induct 1); |
301 by (etac reachable.induct 1); |
219 by (force_tac (claset() addIs [reachable.Acts, ext], |
302 by (force_tac (claset() addIs [reachable.Acts, ext], |
220 simpset() addsimps [Acts_lift_prog]) 2); |
303 simpset()) 2); |
221 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
304 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
222 qed "reachable_lift_progI"; |
305 qed "reachable_lift_progI"; |
223 |
306 |
224 Goal "f : reachable (lift_prog i F) ==> f i : reachable F"; |
307 Goal "f : reachable (lift_prog i F) ==> f i : reachable F"; |
225 by (etac reachable.induct 1); |
308 by (etac reachable.induct 1); |
226 by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog])); |
309 by Auto_tac; |
227 by (ALLGOALS (blast_tac (claset() addIs reachable.intrs))); |
310 by (ALLGOALS (blast_tac (claset() addIs reachable.intrs))); |
228 qed "reachable_lift_progD"; |
311 qed "reachable_lift_progD"; |
229 |
312 |
230 Goal "reachable (lift_prog i F) = lift_set i (reachable F)"; |
313 Goal "reachable (lift_prog i F) = lift_set i (reachable F)"; |
231 auto(); |
314 by Auto_tac; |
232 be reachable_lift_progD 1; |
315 by (etac reachable_lift_progD 1); |
233 ren "f" 1; |
316 ren "f" 1; |
234 by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1); |
317 by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1); |
235 auto(); |
318 by Auto_tac; |
236 qed "reachable_lift_prog"; |
319 qed "reachable_lift_prog"; |
237 |
320 |
238 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
321 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
239 \ (F : A Co B)"; |
322 \ (F : A Co B)"; |
240 by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog, |
323 by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog, |
276 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
359 by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PPROD]) 1); |
277 (*induction over the 2nd "reachable" assumption*) |
360 (*induction over the 2nd "reachable" assumption*) |
278 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
361 by (eres_inst_tac [("xa","f")] reachable.induct 1); |
279 (*Init of PPROD F, action of F case*) |
362 (*Init of PPROD F, action of F case*) |
280 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
363 by (res_inst_tac [("act","lift_act i act")] reachable.Acts 1); |
281 by (force_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join]) 1); |
364 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
282 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
365 by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
283 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
366 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1); |
284 (*last case: an action of PPROD I F*) |
367 (*last case: an action of PPROD I F*) |
285 by (rtac reachable.Acts 1); |
368 by (rtac reachable.Acts 1); |
286 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
369 by (force_tac (claset(), simpset() addsimps [Acts_Join]) 1); |
314 by (auto_tac |
397 by (auto_tac |
315 (claset(), |
398 (claset(), |
316 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
399 simpset() addsimps [Constrains_def, Collect_conj_eq RS sym, |
317 reachable_PPROD_eq])); |
400 reachable_PPROD_eq])); |
318 by (auto_tac (claset(), |
401 by (auto_tac (claset(), |
319 simpset() addsimps [constrains_def, Acts_lift_prog, PPROD_def, |
402 simpset() addsimps [constrains_def, PPROD_def, Acts_JN])); |
320 Acts_JN])); |
|
321 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
403 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); |
322 qed "Constrains_imp_PPROD_Constrains"; |
404 qed "Constrains_imp_PPROD_Constrains"; |
323 |
405 |
324 Goal "[| ALL i:I. f0 i : R i; i: I |] \ |
406 Goal "[| ALL i:I. f0 i : R i; i: I |] \ |
325 \ ==> Applyall ({f. (ALL i:I. f i : R i)} Int lift_set i A) i = R i Int A"; |
407 \ ==> drop_set i ({f. (ALL i:I. f i : R i)} Int lift_set i A) = R i Int A"; |
326 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
408 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] image_eqI], |
327 simpset() addsimps [Applyall_def, lift_set_def]) 1); |
409 simpset() addsimps [drop_set_def, lift_set_def]) 1); |
328 qed "Applyall_Int_depend"; |
410 qed "drop_set_Int_depend"; |
329 |
411 |
330 (*Again, we need the f0 premise so that PPROD I F has an initial state; |
412 (*Again, we need the f0 premise so that PPROD I F has an initial state; |
331 otherwise its Co-property is vacuous.*) |
413 otherwise its Co-property is vacuous.*) |
332 Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B); \ |
414 Goal "[| PPROD I F : (lift_set i A) Co (lift_set i B); \ |
333 \ i: I; finite I; f0: Init (PPROD I F) |] \ |
415 \ i: I; finite I; f0: Init (PPROD I F) |] \ |
357 |
439 |
358 |
440 |
359 (** PFUN (no dependence on i) doesn't require the f0 premise **) |
441 (** PFUN (no dependence on i) doesn't require the f0 premise **) |
360 |
442 |
361 Goal "i: I \ |
443 Goal "i: I \ |
362 \ ==> Applyall ({f. (ALL i:I. f i : R)} Int lift_set i A) i = R Int A"; |
444 \ ==> drop_set i ({f. (ALL i:I. f i : R)} Int lift_set i A) = R Int A"; |
363 by (force_tac (claset(), simpset() addsimps [Applyall_def]) 1); |
445 by (force_tac (claset(), simpset() addsimps [drop_set_def]) 1); |
364 qed "Applyall_Int"; |
446 qed "drop_set_Int"; |
365 |
447 |
366 Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B); \ |
448 Goal "[| (PPI x:I. F) : (lift_set i A) Co (lift_set i B); \ |
367 \ i: I; finite I |] \ |
449 \ i: I; finite I |] \ |
368 \ ==> F : A Co B"; |
450 \ ==> F : A Co B"; |
369 by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); |
451 by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); |
370 by (dtac PPROD_constrains_projection 1); |
452 by (dtac PPROD_constrains_projection 1); |
371 by (assume_tac 1); |
453 by (assume_tac 1); |
372 by (asm_full_simp_tac |
454 by (asm_full_simp_tac |
373 (simpset() addsimps [Applyall_Int, Collect_conj_eq RS sym, |
455 (simpset() addsimps [drop_set_Int, Collect_conj_eq RS sym, |
374 reachable_PPROD_eq]) 1); |
456 reachable_PPROD_eq]) 1); |
375 qed "PFUN_Constrains_imp_Constrains"; |
457 qed "PFUN_Constrains_imp_Constrains"; |
376 |
458 |
377 Goal "[| i: I; finite I |] \ |
459 Goal "[| i: I; finite I |] \ |
378 \ ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) = \ |
460 \ ==> ((PPI x:I. F) : (lift_set i A) Co (lift_set i B)) = \ |
388 |
470 |
389 |
471 |
390 |
472 |
391 (*** guarantees properties ***) |
473 (*** guarantees properties ***) |
392 |
474 |
393 |
|
394 Goal "drop_act i (lift_act i act) = act"; |
475 Goal "drop_act i (lift_act i act) = act"; |
395 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
476 by (force_tac (claset() addSIs [rinst [("x", "?ff(i := ?u)")] exI], |
396 simpset() addsimps [drop_act_def, lift_act_def]) 1); |
477 simpset() addsimps [drop_act_def, lift_act_def]) 1); |
397 qed "lift_act_inverse"; |
478 qed "lift_act_inverse"; |
398 Addsimps [lift_act_inverse]; |
479 Addsimps [lift_act_inverse]; |
399 |
480 |
400 |
481 |
|
482 (*Because A and B could differ outside i, cannot generalize result to |
|
483 drop_set i (A Int B) = drop_set i A Int drop_set i B |
|
484 *) |
|
485 Goalw [lift_set_def, drop_set_def] |
|
486 "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; |
|
487 by Auto_tac; |
|
488 qed "drop_set_lift_set_Int"; |
|
489 |
|
490 Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)"; |
|
491 by (rtac program_equalityI 1); |
|
492 by (simp_tac (simpset() addsimps [Acts_Join, image_Un, |
|
493 image_compose RS sym, o_def]) 2); |
|
494 by (simp_tac (simpset() addsimps [drop_set_lift_set_Int]) 1); |
|
495 qed "drop_prog_lift_prog_Join"; |
|
496 |
401 Goal "(lift_prog i F) Join G = lift_prog i H \ |
497 Goal "(lift_prog i F) Join G = lift_prog i H \ |
402 \ ==> EX J. H = F Join J"; |
498 \ ==> H = F Join (drop_prog i G)"; |
403 by (etac program_equalityE 1); |
499 by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
404 by (auto_tac (claset(), simpset() addsimps [Acts_lift_prog, Acts_Join])); |
500 by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
405 by (res_inst_tac [("x", |
501 by (etac sym 1); |
406 "mk_program(Applyall(Init G) i, drop_act i `` Acts G)")] |
|
407 exI 1); |
|
408 by (rtac program_equalityI 1); |
|
409 (*Init*) |
|
410 by (simp_tac (simpset() addsimps [Applyall_def]) 1); |
|
411 (*Blast_tac can't do HO unification, needed to invent function states*) |
|
412 by (fast_tac (claset() addEs [equalityE]) 1); |
|
413 (*Now for the Actions*) |
|
414 by (dres_inst_tac [("f", "op `` (drop_act i)")] arg_cong 1); |
|
415 by (asm_full_simp_tac |
|
416 (simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1); |
|
417 qed "lift_prog_Join_eq_lift_prog_D"; |
502 qed "lift_prog_Join_eq_lift_prog_D"; |
418 |
|
419 |
503 |
420 Goal "F : X guar Y \ |
504 Goal "F : X guar Y \ |
421 \ ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)"; |
505 \ ==> lift_prog i F : (lift_prog i `` X) guar (lift_prog i `` Y)"; |
422 by (rtac guaranteesI 1); |
506 by (rtac guaranteesI 1); |
423 by Auto_tac; |
507 by Auto_tac; |
424 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
508 by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
425 qed "lift_prog_guarantees"; |
509 qed "lift_prog_guarantees"; |
426 |
510 |
427 |
511 Goalw [PPROD_def] |
|
512 "[| ALL i:I. F i : X guar Y |] \ |
|
513 \ ==> (PPROD I F) : (INT i: I. lift_prog i `` X) \ |
|
514 \ guar (INT i: I. lift_prog i `` Y)"; |
|
515 by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1); |
|
516 qed "guarantees_PPROD_INT"; |
|
517 |
|
518 Goalw [PPROD_def] |
|
519 "[| ALL i:I. F i : X guar Y |] \ |
|
520 \ ==> (PPROD I F) : (UN i: I. lift_prog i `` X) \ |
|
521 \ guar (UN i: I. lift_prog i `` Y)"; |
|
522 by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1); |
|
523 qed "guarantees_PPROD_UN"; |