src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
changeset 55058 4e700eb471d4
parent 55057 6b0fcbeebaba
child 55059 ef2e0fb783c6
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_tactics.ML	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,41 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_n2m_tactics.ML
     1.5 -    Author:     Dmitriy Traytel, TU Muenchen
     1.6 -    Copyright   2013
     1.7 -
     1.8 -Tactics for mutualization of nested (co)datatypes.
     1.9 -*)
    1.10 -
    1.11 -signature BNF_FP_N2M_TACTICS =
    1.12 -sig
    1.13 -  val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list ->
    1.14 -    {prems: thm list, context: Proof.context} -> tactic
    1.15 -end;
    1.16 -
    1.17 -structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS =
    1.18 -struct
    1.19 -
    1.20 -open BNF_Util
    1.21 -open BNF_FP_Util
    1.22 -
    1.23 -fun mk_rel_xtor_co_induct_tactic fp co_inducts rel_defs rel_monos
    1.24 -  {context = ctxt, prems = raw_C_IHs} =
    1.25 -  let
    1.26 -    val unfolds = map (fn def => unfold_thms ctxt (id_apply :: no_reflexive [def])) rel_defs;
    1.27 -    val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
    1.28 -    val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
    1.29 -    val C_IH_monos =
    1.30 -      map3 (fn C_IH => fn mono => fn unfold =>
    1.31 -        (mono RSN (2, @{thm rev_predicate2D}), C_IH)
    1.32 -        |> fp = Greatest_FP ? swap
    1.33 -        |> op RS
    1.34 -        |> unfold)
    1.35 -      folded_C_IHs rel_monos unfolds;
    1.36 -  in
    1.37 -    HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI})
    1.38 -      (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
    1.39 -         REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
    1.40 -           rtac @{thm order_refl}, atac, resolve_tac co_inducts])))
    1.41 -    co_inducts)
    1.42 -  end;
    1.43 -
    1.44 -end;