14 val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic |
14 val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic |
15 val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic |
15 val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic |
16 val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic |
16 val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic |
17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
19 val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic |
19 val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic |
20 val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
20 val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
21 |
21 |
22 val mk_kill_bd_card_order_tac: int -> thm -> tactic |
22 val mk_kill_bd_card_order_tac: int -> thm -> tactic |
23 val mk_kill_bd_cinfinite_tac: thm -> tactic |
23 val mk_kill_bd_cinfinite_tac: thm -> tactic |
24 val kill_in_alt_tac: tactic |
24 val kill_in_alt_tac: tactic |
65 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s = |
65 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s = |
66 EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, |
66 EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, |
67 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ |
67 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ |
68 map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; |
68 map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; |
69 |
69 |
70 fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps = |
70 fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = |
71 EVERY' ([rtac ext] @ |
71 EVERY' ([rtac ext] @ |
72 replicate 3 (rtac trans_o_apply) @ |
72 replicate 3 (rtac trans_o_apply) @ |
73 [rtac (arg_cong_Union RS trans), |
73 [rtac (arg_cong_Union RS trans), |
74 rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), |
74 rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), |
75 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), |
75 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), |
76 rtac Gmap_cong0] @ |
76 rtac Gmap_cong0] @ |
77 map (fn thm => rtac (thm RS fun_cong)) set_maps @ |
77 map (fn thm => rtac (thm RS fun_cong)) set_map0s @ |
78 [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, |
78 [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, |
79 rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, |
79 rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, |
80 rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), |
80 rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), |
81 rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
81 rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
82 rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
82 rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
83 rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
83 rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
84 [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, |
84 [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]}, |
85 rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
85 rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
86 rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, |
86 rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, |
87 rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
87 rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
88 rtac @{thm image_empty}]) 1; |
88 rtac @{thm image_empty}]) 1; |
89 |
89 |