merged
authorhaftmann
Sat, 07 Nov 2009 08:18:12 +0100
changeset 33501 31872dd275c8
parent 33497 39c9d0785911 (diff)
parent 33500 22e5725be1f3 (current diff)
child 33502 cf392b693385
child 33507 6390cc8d2714
merged
--- a/NEWS	Sat Nov 07 08:17:53 2009 +0100
+++ b/NEWS	Sat Nov 07 08:18:12 2009 +0100
@@ -54,6 +54,8 @@
 solvers using the oracle mechanism; for the SMT solver Z3,
 this method is proof-producing. Certificates are provided to
 avoid calling the external solvers solely for re-checking proofs.
+Due to a remote SMT service there is no need for installing SMT
+solvers locally.
 
 * New commands to load and prove verification conditions
 generated by the Boogie program verifier or derived systems
@@ -227,6 +229,10 @@
 * Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
 replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
 
+* Renamed methods:
+    sizechange -> size_change
+    induct_scheme -> induction_schema
+
 
 *** ML ***
 
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -293,8 +293,8 @@
 fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
 
 fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
-val str = Scan.some (fn (_, Token s) => SOME s | _ => NONE)
-val num = Scan.some (fn (_, Token s) => read_int' s | _ => NONE)
+fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
+fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st
 
 fun scan_line key scan =
   $$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false)
--- a/src/HOL/Code_Evaluation.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -243,6 +243,26 @@
 hide const dummy_term App valapp
 hide (open) const Const termify valtermify term_of term_of_num
 
+subsection {* Tracing of generated and evaluated code *}
+
+definition tracing :: "String.literal => 'a => 'a"
+where
+  [code del]: "tracing s x = x"
+
+ML {*
+structure Code_Evaluation =
+struct
+
+fun tracing s x = (Output.tracing s; x)
+
+end
+*}
+
+code_const "tracing :: String.literal => 'a => 'a"
+  (Eval "Code'_Evaluation.tracing")
+
+hide (open) const tracing
+code_reserved Eval Code_Evaluation
 
 subsection {* Evaluation setup *}
 
--- a/src/HOL/FunDef.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/FunDef.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -22,7 +22,7 @@
   ("Tools/Function/lexicographic_order.ML")
   ("Tools/Function/pat_completeness.ML")
   ("Tools/Function/fun.ML")
-  ("Tools/Function/induction_scheme.ML")
+  ("Tools/Function/induction_schema.ML")
   ("Tools/Function/termination.ML")
   ("Tools/Function/decompose.ML")
   ("Tools/Function/descent.ML")
@@ -114,13 +114,13 @@
 use "Tools/Function/function.ML"
 use "Tools/Function/pat_completeness.ML"
 use "Tools/Function/fun.ML"
-use "Tools/Function/induction_scheme.ML"
+use "Tools/Function/induction_schema.ML"
 
 setup {* 
   Function.setup
   #> Pat_Completeness.setup
   #> Function_Fun.setup
-  #> Induction_Scheme.setup
+  #> Induction_Schema.setup
 *}
 
 subsection {* Measure Functions *}
--- a/src/HOL/IsaMakefile	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/IsaMakefile	Sat Nov 07 08:18:12 2009 +0100
@@ -180,7 +180,7 @@
   Tools/Function/function_lib.ML \
   Tools/Function/function.ML \
   Tools/Function/fun.ML \
-  Tools/Function/induction_scheme.ML \
+  Tools/Function/induction_schema.ML \
   Tools/Function/lexicographic_order.ML \
   Tools/Function/measure_functions.ML \
   Tools/Function/mutual.ML \
@@ -939,7 +939,7 @@
   ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
   ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
-  ex/Hilbert_Classical.thy ex/Induction_Scheme.thy			\
+  ex/Hilbert_Classical.thy ex/Induction_Schema.thy			\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
   ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -549,7 +549,7 @@
 
 section {* Bitvectors *}
 
-locale bv
+locale z3_bv_test
 begin
 
 text {*
--- a/src/HOL/SMT/SMT.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/SMT.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -13,9 +13,59 @@
 
 setup {* CVC3_Solver.setup #> Yices_Solver.setup *}
 
-declare [[ smt_solver = z3, smt_timeout = 20 ]]
+
+
+section {* Setup *}
+
+text {*
+Without further ado, the SMT solvers CVC3 and Z3 are provided
+remotely via an SMT server. For faster responses, the solver
+environment variables CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER
+need to point to the respective SMT solver executable.
+*}
+
+
+
+section {* Available configuration options *}
+
+text {* Choose the SMT solver to be applied (one of cvc3, yices, or z3): *}
+
+declare [[ smt_solver = z3 ]]
+
+text {* Restrict the runtime of an SMT solver (in seconds): *}
+
+declare [[ smt_timeout = 20 ]]
+
+
+subsection {* Z3-specific options *}
+
+text {* Enable proof reconstruction for Z3: *}
+
+declare [[ z3_proofs = false ]]
+
+text {* Pass extra command-line arguments to Z3
+to control its behaviour: *}
+
+declare [[ z3_options = "" ]]
+
+
+subsection {* Special configuration options *}
+
+text {*
+Trace the problem file, the result of the SMT solver and
+further information: *}
+
+declare [[ smt_trace = false ]]
+
+text {* Unfold (some) definitions passed to the SMT solver: *}
+
 declare [[ smt_unfold_defs = true ]]
-declare [[ smt_trace = false, smt_keep = "", smt_cert = "" ]]
-declare [[ z3_proofs = false, z3_options = "" ]]
+
+text {*
+Produce or use certificates (to avoid repeated invocation of an
+SMT solver again and again). The value is an absolute path
+pointing to the problem file. See also the examples. *}
+
+declare [[ smt_keep = "", smt_cert = "" ]]
 
 end
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -36,7 +36,7 @@
   end
 
 fun smtlib_solver oracle _ = {
-  command = {env_var=env_var, remote_name=solver_name},
+  command = {env_var=env_var, remote_name=SOME solver_name},
   arguments = options,
   interface = SMTLIB_Interface.interface,
   reconstruct = oracle }
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -18,7 +18,7 @@
     recon: SMT_Translate.recon,
     assms: thm list option }
   type solver_config = {
-    command: {env_var: string, remote_name: string},
+    command: {env_var: string, remote_name: string option},
     arguments: string list,
     interface: interface,
     reconstruct: proof_data -> thm }
@@ -69,7 +69,7 @@
   assms: thm list option }
 
 type solver_config = {
-  command: {env_var: string, remote_name: string},
+  command: {env_var: string, remote_name: string option},
   arguments: string list,
   interface: interface,
   reconstruct: proof_data -> thm }
@@ -96,7 +96,7 @@
 
 local
 
-fun with_files ctxt f x =
+fun with_files ctxt f =
   let
     fun make_names n = (n, n ^ ".proof")
 
@@ -107,43 +107,79 @@
       else pairself (File.tmp_path o Path.explode)
         (make_names ("smt-" ^ serial_string ()))
 
-    val y = Exn.capture (f problem_path proof_path) x
+    val y = Exn.capture f (problem_path, proof_path)
 
     val _ = if keep' = "" then (pairself (try File.rm) paths; ()) else ()
   in Exn.release y end
 
-fun run in_path out_path (ctxt, cmd, output) =
+fun invoke ctxt output f (paths as (problem_path, proof_path)) =
   let
     fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
       (map Pretty.str ls))
 
-    val x = File.open_output output in_path
+    val x = File.open_output output problem_path
     val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
-      in_path
+      problem_path
 
-    val _ = with_timeout ctxt system_out (cmd in_path out_path)
-    fun lines_of path = the_default [] (try (File.fold_lines cons out_path) [])
-    val ls = rev (dropwhile (equal "") (lines_of out_path))
+    val _ = with_timeout ctxt f paths
+    fun lines_of path = the_default [] (try (File.fold_lines cons path) [])
+    val ls = rev (dropwhile (equal "") (lines_of proof_path))
     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in (x, ls) end
 
+val expand_name = Path.implode o Path.expand o Path.explode 
+
+fun run_perl name args ps =
+  system_out (space_implode " " ("perl -w" ::
+    File.shell_path (Path.explode (getenv name)) ::
+    map File.shell_quote args @ ps))
+
+fun use_certificate ctxt ps =
+  let val name = Config.get ctxt cert
+  in
+    if name = "" then false
+    else
+     (tracing ("Using certificate " ^ quote (expand_name name) ^ " ...");
+      run_perl "CERT_SMT_SOLVER" [expand_name name] ps;
+      true)
+  end
+
+fun run_locally f ctxt env_var args ps =
+  if getenv env_var = ""
+  then f ("Undefined Isabelle environment variable: " ^ quote env_var)
+  else
+    let val app = Path.expand (Path.explode (getenv env_var))
+    in
+      if not (File.exists app)
+      then f ("No such file: " ^ quote (Path.implode app))
+      else
+       (tracing ("Invoking local SMT solver " ^ quote (Path.implode app) ^
+          " ...");
+        system_out (space_implode " " (File.shell_path app ::
+        map File.shell_quote args @ ps)); ())
+    end
+
+fun run_remote remote_name args ps msg =
+  (case remote_name of
+    NONE => error msg
+  | SOME name =>
+      let
+        val url = getenv "REMOTE_SMT_URL"
+        val _ = tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^
+          quote url ^ " ...")
+      in (run_perl "REMOTE_SMT_SOLVER" (url :: name :: args) ps; ()) end)
+
+fun run ctxt {env_var, remote_name} args (problem_path, proof_path) =
+  let val ps = [File.shell_path problem_path, ">", File.shell_path proof_path]
+  in
+    if use_certificate ctxt ps then ()
+    else run_locally (run_remote remote_name args ps) ctxt env_var args ps
+  end
+
 in
 
-fun run_solver ctxt {env_var, remote_name} args output =
-  let
-    val qf = File.shell_path and qq = File.shell_quote
-    val qs = qf o Path.explode
-    val local_name = getenv env_var
-    val cert_name = Config.get ctxt cert
-    val remote = qs (getenv "REMOTE_SMT_SOLVER")
-    val cert_script = qs (getenv "CERT_SMT_SOLVER")
-    fun cmd f1 f2 =
-      if cert_name <> ""
-      then "perl -w" :: [cert_script, qs cert_name, qf f1, ">", qf f2]
-      else if local_name <> ""
-      then qs local_name :: map qq args @ [qf f1, ">", qf f2]
-      else "perl -w" :: remote :: map qq (remote_name :: args) @ [qf f1, qf f2]
-  in with_files ctxt run (ctxt, space_implode " " oo cmd, output) end
+fun run_solver ctxt cmd args output =
+  with_files ctxt (invoke ctxt output (run ctxt cmd args))
 
 end
 
@@ -223,13 +259,13 @@
         (map (Syntax.pretty_term ctxt) ex))
     end
 
-  fun fail_tac ctxt msg st = (trace_msg ctxt I msg; Tactical.no_tac st)
+  fun fail_tac f msg st = (f msg; Tactical.no_tac st)
 
   fun SAFE pass_exns tac ctxt i st =
     if pass_exns then tac ctxt i st
     else (tac ctxt i st
-      handle SMT msg => fail_tac ctxt ("SMT: " ^ msg) st
-           | SMT_COUNTEREXAMPLE cex => fail_tac ctxt (pretty_cex ctxt cex) st)
+      handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
+           | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
 
   fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules
 in
--- a/src/HOL/SMT/Tools/yices_solver.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -32,7 +32,7 @@
   end
 
 fun smtlib_solver oracle _ = {
-  command = {env_var=env_var, remote_name=solver_name},
+  command = {env_var=env_var, remote_name=NONE},
   arguments = options,
   interface = SMTLIB_Interface.interface,
   reconstruct = oracle }
--- a/src/HOL/SMT/Tools/z3_model.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_model.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -55,7 +55,8 @@
 val value = mapping |-- expr
 
 val args_case = Scan.repeat expr -- value
-val else_case = space -- Scan.this_string "else" |-- value >> pair []
+val else_case = space -- Scan.this_string "else" |-- value >>
+  pair ([] : expr list)
 
 val func =
   let fun cases st = (else_case >> single || args_case ::: cases) st
--- a/src/HOL/SMT/Tools/z3_solver.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -66,7 +66,7 @@
 fun solver oracle ctxt =
   let val with_proof = Config.get ctxt proofs
   in
-    {command = {env_var=env_var, remote_name=solver_name},
+    {command = {env_var=env_var, remote_name=SOME solver_name},
     arguments = cmdline_options ctxt,
     interface = Z3_Interface.interface,
     reconstruct = if with_proof then prover else oracle}
--- a/src/HOL/SMT/lib/scripts/remote_smt.pl	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/SMT/lib/scripts/remote_smt.pl	Sat Nov 07 08:18:12 2009 +0100
@@ -8,17 +8,12 @@
 use LWP;
 
 
-# environment
-
-my $remote_smt_url = $ENV{"REMOTE_SMT_URL"};
-
-
 # arguments
 
-my $solver = $ARGV[0];
-my @options = @ARGV[1 .. ($#ARGV - 2)];
-my $problem_file = $ARGV[-2];
-my $output_file = $ARGV[-1];
+my $url = $ARGV[0];
+my $solver = $ARGV[1];
+my @options = @ARGV[2 .. ($#ARGV - 1)];
+my $problem_file = $ARGV[-1];
 
 
 # call solver
@@ -26,7 +21,7 @@
 my $agent = LWP::UserAgent->new;
 $agent->agent("SMT-Request");
 $agent->timeout(180);
-my $response = $agent->post($remote_smt_url, [
+my $response = $agent->post($url, [
   "Solver" => $solver,
   "Options" => join(" ", @options),
   "Problem" => [$problem_file] ],
@@ -36,8 +31,6 @@
   exit 1;
 }
 else {
-  open(FILE, ">$output_file");
-  print FILE $response->content;
-  close(FILE);
+  print $response->content;
+  exit 0;
 }
-
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -1,11 +1,15 @@
 (*  Title:      HOL/Tools/ATP_Manager/atp_minimal.ML
     Author:     Philipp Meyer, TU Muenchen
 
-Minimalization of theorem list for metis by using an external automated theorem prover
+Minimization of theorem list for metis by using an external automated theorem prover
 *)
 
 signature ATP_MINIMAL =
 sig
+  val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
+    (string * thm list) list -> ((string * thm list) list * int) option * string
+  (* To be removed once TN has finished his measurements;
+     the int component of the result should then be removed: *)
   val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
     (string * thm list) list -> ((string * thm list) list * int) option * string
 end
@@ -13,7 +17,16 @@
 structure ATP_Minimal: ATP_MINIMAL =
 struct
 
-(* minimalization algorithm *)
+(* Linear minimization *)
+
+fun lin_gen_minimize p s =
+let
+  fun min [] needed = needed
+    | min (x::xs) needed =
+        if p(xs @ needed) then min xs needed else min xs (x::needed)
+in (min s [], length s) end;
+
+(* Clever minimalization algorithm *)
 
 local
   fun isplit (l, r) [] = (l, r)
@@ -120,7 +133,7 @@
 
 (* minimalization of thms *)
 
-fun minimalize prover prover_name time_limit state name_thms_pairs =
+fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
   let
     val _ =
       priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
@@ -141,11 +154,11 @@
             else name_thms_pairs
           val (min_thms, n) =
             if null to_use then ([], 0)
-            else minimal (test_thms (SOME filtered)) to_use
+            else gen_min (test_thms (SOME filtered)) to_use
           val min_names = sort_distinct string_ord (map fst min_thms)
           val _ = priority (cat_lines
-            ["Interations: " ^ string_of_int n,
-              "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
+            ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
+             "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
         in
           (SOME (min_thms, n), "Try this command: " ^
             Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
@@ -193,6 +206,10 @@
 
 fun get_options args = fold get_opt args (default_prover, default_time_limit)
 
+val minimize = gen_minimalize lin_gen_minimize
+
+val minimalize = gen_minimalize minimal
+
 fun sh_min_command args thm_names state =
   let
     val (prover_name, time_limit) = get_options args
@@ -202,10 +219,11 @@
       | NONE => error ("Unknown prover: " ^ quote prover_name))
     val name_thms_pairs = get_thms (Proof.context_of state) thm_names
   in
-    writeln (#2 (minimalize prover prover_name time_limit state name_thms_pairs))
+    writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
   end
 
-val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
+val parse_args =
+  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
 val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
 
 val _ =
@@ -217,4 +235,3 @@
 end
 
 end
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -0,0 +1,405 @@
+(*  Title:      HOL/Tools/Function/induction_schema.ML
+    Author:     Alexander Krauss, TU Muenchen
+
+A method to prove induction schemas.
+*)
+
+signature INDUCTION_SCHEMA =
+sig
+  val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
+                   -> Proof.context -> thm list -> tactic
+  val induction_schema_tac : Proof.context -> thm list -> tactic
+  val setup : theory -> theory
+end
+
+
+structure Induction_Schema : INDUCTION_SCHEMA =
+struct
+
+open Function_Lib
+
+
+type rec_call_info = int * (string * typ) list * term list * term list
+
+datatype scheme_case =
+  SchemeCase of
+  {
+   bidx : int,
+   qs: (string * typ) list,
+   oqnames: string list,
+   gs: term list,
+   lhs: term list,
+   rs: rec_call_info list
+  }
+
+datatype scheme_branch = 
+  SchemeBranch of
+  {
+   P : term,
+   xs: (string * typ) list,
+   ws: (string * typ) list,
+   Cs: term list
+  }
+
+datatype ind_scheme =
+  IndScheme of
+  {
+   T: typ, (* sum of products *)
+   branches: scheme_branch list,
+   cases: scheme_case list
+  }
+
+val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
+val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
+
+fun meta thm = thm RS eq_reflection
+
+val sum_prod_conv = MetaSimplifier.rewrite true 
+                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
+
+fun term_conv thy cv t = 
+    cv (cterm_of thy t)
+    |> prop_of |> Logic.dest_equals |> snd
+
+fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
+
+fun dest_hhf ctxt t = 
+    let 
+      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
+    in
+      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
+    end
+
+
+fun mk_scheme' ctxt cases concl =
+    let
+      fun mk_branch concl =
+          let
+            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+            val (P, xs) = strip_comb Pxs
+          in
+            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
+          end
+
+      val (branches, cases') = (* correction *)
+          case Logic.dest_conjunction_list concl of
+            [conc] => 
+            let 
+              val _ $ Pxs = Logic.strip_assums_concl conc
+              val (P, _) = strip_comb Pxs
+              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
+              val concl' = fold_rev (curry Logic.mk_implies) conds conc
+            in
+              ([mk_branch concl'], cases')
+            end
+          | concls => (map mk_branch concls, cases)
+
+      fun mk_case premise =
+          let
+            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
+            val (P, lhs) = strip_comb Plhs
+                                
+            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
+
+            fun mk_rcinfo pr =
+                let
+                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+                  val (P', rcs) = strip_comb Phyp
+                in
+                  (bidx P', Gvs, Gas, rcs)
+                end
+                
+            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
+
+            val (gs, rcprs) = 
+                take_prefix (not o Term.exists_subterm is_pred) prems
+          in
+            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
+          end
+
+      fun PT_of (SchemeBranch { xs, ...}) =
+            foldr1 HOLogic.mk_prodT (map snd xs)
+
+      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
+    in
+      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
+    end
+
+
+
+fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
+    let
+      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
+      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
+
+      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
+      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
+      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
+                       
+      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
+          HOLogic.mk_Trueprop Pbool
+                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
+                                 (xs' ~~ lhs)
+                     |> fold_rev (curry Logic.mk_implies) gs
+                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+    in
+      HOLogic.mk_Trueprop Pbool
+       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
+       |> fold_rev (curry Logic.mk_implies) Cs'
+       |> fold_rev (Logic.all o Free) ws
+       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
+       |> mk_forall_rename ("P", Pbool)
+    end
+
+fun mk_wf ctxt R (IndScheme {T, ...}) =
+    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
+
+fun mk_ineqs R (IndScheme {T, cases, branches}) =
+    let
+      fun inject i ts =
+          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
+
+      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
+
+      fun mk_pres bdx args = 
+          let
+            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
+            fun replace (x, v) t = betapply (lambda (Free x) t, v)
+            val Cs' = map (fold replace (xs ~~ args)) Cs
+            val cse = 
+                HOLogic.mk_Trueprop thesis
+                |> fold_rev (curry Logic.mk_implies) Cs'
+                |> fold_rev (Logic.all o Free) ws
+          in
+            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
+          end
+
+      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
+          let
+            fun g (bidx', Gvs, Gas, rcarg) =
+                let val export = 
+                         fold_rev (curry Logic.mk_implies) Gas
+                         #> fold_rev (curry Logic.mk_implies) gs
+                         #> fold_rev (Logic.all o Free) Gvs
+                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
+                in
+                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
+                 |> HOLogic.mk_Trueprop
+                 |> export,
+                 mk_pres bidx' rcarg
+                 |> export
+                 |> Logic.all thesis)
+                end
+          in
+            map g rs
+          end
+    in
+      map f cases
+    end
+
+
+fun mk_hol_imp a b = HOLogic.imp $ a $ b
+
+fun mk_ind_goal thy branches =
+    let
+      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
+          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
+          |> fold_rev (curry Logic.mk_implies) Cs
+          |> fold_rev (Logic.all o Free) ws
+          |> term_conv thy ind_atomize
+          |> ObjectLogic.drop_judgment thy
+          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
+    in
+      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
+    end
+
+
+fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
+    let
+      val n = length branches
+
+      val scases_idx = map_index I scases
+
+      fun inject i ts =
+          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
+      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
+
+      val thy = ProofContext.theory_of ctxt
+      val cert = cterm_of thy 
+
+      val P_comp = mk_ind_goal thy branches
+
+      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
+      val ihyp = Term.all T $ Abs ("z", T, 
+               Logic.mk_implies
+                 (HOLogic.mk_Trueprop (
+                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
+                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
+                    $ R),
+                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
+           |> cert
+
+      val aihyp = assume ihyp
+
+     (* Rule for case splitting along the sum types *)
+      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
+      val pats = map_index (uncurry inject) xss
+      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+
+      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
+          let
+            val fxs = map Free xs
+            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
+                             
+            val C_hyps = map (cert #> assume) Cs
+
+            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
+                                            |> split_list
+                           
+            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
+                let
+                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
+                           
+                  val cqs = map (cert o Free) qs
+                  val ags = map (assume o cert) gs
+                            
+                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
+                  val sih = full_simplify replace_x_ss aihyp
+                            
+                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
+                      let
+                        val cGas = map (assume o cert) Gas
+                        val cGvs = map (cert o Free) Gvs
+                        val import = fold forall_elim (cqs @ cGvs)
+                                     #> fold Thm.elim_implies (ags @ cGas)
+                        val ipres = pres
+                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
+                                     |> import
+                      in
+                        sih |> forall_elim (cert (inject idx rcargs))
+                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
+                            |> Conv.fconv_rule sum_prod_conv
+                            |> Conv.fconv_rule ind_rulify
+                            |> (fn th => th COMP ipres) (* P rs *)
+                            |> fold_rev (implies_intr o cprop_of) cGas
+                            |> fold_rev forall_intr cGvs
+                      end
+                      
+                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
+                               
+                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
+                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
+                             |> fold_rev (curry Logic.mk_implies) gs
+                             |> fold_rev (Logic.all o Free) qs
+                             |> cert
+                             
+                  val Plhs_to_Pxs_conv = 
+                      foldl1 (uncurry Conv.combination_conv) 
+                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
+
+                  val res = assume step
+                                   |> fold forall_elim cqs
+                                   |> fold Thm.elim_implies ags
+                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
+                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
+                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
+                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
+                in
+                  (res, (cidx, step))
+                end
+
+            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
+
+            val bstep = complete_thm
+                |> forall_elim (cert (list_comb (P, fxs)))
+                |> fold (forall_elim o cert) (fxs @ map Free ws)
+                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
+                |> fold Thm.elim_implies cases (* P xs *)
+                |> fold_rev (implies_intr o cprop_of) C_hyps
+                |> fold_rev (forall_intr o cert o Free) ws
+
+            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
+                     |> Goal.init
+                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+                         THEN CONVERSION ind_rulify 1)
+                     |> Seq.hd
+                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
+                     |> Goal.finish ctxt
+                     |> implies_intr (cprop_of branch_hyp)
+                     |> fold_rev (forall_intr o cert) fxs
+          in
+            (Pxs, steps)
+          end
+
+      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
+                              |> apsnd flat
+                           
+      val istep = sum_split_rule
+                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
+                |> implies_intr ihyp
+                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
+         
+      val induct_rule =
+          @{thm "wf_induct_rule"}
+            |> (curry op COMP) wf_thm 
+            |> (curry op COMP) istep
+
+      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
+    in
+      (steps_sorted, induct_rule)
+    end
+
+
+fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
+(SUBGOAL (fn (t, i) =>
+  let
+    val (ctxt', _, cases, concl) = dest_hhf ctxt t
+    val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
+(*     val _ = tracing (makestring scheme)*)
+    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
+    val R = Free (Rn, mk_relT ST)
+    val x = Free (xn, ST)
+    val cert = cterm_of (ProofContext.theory_of ctxt)
+
+    val ineqss = mk_ineqs R scheme
+                   |> map (map (pairself (assume o cert)))
+    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
+    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
+
+    val (descent, pres) = split_list (flat ineqss)
+    val newgoals = complete @ pres @ wf_thm :: descent 
+
+    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
+
+    fun project (i, SchemeBranch {xs, ...}) =
+        let
+          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
+        in
+          indthm |> Drule.instantiate' [] [SOME inst]
+                 |> simplify SumTree.sumcase_split_ss
+                 |> Conv.fconv_rule ind_rulify
+(*                 |> (fn thm => (tracing (makestring thm); thm))*)
+        end                  
+
+    val res = Conjunction.intr_balanced (map_index project branches)
+                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
+                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
+
+    val nbranches = length branches
+    val npres = length pres
+  in
+    Thm.compose_no_flatten false (res, length newgoals) i
+    THEN term_tac (i + nbranches + npres)
+    THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
+    THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
+  end))
+
+
+fun induction_schema_tac ctxt =
+  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+
+val setup =
+  Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
+    "proves an induction principle"
+
+end
--- a/src/HOL/Tools/Function/induction_scheme.ML	Sat Nov 07 08:17:53 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,405 +0,0 @@
-(*  Title:      HOL/Tools/Function/induction_scheme.ML
-    Author:     Alexander Krauss, TU Muenchen
-
-A method to prove induction schemes.
-*)
-
-signature INDUCTION_SCHEME =
-sig
-  val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
-                   -> Proof.context -> thm list -> tactic
-  val induct_scheme_tac : Proof.context -> thm list -> tactic
-  val setup : theory -> theory
-end
-
-
-structure Induction_Scheme : INDUCTION_SCHEME =
-struct
-
-open Function_Lib
-
-
-type rec_call_info = int * (string * typ) list * term list * term list
-
-datatype scheme_case =
-  SchemeCase of
-  {
-   bidx : int,
-   qs: (string * typ) list,
-   oqnames: string list,
-   gs: term list,
-   lhs: term list,
-   rs: rec_call_info list
-  }
-
-datatype scheme_branch = 
-  SchemeBranch of
-  {
-   P : term,
-   xs: (string * typ) list,
-   ws: (string * typ) list,
-   Cs: term list
-  }
-
-datatype ind_scheme =
-  IndScheme of
-  {
-   T: typ, (* sum of products *)
-   branches: scheme_branch list,
-   cases: scheme_case list
-  }
-
-val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
-val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
-
-fun meta thm = thm RS eq_reflection
-
-val sum_prod_conv = MetaSimplifier.rewrite true 
-                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
-
-fun term_conv thy cv t = 
-    cv (cterm_of thy t)
-    |> prop_of |> Logic.dest_equals |> snd
-
-fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
-
-fun dest_hhf ctxt t = 
-    let 
-      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
-    in
-      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
-    end
-
-
-fun mk_scheme' ctxt cases concl =
-    let
-      fun mk_branch concl =
-          let
-            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
-            val (P, xs) = strip_comb Pxs
-          in
-            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
-          end
-
-      val (branches, cases') = (* correction *)
-          case Logic.dest_conjunction_list concl of
-            [conc] => 
-            let 
-              val _ $ Pxs = Logic.strip_assums_concl conc
-              val (P, _) = strip_comb Pxs
-              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
-              val concl' = fold_rev (curry Logic.mk_implies) conds conc
-            in
-              ([mk_branch concl'], cases')
-            end
-          | concls => (map mk_branch concls, cases)
-
-      fun mk_case premise =
-          let
-            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
-            val (P, lhs) = strip_comb Plhs
-                                
-            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
-
-            fun mk_rcinfo pr =
-                let
-                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
-                  val (P', rcs) = strip_comb Phyp
-                in
-                  (bidx P', Gvs, Gas, rcs)
-                end
-                
-            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
-
-            val (gs, rcprs) = 
-                take_prefix (not o Term.exists_subterm is_pred) prems
-          in
-            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
-          end
-
-      fun PT_of (SchemeBranch { xs, ...}) =
-            foldr1 HOLogic.mk_prodT (map snd xs)
-
-      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
-    in
-      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
-    end
-
-
-
-fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
-    let
-      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
-      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
-
-      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
-      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
-      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
-                       
-      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
-          HOLogic.mk_Trueprop Pbool
-                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
-                                 (xs' ~~ lhs)
-                     |> fold_rev (curry Logic.mk_implies) gs
-                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
-    in
-      HOLogic.mk_Trueprop Pbool
-       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
-       |> fold_rev (curry Logic.mk_implies) Cs'
-       |> fold_rev (Logic.all o Free) ws
-       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
-       |> mk_forall_rename ("P", Pbool)
-    end
-
-fun mk_wf ctxt R (IndScheme {T, ...}) =
-    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
-
-fun mk_ineqs R (IndScheme {T, cases, branches}) =
-    let
-      fun inject i ts =
-          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
-
-      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
-
-      fun mk_pres bdx args = 
-          let
-            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
-            fun replace (x, v) t = betapply (lambda (Free x) t, v)
-            val Cs' = map (fold replace (xs ~~ args)) Cs
-            val cse = 
-                HOLogic.mk_Trueprop thesis
-                |> fold_rev (curry Logic.mk_implies) Cs'
-                |> fold_rev (Logic.all o Free) ws
-          in
-            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
-          end
-
-      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
-          let
-            fun g (bidx', Gvs, Gas, rcarg) =
-                let val export = 
-                         fold_rev (curry Logic.mk_implies) Gas
-                         #> fold_rev (curry Logic.mk_implies) gs
-                         #> fold_rev (Logic.all o Free) Gvs
-                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
-                in
-                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
-                 |> HOLogic.mk_Trueprop
-                 |> export,
-                 mk_pres bidx' rcarg
-                 |> export
-                 |> Logic.all thesis)
-                end
-          in
-            map g rs
-          end
-    in
-      map f cases
-    end
-
-
-fun mk_hol_imp a b = HOLogic.imp $ a $ b
-
-fun mk_ind_goal thy branches =
-    let
-      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
-          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
-          |> fold_rev (curry Logic.mk_implies) Cs
-          |> fold_rev (Logic.all o Free) ws
-          |> term_conv thy ind_atomize
-          |> ObjectLogic.drop_judgment thy
-          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
-    in
-      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
-    end
-
-
-fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
-    let
-      val n = length branches
-
-      val scases_idx = map_index I scases
-
-      fun inject i ts =
-          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
-      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
-
-      val thy = ProofContext.theory_of ctxt
-      val cert = cterm_of thy 
-
-      val P_comp = mk_ind_goal thy branches
-
-      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-      val ihyp = Term.all T $ Abs ("z", T, 
-               Logic.mk_implies
-                 (HOLogic.mk_Trueprop (
-                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
-                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
-                    $ R),
-                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
-           |> cert
-
-      val aihyp = assume ihyp
-
-     (* Rule for case splitting along the sum types *)
-      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
-      val pats = map_index (uncurry inject) xss
-      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
-
-      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
-          let
-            val fxs = map Free xs
-            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
-                             
-            val C_hyps = map (cert #> assume) Cs
-
-            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
-                                            |> split_list
-                           
-            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
-                let
-                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
-                           
-                  val cqs = map (cert o Free) qs
-                  val ags = map (assume o cert) gs
-                            
-                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
-                  val sih = full_simplify replace_x_ss aihyp
-                            
-                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
-                      let
-                        val cGas = map (assume o cert) Gas
-                        val cGvs = map (cert o Free) Gvs
-                        val import = fold forall_elim (cqs @ cGvs)
-                                     #> fold Thm.elim_implies (ags @ cGas)
-                        val ipres = pres
-                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
-                                     |> import
-                      in
-                        sih |> forall_elim (cert (inject idx rcargs))
-                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
-                            |> Conv.fconv_rule sum_prod_conv
-                            |> Conv.fconv_rule ind_rulify
-                            |> (fn th => th COMP ipres) (* P rs *)
-                            |> fold_rev (implies_intr o cprop_of) cGas
-                            |> fold_rev forall_intr cGvs
-                      end
-                      
-                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
-                               
-                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
-                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
-                             |> fold_rev (curry Logic.mk_implies) gs
-                             |> fold_rev (Logic.all o Free) qs
-                             |> cert
-                             
-                  val Plhs_to_Pxs_conv = 
-                      foldl1 (uncurry Conv.combination_conv) 
-                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
-
-                  val res = assume step
-                                   |> fold forall_elim cqs
-                                   |> fold Thm.elim_implies ags
-                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
-                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
-                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
-                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
-                in
-                  (res, (cidx, step))
-                end
-
-            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
-
-            val bstep = complete_thm
-                |> forall_elim (cert (list_comb (P, fxs)))
-                |> fold (forall_elim o cert) (fxs @ map Free ws)
-                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
-                |> fold Thm.elim_implies cases (* P xs *)
-                |> fold_rev (implies_intr o cprop_of) C_hyps
-                |> fold_rev (forall_intr o cert o Free) ws
-
-            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
-                     |> Goal.init
-                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
-                         THEN CONVERSION ind_rulify 1)
-                     |> Seq.hd
-                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
-                     |> Goal.finish ctxt
-                     |> implies_intr (cprop_of branch_hyp)
-                     |> fold_rev (forall_intr o cert) fxs
-          in
-            (Pxs, steps)
-          end
-
-      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
-                              |> apsnd flat
-                           
-      val istep = sum_split_rule
-                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
-                |> implies_intr ihyp
-                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
-         
-      val induct_rule =
-          @{thm "wf_induct_rule"}
-            |> (curry op COMP) wf_thm 
-            |> (curry op COMP) istep
-
-      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
-    in
-      (steps_sorted, induct_rule)
-    end
-
-
-fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
-(SUBGOAL (fn (t, i) =>
-  let
-    val (ctxt', _, cases, concl) = dest_hhf ctxt t
-    val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-(*     val _ = tracing (makestring scheme)*)
-    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
-    val R = Free (Rn, mk_relT ST)
-    val x = Free (xn, ST)
-    val cert = cterm_of (ProofContext.theory_of ctxt)
-
-    val ineqss = mk_ineqs R scheme
-                   |> map (map (pairself (assume o cert)))
-    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
-    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
-
-    val (descent, pres) = split_list (flat ineqss)
-    val newgoals = complete @ pres @ wf_thm :: descent 
-
-    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
-
-    fun project (i, SchemeBranch {xs, ...}) =
-        let
-          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
-        in
-          indthm |> Drule.instantiate' [] [SOME inst]
-                 |> simplify SumTree.sumcase_split_ss
-                 |> Conv.fconv_rule ind_rulify
-(*                 |> (fn thm => (tracing (makestring thm); thm))*)
-        end                  
-
-    val res = Conjunction.intr_balanced (map_index project branches)
-                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
-                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
-
-    val nbranches = length branches
-    val npres = length pres
-  in
-    Thm.compose_no_flatten false (res, length newgoals) i
-    THEN term_tac (i + nbranches + npres)
-    THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
-    THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
-  end))
-
-
-fun induct_scheme_tac ctxt =
-  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
-
-val setup =
-  Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac))
-    "proves an induction principle"
-
-end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -37,8 +37,7 @@
   map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
     ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
 
-(* TODO: *)
-fun overload_const thy s = s
+fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
 
 fun map_specs f specs =
   map (fn (s, ths) => (s, f ths)) specs
@@ -87,8 +86,8 @@
     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) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4
-    val intross6 = map_specs (map (expand_tuples thy''')) intross4
+    val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
+    val intross6 = map_specs (map (expand_tuples thy''')) intross5
     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'''
@@ -121,7 +120,8 @@
       skip_proof = chk "skip_proof",
       inductify = chk "inductify",
       random = chk "random",
-      depth_limited = chk "depth_limited"
+      depth_limited = chk "depth_limited",
+      annotated = chk "annotated"
     }
   end
 
@@ -149,11 +149,14 @@
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
-  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"]
+  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
+  "annotated"]
 
 local structure P = OuterParse
 in
 
+(* Parser for mode annotations *)
+
 (*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*)
 datatype raw_argmode = Argmode of string | Argmode_Tuple of string list
 
@@ -184,16 +187,42 @@
   Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
     P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE
 
-val scan_params =
+(* Parser for options *)
+
+val scan_options =
   let
-    val scan_bool_param = foldl1 (op ||) (map Args.$$$ bool_options)
+    val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
   in
-    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_param --| P.$$$ "]") []
+    Scan.optional (P.$$$ "[" |-- P.enum1 "," scan_bool_option --| P.$$$ "]") []
   end
 
+val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME)
+
+val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
+  P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE
+
+val value_options =
+  let
+    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
+    val random = Scan.optional (Args.$$$ "random" >> K true) false
+    val annotated = Scan.optional (Args.$$$ "annotated" >> K true) false
+  in
+    Scan.optional (P.$$$ "[" |-- depth_limit -- (random -- annotated) --| P.$$$ "]")
+      (NONE, (false, false))
+  end
+
+(* code_pred command and values command *)
+
 val _ = OuterSyntax.local_theory_to_proof "code_pred"
   "prove equations for predicate specified by intro/elim rules"
-  OuterKeyword.thy_goal (opt_modes -- scan_params -- P.term_group >> code_pred_cmd)
+  OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
+  (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+    >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.no_timing o Toplevel.keep
+        (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
 
 end
 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -170,7 +170,8 @@
 
   inductify : bool,
   random : bool,
-  depth_limited : bool
+  depth_limited : bool,
+  annotated : bool
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
@@ -185,6 +186,7 @@
 fun is_inductify (Options opt) = #inductify opt
 fun is_random (Options opt) = #random opt
 fun is_depth_limited (Options opt) = #depth_limited opt
+fun is_annotated (Options opt) = #annotated opt
 
 val default_options = Options {
   expected_modes = NONE,
@@ -198,7 +200,8 @@
   
   inductify = false,
   random = false,
-  depth_limited = false
+  depth_limited = false,
+  annotated = false
 }
 
 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -6,9 +6,11 @@
 
 signature PREDICATE_COMPILE_CORE =
 sig
-  val setup: theory -> theory
-  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
+  val setup : theory -> theory
+  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
+  val values_cmd : string list -> Predicate_Compile_Aux.smode option list option
+    -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm * int) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
@@ -19,20 +21,21 @@
   val modes_of: theory -> string -> Predicate_Compile_Aux.mode list
   val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
   val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
-  val generator_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
-  val generator_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
+  val random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
+  val random_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
   val all_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
-  val all_generator_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
-  val intros_of: theory -> string -> thm list
-  val nparams_of: theory -> string -> int
-  val add_intro: thm -> theory -> theory
-  val set_elim: thm -> theory -> theory
+  val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
+  val intros_of : theory -> string -> thm list
+  val nparams_of : theory -> string -> int
+  val add_intro : thm -> theory -> theory
+  val set_elim : thm -> theory -> theory
   val set_nparams : string -> int -> theory -> theory
-  val print_stored_rules: theory -> unit
-  val print_all_modes: theory -> unit
+  val print_stored_rules : theory -> unit
+  val print_all_modes : theory -> unit
   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 random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
+    option Unsynchronized.ref
   val code_pred_intros_attrib : attribute
   (* used by Quickcheck_Generator *) 
   (* temporary for testing of the compilation *)
@@ -51,7 +54,9 @@
   val randompred_compfuns : compilation_funs
   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
+  val add_depth_limited_equations : Predicate_Compile_Aux.options
+    -> string list -> theory -> theory
+  val mk_tracing : string -> term -> term
 end;
 
 structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
@@ -116,6 +121,10 @@
   Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
+fun mk_tracing s t =
+  Const(@{const_name Code_Evaluation.tracing},
+    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
+
 (* destruction of intro rules *)
 
 (* FIXME: look for other place where this functionality was used before *)
@@ -197,17 +206,22 @@
   intros : thm list,
   elim : thm option,
   nparams : int,
-  functions : (mode * predfun_data) list,
-  generators : (mode * function_data) list,
-  depth_limited_functions : (mode * function_data) list 
+  functions : bool * (mode * predfun_data) list,
+  random_functions : bool * (mode * function_data) list,
+  depth_limited_functions : bool * (mode * function_data) list,
+  annotated_functions : bool * (mode * function_data) list
 };
 
 fun rep_pred_data (PredData data) = data;
-fun mk_pred_data ((intros, elim, nparams), (functions, generators, depth_limited_functions)) =
+fun mk_pred_data ((intros, elim, nparams),
+  (functions, random_functions, depth_limited_functions, annotated_functions)) =
   PredData {intros = intros, elim = elim, nparams = nparams,
-    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)))
+    functions = functions, random_functions = random_functions,
+    depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions}
+fun map_pred_data f (PredData {intros, elim, nparams,
+  functions, random_functions, depth_limited_functions, annotated_functions}) =
+  mk_pred_data (f ((intros, elim, nparams), (functions, random_functions,
+    depth_limited_functions, annotated_functions)))
 
 fun eq_option eq (NONE, NONE) = true
   | eq_option eq (SOME x, SOME y) = eq (x, y)
@@ -250,22 +264,19 @@
 
 val nparams_of = #nparams oo the_pred_data
 
-val modes_of = (map fst) o #functions oo the_pred_data
+val modes_of = (map fst) o snd o #functions oo the_pred_data
 
-val depth_limited_modes_of = (map fst) o #depth_limited_functions oo the_pred_data
-
-val random_modes_of = (map fst) o #generators oo the_pred_data
-  
 fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 
 
-val is_compiled = not o null o #functions oo the_pred_data
+val defined_functions = fst o #functions oo the_pred_data
 
 fun lookup_predfun_data thy name mode =
-  Option.map rep_predfun_data (AList.lookup (op =)
-  (#functions (the_pred_data thy name)) mode)
+  Option.map rep_predfun_data
+    (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode)
 
 fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
-  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
+  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^
+    " of predicate " ^ name)
    | SOME data => data;
 
 val predfun_name_of = #name ooo the_predfun_data
@@ -276,31 +287,54 @@
 
 val predfun_elim_of = #elim ooo the_predfun_data
 
-fun lookup_generator_data thy name mode = 
-  Option.map rep_function_data (AList.lookup (op =)
-  (#generators (the_pred_data thy name)) mode)
+fun lookup_random_function_data thy name mode =
+  Option.map rep_function_data
+  (AList.lookup (op =) (snd (#random_functions (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)
+fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of
+     NONE => error ("No random function defined for mode " ^ string_of_mode mode ^
+       " of predicate " ^ name)
    | SOME data => data
 
-val generator_name_of = #name ooo the_generator_data
+val random_function_name_of = #name ooo the_random_function_data
+
+val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data
 
-val generator_modes_of = (map fst) o #generators oo the_pred_data
+val defined_random_functions = fst o #random_functions oo the_pred_data
 
-fun all_generator_modes_of thy =
-  map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 
+fun all_random_modes_of thy =
+  map (fn name => (name, random_modes_of thy name)) (all_preds_of thy) 
 
 fun lookup_depth_limited_function_data thy name mode =
-  Option.map rep_function_data (AList.lookup (op =)
-  (#depth_limited_functions (the_pred_data thy name)) mode)
+  Option.map rep_function_data
+    (AList.lookup (op =) (snd (#depth_limited_functions (the_pred_data thy name))) 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 depth_limited_function_name_of = #name ooo the_depth_limited_function_data
 
-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
+val depth_limited_modes_of = (map fst) o snd o #depth_limited_functions oo the_pred_data
+
+val defined_depth_limited_functions = fst o #depth_limited_functions oo the_pred_data
+
+fun lookup_annotated_function_data thy name mode =
+  Option.map rep_function_data
+    (AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode)
+
+fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode
+  of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode
     ^ " of predicate " ^ name)
    | SOME data => data
 
-val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
+val annotated_function_name_of = #name ooo the_annotated_function_data
+
+val annotated_modes_of = (map fst) o snd o #annotated_functions oo the_pred_data
+
+val defined_annotated_functions = fst o #annotated_functions oo the_pred_data
 
 (* diagnostic display functions *)
 
@@ -555,6 +589,16 @@
 
 fun expand_tuples_elim th = th
 
+(* updaters *)
+
+fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4)
+fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4)
+fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4)
+fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4)
+fun appair f g (x, y) = (f x, g x)
+
+val no_compilation = ((false, []), (false, []), (false, []), (false, []))
+
 fun fetch_pred_data thy name =
   case try (Inductive.the_inductive (ProofContext.init thy)) name of
     SOME (info as (_, result)) => 
@@ -576,19 +620,13 @@
           (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                                                                    
+        mk_pred_data ((intros, SOME elim, nparams), no_compilation)
+      end
   | NONE => error ("No such predicate: " ^ quote name)
 
-(* updaters *)
-
-fun apfst3 f (x, y, z) =  (f x, y, z)
-fun apsnd3 f (x, y, z) =  (x, f y, z)
-fun aptrd3 f (x, y, z) =  (x, y, f z)
-
 fun add_predfun name mode data =
   let
-    val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
+    val add = (apsnd o apfst4) (fn (x, y) => (true, cons (mode, mk_predfun_data data) y))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate thy name =
@@ -599,7 +637,8 @@
     val intros = (#intros o rep_pred_data) value
   in
     fold Term.add_const_names (map Thm.prop_of intros) []
-      |> filter (fn c => (not (c = key)) andalso (is_inductive_predicate thy c orelse is_registered thy c))
+      |> filter (fn c => (not (c = key)) andalso
+        (is_inductive_predicate thy c orelse is_registered thy c))
   end;
 
 
@@ -637,8 +676,9 @@
          (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
      | NONE =>
        let
-         val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
-       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;
+         val nparams = the_default (guess_nparams T)
+           (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
+       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end;
   in PredData.map cons_intro thy end
 
 fun set_elim thm = let
@@ -659,7 +699,8 @@
   in
     if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
       PredData.map
-        (Graph.new_node (constname, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
+        (Graph.new_node (constname,
+          mk_pred_data ((intros, SOME elim, nparams), no_compilation))) thy
     else thy
   end
 
@@ -679,16 +720,24 @@
       (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 = 
+fun set_random_function_name pred mode name = 
   let
-    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
+    val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
 
 fun set_depth_limited_function_name pred mode name = 
   let
-    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
+    val set = (apsnd o aptrd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
+  in
+    PredData.map (Graph.map_node pred (map_pred_data set))
+  end
+
+fun set_annotated_function_name pred mode name =
+  let
+    val set = (apsnd o apfourth4)
+      (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
   in
     PredData.map (Graph.map_node pred (map_pred_data set))
   end
@@ -715,19 +764,6 @@
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 
-fun 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 NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
-  in
-    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
-  end;
-
-fun mk_fun_of compfuns thy (name, T) mode = 
-  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
-
-
 structure PredicateCompFuns =
 struct
 
@@ -815,9 +851,9 @@
 fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
-val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT, mk_bot = mk_bot,
-    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
-    mk_map = mk_map};
+val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
+    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+    mk_not = mk_not, mk_map = mk_map};
 
 end;
 (* for external use with interactive mode *)
@@ -829,25 +865,41 @@
     val T = dest_randomT (fastype_of random)
   in
     Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->
-      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> 
+      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
       RandomPredCompFuns.mk_randompredT T) $ random
   end;
 
+(* function types and names of different compilations *)
+
+fun 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 NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
+  in
+    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
+  end;
+
 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 => depth_limited_funT_of 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 bool}, @{typ "code_numeral"}])
       ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
-  end;  
+  end;
 
-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, depth_limited_funT_of compfuns mode T)
+fun random_function_funT_of (iss, is) T =
+  let
+    val Ts = binder_types T
+    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
+    val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs
+  in
+    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
+      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
+  end
 
 (* Mode analysis *)
 
@@ -860,7 +912,8 @@
     fun check t = (case strip_comb t of
         (Free _, []) => true
       | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
-            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+            (SOME (i, Tname), Type (Tname', _)) =>
+              length ts = i andalso Tname = Tname' andalso forall check ts
           | _ => false)
       | _ => false)
   in check end;
@@ -993,11 +1046,14 @@
                   (filter_out (equal p) ps)
               | _ =>
                   let 
-                    val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length))
+                    val all_generator_vs = all_subsets (subtract (op =) vs prem_vs)
+                      |> sort (int_ord o (pairself length))
                   in
                     case (find_first (fn generator_vs => is_some
-                      (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)
+                      (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 => NONE
                   end)
@@ -1073,14 +1129,14 @@
   let
     val prednames = map fst clauses
     val extra_modes' = all_modes_of thy
-    val gen_modes = all_generator_modes_of thy
+    val gen_modes = all_random_modes_of thy
       |> filter_out (fn (name, _) => member (op =) prednames name)
     val starting_modes = remove_from extra_modes' all_modes
     fun eq_mode (m1, m2) = (m1 = m2)
     val modes =
       fixp (fn modes =>
-        map (check_modes_pred options true thy param_vs clauses extra_modes' (gen_modes @ modes)) modes)
-         starting_modes
+        map (check_modes_pred options true thy param_vs clauses extra_modes'
+          (gen_modes @ modes)) modes) starting_modes
   in
     AList.join (op =)
     (fn _ => fn ((mps1, mps2)) =>
@@ -1169,7 +1225,9 @@
 
 datatype comp_modifiers = Comp_Modifiers of
 {
-  const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+  function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+  set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory,
+  function_name_prefix : string,
   funT_of : compilation_funs -> mode -> typ -> typ,
   additional_arguments : string list -> term list,
   wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
@@ -1178,7 +1236,9 @@
 
 fun dest_comp_modifiers (Comp_Modifiers c) = c
 
-val const_name_of = #const_name_of o dest_comp_modifiers
+val function_name_of = #function_name_of o dest_comp_modifiers
+val set_function_name = #set_function_name o dest_comp_modifiers
+val function_name_prefix = #function_name_prefix o dest_comp_modifiers
 val funT_of = #funT_of o dest_comp_modifiers
 val additional_arguments = #additional_arguments o dest_comp_modifiers
 val wrap_compilation = #wrap_compilation o dest_comp_modifiers
@@ -1200,7 +1260,8 @@
       | map_params t = t
     in map_aterms map_params arg end
 
-fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t =
+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'' =
@@ -1243,7 +1304,7 @@
      val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
      val f' =
        case f of
-         Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode,
+         Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode,
            Comp_Mod.funT_of compilation_modifiers compfuns mode T)
        | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T)
        | _ => error ("PredicateCompiler: illegal parameter term")
@@ -1251,23 +1312,26 @@
      list_comb (f', params' @ args')
    end
 
-fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments =
+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' = Comp_Mod.const_name_of compilation_modifiers thy name mode
+         val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode
          val T' = Comp_Mod.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, Comp_Mod.funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments)
+    list_comb (Free (name, Comp_Mod.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) =
+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
+    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
@@ -1302,10 +1366,11 @@
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us;
-                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
-                     thy param_vs iss) in_ts
+                   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'
+                     compile_expr compilation_modifiers compfuns thy
+                       (mode, t) in_ts additional_arguments'
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1313,10 +1378,11 @@
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us
-                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
-                     thy param_vs iss) 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')
+                     (compile_expr compilation_modifiers compfuns thy
+                       (mode, t) in_ts additional_arguments')
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
@@ -1351,12 +1417,14 @@
     val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T)
     val (Us1, Us2) = split_smodeT (snd mode) Ts2
     val Ts1' =
-      map2 (fn NONE => I | SOME is => Comp_Mod.funT_of compilation_modifiers compfuns ([], is)) (fst mode) Ts1
+      map2 (fn NONE => I | SOME is => Comp_Mod.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"
-             | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))]
+             | [T] => [Free (Name.variant (all_vs @ param_vs)
+               ("x" ^ string_of_int i), nth Ts2 (i - 1))]
              | Ts => let
                val vnames = Name.variant_list (all_vs @ param_vs)
                 (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j)
@@ -1365,16 +1433,18 @@
                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 additional_arguments = Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
+    val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
+      (all_vs @ param_vs)
     val cl_ts =
       map (compile_clause compilation_modifiers compfuns
         thy all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts)) moded_cls;
-    val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
+    val compilation = Comp_Mod.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 (Comp_Mod.const_name_of compilation_modifiers thy s mode,
+      Const (Comp_Mod.function_name_of compilation_modifiers thy s mode,
         Comp_Mod.funT_of compilation_modifiers compfuns mode T)
   in
     HOLogic.mk_Trueprop
@@ -1399,7 +1469,8 @@
   val Ts = binder_types (fastype_of pred)
   val funtrm = Const (mode_id, funT)
   val (Ts1, Ts2) = chop (length iss) Ts;
-  val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
+  val Ts1' =
+    map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
   val param_names = Name.variant_list []
     (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1)));
   val params = map Free (param_names ~~ Ts1')
@@ -1440,14 +1511,12 @@
   val simprules = [defthm, @{thm eval_pred},
     @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
   val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
-  val introthm =
-    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y"]) [] introtrm
-      (fn _ => unfolddef_tac)
+  val introthm = Goal.prove (ProofContext.init thy)
+    (argnames @ param_names @ param_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
   val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
   val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
-  val elimthm =
-    Goal.prove (ProofContext.init thy) (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm
-      (fn _ => unfolddef_tac)
+  val elimthm = Goal.prove (ProofContext.init thy)
+    (argnames @ param_names @ param_names' @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
 in
   (introthm, elimthm)
 end;
@@ -1455,7 +1524,8 @@
 fun create_constname_of_mode thy prefix name mode = 
   let
     fun string_of_mode mode = if null mode then "0"
-      else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
+      else space_implode "_"
+        (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
         ^ space_implode "p" (map string_of_int pis)) mode)
     val HOmode = space_implode "_and_"
       (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
@@ -1529,7 +1599,9 @@
                val xin = Free (name_in, HOLogic.mk_tupleT Tins)
                val xout = Free (name_out, HOLogic.mk_tupleT Touts)
                val xarg = mk_arg xin xout pis T
-             in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
+             in
+               (((if null Tins then [] else [xin],
+               if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
              end
       val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
       val (xinout, xargs) = split_list xinoutargs
@@ -1563,46 +1635,22 @@
     fold create_definition modes thy
   end;
 
-fun create_definitions_of_depth_limited_functions preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns 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 "depth_limited_" name mode
-        val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T
+        val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
+        val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+        val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_depth_limited_function_name name mode mode_cname 
+        |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname
       end;
   in
     fold create_definition modes thy
   end;
 
-fun generator_funT_of (iss, is) T =
-  let
-    val Ts = binder_types T
-    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => generator_funT_of ([], is) | NONE => I) iss paramTs
-  in
-    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
-      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
-  end
-
-fun random_create_definitions 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 "gen_" name mode
-        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
-      end;
-  in
-    fold create_definition modes thy
-  end;
-  
 (* Proving equivalence of term *)
 
 fun is_Type (Type _) = true
@@ -1752,7 +1800,8 @@
             in
               rtac @{thm bindI} 1
               THEN (if (is_some name) then
-                  simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1
+                  simp_tac (HOL_basic_ss addsimps
+                    [predfun_definition_of thy (the name) (iss, is)]) 1
                   THEN rtac @{thm not_predI} 1
                   THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
                   THEN (REPEAT_DETERM (atac 1))
@@ -1823,14 +1872,16 @@
         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 (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 (HOLogic.mk_tuple out_ts)
-    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
+    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
+    THEN (etac @{thm botE} 2))))
   end
 
 (* VERY LARGE SIMILIRATIY to function prove_param 
@@ -1910,7 +1961,8 @@
       THEN (print_tac "state before assumption matching")
       THEN (REPEAT (atac 1 ORELSE 
          (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
-           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
+           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
+             @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
           THEN print_tac "state after simp_tac:"))))
     | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
       let
@@ -1932,7 +1984,8 @@
             print_tac "before neg prem 2"
             THEN etac @{thm bindE} 1
             THEN (if is_some name then
-                full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 
+                full_simp_tac (HOL_basic_ss addsimps
+                  [predfun_definition_of thy (the name) (iss, is)]) 1
                 THEN etac @{thm not_predE} 1
                 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
                 THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
@@ -2027,9 +2080,10 @@
 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          
+  | (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))) 
+    | 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
@@ -2044,14 +2098,17 @@
     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, 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 extra_modes = all_modes_of thy
+      |> filter_out (fn (name, _) => member (op =) prednames name)
     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))
+            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)))))
@@ -2087,12 +2144,13 @@
               [] => [(i + 1, NONE)]
             | [U] => [(i + 1, NONE)]
             | Us =>  (i + 1, NONE) ::
-              (map (pair (i + 1) o SOME) (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
+              (map (pair (i + 1) o SOME)
+                (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
           Ts)
       in
         cprod (cprods (map (fn T => case strip_type T of
-          (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts),
-           all_smodes_of_typs Us)
+          (Rs as _ :: _, Type ("bool", [])) =>
+            map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us)
       end
     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;
@@ -2180,7 +2238,7 @@
   {
   compile_preds : theory -> string list -> string list -> (string * typ) list
     -> (moded_clause list) pred_mode_table -> term pred_mode_table,
-  create_definitions: (string * typ) list -> string * mode list -> theory -> theory,
+  define_functions : (string * typ) list -> string * mode list -> theory -> theory,
   infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
     -> string list -> (string * (term list * indprem list) list) list
     -> moded_clause list pred_mode_table,
@@ -2189,7 +2247,7 @@
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
   add_code_equations : theory -> int -> (string * typ) list
     -> (string * thm list) list -> (string * thm list) list,
-  are_not_defined : theory -> string list -> bool,
+  defined : theory -> string -> bool,
   qname : bstring
   }
 
@@ -2197,19 +2255,21 @@
 fun add_equations_of steps options prednames thy =
   let
     fun dest_steps (Steps s) = s
-    val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
+    val _ = print_step options
+      ("Starting predicate compiler for predicates " ^ commas 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 (maps (intros_of thy) prednames)
     val _ = print_step options "Infering modes..."
-    val moded_clauses = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses 
+    val moded_clauses =
+      #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes options modes
     val _ = print_modes options modes
       (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
-    val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy
+    val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
       |> Theory.checkpoint
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
@@ -2236,7 +2296,8 @@
     val (G', v) = case try (Graph.get_node G) key of
         SOME v => (G, v)
       | NONE => (Graph.new_node (key, value_of key) G, value_of key)
-    val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v)))
+    val (G'', visited') = fold (extend' value_of edges_of)
+      (subtract (op =) visited (edges_of (key, v)))
       (G', key :: visited)
   in
     (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
@@ -2247,22 +2308,26 @@
 fun gen_add_equations steps options names thy =
   let
     fun dest_steps (Steps s) = s
-    val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
+    val thy' = thy
+      |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names)
       |> Theory.checkpoint;
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
     val scc = strong_conn_of (PredData.get thy') names
     val thy'' = fold_rev
       (fn preds => fn thy =>
-        if #are_not_defined (dest_steps steps) thy preds then
-          add_equations_of steps options preds thy else thy)
+        if not (forall (#defined (dest_steps 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 = Comp_Mod.Comp_Modifiers
-  {const_name_of = predfun_name_of : (theory -> string -> mode -> string),
+  {function_name_of = predfun_name_of : (theory -> string -> mode -> string),
+  set_function_name = (fn _ => fn _ => fn _ => I),
+  function_name_prefix = "",
   funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
@@ -2271,8 +2336,10 @@
   }
 
 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = depth_limited_function_name_of,
+  {function_name_of = depth_limited_function_name_of,
+  set_function_name = set_depth_limited_function_name,
   funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ),
+  function_name_prefix = "depth_limited_",
   additional_arguments = fn names =>
     let
       val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
@@ -2289,7 +2356,8 @@
     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')))
+          $ (if full_mode then mk_single compfuns HOLogic.unit else
+            Const (@{const_name undefined}, T')))
         $ compilation
     end,
   transform_additional_arguments =
@@ -2304,39 +2372,62 @@
   }
 
 val random_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = generator_name_of,
-  funT_of = K generator_funT_of : (compilation_funs -> mode -> typ -> typ),
+  {function_name_of = random_function_name_of,
+  set_function_name = set_random_function_name,
+  function_name_prefix = "random",
+  funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
   wrap_compilation = K (K (K (K (K I))))
     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   transform_additional_arguments = K I : (indprem -> term list -> term list)
   }
 
+val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {function_name_of = annotated_function_name_of,
+  set_function_name = set_annotated_function_name,
+  function_name_prefix = "annotated",
+  funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
+  additional_arguments = K [],
+  wrap_compilation =
+    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+      mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation,
+  transform_additional_arguments = K I : (indprem -> term list -> term list)
+  }
+
 val add_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
-  create_definitions = create_definitions,
+  define_functions = create_definitions,
   compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove,
   add_code_equations = add_code_equations,
-  are_not_defined = fn thy => forall (null o modes_of thy),
+  defined = defined_functions,
   qname = "equation"})
 
 val add_depth_limited_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
-  create_definitions = create_definitions_of_depth_limited_functions,
+  define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove_by_skip,
   add_code_equations = K (K (K I)),
-  are_not_defined = fn thy => forall (null o depth_limited_modes_of thy),
+  defined = defined_depth_limited_functions,
   qname = "depth_limited_equation"})
 
+val add_annotated_equations = gen_add_equations
+  (Steps {infer_modes = infer_modes,
+  define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns,
+  compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns,
+  prove = prove_by_skip,
+  add_code_equations = K (K (K I)),
+  defined = defined_annotated_functions,
+  qname = "annotated_equation"})
+
 val add_quickcheck_equations = gen_add_equations
   (Steps {infer_modes = infer_modes_with_generator,
-  create_definitions = random_create_definitions,
+  define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
   compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
   prove = prove_by_skip,
   add_code_equations = K (K (K I)),
-  are_not_defined = fn thy => forall (null o random_modes_of thy),
+  defined = defined_random_functions,
   qname = "random_equation"})
 
 (** user interface **)
@@ -2396,6 +2487,8 @@
             add_quickcheck_equations options [const])
            else if is_depth_limited options then
              add_depth_limited_equations options [const]
+           else if is_annotated options then
+             add_annotated_equations options [const]
            else
              add_equations options [const]))
       end
@@ -2409,11 +2502,12 @@
 (* 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);
+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*)
-(* TODO: *)
-fun analyze_compr thy compfuns (depth_limit, random) t_compr =
+(* TODO: make analyze_compr generic with respect to the compilation modifiers*)
+fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) 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);
@@ -2424,9 +2518,17 @@
       (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')
+    val all_modes_of = if random then all_random_modes_of else all_modes_of
+    fun fits_to is NONE = true
+      | fits_to is (SOME pm) = (is = pm)
+    fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) =
+        fits_to is pm andalso valid (ms @ ms') pms
+      | valid (NONE :: ms') pms = valid ms' pms
+      | valid [] [] = true
+      | valid [] _ = error "Too many mode annotations"
+      | valid (SOME _ :: _) [] = error "Not enough mode annotations"
+    val modes = filter (fn Mode (_, is, ms) => is = user_mode'
+        andalso (the_default true (Option.map (valid ms) param_user_modes)))
       (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
     val m = case modes
      of [] => error ("No mode possible for comprehension "
@@ -2440,10 +2542,11 @@
         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 random_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
+      case depth_limit of
+        NONE =>
+          (if random then random_comp_modifiers else
+           if annotated then annotated_comp_modifiers else predicate_comp_modifiers)
+      | SOME _ => depth_limited_comp_modifiers
     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
@@ -2461,10 +2564,10 @@
       in mk_map compfuns T_pred T_compr arrange t_pred end
   in t_eval end;
 
-fun eval thy (options as (depth_limit, random)) t_compr =
+fun eval thy param_user_modes (options as (depth_limit, (random, annotated))) t_compr =
   let
     val compfuns = if random then RandomPredCompFuns.compfuns else PredicateCompFuns.compfuns
-    val t = analyze_compr thy compfuns options t_compr;
+    val t = analyze_compr thy compfuns param_user_modes 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 =
@@ -2476,15 +2579,16 @@
         Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
   in (T, eval) end;
 
-fun values ctxt options k t_compr =
+fun values ctxt param_user_modes options k t_compr =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (T, ts) = eval thy options t_compr;
+    val (T, ts) = eval thy param_user_modes options t_compr;
     val (ts, _) = Predicate.yieldn k ts;
     val setT = HOLogic.mk_setT T;
     val elemsT = HOLogic.mk_set T ts;
+    val cont = Free ("...", setT)
   in if k = ~1 orelse length ts < k then elemsT
-    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ t_compr
+    else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont
   end;
   (*
 fun random_values ctxt k t = 
@@ -2494,35 +2598,16 @@
   in
   end;
   *)
-fun values_cmd modes options k raw_t state =
+fun values_cmd print_modes param_user_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 options k t;
+    val t' = values ctxt param_user_modes options k t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = PrintMode.with_modes print_modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         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 options =
-  let
-    val depth_limit = Scan.optional (Args.$$$ "depth_limit" |-- P.$$$ "=" |-- P.nat >> SOME) NONE
-    val random = Scan.optional (Args.$$$ "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 -- 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;
-
-end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -161,7 +161,9 @@
 
 fun make_const_spec_table options thy =
   let
-    fun store ignore_const f = fold (store_thm_in_table options ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
+    fun store ignore_const f =
+      fold (store_thm_in_table options ignore_const thy)
+        (map (Thm.transfer thy) (f (ProofContext.init thy)))
     val table = Symtab.empty
       |> store [] Predicate_Compile_Alternative_Defs.get
     val ignore_consts = Symtab.keys table
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -33,7 +33,8 @@
   
   inductify = false,
   random = false,
-  depth_limited = false
+  depth_limited = false,
+  annotated = false
 }
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
@@ -86,11 +87,11 @@
       (*  |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
       |> Predicate_Compile_Core.add_quickcheck_equations 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 modes = Predicate_Compile_Core.random_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 name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], [])
           val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
           in Const (name, T) $ Bound 0 end
       (*else if member (op =) depth_limited_modes ([], []) then
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Induction_Schema.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -0,0 +1,48 @@
+(*  Title:      HOL/ex/Induction_Schema.thy
+    Author:     Alexander Krauss, TU Muenchen
+*)
+
+header {* Examples of automatically derived induction rules *}
+
+theory Induction_Schema
+imports Main
+begin
+
+subsection {* Some simple induction principles on nat *}
+
+lemma nat_standard_induct: (* cf. Nat.thy *)
+  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma nat_induct2:
+  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
+  \<Longrightarrow> P n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma minus_one_induct:
+  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem diff_induct: (* cf. Nat.thy *)
+  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
+    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
+by induction_schema (pat_completeness, lexicographic_order)
+
+lemma list_induct2': (* cf. List.thy *)
+  "\<lbrakk> P [] [];
+  \<And>x xs. P (x#xs) [];
+  \<And>y ys. P [] (y#ys);
+   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
+ \<Longrightarrow> P xs ys"
+by induction_schema (pat_completeness, lexicographic_order)
+
+theorem even_odd_induct:
+  assumes "R 0"
+  assumes "Q 0"
+  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
+  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
+  shows "R n" "Q n"
+  using assms
+by induction_schema (pat_completeness+, lexicographic_order)
+
+end
\ No newline at end of file
--- a/src/HOL/ex/Induction_Scheme.thy	Sat Nov 07 08:17:53 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      HOL/ex/Induction_Scheme.thy
-    ID:         $Id$
-    Author:     Alexander Krauss, TU Muenchen
-*)
-
-header {* Examples of automatically derived induction rules *}
-
-theory Induction_Scheme
-imports Main
-begin
-
-subsection {* Some simple induction principles on nat *}
-
-lemma nat_standard_induct: (* cf. Nat.thy *)
-  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
-by induct_scheme (pat_completeness, lexicographic_order)
-
-lemma nat_induct2:
-  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
-  \<Longrightarrow> P n"
-by induct_scheme (pat_completeness, lexicographic_order)
-
-lemma minus_one_induct:
-  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
-by induct_scheme (pat_completeness, lexicographic_order)
-
-theorem diff_induct: (* cf. Nat.thy *)
-  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
-    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
-by induct_scheme (pat_completeness, lexicographic_order)
-
-lemma list_induct2': (* cf. List.thy *)
-  "\<lbrakk> P [] [];
-  \<And>x xs. P (x#xs) [];
-  \<And>y ys. P [] (y#ys);
-   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
- \<Longrightarrow> P xs ys"
-by induct_scheme (pat_completeness, lexicographic_order)
-
-theorem even_odd_induct:
-  assumes "R 0"
-  assumes "Q 0"
-  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
-  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
-  shows "R n" "Q n"
-  using assms
-by induct_scheme (pat_completeness+, lexicographic_order)
-
-end
\ No newline at end of file
--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -9,7 +9,9 @@
 quickcheck[generator=predicate_compile]
 oops
 
+(* TODO: some error with doubled negation *)
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
+(*quickcheck[generator=predicate_compile]*)
 oops
 
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
@@ -23,12 +25,17 @@
 section {* Numerals *}
 
 lemma
-  "x \<in> {1, 2, (3::nat)} ==> x < 3"
+  "x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
 (*quickcheck[generator=predicate_compile]*)
 oops
+
 lemma
-  "x \<in> {1, 2} \<union> {3, 4} ==> x > 4"
-(*quickcheck[generator=predicate_compile]*)
+  "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
+quickcheck[generator=predicate_compile]
 oops
 
 section {* Context Free Grammar *}
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Nov 07 08:18:12 2009 +0100
@@ -188,13 +188,23 @@
 (*values "{x. one_or_two x}"*)
 values [random] "{x. one_or_two x}"
 
-definition one_or_two':
-  "one_or_two' == {1, (2::nat)}"
+inductive one_or_two' :: "nat => bool"
+where
+  "one_or_two' 1"
+| "one_or_two' 2"
+
+code_pred one_or_two' .
+thm one_or_two'.equation
 
-code_pred [inductify] one_or_two' .
-thm one_or_two'.equation
-(* TODO: handling numerals *)
-(*values "{x. one_or_two' x}"*)
+values "{x. one_or_two' x}"
+
+definition one_or_two'':
+  "one_or_two'' == {1, (2::nat)}"
+
+code_pred [inductify] one_or_two'' .
+thm one_or_two''.equation
+
+values "{x. one_or_two'' x}"
 
 
 subsection {* even predicate *}
@@ -250,10 +260,12 @@
 code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
 code_pred [depth_limited] append .
 code_pred [random] append .
+code_pred [annotated] append .
 
 thm append.equation
 thm append.depth_limited_equation
 thm append.random_equation
+thm append.annotated_equation
 
 values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
 values "{zs. append [0, Suc 0, 2] [17, 8] zs}"
@@ -264,6 +276,7 @@
 value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
 value [code] "Predicate.the (append_3 ([]::int list))"
 
+
 text {* tricky case with alternative rules *}
 
 inductive append2
@@ -460,13 +473,13 @@
 values "{m. succ 0 m}"
 values "{m. succ m 0}"
 
-(* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
+text {* values command needs mode annotation of the parameter succ
+to disambiguate which mode is to be chosen. *} 
 
-(*
-values 20 "{n. tranclp succ 10 n}"
-values "{n. tranclp succ n 10}"
+values [mode: [1]] 20 "{n. tranclp succ 10 n}"
+values [mode: [2]] 10 "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
-*)
+
 
 subsection {* IMP *}
 
@@ -529,10 +542,13 @@
 
 code_pred steps .
 
+values 3 
+ "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
+
 values 5
  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
 
-(* FIXME
+(* FIXME:
 values 3 "{(a,q). step (par nil nil) a q}"
 *)
 
@@ -645,6 +661,7 @@
 thm set_of.equation
 
 code_pred [inductify] is_ord .
+thm is_ord_aux.equation
 thm is_ord.equation
 
 
@@ -699,7 +716,7 @@
 code_pred [inductify] take .
 code_pred [inductify] drop .
 code_pred [inductify] zip .
-code_pred [inductify] upt .
+(*code_pred [inductify] upt .*)
 code_pred [inductify] remdups .
 code_pred [inductify] remove1 .
 code_pred [inductify] removeAll .
--- a/src/HOL/ex/ROOT.ML	Sat Nov 07 08:17:53 2009 +0100
+++ b/src/HOL/ex/ROOT.ML	Sat Nov 07 08:18:12 2009 +0100
@@ -24,7 +24,7 @@
   "Binary",
   "Recdefs",
   "Fundefs",
-  "Induction_Scheme",
+  "Induction_Schema",
   "InductiveInvariant_examples",
   "LocaleTest2",
   "Records",