src/HOL/Tools/function_package/inductive_wrap.ML

added code gen II

(*  Title:      HOL/Tools/function_package/inductive_wrap.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen


This is a wrapper around the inductive package which corrects some of its
slightly annoying behaviours and makes the whole business more controllable.

Specifically:

- Following newer Isar conventions, declaration and definition are done in one step

- The specification is expected in fully quantified form. This allows the client to 
  control the variable order. The variables will appear in the result in the same order.
  This is especially relevant for the elimination rule, where the order usually *does* matter.


All this will probably become obsolete in the near future, when the new "predicate" package
is in place.

*)

signature FUNDEF_INDUCTIVE_WRAP =
sig
  val inductive_def :  term list 
                       -> ((bstring * typ) * mixfix) * local_theory
                       -> thm list * (term * thm * local_theory)
end

structure FundefInductiveWrap =
struct

open FundefLib

fun requantify ctxt lfix (qs, t) thm =
    let
      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 qdefs = map dest_all_all defs
                  
      val (lthy, {intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], ...}) =
          InductivePackage.add_inductive_i true (*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 thy = ProofContext.theory_of lthy
                
      fun inst qdef intr_gen =
          intr_gen
            |> Thm.freezeT
            |> requantify lthy (R, T) qdef 
          
      val intrs = map2 inst qdefs intrs_gen
                  
      val elim = elim_gen
                   |> Thm.freezeT
                   |> forall_intr_vars (* FIXME... *)

      val Rdef_real = prop_of (Thm.freezeT elim_gen)
                       |> Logic.dest_implies |> fst
                       |> Term.strip_comb |> snd |> hd (* Trueprop *)
                       |> Term.strip_comb |> fst
    in
      (intrs, (Rdef_real, elim, lthy))
    end
    
end