author | wenzelm |
Sun, 26 Nov 2017 21:08:32 +0100 | |
changeset 67091 | 1393c2340eec |
parent 63813 | 076129f60a31 |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_fp_n2m_tactics.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
Tactics for mutualization of nested (co)datatypes. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
signature BNF_FP_N2M_TACTICS = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
63045 | 10 |
val mk_rel_xtor_co_induct_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
11 |
thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic |
63045 | 12 |
val mk_xtor_un_fold_unique_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
13 |
thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> |
63045 | 14 |
{context: Proof.context, prems: thm list} -> tactic |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
15 |
val mk_xtor_un_fold_tac: Proof.context -> int -> thm list -> thm list -> tactic |
63045 | 16 |
val mk_xtor_un_fold_transfer_tac: Proof.context -> int -> thm list -> thm list -> thm list -> |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
17 |
thm list -> thm list -> thm list -> thm list -> tactic |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
19 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
20 |
structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
open BNF_Util |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
24 |
open BNF_Tactics |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
27 |
val vimage2p_unfolds = o_apply :: @{thms vimage2p_def}; |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
28 |
|
63813 | 29 |
fun unfold_at_most_once_tac ctxt thms = |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
30 |
CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt); |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
31 |
val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac; |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
32 |
|
63045 | 33 |
fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0 |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
34 |
nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
let |
58375
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
36 |
val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0; |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
37 |
val nesting_rel_monos = map (fn thm => rotate_prems ~1 (thm RS @{thm predicate2D})) |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
38 |
(@{thms prod.rel_mono sum.rel_mono} @ nesting_rel_monos0); |
7b92932ffea5
careful with op = in n2m (actually by Dmitriy Traytel)
blanchet
parents:
58237
diff
changeset
|
39 |
val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
40 |
val unfolds = map (fn def => |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
41 |
unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
val C_IHs = map2 (curry op |>) folded_C_IHs unfolds; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
val C_IH_monos = |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58375
diff
changeset
|
45 |
@{map 3} (fn C_IH => fn mono => fn unfold => |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
46 |
(mono RSN (2, @{thm vimage2p_mono}), C_IH) |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
|> fp = Greatest_FP ? swap |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
48 |
|> op RS |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
|> unfold) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
50 |
folded_C_IHs rel_monos unfolds; |
62778 | 51 |
|
52 |
val sym_nested_rel_eqs = map mk_sym nesting_rel_eqs; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
in |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55575
diff
changeset
|
54 |
unfold_thms_tac ctxt vimage2p_unfolds THEN |
60728 | 55 |
HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI}) |
56 |
(fn thm => rtac ctxt thm THEN_ALL_NEW (rotate_tac ~1 THEN' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
57 |
REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos, |
60728 | 58 |
SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl}, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
59 |
assume_tac ctxt, resolve_tac ctxt co_inducts, |
62778 | 60 |
resolve_tac ctxt C_IH_monos THEN_ALL_NEW (TRY o FIRST' |
61 |
[SELECT_GOAL (unfold_thms_tac ctxt sym_nested_rel_eqs) THEN' assume_tac ctxt, |
|
62 |
rtac ctxt @{thm order_refl}, |
|
63 |
REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])]))) |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
co_inducts) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
65 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
66 |
|
63045 | 67 |
fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps |
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
68 |
Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} = |
63045 | 69 |
unfold_thms_tac ctxt xtor_un_fold_defs THEN |
70 |
HEADGOAL (REPEAT_DETERM o FIRST' [hyp_subst_tac_thin true ctxt, rtac ctxt refl, |
|
71 |
rtac ctxt conjI, |
|
67091 | 72 |
rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \<circ>", OF refl]}, |
73 |
rtac ctxt @{thm arg_cong2[of _ _ _ _ "op \<circ>", OF _ refl]}, |
|
63045 | 74 |
resolve_tac ctxt map_arg_congs, |
75 |
resolve_tac ctxt fp_un_fold_uniques THEN_ALL_NEW case_fp fp (K all_tac) (rtac ctxt sym), |
|
76 |
SELECT_GOAL (CHANGED (unfold_thms_tac ctxt (flat [simp_thms, map_thms, map_defs, |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
77 |
xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))), |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
78 |
unfold_once_tac ctxt cache_defs]); |
63045 | 79 |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
80 |
fun mk_xtor_un_fold_tac ctxt n simps cache_defs = |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
81 |
REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt simps) ORELSE |
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
82 |
CHANGED (ALLGOALS (unfold_at_most_once_tac ctxt cache_defs))) THEN |
63045 | 83 |
CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) (1 upto n); |
84 |
||
85 |
fun mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
86 |
map_transfers Abs_transfers fp_or_nesting_rel_eqs cache_defs = |
63045 | 87 |
let |
88 |
val unfold = SELECT_GOAL (unfold_thms_tac ctxt fp_or_nesting_rel_eqs); |
|
89 |
in |
|
90 |
unfold_thms_tac ctxt (xtor_un_fold_defs @ rel_defs) THEN |
|
91 |
HEADGOAL (CONJ_WRAP' |
|
92 |
(fn thm => EVERY' [REPEAT_DETERM_N n o rtac ctxt rel_funI, rtac ctxt thm THEN_ALL_NEW |
|
93 |
REPEAT_DETERM o (FIRST' [assume_tac ctxt, rtac ctxt @{thm id_transfer}, |
|
94 |
rtac ctxt @{thm rel_funD[OF rel_funD[OF comp_transfer]]}, |
|
95 |
resolve_tac ctxt fp_un_fold_transfers, resolve_tac ctxt map_transfers, |
|
63046
8053ef5a0174
intermediate definitions and caching in n2m to keep terms small
traytel
parents:
63045
diff
changeset
|
96 |
unfold_once_tac ctxt cache_defs, |
63045 | 97 |
resolve_tac ctxt Abs_transfers, rtac ctxt @{thm vimage2p_rel_fun}, |
98 |
unfold THEN' rtac ctxt @{thm vimage2p_rel_fun}])]) |
|
99 |
fp_un_fold_transfers) |
|
100 |
end; |
|
101 |
||
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
102 |
end; |