# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID ca77d8c34ce20a8c9b9faa5c7443bde76779df08
# Parent  bf18c8174571b6244f2e8236927c168d2ca5bbe3
cleaned up

diff -r bf18c8174571 -r ca77d8c34ce2 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -89,6 +89,13 @@
     []
   else [intro]
 
+
+fun print_intross thy msg intross =
+  tracing (msg ^ 
+    (space_implode "; " (map 
+      (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross)))
+
+  
 fun preprocess_strong_conn_constnames gr constnames thy =
   let
     val get_specs = map (fn k => (k, Graph.get_node gr k))
@@ -103,8 +110,7 @@
     val _ = priority "Compiling predicates to flat introrules..."
     val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
       (get_specs prednames) thy')
-    val _ = tracing ("Flattened introduction rules: " ^
-      commas (map (Display.string_of_thm_global thy'') (flat intross1)))
+    val _ = print_intross thy'' "Flattened introduction rules: " intross1
     val _ = priority "Replacing functions in introrules..."
       (*  val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross  *)
     val intross2 =
@@ -113,11 +119,12 @@
           SOME intross => intross
         | NONE => let val _ = warning "Function replacement failed!" in intross1 end
       else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
-    val _ = tracing ("Introduction rules with replaced functions: " ^
-      commas (map (Display.string_of_thm_global thy'') (flat intross2)))
-    val intross3 = burrow (maps remove_pointless_clauses) intross2
+    val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2
+    val intross3 = map (maps remove_pointless_clauses) intross2
+    val _ = print_intross thy'' "After removing pointless clauses: " intross3
     val intross4 = burrow (map (AxClass.overload thy'')) intross3
     val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4
+    val _ = print_intross thy'' "introduction rules before registering: " intross5
     val _ = priority "Registering intro rules..."
     val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy''
   in
diff -r bf18c8174571 -r ca77d8c34ce2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -697,6 +697,9 @@
 fun register_intros pre_intros thy =
   let
     val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
+    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr))))
+    val _ = if not (forall (fn intr => constname_of_intro intr = c) pre_intros) then
+      error "register_intros: Introduction rules of different constants are used" else ()
     val _ = Output.tracing ("Registering introduction rules of " ^ c)
     val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
     val nparams = guess_nparams T
diff -r bf18c8174571 -r ca77d8c34ce2 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
@@ -1,5 +1,5 @@
 theory Predicate_Compile_ex
-imports Main Predicate_Compile
+imports Main Predicate_Compile_Alternative_Defs
 begin
 
 inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
@@ -122,7 +122,7 @@
   "map_ofP ((a, b)#xs) a b"
 | "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
 
-code_pred map_ofP .
+code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
 thm map_ofP.equation
 section {* reverse *}
 
@@ -371,10 +371,7 @@
 
 code_pred (inductify_all) avl .
 thm avl.equation
-(*
-lemma [code_pred_inline]: "bot_fun_inst.bot_fun == (\<lambda>(y::'a::type). False)"
-unfolding bot_fun_inst.bot_fun[symmetric] bot_bool_eq[symmetric] bot_fun_eq by simp
-*)
+
 fun set_of
 where
 "set_of ET = {}"
@@ -385,33 +382,10 @@
 "is_ord ET = True"
 | "is_ord (MKT n l r h) =
  ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-(*
-lemma empty_set[code_pred_def]: "{} = (\<lambda>x. False)" unfolding empty_def by simp
-thm set_of.simps[unfolded empty_set Un_def]
-*)
-(*
-declare empty_def[code_pred_def]
-*)
-ML {* prop_of (@{thm set_of.simps(1)}) *}
-thm Un_def
-thm eq_refl
-declare eq_reflection[OF empty_def, code_pred_inline]
-thm Un_def
-definition Un' where "Un' A B == A Un B"
 
-lemma [code_pred_intros]: "A x ==> Un' A B x"
-and  [code_pred_intros] : "B x ==> Un' A B x"
-sorry
-
-code_pred Un' sorry
-
-lemmas a = Un'_def[symmetric]
-declare a[code_pred_inline]
-declare set_of.simps
-ML {* prop_of @{thm Un_def} *}
-ML {* tap *}
 code_pred (inductify_all) set_of .
 thm set_of.equation
+text {* expected mode: [1], [1, 2] *}
 (* FIXME *)
 (*
 code_pred (inductify_all) is_ord .