252 |
252 |
253 Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"; |
253 Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"; |
254 by (Force_tac 1); |
254 by (Force_tac 1); |
255 qed "delete_map_neq_apply"; |
255 qed "delete_map_neq_apply"; |
256 |
256 |
257 (*A set of the form (A Times UNIV) ignores the second (dummy) state component*) |
257 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*) |
258 |
258 |
259 Goal "(f o fst) -`` A = (f-``A) Times UNIV"; |
259 Goal "(f o fst) -`` A = (f-``A) <*> UNIV"; |
260 by Auto_tac; |
260 by Auto_tac; |
261 qed "vimage_o_fst_eq"; |
261 qed "vimage_o_fst_eq"; |
262 |
262 |
263 Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)"; |
263 Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)"; |
264 by Auto_tac; |
264 by Auto_tac; |
265 qed "vimage_sub_eq_lift_set"; |
265 qed "vimage_sub_eq_lift_set"; |
266 |
266 |
267 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set]; |
267 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set]; |
268 |
268 |
269 Goal "[| F : preserves snd; i~=j |] \ |
269 Goal "[| F : preserves snd; i~=j |] \ |
270 \ ==> lift j F : stable (lift_set i (A Times UNIV))"; |
270 \ ==> lift j F : stable (lift_set i (A <*> UNIV))"; |
271 by (auto_tac (claset(), |
271 by (auto_tac (claset(), |
272 simpset() addsimps [lift_def, lift_set_def, |
272 simpset() addsimps [lift_def, lift_set_def, |
273 stable_def, constrains_def, |
273 stable_def, constrains_def, |
274 mem_rename_act_iff, mem_rename_set_iff])); |
274 mem_rename_act_iff, mem_rename_set_iff])); |
275 by (auto_tac (claset() addSDs [preserves_imp_eq], |
275 by (auto_tac (claset() addSDs [preserves_imp_eq], |
278 by Auto_tac; |
278 by Auto_tac; |
279 qed "preserves_snd_lift_stable"; |
279 qed "preserves_snd_lift_stable"; |
280 |
280 |
281 (*If i~=j then lift j F does nothing to lift_set i, and the |
281 (*If i~=j then lift j F does nothing to lift_set i, and the |
282 premise ensures A<=B.*) |
282 premise ensures A<=B.*) |
283 Goal "[| F i : (A Times UNIV) co (B Times UNIV); \ |
283 Goal "[| F i : (A <*> UNIV) co (B <*> UNIV); \ |
284 \ F j : preserves snd |] \ |
284 \ F j : preserves snd |] \ |
285 \ ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))"; |
285 \ ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"; |
286 by (case_tac "i=j" 1); |
286 by (case_tac "i=j" 1); |
287 by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, |
287 by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, |
288 rename_constrains]) 1); |
288 rename_constrains]) 1); |
289 by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1); |
289 by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1); |
290 by (assume_tac 1); |
290 by (assume_tac 1); |
321 by Auto_tac; |
321 by Auto_tac; |
322 by (blast_tac (claset() addDs [insert_map_eq_diff]) 1); |
322 by (blast_tac (claset() addDs [insert_map_eq_diff]) 1); |
323 qed "lift_map_eq_diff"; |
323 qed "lift_map_eq_diff"; |
324 |
324 |
325 Goal "F : preserves snd \ |
325 Goal "F : preserves snd \ |
326 \ ==> (lift i F : transient (lift_set j (A Times UNIV))) = \ |
326 \ ==> (lift i F : transient (lift_set j (A <*> UNIV))) = \ |
327 \ (i=j & F : transient (A Times UNIV) | A={})"; |
327 \ (i=j & F : transient (A <*> UNIV) | A={})"; |
328 by (case_tac "i=j" 1); |
328 by (case_tac "i=j" 1); |
329 by (auto_tac (claset(), simpset() addsimps [lift_transient])); |
329 by (auto_tac (claset(), simpset() addsimps [lift_transient])); |
330 by (auto_tac (claset(), |
330 by (auto_tac (claset(), |
331 simpset() addsimps [lift_def, transient_def, |
331 simpset() addsimps [lift_def, transient_def, |
332 Domain_rename_act])); |
332 Domain_rename_act])); |
347 by (dtac ComplD 1); |
347 by (dtac ComplD 1); |
348 by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1); |
348 by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1); |
349 qed "lift_transient_eq_disj"; |
349 qed "lift_transient_eq_disj"; |
350 |
350 |
351 (*USELESS??*) |
351 (*USELESS??*) |
352 Goal "lift_map i `` (A Times UNIV) = \ |
352 Goal "lift_map i `` (A <*> UNIV) = \ |
353 \ (UN s:A. UN f. {insert_map i s f}) Times UNIV"; |
353 \ (UN s:A. UN f. {insert_map i s f}) <*> UNIV"; |
354 by (auto_tac (claset() addSIs [bexI, image_eqI], |
354 by (auto_tac (claset() addSIs [bexI, image_eqI], |
355 simpset() addsimps [lift_map_def])); |
355 simpset() addsimps [lift_map_def])); |
356 by (rtac (split RS sym) 1); |
356 by (rtac (split RS sym) 1); |
357 qed "lift_map_image_Times"; |
357 qed "lift_map_image_Times"; |
358 |
358 |