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