equal
deleted
inserted
replaced
1 (* Title: HOL/BNF/Tools/bnf_fp_n2m_tactics.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Copyright 2013 |
|
4 |
|
5 Tactics for mutualization of nested (co)datatypes. |
|
6 *) |
|
7 |
|
8 signature BNF_FP_N2M_TACTICS = |
|
9 sig |
|
10 val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list -> |
|
11 {prems: thm list, context: Proof.context} -> tactic |
|
12 end; |
|
13 |
|
14 structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS = |
|
15 struct |
|
16 |
|
17 open BNF_Util |
|
18 open BNF_FP_Util |
|
19 |
|
20 fun mk_rel_xtor_co_induct_tactic fp co_inducts rel_defs rel_monos |
|
21 {context = ctxt, prems = raw_C_IHs} = |
|
22 let |
|
23 val unfolds = map (fn def => unfold_thms ctxt (id_apply :: no_reflexive [def])) rel_defs; |
|
24 val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs; |
|
25 val C_IHs = map2 (curry op |>) folded_C_IHs unfolds; |
|
26 val C_IH_monos = |
|
27 map3 (fn C_IH => fn mono => fn unfold => |
|
28 (mono RSN (2, @{thm rev_predicate2D}), C_IH) |
|
29 |> fp = Greatest_FP ? swap |
|
30 |> op RS |
|
31 |> unfold) |
|
32 folded_C_IHs rel_monos unfolds; |
|
33 in |
|
34 HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI}) |
|
35 (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN' |
|
36 REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos, |
|
37 rtac @{thm order_refl}, atac, resolve_tac co_inducts]))) |
|
38 co_inducts) |
|
39 end; |
|
40 |
|
41 end; |
|