src/HOL/Tools/BNF/bnf_fp_util_tactics.ML
changeset 62905 52c5a25e0c96
child 63045 c50c764aab10
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -0,0 +1,79 @@
     1.4 +(*  Title:      HOL/Tools/BNF/bnf_fp_util_tactics.ML
     1.5 +    Author:     Dmitriy Traytel, ETH Z├╝rich
     1.6 +    Copyright   2016
     1.7 +
     1.8 +Common tactics for datatype and codatatype constructions.
     1.9 +*)
    1.10 +
    1.11 +signature BNF_FP_UTIL_TACTICS =
    1.12 +sig
    1.13 +
    1.14 +val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic
    1.15 +val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic
    1.16 +val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm ->
    1.17 +  thm list -> thm list -> tactic
    1.18 +val mk_xtor_co_rec_transfer_tac: Proof.context -> BNF_Util.fp_kind -> int -> int -> thm list ->
    1.19 +  thm list -> thm list -> thm list -> tactic
    1.20 +
    1.21 +end
    1.22 +
    1.23 +structure BNF_FP_Util_Tactics =
    1.24 +struct
    1.25 +
    1.26 +open BNF_Tactics
    1.27 +open BNF_Util
    1.28 +
    1.29 +fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps =
    1.30 +  unfold_thms_tac ctxt (map mk_sym xtor_un_fold_xtors) THEN
    1.31 +  HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext,
    1.32 +    SELECT_GOAL (unfold_thms_tac ctxt
    1.33 +      (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)),
    1.34 +    rtac ctxt refl]);
    1.35 +
    1.36 +fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms =
    1.37 +  unfold_thms_tac ctxt (un_fold ::
    1.38 +    @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN
    1.39 +    HEADGOAL (rtac ctxt refl);
    1.40 +
    1.41 +fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps =
    1.42 +  unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN
    1.43 +  HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN
    1.44 +  unfold_thms_tac ctxt (map_ids @ map_comps @ case_fp fp
    1.45 +    @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]}
    1.46 +    @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN
    1.47 +  ALLGOALS (etac ctxt (case_fp fp
    1.48 +    @{thm arg_cong2[of _ _ _ _ BNF_Def.convol, OF refl]}
    1.49 +    @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]}));
    1.50 +
    1.51 +fun mk_xtor_co_rec_transfer_tac ctxt fp n m defs un_fold_transfers pre_T_map_transfers xtor_rels =
    1.52 +  case_fp fp
    1.53 +    (CONJ_WRAP (fn (def, un_fold_transfer) =>
    1.54 +        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
    1.55 +        unfold_thms_tac ctxt [def, o_apply] THEN
    1.56 +        HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN'
    1.57 +          etac ctxt (mk_rel_funDN_rotated (n + 1) un_fold_transfer) THEN'
    1.58 +          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
    1.59 +            etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
    1.60 +            rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
    1.61 +            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
    1.62 +            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
    1.63 +            REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN'
    1.64 +            rtac ctxt rel_funI THEN'
    1.65 +            etac ctxt (xtor_rel RS iffD2)) pre_T_map_transfers xtor_rels)))
    1.66 +      (defs ~~ un_fold_transfers))
    1.67 +    (CONJ_WRAP (fn (def, un_fold_transfer) =>
    1.68 +        REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN
    1.69 +        unfold_thms_tac ctxt [def, o_apply] THEN
    1.70 +        HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) un_fold_transfer) THEN'
    1.71 +          EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel =>
    1.72 +            etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
    1.73 +            rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
    1.74 +            rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
    1.75 +            REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN'
    1.76 +            REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN'
    1.77 +            rtac ctxt rel_funI THEN'
    1.78 +            etac ctxt (xtor_rel RS iffD1)) pre_T_map_transfers xtor_rels) THEN'
    1.79 +          etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer})))
    1.80 +      (defs ~~ un_fold_transfers));
    1.81 +
    1.82 +end
    1.83 \ No newline at end of file