1(*  Title:      HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
2    Author:     Dmitriy Traytel, TU Muenchen
3    Copyright   2013
4
5Tactics for mutualization of nested (co)datatypes.
6*)
7
8signature BNF_FP_N2M_TACTICS =
9sig
10  val mk_rel_xtor_co_induct_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
11    thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic
12  val mk_xtor_un_fold_unique_tac: BNF_Util.fp_kind -> thm list -> thm list -> thm list ->
13    thm list -> thm list -> thm list -> thm list -> thm list -> thm list ->
14    {context: Proof.context, prems: thm list} -> tactic
15  val mk_xtor_un_fold_tac: Proof.context -> int -> thm list -> thm list -> tactic
16  val mk_xtor_un_fold_transfer_tac: Proof.context -> int -> thm list -> thm list -> thm list ->
17    thm list -> thm list -> thm list -> thm list -> tactic
18end;
19
20structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
21struct
22
23open BNF_Util
24open BNF_Tactics
25open BNF_FP_Util
26
27val vimage2p_unfolds = o_apply :: @{thms vimage2p_def};
28
29fun unfold_at_most_once_tac ctxt thms =
30  CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt);
31val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac;
32
33fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0
34  nesting_rel_monos0 {context = ctxt, prems = raw_C_IHs} =
35  let
36    val nesting_rel_eqs = @{thms prod.rel_eq sum.rel_eq} @ nesting_rel_eqs0;
37    val nesting_rel_monos = map (fn thm => rotate_prems ~1 (thm RS @{thm predicate2D}))
38      (@{thms prod.rel_mono sum.rel_mono} @ nesting_rel_monos0);
39    val co_inducts = map (unfold_thms ctxt (vimage2p_unfolds @ nesting_rel_eqs)) co_inducts0;
40    val unfolds = map (fn def =>
41      unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
42    val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
43    val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
44    val C_IH_monos =
45      @{map 3} (fn C_IH => fn mono => fn unfold =>
46        (mono RSN (2, @{thm vimage2p_mono}), C_IH)
47        |> fp = Greatest_FP ? swap
48        |> op RS
49        |> unfold)
50      folded_C_IHs rel_monos unfolds;
51
52    val sym_nested_rel_eqs = map mk_sym nesting_rel_eqs;
53  in
54    unfold_thms_tac ctxt vimage2p_unfolds THEN
55    HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI})
56      (fn thm => rtac ctxt thm THEN_ALL_NEW (rotate_tac ~1 THEN'
57         REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos,
58           SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl},
59           assume_tac ctxt, resolve_tac ctxt co_inducts,
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)])])))
64    co_inducts)
65  end;
66
67fun mk_xtor_un_fold_unique_tac fp xtor_un_fold_defs map_arg_congs xtor_un_fold_o_maps
68   Rep_o_Abss fp_un_fold_uniques simp_thms map_thms map_defs cache_defs {context = ctxt, prems} =
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,
72    rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<circ>)", OF refl]},
73    rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\<circ>)", OF _ refl]},
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,
77      xtor_un_fold_defs, xtor_un_fold_o_maps, Rep_o_Abss, prems]))),
78    unfold_once_tac ctxt cache_defs]);
79
80fun mk_xtor_un_fold_tac ctxt n simps cache_defs =
81  REPEAT_DETERM (CHANGED (unfold_thms_tac ctxt simps) ORELSE
82    CHANGED (ALLGOALS (unfold_at_most_once_tac ctxt cache_defs))) THEN
83  CONJ_WRAP (K (HEADGOAL (rtac ctxt refl))) (1 upto n);
84
85fun mk_xtor_un_fold_transfer_tac ctxt n xtor_un_fold_defs rel_defs fp_un_fold_transfers
86    map_transfers Abs_transfers fp_or_nesting_rel_eqs cache_defs =
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,
96            unfold_once_tac ctxt cache_defs,
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
102end;
103