(* Title: HOL/Tools/function_package/inductive_wrap.ML
ID: $Id$
Author: Alexander Krauss, TU Muenchen
A wrapper around the inductive package, restoring the quantifiers in
the introduction and elimination rules.
*)
signature FUNDEF_INDUCTIVE_WRAP =
sig
val inductive_def : term list
-> ((bstring * typ) * mixfix) * local_theory
-> thm list * (term * thm * thm * local_theory)
end
structure FundefInductiveWrap =
struct
open FundefLib
fun requantify ctxt lfix orig_def thm =
let
val (qs, t) = dest_all_all orig_def
val thy = theory_of_thm thm
val frees = frees_in_term ctxt t
|> remove (op =) lfix
val vars = Term.add_vars (prop_of thm) [] |> rev
val varmap = frees ~~ vars
in
fold_rev (fn Free (n, T) =>
forall_intr_rename (n, cterm_of thy (Var (the_default (("",0), T) (AList.lookup (op =) varmap (n, T))))))
qs
thm
end
fun inductive_def defs (((R, T), mixfix), lthy) =
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
InductivePackage.add_inductive_i (! Toplevel.debug) (*verbose*)
"" (* no altname *)
false (* no coind *)
false (* elims, please *)
false (* induction thm please *)
[(R, SOME T, NoSyn)] (* the relation *)
[] (* no parameters *)
(map (fn t => (("", []), t)) defs) (* the intros *)
[] (* no special monos *)
lthy
val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
val elim = elim_gen
|> forall_intr_vars (* FIXME... *)
in
(intrs, (Rdef, elim, induct, lthy))
end
end