9 signature BNF_COMP_TACTICS = |
9 signature BNF_COMP_TACTICS = |
10 sig |
10 sig |
11 val mk_comp_bd_card_order_tac: thm list -> thm -> tactic |
11 val mk_comp_bd_card_order_tac: thm list -> thm -> tactic |
12 val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic |
12 val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic |
13 val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic |
13 val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic |
14 val mk_comp_map_comp_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_map_tac: thm -> thm -> thm -> thm list -> tactic |
60 |
60 |
61 fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s = |
61 fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s = |
62 EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ |
62 EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ |
63 map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1; |
63 map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1; |
64 |
64 |
65 fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps = |
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_comp 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_comps) 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_comp Gmap_cong0 Gset_map set_maps = |
70 fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps = |
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_comp 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_maps @ |
78 [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, |
78 [rtac (Gset_map 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_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), |