|
62905
|
1 |
(* Title: HOL/Tools/BNF/bnf_fp_util_tactics.ML
|
|
|
2 |
Author: Dmitriy Traytel, ETH Zürich
|
|
|
3 |
Copyright 2016
|
|
|
4 |
|
|
|
5 |
Common tactics for datatype and codatatype constructions.
|
|
|
6 |
*)
|
|
|
7 |
|
|
|
8 |
signature BNF_FP_UTIL_TACTICS =
|
|
|
9 |
sig
|
|
|
10 |
|
|
63045
|
11 |
val mk_xtor_un_fold_xtor_tac: Proof.context -> thm -> thm list -> thm list -> tactic
|
|
62905
|
12 |
val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic
|
|
|
13 |
val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic
|
|
|
14 |
val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm ->
|
|
|
15 |
thm list -> thm list -> tactic
|
|
|
16 |
val 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 |
|
|
|
19 |
end
|
|
|
20 |
|
|
|
21 |
structure BNF_FP_Util_Tactics =
|
|
|
22 |
struct
|
|
|
23 |
|
|
|
24 |
open BNF_Tactics
|
|
|
25 |
open BNF_Util
|
|
|
26 |
|
|
63045
|
27 |
fun 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 |
|
|
|
32 |
fun 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 _ _ _ _ "op \<and>"]});
|
|
|
34 |
|
|
62905
|
35 |
fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps =
|
|
63045
|
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]);
|
|
62905
|
42 |
|
|
|
43 |
fun 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 |
|
|
63045
|
48 |
fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps
|
|
|
49 |
inverses =
|
|
62905
|
50 |
unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN
|
|
|
51 |
HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN
|
|
63045
|
52 |
unfold_thms_tac ctxt (map_ids @ map_comps @ inverses @ case_fp fp
|
|
62905
|
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 |
|
|
|
59 |
fun 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 |
|
|
|
90 |
end |