merged

--- a/src/HOL/Predicate.thy	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Predicate.thy	Sun Oct 25 00:10:25 2009 +0200
@@ -471,49 +471,49 @@
   "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
   by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
 
-definition singleton :: "'a pred \<Rightarrow> 'a" where
-  "singleton A = (if \<exists>!x. eval A x then THE x. eval A x else undefined)"
+definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
+  "singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
 
 lemma singleton_eqI:
-  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton A = x"
+  "\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x"
   by (auto simp add: singleton_def)
 
 lemma eval_singletonI:
-  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton A)"
+  "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
 proof -
   assume assm: "\<exists>!x. eval A x"
   then obtain x where "eval A x" ..
-  moreover with assm have "singleton A = x" by (rule singleton_eqI)
+  moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
   ultimately show ?thesis by simp 
 qed
 
 lemma single_singleton:
-  "\<exists>!x. eval A x \<Longrightarrow> single (singleton A) = A"
+  "\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A"
 proof -
   assume assm: "\<exists>!x. eval A x"
-  then have "eval A (singleton A)"
+  then have "eval A (singleton dfault A)"
     by (rule eval_singletonI)
-  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton A = x"
+  moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
     by (rule singleton_eqI)
-  ultimately have "eval (single (singleton A)) = eval A"
+  ultimately have "eval (single (singleton dfault A)) = eval A"
     by (simp (no_asm_use) add: single_def expand_fun_eq) blast
   then show ?thesis by (simp add: eval_inject)
 qed
 
 lemma singleton_undefinedI:
-  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton A = undefined"
+  "\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()"
   by (simp add: singleton_def)
 
 lemma singleton_bot:
-  "singleton \<bottom> = undefined"
+  "singleton dfault \<bottom> = dfault ()"
   by (auto simp add: bot_pred_def intro: singleton_undefinedI)
 
 lemma singleton_single:
-  "singleton (single x) = x"
+  "singleton dfault (single x) = x"
   by (auto simp add: intro: singleton_eqI singleI elim: singleE)
 
 lemma singleton_sup_single_single:
-  "singleton (single x \<squnion> single y) = (if x = y then x else undefined)"
+  "singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())"
 proof (cases "x = y")
   case True then show ?thesis by (simp add: singleton_single)
 next
@@ -523,25 +523,25 @@
   by (auto intro: supI1 supI2 singleI)
   with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)"
     by blast
-  then have "singleton (single x \<squnion> single y) = undefined"
+  then have "singleton dfault (single x \<squnion> single y) = dfault ()"
     by (rule singleton_undefinedI)
   with False show ?thesis by simp
 qed
 
 lemma singleton_sup_aux:
-  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
-    else if B = \<bottom> then singleton A
-    else singleton
-      (single (singleton A) \<squnion> single (singleton B)))"
+  "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
+    else if B = \<bottom> then singleton dfault A
+    else singleton dfault
+      (single (singleton dfault A) \<squnion> single (singleton dfault B)))"
 proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)")
   case True then show ?thesis by (simp add: single_singleton)
 next
   case False
   from False have A_or_B:
-    "singleton A = undefined \<or> singleton B = undefined"
+    "singleton dfault A = dfault () \<or> singleton dfault B = dfault ()"
     by (auto intro!: singleton_undefinedI)
-  then have rhs: "singleton
-    (single (singleton A) \<squnion> single (singleton B)) = undefined"
+  then have rhs: "singleton dfault
+    (single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()"
     by (auto simp add: singleton_sup_single_single singleton_single)
   from False have not_unique:
     "\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp
@@ -551,7 +551,7 @@
       by (blast elim: not_bot)
     with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)"
       by (auto simp add: sup_pred_def bot_pred_def)
-    then have "singleton (A \<squnion> B) = undefined" by (rule singleton_undefinedI)
+    then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI)
     with True rhs show ?thesis by simp
   next
     case False then show ?thesis by auto
@@ -559,10 +559,10 @@
 qed
 
 lemma singleton_sup:
-  "singleton (A \<squnion> B) = (if A = \<bottom> then singleton B
-    else if B = \<bottom> then singleton A
-    else if singleton A = singleton B then singleton A else undefined)"
-using singleton_sup_aux [of A B] by (simp only: singleton_sup_single_single)
+  "singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B
+    else if B = \<bottom> then singleton dfault A
+    else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())"
+using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single)
 
 
 subsubsection {* Derived operations *}
@@ -743,36 +743,43 @@
   "is_empty (Seq f) \<longleftrightarrow> null (f ())"
   by (simp add: null_is_empty Seq_def)
 
-primrec the_only :: "'a seq \<Rightarrow> 'a" where
-  [code del]: "the_only Empty = undefined"
-  | "the_only (Insert x P) = (if is_empty P then x else let y = singleton P in if x = y then x else undefined)"
-  | "the_only (Join P xq) = (if is_empty P then the_only xq else if null xq then singleton P
-       else let x = singleton P; y = the_only xq in
-       if x = y then x else undefined)"
+primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
+  [code del]: "the_only dfault Empty = dfault ()"
+  | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
+  | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
+       else let x = singleton dfault P; y = the_only dfault xq in
+       if x = y then x else dfault ())"
 
 lemma the_only_singleton:
-  "the_only xq = singleton (pred_of_seq xq)"
+  "the_only dfault xq = singleton dfault (pred_of_seq xq)"
   by (induct xq)
     (auto simp add: singleton_bot singleton_single is_empty_def
     null_is_empty Let_def singleton_sup)
 
 lemma singleton_code [code]:
-  "singleton (Seq f) = (case f ()
-   of Empty \<Rightarrow> undefined
+  "singleton dfault (Seq f) = (case f ()
+   of Empty \<Rightarrow> dfault ()
     | Insert x P \<Rightarrow> if is_empty P then x
-        else let y = singleton P in
-          if x = y then x else undefined
-    | Join P xq \<Rightarrow> if is_empty P then the_only xq
-        else if null xq then singleton P
-        else let x = singleton P; y = the_only xq in
-          if x = y then x else undefined)"
+        else let y = singleton dfault P in
+          if x = y then x else dfault ()
+    | Join P xq \<Rightarrow> if is_empty P then the_only dfault xq
+        else if null xq then singleton dfault P
+        else let x = singleton dfault P; y = the_only dfault xq in
+          if x = y then x else dfault ())"
   by (cases "f ()")
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
 
-lemma meta_fun_cong:
-"f == g ==> f x == g x"
-by simp
+definition not_unique :: "'a pred => 'a"
+where
+  [code del]: "not_unique A = (THE x. eval A x)"
+
+definition the :: "'a pred => 'a"
+where
+  [code del]: "the A = (THE x. eval A x)"
+
+lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
+by (auto simp add: the_def singleton_def not_unique_def)
 
 ML {*
 signature PREDICATE =
@@ -819,6 +826,8 @@
 code_const Seq and Empty and Insert and Join
   (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
 
+code_abort not_unique
+
 text {* dummy setup for @{text code_pred} and @{text values} keywords *}
 
 ML {*
@@ -852,6 +861,6 @@
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
+  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/pred_compile_aux.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -6,8 +6,16 @@
 structure Predicate_Compile_Aux =
 struct
 
+(* general syntactic functions *)
+
+(*Like dest_conj, but flattens conjunctions however nested*)
+fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
+  | conjuncts_aux t conjs = t::conjs;
+
+fun conjuncts t = conjuncts_aux t [];
+
 (* syntactic functions *)
- 
+
 fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
   | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
   | is_equationlike_term _ = false
@@ -69,26 +77,52 @@
   in ((ps', t''), nctxt') end;
 
 
+(* introduction rule combinators *)
 
+(* combinators to apply a function to all literals of an introduction rules *)
 
-(*
 fun map_atoms f intro = 
-fun fold_atoms f intro =
-*)
+  let
+    val (literals, head) = Logic.strip_horn intro
+    fun appl t = (case t of
+        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
+      | _ => f t)
+  in
+    Logic.list_implies
+      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
+  end
+
+fun fold_atoms f intro s =
+  let
+    val (literals, head) = Logic.strip_horn intro
+    fun appl t s = (case t of
+      (@{term "Not"} $ t') => f t' s
+      | _ => f t s)
+  in fold appl (map HOLogic.dest_Trueprop literals) s end
+
 fun fold_map_atoms f intro s =
   let
     val (literals, head) = Logic.strip_horn intro
     fun appl t s = (case t of
-      (@{term "Not"} $ t') =>
-        let
-          val (t'', s') = f t' s
-        in (@{term "Not"} $ t'', s') end
+      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
       | _ => f t s)
     val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
   in
     (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
   end;
+
+fun maps_premises f intro =
+  let
+    val (premises, head) = Logic.strip_horn intro
+  in
+    Logic.list_implies (maps f premises, head)
+  end
   
+(* lifting term operations to theorems *)
+
+fun map_term thy f th =
+  Skip_Proof.make_thm thy (f (prop_of th))
+
 (*
 fun equals_conv lhs_cv rhs_cv ct =
   case Thm.term_of ct of
@@ -96,5 +130,107 @@
   | _ => error "equals_conv"  
 *)
 
+(* Different options for compiler *)
+
+datatype options = Options of {  
+  expected_modes : (string * int list list) option,
+  show_steps : bool,
+  show_mode_inference : bool,
+  show_proof_trace : bool,
+  show_intermediate_results : bool,
+  show_compilation : bool,
+  skip_proof : bool,
+
+  inductify : bool,
+  rpred : bool,
+  depth_limited : bool
+};
+
+fun expected_modes (Options opt) = #expected_modes opt
+fun show_steps (Options opt) = #show_steps opt
+fun show_mode_inference (Options opt) = #show_mode_inference opt
+fun show_intermediate_results (Options opt) = #show_intermediate_results opt
+fun show_proof_trace (Options opt) = #show_proof_trace opt
+fun show_compilation (Options opt) = #show_compilation opt
+fun skip_proof (Options opt) = #skip_proof opt
+
+fun is_inductify (Options opt) = #inductify opt
+fun is_rpred (Options opt) = #rpred opt
+fun is_depth_limited (Options opt) = #depth_limited opt
+
+val default_options = Options {
+  expected_modes = NONE,
+  show_steps = false,
+  show_intermediate_results = false,
+  show_proof_trace = false,
+  show_mode_inference = false,
+  show_compilation = false,
+  skip_proof = false,
+  
+  inductify = false,
+  rpred = false,
+  depth_limited = false
+}
+
+
+fun print_step options s =
+  if show_steps options then tracing s else ()
+
+(* tuple processing *)
+
+fun expand_tuples thy intro =
+  let
+    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
+      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
+      (case HOLogic.strip_tupleT (fastype_of arg) of
+        (Ts as _ :: _ :: _) =>
+        let
+          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
+            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
+            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
+              let
+                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
+                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
+                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
+                val args' = map (Pattern.rewrite_term thy [pat] []) args
+              in
+                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
+              end
+            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
+          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
+            (args, (pats, intro_t, ctxt))
+        in
+          rewrite_args args' (pats, intro_t', ctxt')
+        end
+      | _ => rewrite_args args (pats, intro_t, ctxt))
+    fun rewrite_prem atom =
+      let
+        val (_, args) = strip_comb atom
+      in rewrite_args args end
+    val ctxt = ProofContext.init thy
+    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
+    val intro_t = prop_of intro'
+    val concl = Logic.strip_imp_concl intro_t
+    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
+    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
+    val (pats', intro_t', ctxt3) = 
+      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
+    fun rewrite_pat (ct1, ct2) =
+      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
+    val t_insts' = map rewrite_pat t_insts
+    val intro'' = Thm.instantiate (T_insts, t_insts') intro
+    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
+    val intro'''' = Simplifier.full_simplify
+      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
+      intro'''
+    (* splitting conjunctions introduced by Pair_eq*)
+    fun split_conj prem =
+      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
+    val intro''''' = map_term thy (maps_premises split_conj) intro''''
+  in
+    intro'''''
+  end
+
+
 
 end;

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -3,16 +3,16 @@
 Book-keeping datastructure for the predicate compiler
 
 *)
-signature PRED_COMPILE_DATA =
+signature PREDICATE_COMPILE_DATA =
 sig
   type specification_table;
   val make_const_spec_table : theory -> specification_table
   val get_specification :  specification_table -> string -> thm list
-  val obtain_specification_graph : specification_table -> string -> thm list Graph.T
+  val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T
   val normalize_equation : theory -> thm -> thm
 end;
 
-structure Pred_Compile_Data : PRED_COMPILE_DATA =
+structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA =
 struct
 
 open Predicate_Compile_Aux;
@@ -81,11 +81,13 @@
     Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection}
   | _ => th
 
+val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+
 fun full_fun_cong_expand th =
   let
     val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th)))
     val i = length (binder_types (fastype_of f)) - length args
-  in funpow i (fn th => th RS @{thm meta_fun_cong}) th end;
+  in funpow i (fn th => th RS meta_fun_cong) th end;
 
 fun declare_names s xs ctxt =
   let
@@ -117,7 +119,7 @@
 
 fun normalize_equation thy th =
   mk_meta_equation th
-  |> Pred_Compile_Set.unfold_set_notation
+  |> Predicate_Compile_Set.unfold_set_notation
   |> full_fun_cong_expand
   |> split_all_pairs thy
   |> tap check_equation_format
@@ -127,19 +129,18 @@
 
 fun store_thm_in_table ignore_consts thy th=
   let
-    val th = AxClass.unoverload thy th
+    val th = th
       |> inline_equations thy
+      |> Predicate_Compile_Set.unfold_set_notation
+      |> AxClass.unoverload thy
     val (const, th) =
       if is_equationlike th then
         let
-          val _ = priority "Normalizing definition..."
           val eq = normalize_equation thy th
         in
           (defining_const_of_equation eq, eq)
         end
-      else if (is_introlike th) then
-        let val th = Pred_Compile_Set.unfold_set_notation th
-        in (defining_const_of_introrule th, th) end
+      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
@@ -147,18 +148,6 @@
     else I
   end
 
-(*
-fun make_const_spec_table_warning thy =
-  fold
-    (fn th => fn thy => case try (store_thm th) thy of
-      SOME thy => thy
-    | NONE => (warning ("store_thm fails for " ^ Display.string_of_thm_global thy th) ; thy))
-      (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
-
-fun make_const_spec_table thy =
-  fold store_thm (Predicate_Compile_Preproc_Const_Defs.get (ProofContext.init thy)) thy
-  |> (fn thy => fold store_thm (Nitpick_Simps.get (ProofContext.init thy)) thy)
-*)
 fun make_const_spec_table thy =
   let
     fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
@@ -166,35 +155,27 @@
       |> store [] Predicate_Compile_Alternative_Defs.get
     val ignore_consts = Symtab.keys table
   in
-    table   
+    table
     |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
     |> store ignore_consts Nitpick_Simps.get
     |> store ignore_consts Nitpick_Intros.get
   end
-  (*
-fun get_specification thy constname =
-  case Symtab.lookup (#const_spec_table (Data.get thy)) constname of
-    SOME thms => thms
-  | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
-  *)
+
 fun get_specification table constname =
   case Symtab.lookup table constname of
-  SOME thms =>
-    let
-      val _ = tracing ("Looking up specification of " ^ constname ^ ": "
-        ^ (commas (map Display.string_of_thm_without_context thms)))
-    in thms end
+    SOME thms => thms
   | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
 
 val logic_operator_names =
-  [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "op &"}]
+  [@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, 
+   @{const_name "op &"}]
 
-val special_cases = member (op =) [@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
+val special_cases = member (op =) [
+    @{const_name "False"},
+    @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
     @{const_name Nat.one_nat_inst.one_nat},
 @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"},
 @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
-@{const_name "Nat.nat.nat_case"}, @{const_name "List.list.list_case"},
-@{const_name "Option.option.option_case"},
 @{const_name Nat.ord_nat_inst.less_eq_nat},
 @{const_name number_nat_inst.number_of_nat},
   @{const_name Int.Bit0},
@@ -203,13 +184,19 @@
 @{const_name "Int.zero_int_inst.zero_int"},
 @{const_name "List.filter"}]
 
-fun obtain_specification_graph table constname =
+fun case_consts thy s = is_some (Datatype.info_of_case thy s)
+
+fun obtain_specification_graph thy table constname =
   let
     fun is_nondefining_constname c = member (op =) logic_operator_names c
     val is_defining_constname = member (op =) (Symtab.keys table)
+    fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c)
     fun defiants_of specs =
       fold (Term.add_const_names o prop_of) specs []
       |> filter is_defining_constname
+      |> filter_out is_nondefining_constname
+      |> filter_out has_code_pred_intros
+      |> filter_out (case_consts thy)
       |> filter_out special_cases
     fun extend constname =
       let

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -5,9 +5,10 @@
 
 signature PREDICATE_COMPILE_FUN =
 sig
-  val define_predicates : (string * thm list) list -> theory -> theory
+val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
   val rewrite_intro : theory -> thm -> thm list
   val setup_oracle : theory -> theory
+  val pred_of_function : theory -> string -> string option
 end;
 
 structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
@@ -63,6 +64,8 @@
   fun merge _ = Symtab.merge (op =);
 )
 
+fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
+
 fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) 
 
 
@@ -99,23 +102,29 @@
       (Free (Long_Name.base_name name ^ "P", pred_type T))
   end
 
-fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t
-  | mk_param lookup_pred t =
+fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
+  | mk_param thy lookup_pred t =
   let
-    val (vs, body) = strip_abs t
-    val names = Term.add_free_names body []
-    val vs_names = Name.variant_list names (map fst vs)
-    val vs' = map2 (curry Free) vs_names (map snd vs)
-    val body' = subst_bounds (rev vs', body)
-    val (f, args) = strip_comb body'
-    val resname = Name.variant (vs_names @ names) "res"
-    val resvar = Free (resname, body_type (fastype_of body'))
-    val P = lookup_pred f
-    val pred_body = list_comb (P, args @ [resvar])
-    val param = fold_rev lambda (vs' @ [resvar]) pred_body
-  in param end;
-
-
+  val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
+  in if Predicate_Compile_Aux.is_predT (fastype_of t) then
+    t
+  else
+    let
+      val (vs, body) = strip_abs t
+      val names = Term.add_free_names body []
+      val vs_names = Name.variant_list names (map fst vs)
+      val vs' = map2 (curry Free) vs_names (map snd vs)
+      val body' = subst_bounds (rev vs', body)
+      val (f, args) = strip_comb body'
+      val resname = Name.variant (vs_names @ names) "res"
+      val resvar = Free (resname, body_type (fastype_of body'))
+      (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
+      val pred_body = list_comb (P, args @ [resvar])
+      *)
+      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) *)
 
@@ -210,10 +219,14 @@
   let
     fun mk_prems' (t as Const (name, T)) (names, prems) =
       if is_constr thy name orelse (is_none (try lookup_pred t)) then
-        [(t ,(names, prems))]
+        [(t, (names, prems))]
       else [(lookup_pred t, (names, prems))]
     | mk_prems' (t as Free (f, T)) (names, prems) = 
       [(lookup_pred t, (names, prems))]
+    | mk_prems' (t as Abs _) (names, prems) =
+      if Predicate_Compile_Aux.is_predT (fastype_of t) then
+      [(t, (names, prems))] else error "mk_prems': Abs "
+      (* mk_param *)
     | mk_prems' t (names, prems) =
       if Predicate_Compile_Aux.is_constrt thy t then
         [(t, (names, prems))]
@@ -243,8 +256,10 @@
             maps mk_prems_of_assm assms
           end
         else
-          let 
+          let
             val (f, args) = strip_comb t
+            (* TODO: special procedure for higher-order functions: split arguments in
+              simple types and function types *)
             val resname = Name.variant names "res"
             val resvar = Free (resname, body_type (fastype_of t))
             val names' = resname :: names
@@ -261,8 +276,7 @@
                   val pred = lookup_pred t
                   val nparams = get_nparams pred
                   val (params, args) = chop nparams args
-                  val _ = tracing ("mk_prems'': " ^ (Syntax.string_of_term_global thy t) ^ " has " ^ string_of_int nparams ^ " parameters.")
-                  val params' = map (mk_param lookup_pred) params
+                  val params' = map (mk_param thy lookup_pred) params
                 in
                   folds_map mk_prems' args (names', prems)
                   |> map (fn (argvs, (names'', prems')) =>
@@ -281,7 +295,8 @@
                        val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
                      in (names', prem :: prems') end)
                 end
-            | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
+            | mk_prems'' t =
+              error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
           in
             map (pair resvar) (mk_prems'' f)
           end
@@ -292,7 +307,7 @@
 (* assumption: mutual recursive predicates all have the same parameters. *)  
 fun define_predicates specs thy =
   if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
-    thy
+    ([], thy)
   else
   let
     val consts = map fst specs
@@ -307,16 +322,14 @@
     val funnames = map (fst o dest_Const) funs
     val fun_pred_names = (funnames ~~ prednames)  
       (* mapping from term (Free or Const) to term *)
-    fun lookup_pred (Const (@{const_name Cons}, T)) =
-      Const ("Preprocessing.ConsP", pred_type T) (* FIXME: temporary - Cons lookup *)
-      | lookup_pred (Const (name, T)) =
+    fun lookup_pred (Const (name, T)) =
       (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
           SOME c => Const (c, pred_type T)
         | NONE =>
           (case AList.lookup op = fun_pred_names name of
             SOME f => Free (f, pred_type T)
           | NONE => Const (name, T)))
-      | lookup_pred  (Free (name, T)) =
+      | lookup_pred (Free (name, T)) =
         if member op = (map fst pnames) name then
           Free (name, transform_ho_typ T)
         else
@@ -347,12 +360,10 @@
             Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
         end
     fun mk_rewr_thm (func, pred) = @{thm refl}
-  in    
+  in
     case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
-      NONE => thy 
-    | SOME intr_ts => let
-        val _ = map (tracing o (Syntax.string_of_term_global thy)) intr_ts      
-      in
+      NONE => ([], thy) 
+    | SOME intr_ts =>
         if is_some (try (map (cterm_of thy)) intr_ts) then
           let
             val (ind_result, thy') =
@@ -367,10 +378,15 @@
             val prednames = map (fst o dest_Const) (#preds ind_result)
             (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
             (* add constants to my table *)
-          in Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy' end
+            val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames
+            val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
+          in
+            (specs, thy'')
+          end
         else
-          thy
-      end
+          let
+            val _ = tracing "Introduction rules of function_predicate are not welltyped"
+          in ([], thy) end
   end
 
 (* preprocessing intro rules - uses oracle *)
@@ -391,7 +407,6 @@
     | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
     
     val intro_t = (Logic.unvarify o prop_of) intro
-    val _ = tracing (Syntax.string_of_term_global thy intro_t)
     val (prems, concl) = Logic.strip_horn intro_t
     val frees = map fst (Term.add_frees intro_t [])
     fun rewrite prem names =
@@ -415,8 +430,6 @@
         rewrite concl frees'
         |> map (fn (concl'::conclprems, _) =>
           Logic.list_implies ((flat prems') @ conclprems, concl')))
-    val _ = tracing ("intro_ts': " ^
-      commas (map (Syntax.string_of_term_global thy) intro_ts'))
   in
     map (Drule.standard o the_oracle () o cterm_of thy) intro_ts'
   end; 

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -123,16 +123,67 @@
       else
         error ("unexpected specification for constant " ^ quote constname ^ ":\n"
           ^ commas (map (quote o Display.string_of_thm_global thy) specs))
-    val _ = tracing ("Introduction rules of definitions before flattening: "
-      ^ commas (map (Display.string_of_thm ctxt) intros))
-    val _ = tracing "Defining local predicates and their intro rules..."
     val (intros', (local_defs, thy')) = flatten_intros constname intros thy
     val (intross, thy'') = fold_map preprocess local_defs thy'
   in
-    (intros' :: flat intross,thy'')
+    ((constname, intros') :: flat intross,thy'')
   end;
 
 fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
-  
-  
+
+fun is_Abs (Abs _) = true
+  | is_Abs _       = false
+
+fun flat_higher_order_arguments (intross, thy) =
+  let
+    fun process constname atom (new_defs, thy) =
+      let
+        val (pred, args) = strip_comb atom
+        val abs_args = filter is_Abs args
+        fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
+          let
+            val _ = tracing ("Introduce new constant for " ^
+              Syntax.string_of_term_global thy abs_arg)
+            val vars = map Var (Term.add_vars abs_arg [])
+            val abs_arg' = Logic.unvarify abs_arg
+            val frees = map Free (Term.add_frees abs_arg' [])
+            val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
+              ((Long_Name.base_name constname) ^ "_hoaux")
+            val full_constname = Sign.full_bname thy constname
+            val constT = map fastype_of frees ---> (fastype_of abs_arg')
+            val const = Const (full_constname, constT)
+            val lhs = list_comb (const, frees)
+            val def = Logic.mk_equals (lhs, abs_arg')
+            val _ = tracing (Syntax.string_of_term_global thy def)
+            val ([definition], thy') = thy
+              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+          in
+            (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
+          end
+        | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
+        val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
+      in
+        (list_comb (pred, args'), (new_defs', thy'))
+      end
+    fun flat_intro intro (new_defs, thy) =
+      let
+        val constname = fst (dest_Const (fst (strip_comb
+          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
+        val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
+        val th = Skip_Proof.make_thm thy intro_ts
+      in
+        (th, (new_defs, thy))
+      end
+    fun fold_map_spec f [] s = ([], s)
+      | fold_map_spec f ((c, ths) :: specs) s =
+        let
+          val (ths', s') = f ths s
+          val (specs', s'') = fold_map_spec f specs s'
+        in ((c, ths') :: specs', s'') end
+    val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
+  in
+    (intross', (new_defs, thy'))
+  end
+
 end;

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -3,18 +3,19 @@
 A quickcheck generator based on the predicate compiler
 *)
 
-signature PRED_COMPILE_QUICKCHECK =
+signature PREDICATE_COMPILE_QUICKCHECK =
 sig
   val quickcheck : Proof.context -> term -> int -> term list option
   val test_ref :
     ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
 end;
 
-structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK =
+structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
 struct
 
 val test_ref =
   Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+
 val target = "Quickcheck"
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
@@ -63,21 +64,21 @@
     val _ = tracing (Display.string_of_thm ctxt' intro)
     val thy'' = thy'
       |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
-      |> Predicate_Compile.preprocess full_constname
-      |> Predicate_Compile_Core.add_equations [full_constname]
-      |> Predicate_Compile_Core.add_sizelim_equations [full_constname]
-      |> Predicate_Compile_Core.add_quickcheck_equations [full_constname]
-    val sizelim_modes = Predicate_Compile_Core.sizelim_modes_of thy'' full_constname
+      |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname
+      (* |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname]*)
+      (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
+      (* |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] *)
+    val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
     val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname  
     val prog =
       if member (op =) modes ([], []) then
         let
           val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], [])
-          val T = @{typ code_numeral} --> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
-        in Const (name, T) $ Bound 0 end
-      else if member (op =) sizelim_modes ([], []) then
+          val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs')))
+          in Const (name, T) $ @{term True} $ Bound 0 end
+      else if member (op =) depth_limited_modes ([], []) then
         let
-          val name = Predicate_Compile_Core.sizelim_function_name_of thy'' full_constname ([], [])
+          val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
           val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
         in lift_pred (Const (name, T) $ Bound 0) end
       else error "Predicate Compile Quickcheck failed"
@@ -85,7 +86,7 @@
       mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
       (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
     val _ = tracing (Syntax.string_of_term ctxt' qc_term)
-    val compile = Code_ML.eval (SOME target) ("Pred_Compile_Quickcheck.test_ref", test_ref)
+    val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
       (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
       thy'' qc_term []
   in

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -3,7 +3,7 @@
 Preprocessing sets to predicates
 *)
 
-signature PRED_COMPILE_SET =
+signature PREDICATE_COMPILE_SET =
 sig
 (*
   val preprocess_intro : thm -> theory -> thm * theory
@@ -12,10 +12,11 @@
   val unfold_set_notation : thm -> thm;
 end;
 
-structure Pred_Compile_Set : PRED_COMPILE_SET =
+structure Predicate_Compile_Set : PREDICATE_COMPILE_SET =
 struct
 (*FIXME: unfolding Ball in pretty adhoc here *)
-val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}]
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def},
+@{thm Ball_def}, @{thm Bex_def}]
 
 val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -4,87 +4,170 @@
 signature PREDICATE_COMPILE =
 sig
   val setup : theory -> theory
-  val preprocess : string -> theory -> theory
+  val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
 struct
 
+(* options *)
+val fail_safe_mode = true
+
 open Predicate_Compile_Aux;
 
 val priority = tracing;
 
 (* Some last processing *)
+
 fun remove_pointless_clauses intro =
   if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
     []
   else [intro]
 
-fun preprocess_strong_conn_constnames gr constnames thy =
+fun tracing s = ()
+
+fun print_intross options thy msg intross =
+  if show_intermediate_results options then
+   Output.tracing (msg ^ 
+    (space_implode "\n" (map 
+      (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
+         commas (map (Display.string_of_thm_global thy) intros)) intross)))
+  else ()
+      
+fun print_specs thy specs =
+  map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
+    ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+
+fun map_specs f specs =
+  map (fn (s, ths) => (s, f ths)) specs
+
+fun process_specification options specs thy' =
+  let
+    val _ = print_step options "Compiling predicates to flat introrules..."
+    val specs = map (apsnd (map
+      (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs
+    val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy')
+    val _ = print_intross options thy'' "Flattened introduction rules: " intross1
+    val _ = print_step options "Replacing functions in introrules..."
+    val intross2 =
+      if fail_safe_mode then
+        case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
+          SOME intross => intross
+        | NONE => let val _ = warning "Function replacement failed!" in intross1 end
+      else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
+    val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2
+    val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..."
+    val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
+    val (new_intross, thy'''')  =
+      if not (null new_defs) then
+      let
+        val _ = print_step options "Recursively obtaining introduction rules for new definitions..."
+      in process_specification options new_defs thy''' end
+    else ([], thy''')
+  in
+    (intross3 @ new_intross, thy'''')
+  end
+
+
+fun preprocess_strong_conn_constnames options gr constnames thy =
   let
     val get_specs = map (fn k => (k, Graph.get_node gr k))
-    val _ = priority ("Preprocessing scc of " ^ commas constnames)
+    val _ = print_step options ("Preprocessing scc of " ^ commas constnames)
     val (prednames, funnames) = List.partition (is_pred thy) constnames
     (* untangle recursion by defining predicates for all functions *)
-    val _ = priority "Compiling functions to predicates..."
-    val _ = tracing ("funnames: " ^ commas funnames)
-    val thy' =
-      thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
-      (get_specs funnames)
-    val _ = priority "Compiling predicates to flat introrules..."
-    val (intross, 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 intross)))
-    val _ = priority "Replacing functions in introrules..."
-      (*  val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross  *)
-    val intross' =
-      case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of
-        SOME intross' => intross'
-      | NONE => let val _ = warning "Function replacement failed!" in intross end
-    val _ = tracing ("Introduction rules with replaced functions: " ^
-      commas (map (Display.string_of_thm_global thy'') (flat intross')))
-    val intross'' = burrow (maps remove_pointless_clauses) intross'
-    val intross'' = burrow (map (AxClass.overload thy'')) intross''
-    val _ = priority "Registering intro rules..."
-    val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
+    val _ = print_step options
+      ("Compiling functions (" ^ commas funnames ^ ") to predicates...")
+    val (fun_pred_specs, thy') =
+      if not (null funnames) then Predicate_Compile_Fun.define_predicates
+      (get_specs funnames) thy else ([], thy)
+    val _ = print_specs thy' fun_pred_specs
+    val specs = (get_specs prednames) @ fun_pred_specs
+    val (intross3, thy''') = process_specification options specs thy'
+    val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
+    val intross4 = map_specs (maps remove_pointless_clauses) intross3
+    val _ = print_intross options thy''' "After removing pointless clauses: " intross4
+      (*val intross5 = map (fn s, ths) => ( s, map (AxClass.overload thy''') ths)) intross4*)
+    val intross6 = map_specs (map (expand_tuples thy''')) intross4
+    val _ = print_intross options thy''' "introduction rules before registering: " intross6
+    val _ = print_step options "Registering introduction rules..."
+    val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
   in
-    thy'''
+    thy''''
   end;
 
-fun preprocess const thy =
+fun preprocess options const thy =
   let
-    val _ = tracing ("Fetching definitions from theory...")
-    val table = Pred_Compile_Data.make_const_spec_table thy
-    val gr = Pred_Compile_Data.obtain_specification_graph table const
-    val _ = tracing (commas (Graph.all_succs gr [const]))
+    val _ = print_step options "Fetching definitions from theory..."
+    val table = Predicate_Compile_Data.make_const_spec_table thy
+    val gr = Predicate_Compile_Data.obtain_specification_graph thy table const
     val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
-  in fold_rev (preprocess_strong_conn_constnames gr)
+  in fold_rev (preprocess_strong_conn_constnames options gr)
     (Graph.strong_conn gr) thy
   end
 
-fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy =
-  if inductify_all then
-    let
-      val thy = ProofContext.theory_of lthy
-      val const = Code.read_const thy raw_const
-      val lthy' = LocalTheory.theory (preprocess const) lthy
-        |> LocalTheory.checkpoint
-      val _ = tracing "Starting Predicate Compile Core..."
-    in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end
-  else
-    Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy
+fun extract_options ((modes, raw_options), const) =
+  let
+    fun chk s = member (op =) raw_options s
+  in
+    Options {
+      expected_modes = Option.map (pair const) modes,
+      show_steps = chk "show_steps",
+      show_intermediate_results = chk "show_intermediate_results",
+      show_proof_trace = chk "show_proof_trace",
+      show_mode_inference = chk "show_mode_inference",
+      show_compilation = chk "show_compilation",
+      skip_proof = chk "skip_proof",
+      inductify = chk "inductify",
+      rpred = chk "rpred",
+      depth_limited = chk "depth_limited"
+    }
+  end
+
+fun code_pred_cmd ((modes, raw_options), raw_const) lthy =
+  let
+     val thy = ProofContext.theory_of lthy
+     val const = Code.read_const thy raw_const
+     val options = extract_options ((modes, raw_options), const)
+  in
+    if (is_inductify options) then
+      let
+        val lthy' = LocalTheory.theory (preprocess options const) lthy
+          |> LocalTheory.checkpoint
+        val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
+            SOME c => c
+          | NONE => const
+        val _ = print_step options "Starting Predicate Compile Core..."
+      in
+        Predicate_Compile_Core.code_pred options const lthy'
+      end
+    else
+      Predicate_Compile_Core.code_pred_cmd options raw_const lthy
+  end
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
-val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"]
+val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace",
+  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"]
 
 local structure P = OuterParse
 in
 
+val opt_modes =
+  Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
+   P.enum1 "," (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]")
+  --| P.$$$ ")" >> SOME) NONE
+
+val scan_params =
+  let
+    val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
+  in
+    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
+  end
+
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd)
+  OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >>
+    code_pred_cmd)
 
 end
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Oct 25 00:10:25 2009 +0200
@@ -7,26 +7,25 @@
 signature PREDICATE_COMPILE_CORE =
 sig
   val setup: theory -> theory
-  val code_pred: bool -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: bool -> string -> Proof.context -> Proof.state
+  val code_pred: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
+  val code_pred_cmd: Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
   type smode = (int * int list option) list
   type mode = smode option list * smode
   datatype tmode = Mode of mode * smode * tmode option list;
-  (*val add_equations_of: bool -> string list -> theory -> theory *)
-  val register_predicate : (thm list * thm * int) -> theory -> theory
-  val register_intros : thm list -> theory -> theory
+  val register_predicate : (string * thm list * thm * int) -> theory -> theory
+  val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
- (* val fetch_pred_data : theory -> string -> (thm list * thm * int)  *)
   val predfun_intro_of: theory -> string -> mode -> thm
   val predfun_elim_of: theory -> string -> mode -> thm
-  val strip_intro_concl: int -> term -> term * (term list * term list)
   val predfun_name_of: theory -> string -> mode -> string
   val all_preds_of : theory -> string list
   val modes_of: theory -> string -> mode list
-  val sizelim_modes_of: theory -> string -> mode list
-  val sizelim_function_name_of : theory -> string -> mode -> string
+  val depth_limited_modes_of: theory -> string -> mode list
+  val depth_limited_function_name_of : theory -> string -> mode -> string
   val generator_modes_of: theory -> string -> mode list
   val generator_name_of : theory -> string -> mode -> string
+  val all_modes_of : theory -> (string * mode list) list
+  val all_generator_modes_of : theory -> (string * mode list) list
   val string_of_mode : mode -> string
   val intros_of: theory -> string -> thm list
   val nparams_of: theory -> string -> int
@@ -35,24 +34,12 @@
   val set_nparams : string -> int -> theory -> theory
   val print_stored_rules: theory -> unit
   val print_all_modes: theory -> unit
-  val do_proofs: bool Unsynchronized.ref
-  val mk_casesrule : Proof.context -> int -> thm list -> term
-  val analyze_compr: theory -> term -> term
-  val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
-  val add_equations : string list -> theory -> theory
+  val mk_casesrule : Proof.context -> term -> int -> thm list -> term
+  val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
+  val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref
   val code_pred_intros_attrib : attribute
   (* used by Quickcheck_Generator *) 
-  (*val funT_of : mode -> typ -> typ
-  val mk_if_pred : term -> term
-  val mk_Eval : term * term -> term*)
-  val mk_tupleT : typ list -> typ
-(*  val mk_predT :  typ -> typ *)
   (* temporary for testing of the compilation *)
-  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
-    GeneratorPrem of term list * term | Generator of (string * typ);
- (* val prepare_intrs: theory -> string list ->
-    (string * typ) list * int * string list * string list * (string * mode list) list *
-    (string * (term list * indprem list) list) list * (string * (int option list * int)) list*)
   datatype compilation_funs = CompilationFuns of {
     mk_predT : typ -> typ,
     dest_predT : typ -> typ,
@@ -64,66 +51,39 @@
     mk_not : term -> term,
     mk_map : typ -> typ -> term -> term -> term,
     lift_pred : term -> term
-  };  
-  type moded_clause = term list * (indprem * tmode) list
-  type 'a pred_mode_table = (string * (mode * 'a) list) list
-  val infer_modes : theory -> (string * mode list) list
-    -> (string * mode list) list
-    -> string list
-    -> (string * (term list * indprem list) list) list
-    -> (moded_clause list) pred_mode_table
-  val infer_modes_with_generator : theory -> (string * mode list) list
-    -> (string * mode list) list
-    -> string list
-    -> (string * (term list * indprem list) list) list
-    -> (moded_clause list) pred_mode_table  
-  (*val compile_preds : theory -> compilation_funs -> string list -> string list
-    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table
-  val rpred_create_definitions :(string * typ) list -> string * mode list
-    -> theory -> theory 
-  val split_smode : int list -> term list -> (term list * term list) *)
-  val print_moded_clauses :
-    theory -> (moded_clause list) pred_mode_table -> unit
-  val print_compiled_terms : theory -> term pred_mode_table -> unit
-  (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)
+  };
   val pred_compfuns : compilation_funs
   val rpred_compfuns : compilation_funs
-  val dest_funT : typ -> typ * typ
- (* val depending_preds_of : theory -> thm list -> string list *)
-  val add_quickcheck_equations : string list -> theory -> theory
-  val add_sizelim_equations : string list -> theory -> theory
-  val is_inductive_predicate : theory -> string -> bool
-  val terms_vs : term list -> string list
-  val subsets : int -> int -> int list list
-  val check_mode_clause : bool -> theory -> string list ->
-    (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list)
-      -> (term list * (indprem * tmode) list) option
-  val string_of_moded_prem : theory -> (indprem * tmode) -> string
-  val all_modes_of : theory -> (string * mode list) list
-  val all_generator_modes_of : theory -> (string * mode list) list
-  val compile_clause : compilation_funs -> term option -> (term list -> term) ->
-    theory -> string list -> string list -> mode -> term -> moded_clause -> term
-  val preprocess_intro : theory -> thm -> thm
-  val is_constrt : theory -> term -> bool
-  val is_predT : typ -> bool
-  val guess_nparams : typ -> int
-  val cprods_subset : 'a list list -> 'a list list
+    (*  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  *)
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
 struct
 
 open Predicate_Compile_Aux;
+
 (** auxiliary **)
 
 (* debug stuff *)
 
-fun tracing s = (if ! Toplevel.debug then tracing s else ());
+fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+
+fun print_tac s = Seq.single;
+
+fun print_tac' options s = 
+  if show_proof_trace options then Tactical.print_tac s else Seq.single;
 
-fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
-fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
+fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
 
-val do_proofs = Unsynchronized.ref true;
+datatype assertion = Max_number_of_subgoals of int
+fun assert_tac (Max_number_of_subgoals i) st =
+  if (nprems_of st <= i) then Seq.single st
+  else error ("assert_tac: Numbers of subgoals mismatch at goal state :"
+    ^ "\n" ^ Pretty.string_of (Pretty.chunks
+      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
 
 (* reference to preprocessing of InductiveSet package *)
 
@@ -139,20 +99,6 @@
             HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
   in mk_eqs x xs end;
 
-fun mk_tupleT [] = HOLogic.unitT
-  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
-
-fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
-  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
-  | dest_tupleT t = [t]
-
-fun mk_tuple [] = HOLogic.unit
-  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
-
-fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
-  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
-  | dest_tuple t = [t]
-
 fun mk_scomp (t, u) =
   let
     val T = fastype_of t
@@ -189,6 +135,13 @@
 
 (** data structures **)
 
+(* new datatype for modes: *)
+(*
+datatype instantiation = Input | Output
+type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode
+type mode = arg_mode list
+type tmode = Mode of mode * 
+*)
 type smode = (int * int list option) list
 type mode = smode option list * smode;
 datatype tmode = Mode of mode * smode * tmode option list;
@@ -241,35 +194,8 @@
   (if null param_modes then "" else
     "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
 
-(* generation of case rules from user-given introduction rules *)
-
-fun mk_casesrule ctxt nparams introrules =
-  let
-    val ((_, intros_th), ctxt1) = Variable.import false introrules ctxt
-    val intros = map prop_of intros_th
-    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
-    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
-    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
-    val (argnames, ctxt3) = Variable.variant_fixes
-      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt2
-    val argvs = map2 (curry Free) argnames (map fastype_of args)
-    fun mk_case intro =
-      let
-        val (_, (_, args)) = strip_intro_concl nparams intro
-        val prems = Logic.strip_imp_prems intro
-        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
-        val frees = (fold o fold_aterms)
-          (fn t as Free _ =>
-              if member (op aconv) params t then I else insert (op aconv) t
-           | _ => I) (args @ prems) []
-      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
-    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
-    val cases = map mk_case intros
-  in Logic.list_implies (assm :: cases, prop) end;
-    
-
-datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
-  GeneratorPrem of term list * term | Generator of (string * typ);
+datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term
+  | Generator of (string * typ);
 
 type moded_clause = term list * (indprem * tmode) list
 type 'a pred_mode_table = (string * (mode * 'a) list) list
@@ -300,25 +226,25 @@
   nparams : int,
   functions : (mode * predfun_data) list,
   generators : (mode * function_data) list,
-  sizelim_functions : (mode * function_data) list 
+  depth_limited_functions : (mode * function_data) list 
 };
 
 fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim, nparams), (functions, generators, sizelim_functions)) =
+fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =
   PredData {intros = intros, elim = elim, nparams = nparams,
-    functions = functions, generators = generators, sizelim_functions = sizelim_functions}
-fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, sizelim_functions}) =
-  mk_pred_data (f ((intros, elim, nparams), (functions, generators, sizelim_functions)))
-  
+    functions = functions, generators = generators, depth_limited_functions = depth_limited_functions}
+fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, depth_limited_functions}) =
+  mk_pred_data (f ((intros, elim, nparams), (functions, generators, depth_limited_functions)))
+
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
   | eq_option eq _ = false
-  
+
 fun eq_pred_data (PredData d1, PredData d2) = 
   eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
   eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
   #nparams d1 = #nparams d2
-  
+
 structure PredData = TheoryDataFun
 (
   type T = pred_data Graph.T;
@@ -353,7 +279,7 @@
 
 val modes_of = (map fst) o #functions oo the_pred_data
 
-val sizelim_modes_of = (map fst) o #sizelim_functions oo the_pred_data
+val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data
 
 val rpred_modes_of = (map fst) o #generators oo the_pred_data
   
@@ -380,7 +306,7 @@
 fun lookup_generator_data thy name mode = 
   Option.map rep_function_data (AList.lookup (op =)
   (#generators (the_pred_data thy name)) mode)
-  
+
 fun the_generator_data thy name mode = case lookup_generator_data thy name mode
   of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
    | SOME data => data
@@ -392,24 +318,25 @@
 fun all_generator_modes_of thy =
   map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 
 
-fun lookup_sizelim_function_data thy name mode =
+fun lookup_depth_limited_function_data thy name mode =
   Option.map rep_function_data (AList.lookup (op =)
-  (#sizelim_functions (the_pred_data thy name)) mode)
+  (#depth_limited_functions (the_pred_data thy name)) mode)
 
-fun the_sizelim_function_data thy name mode = case lookup_sizelim_function_data thy name mode
-  of NONE => error ("No size-limited function defined for mode " ^ string_of_mode mode
+fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode
+  of NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode
     ^ " of predicate " ^ name)
    | SOME data => data
 
-val sizelim_function_name_of = #name ooo the_sizelim_function_data
+val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
 
 (*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
-     
+
 (* diagnostic display functions *)
 
-fun print_modes modes = tracing ("Inferred modes:\n" ^
-  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
-    string_of_mode ms)) modes));
+fun print_modes modes =
+  Output.tracing ("Inferred modes:\n" ^
+    cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+      string_of_mode ms)) modes));
 
 fun print_pred_mode_table string_of_entry thy pred_mode_table =
   let
@@ -417,15 +344,20 @@
       ^ (string_of_entry pred mode entry)  
     fun print_pred (pred, modes) =
       "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
-    val _ = tracing (cat_lines (map print_pred pred_mode_table))
+    val _ = Output.tracing (cat_lines (map print_pred pred_mode_table))
   in () end;
 
+fun string_of_prem thy (Prem (ts, p)) =
+    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)"
+  | string_of_prem thy (Negprem (ts, p)) =
+    (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)"
+  | string_of_prem thy (Sidecond t) =
+    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"
+  | string_of_prem thy _ = error "string_of_prem: unexpected input"
+
 fun string_of_moded_prem thy (Prem (ts, p), tmode) =
     (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
     "(" ^ (string_of_tmode tmode) ^ ")"
-  | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (predmode, is, _)) =
-    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
-    "(generator_mode: " ^ (string_of_mode predmode) ^ ")"
   | string_of_moded_prem thy (Generator (v, T), _) =
     "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
   | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
@@ -435,18 +367,25 @@
     (Syntax.string_of_term_global thy t) ^
     "(sidecond mode: " ^ string_of_smode is ^ ")"    
   | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
-     
+
 fun print_moded_clauses thy =
-  let        
+  let
     fun string_of_clause pred mode clauses =
       cat_lines (map (fn (ts, prems) => (space_implode " --> "
         (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
         ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
   in print_pred_mode_table string_of_clause thy end;
 
-fun print_compiled_terms thy =
-  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
-    
+fun string_of_clause thy pred (ts, prems) =
+  (space_implode " --> "
+  (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
+   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
+
+fun print_compiled_terms options thy =
+  if show_compilation options then
+    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
+  else K ()
+
 fun print_stored_rules thy =
   let
     val preds = (Graph.keys o PredData.get) thy
@@ -477,7 +416,105 @@
   in
     fold print (all_modes_of thy) ()
   end
-  
+
+(* validity checks *)
+
+fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =
+  case expected_modes options of
+    SOME (s, ms) => (case AList.lookup (op =) modes s of
+      SOME modes =>
+        if not (eq_set (op =) (map (map (rpair NONE)) ms, map snd modes)) then
+          error ("expected modes were not inferred:\n"
+          ^ "inferred modes for " ^ s ^ ": "
+          ^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes))
+        else ()
+      | NONE => ())
+  | NONE => ()
+
+(* importing introduction rules *)
+
+fun unify_consts thy cs intr_ts =
+  (let
+     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
+     fun varify (t, (i, ts)) =
+       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] t))
+       in (maxidx_of_term t', t'::ts) end;
+     val (i, cs') = List.foldr varify (~1, []) cs;
+     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
+     val rec_consts = fold add_term_consts_2 cs' [];
+     val intr_consts = fold add_term_consts_2 intr_ts' [];
+     fun unify (cname, cT) =
+       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
+       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+     val (env, _) = fold unify rec_consts (Vartab.empty, i');
+     val subst = map_types (Envir.norm_type env)
+   in (map subst cs', map subst intr_ts')
+   end) handle Type.TUNIFY =>
+     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+
+fun import_intros inp_pred nparams [] ctxt =
+  let
+    val ([outp_pred], ctxt') = Variable.import_terms false [inp_pred] ctxt
+    val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred))
+    val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i))
+      (1 upto nparams)) ctxt'
+    val params = map Free (param_names ~~ paramTs)
+    in (((outp_pred, params), []), ctxt') end
+  | import_intros inp_pred nparams (th :: ths) ctxt =
+    let
+      val ((_, [th']), ctxt') = Variable.import false [th] ctxt
+      val thy = ProofContext.theory_of ctxt'
+      val (pred, (params, args)) = strip_intro_concl nparams (prop_of th')
+      val ho_args = filter (is_predT o fastype_of) args
+      fun subst_of (pred', pred) =
+        let
+          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
+        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
+      fun instantiate_typ th =
+        let
+          val (pred', _) = strip_intro_concl 0 (prop_of th)
+          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+            error "Trying to instantiate another predicate" else ()
+        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
+      fun instantiate_ho_args th =
+        let
+          val (_, (params', args')) = strip_intro_concl nparams (prop_of th)
+          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')
+        in Thm.certify_instantiate ([], map dest_Var params' ~~ params) th end
+      val outp_pred =
+        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+      val ((_, ths'), ctxt1) =
+        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
+    in
+      (((outp_pred, params), th' :: ths'), ctxt1)
+    end
+
+(* generation of case rules from user-given introduction rules *)
+
+fun mk_casesrule ctxt pred nparams introrules =
+  let
+    val (((pred, params), intros_th), ctxt1) = import_intros pred nparams introrules ctxt
+    val intros = map prop_of intros_th
+    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
+    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
+    val (_, argsT) = chop nparams (binder_types (fastype_of pred))
+    val (argnames, ctxt3) = Variable.variant_fixes
+      (map (fn i => "a" ^ string_of_int i) (1 upto length argsT)) ctxt2
+    val argvs = map2 (curry Free) argnames argsT
+    fun mk_case intro =
+      let
+        val (_, (_, args)) = strip_intro_concl nparams intro
+        val prems = Logic.strip_imp_prems intro
+        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
+        val frees = (fold o fold_aterms)
+          (fn t as Free _ =>
+              if member (op aconv) params t then I else insert (op aconv) t
+           | _ => I) (args @ prems) []
+      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
+    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
+    val cases = map mk_case intros
+  in Logic.list_implies (assm :: cases, prop) end;
+
 (** preprocessing rules **)  
 
 fun imp_prems_conv cv ct =
@@ -498,39 +535,30 @@
 
 fun preprocess_elim thy nparams elimrule =
   let
-    val _ = tracing ("Preprocessing elimination rule "
-      ^ (Display.string_of_thm_global thy elimrule))
     fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
        HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
      | replace_eqs t = t
+    val ctxt = ProofContext.init thy
+    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
     val prems = Thm.prems_of elimrule
     val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams
     fun preprocess_case t =
-     let
+      let
        val params = Logic.strip_params t
        val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
        val assums_hyp' = assums1 @ (map replace_eqs assums2)
-     in
+      in
        list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
-     end
+      end
     val cases' = map preprocess_case (tl prems)
     val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
-    (*val _ =  tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
     val bigeq = (Thm.symmetric (Conv.implies_concl_conv
       (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
         (cterm_of thy elimrule')))
-    (*
-    val _ = tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))   
-    val res = 
-    Thm.equal_elim bigeq elimrule
-    *)
-    (*
-    val t = (fn {...} => mycheat_tac thy 1)
-    val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t
-    *)
-    val _ = tracing "Preprocessed elimination rule"
+    val tac = (fn _ => Skip_Proof.cheat_tac thy)    
+    val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
   in
-    Thm.equal_elim bigeq elimrule
+    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
   end;
 
 (* special case: predicate with no introduction rule *)
@@ -552,6 +580,8 @@
   ([intro], elim)
 end
 
+fun expand_tuples_elim th = th
+
 fun fetch_pred_data thy name =
   case try (Inductive.the_inductive (ProofContext.init thy)) name of
     SOME (info as (_, result)) => 
@@ -560,17 +590,23 @@
           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 ((map (preprocess_intro thy))
-          (filter is_intro_of (#intrs result)))
-        val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
+        val intros = ind_set_codegen_preproc thy
+          (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 pre_elim)
-        val (intros, elim) = if null intros then noclause thy name elim else (intros, elim)
+        (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams 
+          (expand_tuples_elim pre_elim))*)
+        val elim =
+          (Drule.standard o Skip_Proof.make_thm thy)
+          (mk_casesrule (ProofContext.init thy) pred nparams intros)
+        val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim)
       in
         mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
       end                                                                    
   | NONE => error ("No such predicate: " ^ quote name)
-  
+
 (* updaters *)
 
 fun apfst3 f (x, y, z) =  (f x, y, z)
@@ -605,6 +641,7 @@
     (data, keys)
   end;
 *)
+
 (* guessing number of parameters *)
 fun find_indexes pred xs =
   let
@@ -624,7 +661,7 @@
    fun cons_intro gr =
      case try (Graph.get_node gr) name of
        SOME pred_data => Graph.map_node name (map_pred_data
-         (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr
+         (apfst (fn (intros, elim, nparams) => (thm::intros, elim, nparams)))) gr
      | NONE =>
        let
          val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
@@ -640,30 +677,34 @@
 fun set_nparams name nparams = let
     fun set (intros, elim, _ ) = (intros, elim, nparams) 
   in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
-    
-fun register_predicate (pre_intros, pre_elim, nparams) thy =
+
+fun register_predicate (constname, pre_intros, pre_elim, nparams) thy =
   let
-    val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))
     (* 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)
   in
-    if not (member (op =) (Graph.keys (PredData.get thy)) name) then
+    if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
-        (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
+        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
     else thy
   end
 
-fun register_intros pre_intros thy =
+fun register_intros (constname, pre_intros) thy =
   let
-    val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
-    val _ = tracing ("Registering introduction rules of " ^ c)
-    val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
+    val T = Sign.the_const_type thy constname
+    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 = constname) pre_intros) then
+      error ("register_intros: Introduction rules of different constants are used\n" ^
+        "expected rules for " ^ constname ^ ", but received rules for " ^
+          commas (map constname_of_intro pre_intros))
+      else ()
+    val pred = Const (constname, T)
     val nparams = guess_nparams T
     val pre_elim = 
       (Drule.standard o Skip_Proof.make_thm thy)
-      (mk_casesrule (ProofContext.init thy) nparams pre_intros)
-  in register_predicate (pre_intros, pre_elim, nparams) thy end
+      (mk_casesrule (ProofContext.init thy) pred nparams pre_intros)
+  in register_predicate (constname, pre_intros, pre_elim, nparams) thy end
 
 fun set_generator_name pred mode name = 
   let
@@ -672,7 +713,7 @@
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
-fun set_sizelim_function_name pred mode name = 
+fun set_depth_limited_function_name pred mode name = 
   let
     val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
   in
@@ -694,8 +735,6 @@
   mk_sup : term * term -> term,
   mk_if : term -> term,
   mk_not : term -> term,
-(*  funT_of : mode -> typ -> typ, *)
-(*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 
   mk_map : typ -> typ -> term -> term -> term,
   lift_pred : term -> term
 };
@@ -708,8 +747,6 @@
 fun mk_sup (CompilationFuns funs) = #mk_sup funs
 fun mk_if (CompilationFuns funs) = #mk_if funs
 fun mk_not (CompilationFuns funs) = #mk_not funs
-(*fun funT_of (CompilationFuns funs) = #funT_of funs*)
-(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
 fun mk_map (CompilationFuns funs) = #mk_map funs
 fun lift_pred (CompilationFuns funs) = #lift_pred funs
 
@@ -719,7 +756,7 @@
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
     val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
   in
-    (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
+    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   end;
 
 fun mk_fun_of compfuns thy (name, T) mode = 
@@ -809,9 +846,11 @@
 fun mk_if cond = Const (@{const_name RPred.if_rpred},
   HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
 
-fun mk_not t = error "Negation is not defined for RPred"
+fun mk_not t = let val T = mk_rpredT HOLogic.unitT
+  in Const (@{const_name RPred.not_rpred}, T --> T) $ t end
 
-fun mk_map t = error "FIXME" (*FIXME*)
+fun mk_map T1 T2 tf tp = Const (@{const_name RPred.map},
+  (T1 --> T2) --> mk_rpredT T1 --> mk_rpredT T2) $ tf $ tp
 
 fun lift_pred t =
   let
@@ -839,20 +878,21 @@
       RPredCompFuns.mk_rpredT T) $ random
   end;
 
-fun sizelim_funT_of compfuns (iss, is) T =
+fun depth_limited_funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
+    val paramTs' = map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs 
   in
-    (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
+    (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])
+      ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   end;  
 
-fun mk_sizelim_fun_of compfuns thy (name, T) mode =
-  Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T)
+fun mk_depth_limited_fun_of compfuns thy (name, T) mode =
+  Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
   
 fun mk_generator_of compfuns thy (name, T) mode = 
-  Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T)
+  Const (generator_name_of thy name mode, depth_limited_funT_of compfuns mode T)
 
 (* Mode analysis *)
 
@@ -882,16 +922,16 @@
 fun term_vTs tm =
   fold_aterms (fn Free xT => cons xT | _ => I) tm [];
 
-(*FIXME this function should not be named merge... make it local instead*)
-fun merge xs [] = xs
-  | merge [] ys = ys
-  | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
-      else y::merge (x::xs) ys;
-
-fun subsets i j = if i <= j then
-       let val is = subsets (i+1) j
-       in merge (map (fn ks => i::ks) is) is end
-     else [[]];
+fun subsets i j =
+  if i <= j then
+    let
+      fun merge xs [] = xs
+        | merge [] ys = ys
+        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
+            else y::merge (x::xs) ys;
+      val is = subsets (i+1) j
+    in merge (map (fn ks => i::ks) is) is end
+  else [[]];
      
 (* FIXME: should be in library - cprod = map_prod I *)
 fun cprod ([], ys) = []
@@ -905,46 +945,9 @@
     val yss = (cprods_subset xss)
   in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end
   
-(*TODO: cleanup function and put together with modes_of_term *)
-(*
-fun modes_of_param default modes t = let
-    val (vs, t') = strip_abs t
-    val b = length vs
-    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
-        let
-          val (args1, args2) =
-            if length args < length iss then
-              error ("Too few arguments for inductive predicate " ^ name)
-            else chop (length iss) args;
-          val k = length args2;
-          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
-            (1 upto b)  
-          val partial_mode = (1 upto k) \\ perm
-        in
-          if not (partial_mode subset is) then [] else
-          let
-            val is' = 
-            (fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm [])
-            |> fold (fn i => if i > k then cons (i - k + b) else I) is
-              
-           val res = map (fn x => Mode (m, is', x)) (cprods (map
-            (fn (NONE, _) => [NONE]
-              | (SOME js, arg) => map SOME (filter
-                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
-                    (iss ~~ args1)))
-          in res end
-        end)) (AList.lookup op = modes name)
-  in case strip_comb t' of
-    (Const (name, _), args) => the_default default (mk_modes name args)
-    | (Var ((name, _), _), args) => the (mk_modes name args)
-    | (Free (name, _), args) => the (mk_modes name args)
-    | _ => default end
-  
-and
-*)
 fun modes_of_term modes t =
   let
-    val ks = map_index (fn (i, T) => (i, NONE)) (binder_types (fastype_of t));
+    val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t));
     val default = [Mode (([], ks), ks, [])];
     fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
         let
@@ -956,7 +959,7 @@
           val prfx = map (rpair NONE) (1 upto k)
         in
           if not (is_prefix op = prfx is) then [] else
-          let val is' = List.drop (is, k)
+          let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k))
           in map (fn x => Mode (m, is', x)) (cprods (map
             (fn (NONE, _) => [NONE]
               | (SOME js, arg) => map SOME (filter
@@ -992,7 +995,7 @@
             (modes_of_term modes t handle Option =>
                error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
       | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
-            length us = length is andalso
+            is = map (rpair NONE) (1 upto length us) andalso
             subset (op =) (terms_vs us, vs) andalso
             subset (op =) (term_vs t, vs))
             (modes_of_term modes t handle Option =>
@@ -1015,24 +1018,8 @@
     (Generator (v, T), Mode (([], []), [], []))
   end;
 
-fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t)
-  | gen_prem (Negprem (us, t)) = error "it is a negated prem"
-  | gen_prem (Sidecond t) = error "it is a sidecond"
-  | gen_prem _ = error "gen_prem : invalid input for gen_prem"
-
-fun param_gen_prem param_vs (p as Prem (us, t as Free (v, _))) =
-  if member (op =) param_vs v then
-    GeneratorPrem (us, t)
-  else p  
-  | param_gen_prem param_vs p = p
-  
 fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
   let
-    (*
-  val _ = tracing ("param_vs:" ^ commas param_vs)
-  val _ = tracing ("iss:" ^
-    commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
-    *)
     val modes' = modes @ map_filter
       (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
         (param_vs ~~ iss);
@@ -1046,7 +1033,7 @@
           NONE =>
             (if with_generator then
               (case select_mode_prem thy gen_modes' vs ps of
-                SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
+                SOME (p as Prem _, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
                   (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
                   (filter_out (equal p) ps)
               | _ =>
@@ -1057,14 +1044,11 @@
                       (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
                       SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
                         (union (op =) vs generator_vs) ps
-                    | NONE => let
-                    val _ = tracing ("ps:" ^ (commas
-                    (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
-                  in (*error "mode analysis failed"*)NONE end
+                    | NONE => NONE
                   end)
             else
               NONE)
-        | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
+        | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
             (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
             (filter_out (equal p) ps))
     val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
@@ -1083,33 +1067,41 @@
     else NONE
   end;
 
-fun check_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
-  let val SOME rs = AList.lookup (op =) clauses p
+fun print_failed_mode options thy modes p m rs i =
+  if show_mode_inference options then
+    let
+      val _ = Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
+      p ^ " violates mode " ^ string_of_mode m)
+      val _ = Output.tracing (string_of_clause thy p (nth rs i))
+    in () end
+  else ()
+
+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, List.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 => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
-      p ^ " violates mode " ^ string_of_mode m);
-        tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
+    | i => (print_failed_mode options thy modes p m rs i; false)) ms)
   end;
 
 fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
   let
-    val SOME rs = AList.lookup (op =) clauses p 
+    val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
   in
     (p, map (fn m =>
       (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
   end;
-  
+
 fun fixp f (x : (string * mode list) list) =
   let val y = f x
   in if x = y then x else fixp f y end;
 
-fun infer_modes thy extra_modes all_modes param_vs clauses =
+fun infer_modes options thy extra_modes all_modes param_vs clauses =
   let
     val modes =
       fixp (fn modes =>
-        map (check_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes)
+        map (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes)
           all_modes
   in
     map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes
@@ -1122,19 +1114,24 @@
     | SOME vs' => (k, subtract (op =) vs' vs))
     :: remove_from rem xs
     
-fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses =
+fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses =
   let
     val prednames = map fst clauses
-    val extra_modes = all_modes_of thy
+    val extra_modes' = all_modes_of thy
     val gen_modes = all_generator_modes_of thy
       |> filter_out (fn (name, _) => member (op =) prednames name)
-    val starting_modes = remove_from extra_modes all_modes 
+    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 true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
-         starting_modes 
+        map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes)
+         starting_modes
   in
-    map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
+    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)
   end;
 
 (* term construction *)
@@ -1157,136 +1154,10 @@
       in (t' $ u', nvs'') end
   | distinct_v x nvs = (x, nvs);
 
-fun compile_match thy compfuns eqs eqs' out_ts success_t =
-  let
-    val eqs'' = maps mk_eq eqs @ eqs'
-    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
-    val name = Name.variant names "x";
-    val name' = Name.variant (name :: names) "y";
-    val T = mk_tupleT (map fastype_of out_ts);
-    val U = fastype_of success_t;
-    val U' = dest_predT compfuns U;
-    val v = Free (name, T);
-    val v' = Free (name', T);
-  in
-    lambda v (fst (Datatype.make_case
-      (ProofContext.init thy) DatatypeCase.Quiet [] v
-      [(mk_tuple out_ts,
-        if null eqs'' then success_t
-        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
-          foldr1 HOLogic.mk_conj eqs'' $ success_t $
-            mk_bot compfuns U'),
-       (v', mk_bot compfuns U')]))
-  end;
-
-(*FIXME function can be removed*)
-fun mk_funcomp f t =
-  let
-    val names = Term.add_free_names t [];
-    val Ts = binder_types (fastype_of t);
-    val vs = map Free
-      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
-  in
-    fold_rev lambda vs (f (list_comb (t, vs)))
-  end;
-(*
-fun compile_param_ext thy compfuns modes (NONE, t) = t
-  | compile_param_ext thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
-      let
-        val (vs, u) = strip_abs t
-        val (ivs, ovs) = split_mode is vs    
-        val (f, args) = strip_comb u
-        val (params, args') = chop (length ms) args
-        val (inargs, outargs) = split_mode is' args'
-        val b = length vs
-        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
-        val outp_perm =
-          snd (split_mode is perm)
-          |> map (fn i => i - length (filter (fn x => x < i) is'))
-        val names = [] -- TODO
-        val out_names = Name.variant_list names (replicate (length outargs) "x")
-        val f' = case f of
-            Const (name, T) =>
-              if AList.defined op = modes name then
-                mk_predfun_of thy compfuns (name, T) (iss, is')
-              else error "compile param: Not an inductive predicate with correct mode"
-          | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is'))
-        val outTs = dest_tupleT (dest_predT compfuns (body_type (fastype_of f')))
-        val out_vs = map Free (out_names ~~ outTs)
-        val params' = map (compile_param thy modes) (ms ~~ params)
-        val f_app = list_comb (f', params' @ inargs)
-        val single_t = (mk_single compfuns (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
-        val match_t = compile_match thy compfuns [] [] out_vs single_t
-      in list_abs (ivs,
-        mk_bind compfuns (f_app, match_t))
-      end
-  | compile_param_ext _ _ _ _ = error "compile params"
-*)
-
-fun compile_param neg_in_sizelim size thy compfuns (NONE, t) = t
-  | compile_param neg_in_sizelim size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
-   let
-     val (f, args) = strip_comb (Envir.eta_contract t)
-     val (params, args') = chop (length ms) args
-     val params' = map (compile_param neg_in_sizelim size thy compfuns) (ms ~~ params)
-     val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
-     val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
-     val f' =
-       case f of
-         Const (name, T) =>
-           mk_fun_of compfuns thy (name, T) (iss, is')
-       | Free (name, T) =>
-         case neg_in_sizelim of
-           SOME _ =>  Free (name, sizelim_funT_of compfuns (iss, is') T)
-         | NONE => Free (name, funT_of compfuns (iss, is') T)
-           
-       | _ => error ("PredicateCompiler: illegal parameter term")
-   in
-     (case neg_in_sizelim of SOME size_t =>
-       (fn t =>
-       let
-         val Ts = fst (split_last (binder_types (fastype_of t)))
-         val names = map (fn i => "x" ^ string_of_int i) (1 upto length Ts)
-       in
-         list_abs (names ~~ Ts, list_comb (t, (map Bound ((length Ts) - 1 downto 0)) @ [size_t]))
-       end)
-     | NONE => I)
-     (list_comb (f', params' @ args'))
-   end
-
-fun compile_expr neg_in_sizelim size thy ((Mode (mode, is, ms)), t) =
-  case strip_comb t of
-    (Const (name, T), params) =>
-       let
-         val params' = map (compile_param neg_in_sizelim size thy PredicateCompFuns.compfuns) (ms ~~ params)
-         val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
-       in
-         list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
-       end
-  | (Free (name, T), args) =>
-       let 
-         val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of 
-       in
-         list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args)
-       end;
-       
-fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) inargs =
-  case strip_comb t of
-    (Const (name, T), params) =>
-      let
-        val params' = map (compile_param NONE size thy PredicateCompFuns.compfuns) (ms ~~ params)
-      in
-        list_comb (mk_generator_of compfuns thy (name, T) mode, params' @ inargs)
-      end
-    | (Free (name, T), params) =>
-    lift_pred compfuns
-    (list_comb (Free (name, sizelim_funT_of PredicateCompFuns.compfuns ([], is) T), params @ inargs))
-      
-          
 (** specific rpred functions -- move them to the correct place in this file *)
 
-fun mk_Eval_of size ((x, T), NONE) names = (x, names)
-  | mk_Eval_of size ((x, T), SOME mode) names =
+fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
+  | mk_Eval_of additional_arguments ((x, T), SOME mode) names =
 	let
     val Ts = binder_types T
     (*val argnames = Name.variant_list names
@@ -1331,32 +1202,99 @@
 			end
 		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
     val (inargs, outargs) = pairself flat (split_list inoutargs)
-    val size_t = case size of NONE => [] | SOME size_t => [size_t]
-		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs)
+		val r = PredicateCompFuns.mk_Eval 
+      (list_comb (x, inargs @ additional_arguments), HOLogic.mk_tuple outargs)
     val t = fold_rev mk_split_lambda args r
   in
     (t, names)
   end;
 
-fun compile_arg size thy param_vs iss arg = 
+fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg = 
   let
-    val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
     fun map_params (t as Free (f, T)) =
       if member (op =) param_vs f then
         case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of
-          SOME is => let val T' = funT_of PredicateCompFuns.compfuns ([], is) T
-            in fst (mk_Eval_of size ((Free (f, T'), T), SOME is) []) end
+          SOME is =>
+            let
+              val T' = #funT_of compilation_modifiers compfuns ([], is) T
+            in fst (mk_Eval_of additional_arguments ((Free (f, T'), T), SOME is) []) end
         | NONE => t
       else t
       | map_params t = t
     in map_aterms map_params arg end
-  
-fun compile_clause compfuns size final_term thy all_vs param_vs (iss, is) inp (ts, moded_ps) =
+
+fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t =
+  let
+    val eqs'' = maps mk_eq eqs @ eqs'
+    val eqs'' =
+      map (compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss) eqs''
+    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
+    val name = Name.variant names "x";
+    val name' = Name.variant (name :: names) "y";
+    val T = HOLogic.mk_tupleT (map fastype_of out_ts);
+    val U = fastype_of success_t;
+    val U' = dest_predT compfuns U;
+    val v = Free (name, T);
+    val v' = Free (name', T);
+  in
+    lambda v (fst (Datatype.make_case
+      (ProofContext.init thy) DatatypeCase.Quiet [] v
+      [(HOLogic.mk_tuple out_ts,
+        if null eqs'' then success_t
+        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
+          foldr1 HOLogic.mk_conj eqs'' $ success_t $
+            mk_bot compfuns U'),
+       (v', mk_bot compfuns U')]))
+  end;
+
+(*FIXME function can be removed*)
+fun mk_funcomp f t =
   let
+    val names = Term.add_free_names t [];
+    val Ts = binder_types (fastype_of t);
+    val vs = map Free
+      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
+  in
+    fold_rev lambda vs (f (list_comb (t, vs)))
+  end;
+
+fun compile_param compilation_modifiers compfuns thy (NONE, t) = t
+  | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) =
+   let
+     val (f, args) = strip_comb (Envir.eta_contract t)
+     val (params, args') = chop (length ms) args
+     val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+     val f' =
+       case f of
+         Const (name, T) => Const (#const_name_of compilation_modifiers thy name mode,
+           #funT_of compilation_modifiers compfuns mode T)
+       | Free (name, T) => Free (name, #funT_of compilation_modifiers compfuns mode T)
+       | _ => error ("PredicateCompiler: illegal parameter term")
+   in
+     list_comb (f', params' @ args')
+   end
+
+fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments =
+  case strip_comb t of
+    (Const (name, T), params) =>
+       let
+         val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+           (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*)
+         val name' = #const_name_of compilation_modifiers thy name mode
+         val T' = #funT_of compilation_modifiers compfuns mode T
+       in
+         (list_comb (Const (name', T'), params' @ inargs @ additional_arguments))
+       end
+  | (Free (name, T), params) =>
+    list_comb (Free (name, #funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments)
+
+fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) =
+  let
+    val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy
     fun check_constrt t (names, eqs) =
       if is_constrt thy t then (t, (names, eqs)) else
         let
-          val s = Name.variant names "x";
+          val s = Name.variant names "x"
           val v = Free (s, fastype_of t)
         in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
 
@@ -1371,12 +1309,8 @@
             val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
               out_ts'' (names', map (rpair []) vs);
           in
-          (* termify code:
-            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
-              (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts)))
-           *)
-            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
-              (final_term out_ts)
+            compile_match constr_vs (eqs @ eqs') out_ts'''
+              (mk_single compfuns (HOLogic.mk_tuple out_ts))
           end
       | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) =
           let
@@ -1385,16 +1319,16 @@
               fold_map check_constrt out_ts (names, [])
             val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
               out_ts' ((names', map (rpair []) vs))
+            val additional_arguments' =
+              #transform_additional_arguments compilation_modifiers p additional_arguments
             val (compiled_clause, rest) = case p of
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us;
-                   val in_ts = map (compile_arg size thy param_vs iss) in_ts
-                   val args = case size of
-                     NONE => in_ts
-                   | SOME size_t => in_ts @ [size_t]
-                   val u = lift_pred compfuns
-                     (list_comb (compile_expr NONE size thy (mode, t), args))                     
+                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss) in_ts
+                   val u =
+                     compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments'
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1402,38 +1336,32 @@
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us
-                   val u = lift_pred compfuns
-                     (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr size NONE thy (mode, t), in_ts)))
+                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss) in_ts
+                   val u = mk_not compfuns
+                     (compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments')
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Sidecond t =>
                  let
+                   val t = compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss t
                    val rest = compile_prems [] vs' names'' ps;
                  in
                    (mk_if compfuns t, rest)
                  end
-             | GeneratorPrem (us, t) =>
-                 let
-                   val (in_ts, out_ts''') = split_smode is us;
-                   val args = case size of
-                     NONE => in_ts
-                   | SOME size_t => in_ts @ [size_t]
-                   val u = compile_gen_expr size thy compfuns (mode, t) args
-                   val rest = compile_prems out_ts''' vs' names'' ps
-                 in
-                   (u, rest)
-                 end
              | Generator (v, T) =>
                  let
-                   val u = lift_random (HOLogic.mk_random T (the size))
+                   val [size] = additional_arguments
+                   val u = lift_random (HOLogic.mk_random T size)
                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
                  in
                    (u, rest)
                  end
           in
-            compile_match thy compfuns constr_vs' eqs out_ts'' 
+            compile_match constr_vs' eqs out_ts''
               (mk_bind compfuns (compiled_clause, rest))
           end
     val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps;
@@ -1441,14 +1369,13 @@
     mk_bind compfuns (mk_single compfuns inp, prem_t)
   end
 
-fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
+fun compile_pred compilation_modifiers compfuns thy all_vs param_vs s T mode moded_cls =
   let
 	  val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
     val (Us1, Us2) = split_smodeT (snd mode) Ts2
-    val funT_of = if use_size then sizelim_funT_of else funT_of
-    val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1
-    val size_name = Name.variant (all_vs @ param_vs) "size"
-  	fun mk_input_term (i, NONE) =
+    val Ts1' =
+      map2 (fn NONE => I | SOME is => #funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
+    fun mk_input_term (i, NONE) =
 		    [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
 		  | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of
 						   [] => error "strange unit input"
@@ -1461,30 +1388,22 @@
 						   else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end
 		val in_ts = maps mk_input_term (snd mode)
     val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
-    val size = Free (size_name, @{typ "code_numeral"})
-    val decr_size =
-      if use_size then
-        SOME (Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
-          $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}))
-      else
-        NONE
+    val additional_arguments = #additional_arguments compilation_modifiers (all_vs @ param_vs)
     val cl_ts =
-      map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts))
-        thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls;
-    val t = foldr1 (mk_sup compfuns) cl_ts
-    val T' = mk_predT compfuns (mk_tupleT Us2)
-    val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
-      $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"})
-      $ mk_bot compfuns (dest_predT compfuns T') $ t
-    val fun_const = mk_fun_of compfuns thy (s, T) mode
-    val eq = if use_size then
-      (list_comb (fun_const, params @ in_ts @ [size]), size_t)
-    else
-      (list_comb (fun_const, params @ in_ts), t)
+      map (compile_clause compilation_modifiers compfuns
+        thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls;
+    val compilation = #wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
+      (if null cl_ts then
+        mk_bot compfuns (HOLogic.mk_tupleT Us2)
+      else foldr1 (mk_sup compfuns) cl_ts)
+    val fun_const =
+      Const (#const_name_of compilation_modifiers thy s mode,
+        #funT_of compilation_modifiers compfuns mode T)
   in
-    HOLogic.mk_Trueprop (HOLogic.mk_eq eq)
+    HOLogic.mk_Trueprop
+      (HOLogic.mk_eq (list_comb (fun_const, params @ in_ts @ additional_arguments), compilation))
   end;
-  
+
 (* special setup for simpset *)                  
 val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
   setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
@@ -1531,15 +1450,15 @@
   val param_names' = Name.variant_list (param_names @ argnames)
     (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
   val param_vs = map Free (param_names' ~~ Ts1)
-  val (params', names) = fold_map (mk_Eval_of NONE) ((params ~~ Ts1) ~~ iss) []
+  val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) []
   val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args))
   val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args))
   val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
   val funargs = params @ inargs
   val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
-                  if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
+                  if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
   val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
-                   mk_tuple outargs))
+                   HOLogic.mk_tuple outargs))
   val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
   val simprules = [defthm, @{thm eval_pred},
 	  @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
@@ -1601,7 +1520,7 @@
       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 (mk_tupleT Us2))
+      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)));
 			(* old *)
@@ -1634,7 +1553,7 @@
    	  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 NONE) ((xparams ~~ Ts1) ~~ iss) names
+			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 =
@@ -1663,16 +1582,16 @@
     fold create_definition modes thy
   end;
 
-fun sizelim_create_definitions preds (name, modes) thy =
+fun create_definitions_of_depth_limited_functions preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
-        val mode_cname = create_constname_of_mode thy "sizelim_" name mode
-        val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T
+        val mode_cname = create_constname_of_mode thy "depth_limited_" name mode
+        val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_sizelim_function_name name mode mode_cname 
+        |> set_depth_limited_function_name name mode mode_cname 
       end;
   in
     fold create_definition modes thy
@@ -1682,9 +1601,10 @@
   let
     val Ts = binder_types T
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => sizelim_funT_of PredicateCompFuns.compfuns ([], is) | NONE => I) iss paramTs 
+    val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs
   in
-    (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT RPredCompFuns.compfuns (mk_tupleT outargTs))
+    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
+      (mk_predT RPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
   end
 
 fun rpred_create_definitions preds (name, modes) thy =
@@ -1696,7 +1616,7 @@
         val funT = generator_funT_of mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_generator_name name mode mode_cname 
+        |> set_generator_name name mode mode_cname
       end;
   in
     fold create_definition modes thy
@@ -1818,7 +1738,7 @@
     (* need better control here! *)
   end
 
-fun prove_clause thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) =
+fun prove_clause options thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) =
   let
     val (in_ts, clause_out_ts) = split_smode is ts;
     fun prove_prems out_ts [] =
@@ -1874,7 +1794,8 @@
       end;
     val prems_tac = prove_prems in_ts moded_ps
   in
-    rtac @{thm bindI} 1
+    print_tac' options "Proving clause..."
+    THEN rtac @{thm bindI} 1
     THEN rtac @{thm singleI} 1
     THEN prems_tac
   end;
@@ -1883,20 +1804,20 @@
   | select_sup _ 1 = [rtac @{thm supI1}]
   | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
 
-fun prove_one_direction thy clauses preds modes pred mode moded_clauses =
+fun prove_one_direction options thy clauses preds modes pred mode moded_clauses =
   let
     val T = the (AList.lookup (op =) preds pred)
     val nargs = length (binder_types T) - nparams_of thy pred
     val pred_case_rule = the_elim_of thy pred
   in
     REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
-		THEN print_tac "before applying elim rule"
+		THEN print_tac' options "before applying elim rule"
     THEN etac (predfun_elim_of thy pred mode) 1
     THEN etac pred_case_rule 1
     THEN (EVERY (map
            (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
              (1 upto (length moded_clauses))))
-    THEN (EVERY (map2 (prove_clause thy nargs modes mode) clauses moded_clauses))
+    THEN (EVERY (map2 (prove_clause options thy nargs modes mode) clauses moded_clauses))
     THEN print_tac "proved one direction"
   end;
 
@@ -1914,15 +1835,20 @@
           | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
         val (_, ts) = strip_comb t
       in
-        (Splitter.split_asm_tac split_rules 1)
-(*        THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
-          THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
-        THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
+        (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ 
+          "splitting with rules \n" ^
+        commas (map (Display.string_of_thm_global thy) split_rules)))
+        THEN TRY ((Splitter.split_asm_tac split_rules 1)
+        THEN (print_tac "after splitting with split_asm rules")
+        (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
+          THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
+          THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
+        THEN (assert_tac (Max_number_of_subgoals 2))
         THEN (EVERY (map split_term_tac ts))
       end
     else all_tac
   in
-    split_term_tac (mk_tuple out_ts)
+    split_term_tac (HOLogic.mk_tuple out_ts)
     THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
   end
 
@@ -2053,7 +1979,7 @@
     THEN prems_tac
   end;
  
-fun prove_other_direction thy modes pred mode moded_clauses =
+fun prove_other_direction options thy modes pred mode moded_clauses =
   let
     fun prove_clause clause i =
       (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
@@ -2063,26 +1989,28 @@
      THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
      THEN (rtac (predfun_intro_of thy pred mode) 1)
      THEN (REPEAT_DETERM (rtac @{thm refl} 2))
-     THEN (EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
+     THEN (if null moded_clauses then
+         etac @{thm botE} 1
+       else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
   end;
 
 (** proof procedure **)
 
-fun prove_pred thy clauses preds modes pred mode (moded_clauses, compiled_term) =
+fun prove_pred options thy clauses preds modes pred mode (moded_clauses, compiled_term) =
   let
     val ctxt = ProofContext.init thy
-    val clauses = the (AList.lookup (op =) clauses pred)
+    val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
   in
     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
-      (if !do_proofs then
+      (if not (skip_proof options) then
         (fn _ =>
         rtac @{thm pred_iffI} 1
-        THEN print_tac "after pred_iffI"
-        THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
-        THEN print_tac "proved one direction"
-        THEN prove_other_direction thy modes pred mode moded_clauses
-        THEN print_tac "proved other direction")
-      else fn _ => Skip_Proof.cheat_tac thy)
+				THEN print_tac' options "after pred_iffI"
+        THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses
+        THEN print_tac' options "proved one direction"
+        THEN prove_other_direction options thy modes pred mode moded_clauses
+        THEN print_tac' options "proved other direction")
+      else (fn _ => Skip_Proof.cheat_tac thy))
   end;
 
 (* composition of mode inference, definition, compilation and proof *)
@@ -2101,48 +2029,57 @@
   map (fn (pred, modes) =>
     (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
     
-fun compile_preds compfuns mk_fun_of use_size thy all_vs param_vs preds moded_clauses =
-  map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred
-      (the (AList.lookup (op =) preds pred))) moded_clauses  
-  
-fun prove thy clauses preds modes moded_clauses compiled_terms =
-  map_preds_modes (prove_pred thy clauses preds modes)
+fun compile_preds comp_modifiers compfuns thy all_vs param_vs preds moded_clauses =
+  map_preds_modes (fn pred => compile_pred comp_modifiers compfuns thy all_vs param_vs pred
+      (the (AList.lookup (op =) preds pred))) moded_clauses
+
+fun prove options thy clauses preds modes moded_clauses compiled_terms =
+  map_preds_modes (prove_pred options thy clauses preds modes)
     (join_preds_modes moded_clauses compiled_terms)
 
-fun prove_by_skip thy _ _ _ _ compiled_terms =
+fun prove_by_skip options thy _ _ _ _ compiled_terms =
   map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
     compiled_terms
+
+fun dest_prem thy params t =
+  (case strip_comb t of
+    (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
+  | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of          
+      Prem (ts, t) => Negprem (ts, t)
+    | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
+    | Sidecond t => Sidecond (c $ t))
+  | (c as Const (s, _), ts) =>
+    if is_registered thy s then
+      let val (ts1, ts2) = chop (nparams_of thy s) ts
+      in Prem (ts2, list_comb (c, ts1)) end
+    else Sidecond t
+  | _ => Sidecond t)
     
-fun prepare_intrs thy prednames =
+fun prepare_intrs thy prednames intros =
   let
-    val intrs = maps (intros_of thy) prednames
-      |> map (Logic.unvarify o prop_of)
+    val intrs = map prop_of intros
     val nparams = nparams_of thy (hd prednames)
+    val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
+    val (preds, intrs) = unify_consts thy preds intrs
+    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] (ProofContext.init thy)
+    val preds = map dest_Const preds
     val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
-    val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
-    val _ $ u = Logic.strip_imp_concl (hd intrs);
-    val params = List.take (snd (strip_comb u), nparams);
+    val params = case intrs of
+        [] =>
+          let
+            val (paramTs, _) = chop nparams (binder_types (snd (hd preds)))
+            val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs))
+          in map Free (param_names ~~ paramTs) end
+      | intr :: _ => fst (chop nparams
+        (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)))))
     val param_vs = maps term_vs params
     val all_vs = terms_vs intrs
-    fun dest_prem t =
-      (case strip_comb t of
-        (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
-      | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of          
-          Prem (ts, t) => Negprem (ts, t)
-        | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
-        | Sidecond t => Sidecond (c $ t))
-      | (c as Const (s, _), ts) =>
-        if is_registered thy s then
-          let val (ts1, ts2) = chop (nparams_of thy s) ts
-          in Prem (ts2, list_comb (c, ts1)) end
-        else Sidecond t
-      | _ => Sidecond t)
     fun add_clause intr (clauses, arities) =
     let
       val _ $ t = Logic.strip_imp_concl intr;
       val (Const (name, T), ts) = strip_comb t;
       val (ts1, ts2) = chop nparams ts;
-      val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
+      val prems = map (dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
       val (Ts, Us) = chop nparams (binder_types T)
     in
       (AList.update op = (name, these (AList.lookup op = clauses name) @
@@ -2177,31 +2114,74 @@
     val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
   in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
 
+fun check_format_of_intro_rule thy intro =
+  let
+    val concl = Logic.strip_imp_concl (prop_of intro)
+    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
+    val params = List.take (args, nparams_of thy (fst (dest_Const p)))
+    fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
+      (Ts as _ :: _ :: _) =>
+        if (length (HOLogic.strip_tuple arg) = length Ts) then true
+        else
+        error ("Format of introduction rule is invalid: tuples must be expanded:"
+        ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
+        (Display.string_of_thm_global thy intro)) 
+      | _ => true
+    val prems = Logic.strip_imp_prems (prop_of intro)
+    fun check_prem (Prem (args, _)) = forall check_arg args
+      | check_prem (Negprem (args, _)) = forall check_arg args
+      | check_prem _ = true
+  in
+    forall check_arg args andalso
+    forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
+  end
+
+(*
+fun check_intros_elim_match thy prednames =
+  let
+    fun check predname =
+      let
+        val intros = intros_of thy predname
+        val elim = the_elim_of thy predname
+        val nparams = nparams_of thy predname
+        val elim' =
+          (Drule.standard o (Skip_Proof.make_thm thy))
+          (mk_casesrule (ProofContext.init thy) nparams intros)
+      in
+        if not (Thm.equiv_thm (elim, elim')) then
+          error "Introduction and elimination rules do not match!"
+        else true
+      end
+  in forall check prednames end
+*)
+
 (** main function of predicate compiler **)
 
-fun add_equations_of steps prednames thy =
+fun add_equations_of steps options prednames thy =
   let
-    val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+    val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
     val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+      (*val _ = check_intros_elim_match thy prednames*)
+      (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
-      prepare_intrs thy prednames
-    val _ = tracing "Infering modes..."
-    val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
+      prepare_intrs thy prednames (maps (intros_of thy) prednames)
+    val _ = print_step options "Infering modes..."
+    val moded_clauses = #infer_modes 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 options modes
     val _ = print_modes modes
-    val _ = print_moded_clauses thy moded_clauses
-    val _ = tracing "Defining executable functions..."
+      (*val _ = print_moded_clauses thy moded_clauses*)
+    val _ = print_step options "Defining executable functions..."
     val thy' = fold (#create_definitions steps preds) modes thy
       |> Theory.checkpoint
-    val _ = tracing "Compiling equations..."
+    val _ = print_step options "Compiling equations..."
     val compiled_terms =
       (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
-    val _ = print_compiled_terms thy' compiled_terms
-    val _ = tracing "Proving equations..."
-    val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
+    val _ = print_compiled_terms options thy' compiled_terms
+    val _ = print_step options "Proving equations..."
+    val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes)
       moded_clauses compiled_terms
     val qname = #qname steps
-    (* val attrib = gn thy => Attrib.attribute_i thy Code.add_eqn_attrib *)
     val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
       (fn thm => Context.mapping (Code.add_eqn thm) I))))
     val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
@@ -2226,7 +2206,7 @@
 
 fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
   
-fun gen_add_equations steps names thy =
+fun gen_add_equations steps options names thy =
   let
     val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
       |> Theory.checkpoint;
@@ -2235,33 +2215,83 @@
     val scc = strong_conn_of (PredData.get thy') names
     val thy'' = fold_rev
       (fn preds => fn thy =>
-        if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy)
+        if #are_not_defined steps thy preds then
+          add_equations_of steps options preds thy else thy)
       scc thy' |> Theory.checkpoint
   in thy'' end
 
 (* different instantiantions of the predicate compiler *)
 
+val predicate_comp_modifiers =
+  {const_name_of = predfun_name_of,
+  funT_of = funT_of,
+  additional_arguments = K [],
+  wrap_compilation = K (K (K (K (K I)))),
+  transform_additional_arguments = K I
+  }
+
+val depth_limited_comp_modifiers =
+  {const_name_of = depth_limited_function_name_of,
+  funT_of = depth_limited_funT_of,
+  additional_arguments = fn names =>
+    let
+      val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
+    in [Free (polarity_name, @{typ "bool"}), Free (depth_name, @{typ "code_numeral"})] end,
+  wrap_compilation =
+    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+    let
+      val [polarity, depth] = additional_arguments
+      val (_, Ts2) = chop (length (fst mode)) (binder_types T)
+      val (_, Us2) = split_smodeT (snd mode) Ts2
+      val T' = mk_predT compfuns (HOLogic.mk_tupleT Us2)
+      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+      val full_mode = null Us2
+    in
+      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+        $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T')
+          $ (if full_mode then mk_single compfuns HOLogic.unit else Const (@{const_name undefined}, T')))
+        $ compilation
+    end,
+  transform_additional_arguments =
+    fn prem => fn additional_arguments =>
+    let
+      val [polarity, depth] = additional_arguments
+      val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
+      val depth' =
+        Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})
+    in [polarity', depth'] end
+  }
+
+val rpred_comp_modifiers =
+  {const_name_of = generator_name_of,
+  funT_of = K generator_funT_of,
+  additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
+  wrap_compilation = K (K (K (K (K I)))),
+  transform_additional_arguments = K I
+  }
+
+
 val add_equations = gen_add_equations
   {infer_modes = infer_modes,
   create_definitions = create_definitions,
-  compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
+  compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove,
   are_not_defined = fn thy => forall (null o modes_of thy),
   qname = "equation"}
 
-val add_sizelim_equations = gen_add_equations
+val add_depth_limited_equations = gen_add_equations
   {infer_modes = infer_modes,
-  create_definitions = sizelim_create_definitions,
-  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
+  create_definitions = create_definitions_of_depth_limited_functions,
+  compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove_by_skip,
-  are_not_defined = fn thy => forall (null o sizelim_modes_of thy),
-  qname = "sizelim_equation"
-  }
+  are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
+  qname = "depth_limited_equation"}
 
 val add_quickcheck_equations = gen_add_equations
   {infer_modes = infer_modes_with_generator,
   create_definitions = rpred_create_definitions,
-  compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true,
+  compile_preds = compile_preds rpred_comp_modifiers RPredCompFuns.compfuns,
   prove = prove_by_skip,
   are_not_defined = fn thy => forall (null o rpred_modes_of thy),
   qname = "rpred_equation"}
@@ -2283,15 +2313,11 @@
 val setup = PredData.put (Graph.empty) #>
   Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
     "adding alternative introduction rules for code generation of inductive predicates"
-(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
-    "adding alternative elimination rules for code generation of inductive predicates";
-    *)
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
-  (*FIXME why distinguished attribute for cases?*)
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const rpred raw_const lthy =
+fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
@@ -2302,9 +2328,11 @@
     val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
     fun mk_cases const =
       let
+        val T = Sign.the_const_type thy const
+        val pred = Const (const, T)
         val nparams = nparams_of thy' const
         val intros = intros_of thy' const
-      in mk_casesrule lthy' nparams intros end  
+      in mk_casesrule lthy' pred nparams intros end  
     val cases_rules = map mk_cases preds
     val cases =
       map (fn case_rule => RuleCases.Case {fixes = [],
@@ -2320,11 +2348,14 @@
           (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       in
         goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
-          (if rpred then
-            (add_equations [const] #>
-             add_sizelim_equations [const] #> add_quickcheck_equations [const])
-        else add_equations [const]))
-      end  
+          (if is_rpred options then
+            (add_equations options [const] #>
+            add_quickcheck_equations options [const])
+           else if is_depth_limited options then
+             add_depth_limited_equations options [const]
+           else
+             add_equations options [const]))
+      end
   in
     Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
   end;
@@ -2335,9 +2366,11 @@
 (* transformation for code generation *)
 
 val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
+val random_eval_ref = Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
-fun analyze_compr thy t_compr =
+(* TODO: *)
+fun analyze_compr thy compfuns (depth_limit, random) t_compr =
   let
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
       | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
@@ -2348,6 +2381,8 @@
       (fn (i, t) => case t of Bound j => if j < length Ts then NONE
         else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
     val user_mode' = map (rpair NONE) user_mode
+    val all_modes_of = if random then all_generator_modes_of else all_modes_of
+      (*val compile_expr = if random then compile_gen_expr else compile_expr*)
     val modes = filter (fn Mode (_, is, _) => is = user_mode')
       (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes
@@ -2357,7 +2392,17 @@
       | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
                 ^ Syntax.string_of_term_global thy t_compr); m);
     val (inargs, outargs) = split_smode user_mode' args;
-    val t_pred = list_comb (compile_expr NONE NONE thy (m, list_comb (pred, params)), inargs);
+    val additional_arguments =
+      case depth_limit of
+        NONE => (if random then [@{term "5 :: code_numeral"}] else [])
+      | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
+    val comp_modifiers =
+      case depth_limit of NONE => 
+      (if random then rpred_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
+    val mk_fun_of = if random then mk_generator_of else
+      if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of
+    val t_pred = compile_expr comp_modifiers compfuns thy
+      (m, list_comb (pred, params)) inargs additional_arguments;
     val t_eval = if null outargs then t_pred else
       let
         val outargs_bounds = map (fn Bound i => i) outargs;
@@ -2370,22 +2415,30 @@
         val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
           (Term.list_abs (map (pair "") outargsTs,
             HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
-      in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
+      in mk_map compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
-fun eval thy t_compr =
+fun eval thy (options as (depth_limit, random)) t_compr =
   let
-    val t = analyze_compr thy t_compr;
-    val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
-    val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
-  in (T, Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []) end;
+    val compfuns = if random then RPredCompFuns.compfuns else PredicateCompFuns.compfuns
+    val t = analyze_compr thy compfuns options t_compr;
+    val T = dest_predT compfuns (fastype_of t);
+    val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
+    val eval =
+      if random then
+        Code_ML.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
+            (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
+          |> Random_Engine.run
+      else
+        Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
+  in (T, eval) end;
 
-fun values ctxt k t_compr =
+fun values ctxt options k t_compr =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (T, t) = eval thy t_compr;
+    val (T, ts) = eval thy options t_compr;
+    val (ts, _) = Predicate.yieldn k ts;
     val setT = HOLogic.mk_setT T;
-    val (ts, _) = Predicate.yieldn k t;
     val elemsT = HOLogic.mk_set T ts;
   in if k = ~1 orelse length ts < k then elemsT
     else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
@@ -2398,11 +2451,11 @@
   in
   end;
   *)
-fun values_cmd modes k raw_t state =
+fun values_cmd modes options k raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
-    val t' = values ctxt k t;
+    val t' = values ctxt options k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
     val p = PrintMode.with_modes modes (fn () =>
@@ -2410,15 +2463,24 @@
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
-
 local structure P = OuterParse in
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 
+val _ = List.app OuterKeyword.keyword ["depth_limit", "random"]
+
+val options =
+  let
+    val depth_limit = Scan.optional (P.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+    val random = Scan.optional (P.$$$ "random" >> K true) false
+  in
+    Scan.optional (P.$$$ "[" |-- depth_limit -- random --| P.$$$ "]") (NONE, false)
+  end
+
 val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
-  (opt_modes -- Scan.optional P.nat ~1 -- P.term
-    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
-        (values_cmd modes k t)));
+  (opt_modes -- options -- Scan.optional P.nat ~1 -- P.term
+    >> (fn (((modes, options), k), t) => Toplevel.no_timing o Toplevel.keep
+        (values_cmd modes options k t)));
 
 end;
 

--- a/src/HOL/ex/Predicate_Compile.thy	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Sun Oct 25 00:10:25 2009 +0200
@@ -12,6 +12,6 @@
 begin
 
 setup {* Predicate_Compile.setup *}
-setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *}
+setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *}
 
 end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Sun Oct 25 00:10:25 2009 +0200
@@ -0,0 +1,76 @@
+theory Predicate_Compile_Alternative_Defs
+imports Predicate_Compile
+begin
+
+section {* Set operations *}
+(*
+definition Empty where "Empty == {}"
+declare empty_def[symmetric, code_pred_inline]
+*)
+declare eq_reflection[OF empty_def, code_pred_inline] 
+(*
+definition Union where "Union A B == A Un B"
+
+lemma [code_pred_intros]: "A x ==> Union A B x"
+and  [code_pred_intros] : "B x ==> Union A B x"
+unfolding Union_def Un_def Collect_def mem_def by auto
+
+code_pred Union
+unfolding Union_def Un_def Collect_def mem_def by auto
+
+declare Union_def[symmetric, code_pred_inline]
+*)
+declare eq_reflection[OF Un_def, code_pred_inline]
+
+section {* Alternative list definitions *}
+ 
+subsection {* Alternative rules for set *}
+
+lemma set_ConsI1 [code_pred_intros]:
+  "set (x # xs) x"
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+lemma set_ConsI2 [code_pred_intros]:
+  "set xs x ==> set (x' # xs) x" 
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+code_pred set
+proof -
+  case set
+  from this show thesis
+    apply (case_tac a1)
+    apply auto
+    unfolding mem_def[symmetric, of _ a2]
+    apply auto
+    unfolding mem_def
+    apply auto
+    done
+qed
+
+
+subsection {* Alternative rules for list_all2 *}
+
+lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+by auto
+
+lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+by auto
+
+code_pred list_all2
+proof -
+  case list_all2
+  from this show thesis
+    apply -
+    apply (case_tac a1)
+    apply (case_tac a2)
+    apply auto
+    apply (case_tac a2)
+    apply auto
+    done
+qed
+
+
+
+end
\ No newline at end of file

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sun Oct 25 00:10:25 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
@@ -7,66 +7,216 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
-code_pred even .
+code_pred (mode: [], [1]) even .
+code_pred [depth_limited] even .
+code_pred [rpred] even .
 
 thm odd.equation
 thm even.equation
+thm odd.depth_limited_equation
+thm even.depth_limited_equation
+thm even.rpred_equation
+thm odd.rpred_equation
 
 values "{x. even 2}"
 values "{x. odd 2}"
 values 10 "{n. even n}"
 values 10 "{n. odd n}"
+values [depth_limit = 2] "{x. even 6}"
+values [depth_limit = 7] "{x. even 6}"
+values [depth_limit = 2] "{x. odd 7}"
+values [depth_limit = 8] "{x. odd 7}"
+
+values [depth_limit = 7] 10 "{n. even n}"
+
+definition odd' where "odd' x == \<not> even x"
+
+code_pred [inductify] odd' .
+code_pred [inductify, depth_limited] odd' .
+code_pred [inductify, rpred] odd' .
+
+thm odd'.depth_limited_equation
+values [depth_limit = 2] "{x. odd' 7}"
+values [depth_limit = 9] "{x. odd' 7}"
 
 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-code_pred append .
-code_pred (inductify_all) (rpred) append .
+code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+code_pred [depth_limited] append .
+code_pred [rpred] append .
 
 thm append.equation
+thm append.depth_limited_equation
 thm append.rpred_equation
 
 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
-values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0,5]}"
+values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
+values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}"
+
+value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
+value [code] "Predicate.the (append_3 ([]::int list))"
+
+subsection {* Tricky case with alternative rules *}
+
+inductive append2
+where
+  "append2 [] xs xs"
+| "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
+
+lemma append2_Nil: "append2 [] (xs::'b list) xs"
+  by (simp add: append2.intros(1))
+
+lemmas [code_pred_intros] = append2_Nil append2.intros(2)
+
+code_pred append2
+proof -
+  case append2
+  from append2.cases[OF append2(1)] append2(2-3) show thesis by blast
+qed
+
+subsection {* Tricky cases with tuples *}
+
+inductive zerozero :: "nat * nat => bool"
+where
+  "zerozero (0, 0)"
+
+code_pred zerozero .
+code_pred [rpred] zerozero .
+
+inductive tupled_append :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+  "tupled_append ([], xs, xs)"
+| "tupled_append (xs, ys, zs) \<Longrightarrow> tupled_append (x # xs, ys, x # zs)"
+
+code_pred tupled_append .
+code_pred [rpred] tupled_append .
+thm tupled_append.equation
+(*
+TODO: values with tupled modes
+values "{xs. tupled_append ([1,2,3], [4,5], xs)}"
+*)
+
+inductive tupled_append'
+where
+"tupled_append' ([], xs, xs)"
+| "[| ys = fst (xa, y); x # zs = snd (xa, y);
+ tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)"
+
+code_pred tupled_append' .
+thm tupled_append'.equation
+
+inductive tupled_append'' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+  "tupled_append'' ([], xs, xs)"
+| "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
+
+thm tupled_append''.cases
+
+code_pred [inductify] tupled_append'' .
+thm tupled_append''.equation
+
+inductive tupled_append''' :: "'a list \<times> 'a list \<times> 'a list \<Rightarrow> bool"
+where
+  "tupled_append''' ([], xs, xs)"
+| "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
+
+code_pred [inductify] tupled_append''' .
+thm tupled_append'''.equation
+
+inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+where
+  "map_ofP ((a, b)#xs) a b"
+| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
+
+code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP .
+thm map_ofP.equation
+
+inductive filter1
+for P
+where
+  "filter1 P [] []"
+| "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)"
+| "\<not> P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys"
+
+code_pred (mode: [1], [1, 2]) filter1 .
+code_pred [depth_limited] filter1 .
+code_pred [rpred] filter1 .
+
+thm filter1.equation
+
+inductive filter2
+where
+  "filter2 P [] []"
+| "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)"
+| "\<not> P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys"
+
+code_pred (mode: [1, 2, 3], [1, 2]) filter2 .
+code_pred [depth_limited] filter2 .
+code_pred [rpred] filter2 .
+thm filter2.equation
+thm filter2.rpred_equation
+
+inductive filter3
+for P
+where
+  "List.filter P xs = ys ==> filter3 P xs ys"
+
+code_pred filter3 .
+code_pred [depth_limited] filter3 .
+thm filter3.depth_limited_equation
+(*code_pred [rpred] filter3 .*)
+inductive filter4
+where
+  "List.filter P xs = ys ==> filter4 P xs ys"
+
+code_pred filter4 .
+code_pred [depth_limited] filter4 .
+code_pred [rpred] filter4 .
+
+section {* reverse *}
 
 inductive rev where
     "rev [] []"
   | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
 
-code_pred rev .
+code_pred (mode: [1], [2], [1, 2]) rev .
 
 thm rev.equation
 
 values "{xs. rev [0, 1, 2, 3::nat] xs}"
 
+inductive tupled_rev where
+  "tupled_rev ([], [])"
+| "tupled_rev (xs, xs') \<Longrightarrow> tupled_append (xs', [x], ys) \<Longrightarrow> tupled_rev (x#xs, ys)"
+
+code_pred tupled_rev .
+thm tupled_rev.equation
+
 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for f where
     "partition f [] [] []"
   | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
   | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
 
-code_pred partition .
+code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition .
+code_pred [depth_limited] partition .
+code_pred [rpred] partition .
 
-thm partition.equation
+inductive tupled_partition :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<times> 'a list \<times> 'a list) \<Rightarrow> bool"
+  for f where
+   "tupled_partition f ([], [], [])"
+  | "f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, x # ys, zs)"
+  | "\<not> f x \<Longrightarrow> tupled_partition f (xs, ys, zs) \<Longrightarrow> tupled_partition f (x # xs, ys, x # zs)"
+
+code_pred tupled_partition .
+
+thm tupled_partition.equation
 
 
-inductive member
-for xs
-where "x \<in> set xs ==> member xs x"
-
-lemma [code_pred_intros]:
-  "member (x#xs') x"
-by (auto intro: member.intros)
-
-lemma [code_pred_intros]:
-"member xs x ==> member (x'#xs) x"
-by (auto intro: member.intros elim!: member.cases)
-(* strange bug must be repaired! *)
-(*
-code_pred member sorry
-*)
 inductive is_even :: "nat \<Rightarrow> bool"
 where
   "n mod 2 = 0 \<Longrightarrow> is_even n"
@@ -88,18 +238,20 @@
   case tranclp
   from this converse_tranclpE[OF this(1)] show thesis by metis
 qed
-(*
-code_pred (inductify_all) (rpred) tranclp .
+
+code_pred [depth_limited] tranclp .
+code_pred [rpred] tranclp .
 thm tranclp.equation
 thm tranclp.rpred_equation
-*)
+
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
 
 code_pred succ .
-
+code_pred [rpred] succ .
 thm succ.equation
+thm succ.rpred_equation
 
 values 10 "{(m, n). succ n m}"
 values "{m. succ 0 m}"
@@ -141,6 +293,16 @@
  (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
  [3,5] t}"
 
+inductive tupled_exec :: "(com \<times> state \<times> state) \<Rightarrow> bool" where
+"tupled_exec (Skip, s, s)" |
+"tupled_exec (Ass x e, s, s[x := e(s)])" |
+"tupled_exec (c1, s1, s2) ==> tupled_exec (c2, s2, s3) ==> tupled_exec (Seq c1 c2, s1, s3)" |
+"b s ==> tupled_exec (c1, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
+"~b s ==> tupled_exec (c2, s, t) ==> tupled_exec (IF b c1 c2, s, t)" |
+"~b s ==> tupled_exec (While b c, s, s)" |
+"b s1 ==> tupled_exec (c, s1, s2) ==> tupled_exec (While b c, s2, s3) ==> tupled_exec (While b c, s1, s3)"
+
+code_pred tupled_exec .
 
 subsection{* CCS *}
 
@@ -171,6 +333,17 @@
 values 3 "{(a,q). step (par nil nil) a q}"
 *)
 
+inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
+where
+"tupled_step (pre n p, n, p)" |
+"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
+"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (or p1 p2, a, q)" |
+"tupled_step (p1, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par q p2)" |
+"tupled_step (p2, a, q) \<Longrightarrow> tupled_step (par p1 p2, a, par p1 q)"
+
+code_pred tupled_step .
+thm tupled_step.equation
+
 subsection {* divmod *}
 
 inductive divmod_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -179,52 +352,75 @@
 
 code_pred divmod_rel ..
 
-value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
+value [code] "Predicate.the (divmod_rel_1_2 1705 42)"
 
 section {* Executing definitions *}
 
 definition Min
 where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
 
-code_pred (inductify_all) Min .
+code_pred [inductify] Min .
 
 subsection {* Examples with lists *}
 
-inductive filterP for Pa where
-"(filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) [] []"
-| "[| (res::'a list) = (y::'a) # (resa::'a list); (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) resa; Pa y |]
-==> filterP Pa (y # xt) res"
-| "[| (filterP::('a => bool) => 'a list => 'a list => bool) (Pa::'a => bool) (xt::'a list) (res::'a list); ~ Pa (y::'a) |] ==> filterP Pa (y # xt) res"
+subsubsection {* Lexicographic order *}
+
+thm lexord_def
+code_pred [inductify] lexord .
+code_pred [inductify, rpred] lexord .
+thm lexord.equation
+thm lexord.rpred_equation
+
+inductive less_than_nat :: "nat * nat => bool"
+where
+  "less_than_nat (0, x)"
+| "less_than_nat (x, y) ==> less_than_nat (Suc x, Suc y)"
+ 
+code_pred less_than_nat .
+
+code_pred [depth_limited] less_than_nat .
+code_pred [rpred] less_than_nat .
 
+inductive test_lexord :: "nat list * nat list => bool"
+where
+  "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)"
+
+code_pred [rpred] test_lexord .
+code_pred [depth_limited] test_lexord .
+thm test_lexord.depth_limited_equation
+thm test_lexord.rpred_equation
+
+values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
+values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
+(*values [random] "{xys. test_lexord xys}"*)
+(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*)
 (*
-code_pred (inductify_all) (rpred) filterP .
-thm filterP.rpred_equation
+lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat"
+quickcheck[generator=pred_compile]
+oops
 *)
-
-code_pred (inductify_all) lexord .
-
-thm lexord.equation
-
-lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r"
-(*quickcheck[generator=pred_compile]*)
-oops
-
 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
 
-code_pred (inductify_all) lexn .
+code_pred [inductify] lexn .
 thm lexn.equation
 
-code_pred (inductify_all) lenlex .
+code_pred [rpred] lexn .
+
+thm lexn.rpred_equation
+
+code_pred [inductify, show_steps] lenlex .
 thm lenlex.equation
-(*
-code_pred (inductify_all) (rpred) lenlex .
+
+code_pred [inductify, rpred] lenlex .
 thm lenlex.rpred_equation
-*)
+
 thm lists.intros
-code_pred (inductify_all) lists .
+code_pred [inductify] lists .
 
 thm lists.equation
 
+section {* AVL Tree Example *}
+
 datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
 fun height :: "'a tree => nat" where
 "height ET = 0"
@@ -236,40 +432,107 @@
   "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
 
-code_pred (inductify_all) avl .
+code_pred [inductify] 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
+code_pred [rpred] avl .
+thm avl.rpred_equation
+(*values [random] 10 "{t. avl (t::int tree)}"*)
 
 fun set_of
 where
 "set_of ET = {}"
 | "set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
 
-fun is_ord
+fun is_ord :: "nat tree => bool"
 where
 "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)"
 
-declare Un_def[code_pred_def]
-
-code_pred (inductify_all) set_of .
+code_pred (mode: [1], [1, 2]) [inductify] set_of .
 thm set_of.equation
-(* FIXME *)
-(*
-code_pred (inductify_all) is_ord .
+
+code_pred [inductify] is_ord .
 thm is_ord.equation
-*)
+code_pred [rpred] is_ord .
+thm is_ord.rpred_equation
+
 section {* Definitions about Relations *}
 
-code_pred (inductify_all) converse .
+code_pred [inductify] converse .
 thm converse.equation
+code_pred [inductify] rel_comp .
+thm rel_comp.equation
+code_pred [inductify] Image .
+thm Image.equation
+(*TODO: *)
+ML {* Toplevel.debug := true *}
+declare Id_on_def[unfolded UNION_def, code_pred_def]
+
+code_pred [inductify] Id_on .
+thm Id_on.equation
+code_pred [inductify] Domain .
+thm Domain.equation
+code_pred [inductify] Range .
+thm sym_def
+code_pred [inductify] Field .
+declare Sigma_def[unfolded UNION_def, code_pred_def]
+declare refl_on_def[unfolded UNION_def, code_pred_def]
+code_pred [inductify] refl_on .
+thm refl_on.equation
+code_pred [inductify] total_on .
+thm total_on.equation
+(*
+code_pred [inductify] sym .
+thm sym.equation
+*)
+code_pred [inductify] antisym .
+thm antisym.equation
+code_pred [inductify] trans .
+thm trans.equation
+code_pred [inductify] single_valued .
+thm single_valued.equation
+code_pred [inductify] inv_image .
+thm inv_image.equation
 
-code_pred (inductify_all) Domain .
-thm Domain.equation
+section {* List functions *}
+
+code_pred [inductify] length .
+thm size_listP.equation
+code_pred [inductify, rpred] length .
+thm size_listP.rpred_equation
+values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}"
 
+code_pred [inductify] concat .
+code_pred [inductify] hd .
+code_pred [inductify] tl .
+code_pred [inductify] last .
+code_pred [inductify] butlast .
+(*code_pred [inductify] listsum .*)
+code_pred [inductify] take .
+code_pred [inductify] drop .
+code_pred [inductify] zip .
+code_pred [inductify] upt .
+code_pred [inductify] remdups .
+code_pred [inductify] remove1 .
+code_pred [inductify] removeAll .
+code_pred [inductify] distinct .
+code_pred [inductify] replicate .
+code_pred [inductify] splice .
+code_pred [inductify] List.rev .
+code_pred [inductify] map .
+code_pred [inductify] foldr .
+code_pred [inductify] foldl .
+code_pred [inductify] filter .
+code_pred [inductify, rpred] filter .
+thm filterP.rpred_equation
+
+definition test where "test xs = filter (\<lambda>x. x = (1::nat)) xs"
+code_pred [inductify] test .
+thm testP.equation
+code_pred [inductify, rpred] test .
+thm testP.rpred_equation
 
 section {* Context Free Grammar *}
 
@@ -283,15 +546,86 @@
 | "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
 | "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
 
-code_pred (inductify_all) S\<^isub>1p .
+code_pred [inductify] S\<^isub>1p .
+code_pred [inductify, rpred] S\<^isub>1p .
+thm S\<^isub>1p.equation
+thm S\<^isub>1p.rpred_equation
 
-thm S\<^isub>1p.equation
+values [random] 5 "{x. S\<^isub>1p x}"
+
+inductive is_a where
+  "is_a a"
+
+inductive is_b where
+  "is_b b"
 
-theorem S\<^isub>1_sound:
-"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=pred_compile]
+code_pred is_a .
+code_pred [depth_limited] is_a .
+code_pred [rpred] is_a .
+
+values [random] "{x. is_a x}"
+code_pred [depth_limited] is_b .
+code_pred [rpred] is_b .
+
+code_pred [inductify, depth_limited] filter .
+
+values [depth_limit=5] "{x. filterP is_a [a, b] x}"
+values [depth_limit=3] "{x. filterP is_b [a, b] x}"
+
+lemma "w \<in> S\<^isub>1 \<Longrightarrow> length (filter (\<lambda>x. x = a) w) = 1"
+(*quickcheck[generator=pred_compile, size=10]*)
 oops
 
+inductive test_lemma where
+  "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \<noteq> r4 ==> test_lemma w"
+(*
+code_pred [rpred] test_lemma .
+*)
+(*
+definition test_lemma' where
+  "test_lemma' w == (w \<in> S\<^isub>1 \<and> (\<not> length [x <- w. x = a] = length [x <- w. x = b]))"
+
+code_pred [inductify, rpred] test_lemma' .
+thm test_lemma'.rpred_equation
+*)
+(*thm test_lemma'.rpred_equation*)
+(*
+values [depth_limit=3 random] "{x. S\<^isub>1 x}"
+*)
+code_pred [depth_limited] is_b .
+(*
+code_pred [inductify, depth_limited] filter .
+*)
+thm filterP.intros
+thm filterP.equation
+(*
+values [depth_limit=3] "{x. filterP is_b [a, b] x}"
+find_theorems "test_lemma'_hoaux"
+code_pred [depth_limited] test_lemma'_hoaux .
+thm test_lemma'_hoaux.depth_limited_equation
+values [depth_limit=2] "{x. test_lemma'_hoaux b}"
+inductive test1 where
+  "\<not> test_lemma'_hoaux x ==> test1 x"
+code_pred test1 .
+code_pred [depth_limited] test1 .
+thm test1.depth_limited_equation
+thm test_lemma'_hoaux.depth_limited_equation
+thm test1.intros
+
+values [depth_limit=2] "{x. test1 b}"
+
+thm filterP.intros
+thm filterP.depth_limited_equation
+values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}"
+values [depth_limit=4 random] "{w. test_lemma w}"
+values [depth_limit=4 random] "{w. test_lemma' w}"
+*)
+(*
+theorem S\<^isub>1_sound:
+"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
+quickcheck[generator=pred_compile, size=15]
+oops
+*)
 inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   "[] \<in> S\<^isub>2"
 | "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
@@ -299,14 +633,18 @@
 | "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
 | "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
 | "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
-(*
-code_pred (inductify_all) (rpred) S\<^isub>2 .
-ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name "B\<^isub>2"} *}
-*)
+
+code_pred [inductify, rpred] S\<^isub>2 .
+thm S\<^isub>2.rpred_equation
+thm A\<^isub>2.rpred_equation
+thm B\<^isub>2.rpred_equation
+
+values [random] 10 "{x. S\<^isub>2 x}"
+
 theorem S\<^isub>2_sound:
 "w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 (*quickcheck[generator=SML]*)
-quickcheck[generator=pred_compile, size=15, iterations=100]
+(*quickcheck[generator=pred_compile, size=15, iterations=1]*)
 oops
 
 inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -317,23 +655,35 @@
 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
 
+code_pred [inductify] S\<^isub>3 .
+thm S\<^isub>3.equation
+
+values 10 "{x. S\<^isub>3 x}"
 (*
-code_pred (inductify_all) S\<^isub>3 .
-*)
 theorem S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 quickcheck[generator=pred_compile, size=10, iterations=1]
 oops
-
+*)
 lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = pred_compile]
+(*quickcheck[size=10, generator = pred_compile]*)
 oops
+(*
+inductive test
+where
+  "length [x \<leftarrow> w. a = x] = length [x \<leftarrow> w. x = b] ==> test w"
+ML {* @{term "[x \<leftarrow> w. x = a]"} *}
+code_pred (inductify_all) test .
 
+thm test.equation
+*)
+(*
 theorem S\<^isub>3_complete:
-"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
+"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. b = x] \<longrightarrow> w \<in> S\<^isub>3"
 (*quickcheck[generator=SML]*)
 quickcheck[generator=pred_compile, size=10, iterations=100]
 oops
+*)
 
 inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   "[] \<in> S\<^isub>4"
@@ -343,15 +693,15 @@
 | "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
 | "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
 | "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
-
+(*
 theorem S\<^isub>4_sound:
 "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
 quickcheck[generator = pred_compile, size=2, iterations=1]
 oops
-
+*)
 theorem S\<^isub>4_complete:
 "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = pred_compile, size=5, iterations=1]
+(*quickcheck[generator = pred_compile, size=5, iterations=1]*)
 oops
 
 theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
@@ -361,8 +711,8 @@
 (*quickcheck[generator = pred_compile, size=5, iterations=1]*)
 oops
 
+section {* Lambda *}
 
-section {* Lambda *}
 datatype type =
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
@@ -378,15 +728,15 @@
   "[]\<langle>i\<rangle> = None"
 | "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
 
-(*
+
 inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
 where
   "nth_el' (x # xs) 0 x"
 | "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
-*)
+
 inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   where
-    Var [intro!]: "nth_el env x = Some T \<Longrightarrow> env \<turnstile> Var x : T"
+    Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
   | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
 (*  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U" *)
   | App [intro!]: "env \<turnstile> s : U \<Rightarrow> T \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
@@ -414,22 +764,8 @@
   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
 
 lemma "Gamma \<turnstile> t : T \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> Gamma \<turnstile> t' : T"
-quickcheck[generator = pred_compile, size = 10, iterations = 1000]
+(*quickcheck[generator = pred_compile, size = 10, iterations = 1]*)
 oops
-(* FIXME *)
-(*
-inductive test for P where
-"[| filter P vs = res |]
-==> test P vs res"
-
-code_pred test .
-*)
-(*
-export_code test_for_1_yields_1_2 in SML file -
-code_pred (inductify_all) (rpred) test .
-
-thm test.equation
-*)
 
 lemma filter_eq_ConsD:
  "filter P ys = x#xs \<Longrightarrow>

--- a/src/HOL/ex/RPred.thy	Sun Oct 25 00:05:57 2009 +0200
+++ b/src/HOL/ex/RPred.thy	Sun Oct 25 00:10:25 2009 +0200
@@ -2,7 +2,7 @@
 imports Quickcheck Random Predicate
 begin
 
-types 'a rpred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+types 'a "rpred" = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
 
 section {* The RandomPred Monad *}
 
@@ -33,9 +33,9 @@
 
 (* Missing a good definition for negation: not_rpred *)
 
-definition not_rpred :: "unit Predicate.pred \<Rightarrow> unit rpred"
+definition not_rpred :: "unit rpred \<Rightarrow> unit rpred"
 where
-  "not_rpred = Pair o Predicate.not_pred"
+  "not_rpred P = (\<lambda>s. let (P', s') = P s in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
 
 definition lift_pred :: "'a Predicate.pred \<Rightarrow> 'a rpred"
   where
@@ -44,9 +44,9 @@
 definition lift_random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a rpred"
   where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
 
-definition map_rpred :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
-where "map_rpred f P = bind P (return o f)"
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
+  where "map f P = bind P (return o f)"
 
-hide (open) const return bind supp 
+hide (open) const return bind supp map
   
 end
\ No newline at end of file