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