merged
authorbulwahn
Thu, 19 Nov 2009 10:49:43 +0100
changeset 33757 bc75dbbbf3e6
parent 33756 47b7c9e0bf6e (diff)
parent 33751 7ead0ccf6cbd (current diff)
child 33758 53078b0d21f5
child 33761 15f9bd93a1dd
merged
--- a/src/HOL/HOL.thy	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/HOL.thy	Thu Nov 19 10:49:43 2009 +0100
@@ -2060,7 +2060,6 @@
 setup {*
   Predicate_Compile_Alternative_Defs.setup
   #> Predicate_Compile_Inline_Defs.setup
-  #> Predicate_Compile_Preproc_Const_Defs.setup
 *}
 
 
--- a/src/HOL/Predicate.thy	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Predicate.thy	Thu Nov 19 10:49:43 2009 +0100
@@ -570,6 +570,9 @@
 definition if_pred :: "bool \<Rightarrow> unit pred" where
   if_pred_eq: "if_pred b = (if b then single () else \<bottom>)"
 
+definition holds :: "unit pred \<Rightarrow> bool" where
+  holds_eq: "holds P = eval P ()"
+
 definition not_pred :: "unit pred \<Rightarrow> unit pred" where
   not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())"
 
@@ -592,7 +595,54 @@
 lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   unfolding not_pred_eq
   by (auto split: split_if_asm elim: botE)
+lemma "f () = False \<or> f () = True"
+by simp
 
+lemma closure_of_bool_cases:
+assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
+assumes "f = (%u. True) \<Longrightarrow> P f"
+shows "P f"
+proof -
+  have "f = (%u. False) \<or> f = (%u. True)"
+    apply (cases "f ()")
+    apply (rule disjI2)
+    apply (rule ext)
+    apply (simp add: unit_eq)
+    apply (rule disjI1)
+    apply (rule ext)
+    apply (simp add: unit_eq)
+    done
+  from this prems show ?thesis by blast
+qed
+
+lemma unit_pred_cases:
+assumes "P \<bottom>"
+assumes "P (single ())"
+shows "P Q"
+using assms
+unfolding bot_pred_def Collect_def empty_def single_def
+apply (cases Q)
+apply simp
+apply (rule_tac f="fun" in closure_of_bool_cases)
+apply auto
+apply (subgoal_tac "(%x. () = x) = (%x. True)") 
+apply auto
+done
+
+lemma holds_if_pred:
+  "holds (if_pred b) = b"
+unfolding if_pred_eq holds_eq
+by (cases b) (auto intro: singleI elim: botE)
+
+lemma if_pred_holds:
+  "if_pred (holds P) = P"
+unfolding if_pred_eq holds_eq
+by (rule unit_pred_cases) (auto intro: singleI elim: botE)
+
+lemma is_empty_holds:
+  "is_empty P \<longleftrightarrow> \<not> holds P"
+unfolding is_empty_def holds_eq
+by (rule unit_pred_cases) (auto elim: botE intro: singleI)
 
 subsubsection {* Implementation *}
 
@@ -838,7 +888,7 @@
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
+hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
 
 end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -111,10 +111,10 @@
   in
     Options {
       expected_modes = Option.map (pair const) expected_modes,
-      proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [],
+      proposed_modes = Option.map (pair const o map fst) proposed_modes,
       proposed_names =
-        map_filter
-          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes,
+        the_default [] (Option.map (map_filter
+          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
@@ -176,7 +176,7 @@
 
 val opt_modes =
   Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
-    P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") []
+    P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
 
 val opt_expected_modes =
   Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -282,7 +282,7 @@
 
 datatype options = Options of {  
   expected_modes : (string * mode' list) option,
-  proposed_modes : (string * mode' list) list,
+  proposed_modes : (string * mode' list) option,
   proposed_names : ((string * mode') * string) list,
   show_steps : bool,
   show_proof_trace : bool,
@@ -299,7 +299,7 @@
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name
+fun proposed_modes (Options opt) = #proposed_modes opt
 fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode')
   (#proposed_names opt) (name, mode)
 
@@ -318,7 +318,7 @@
 
 val default_options = Options {
   expected_modes = NONE,
-  proposed_modes = [],
+  proposed_modes = NONE,
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -82,10 +82,6 @@
     ^ "\n" ^ Pretty.string_of (Pretty.chunks
       (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
 
-(* reference to preprocessing of InductiveSet package *)
-
-val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)
-
 (** fundamentals **)
 
 (* syntactic operations *)
@@ -417,22 +413,45 @@
   end
 
 (* validity checks *)
+(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)
 
-fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes =
-      case expected_modes options of
-      SOME (s, ms) => (case AList.lookup (op =) modes s of
-        SOME modes =>
-          let
-            val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
-          in
-            if not (eq_set eq_mode' (ms, modes')) then
-              error ("expected modes were not inferred:\n"
-              ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes')  ^ "\n"
-              ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
-            else ()
-          end
-        | NONE => ())
-    | NONE => ()
+fun check_expected_modes preds options modes =
+  case expected_modes options of
+    SOME (s, ms) => (case AList.lookup (op =) modes s of
+      SOME modes =>
+        let
+          val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
+        in
+          if not (eq_set eq_mode' (ms, modes')) then
+            error ("expected modes were not inferred:\n"
+            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes')  ^ "\n"
+            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
+          else ()
+        end
+      | NONE => ())
+  | NONE => ()
+
+fun check_proposed_modes preds options modes extra_modes errors =
+  case proposed_modes options of
+    SOME (s, ms) => (case AList.lookup (op =) modes s of
+      SOME inferred_ms =>
+        let
+          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
+          val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) inferred_ms
+        in
+          if not (eq_set eq_mode' (ms, modes')) then
+            error ("expected modes were not inferred:\n"
+            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes')  ^ "\n"
+            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms) ^ "\n"
+            ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
+            ^ cat_lines errors ^
+            (if not (null preds_without_modes) then
+              "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
+            else ""))
+          else ()
+        end
+      | NONE => ())
+  | NONE => ()
 
 (* importing introduction rules *)
 
@@ -584,13 +603,13 @@
           let
             val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
           in (fst (dest_Const const) = name) end;      
-        val intros = ind_set_codegen_preproc thy
+        val intros =
           (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
         val index = find_index (fn s => s = name) (#names (fst info))
         val pre_elim = nth (#elims result) index
         val pred = nth (#preds result) index
         val nparams = length (Inductive.params_of (#raw_induct result))
-        (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams 
+        (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
           (expand_tuples_elim pre_elim))*)
         val elim =
           (Drule.standard o Skip_Proof.make_thm thy)
@@ -659,8 +678,8 @@
 fun register_predicate (constname, pre_intros, pre_elim, nparams) thy =
   let
     (* preprocessing *)
-    val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
-    val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
+    val intros = map (preprocess_intro thy) pre_intros
+    val elim = preprocess_elim thy nparams pre_elim
   in
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
@@ -1042,21 +1061,34 @@
     else NONE
   end;
 
-fun print_failed_mode options thy modes p m rs i =
+fun print_failed_mode options thy modes p m rs is =
   if show_mode_inference options then
     let
-      val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
-      p ^ " violates mode " ^ string_of_mode thy p m)
+      val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+        p ^ " violates mode " ^ string_of_mode thy p m)
     in () end
   else ()
 
+fun error_of thy p m is =
+  ("  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
+        p ^ " violates mode " ^ string_of_mode thy p m)
+
+fun find_indices f xs =
+  map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
+
 fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
   let
     val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
-  in (p, filter (fn m => case find_index
-    (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
-      ~1 => true
-    | i => (print_failed_mode options thy modes p m rs i; false)) ms)
+    fun invalid_mode m =
+      case find_indices
+        (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
+        [] => NONE
+      | is => SOME (error_of thy p m is)
+    val res = map (fn m => (m, invalid_mode m)) ms
+    val ms' = map_filter (fn (m, NONE) => SOME m | _ => NONE) res
+    val errors = map_filter snd res
+  in
+    ((p, ms'), errors)
   end;
 
 fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
@@ -1071,14 +1103,24 @@
   let val y = f x
   in if x = y then x else fixp f y end;
 
+fun fixp_with_state f ((x : (string * mode list) list), state) =
+  let
+    val (y, state') = f (x, state)
+  in
+    if x = y then (y, state') else fixp_with_state f (y, state')
+  end
+
 fun infer_modes options thy extra_modes all_modes param_vs clauses =
   let
-    val modes =
-      fixp (fn modes =>
-        map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes)
-          all_modes
+    val (modes, errors) =
+      fixp_with_state (fn (modes, errors) =>
+        let
+          val res = map
+            (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes
+        in (map fst res, errors @ maps snd res) end)
+          (all_modes, [])
   in
-    map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes
+    (map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes, errors)
   end;
 
 fun remove_from rem [] = []
@@ -1087,7 +1129,7 @@
       NONE => (k, vs)
     | SOME vs' => (k, subtract (op =) vs' vs))
     :: remove_from rem xs
-    
+
 fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses =
   let
     val prednames = map fst clauses
@@ -1096,16 +1138,21 @@
       |> filter_out (fn (name, _) => member (op =) prednames name)
     val starting_modes = remove_from extra_modes' all_modes
     fun eq_mode (m1, m2) = (m1 = m2)
-    val modes =
-      fixp (fn modes =>
-        map (check_modes_pred options true thy param_vs clauses extra_modes'
-          (gen_modes @ modes)) modes) starting_modes
+    val (modes, errors) =
+      fixp_with_state (fn (modes, errors) =>
+        let
+          val res = map
+            (check_modes_pred options true thy param_vs clauses extra_modes'
+              (gen_modes @ modes)) modes
+        in (map fst res, errors @ maps snd res) end) (starting_modes, [])
+    val moded_clauses =
+      map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
+    val (moded_clauses', _) = infer_modes options thy extra_modes all_modes param_vs clauses
+    val join_moded_clauses_table = AList.join (op =)
+      (fn _ => fn ((mps1, mps2)) =>
+        merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2))
   in
-    AList.join (op =)
-    (fn _ => fn ((mps1, mps2)) =>
-      merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2))
-    (infer_modes options thy extra_modes all_modes param_vs clauses,
-    map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
+    (join_moded_clauses_table (moded_clauses', moded_clauses), errors)
   end;
 
 (* term construction *)
@@ -1524,66 +1571,67 @@
   let
     val compfuns = PredicateCompFuns.compfuns
     val T = AList.lookup (op =) preds name |> the
-    fun create_definition (mode as (iss, is)) thy = let
-      val mode_cname = create_constname_of_mode options thy "" name T mode
-      val mode_cbasename = Long_Name.base_name mode_cname
-      val Ts = binder_types T
-      val (Ts1, Ts2) = chop (length iss) Ts
-      val (Us1, Us2) =  split_smodeT is Ts2
-      val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
-      val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
-      val names = Name.variant_list []
-        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
-      val param_names = Name.variant_list []
-        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
-      val xparams = map2 (curry Free) param_names Ts1'
-      fun mk_vars (i, T) names =
-        let
-          val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
-        in
-          case AList.lookup (op =) is i of
-             NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
-           | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
-           | SOME (SOME pis) =>
-             let
-               val (Tins, Touts) = split_tupleT pis T
-               val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
-               val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
-               val xin = Free (name_in, HOLogic.mk_tupleT Tins)
-               val xout = Free (name_out, HOLogic.mk_tupleT Touts)
-               val xarg = mk_arg xin xout pis T
-             in
-               (((if null Tins then [] else [xin],
-               if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
-             end
-      val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
-      val (xinout, xargs) = split_list xinoutargs
-      val (xins, xouts) = pairself flat (split_list xinout)
-      val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
-      fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
-        | mk_split_lambda [x] t = lambda x t
-        | mk_split_lambda xs t =
-        let
-          fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
-            | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
-        in
-          mk_split_lambda' xs t
+    fun create_definition (mode as (iss, is)) thy =
+      let
+        val mode_cname = create_constname_of_mode options thy "" name T mode
+        val mode_cbasename = Long_Name.base_name mode_cname
+        val Ts = binder_types T
+        val (Ts1, Ts2) = chop (length iss) Ts
+        val (Us1, Us2) =  split_smodeT is Ts2
+        val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
+        val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2))
+        val names = Name.variant_list []
+          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
+        val param_names = Name.variant_list []
+          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1')))
+        val xparams = map2 (curry Free) param_names Ts1'
+        fun mk_vars (i, T) names =
+          let
+            val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
+          in
+            case AList.lookup (op =) is i of
+               NONE => ((([], [Free (vname, T)]), Free (vname, T)), vname :: names)
+             | SOME NONE => ((([Free (vname, T)], []), Free (vname, T)), vname :: names)
+             | SOME (SOME pis) =>
+               let
+                 val (Tins, Touts) = split_tupleT pis T
+                 val name_in = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "in")
+                 val name_out = Name.variant names ("x" ^ string_of_int (length Ts1' + i) ^ "out")
+                 val xin = Free (name_in, HOLogic.mk_tupleT Tins)
+                 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
+                 val xarg = mk_arg xin xout pis T
+               in
+                 (((if null Tins then [] else [xin],
+                 if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+               end
+        val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
+        val (xinout, xargs) = split_list xinoutargs
+        val (xins, xouts) = pairself flat (split_list xinout)
+        val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
+        fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
+          | mk_split_lambda [x] t = lambda x t
+          | mk_split_lambda xs t =
+          let
+            fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
+              | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
+          in
+            mk_split_lambda' xs t
+          end;
+        val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
+          (list_comb (Const (name, T), xparams' @ xargs)))
+        val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
+        val def = Logic.mk_equals (lhs, predterm)
+        val ([definition], thy') = thy |>
+          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
+          PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
+        val (intro, elim) =
+          create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
+        in thy'
+          |> add_predfun name mode (mode_cname, definition, intro, elim)
+          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
+          |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
+          |> Theory.checkpoint
         end;
-      val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
-        (list_comb (Const (name, T), xparams' @ xargs)))
-      val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
-      val def = Logic.mk_equals (lhs, predterm)
-      val ([definition], thy') = thy |>
-        Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
-        PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
-      val (intro, elim) =
-        create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
-      in thy'
-        |> add_predfun name mode (mode_cname, definition, intro, elim)
-        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
-        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
-        |> Theory.checkpoint
-      end;
   in
     fold create_definition modes thy
   end;
@@ -1626,8 +1674,8 @@
 
 (* MAJOR FIXME:  prove_params should be simple
  - different form of introrule for parameters ? *)
-fun prove_param thy NONE t = TRY (rtac @{thm refl} 1)
-  | prove_param thy (m as SOME (Mode (mode, is, ms))) t =
+fun prove_param options thy NONE t = TRY (rtac @{thm refl} 1)
+  | prove_param options thy (m as SOME (Mode (mode, is, ms))) t =
   let
     val  (f, args) = strip_comb (Envir.eta_contract t)
     val (params, _) = chop (length ms) args
@@ -1639,16 +1687,15 @@
     | Free _ => TRY (rtac @{thm refl} 1)
     | Abs _ => error "prove_param: No valid parameter term"
   in
-    REPEAT_DETERM (etac @{thm thin_rl} 1)
-    THEN REPEAT_DETERM (rtac @{thm ext} 1)
-    THEN print_tac "prove_param"
+    REPEAT_DETERM (rtac @{thm ext} 1)
+    THEN print_tac' options "prove_param"
     THEN f_tac
-    THEN print_tac "after simplification in prove_args"
-    THEN (EVERY (map2 (prove_param thy) ms params))
+    THEN print_tac' options "after simplification in prove_args"
+    THEN (EVERY (map2 (prove_param options thy) ms params))
     THEN (REPEAT_DETERM (atac 1))
   end
 
-fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) =
+fun prove_expr options thy (Mode (mode, is, ms), t, us) (premposition : int) =
   case strip_comb t of
     (Const (name, T), args) =>  
       let
@@ -1656,16 +1703,16 @@
         val (args1, args2) = chop (length ms) args
       in
         rtac @{thm bindI} 1
-        THEN print_tac "before intro rule:"
+        THEN print_tac' options "before intro rule:"
         (* for the right assumption in first position *)
         THEN rotate_tac premposition 1
         THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
         THEN rtac introrule 1
-        THEN print_tac "after intro rule"
+        THEN print_tac' options "after intro rule"
         (* work with parameter arguments *)
-        THEN (atac 1)
-        THEN (print_tac "parameter goal")
-        THEN (EVERY (map2 (prove_param thy) ms args1))
+        THEN atac 1
+        THEN print_tac' options "parameter goal"
+        THEN (EVERY (map2 (prove_param options thy) ms args1))
         THEN (REPEAT_DETERM (atac 1))
       end
   | _ => rtac @{thm bindI} 1
@@ -1673,7 +1720,7 @@
       (HOL_basic_ss' addsimps [@{thm "split_eta"}, @{thm "split_beta"}, @{thm "fst_conv"},
          @{thm "snd_conv"}, @{thm pair_collapse}]) 1
     THEN (atac 1)
-    THEN print_tac "after prove parameter call"
+    THEN print_tac' options "after prove parameter call"
     
 
 fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
@@ -1725,9 +1772,9 @@
     val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems out_ts [] =
       (prove_match thy out_ts)
-      THEN print_tac "before simplifying assumptions"
+      THEN print_tac' options "before simplifying assumptions"
       THEN asm_full_simp_tac HOL_basic_ss' 1
-      THEN print_tac "before single intro rule"
+      THEN print_tac' options "before single intro rule"
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
       let
@@ -1737,11 +1784,11 @@
               val (_, out_ts''') = split_smode is us
               val rec_tac = prove_prems out_ts''' ps
             in
-              print_tac "before clause:"
+              print_tac' options "before clause:"
               THEN asm_simp_tac HOL_basic_ss 1
-              THEN print_tac "before prove_expr:"
-              THEN prove_expr thy (mode, t, us) premposition
-              THEN print_tac "after prove_expr:"
+              THEN print_tac' options "before prove_expr:"
+              THEN prove_expr options thy (mode, t, us) premposition
+              THEN print_tac' options "after prove_expr:"
               THEN rec_tac
             end
           | Negprem (us, t) =>
@@ -1752,13 +1799,18 @@
               val (_, params) = strip_comb t
             in
               rtac @{thm bindI} 1
+              THEN print_tac' options "before prove_neg_expr:"
               THEN (if (is_some name) then
-                  simp_tac (HOL_basic_ss addsimps
+                  print_tac' options ("before unfolding definition " ^
+                    (Display.string_of_thm_global thy
+                      (predfun_definition_of thy (the name) (iss, is))))
+                  THEN simp_tac (HOL_basic_ss addsimps
                     [predfun_definition_of thy (the name) (iss, is)]) 1
                   THEN rtac @{thm not_predI} 1
+                  THEN print_tac' options "after applying rule not_predI"
                   THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
                   THEN (REPEAT_DETERM (atac 1))
-                  THEN (EVERY (map2 (prove_param thy) param_modes params))
+                  THEN (EVERY (map2 (prove_param options thy) param_modes params))
                 else
                   rtac @{thm not_predI'} 1)
                   THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
@@ -1767,9 +1819,9 @@
           | Sidecond t =>
            rtac @{thm bindI} 1
            THEN rtac @{thm if_predI} 1
-           THEN print_tac "before sidecond:"
+           THEN print_tac' options "before sidecond:"
            THEN prove_sidecond thy modes t
-           THEN print_tac "after sidecond:"
+           THEN print_tac' options "after sidecond:"
            THEN prove_prems [] ps)
       in (prove_match thy out_ts)
           THEN rest_tac
@@ -1800,7 +1852,7 @@
            (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
              (1 upto (length moded_clauses))))
     THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses))
-    THEN print_tac "proved one direction"
+    THEN print_tac' options "proved one direction"
   end;
 
 (** Proof in the other direction **)
@@ -2106,9 +2158,10 @@
             map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
       end
     val all_modes = map (fn (s, T) =>
-      case proposed_modes options s of
+      case proposed_modes options of
         NONE => (s, modes_of_typ T)
-      | SOME modes' => (s, map (translate_mode' nparams) modes'))
+      | SOME (s', modes') =>
+          if s = s' then (s, map (translate_mode' nparams) modes') else (s, modes_of_typ T))
         preds
   in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
 
@@ -2173,12 +2226,12 @@
             val args = map2 (curry Free) arg_names Ts
             val predfun = Const (predfun_name_of thy predname full_mode,
               Ts ---> PredicateCompFuns.mk_predT @{typ unit})
-            val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"})
+            val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = predfun_definition_of thy predname full_mode
             val tac = fn _ => Simplifier.simp_tac
-              (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
+              (HOL_basic_ss addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
             val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
           in
             (pred, result_thms @ [eq])
@@ -2199,7 +2252,7 @@
   define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory,
   infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
     -> string list -> (string * (term list * indprem list) list) list
-    -> moded_clause list pred_mode_table,
+    -> moded_clause list pred_mode_table * string list,
   prove : options -> theory -> (string * (term list * indprem list) list) list
     -> (string * typ) list -> (string * mode list) list
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
@@ -2220,10 +2273,11 @@
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
       prepare_intrs options thy prednames (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
-    val moded_clauses =
+    val (moded_clauses, errors) =
       #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes preds options modes
+    val _ = check_proposed_modes preds options modes extra_modes errors
     val _ = print_modes options thy modes
       (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -137,7 +137,7 @@
     th'
   end
 
-fun store_thm_in_table options ignore_consts thy th=
+fun store_thm_in_table options ignore thy th=
   let
     val th = th
       |> inline_equations options thy
@@ -153,29 +153,29 @@
       else if (is_introlike th) then (defining_const_of_introrule th, th)
       else error "store_thm: unexpected definition format"
   in
-    if not (member (op =) ignore_consts const) then
-      Symtab.cons_list (const, th)
-    else I
+    if ignore const then I else Symtab.cons_list (const, th)
   end
 
 fun make_const_spec_table options thy =
   let
-    fun store ignore_const f =
-      fold (store_thm_in_table options ignore_const thy)
+    fun store ignore f =
+      fold (store_thm_in_table options ignore thy)
         (map (Thm.transfer thy) (f (ProofContext.init thy)))
     val table = Symtab.empty
-      |> store [] Predicate_Compile_Alternative_Defs.get
-    val ignore_consts = Symtab.keys table
+      |> store (K false) Predicate_Compile_Alternative_Defs.get
+    val ignore = Symtab.defined table
   in
     table
-    |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
-    |> store ignore_consts Nitpick_Simps.get
-    |> store ignore_consts Nitpick_Intros.get
+    |> store ignore (fn ctxt => maps
+      (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else [])
+        (Spec_Rules.get ctxt))
+    |> store ignore Nitpick_Simps.get
+    |> store ignore Nitpick_Intros.get
   end
 
 fun get_specification table constname =
   case Symtab.lookup table constname of
-    SOME thms => thms
+    SOME thms => thms                  
   | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
 
 val logic_operator_names =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -89,9 +89,7 @@
 
 fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
   | mk_param thy lookup_pred t =
-  let
-  val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
-  in if Predicate_Compile_Aux.is_predT (fastype_of t) then
+  if Predicate_Compile_Aux.is_predT (fastype_of t) then
     t
   else
     let
@@ -109,7 +107,7 @@
       val pred_body = HOLogic.mk_eq (body', resvar)
       val param = fold_rev lambda (vs' @ [resvar]) pred_body
     in param end
-  end
+    
 (* creates the list of premises for every intro rule *)
 (* theory -> term -> (string list, term list list) *)
 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -23,7 +23,7 @@
 
 val options = Options {
   expected_modes = NONE,
-  proposed_modes = [],
+  proposed_modes = NONE,
   proposed_names = [],
   show_steps = true,
   show_intermediate_results = true,
@@ -83,7 +83,7 @@
     val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
     val _ = tracing (Display.string_of_thm ctxt' intro)
     val thy'' = thy'
-      |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
+      |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
       |> Predicate_Compile.preprocess options full_constname
       |> Predicate_Compile_Core.add_equations options [full_constname]
       (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
--- a/src/HOL/Tools/primrec.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -198,7 +198,7 @@
       (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     val rhs = singleton (Syntax.check_terms ctxt)
       (TypeInfer.constrain varT raw_rhs);
-  in (var, ((Binding.name def_name, []), rhs)) end;
+  in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 19 10:49:43 2009 +0100
@@ -87,6 +87,9 @@
 values "{(c, a, b). JamesBond a b c}"
 values "{(c, b, a). JamesBond a b c}"
 
+values "{(a, b). JamesBond 0 b a}"
+values "{(c, a). JamesBond a 0 c}"
+values "{(a, c). JamesBond a 0 c}"
 
 subsection {* Alternative Rules *}
 
@@ -476,6 +479,8 @@
 
 subsection {* transitive predicate *}
 
+text {* Also look at the tabled transitive closure in the Library *}
+
 code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl,
   (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool,
   (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp
@@ -509,6 +514,28 @@
 values [mode: o => i => bool] 10 "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
 
+inductive example_graph :: "int => int => bool"
+where
+  "example_graph 0 1"
+| "example_graph 1 2"
+| "example_graph 1 3"
+| "example_graph 4 7"
+| "example_graph 4 5"
+| "example_graph 5 6"
+| "example_graph 7 6"
+| "example_graph 7 8"
+ 
+inductive not_reachable_in_example_graph :: "int => int => bool"
+where "\<not> (tranclp example_graph x y) ==> not_reachable_in_example_graph x y"
+
+code_pred (expected_modes: i => i => bool) not_reachable_in_example_graph .
+
+thm not_reachable_in_example_graph.equation
+
+value "not_reachable_in_example_graph 0 3"
+value "not_reachable_in_example_graph 4 8"
+value "not_reachable_in_example_graph 5 6"
+
 subsection {* IMP *}
 
 types
@@ -724,7 +751,7 @@
 
 subsection {* Inverting list functions *}
 
-code_pred [inductify, show_intermediate_results] length .
+code_pred [inductify] length .
 code_pred [inductify, random] length .
 thm size_listP.equation
 thm size_listP.random_equation
@@ -804,8 +831,6 @@
 thm spliceP.equation
 
 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
-(* TODO: correct error messages:*)
-(* values {(xs, ys, zs). spliceP xs ... } *)
 
 code_pred [inductify] List.rev .
 code_pred [inductify] map .
@@ -965,13 +990,8 @@
 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
 | plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
 
-(* TODO: breaks if code_pred_intro is used? *)
-(*
-lemmas [code_pred_intro] = irconst objaddr plus
-*)
-thm eval_var.cases
 
-code_pred eval_var . (*by (rule eval_var.cases)*)
+code_pred eval_var .
 thm eval_var.equation
 
 values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
--- a/src/Pure/Isar/code.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/Pure/Isar/code.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -775,49 +775,4 @@
 
 end;
 
-(** datastructure to log definitions for preprocessing of the predicate compiler **)
-(* obviously a clone of Named_Thms *)
-
-signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-sig
-  val get: Proof.context -> thm list
-  val add_thm: thm -> Context.generic -> Context.generic
-  val del_thm: thm -> Context.generic -> Context.generic
-  
-  val add_attribute : attribute
-  val del_attribute : attribute
-  
-  val add_attrib : Attrib.src
-  
-  val setup: theory -> theory
-end;
-
-structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
-struct
-
-structure Data = Generic_Data
-(
-  type T = thm list;
-  val empty = [];
-  val extend = I;
-  val merge = Thm.merge_thms;
-);
-
-val get = Data.get o Context.Proof;
-
-val add_thm = Data.map o Thm.add_thm;
-val del_thm = Data.map o Thm.del_thm;
-
-val add_attribute = Thm.declaration_attribute add_thm;
-val del_attribute = Thm.declaration_attribute del_thm;
-
-val add_attrib = Attrib.internal (K add_attribute)
-
-val setup =
-  Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
-    ("declaration of definition for preprocessing of the predicate compiler") #>
-  PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
-
-end;
-
 structure Code : CODE = struct open Code; end;
--- a/src/Pure/Isar/constdefs.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -55,8 +55,7 @@
       |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
         Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
-        Code.add_default_eqn thm #>
-        Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
+        Code.add_default_eqn thm);
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
--- a/src/Pure/Isar/specification.ML	Thu Nov 19 10:33:20 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Nov 19 10:49:43 2009 +0100
@@ -212,8 +212,7 @@
 
     val ([(def_name, [th'])], lthy4) = lthy3
       |> Local_Theory.notes_kind Thm.definitionK
-        [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
-            Code.add_default_eqn_attrib :: atts), [([th], [])])];
+        [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
     val _ =