src/HOL/Tools/function_package/inductive_wrap.ML

internal inductive: fresh theorem group;

(*  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
            {verbose = ! Toplevel.debug,
              kind = Thm.internalK,
              group = serial_string (),   (* FIXME pass proper group (!?) *)
              alt_name = "",
              coind = false,
              no_elim = false,
              no_ind = false}
            [((R, 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