# HG changeset patch
# User krauss
# Date 1256862726 -3600
# Node ID bb65583ab70d34aa09f66b034472f3722e21abf4
# Parent  6748bd742d7a49f829aead71cd7d3b77b2368bc4
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned

diff -r 6748bd742d7a -r bb65583ab70d src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Thu Oct 29 23:58:15 2009 +0100
+++ b/src/HOL/FunDef.thy	Fri Oct 30 01:32:06 2009 +0100
@@ -11,7 +11,6 @@
   "Tools/sat_solver.ML"
   ("Tools/Function/function_lib.ML")
   ("Tools/Function/function_common.ML")
-  ("Tools/Function/inductive_wrap.ML")
   ("Tools/Function/context_tree.ML")
   ("Tools/Function/function_core.ML")
   ("Tools/Function/sum_tree.ML")
@@ -106,7 +105,6 @@
 
 use "Tools/Function/function_lib.ML"
 use "Tools/Function/function_common.ML"
-use "Tools/Function/inductive_wrap.ML"
 use "Tools/Function/context_tree.ML"
 use "Tools/Function/function_core.ML"
 use "Tools/Function/sum_tree.ML"
diff -r 6748bd742d7a -r bb65583ab70d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 29 23:58:15 2009 +0100
+++ b/src/HOL/IsaMakefile	Fri Oct 30 01:32:06 2009 +0100
@@ -180,7 +180,6 @@
   Tools/Function/function.ML \
   Tools/Function/fun.ML \
   Tools/Function/induction_scheme.ML \
-  Tools/Function/inductive_wrap.ML \
   Tools/Function/lexicographic_order.ML \
   Tools/Function/measure_functions.ML \
   Tools/Function/mutual.ML \
diff -r 6748bd742d7a -r bb65583ab70d src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Thu Oct 29 23:58:15 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -451,20 +451,58 @@
       (goalstate, values)
     end
 
+(* wrapper -- restores quantifiers in rule specifications *)
+fun inductive_def (binding as ((R, T), _)) intrs lthy =
+  let
+    val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
+      lthy
+      |> LocalTheory.conceal
+      |> Inductive.add_inductive_i
+          {quiet_mode = false,
+            verbose = ! Toplevel.debug,
+            kind = Thm.internalK,
+            alt_name = Binding.empty,
+            coind = false,
+            no_elim = false,
+            no_ind = false,
+            skip_mono = true,
+            fork_mono = false}
+          [binding] (* relation *)
+          [] (* no parameters *)
+          (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
+          [] (* no special monos *)
+      ||> LocalTheory.restore_naming lthy
+
+    val cert = cterm_of (ProofContext.theory_of lthy)
+    fun requantify orig_intro thm =
+      let
+        val (qs, t) = dest_all_all orig_intro
+        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
+        val vars = Term.add_vars (prop_of thm) [] |> rev
+        val varmap = AList.lookup (op =) (frees ~~ map fst vars)
+          #> the_default ("",0)
+      in
+        fold_rev (fn Free (n, T) =>
+          forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
+      end
+  in
+      ((map2 requantify intrs intrs_gen, Rdef, forall_intr_vars elim_gen, induct), lthy)
+  end
+
 
 fun define_graph Gname fvar domT ranT clauses RCss lthy =
     let
       val GT = domT --> ranT --> boolT
-      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
+      val (Gvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Gname, GT)])
 
       fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
           let
             fun mk_h_assm (rcfix, rcassm, rcarg) =
-                HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
+                HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
                           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                           |> fold_rev (Logic.all o Free) rcfix
           in
-            HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
+            HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
                       |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
                       |> fold_rev (curry Logic.mk_implies) gs
                       |> fold_rev Logic.all (fvar :: qs)
@@ -472,8 +510,8 @@
 
       val G_intros = map2 mk_GIntro clauses RCss
 
-      val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
-          Function_Inductive_Wrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
+      val ((GIntro_thms, G, G_elim, G_induct), lthy) =
+        inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
     in
       ((G, GIntro_thms, G_elim, G_induct), lthy)
     end
@@ -500,10 +538,10 @@
     let
 
       val RT = domT --> domT --> boolT
-      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
+      val (Rvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Rname, RT)])
 
       fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-          HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
+          HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
                     |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                     |> fold_rev (curry Logic.mk_implies) gs
                     |> fold_rev (Logic.all o Free) rcfix
@@ -512,10 +550,10 @@
 
       val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-      val (RIntro_thmss, (R, R_elim, _, lthy)) =
-          fold_burrow Function_Inductive_Wrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
+      val ((RIntro_thms, R, R_elim, _), lthy) =
+        inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
     in
-      ((R, RIntro_thmss, R_elim), lthy)
+      ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
     end
 
 
diff -r 6748bd742d7a -r bb65583ab70d src/HOL/Tools/Function/inductive_wrap.ML
--- a/src/HOL/Tools/Function/inductive_wrap.ML	Thu Oct 29 23:58:15 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      HOL/Tools/Function/inductive_wrap.ML
-    Author:     Alexander Krauss, TU Muenchen
-
-
-A wrapper around the inductive package, restoring the quantifiers in
-the introduction and elimination rules.
-*)
-
-signature FUNCTION_INDUCTIVE_WRAP =
-sig
-  val inductive_def :  term list 
-                       -> ((bstring * typ) * mixfix) * local_theory
-                       -> thm list * (term * thm * thm * local_theory)
-end
-
-structure Function_Inductive_Wrap: FUNCTION_INDUCTIVE_WRAP =
-struct
-
-open Function_Lib
-
-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) =
-        lthy
-        |> LocalTheory.conceal
-        |> Inductive.add_inductive_i
-            {quiet_mode = false,
-              verbose = ! Toplevel.debug,
-              kind = Thm.internalK,
-              alt_name = Binding.empty,
-              coind = false,
-              no_elim = false,
-              no_ind = false,
-              skip_mono = true,
-              fork_mono = false}
-            [((Binding.name R, T), NoSyn)] (* the relation *)
-            [] (* no parameters *)
-            (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
-            [] (* no special monos *)
-        ||> LocalTheory.restore_naming 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