src/HOL/Nominal/nominal_inductive.ML
author berghofe
Tue Feb 13 18:18:45 2007 +0100 (2007-02-13)
changeset 22313 1a507b463f50
child 22530 c192c5d1a6f2
permissions -rw-r--r--
First steps towards strengthening of induction rules for
inductively defined predicates involving nominal datatypes.
berghofe@22313
     1
(*  Title:      HOL/Nominal/nominal_inductive.ML
berghofe@22313
     2
    ID:         $Id$
berghofe@22313
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@22313
     4
berghofe@22313
     5
Infrastructure for proving additional properties of inductive predicates
berghofe@22313
     6
involving nominal datatypes
berghofe@22313
     7
*)
berghofe@22313
     8
berghofe@22313
     9
signature NOMINAL_INDUCTIVE =
berghofe@22313
    10
sig
berghofe@22313
    11
  val nominal_inductive: string -> theory -> theory
berghofe@22313
    12
end
berghofe@22313
    13
berghofe@22313
    14
structure NominalInductive : NOMINAL_INDUCTIVE =
berghofe@22313
    15
struct
berghofe@22313
    16
berghofe@22313
    17
val perm_boolI = thm "perm_boolI";
berghofe@22313
    18
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
berghofe@22313
    19
  (Drule.strip_imp_concl (cprop_of perm_boolI))));
berghofe@22313
    20
berghofe@22313
    21
fun transp ([] :: _) = []
berghofe@22313
    22
  | transp xs = map hd xs :: transp (map tl xs);
berghofe@22313
    23
berghofe@22313
    24
fun nominal_inductive s thy =
berghofe@22313
    25
  let
berghofe@22313
    26
    val ctxt = ProofContext.init thy;
berghofe@22313
    27
    val ({names, ...}, {raw_induct, intrs, ...}) =
berghofe@22313
    28
      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
berghofe@22313
    29
    val atoms = NominalAtoms.atoms_of thy;
berghofe@22313
    30
    val eqvt_ss = HOL_basic_ss addsimps NominalThmDecls.get_eqvt_thms thy;
berghofe@22313
    31
    val t = Logic.unvarify (concl_of raw_induct);
berghofe@22313
    32
    val pi = Name.variant (add_term_names (t, [])) "pi";
berghofe@22313
    33
    val ps = map (fst o HOLogic.dest_imp)
berghofe@22313
    34
      (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
berghofe@22313
    35
    fun eqvt_tac th intr = SUBPROOF (fn {prems, ...} =>
berghofe@22313
    36
      let val prems' = map (fn th' => th' RS th) prems
berghofe@22313
    37
      in (rtac intr THEN_ALL_NEW
berghofe@22313
    38
        (resolve_tac prems ORELSE'
berghofe@22313
    39
          (cut_facts_tac prems' THEN' full_simp_tac eqvt_ss))) 1
berghofe@22313
    40
      end) ctxt;
berghofe@22313
    41
    val thss = map (fn atom =>
berghofe@22313
    42
      let
berghofe@22313
    43
        val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])));
berghofe@22313
    44
        val perm_boolI' = Drule.cterm_instantiate
berghofe@22313
    45
          [(perm_boolI_pi, cterm_of thy pi')] perm_boolI
berghofe@22313
    46
      in map (fn th => standard (th RS mp))
berghofe@22313
    47
        (DatatypeAux.split_conj_thm (Goal.prove_global thy [] []
berghofe@22313
    48
          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
berghofe@22313
    49
            HOLogic.mk_imp (p, list_comb
berghofe@22313
    50
             (apsnd (map (NominalPackage.mk_perm [] pi')) (strip_comb p)))) ps)))
berghofe@22313
    51
          (fn _ => EVERY (rtac raw_induct 1 :: map (fn (intr, i) =>
berghofe@22313
    52
              full_simp_tac eqvt_ss i THEN TRY (eqvt_tac perm_boolI' intr i))
berghofe@22313
    53
            (rev intrs ~~ (length intrs downto 1))))))
berghofe@22313
    54
      end) atoms;
berghofe@22313
    55
    val (_, thy') = PureThy.add_thmss (map (fn (name, ths) =>
berghofe@22313
    56
        ((Sign.base_name name ^ "_eqvt", ths), [NominalThmDecls.eqvt_add]))
berghofe@22313
    57
      (names ~~ transp thss)) thy;
berghofe@22313
    58
  in thy' end;
berghofe@22313
    59
berghofe@22313
    60
berghofe@22313
    61
(* outer syntax *)
berghofe@22313
    62
berghofe@22313
    63
local structure P = OuterParse and K = OuterKeyword in
berghofe@22313
    64
berghofe@22313
    65
val nominal_inductiveP =
berghofe@22313
    66
  OuterSyntax.command "nominal_inductive"
berghofe@22313
    67
    "prove additional properties of inductive predicate involving nominal datatypes" K.thy_decl
berghofe@22313
    68
    (P.name >> (Toplevel.theory o nominal_inductive));
berghofe@22313
    69
berghofe@22313
    70
val _ = OuterSyntax.add_parsers [nominal_inductiveP];
berghofe@22313
    71
berghofe@22313
    72
end;
berghofe@22313
    73
berghofe@22313
    74
end