src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -71,17 +71,6 @@
     (Ts' @ [T']) ---> HOLogic.boolT
   end;
 
-(* FIXME: create new predicate name -- does not avoid nameclashing *)
-fun pred_of f =
-  let
-    val (name, T) = dest_Const f
-  in
-    if (body_type T = @{typ bool}) then
-      (Free (Long_Name.base_name name ^ "P", T))
-    else
-      (Free (Long_Name.base_name name ^ "P", pred_type T))
-  end
-
 (* creates the list of premises for every intro rule *)
 (* theory -> term -> (string list, term list list) *)
 
@@ -274,6 +263,17 @@
     map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
   end;
 
+(* FIXME: create new predicate name -- does not avoid nameclashing *)
+fun pred_of thy f =
+  let
+    val (name, T) = dest_Const f
+    val base_name' = (Long_Name.base_name name ^ "P")
+    val name' = Sign.full_bname thy base_name'
+    val T' = if (body_type T = @{typ bool}) then T else pred_type T
+  in
+    (name', Const (name', T'))
+  end
+
 (* assumption: mutual recursive predicates all have the same parameters. *)
 fun define_predicates specs thy =
   if forall (fn (const, _) => defined_const thy const) specs then
@@ -284,14 +284,17 @@
       val eqns = maps snd specs
       (* create prednames *)
       val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
+      val dst_funs = distinct (op =) funs
       val argss' = map (map transform_ho_arg) argss
       fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1))
-     (* FIXME: higher order arguments also occur in tuples! *)
+      (* FIXME: higher order arguments also occur in tuples! *)
       val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss'))
-      val preds = map pred_of funs
+      val (prednames, preds) = split_list (map (pred_of thy) funs)
+      val dst_preds = distinct (op =) preds
+      val dst_prednames = distinct (op =) prednames
       (* mapping from term (Free or Const) to term *)
       val net = fold Item_Net.update
-        ((funs ~~ preds) @ lifted_args)
+        ((dst_funs ~~ dst_preds) @ lifted_args)
           (Fun_Pred.get thy)
       fun lookup_pred t = lookup thy net t
       (* create intro rules *)
@@ -308,51 +311,42 @@
           end
       fun mk_rewr_thm (func, pred) = @{thm refl}
       val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
-      val (ind_result, thy') =
-        thy
-        |> Sign.map_naming Name_Space.conceal
-        |> Inductive.add_inductive_global
-          {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
-            no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
-          (map (fn (s, T) =>
-            ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
-          (map (dest_Free o snd) lifted_args)
-          (map (fn x => (Attrib.empty_binding, x)) intr_ts)
-          []
-        ||> Sign.restore_naming thy
-      val prednames = map (fst o dest_Const) (#preds ind_result)
-      (* add constants to my table *)
-      val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
-        (#intrs ind_result))) prednames
+      val (intrs, thy') = thy
+        |> Sign.add_consts_i
+          (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
+           dst_preds)
+        |> fold_map Specification.axiom (map (pair (Binding.empty, [])) intr_ts)
+      val specs = map (fn predname => (predname,
+          map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
+        dst_prednames
       val thy'' = Fun_Pred.map
-        (fold Item_Net.update (map (apfst Logic.varify_global)
-          (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+        (fold Item_Net.update (map (pairself Logic.varify_global)
+          (dst_funs ~~ dst_preds))) thy'
       fun functional_mode_of T =
         list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
       val thy''' = fold
         (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
           predname (functional_mode_of T) name)
-      (prednames ~~ distinct (op =) funs) thy''
+      (dst_prednames ~~ dst_funs) thy''
     in
       (specs, thy''')
     end
 
 fun rewrite_intro thy intro =
   let
-    (*val _ = tracing ("Rewriting intro with registered mapping for: " ^
-      commas (Symtab.keys (Pred_Compile_Preproc.get thy)))*)
     fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
+    (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
     val intro_t = Logic.unvarify_global (prop_of intro)
     val (prems, concl) = Logic.strip_horn intro_t
     val frees = map fst (Term.add_frees intro_t [])
     fun rewrite prem names =
       let
         (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
-        val t = (HOLogic.dest_Trueprop prem)
+        val t = HOLogic.dest_Trueprop prem
         val (lit, mk_lit) = case try HOLogic.dest_not t of
             SOME t => (t, HOLogic.mk_not)
           | NONE => (t, I)
-        val (P, args) = (strip_comb lit)
+        val (P, args) = strip_comb lit
       in
         folds_map (flatten thy lookup_pred) args (names, [])
         |> map (fn (resargs, (names', prems')) =>
@@ -365,6 +359,8 @@
         rewrite concl frees'
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
+    (*val _ = tracing ("Rewritten intro to " ^
+      commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
   end