1(* Title: HOL/Tools/BNF/bnf_fp_util_tactics.ML 2 Author: Dmitriy Traytel, ETH Z��rich 3 Copyright 2016 4 5Common tactics for datatype and codatatype constructions. 6*) 7 8signature BNF_FP_UTIL_TACTICS = 9sig 10 11val mk_xtor_un_fold_xtor_tac: Proof.context -> thm -> thm list -> thm list -> tactic 12val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic 13val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic 14val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm -> 15 thm list -> thm list -> tactic 16val mk_xtor_co_rec_transfer_tac: Proof.context -> BNF_Util.fp_kind -> int -> int -> thm list -> 17 thm list -> thm list -> thm list -> tactic 18 19end 20 21structure BNF_FP_Util_Tactics = 22struct 23 24open BNF_Tactics 25open BNF_Util 26 27fun mk_xtor_un_fold_xtor_tac ctxt xtor_un_fold_unique map_id0s inverses = 28 HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW rtac ctxt ext) THEN 29 unfold_thms_tac ctxt (@{thms o_apply id_o o_id} @ map_id0s @ inverses) THEN 30 ALLGOALS (rtac ctxt refl); 31 32fun mk_conj_arg_congN 1 = @{thm DEADID.rel_mono_strong} 33 | mk_conj_arg_congN n = mk_conj_arg_congN (n - 1) RSN (2, @{thm arg_cong2[of _ _ _ _ "(\<and>)"]}); 34 35fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps = 36 HEADGOAL (rtac ctxt (mk_conj_arg_congN (length xtor_un_fold_xtors) RS iffD1 OF 37 (map (fn thm => @{thm DEADID.rel_cong} OF [refl, thm]) xtor_un_fold_xtors)) THEN' 38 rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext, 39 SELECT_GOAL (unfold_thms_tac ctxt 40 (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)), 41 rtac ctxt refl]); 42 43fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms = 44 unfold_thms_tac ctxt (un_fold :: 45 @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN 46 HEADGOAL (rtac ctxt refl); 47 48fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps 49 inverses = 50 unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN 51 HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN 52 unfold_thms_tac ctxt (map_ids @ map_comps @ inverses @ case_fp fp 53 @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]} 54 @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN 55 ALLGOALS (etac ctxt (case_fp fp 56 @{thm arg_cong2[of _ _ _ _ BNF_Def.convol, OF refl]} 57 @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]})); 58 59fun mk_xtor_co_rec_transfer_tac ctxt fp n m defs un_fold_transfers pre_T_map_transfers xtor_rels = 60 case_fp fp 61 (CONJ_WRAP (fn (def, un_fold_transfer) => 62 REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 63 unfold_thms_tac ctxt [def, o_apply] THEN 64 HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN' 65 etac ctxt (mk_rel_funDN_rotated (n + 1) un_fold_transfer) THEN' 66 EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel => 67 etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN' 68 rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN' 69 rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' 70 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' 71 REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN' 72 rtac ctxt rel_funI THEN' 73 etac ctxt (xtor_rel RS iffD2)) pre_T_map_transfers xtor_rels))) 74 (defs ~~ un_fold_transfers)) 75 (CONJ_WRAP (fn (def, un_fold_transfer) => 76 REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN 77 unfold_thms_tac ctxt [def, o_apply] THEN 78 HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) un_fold_transfer) THEN' 79 EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel => 80 etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN' 81 rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN' 82 rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' 83 REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' 84 REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN' 85 rtac ctxt rel_funI THEN' 86 etac ctxt (xtor_rel RS iffD1)) pre_T_map_transfers xtor_rels) THEN' 87 etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer}))) 88 (defs ~~ un_fold_transfers)); 89 90end 91