merged

--- a/src/HOL/DSequence.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/DSequence.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -27,12 +27,6 @@
     None => None
   | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
 
-definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
-where
-  "yieldn n dseq i pol = (case eval dseq i pol of
-    None => ([], %i pol. None)
-  | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
-
 fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
 where
   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
@@ -91,8 +85,11 @@
 
 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
 
-val yieldn = @{code yieldn}
 val yield = @{code yield}
+fun yieldn n s d pol = case s d pol of  
+    NONE => ([], fn d => fn pol => NONE)
+  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
+
 val map = @{code map}
 
 end;

--- a/src/HOL/IsaMakefile	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Mar 30 12:47:39 2010 +0200
@@ -301,6 +301,7 @@
   Tools/Predicate_Compile/predicate_compile_data.ML \
   Tools/Predicate_Compile/predicate_compile_fun.ML \
   Tools/Predicate_Compile/predicate_compile.ML \
+  Tools/Predicate_Compile/predicate_compile_specialisation.ML \
   Tools/Predicate_Compile/predicate_compile_pred.ML \
   Tools/quickcheck_generators.ML \
   Tools/Qelim/cooper_data.ML \

--- a/src/HOL/Lazy_Sequence.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -20,15 +20,6 @@
   "yield Empty = None"
 | "yield (Insert x xq) = Some (x, xq)"
 
-fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
-where
-  "yieldn i S = (if i = 0 then ([], S) else
-    case yield S of
-      None => ([], S)
-    | Some (x, S') => let
-       (xs, S'') = yieldn (i - 1) S'
-      in (x # xs, S''))"
-
 lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
 by (cases xq) auto
 
@@ -131,6 +122,7 @@
   datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
   val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
+  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
 end;
 
 structure Lazy_Sequence : LAZY_SEQUENCE =
@@ -140,7 +132,16 @@
 
 val yield = @{code yield}
 
-val yieldn = @{code yieldn}
+fun anamorph f k x = (if k = 0 then ([], x)
+  else case f x
+   of NONE => ([], x)
+    | SOME (v, y) => let
+        val (vs, z) = anamorph f (k - 1) y
+      in (v :: vs, z) end);
+
+fun yieldn S = anamorph yield S;
+
+val map = @{code map}
 
 end;
 *}
@@ -151,8 +152,61 @@
 
 code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
 
+section {* With Hit Bound Value *}
+text {* assuming in negative context *}
+
+types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
+
+definition hit_bound :: "'a hit_bound_lazy_sequence"
+where
+  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
+
+
+definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
+where
+  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
+
+primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
+where
+  "hb_flat Empty = Empty"
+| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
+
+lemma [code]:
+  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
+    None => None
+  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
+apply (cases "xqq")
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+by auto
+
+primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
+where
+  "hb_map f Empty = Empty"
+| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
+
+lemma [code]:
+  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
+apply (cases xq)
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+apply auto
+done
+
+definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
+where
+  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
+
+definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
+where
+  "hb_if_seq b = (if b then hb_single () else empty)"
+
+definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
+where
+  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
+
 hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
-hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
+hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
+hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
 
 end

--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -7,8 +7,11 @@
 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
+  Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",
+  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",
+  Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4) *}
 
 end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/New_DSequence.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -0,0 +1,95 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Depth-Limited Sequences with failure element *}
+
+theory New_DSequence
+imports Random_Sequence
+begin
+
+section {* Positive Depth-Limited Sequence *}
+
+types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
+
+definition pos_empty :: "'a pos_dseq"
+where
+  "pos_empty = (%i. Lazy_Sequence.empty)"
+
+definition pos_single :: "'a => 'a pos_dseq"
+where
+  "pos_single x = (%i. Lazy_Sequence.single x)"
+
+definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
+where
+  "pos_bind x f = (%i. 
+     if i = 0 then
+       Lazy_Sequence.empty
+     else
+       Lazy_Sequence.bind (x (i - 1)) (%a. f a i))"
+
+definition pos_union :: "'a pos_dseq => 'a pos_dseq => 'a pos_dseq"
+where
+  "pos_union xq yq = (%i. Lazy_Sequence.append (xq i) (yq i))"
+
+definition pos_if_seq :: "bool => unit pos_dseq"
+where
+  "pos_if_seq b = (if b then pos_single () else pos_empty)"
+
+definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
+where
+  "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
+
+section {* Negative Depth-Limited Sequence *}
+
+types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
+
+definition neg_empty :: "'a neg_dseq"
+where
+  "neg_empty = (%i. Lazy_Sequence.empty)"
+
+definition neg_single :: "'a => 'a neg_dseq"
+where
+  "neg_single x = (%i. Lazy_Sequence.hb_single x)"
+
+definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
+where
+  "neg_bind x f = (%i. 
+     if i = 0 then
+       Lazy_Sequence.hit_bound
+     else
+       hb_bind (x (i - 1)) (%a. f a i))"
+
+definition neg_union :: "'a neg_dseq => 'a neg_dseq => 'a neg_dseq"
+where
+  "neg_union x y = (%i. Lazy_Sequence.append (x i) (y i))"
+
+definition neg_if_seq :: "bool => unit neg_dseq"
+where
+  "neg_if_seq b = (if b then neg_single () else neg_empty)"
+
+definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
+where
+  "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
+
+section {* Negation *}
+
+definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
+where
+  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
+
+definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
+where
+  "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of
+    None => Lazy_Sequence.hb_single ()
+  | Some ((), xq) => Lazy_Sequence.empty)"
+
+hide (open) type pos_dseq neg_dseq
+
+hide (open) const 
+  pos_empty pos_single pos_bind pos_union pos_if_seq pos_not_seq
+  neg_empty neg_single neg_bind neg_union neg_if_seq neg_not_seq
+hide (open) fact
+  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_not_seq_def pos_map_def
+  neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_not_seq_def neg_map_def
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/New_Random_Sequence.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -0,0 +1,97 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+theory New_Random_Sequence
+imports Quickcheck New_DSequence
+begin
+
+types 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
+types 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
+
+definition pos_empty :: "'a pos_random_dseq"
+where
+  "pos_empty = (%nrandom size seed. New_DSequence.pos_empty)"
+
+definition pos_single :: "'a => 'a pos_random_dseq"
+where
+  "pos_single x = (%nrandom size seed. New_DSequence.pos_single x)"
+
+definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
+where
+  "pos_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
+where
+  "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
+
+definition pos_if_random_dseq :: "bool => unit pos_random_dseq"
+where
+  "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
+
+definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
+where
+  "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))"
+
+fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+  "iter random nrandom seed =
+    (if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))"
+
+definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
+where
+  "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
+
+definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
+where
+  "pos_map f P = pos_bind P (pos_single o f)"
+
+
+definition neg_empty :: "'a neg_random_dseq"
+where
+  "neg_empty = (%nrandom size seed. New_DSequence.neg_empty)"
+
+definition neg_single :: "'a => 'a neg_random_dseq"
+where
+  "neg_single x = (%nrandom size seed. New_DSequence.neg_single x)"
+
+definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
+where
+  "neg_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
+where
+  "neg_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
+
+definition neg_if_random_dseq :: "bool => unit neg_random_dseq"
+where
+  "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
+
+definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
+where
+  "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))"
+(*
+fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+  "iter random nrandom seed =
+    (if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))"
+
+definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
+where
+  "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
+*)
+definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
+where
+  "neg_map f P = neg_bind P (neg_single o f)"
+(*
+hide const DSequence.empty DSequence.single DSequence.eval
+  DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
+  DSequence.map
+*)
+
+hide (open) const pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_not_random_dseq iter Random pos_map
+  neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_not_random_dseq neg_map
+hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+(* FIXME: hide facts *)
+(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+
+end
\ No newline at end of file

--- a/src/HOL/Predicate_Compile.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Predicate_Compile.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -5,13 +5,14 @@
 header {* A compiler for predicates defined by introduction rules *}
 
 theory Predicate_Compile
-imports Random_Sequence Quickcheck
+imports New_Random_Sequence
 uses
   "Tools/Predicate_Compile/predicate_compile_aux.ML"
   "Tools/Predicate_Compile/predicate_compile_core.ML"
   "Tools/Predicate_Compile/predicate_compile_data.ML"
   "Tools/Predicate_Compile/predicate_compile_fun.ML"
   "Tools/Predicate_Compile/predicate_compile_pred.ML"
+  "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
   "Tools/Predicate_Compile/predicate_compile.ML"
 begin
 

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -788,7 +788,7 @@
 definition
   "case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
 
-code_pred [inductify] case_f .
+code_pred [inductify, skip_proof] case_f .
 thm case_fP.equation
 thm case_fP.intros
 
@@ -910,11 +910,11 @@
 declare list.size(3,4)[code_pred_def]
 (*code_pred [inductify, show_steps, show_intermediate_results] length .*)
 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
-code_pred [inductify] lex .
+code_pred [inductify, skip_proof] lex .
 thm lex.equation
 thm lex_def
 declare lenlex_conv[code_pred_def]
-code_pred [inductify] lenlex .
+code_pred [inductify, skip_proof] lenlex .
 thm lenlex.equation
 
 code_pred [random_dseq inductify] lenlex .
@@ -1037,7 +1037,7 @@
 *)
 (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
 
-code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
 thm concatP.equation
 
 values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
@@ -1068,31 +1068,31 @@
 values "{x. tlP [1, 2, (3::nat)] x}"
 values "{x. tlP [1, 2, (3::int)] [3]}"
 
-code_pred [inductify] last .
+code_pred [inductify, skip_proof] last .
 thm lastP.equation
 
-code_pred [inductify] butlast .
+code_pred [inductify, skip_proof] butlast .
 thm butlastP.equation
 
-code_pred [inductify] take .
+code_pred [inductify, skip_proof] take .
 thm takeP.equation
 
-code_pred [inductify] drop .
+code_pred [inductify, skip_proof] drop .
 thm dropP.equation
-code_pred [inductify] zip .
+code_pred [inductify, skip_proof] zip .
 thm zipP.equation
 
-code_pred [inductify] upt .
-code_pred [inductify] remdups .
+code_pred [inductify, skip_proof] upt .
+code_pred [inductify, skip_proof] remdups .
 thm remdupsP.equation
 code_pred [dseq inductify] remdups .
 values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
 
-code_pred [inductify] remove1 .
+code_pred [inductify, skip_proof] remove1 .
 thm remove1P.equation
 values "{xs. remove1P 1 xs [2, (3::int)]}"
 
-code_pred [inductify] removeAll .
+code_pred [inductify, skip_proof] removeAll .
 thm removeAllP.equation
 code_pred [dseq inductify] removeAll .
 
@@ -1100,17 +1100,17 @@
 
 code_pred [inductify] distinct .
 thm distinct.equation
-code_pred [inductify] replicate .
+code_pred [inductify, skip_proof] replicate .
 thm replicateP.equation
 values 5 "{(n, xs). replicateP n (0::int) xs}"
 
-code_pred [inductify] splice .
+code_pred [inductify, skip_proof] splice .
 thm splice.simps
 thm spliceP.equation
 
 values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
 
-code_pred [inductify] List.rev .
+code_pred [inductify, skip_proof] List.rev .
 code_pred [inductify] map .
 code_pred [inductify] foldr .
 code_pred [inductify] foldl .
@@ -1159,7 +1159,7 @@
 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
 
-code_pred [inductify] S\<^isub>3p .
+code_pred [inductify, skip_proof] S\<^isub>3p .
 thm S\<^isub>3p.equation
 
 values 10 "{x. S\<^isub>3p x}"

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -108,7 +108,7 @@
 | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
 | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
 
-code_pred [inductify] S\<^isub>3 .
+code_pred [inductify, skip_proof] S\<^isub>3 .
 thm S\<^isub>3.equation
 (*
 values 10 "{x. S\<^isub>3 x}"

--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -1,1 +1,1 @@
-use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples"];
+use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -0,0 +1,241 @@
+theory Specialisation_Examples
+imports Main "../ex/Predicate_Compile_Alternative_Defs"
+begin
+
+section {* Specialisation Examples *}
+
+fun nth_el'
+where
+  "nth_el' [] i = None"
+| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
+
+definition
+  "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
+
+code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
+
+thm greater_than_index.equation
+
+values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
+values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"
+
+subsection {* Common subterms *}
+
+text {* If a predicate is called with common subterms as arguments,
+  this predicate should be specialised. 
+*}
+
+definition max_nat :: "nat => nat => nat"
+  where "max_nat a b = (if a <= b then b else a)"
+
+lemma [code_pred_inline]:
+  "max = max_nat"
+by (simp add: expand_fun_eq max_def max_nat_def)
+
+definition
+  "max_of_my_Suc x = max x (Suc x)"
+
+text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
+
+code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+
+thm max_of_my_SucP.equation
+
+ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
+
+values "{x. max_of_my_SucP x 6}"
+
+subsection {* Sorts *}
+
+code_pred [inductify] sorted .
+thm sorted.equation
+
+section {* Specialisation in POPLmark theory *}
+
+notation
+  Some ("\<lfloor>_\<rfloor>")
+
+notation
+  None ("\<bottom>")
+
+notation
+  length ("\<parallel>_\<parallel>")
+
+notation
+  Cons ("_ \<Colon>/ _" [66, 65] 65)
+
+primrec
+  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
+where
+  "[]\<langle>i\<rangle> = \<bottom>"
+| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> \<lfloor>x\<rfloor> | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
+
+primrec assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" ("_\<langle>_\<rangle>\<^isub>?" [90, 0] 91)
+where
+  "[]\<langle>a\<rangle>\<^isub>? = \<bottom>"
+| "(x # xs)\<langle>a\<rangle>\<^isub>? = (if fst x = a then \<lfloor>snd x\<rfloor> else xs\<langle>a\<rangle>\<^isub>?)"
+
+primrec unique :: "('a \<times> 'b) list \<Rightarrow> bool"
+where
+  "unique [] = True"
+| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^isub>? = \<bottom> \<and> unique xs)"
+
+datatype type =
+    TVar nat
+  | Top
+  | Fun type type    (infixr "\<rightarrow>" 200)
+  | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
+
+datatype binding = VarB type | TVarB type
+types env = "binding list"
+
+primrec is_TVarB :: "binding \<Rightarrow> bool"
+where
+  "is_TVarB (VarB T) = False"
+| "is_TVarB (TVarB T) = True"
+
+primrec type_ofB :: "binding \<Rightarrow> type"
+where
+  "type_ofB (VarB T) = T"
+| "type_ofB (TVarB T) = T"
+
+primrec mapB :: "(type \<Rightarrow> type) \<Rightarrow> binding \<Rightarrow> binding"
+where
+  "mapB f (VarB T) = VarB (f T)"
+| "mapB f (TVarB T) = TVarB (f T)"
+
+datatype trm =
+    Var nat
+  | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
+  | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)
+  | App trm trm    (infixl "\<bullet>" 200)
+  | TApp trm type  (infixl "\<bullet>\<^isub>\<tau>" 200)
+
+primrec liftT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<up>\<^isub>\<tau>")
+where
+  "\<up>\<^isub>\<tau> n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
+| "\<up>\<^isub>\<tau> n k Top = Top"
+| "\<up>\<^isub>\<tau> n k (T \<rightarrow> U) = \<up>\<^isub>\<tau> n k T \<rightarrow> \<up>\<^isub>\<tau> n k U"
+| "\<up>\<^isub>\<tau> n k (\<forall><:T. U) = (\<forall><:\<up>\<^isub>\<tau> n k T. \<up>\<^isub>\<tau> n (k + 1) U)"
+
+primrec lift :: "nat \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("\<up>")
+where
+  "\<up> n k (Var i) = (if i < k then Var i else Var (i + n))"
+| "\<up> n k (\<lambda>:T. t) = (\<lambda>:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
+| "\<up> n k (\<lambda><:T. t) = (\<lambda><:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
+| "\<up> n k (s \<bullet> t) = \<up> n k s \<bullet> \<up> n k t"
+| "\<up> n k (t \<bullet>\<^isub>\<tau> T) = \<up> n k t \<bullet>\<^isub>\<tau> \<up>\<^isub>\<tau> n k T"
+
+primrec substTT :: "type \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>\<tau>" [300, 0, 0] 300)
+where
+  "(TVar i)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> =
+     (if k < i then TVar (i - 1) else if i = k then \<up>\<^isub>\<tau> k 0 S else TVar i)"
+| "Top[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = Top"
+| "(T \<rightarrow> U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> \<rightarrow> U[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
+| "(\<forall><:T. U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = (\<forall><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. U[k+1 \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>)"
+
+primrec decT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type"  ("\<down>\<^isub>\<tau>")
+where
+  "\<down>\<^isub>\<tau> 0 k T = T"
+| "\<down>\<^isub>\<tau> (Suc n) k T = \<down>\<^isub>\<tau> n k (T[k \<mapsto>\<^isub>\<tau> Top]\<^isub>\<tau>)"
+
+primrec subst :: "trm \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm"  ("_[_ \<mapsto> _]" [300, 0, 0] 300)
+where
+  "(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)"
+| "(t \<bullet> u)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet> u[k \<mapsto> s]"
+| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet>\<^isub>\<tau> \<down>\<^isub>\<tau> 1 k T"
+| "(\<lambda>:T. t)[k \<mapsto> s] = (\<lambda>:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
+| "(\<lambda><:T. t)[k \<mapsto> s] = (\<lambda><:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
+
+primrec substT :: "trm \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> trm"    ("_[_ \<mapsto>\<^isub>\<tau> _]" [300, 0, 0] 300)
+where
+  "(Var i)[k \<mapsto>\<^isub>\<tau> S] = (if k < i then Var (i - 1) else Var i)"
+| "(t \<bullet> u)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet> u[k \<mapsto>\<^isub>\<tau> S]"
+| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet>\<^isub>\<tau> T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
+| "(\<lambda>:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda>:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
+| "(\<lambda><:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
+
+primrec liftE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<up>\<^isub>e")
+where
+  "\<up>\<^isub>e n k [] = []"
+| "\<up>\<^isub>e n k (B \<Colon> \<Gamma>) = mapB (\<up>\<^isub>\<tau> n (k + \<parallel>\<Gamma>\<parallel>)) B \<Colon> \<up>\<^isub>e n k \<Gamma>"
+
+primrec substE :: "env \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> env"  ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>e" [300, 0, 0] 300)
+where
+  "[][k \<mapsto>\<^isub>\<tau> T]\<^isub>e = []"
+| "(B \<Colon> \<Gamma>)[k \<mapsto>\<^isub>\<tau> T]\<^isub>e = mapB (\<lambda>U. U[k + \<parallel>\<Gamma>\<parallel> \<mapsto>\<^isub>\<tau> T]\<^isub>\<tau>) B \<Colon> \<Gamma>[k \<mapsto>\<^isub>\<tau> T]\<^isub>e"
+
+primrec decE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env"  ("\<down>\<^isub>e")
+where
+  "\<down>\<^isub>e 0 k \<Gamma> = \<Gamma>"
+| "\<down>\<^isub>e (Suc n) k \<Gamma> = \<down>\<^isub>e n k (\<Gamma>[k \<mapsto>\<^isub>\<tau> Top]\<^isub>e)"
+
+inductive
+  well_formed :: "env \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50)
+where
+  wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
+| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
+| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
+| wf_all: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+
+inductive
+  well_formedE :: "env \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50)
+  and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool"  ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50)
+where
+  "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B"
+| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>"
+| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+
+inductive_cases well_formed_cases:
+  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
+  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
+  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
+  "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+
+inductive_cases well_formedE_cases:
+  "B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+
+inductive
+  subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
+where
+  SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
+| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
+| SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow>
+    \<Gamma> \<turnstile> \<up>\<^isub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T"
+| SA_arrow: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"
+| SA_all: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow>
+    \<Gamma> \<turnstile> (\<forall><:S\<^isub>1. S\<^isub>2) <: (\<forall><:T\<^isub>1. T\<^isub>2)"
+
+inductive
+  typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+where
+  T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
+| T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
+| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
+| T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
+| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
+    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
+| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
+
+code_pred [inductify, skip_proof] typing .
+
+thm typing.equation
+
+values 6 "{(E, t, T). typing E t T}"
+
+subsection {* Higher-order predicate *}
+
+code_pred [inductify] mapB .
+
+subsection {* Multiple instances *}
+
+inductive subtype_refl' where
+  "\<Gamma> \<turnstile> t : T ==> \<not> (\<Gamma> \<turnstile> T <: T) ==> subtype_refl' t T"
+
+code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' .
+
+thm subtype_refl'.equation
+
+
+end
\ No newline at end of file

--- a/src/HOL/Random.thy	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Random.thy	Tue Mar 30 12:47:39 2010 +0200
@@ -1,3 +1,4 @@
+
 (* Author: Florian Haftmann, TU Muenchen *)
 
 header {* A HOL random engine *}
@@ -154,6 +155,14 @@
 
 in
 
+fun next_seed () =
+  let
+    val (seed1, seed') = @{code split_seed} (! seed)
+    val _ = seed := seed'
+  in
+    seed1
+  end
+
 fun run f =
   let
     val (x, seed') = f (! seed);

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -9,6 +9,7 @@
   val setup : theory -> theory
   val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
   val present_graph : bool Unsynchronized.ref
+  val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
 end;
 
 structure Predicate_Compile (*: PREDICATE_COMPILE*) =
@@ -16,6 +17,9 @@
 
 val present_graph = Unsynchronized.ref false
 
+val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
+  
+
 open Predicate_Compile_Aux;
 
 (* Some last processing *)
@@ -93,7 +97,7 @@
       val _ = print_step options
         ("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^
           ") to predicates...")
-      val (fun_pred_specs, thy') =
+      val (fun_pred_specs, thy1) =
         (if function_flattening options andalso (not (null funnames)) then
           if fail_safe_function_flattening options then
             case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
@@ -102,21 +106,26 @@
           else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy
         else ([], thy))
         (*||> Theory.checkpoint*)
-      val _ = print_specs options thy' fun_pred_specs
+      val _ = print_specs options thy1 fun_pred_specs
       val specs = (get_specs prednames) @ fun_pred_specs
-      val (intross3, thy''') = process_specification options specs thy'
-      val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
+      val (intross3, thy2) = process_specification options specs thy1
+      val _ = print_intross options thy2 "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 thy''' s, map (AxClass.overload thy''') ths)) intross4
-      val intross6 = map_specs (map (expand_tuples thy''')) intross5
-      val intross7 = map_specs (map (eta_contract_ho_arguments thy''')) intross6
-      val _ = print_intross options thy''' "introduction rules before registering: " intross7
+      val _ = print_intross options thy2 "After removing pointless clauses: " intross4
+      val intross5 = map_specs (map (remove_equalities thy2)) intross4
+      val _ = print_intross options thy2 "After removing equality premises:" intross5
+      val intross6 =
+        map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5
+      val intross7 = map_specs (map (expand_tuples thy2)) intross6
+      val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
+      val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
+      val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
+      val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+      val _ = print_intross options thy3 "introduction rules before registering: " intross9
       val _ = print_step options "Registering introduction rules..."
-      val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
+      val thy4 = fold Predicate_Compile_Core.register_intros intross9 thy3
     in
-      thy''''
+      thy4
     end;
 
 fun preprocess options t thy =
@@ -228,6 +237,8 @@
 val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
   P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
 
+val stats = Scan.optional (Args.$$$ "stats" >> K true) false
+
 val value_options =
   let
     val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
@@ -238,7 +249,8 @@
             compilation_names))
         (Pred, [])
   in
-    Scan.optional (P.$$$ "[" |-- expected_values -- scan_compilation --| P.$$$ "]") (NONE, (Pred, []))
+    Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+      ((NONE, false), (Pred, []))
   end
 
 (* code_pred command and values command *)

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -46,6 +46,9 @@
   | eq_mode (Bool, Bool) = true
   | eq_mode _ = false
 
+fun list_fun_mode [] = Bool
+  | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
+
 (* name: binder_modes? *)
 fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
   | strip_fun_mode Bool = []
@@ -295,12 +298,13 @@
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
       (Symtab.dest (Datatype.get_all thy)));
     fun check t = (case strip_comb t of
-        (Free _, []) => true
+        (Var _, []) => true
+      | (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
           | _ => false)
       | _ => false)
-  in check end;  
+  in check end;
 
 fun is_funtype (Type ("fun", [_, _])) = true
   | is_funtype _ = false;
@@ -400,52 +404,13 @@
 
 (* split theorems of case expressions *)
 
-(*
-fun has_split_rule_cname @{const_name "nat_case"} = true
-  | has_split_rule_cname @{const_name "list_case"} = true
-  | has_split_rule_cname _ = false
-  
-fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
-  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
-  | has_split_rule_term thy _ = false
-
-fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
-  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
-  | has_split_rule_term' thy c = has_split_rule_term thy c
-
-*)
 fun prepare_split_thm ctxt split_thm =
     (split_thm RS @{thm iffD2})
     |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
       @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
 
-fun find_split_thm thy (Const (name, typ)) =
-  let
-    fun split_name str =
-      case first_field "." str
-        of (SOME (field, rest)) => field :: split_name rest
-         | NONE => [str]
-    val splitted_name = split_name name
-  in
-    if length splitted_name > 0 andalso
-       String.isSuffix "_case" (List.last splitted_name)
-    then
-      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
-      |> space_implode "."
-      |> PureThy.get_thm thy
-      |> SOME
-      handle ERROR msg => NONE
-    else NONE
-  end
-  | find_split_thm _ _ = NONE
-
-
-(* TODO: split rules for let and if are different *)
-fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
-  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
-  | find_split_thm' thy c = find_split_thm thy c
-
-fun has_split_thm thy t = is_some (find_split_thm thy t)
+fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
+  | find_split_thm thy _ = NONE
 
 fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
 
@@ -462,17 +427,19 @@
   | _ => error "equals_conv"  
 *)
 
-(* Different options for compiler *)
+(* Different compilations *)
 
 datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
-  | Pos_Random_DSeq | Neg_Random_DSeq
-
+  | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
 
 fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
   | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
+  | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
+  | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
   | negative_compilation_of c = c
   
 fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
+  | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
   | compilation_for_polarity _ c = c
 
 fun string_of_compilation c =
@@ -485,7 +452,25 @@
   | Annotated => "annotated"
   | Pos_Random_DSeq => "pos_random dseq"
   | Neg_Random_DSeq => "neg_random_dseq"
-  
+  | New_Pos_Random_DSeq => "new_pos_random dseq"
+  | New_Neg_Random_DSeq => "new_neg_random_dseq"
+
+val compilation_names = [("pred", Pred),
+  ("random", Random),
+  ("depth_limited", Depth_Limited),
+  ("depth_limited_random", Depth_Limited_Random),
+  (*("annotated", Annotated),*)
+  ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
+  ("new_random_dseq", New_Pos_Random_DSeq)]
+
+val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
+
+
+val random_compilations = [Random, Depth_Limited_Random,
+  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
+
+(* Different options for compiler *)
+
 (*datatype compilation_options =
   Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)
 
@@ -557,13 +542,6 @@
   "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
   "no_topmost_reordering"]
 
-val compilation_names = [("pred", Pred),
-  ("random", Random),
-  ("depth_limited", Depth_Limited),
-  ("depth_limited_random", Depth_Limited_Random),
-  (*("annotated", Annotated),*)
-  ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
-
 fun print_step options s =
   if show_steps options then tracing s else ()
 
@@ -624,7 +602,6 @@
 
 (* eta contract higher-order arguments *)
 
-
 fun eta_contract_ho_arguments thy intro =
   let
     fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom))
@@ -632,5 +609,42 @@
     map_term thy (map_concl f o map_atoms f) intro
   end
 
+(* remove equalities *)
+
+fun remove_equalities thy intro =
+  let
+    fun remove_eqs intro_t =
+      let
+        val (prems, concl) = Logic.strip_horn intro_t
+        fun remove_eq (prems, concl) =
+          let
+            fun removable_eq prem =
+              case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
+                SOME (lhs, rhs) => (case lhs of
+                  Var _ => true
+                  | _ => (case rhs of Var _ => true | _ => false))
+              | NONE => false
+          in
+            case find_first removable_eq prems of
+              NONE => (prems, concl)
+            | SOME eq =>
+              let
+                val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+                val prems' = remove (op =) eq prems
+                val subst = (case lhs of
+                  (v as Var _) =>
+                    (fn t => if t = v then rhs else t)
+                | _ => (case rhs of
+                   (v as Var _) => (fn t => if t = v then lhs else t)))
+              in
+                remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
+              end
+          end
+      in
+        Logic.list_implies (remove_eq (prems, concl))
+      end
+  in
+    map_term thy remove_eqs intro
+  end
 
 end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -10,13 +10,13 @@
   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.mode option list option
-    -> (string option * (Predicate_Compile_Aux.compilation * int list))
+    -> ((string option * bool) * (Predicate_Compile_Aux.compilation * int list))
     -> int -> string -> Toplevel.state -> unit
   val register_predicate : (string * thm list * thm) -> theory -> theory
   val register_intros : string * thm list -> theory -> theory
   val is_registered : theory -> string -> bool
   val function_name_of : Predicate_Compile_Aux.compilation -> theory
-    -> string -> bool * Predicate_Compile_Aux.mode -> string
+    -> string -> Predicate_Compile_Aux.mode -> string
   val predfun_intro_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
   val predfun_elim_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
   val all_preds_of : theory -> string list
@@ -28,22 +28,6 @@
   val intros_of : theory -> string -> thm list
   val add_intro : thm -> theory -> theory
   val set_elim : thm -> theory -> theory
-  val preprocess_intro : theory -> thm -> thm
-  val print_stored_rules : theory -> unit
-  val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit
-  val mk_casesrule : Proof.context -> term -> 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 dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
-  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
-    option Unsynchronized.ref
-  val code_pred_intro_attrib : attribute
-  
-  (* used by Quickcheck_Generator *) 
-  (* temporary for testing of the compilation *)
-  
   datatype compilation_funs = CompilationFuns of {
     mk_predT : typ -> typ,
     dest_predT : typ -> typ,
@@ -55,11 +39,40 @@
     mk_not : term -> term,
     mk_map : typ -> typ -> term -> term -> term
   };
-  
+  val register_alternative_function : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory
+  val alternative_compilation_of : theory -> string -> Predicate_Compile_Aux.mode ->
+    (compilation_funs -> typ -> term) option
+  val functional_compilation : string -> Predicate_Compile_Aux.mode -> compilation_funs -> typ -> term
+  val force_modes_and_functions : string ->
+    (Predicate_Compile_Aux.mode * (string * bool)) list -> theory -> theory
+  val force_modes_and_compilations : string ->
+    (Predicate_Compile_Aux.mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
+  val preprocess_intro : theory -> thm -> thm
+  val print_stored_rules : theory -> unit
+  val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit
+  val mk_casesrule : Proof.context -> term -> 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 dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
+  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
+    option Unsynchronized.ref
+  val new_random_dseq_eval_ref :
+    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
+      option Unsynchronized.ref
+  val new_random_dseq_stats_eval_ref :
+    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
+      option Unsynchronized.ref
+  val code_pred_intro_attrib : attribute
+  (* used by Quickcheck_Generator *) 
+  (* temporary for testing of the compilation *)
   val pred_compfuns : compilation_funs
   val randompred_compfuns : compilation_funs
+  val new_randompred_compfuns : compilation_funs
   val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_depth_limited_random_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+  val add_new_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
   val mk_tracing : string -> term -> term
 end;
 
@@ -254,11 +267,11 @@
       ^ "functions defined for predicate " ^ quote name)
   | SOME fun_names => fun_names
 
-fun function_name_of compilation thy name (pol, mode) =
+fun function_name_of compilation thy name mode =
   case AList.lookup eq_mode
-    (function_names_of (compilation_for_polarity pol compilation) thy name) mode of
+    (function_names_of compilation thy name) mode of
     NONE => error ("No " ^ string_of_compilation compilation
-      ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
+      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
   | SOME function_name => function_name
 
 fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
@@ -735,6 +748,56 @@
 fun mk_not (CompilationFuns funs) = #mk_not funs
 fun mk_map (CompilationFuns funs) = #mk_map funs
 
+(* registration of alternative function names *)
+
+structure Alt_Compilations_Data = Theory_Data
+(
+  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.merge (K true);
+);
+
+fun alternative_compilation_of thy pred_name mode =
+  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
+
+fun force_modes_and_compilations pred_name compilations =
+  let
+    (* thm refl is a dummy thm *)
+    val modes = map fst compilations
+    val (needs_random, non_random_modes) = pairself (map fst)
+      (List.partition (fn (m, (fun_name, random)) => random) compilations)
+    val non_random_dummys = map (rpair "dummy") non_random_modes
+    val all_dummys = map (rpair "dummy") modes
+    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
+      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
+    val alt_compilations = map (apsnd fst) compilations
+  in
+    PredData.map (Graph.new_node
+      (pred_name, mk_pred_data (([], SOME @{thm refl}), (dummy_function_names, ([], needs_random)))))
+    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
+  end
+
+fun functional_compilation fun_name mode compfuns T =
+  let
+    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
+      mode (binder_types T)
+    val bs = map (pair "x") inpTs
+    val bounds = map Bound (rev (0 upto (length bs) - 1))
+    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
+  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
+
+fun register_alternative_function pred_name mode fun_name =
+  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
+    (pred_name, (mode, functional_compilation fun_name mode)))
+
+fun force_modes_and_functions pred_name fun_names =
+  force_modes_and_compilations pred_name
+    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
+    fun_names)
+
+(* structures for different compilations *)
+
 structure PredicateCompFuns =
 struct
 
@@ -873,6 +936,104 @@
 
 end;
 
+structure New_Pos_Random_Sequence_CompFuns =
+struct
+
+fun mk_pos_random_dseqT T =
+  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+
+fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+
+fun mk_single t =
+  let
+    val T = fastype_of t
+  in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
+  HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+  let
+    val pT = mk_pos_random_dseqT HOLogic.unitT
+    val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [Type (@{type_name Option.option}, [@{typ unit}])])
+
+  in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
+  (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
+
+val compfuns = CompilationFuns {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
+    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;
+
+structure New_Neg_Random_Sequence_CompFuns =
+struct
+
+fun mk_neg_random_dseqT T =
+   @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+    @{typ code_numeral} --> 
+    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+
+fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+      Type (@{type_name Lazy_Sequence.lazy_sequence},
+        [Type (@{type_name Option.option}, [T])])])])])])) = T
+  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+
+fun mk_single t =
+  let
+    val T = fastype_of t
+  in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+  let
+    val T as Type ("fun", [_, U]) = fastype_of f
+  in
+    Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+  end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
+  HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_not t =
+  let
+    val nT = mk_neg_random_dseqT HOLogic.unitT
+    val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
+  in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
+  (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
+
+val compfuns = CompilationFuns {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
+    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;
+
 structure Random_Sequence_CompFuns =
 struct
 
@@ -921,6 +1082,9 @@
 (* for external use with interactive mode *)
 val pred_compfuns = PredicateCompFuns.compfuns
 val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
+val new_randompred_compfuns = New_Pos_Random_Sequence_CompFuns.compfuns
+
+(* compilation modifiers *)
 
 (* function types and names of different compilations *)
 
@@ -932,6 +1096,264 @@
     inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
   end;
 
+structure Comp_Mod =
+struct
+
+datatype comp_modifiers = Comp_Modifiers of
+{
+  compilation : compilation,
+  function_name_prefix : string,
+  compfuns : compilation_funs,
+  mk_random : typ -> term list -> term,
+  modify_funT : typ -> typ,
+  additional_arguments : string list -> term list,
+  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
+  transform_additional_arguments : indprem -> term list -> term list
+}
+
+fun dest_comp_modifiers (Comp_Modifiers c) = c
+
+val compilation = #compilation o dest_comp_modifiers
+val function_name_prefix = #function_name_prefix o dest_comp_modifiers
+val compfuns = #compfuns o dest_comp_modifiers
+
+val mk_random = #mk_random o dest_comp_modifiers
+val funT_of' = funT_of o compfuns
+val modify_funT = #modify_funT o dest_comp_modifiers
+fun funT_of comp mode = modify_funT comp o funT_of' comp mode
+
+val additional_arguments = #additional_arguments o dest_comp_modifiers
+val wrap_compilation = #wrap_compilation o dest_comp_modifiers
+val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
+
+end;
+
+val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Depth_Limited,
+  function_name_prefix = "depth_limited_",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  additional_arguments = fn names =>
+    let
+      val depth_name = Name.variant names "depth"
+    in [Free (depth_name, @{typ code_numeral})] end,
+  modify_funT = (fn T => let val (Ts, U) = strip_type T
+  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
+  wrap_compilation =
+    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+    let
+      val [depth] = additional_arguments
+      val (_, Ts) = split_modeT' mode (binder_types T)
+      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+    in
+      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+        $ mk_bot compfuns (dest_predT compfuns T')
+        $ compilation
+    end,
+  transform_additional_arguments =
+    fn prem => fn additional_arguments =>
+    let
+      val [depth] = additional_arguments
+      val depth' =
+        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+    in [depth'] end
+  }
+
+val random_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Random,
+  function_name_prefix = "random_",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn T => fn additional_arguments =>
+  list_comb (Const(@{const_name Quickcheck.iter},
+  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
+    PredicateCompFuns.mk_predT T), additional_arguments)),
+  modify_funT = (fn T =>
+    let
+      val (Ts, U) = strip_type T
+      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
+    in (Ts @ Ts') ---> U end),
+  additional_arguments = (fn names =>
+    let
+      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
+    in
+      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
+        Free (seed, @{typ "code_numeral * code_numeral"})]
+    end),
+  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 depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Depth_Limited_Random,
+  function_name_prefix = "depth_limited_random_",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn T => fn additional_arguments =>
+  list_comb (Const(@{const_name Quickcheck.iter},
+  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
+    PredicateCompFuns.mk_predT T), tl additional_arguments)),
+  modify_funT = (fn T =>
+    let
+      val (Ts, U) = strip_type T
+      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+        @{typ "code_numeral * code_numeral"}]
+    in (Ts @ Ts') ---> U end),
+  additional_arguments = (fn names =>
+    let
+      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
+    in
+      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
+        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
+    end),
+  wrap_compilation =
+  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+    let
+      val depth = hd (additional_arguments)
+      val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
+        mode (binder_types T)
+      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+    in
+      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+        $ mk_bot compfuns (dest_predT compfuns T')
+        $ compilation
+    end,
+  transform_additional_arguments =
+    fn prem => fn additional_arguments =>
+    let
+      val [depth, nrandom, size, seed] = additional_arguments
+      val depth' =
+        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+    in [depth', nrandom, size, seed] end
+}
+
+val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Pred,
+  function_name_prefix = "",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  modify_funT = I,
+  additional_arguments = K [],
+  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
+  {
+  compilation = Annotated,
+  function_name_prefix = "annotated_",
+  compfuns = PredicateCompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  modify_funT = I,
+  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 dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = DSeq,
+  function_name_prefix = "dseq_",
+  compfuns = DSequence_CompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  modify_funT = I,
+  additional_arguments = K [],
+  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 pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Pos_Random_DSeq,
+  function_name_prefix = "random_dseq_",
+  compfuns = Random_Sequence_CompFuns.compfuns,
+  mk_random = (fn T => fn additional_arguments =>
+  let
+    val random = Const ("Quickcheck.random_class.random",
+      @{typ code_numeral} --> @{typ Random.seed} -->
+        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+  in
+    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
+      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
+  end),
+
+  modify_funT = I,
+  additional_arguments = K [],
+  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 neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = Neg_Random_DSeq,
+  function_name_prefix = "random_dseq_neg_",
+  compfuns = Random_Sequence_CompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  modify_funT = I,
+  additional_arguments = K [],
+  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 new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = New_Pos_Random_DSeq,
+  function_name_prefix = "new_random_dseq_",
+  compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
+  mk_random = (fn T => fn additional_arguments =>
+  let
+    val random = Const ("Quickcheck.random_class.random",
+      @{typ code_numeral} --> @{typ Random.seed} -->
+        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+  in
+    Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
+      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
+  end),
+  modify_funT = I,
+  additional_arguments = K [],
+  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 new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+  {
+  compilation = New_Neg_Random_DSeq,
+  function_name_prefix = "new_random_dseq_neg_",
+  compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
+  mk_random = (fn _ => error "no random generation"),
+  modify_funT = I,
+  additional_arguments = K [],
+  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)
+  }
+
+fun negative_comp_modifiers_of comp_modifiers =
+    (case Comp_Mod.compilation comp_modifiers of
+      Pos_Random_DSeq => neg_random_dseq_comp_modifiers
+    | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
+    | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
+    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
+    | c => comp_modifiers)
+
 (** mode analysis **)
 
 type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
@@ -1194,50 +1616,60 @@
     EQUAL => ord2 (x, x')
   | ord => ord
 
-fun deriv_ord2' thy modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun deriv_ord2' thy pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
   let
+    (* prefer modes without requirement for generating random values *)
     fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (length mvars1, length mvars2)
+    (* prefer non-random modes *)
     fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
         if random_mode_in_deriv modes t1 deriv1 then 1 else 0)
+    (* prefer modes with more input and less output *)
     fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
       int_ord (number_of_output_positions (head_mode_of deriv1),
         number_of_output_positions (head_mode_of deriv2))
+    (* prefer recursive calls *)
+    fun is_rec_premise t =
+      case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
+    fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+      int_ord (if is_rec_premise t1 then 0 else 1,
+        if is_rec_premise t2 then 0 else 1)
+    val ord = lex_ord mvars_ord (lex_ord random_mode_ord (lex_ord output_mode_ord recursive_ord))
   in
-    lex_ord mvars_ord (lex_ord random_mode_ord output_mode_ord)
-      ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
+    ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
   end
 
-fun deriv_ord2 thy modes t = deriv_ord2' thy modes t t
+fun deriv_ord2 thy pred modes t = deriv_ord2' thy pred modes t t
 
 fun deriv_ord ((deriv1, mvars1), (deriv2, mvars2)) =
   int_ord (length mvars1, length mvars2)
 
-fun premise_ord thy modes ((prem1, a1), (prem2, a2)) =
-  rev_option_ord (deriv_ord2' thy modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
+fun premise_ord thy pred modes ((prem1, a1), (prem2, a2)) =
+  rev_option_ord (deriv_ord2' thy pred modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
 
 fun print_mode_list modes =
   tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
     commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
 
-fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pol (modes, (pos_modes, neg_modes)) vs ps =
+fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pred
+  pol (modes, (pos_modes, neg_modes)) vs ps =
   let
     fun choose_mode_of_prem (Prem t) = partial_hd
-        (sort (deriv_ord2 thy modes t) (all_derivations_of thy pos_modes vs t))
+        (sort (deriv_ord2 thy pred modes t) (all_derivations_of thy pos_modes vs t))
       | choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
       | choose_mode_of_prem (Negprem t) = partial_hd
-          (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+          (sort (deriv_ord2 thy pred modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
              (all_derivations_of thy neg_modes vs t)))
       | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
   in
     if #reorder_premises mode_analysis_options then
-      partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps))
+      partial_hd (sort (premise_ord thy pred modes) (ps ~~ map choose_mode_of_prem ps))
     else
       SOME (hd ps, choose_mode_of_prem (hd ps))
   end
 
-fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy param_vs (modes :
+fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
   (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   let
     val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts []))
@@ -1262,7 +1694,7 @@
     fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
       | check_mode_prems acc_ps rnd vs ps =
         (case
-          (select_mode_prem mode_analysis_options thy pol (modes', (pos_modes', neg_modes')) vs ps) of
+          (select_mode_prem mode_analysis_options thy pred pol (modes', (pos_modes', neg_modes')) vs ps) of
           SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
             (known_vs_after p vs) (filter_out (equal p) ps)
         | SOME (p, SOME (deriv, missing_vars)) =>
@@ -1309,7 +1741,7 @@
     fun check_mode m =
       let
         val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ => 
-          map (check_mode_clause' mode_analysis_options thy param_vs modes m) rs)
+          map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
       in
         Output.cond_timeit false "aux part of check_mode for one mode" (fn _ => 
         case find_indices is_none res of
@@ -1332,7 +1764,7 @@
     (p, map (fn (m, rnd) =>
       (m, map
         ((fn (ts, ps, rnd) => (ts, ps)) o the o
-          check_mode_clause' mode_analysis_options thy param_vs modes m) rs)) ms)
+          check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
   end;
 
 fun fixp f (x : (string * ((bool * mode) * bool) list) list) =
@@ -1390,8 +1822,8 @@
       else
         map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
     fun iteration modes = map
-      (check_modes_pred' mode_analysis_options options thy param_vs clauses (modes @ extra_modes))
-        modes
+      (check_modes_pred' mode_analysis_options options thy param_vs clauses
+        (modes @ extra_modes)) modes
     val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
       Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
       if collect_errors then
@@ -1482,40 +1914,8 @@
     (t, names)
   end;
 
-structure Comp_Mod =
-struct
-
-datatype comp_modifiers = Comp_Modifiers of
-{
-  compilation : compilation,
-  function_name_prefix : string,
-  compfuns : compilation_funs,
-  mk_random : typ -> term list -> term,
-  modify_funT : typ -> typ,
-  additional_arguments : string list -> term list,
-  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
-  transform_additional_arguments : indprem -> term list -> term list
-}
-
-fun dest_comp_modifiers (Comp_Modifiers c) = c
-
-val compilation = #compilation o dest_comp_modifiers
-val function_name_prefix = #function_name_prefix o dest_comp_modifiers
-val compfuns = #compfuns o dest_comp_modifiers
-
-val mk_random = #mk_random o dest_comp_modifiers
-val funT_of' = funT_of o compfuns
-val modify_funT = #modify_funT o dest_comp_modifiers
-fun funT_of comp mode = modify_funT comp o funT_of' comp mode
-
-val additional_arguments = #additional_arguments o dest_comp_modifiers
-val wrap_compilation = #wrap_compilation o dest_comp_modifiers
-val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
-
-end;
-
 (* TODO: uses param_vs -- change necessary for compilation with new modes *)
-fun compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss arg = 
+fun compile_arg compilation_modifiers additional_arguments ctxt param_vs iss arg = 
   let
     fun map_params (t as Free (f, T)) =
       if member (op =) param_vs f then
@@ -1530,18 +1930,19 @@
       | map_params t = t
     in map_aterms map_params arg end
 
-fun compile_match compilation_modifiers compfuns additional_arguments
+fun compile_match compilation_modifiers additional_arguments
   param_vs iss ctxt eqs eqs' out_ts success_t =
   let
+    val compfuns = Comp_Mod.compfuns compilation_modifiers
     val eqs'' = maps mk_eq eqs @ eqs'
     val eqs'' =
-      map (compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss) eqs''
+      map (compile_arg compilation_modifiers additional_arguments ctxt param_vs iss) eqs''
     val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
     val name = Name.variant names "x";
     val name' = Name.variant (name :: names) "y";
     val T = HOLogic.mk_tupleT (map fastype_of out_ts);
     val U = fastype_of success_t;
-    val U' = dest_predT compfuns U;
+    val U' = dest_predT compfuns U;        
     val v = Free (name, T);
     val v' = Free (name', T);
   in
@@ -1564,16 +1965,20 @@
   | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
   | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
 
-fun compile_expr compilation_modifiers compfuns ctxt pol (t, deriv) additional_arguments =
+fun compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments =
   let
+    val compfuns = Comp_Mod.compfuns compilation_modifiers
     fun expr_of (t, deriv) =
       (case (t, deriv) of
         (t, Term Input) => SOME t
       | (t, Term Output) => NONE
       | (Const (name, T), Context mode) =>
-        SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-          (ProofContext.theory_of ctxt) name (pol, mode),
-          Comp_Mod.funT_of compilation_modifiers mode T))
+        (case alternative_compilation_of (ProofContext.theory_of ctxt) name mode of
+          SOME alt_comp => SOME (alt_comp compfuns T)
+        | NONE =>
+          SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+            (ProofContext.theory_of ctxt) name mode,
+            Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
         SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
       | (t, Context m) =>
@@ -1596,11 +2001,12 @@
     list_comb (the (expr_of (t, deriv)), additional_arguments)
   end
 
-fun compile_clause compilation_modifiers compfuns ctxt all_vs param_vs additional_arguments
-  (pol, mode) inp (ts, moded_ps) =
+fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+  mode inp (ts, moded_ps) =
   let
+    val compfuns = Comp_Mod.compfuns compilation_modifiers
     val iss = ho_arg_modes_of mode
-    val compile_match = compile_match compilation_modifiers compfuns
+    val compile_match = compile_match compilation_modifiers
       additional_arguments param_vs iss ctxt
     val (in_ts, out_ts) = split_mode mode ts;
     val (in_ts', (all_vs', eqs)) =
@@ -1629,8 +2035,7 @@
                Prem t =>
                  let
                    val u =
-                     compile_expr compilation_modifiers compfuns ctxt
-                       pol (t, deriv) additional_arguments'
+                     compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments'
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
@@ -1638,9 +2043,10 @@
                  end
              | Negprem t =>
                  let
+                   val neg_compilation_modifiers =
+                     negative_comp_modifiers_of compilation_modifiers
                    val u = mk_not compfuns
-                     (compile_expr compilation_modifiers compfuns ctxt
-                       (not pol) (t, deriv) additional_arguments')
+                     (compile_expr neg_compilation_modifiers ctxt (t, deriv) additional_arguments')
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
@@ -1648,7 +2054,7 @@
                  end
              | Sidecond t =>
                  let
-                   val t = compile_arg compilation_modifiers compfuns additional_arguments
+                   val t = compile_arg compilation_modifiers additional_arguments
                      ctxt param_vs iss t
                    val rest = compile_prems [] vs' names'' ps;
                  in
@@ -1673,6 +2079,8 @@
 fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
   let
     val ctxt = ProofContext.init thy
+    val compilation_modifiers = if pol then compilation_modifiers else
+      negative_comp_modifiers_of compilation_modifiers
     val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
       (all_vs @ param_vs)
     val compfuns = Comp_Mod.compfuns compilation_modifiers
@@ -1686,7 +2094,7 @@
     
     val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
       (fn T => fn (param_vs, names) =>
-        if is_param_type T then                                                
+        if is_param_type T then
           (Free (hd param_vs, T), (tl param_vs, names))
         else
           let
@@ -1696,8 +2104,8 @@
     val in_ts' = map_filter (map_filter_prod
       (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
     val cl_ts =
-      map (compile_clause compilation_modifiers compfuns
-        ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
+      map (compile_clause compilation_modifiers
+        ctxt 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
       (if null cl_ts then
@@ -1705,7 +2113,7 @@
       else foldr1 (mk_sup compfuns) cl_ts)
     val fun_const =
       Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
-      (ProofContext.theory_of ctxt) s (pol, mode), funT)
+      (ProofContext.theory_of ctxt) s mode, funT)
   in
     HOLogic.mk_Trueprop
       (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -2491,7 +2899,7 @@
             val arg_names = Name.variant_list []
               (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
             val args = map2 (curry Free) arg_names Ts
-            val predfun = Const (function_name_of Pred thy predname (true, full_mode),
+            val predfun = Const (function_name_of Pred thy predname full_mode,
               Ts ---> PredicateCompFuns.mk_predT @{typ unit})
             val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
             val eq_term = HOLogic.mk_Trueprop
@@ -2614,125 +3022,6 @@
       scc thy' |> Theory.checkpoint
   in thy'' end
 
-val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Depth_Limited,
-  function_name_prefix = "depth_limited_",
-  compfuns = PredicateCompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  additional_arguments = fn names =>
-    let
-      val depth_name = Name.variant names "depth"
-    in [Free (depth_name, @{typ code_numeral})] end,
-  modify_funT = (fn T => let val (Ts, U) = strip_type T
-  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
-  wrap_compilation =
-    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
-    let
-      val [depth] = additional_arguments
-      val (_, Ts) = split_modeT' mode (binder_types T)
-      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
-      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
-    in
-      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
-        $ mk_bot compfuns (dest_predT compfuns T')
-        $ compilation
-    end,
-  transform_additional_arguments =
-    fn prem => fn additional_arguments =>
-    let
-      val [depth] = additional_arguments
-      val depth' =
-        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
-          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
-    in [depth'] end
-  }
-
-val random_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Random,
-  function_name_prefix = "random_",
-  compfuns = PredicateCompFuns.compfuns,
-  mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Quickcheck.iter},
-  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    PredicateCompFuns.mk_predT T), additional_arguments)),
-  modify_funT = (fn T =>
-    let
-      val (Ts, U) = strip_type T
-      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
-    in (Ts @ Ts') ---> U end),
-  additional_arguments = (fn names =>
-    let
-      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
-    in
-      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
-        Free (seed, @{typ "code_numeral * code_numeral"})]
-    end),
-  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 depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Depth_Limited_Random,
-  function_name_prefix = "depth_limited_random_",
-  compfuns = PredicateCompFuns.compfuns,
-  mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Quickcheck.iter},
-  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
-    PredicateCompFuns.mk_predT T), tl additional_arguments)),
-  modify_funT = (fn T =>
-    let
-      val (Ts, U) = strip_type T
-      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
-        @{typ "code_numeral * code_numeral"}]
-    in (Ts @ Ts') ---> U end),
-  additional_arguments = (fn names =>
-    let
-      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
-    in
-      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
-        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
-    end),
-  wrap_compilation =
-  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
-    let
-      val depth = hd (additional_arguments)
-      val (_, Ts) = split_modeT' mode (binder_types T)
-      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
-      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
-    in
-      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
-        $ mk_bot compfuns (dest_predT compfuns T')
-        $ compilation
-    end,
-  transform_additional_arguments =
-    fn prem => fn additional_arguments =>
-    let
-      val [depth, nrandom, size, seed] = additional_arguments
-      val depth' =
-        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
-          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
-    in [depth', nrandom, size, seed] end
-}
-
-(* different instantiantions of the predicate compiler *)
-
-val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Pred,
-  function_name_prefix = "",
-  compfuns = PredicateCompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  modify_funT = I,
-  additional_arguments = K [],
-  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 add_equations = gen_add_equations
   (Steps {
   define_functions =
@@ -2745,70 +3034,6 @@
   use_random = false,
   qname = "equation"})
 
-val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Annotated,
-  function_name_prefix = "annotated_",
-  compfuns = PredicateCompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  modify_funT = I,
-  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 dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = DSeq,
-  function_name_prefix = "dseq_",
-  compfuns = DSequence_CompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  modify_funT = I,
-  additional_arguments = K [],
-  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 pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Pos_Random_DSeq,
-  function_name_prefix = "random_dseq_",
-  compfuns = Random_Sequence_CompFuns.compfuns,
-  mk_random = (fn T => fn additional_arguments =>
-  let
-    val random = Const ("Quickcheck.random_class.random",
-      @{typ code_numeral} --> @{typ Random.seed} -->
-        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
-  in
-    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
-      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
-      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
-  end),
-
-  modify_funT = I,
-  additional_arguments = K [],
-  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 neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {
-  compilation = Neg_Random_DSeq,
-  function_name_prefix = "random_dseq_neg_",
-  compfuns = Random_Sequence_CompFuns.compfuns,
-  mk_random = (fn _ => error "no random generation"),
-  modify_funT = I,
-  additional_arguments = K [],
-  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 add_depth_limited_equations = gen_add_equations
   (Steps {
   define_functions =
@@ -2887,6 +3112,23 @@
   use_random = true,
   qname = "random_dseq_equation"})
 
+val add_new_random_dseq_equations = gen_add_equations
+  (Steps {
+  define_functions =
+    fn options => fn preds => fn (s, modes) =>
+    let
+      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+    in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.compfuns
+      options preds (s, pos_modes)
+      #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.compfuns
+      options preds (s, neg_modes)
+    end,
+  prove = prove_by_skip,
+  add_code_equations = K (K I),
+  comp_modifiers = new_pos_random_dseq_comp_modifiers,
+  use_random = true,
+  qname = "new_random_dseq_equation"})
 
 (** user interface **)
 
@@ -2942,6 +3184,7 @@
            | Depth_Limited => add_depth_limited_equations
            | Random => add_random_equations
            | Depth_Limited_Random => add_depth_limited_random_equations
+           | New_Pos_Random_DSeq => add_new_random_dseq_equations
            | compilation => error ("Compilation not supported")
            ) options [const]))
       end
@@ -2960,6 +3203,11 @@
 val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
 val random_dseq_eval_ref =
   Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
+val new_random_dseq_eval_ref =
+  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
+val new_random_dseq_stats_eval_ref =
+    Unsynchronized.ref (NONE :
+      (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
 fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
@@ -2974,7 +3222,10 @@
     val body = subst_bounds (output_frees, body)
     val T_compr = HOLogic.mk_ptupleT fp Ts
     val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
-    val (pred as Const (name, T), all_args) = strip_comb body
+    val (pred as Const (name, T), all_args) =
+      case strip_comb body of
+        (Const (name, T), all_args) => (Const (name, T), all_args)
+      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
   in
     if defined_functions compilation thy name then
       let
@@ -3029,6 +3280,7 @@
             [@{term "(1, 1) :: code_numeral * code_numeral"}]
           | DSeq => []
           | Pos_Random_DSeq => []
+          | New_Pos_Random_DSeq => []
         val comp_modifiers =
           case compilation of
             Pred => predicate_comp_modifiers
@@ -3038,8 +3290,9 @@
           (*| Annotated => annotated_comp_modifiers*)
           | DSeq => dseq_comp_modifiers
           | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
-        val t_pred = compile_expr comp_modifiers compfuns (ProofContext.init thy)
-          true (body, deriv) additional_arguments;
+          | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
+        val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
+          (body, deriv) additional_arguments;
         val T_pred = dest_predT compfuns (fastype_of t_pred)
         val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
       in
@@ -3049,18 +3302,31 @@
       error "Evaluation with values is not possible because compilation with code_pred was not invoked"
   end
 
-fun eval thy param_user_modes (options as (compilation, arguments)) k t_compr =
+fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
   let
+    fun count xs x =
+      let
+        fun count' i [] = i
+          | count' i (x' :: xs) = if x = x' then count' (i + 1) xs else count' i xs
+      in count' 0 xs end
+    fun accumulate xs = map (fn x => (x, count xs x)) (sort int_ord (distinct (op =) xs))
     val compfuns =
       case compilation of
         Random => PredicateCompFuns.compfuns
       | DSeq => DSequence_CompFuns.compfuns
       | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
+      | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
       | _ => PredicateCompFuns.compfuns
     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 ts =
+    val t' =
+      if stats andalso compilation = New_Pos_Random_DSeq then
+        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
+          (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
+            @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
+      else
+        mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
+    val (ts, statistics) =
       case compilation of
        (* Random =>
           fst (Predicate.yieldn k
@@ -3071,27 +3337,48 @@
           let
             val [nrandom, size, depth] = arguments
           in
-            fst (DSequence.yieldn k
+            rpair NONE (fst (DSequence.yieldn k
               (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
                 (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   thy t' [] nrandom size
                 |> Random_Engine.run)
-              depth true)
+              depth true))
           end
       | DSeq =>
-          fst (DSequence.yieldn k
+          rpair NONE (fst (DSequence.yieldn k
             (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
-              DSequence.map thy t' []) (the_single arguments) true)
+              DSequence.map thy t' []) (the_single arguments) true))
+      | New_Pos_Random_DSeq =>
+          let
+            val [nrandom, size, depth] = arguments
+            val seed = Random_Engine.next_seed ()
+          in
+            if stats then
+              apsnd (SOME o accumulate) (split_list
+              (fst (Lazy_Sequence.yieldn k
+                (Code_Eval.eval NONE
+                  ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
+                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+                    |> Lazy_Sequence.map (apfst proc))
+                    thy t' [] nrandom size seed depth))))
+            else rpair NONE
+              (fst (Lazy_Sequence.yieldn k
+                (Code_Eval.eval NONE
+                  ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
+                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+                    |> Lazy_Sequence.map proc)
+                    thy t' [] nrandom size seed depth)))
+          end
       | _ =>
-          fst (Predicate.yieldn k
+          rpair NONE (fst (Predicate.yieldn k
             (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
-              Predicate.map thy t' []))
-  in (T, ts) end;
-
-fun values ctxt param_user_modes (raw_expected, comp_options) k t_compr =
+              Predicate.map thy t' [])))
+  in ((T, ts), statistics) end;
+
+fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
   let
     val thy = ProofContext.theory_of ctxt
-    val (T, ts) = eval thy param_user_modes comp_options k t_compr
+    val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
     val setT = HOLogic.mk_setT T
     val elems = HOLogic.mk_set T ts
     val cont = Free ("...", setT)
@@ -3106,20 +3393,36 @@
             "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
             "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
   in
-    if k = ~1 orelse length ts < k then elems
-      else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
+    (if k = ~1 orelse length ts < k then elems
+    else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont, statistics)
   end;
 
 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 param_user_modes options k t
+    val (t', stats) = values ctxt param_user_modes options k t
     val ty' = Term.type_of t'
     val ctxt' = Variable.auto_fixes t' ctxt
+    val pretty_stat =
+      case stats of
+          NONE => []
+        | SOME xs =>
+          let
+            val total = fold (curry (op +)) (map snd xs) 0
+            fun pretty_entry (s, n) =
+              [Pretty.str "size", Pretty.brk 1,
+               Pretty.str (string_of_int s), Pretty.str ":", Pretty.brk 1,
+               Pretty.str (string_of_int n), Pretty.fbrk]
+          in
+            [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
+             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
+             @ maps pretty_entry xs
+          end
     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')]) ();
+      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
+        @ pretty_stat)) ();
   in Pretty.writeln p end;
 
 end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -31,11 +31,8 @@
   case Item_Net.retrieve net t of
     [] => NONE
   | [(f, p)] =>
-    let
-      val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)
-    in
-      SOME (Envir.subst_term subst p)
-    end
+    SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
+      handle Pattern.MATCH => NONE
   | _ => NONE
 
 fun pred_of_function thy name =
@@ -202,11 +199,12 @@
               HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
             end)
         | _ =>
-        if has_split_thm thy (fst (strip_comb t)) then
+        case find_split_thm thy (fst (strip_comb t)) of
+          SOME raw_split_thm =>
           let
             val (f, args) = strip_comb t
-            val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
-            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+            val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+            val (assms, concl) = Logic.strip_horn (prop_of split_thm)
             val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
             val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
             val (_, split_args) = strip_comb split_t
@@ -231,7 +229,7 @@
           in
             maps flatten_of_assm assms
           end
-        else
+      | NONE =>
           let
             val (f, args) = strip_comb t
             val args = map (Pattern.eta_long []) args
@@ -326,8 +324,14 @@
       val thy'' = Fun_Pred.map
         (fold Item_Net.update (map (apfst Logic.varify_global)
           (distinct (op =) funs ~~ (#preds ind_result)))) thy'
+      fun functional_mode_of T =
+        list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
+      val thy''' = fold
+        (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
+          predname (functional_mode_of T) name)
+      (prednames ~~ distinct (op =) funs) thy''
     in
-      (specs, thy'')
+      (specs, thy''')
     end
 
 fun rewrite_intro thy intro =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -113,7 +113,7 @@
       (lhs, ((full_constname, [definition]) :: defs, thy'))
     end
   else
-    (case (fst (strip_comb atom)) of
+    case (fst (strip_comb atom)) of
       (Const (@{const_name If}, _)) => let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = MetaSimplifier.rewrite_term thy
@@ -122,14 +122,16 @@
         in
           flatten constname atom' (defs, thy)
         end
-    | _ =>  
-      if (has_split_thm thy (fst (strip_comb atom))) then
+    | _ =>
+      case find_split_thm thy (fst (strip_comb atom)) of
+        NONE => (atom, (defs, thy))
+      | SOME raw_split_thm =>
         let
           val (f, args) = strip_comb atom
-          val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
+          val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
           (* TODO: contextify things - this line is to unvarify the split_thm *)
           (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
-          val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+          val (assms, concl) = Logic.strip_horn (prop_of split_thm)
           val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
           val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
           val ths = maps (instantiated_case_rewrites thy) Tcons
@@ -182,8 +184,7 @@
         in
           (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end
-      else
-        (atom, (defs, thy)))
+
 
 fun flatten_intros constname intros thy =
   let

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 30 00:47:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -9,8 +9,14 @@
   (*val quickcheck : Proof.context -> term -> int -> term list option*)
   val test_ref :
     ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
+  val new_test_ref :
+    ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref;
+  val eval_random_ref :
+    ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref;
+
   val tracing : bool Unsynchronized.ref;
-  val quickcheck_compile_term : bool -> bool -> int ->
+  val quiet : bool Unsynchronized.ref;
+  val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
     Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
 (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
   val nrandom : int Unsynchronized.ref;
@@ -27,13 +33,20 @@
 val test_ref =
   Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
 
+val new_test_ref =
+  Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option)
+
+val eval_random_ref =
+  Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option);
+
+
 val tracing = Unsynchronized.ref false;
 
 val quiet = Unsynchronized.ref true;
 
 val target = "Quickcheck"
 
-val nrandom = Unsynchronized.ref 2;
+val nrandom = Unsynchronized.ref 3;
 
 val debug = Unsynchronized.ref false;
 
@@ -131,10 +144,18 @@
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
 val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
+val mk_return' = #mk_single (dest_compfuns Predicate_Compile_Core.pred_compfuns)
+val mk_bind' = #mk_bind (dest_compfuns Predicate_Compile_Core.pred_compfuns)
+
 val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
 val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
 val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
 
+val mk_new_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
+val mk_new_return = #mk_single (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
+val mk_new_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
+
+
 fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
   | mk_split_lambda [x] t = lambda x t
   | mk_split_lambda xs t =
@@ -160,7 +181,7 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
-fun compile_term options ctxt t =
+fun compile_term compilation options ctxt t =
   let
     val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
     val thy = (ProofContext.theory_of ctxt') 
@@ -181,33 +202,90 @@
     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     val (thy3, preproc_time) =  cpu_time "predicate preprocessing"
         (fn () => Predicate_Compile.preprocess options const thy2)
-    (* FIXME: this is just for testing the predicate compiler proof procedure! *)
-    val thy3' = Predicate_Compile_Core.add_equations options [full_constname] thy3
     val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
-        (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3')
-    val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4
-    val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname
+        (fn () =>
+          case compilation of
+            Pos_Random_DSeq =>
+              Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3
+          | New_Pos_Random_DSeq =>
+              Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
+          (*| Depth_Limited_Random =>
+              Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
+    val _ = Predicate_Compile_Core.print_all_modes compilation thy4
+    val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
     val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
     val prog =
       if member eq_mode modes output_mode then
         let
-          val name = Predicate_Compile_Core.function_name_of Pos_Random_DSeq thy4
-            full_constname (true, output_mode)
-          val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
+          val name = Predicate_Compile_Core.function_name_of compilation thy4
+            full_constname output_mode
+          val T = 
+            case compilation of
+              Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
+            | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
+            | Depth_Limited_Random =>
+              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+              @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
         in
           Const (name, T)
         end
       else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
-    val qc_term = mk_bind (prog,
-      mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
-      (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
-    val compilation =
-      Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
-        (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
-        thy4 qc_term []
+    
+    val qc_term =
+      case compilation of
+          Pos_Random_DSeq => mk_bind (prog,
+            mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
+            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+        | New_Pos_Random_DSeq => mk_new_bind (prog,
+            mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
+            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+        | Depth_Limited_Random => fold_rev (curry absdummy)
+            [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+             @{typ "code_numeral * code_numeral"}]
+            (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
+            mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
+            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
+    val prog =
+      case compilation of
+        Pos_Random_DSeq =>
+          let
+            val compiled_term =
+              Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
+                thy4 qc_term []
+          in
+            (fn size => fn nrandom => fn depth =>
+              Option.map fst (DSequence.yield
+                (compiled_term nrandom size |> Random_Engine.run) depth true))
+          end
+      | New_Pos_Random_DSeq =>
+          let
+            val compiled_term =
+              Code_Eval.eval (SOME target)
+                ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
+                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
+                  thy4 qc_term []
+          in
+            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
+               (
+               let
+                 val seed = Random_Engine.next_seed ()
+               in compiled_term nrandom size seed depth end))
+          end
+      | Depth_Limited_Random =>
+          let
+            val compiled_term = Code_Eval.eval (SOME target)
+              ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref)
+                (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+                  g depth nrandom size seed |> (Predicate.map o map) proc)
+                thy4 qc_term []
+          in
+            fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield 
+              (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
+          end
   in
-    (fn size => fn nrandom => fn depth =>
-      Option.map fst (DSequence.yield (compilation nrandom size |> Random_Engine.run) depth true))
+    prog
   end
 
 fun try_upto quiet f i =
@@ -229,21 +307,21 @@
 
 (* quickcheck interface functions *)
 
-fun compile_term' options depth ctxt report t =
+fun compile_term' compilation options depth ctxt report t =
   let
-    val c = compile_term options ctxt t
+    val c = compile_term compilation options ctxt t
     val dummy_report = ([], false)
   in
     fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
   end
 
-fun quickcheck_compile_term function_flattening fail_safe_function_flattening depth =
+fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
   let
      val options =
        set_fail_safe_function_flattening fail_safe_function_flattening
          (set_function_flattening function_flattening (get_options ()))
   in
-    compile_term' options depth
+    compile_term' compilation options depth
   end
 
 end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Tue Mar 30 12:47:39 2010 +0200
@@ -0,0 +1,214 @@
+(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
+    Author:     Lukas Bulwahn, TU Muenchen
+
+Deriving specialised predicates and their intro rules
+*)
+
+signature PREDICATE_COMPILE_SPECIALISATION =
+sig
+  val find_specialisations : string list -> (string * thm list) list -> theory -> (string * thm list) list * theory
+end;
+
+structure Predicate_Compile_Specialisation : PREDICATE_COMPILE_SPECIALISATION =
+struct
+
+open Predicate_Compile_Aux;
+
+(* table of specialisations *)
+structure Specialisations = Theory_Data
+(
+  type T = (term * term) Item_Net.T;
+  val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
+    (single o fst);
+  val extend = I;
+  val merge = Item_Net.merge;
+)
+
+fun specialisation_of thy atom =
+  Item_Net.retrieve (Specialisations.get thy) atom
+
+fun print_specialisations thy =
+  tracing (cat_lines (map (fn (t, spec_t) =>
+      Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t)
+    (Item_Net.content (Specialisations.get thy))))
+
+fun import (pred, intros) args ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt
+    val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
+    val Ts = binder_types (fastype_of pred')
+    val argTs = map fastype_of args
+    val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty
+    val args' = map (Envir.subst_term_types Tsubst) args
+  in
+    (((pred', intros'), args'), ctxt')
+  end
+
+(* patterns only constructed of variables and pairs/tuples are trivial constructor terms*)
+fun is_nontrivial_constrt thy t =
+  let
+    val cnstrs = flat (maps
+      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+      (Symtab.dest (Datatype.get_all thy)));
+    fun check t = (case strip_comb t of
+        (Var _, []) => (true, true)
+      | (Free _, []) => (true, true)
+      | (Const (@{const_name Pair}, _), ts) =>
+        pairself (forall I) (split_list (map check ts))
+      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+            (SOME (i, Tname), Type (Tname', _)) => (false,
+              length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
+          | _ => (false, false))
+      | _ => (false, false))
+  in check t = (false, true) end;
+
+fun specialise_intros black_list (pred, intros) pats thy =
+  let
+    val ctxt = ProofContext.init thy
+    val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
+    val pats = map (Logic.incr_indexes ([],  maxidx + 1)) pats
+    val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
+    val intros_t = map prop_of intros
+    val result_pats = map Var (fold_rev Term.add_vars pats [])
+    fun mk_fresh_name names =
+      let
+        val name =
+          Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+        val bname = Sign.full_bname thy name
+      in
+        if Sign.declared_const thy bname then
+          mk_fresh_name (name :: names)
+        else
+          bname
+      end
+    val constname = mk_fresh_name []
+    val constT = map fastype_of result_pats ---> @{typ bool}
+    val specialised_const = Const (constname, constT)
+    val specialisation =
+      [(HOLogic.mk_Trueprop (list_comb (pred, pats)),
+        HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))]
+    fun specialise_intro intro =
+      (let
+        val (prems, concl) = Logic.strip_horn (prop_of intro)
+        val env = Pattern.unify thy
+          (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0)
+        val prems = map (Envir.norm_term env) prems
+        val args = map (Envir.norm_term env) result_pats
+        val concl = HOLogic.mk_Trueprop (list_comb (specialised_const, args))
+        val intro = Logic.list_implies (prems, concl)
+      in
+        SOME intro
+      end handle Pattern.Unif => NONE)
+    val specialised_intros_t = map_filter I (map specialise_intro intros)
+    val thy' = Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
+    val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
+    val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
+    val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
+      [list_comb (pred, pats), list_comb (specialised_const, result_pats)]
+    val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
+    val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+    val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
+  in
+    thy''''
+  end
+
+and find_specialisations black_list specs thy =
+  let
+    val add_vars = fold_aterms (fn Var v => cons v | _ => I);
+    fun fresh_free T free_names =
+      let
+        val free_name = Name.variant free_names "x"
+      in
+        (Free (free_name, T), free_name :: free_names)
+      end
+    fun replace_term_and_restrict thy T t Tts free_names =
+      let
+        val (free, free_names') = fresh_free T free_names
+        val Tts' = map (apsnd (Pattern.rewrite_term thy [(t, free)] [])) Tts
+        val (ts', free_names'') = restrict_pattern' thy Tts' free_names'
+      in
+        (free :: ts', free_names'')
+      end
+    and restrict_pattern' thy [] free_names = ([], free_names)
+      | restrict_pattern' thy ((T, Free (x, _)) :: Tts) free_names =
+      let
+        val (ts', free_names') = restrict_pattern' thy Tts free_names
+      in
+        (Free (x, T) :: ts', free_names')
+      end
+      | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
+        replace_term_and_restrict thy T t Tts free_names
+      | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
+        case Datatype_Data.get_constrs thy Tcon of
+          NONE => replace_term_and_restrict thy T t Tts free_names
+        | SOME constrs => (case strip_comb t of
+          (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
+            SOME constr_T =>
+              let
+                val (Ts', T') = strip_type constr_T
+                val Tsubst = Type.raw_match (T', T) Vartab.empty
+                val Ts = map (Envir.subst_type Tsubst) Ts'
+                val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
+                val (ats', ts') = chop (length ats) bts'
+              in
+                (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
+              end
+            | NONE => replace_term_and_restrict thy T t Tts free_names))
+    fun restrict_pattern thy Ts args =
+      let
+        val args = map Logic.unvarify_global args
+        val Ts = map Logic.unvarifyT_global Ts
+        val free_names = fold Term.add_free_names args []
+        val (pat, _) = restrict_pattern' thy (Ts ~~ args) free_names
+      in map Logic.varify_global pat end
+    fun detect' atom thy =
+      case strip_comb atom of
+        (pred as Const (pred_name, _), args) =>
+          let
+          val Ts = binder_types (Sign.the_const_type thy pred_name)
+          val vnames = map fst (fold Term.add_var_names args [])
+          val pats = restrict_pattern thy Ts args
+        in
+          if (exists (is_nontrivial_constrt thy) pats)
+            orelse (has_duplicates (op =) (fold add_vars pats [])) then
+            let
+              val thy' =
+                case specialisation_of thy atom of
+                  [] =>
+                    if member (op =) ((map fst specs) @ black_list) pred_name then
+                      thy
+                    else
+                      (case try (Predicate_Compile_Core.intros_of thy) pred_name of
+                        NONE => thy
+                      | SOME intros =>
+                          specialise_intros ((map fst specs) @ (pred_name :: black_list))
+                            (pred, intros) pats thy)
+                  | (t, specialised_t) :: _ => thy
+                val atom' =
+                  case specialisation_of thy' atom of
+                    [] => atom
+                  | (t, specialised_t) :: _ =>
+                    let
+                      val subst = Pattern.match thy' (t, atom) (Vartab.empty, Vartab.empty)
+                    in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom
+                    (*FIXME: this exception could be caught earlier in specialisation_of *)
+            in
+              (atom', thy')
+            end
+          else (atom, thy)
+        end
+      | _ => (atom, thy)
+    fun specialise' (constname, intros) thy =
+      let
+        (* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *)
+        val intros = Drule.zero_var_indexes_list intros
+        val (intros_t', thy') = (fold_map o fold_map_atoms) detect' (map prop_of intros) thy
+      in
+        ((constname, map (Skip_Proof.make_thm thy') intros_t'), thy')
+      end
+  in
+    fold_map specialise' specs thy
+  end
+
+end;
\ No newline at end of file