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