57 val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic |
57 val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic |
58 val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> |
58 val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> |
59 thm list list -> thm list list list -> tactic |
59 thm list list -> thm list list list -> tactic |
60 val mk_map_id_tac: thm list -> thm -> thm -> tactic |
60 val mk_map_id_tac: thm list -> thm -> thm -> tactic |
61 val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic |
61 val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic |
62 val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
62 val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
63 val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
63 val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
64 val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list -> |
64 val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list -> |
65 thm list -> {prems: 'a, context: Proof.context} -> tactic |
65 thm list -> {prems: 'a, context: Proof.context} -> tactic |
66 val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic |
66 val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic |
67 val mk_mor_UNIV_tac: thm list -> thm -> tactic |
67 val mk_mor_UNIV_tac: thm list -> thm -> tactic |
1253 CONJ_WRAP' (fn k => |
1253 CONJ_WRAP' (fn k => |
1254 EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, |
1254 EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, |
1255 rtac conjI, rtac refl, rtac refl]) ks]) 1 |
1255 rtac conjI, rtac refl, rtac refl]) ks]) 1 |
1256 end |
1256 end |
1257 |
1257 |
1258 fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} = |
1258 fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} = |
1259 rtac unfold_unique 1 THEN |
1259 rtac unfold_unique 1 THEN |
1260 unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN |
1260 unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN |
1261 ALLGOALS (etac sym); |
1261 ALLGOALS (etac sym); |
1262 |
1262 |
1263 fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss |
1263 fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss |