# HG changeset patch
# User haftmann
# Date 1360852030 -3600
# Node ID df86080de4cbe098d556686afa3a072ff60f15d4
# Parent  f90874d3a246fb1495102abe75a80490dbf36ccb
reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

diff -r f90874d3a246 -r df86080de4cb src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -5,7 +5,7 @@
 header {* Term evaluation using the generic code generator *}
 
 theory Code_Evaluation
-imports Typerep New_DSequence
+imports Typerep Limited_Sequence
 begin
 
 subsection {* Term representation *}
diff -r f90874d3a246 -r df86080de4cb src/HOL/DSequence.thy
--- a/src/HOL/DSequence.thy	Thu Feb 14 17:58:28 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-
-(* Author: Lukas Bulwahn, TU Muenchen *)
-
-header {* Depth-Limited Sequences with failure element *}
-
-theory DSequence
-imports Lazy_Sequence
-begin
-
-type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
-
-definition empty :: "'a dseq"
-where
-  "empty = (%i pol. Some Lazy_Sequence.empty)"
-
-definition single :: "'a => 'a dseq"
-where
-  "single x = (%i pol. Some (Lazy_Sequence.single x))"
-
-fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
-where
-  "eval f i pol = f i pol"
-
-definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" 
-where
-  "yield dseq i pol = (case eval dseq i pol of
-    None => None
-  | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
-
-definition yieldn :: "code_numeral \<Rightarrow> 'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a list \<times> 'a dseq"
-where
-  "yieldn n dseq i pol = (case dseq i pol of
-    None \<Rightarrow> ([], \<lambda>i pol. None)
-  | Some s \<Rightarrow> let (xs, s') = Lazy_Sequence.yieldn n s in (xs, \<lambda>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
-    None => Some Lazy_Sequence.empty
-  | Some (x, xq') => (case eval (f x) i pol of
-      None => None
-    | Some yq => (case map_seq f xq' i pol of
-        None => None
-      | Some zq => Some (Lazy_Sequence.append yq zq))))"
-
-definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
-where
-  "bind x f = (%i pol. 
-     if i = 0 then
-       (if pol then Some Lazy_Sequence.empty else None)
-     else
-       (case x (i - 1) pol of
-         None => None
-       | Some xq => map_seq f xq i pol))"
-
-definition union :: "'a dseq => 'a dseq => 'a dseq"
-where
-  "union x y = (%i pol. case (x i pol, y i pol) of
-      (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
-    | _ => None)"
-
-definition if_seq :: "bool => unit dseq"
-where
-  "if_seq b = (if b then single () else empty)"
-
-definition not_seq :: "unit dseq => unit dseq"
-where
-  "not_seq x = (%i pol. case x i (\<not>pol) of
-    None => Some Lazy_Sequence.empty
-  | Some xq => (case Lazy_Sequence.yield xq of
-      None => Some (Lazy_Sequence.single ())
-    | Some _ => Some (Lazy_Sequence.empty)))"
-
-definition map :: "('a => 'b) => 'a dseq => 'b dseq"
-where
-  "map f g = (%i pol. case g i pol of
-     None => None
-   | Some xq => Some (Lazy_Sequence.map f xq))"
-
-ML {*
-signature DSEQUENCE =
-sig
-  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
-  val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
-  val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
-  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
-end;
-
-structure DSequence : DSEQUENCE =
-struct
-
-type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
-
-val yield = @{code yield}
-val yieldn = @{code yieldn}
-val map = @{code map}
-
-end;
-*}
-
-code_reserved Eval DSequence
-(*
-hide_type Sequence.seq
-
-hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
-  Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
-*)
-hide_const (open) empty single eval map_seq bind union if_seq not_seq map
-hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
-  if_seq_def not_seq_def map_def
-
-end
-
diff -r f90874d3a246 -r df86080de4cb src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Lazy_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -7,158 +7,230 @@
 imports Predicate
 begin
 
-datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
+subsection {* Type of lazy sequences *}
 
-definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence"
-where
-  "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
+datatype 'a lazy_sequence = lazy_sequence_of_list "'a list"
 
-code_datatype Lazy_Sequence 
-
-primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
+primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
 where
-  "yield Empty = None"
-| "yield (Insert x xq) = Some (x, xq)"
+  "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
+
+lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
+  "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
+  by (cases xq) simp_all
+
+lemma lazy_sequence_eqI:
+  "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
+  by (cases xq, cases yq) simp
+
+lemma lazy_sequence_eq_iff:
+  "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
+  by (auto intro: lazy_sequence_eqI)
 
-lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
-by (cases xq) auto
+lemma lazy_sequence_size_eq:
+  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
+  by (cases xq) simp
+
+lemma size_lazy_sequence_eq [code]:
+  "size (xq :: 'a lazy_sequence) = 0"
+  by (cases xq) simp
+
+lemma lazy_sequence_case [simp]:
+  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
+  by (cases xq) auto
+
+lemma lazy_sequence_rec [simp]:
+  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
+  by (cases xq) auto
 
-lemma yield_Seq [code]:
-  "yield (Lazy_Sequence f) = f ()"
-unfolding Lazy_Sequence_def by (cases "f ()") auto
+definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
+where
+  "Lazy_Sequence f = lazy_sequence_of_list (case f () of
+    None \<Rightarrow> []
+  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
+
+code_datatype Lazy_Sequence
+
+declare list_of_lazy_sequence.simps [code del]
+declare lazy_sequence.cases [code del]
+declare lazy_sequence.recs [code del]
 
-lemma Seq_yield:
-  "Lazy_Sequence (%u. yield f) = f"
-unfolding Lazy_Sequence_def by (cases f) auto
+lemma list_of_Lazy_Sequence [simp]:
+  "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
+    None \<Rightarrow> []
+  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
+  by (simp add: Lazy_Sequence_def)
+
+definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
+where
+  "yield xq = (case list_of_lazy_sequence xq of
+    [] \<Rightarrow> None
+  | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
+
+lemma yield_Seq [simp, code]:
+  "yield (Lazy_Sequence f) = f ()"
+  by (cases "f ()") (simp_all add: yield_def split_def)
+
+lemma case_yield_eq [simp]: "option_case g h (yield xq) =
+  list_case g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
+  by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
 
 lemma lazy_sequence_size_code [code]:
-  "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
-by (cases xq) auto
+  "lazy_sequence_size s xq = (case yield xq of
+    None \<Rightarrow> 1
+  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
+  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
 
-lemma size_code [code]:
-  "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
-by (cases xq) auto
-
-lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
-  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
-apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
-apply (cases yq) apply (auto simp add: equal_eq) done
+lemma equal_lazy_sequence_code [code]:
+  "HOL.equal xq yq = (case (yield xq, yield yq) of
+    (None, None) \<Rightarrow> True
+  | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
+  | _ \<Rightarrow> False)"
+  by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
 
 lemma [code nbe]:
   "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
   by (fact equal_refl)
 
-lemma seq_case [code]:
-  "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
-by (cases xq) auto
-
-lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))"
-by (cases xq) auto
-
 definition empty :: "'a lazy_sequence"
 where
-  [code]: "empty = Lazy_Sequence (%u. None)"
+  "empty = lazy_sequence_of_list []"
 
-definition single :: "'a => 'a lazy_sequence"
-where
-  [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
+lemma list_of_lazy_sequence_empty [simp]:
+  "list_of_lazy_sequence empty = []"
+  by (simp add: empty_def)
 
-primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
-where
-  "append Empty yq = yq"
-| "append (Insert x xq) yq = Insert x (append xq yq)"
+lemma empty_code [code]:
+  "empty = Lazy_Sequence (\<lambda>_. None)"
+  by (simp add: lazy_sequence_eq_iff)
 
-lemma [code]:
-  "append xq yq = Lazy_Sequence (%u. case yield xq of
-     None => yield yq
-  | Some (x, xq') => Some (x, append xq' yq))"
-unfolding Lazy_Sequence_def
-apply (cases "xq")
-apply auto
-apply (cases "yq")
-apply auto
-done
+definition single :: "'a \<Rightarrow> 'a lazy_sequence"
+where
+  "single x = lazy_sequence_of_list [x]"
 
-primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
+lemma list_of_lazy_sequence_single [simp]:
+  "list_of_lazy_sequence (single x) = [x]"
+  by (simp add: single_def)
+
+lemma single_code [code]:
+  "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
+  by (simp add: lazy_sequence_eq_iff)
+
+definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
 where
-  "flat Empty = Empty"
-| "flat (Insert xq xqq) = append xq (flat xqq)"
- 
-lemma [code]:
-  "flat xqq = Lazy_Sequence (%u. case yield xqq of
-    None => None
-  | Some (xq, xqq') => yield (append xq (flat xqq')))"
-apply (cases "xqq")
-apply (auto simp add: Seq_yield)
-unfolding Lazy_Sequence_def
-by auto
+  "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
+
+lemma list_of_lazy_sequence_append [simp]:
+  "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
+  by (simp add: append_def)
 
-primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
+lemma append_code [code]:
+  "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
+    None \<Rightarrow> yield yq
+  | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
+  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
 where
-  "map f Empty = Empty"
-| "map f (Insert x xq) = Insert (f x) (map f xq)"
+  "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
+
+lemma list_of_lazy_sequence_map [simp]:
+  "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
+  by (simp add: map_def)
+
+lemma map_code [code]:
+  "map f xq =
+    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
+  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
+
+definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
+where
+  "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
 
-lemma [code]:
-  "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
-apply (cases xq)
-apply (auto simp add: Seq_yield)
-unfolding Lazy_Sequence_def
-apply auto
-done
+lemma list_of_lazy_sequence_flat [simp]:
+  "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
+  by (simp add: flat_def)
 
-definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
+lemma flat_code [code]:
+  "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
+    None \<Rightarrow> None
+  | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
+  by (simp add: lazy_sequence_eq_iff split: list.splits)
+
+definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
 where
-  [code]: "bind xq f = flat (map f xq)"
+  "bind xq f = flat (map f xq)"
 
-definition if_seq :: "bool => unit lazy_sequence"
+definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
 where
   "if_seq b = (if b then single () else empty)"
 
-function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
+definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
 where
-  "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
-by pat_completeness auto
+  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
+  
+function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a lazy_sequence"
+where
+  "iterate_upto f n m =
+    Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
+  by pat_completeness auto
 
 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
 
-definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
+definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
 where
-  "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
-
-subsection {* Code setup *}
+  "not_seq xq = (case yield xq of
+    None \<Rightarrow> single ()
+  | Some ((), xq) \<Rightarrow> empty)"
 
-fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
-  "anamorph f k x = (if k = 0 then ([], x)
-    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
-      let (vs, z) = anamorph f (k - 1) y
-    in (v # vs, z))"
-
-definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
-  "yieldn = anamorph yield"
+  
+subsection {* Code setup *}
 
 code_reflect Lazy_Sequence
   datatypes lazy_sequence = Lazy_Sequence
-  functions map yield yieldn
+
+ML {*
+signature LAZY_SEQUENCE =
+sig
+  datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
+  val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
+  val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
+  val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
+end;
+
+structure Lazy_Sequence : LAZY_SEQUENCE =
+struct
+
+datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
+
+fun map f = @{code Lazy_Sequence.map} f;
+
+fun yield P = @{code Lazy_Sequence.yield} P;
+
+fun yieldn k = Predicate.anamorph yield k;
+
+end;
+*}
+
 
 subsection {* Generator Sequences *}
 
-
 subsubsection {* General lazy sequence operation *}
 
-definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
+definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
 where
-  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
+  "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
 
 
 subsubsection {* Small lazy typeclasses *}
 
 class small_lazy =
-  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
+  fixes small_lazy :: "code_numeral \<Rightarrow> 'a lazy_sequence"
 
 instantiation unit :: small_lazy
 begin
 
-definition "small_lazy d = Lazy_Sequence.single ()"
+definition "small_lazy d = single ()"
 
 instance ..
 
@@ -170,15 +242,17 @@
 text {* maybe optimise this expression -> append (single x) xs == cons x xs 
 Performance difference? *}
 
-function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
-where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
-  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
-by pat_completeness auto
+function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
+where
+  "small_lazy' d i = (if d < i then empty
+    else append (single i) (small_lazy' d (i + 1)))"
+    by pat_completeness auto
 
 termination 
   by (relation "measure (%(d, i). nat (d + 1 - i))") auto
 
-definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+definition
+  "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
 
 instance ..
 
@@ -197,9 +271,11 @@
 instantiation list :: (small_lazy) small_lazy
 begin
 
-fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
+fun small_lazy_list :: "code_numeral \<Rightarrow> 'a list lazy_sequence"
 where
-  "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
+  "small_lazy_list d = append (single [])
+    (if d > 0 then bind (product (small_lazy (d - 1))
+      (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
 
 instance ..
 
@@ -212,56 +288,61 @@
 
 definition hit_bound :: "'a hit_bound_lazy_sequence"
 where
-  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
+  "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
 
-definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
+lemma list_of_lazy_sequence_hit_bound [simp]:
+  "list_of_lazy_sequence hit_bound = [None]"
+  by (simp add: hit_bound_def)
+  
+definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
 where
-  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
+  "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
 
-primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
+definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b 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)"
+  "hb_map f xq = map (Option.map f) xq"
+
+lemma hb_map_code [code]:
+  "hb_map f xq =
+    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
+  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
 
-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
+definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
+where
+  "hb_flat xqq = lazy_sequence_of_list (concat
+    (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq)))"
 
-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 list_of_lazy_sequence_hb_flat [simp]:
+  "list_of_lazy_sequence (hb_flat xqq) =
+    concat (List.map ((\<lambda>x. case x of None \<Rightarrow> [None] | Some xs \<Rightarrow> xs) \<circ> Option.map list_of_lazy_sequence) (list_of_lazy_sequence xqq))"
+  by (simp add: hb_flat_def)
 
-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
+lemma hb_flat_code [code]:
+  "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
+    None \<Rightarrow> None
+  | Some (xq, xqq') \<Rightarrow> yield
+     (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
+  by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
 
-definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
+definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
 where
-  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
+  "hb_bind xq f = hb_flat (hb_map f xq)"
 
-definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
+definition hb_if_seq :: "bool \<Rightarrow> 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"
+definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
 where
-  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
+  "hb_not_seq xq = (case yield xq of
+    None \<Rightarrow> single ()
+  | Some (x, xq) \<Rightarrow> empty)"
 
-hide_type (open) lazy_sequence
-hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
-  iterate_upto not_seq product
-  
-hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
-  iterate_upto.simps product_def if_seq_def not_seq_def
+hide_const (open) yield empty single append flat map bind
+  if_seq those iterate_upto not_seq product
+
+hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
+  if_seq_def those_def not_seq_def product_def 
 
 end
+
diff -r f90874d3a246 -r df86080de4cb src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Library/DAList.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -117,7 +117,7 @@
 
 fun (in term_syntax) random_aux_alist 
 where
-  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
+  "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck_Random.collapse (Random.select_weight [(i, Quickcheck_Random.random j \<circ>\<rightarrow> (%k. Quickcheck_Random.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))"
 
 instantiation alist :: (random, random) random
 begin
diff -r f90874d3a246 -r df86080de4cb src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -1314,7 +1314,7 @@
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
+  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
 
 instance ..
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/Limited_Sequence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Limited_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -0,0 +1,216 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Depth-Limited Sequences with failure element *}
+
+theory Limited_Sequence
+imports Lazy_Sequence
+begin
+
+subsection {* Depth-Limited Sequence *}
+
+type_synonym 'a dseq = "code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
+
+definition empty :: "'a dseq"
+where
+  "empty = (\<lambda>_ _. Some Lazy_Sequence.empty)"
+
+definition single :: "'a \<Rightarrow> 'a dseq"
+where
+  "single x = (\<lambda>_ _. Some (Lazy_Sequence.single x))"
+
+definition eval :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
+where
+  [simp]: "eval f i pol = f i pol"
+
+definition yield :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> ('a \<times> 'a dseq) option" 
+where
+  "yield f i pol = (case eval f i pol of
+    None \<Rightarrow> None
+  | Some s \<Rightarrow> (Option.map \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
+
+definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq"
+where
+  "map_seq f xq i pol = Option.map Lazy_Sequence.flat
+    (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))"
+
+lemma map_seq_code [code]:
+  "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
+    None \<Rightarrow> Some Lazy_Sequence.empty
+  | Some (x, xq') \<Rightarrow> (case eval (f x) i pol of
+      None \<Rightarrow> None
+    | Some yq \<Rightarrow> (case map_seq f xq' i pol of
+        None \<Rightarrow> None
+      | Some zq \<Rightarrow> Some (Lazy_Sequence.append yq zq))))"
+  by (cases xq)
+    (auto simp add: map_seq_def Lazy_Sequence.those_def lazy_sequence_eq_iff split: list.splits option.splits)
+
+definition bind :: "'a dseq \<Rightarrow> ('a \<Rightarrow> 'b dseq) \<Rightarrow> 'b dseq"
+where
+  "bind x f = (\<lambda>i pol. 
+     if i = 0 then
+       (if pol then Some Lazy_Sequence.empty else None)
+     else
+       (case x (i - 1) pol of
+         None \<Rightarrow> None
+       | Some xq \<Rightarrow> map_seq f xq i pol))"
+
+definition union :: "'a dseq \<Rightarrow> 'a dseq \<Rightarrow> 'a dseq"
+where
+  "union x y = (\<lambda>i pol. case (x i pol, y i pol) of
+      (Some xq, Some yq) \<Rightarrow> Some (Lazy_Sequence.append xq yq)
+    | _ \<Rightarrow> None)"
+
+definition if_seq :: "bool \<Rightarrow> unit dseq"
+where
+  "if_seq b = (if b then single () else empty)"
+
+definition not_seq :: "unit dseq \<Rightarrow> unit dseq"
+where
+  "not_seq x = (\<lambda>i pol. case x i (\<not> pol) of
+    None \<Rightarrow> Some Lazy_Sequence.empty
+  | Some xq \<Rightarrow> (case Lazy_Sequence.yield xq of
+      None \<Rightarrow> Some (Lazy_Sequence.single ())
+    | Some _ \<Rightarrow> Some (Lazy_Sequence.empty)))"
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dseq \<Rightarrow> 'b dseq"
+where
+  "map f g = (\<lambda>i pol. case g i pol of
+     None \<Rightarrow> None
+   | Some xq \<Rightarrow> Some (Lazy_Sequence.map f xq))"
+
+
+subsection {* Positive Depth-Limited Sequence *}
+
+type_synonym 'a pos_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
+
+definition pos_empty :: "'a pos_dseq"
+where
+  "pos_empty = (\<lambda>i. Lazy_Sequence.empty)"
+
+definition pos_single :: "'a \<Rightarrow> 'a pos_dseq"
+where
+  "pos_single x = (\<lambda>i. Lazy_Sequence.single x)"
+
+definition pos_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
+where
+  "pos_bind x f = (\<lambda>i. Lazy_Sequence.bind (x i) (\<lambda>a. f a i))"
+
+definition pos_decr_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
+where
+  "pos_decr_bind x f = (\<lambda>i. 
+     if i = 0 then
+       Lazy_Sequence.empty
+     else
+       Lazy_Sequence.bind (x (i - 1)) (\<lambda>a. f a i))"
+
+definition pos_union :: "'a pos_dseq \<Rightarrow> 'a pos_dseq \<Rightarrow> 'a pos_dseq"
+where
+  "pos_union xq yq = (\<lambda>i. Lazy_Sequence.append (xq i) (yq i))"
+
+definition pos_if_seq :: "bool \<Rightarrow> unit pos_dseq"
+where
+  "pos_if_seq b = (if b then pos_single () else pos_empty)"
+
+definition pos_iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a pos_dseq"
+where
+  "pos_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto f n m)"
+ 
+definition pos_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pos_dseq \<Rightarrow> 'b pos_dseq"
+where
+  "pos_map f xq = (\<lambda>i. Lazy_Sequence.map f (xq i))"
+
+
+subsection {* Negative Depth-Limited Sequence *}
+
+type_synonym 'a neg_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.hit_bound_lazy_sequence"
+
+definition neg_empty :: "'a neg_dseq"
+where
+  "neg_empty = (\<lambda>i. Lazy_Sequence.empty)"
+
+definition neg_single :: "'a \<Rightarrow> 'a neg_dseq"
+where
+  "neg_single x = (\<lambda>i. Lazy_Sequence.hb_single x)"
+
+definition neg_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
+where
+  "neg_bind x f = (\<lambda>i. hb_bind (x i) (\<lambda>a. f a i))"
+
+definition neg_decr_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
+where
+  "neg_decr_bind x f = (\<lambda>i. 
+     if i = 0 then
+       Lazy_Sequence.hit_bound
+     else
+       hb_bind (x (i - 1)) (\<lambda>a. f a i))"
+
+definition neg_union :: "'a neg_dseq \<Rightarrow> 'a neg_dseq \<Rightarrow> 'a neg_dseq"
+where
+  "neg_union x y = (\<lambda>i. Lazy_Sequence.append (x i) (y i))"
+
+definition neg_if_seq :: "bool \<Rightarrow> unit neg_dseq"
+where
+  "neg_if_seq b = (if b then neg_single () else neg_empty)"
+
+definition neg_iterate_upto 
+where
+  "neg_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto (\<lambda>i. Some (f i)) n m)"
+
+definition neg_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a neg_dseq \<Rightarrow> 'b neg_dseq"
+where
+  "neg_map f xq = (\<lambda>i. Lazy_Sequence.hb_map f (xq i))"
+
+
+subsection {* Negation *}
+
+definition pos_not_seq :: "unit neg_dseq \<Rightarrow> unit pos_dseq"
+where
+  "pos_not_seq xq = (\<lambda>i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
+
+definition neg_not_seq :: "unit pos_dseq \<Rightarrow> unit neg_dseq"
+where
+  "neg_not_seq x = (\<lambda>i. case Lazy_Sequence.yield (x i) of
+    None => Lazy_Sequence.hb_single ()
+  | Some ((), xq) => Lazy_Sequence.empty)"
+
+
+ML {*
+signature LIMITED_SEQUENCE =
+sig
+  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
+  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
+  val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
+  val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
+end;
+
+structure Limited_Sequence : LIMITED_SEQUENCE =
+struct
+
+type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
+
+fun map f = @{code Limited_Sequence.map} f;
+
+fun yield f = @{code Limited_Sequence.yield} f;
+
+fun yieldn n f i pol = (case f i pol of
+    NONE => ([], fn _ => fn _ => NONE)
+  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn _ => fn _ => SOME s') end);
+
+end;
+*}
+
+code_reserved Eval Limited_Sequence
+
+
+hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
+  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
+  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
+
+hide_fact (open) yield_def empty_def single_def eval_def map_seq_def bind_def union_def
+  if_seq_def not_seq_def map_def
+  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_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_iterate_upto_def neg_not_seq_def neg_map_def
+
+end
+
diff -r f90874d3a246 -r df86080de4cb src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -269,7 +269,7 @@
  @{const_name transfer_morphism},
  @{const_name enum_prod_inst.enum_all_prod},
  @{const_name enum_prod_inst.enum_ex_prod},
- @{const_name Quickcheck.catch_match},
+ @{const_name Quickcheck_Random.catch_match},
  @{const_name Quickcheck_Exhaustive.unknown},
  @{const_name Num.Bit0}, @{const_name Num.Bit1}
  (*@{const_name "==>"}, @{const_name "=="}*)]
diff -r f90874d3a246 -r df86080de4cb src/HOL/New_DSequence.thy
--- a/src/HOL/New_DSequence.thy	Thu Feb 14 17:58:28 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-
-(* Author: Lukas Bulwahn, TU Muenchen *)
-
-header {* Depth-Limited Sequences with failure element *}
-
-theory New_DSequence
-imports DSequence
-begin
-
-subsection {* Positive Depth-Limited Sequence *}
-
-type_synonym '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. Lazy_Sequence.bind (x i) (%a. f a i))"
-
-definition pos_decr_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
-where
-  "pos_decr_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_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_dseq"
-where
-  "pos_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto f n m)"
- 
-definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
-where
-  "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
-
-subsection {* Negative Depth-Limited Sequence *}
-
-type_synonym '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. hb_bind (x i) (%a. f a i))"
-
-definition neg_decr_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
-where
-  "neg_decr_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_iterate_upto 
-where
-  "neg_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto (%i. Some (f i)) n m)"
-
-definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
-where
-  "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
-
-subsection {* Negation *}
-
-definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
-where
-  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * 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_type (open) pos_dseq neg_dseq
-
-hide_const (open)
-  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
-  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
-hide_fact (open)
-  pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_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_iterate_upto_def neg_not_seq_def neg_map_def
-
-end
diff -r f90874d3a246 -r df86080de4cb src/HOL/New_Random_Sequence.thy
--- a/src/HOL/New_Random_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-
-(* Author: Lukas Bulwahn, TU Muenchen *)
-
-theory New_Random_Sequence
-imports Random_Sequence
-begin
-
-type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
-type_synonym '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_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
-where
-  "pos_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_decr_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_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
-where
-  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)"
-
-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_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
-where
-  "neg_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_decr_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_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
-where
-  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)"
-
-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_const (open)
-  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
-  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto 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_fact (open) 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
diff -r f90874d3a246 -r df86080de4cb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Predicate.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -600,25 +600,34 @@
 
 code_reflect Predicate
   datatypes pred = Seq and seq = Empty | Insert | Join
-  functions map
 
 ML {*
 signature PREDICATE =
 sig
+  val anamorph: ('a -> ('b * 'a) option) -> int -> 'a -> 'b list * 'a
   datatype 'a pred = Seq of (unit -> 'a seq)
   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
+  val map: ('a -> 'b) -> 'a pred -> 'b pred
   val yield: 'a pred -> ('a * 'a pred) option
   val yieldn: int -> 'a pred -> 'a list * 'a pred
-  val map: ('a -> 'b) -> 'a pred -> 'b pred
 end;
 
 structure Predicate : PREDICATE =
 struct
 
+fun anamorph f k x =
+ (if k = 0 then ([], x)
+  else case f x
+   of NONE => ([], x)
+    | SOME (v, y) => let
+        val k' = k - 1;
+        val (vs, z) = anamorph f k' y
+      in (v :: vs, z) end);
+
 datatype pred = datatype Predicate.pred
 datatype seq = datatype Predicate.seq
 
-fun map f = Predicate.map f;
+fun map f = @{code Predicate.map} f;
 
 fun yield (Seq f) = next (f ())
 and next Empty = NONE
@@ -627,14 +636,7 @@
      of NONE => next xq
       | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
 
-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 P = anamorph yield P;
+fun yieldn k = anamorph yield k;
 
 end;
 *}
diff -r f90874d3a246 -r df86080de4cb src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Predicate_Compile.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -5,7 +5,7 @@
 header {* A compiler for predicates defined by introduction rules *}
 
 theory Predicate_Compile
-imports New_Random_Sequence Quickcheck_Exhaustive
+imports Random_Sequence Quickcheck_Exhaustive
 keywords "code_pred" :: thy_goal and "values" :: diag
 begin
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Feb 14 17:58:28 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,284 +0,0 @@
-(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
-
-header {* A simple counterexample generator performing random testing *}
-
-theory Quickcheck
-imports Random Code_Evaluation Enum
-begin
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
-
-subsection {* Catching Match exceptions *}
-
-axiomatization catch_match :: "'a => 'a => 'a"
-
-code_const catch_match 
-  (Quickcheck "((_) handle Match => _)")
-
-subsection {* The @{text random} class *}
-
-class random = typerep +
-  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-
-subsection {* Fundamental and numeric types*}
-
-instantiation bool :: random
-begin
-
-definition
-  "random i = Random.range 2 \<circ>\<rightarrow>
-    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
-
-instance ..
-
-end
-
-instantiation itself :: (typerep) random
-begin
-
-definition
-  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
-
-instance ..
-
-end
-
-instantiation char :: random
-begin
-
-definition
-  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
-
-instance ..
-
-end
-
-instantiation String.literal :: random
-begin
-
-definition 
-  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
-
-instance ..
-
-end
-
-instantiation nat :: random
-begin
-
-definition random_nat :: "code_numeral \<Rightarrow> Random.seed
-  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
-where
-  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
-     let n = Code_Numeral.nat_of k
-     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
-
-instance ..
-
-end
-
-instantiation int :: random
-begin
-
-definition
-  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
-     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
-     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
-
-instance ..
-
-end
-
-
-subsection {* Complex generators *}
-
-text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
-
-axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
-  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
-  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
-  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
-  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-where
-  "random_fun_lift f =
-    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
-
-instantiation "fun" :: ("{equal, term_of}", random) random
-begin
-
-definition
-  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-  where "random i = random_fun_lift (random i)"
-
-instance ..
-
-end
-
-text {* Towards type copies and datatypes *}
-
-definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
-  where "collapse f = (f \<circ>\<rightarrow> id)"
-
-definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
-  where "beyond k l = (if l > k then l else 0)"
-
-lemma beyond_zero: "beyond k 0 = 0"
-  by (simp add: beyond_def)
-
-
-definition (in term_syntax) [code_unfold]:
-  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
-
-definition (in term_syntax) [code_unfold]:
-  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
-
-instantiation set :: (random) random
-begin
-
-primrec random_aux_set
-where
-  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
-| "random_aux_set (Code_Numeral.Suc i) j =
-    collapse (Random.select_weight
-      [(1, Pair valterm_emptyset),
-       (Code_Numeral.Suc i,
-        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
-
-lemma [code]:
-  "random_aux_set i j =
-    collapse (Random.select_weight [(1, Pair valterm_emptyset),
-      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
-proof (induct i rule: code_numeral.induct)
-  case zero
-  show ?case by (subst select_weight_drop_zero [symmetric])
-    (simp add: random_aux_set.simps [simplified])
-next
-  case (Suc i)
-  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
-qed
-
-definition "random_set i = random_aux_set i i"
-
-instance ..
-
-end
-
-lemma random_aux_rec:
-  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
-  assumes "random_aux 0 = rhs 0"
-    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
-  shows "random_aux k = rhs k"
-  using assms by (rule code_numeral.induct)
-
-subsection {* Deriving random generators for datatypes *}
-
-ML_file "Tools/Quickcheck/quickcheck_common.ML" 
-ML_file "Tools/Quickcheck/random_generators.ML"
-setup Random_Generators.setup
-
-
-subsection {* Code setup *}
-
-code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
-  -- {* With enough criminal energy this can be abused to derive @{prop False};
-  for this reason we use a distinguished target @{text Quickcheck}
-  not spoiling the regular trusted code generation *}
-
-code_reserved Quickcheck Random_Generators
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-subsection {* The Random-Predicate Monad *} 
-
-fun iter' ::
-  "'a itself => code_numeral => code_numeral => code_numeral * code_numeral
-    => ('a::random) Predicate.pred"
-where
-  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
-     let ((x, _), seed') = random sz seed
-   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
-
-definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral
-  => ('a::random) Predicate.pred"
-where
-  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
-
-lemma [code]:
-  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
-     let ((x, _), seed') = random sz seed
-   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
-unfolding iter_def iter'.simps[of _ nrandom] ..
-
-type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
-
-definition empty :: "'a randompred"
-  where "empty = Pair (bot_class.bot)"
-
-definition single :: "'a => 'a randompred"
-  where "single x = Pair (Predicate.single x)"
-
-definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
-  where
-    "bind R f = (\<lambda>s. let
-       (P, s') = R s;
-       (s1, s2) = Random.split_seed s'
-     in (Predicate.bind P (%a. fst (f a s1)), s2))"
-
-definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
-where
-  "union R1 R2 = (\<lambda>s. let
-     (P1, s') = R1 s; (P2, s'') = R2 s'
-   in (sup_class.sup P1 P2, s''))"
-
-definition if_randompred :: "bool \<Rightarrow> unit randompred"
-where
-  "if_randompred b = (if b then single () else empty)"
-
-definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
-where
-  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
-
-definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
-where
-  "not_randompred P = (\<lambda>s. let
-     (P', s') = P s
-   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
-
-definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
-  where "Random g = scomp g (Pair o (Predicate.single o fst))"
-
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
-  where "map f P = bind P (single o f)"
-
-hide_fact
-  random_bool_def
-  random_itself_def
-  random_char_def
-  random_literal_def
-  random_nat_def
-  random_int_def
-  random_fun_lift_def
-  random_fun_def
-  collapse_def
-  beyond_def
-  beyond_zero
-  random_aux_rec
-
-hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
-
-hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def
-  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
-hide_type (open) randompred
-hide_const (open) iter' iter empty single bind union if_randompred
-  iterate_upto not_randompred Random map
-
-end
-
diff -r f90874d3a246 -r df86080de4cb src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -3,7 +3,7 @@
 header {* A simple counterexample generator performing exhaustive testing *}
 
 theory Quickcheck_Exhaustive
-imports Quickcheck
+imports Quickcheck_Random
 keywords "quickcheck_generator" :: thy_decl
 begin
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/Quickcheck_Random.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Random.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -0,0 +1,204 @@
+(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
+
+header {* A simple counterexample generator performing random testing *}
+
+theory Quickcheck_Random
+imports Random Code_Evaluation Enum
+begin
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
+
+subsection {* Catching Match exceptions *}
+
+axiomatization catch_match :: "'a => 'a => 'a"
+
+code_const catch_match 
+  (Quickcheck "((_) handle Match => _)")
+
+subsection {* The @{text random} class *}
+
+class random = typerep +
+  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+
+subsection {* Fundamental and numeric types*}
+
+instantiation bool :: random
+begin
+
+definition
+  "random i = Random.range 2 \<circ>\<rightarrow>
+    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
+
+instance ..
+
+end
+
+instantiation itself :: (typerep) random
+begin
+
+definition
+  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
+
+instance ..
+
+end
+
+instantiation char :: random
+begin
+
+definition
+  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
+
+instance ..
+
+end
+
+instantiation String.literal :: random
+begin
+
+definition 
+  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
+
+instance ..
+
+end
+
+instantiation nat :: random
+begin
+
+definition random_nat :: "code_numeral \<Rightarrow> Random.seed
+  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
+where
+  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
+     let n = Code_Numeral.nat_of k
+     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
+
+instance ..
+
+end
+
+instantiation int :: random
+begin
+
+definition
+  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
+     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
+     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
+
+instance ..
+
+end
+
+
+subsection {* Complex generators *}
+
+text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
+
+axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
+  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
+  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
+  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+where
+  "random_fun_lift f =
+    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
+
+instantiation "fun" :: ("{equal, term_of}", random) random
+begin
+
+definition
+  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+  where "random i = random_fun_lift (random i)"
+
+instance ..
+
+end
+
+text {* Towards type copies and datatypes *}
+
+definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
+  where "collapse f = (f \<circ>\<rightarrow> id)"
+
+definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+  where "beyond k l = (if l > k then l else 0)"
+
+lemma beyond_zero: "beyond k 0 = 0"
+  by (simp add: beyond_def)
+
+
+definition (in term_syntax) [code_unfold]:
+  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
+
+definition (in term_syntax) [code_unfold]:
+  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+
+instantiation set :: (random) random
+begin
+
+primrec random_aux_set
+where
+  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
+| "random_aux_set (Code_Numeral.Suc i) j =
+    collapse (Random.select_weight
+      [(1, Pair valterm_emptyset),
+       (Code_Numeral.Suc i,
+        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
+
+lemma [code]:
+  "random_aux_set i j =
+    collapse (Random.select_weight [(1, Pair valterm_emptyset),
+      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
+proof (induct i rule: code_numeral.induct)
+  case zero
+  show ?case by (subst select_weight_drop_zero [symmetric])
+    (simp add: random_aux_set.simps [simplified])
+next
+  case (Suc i)
+  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
+qed
+
+definition "random_set i = random_aux_set i i"
+
+instance ..
+
+end
+
+lemma random_aux_rec:
+  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
+  assumes "random_aux 0 = rhs 0"
+    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
+  shows "random_aux k = rhs k"
+  using assms by (rule code_numeral.induct)
+
+subsection {* Deriving random generators for datatypes *}
+
+ML_file "Tools/Quickcheck/quickcheck_common.ML" 
+ML_file "Tools/Quickcheck/random_generators.ML"
+setup Random_Generators.setup
+
+
+subsection {* Code setup *}
+
+code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
+  -- {* With enough criminal energy this can be abused to derive @{prop False};
+  for this reason we use a distinguished target @{text Quickcheck}
+  not spoiling the regular trusted code generation *}
+
+code_reserved Quickcheck Random_Generators
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+    
+hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
+
+hide_fact (open) collapse_def beyond_def random_fun_lift_def
+
+end
+
diff -r f90874d3a246 -r df86080de4cb src/HOL/Random_Pred.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Random_Pred.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -0,0 +1,76 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* The Random-Predicate Monad *}
+
+theory Random_Pred
+imports Quickcheck_Random
+begin
+
+fun iter' :: "'a itself \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
+where
+  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
+     let ((x, _), seed') = Quickcheck_Random.random sz seed
+   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
+
+definition iter :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
+where
+  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
+
+lemma [code]:
+  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
+     let ((x, _), seed') = Quickcheck_Random.random sz seed
+   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
+   unfolding iter_def iter'.simps [of _ nrandom] ..
+
+type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
+
+definition empty :: "'a random_pred"
+  where "empty = Pair bot"
+
+definition single :: "'a => 'a random_pred"
+  where "single x = Pair (Predicate.single x)"
+
+definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred"
+  where
+    "bind R f = (\<lambda>s. let
+       (P, s') = R s;
+       (s1, s2) = Random.split_seed s'
+     in (Predicate.bind P (%a. fst (f a s1)), s2))"
+
+definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred"
+where
+  "union R1 R2 = (\<lambda>s. let
+     (P1, s') = R1 s; (P2, s'') = R2 s'
+   in (sup_class.sup P1 P2, s''))"
+
+definition if_randompred :: "bool \<Rightarrow> unit random_pred"
+where
+  "if_randompred b = (if b then single () else empty)"
+
+definition iterate_upto :: "(code_numeral \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
+where
+  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
+
+definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
+where
+  "not_randompred P = (\<lambda>s. let
+     (P', s') = P s
+   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
+
+definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred"
+  where "Random g = scomp g (Pair o (Predicate.single o fst))"
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred"
+  where "map f P = bind P (single o f)"
+
+hide_const (open) iter' iter empty single bind union if_randompred
+  iterate_upto not_randompred Random map
+
+hide_fact iter'.simps
+  
+hide_fact (open) iter_def empty_def single_def bind_def union_def
+  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
+
+end
+
diff -r f90874d3a246 -r df86080de4cb src/HOL/Random_Sequence.thy
--- a/src/HOL/Random_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Random_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -1,32 +1,34 @@
 
 (* Author: Lukas Bulwahn, TU Muenchen *)
 
+header {* Various kind of sequences inside the random monad *}
+
 theory Random_Sequence
-imports Quickcheck
+imports Random_Pred
 begin
 
-type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
+type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)"
 
 definition empty :: "'a random_dseq"
 where
-  "empty = (%nrandom size. Pair (DSequence.empty))"
+  "empty = (%nrandom size. Pair (Limited_Sequence.empty))"
 
 definition single :: "'a => 'a random_dseq"
 where
-  "single x = (%nrandom size. Pair (DSequence.single x))"
+  "single x = (%nrandom size. Pair (Limited_Sequence.single x))"
 
 definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq"
 where
   "bind R f = (\<lambda>nrandom size s. let
      (P, s') = R nrandom size s;
      (s1, s2) = Random.split_seed s'
-  in (DSequence.bind P (%a. fst (f a nrandom size s1)), s2))"
+  in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))"
 
 definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq"
 where
   "union R1 R2 = (\<lambda>nrandom size s. let
      (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s'
-  in (DSequence.union S1 S2, s''))"
+  in (Limited_Sequence.union S1 S2, s''))"
 
 definition if_random_dseq :: "bool => unit random_dseq"
 where
@@ -36,26 +38,120 @@
 where
   "not_random_dseq R = (\<lambda>nrandom size s. let
      (S, s') = R nrandom size s
-   in (DSequence.not_seq S, s'))"
-
-fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
-where
-  "Random g nrandom = (%size. if nrandom <= 0 then (Pair DSequence.empty) else
-     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (DSequence.union (DSequence.single (fst r)) rs)))))"
+   in (Limited_Sequence.not_seq S, s'))"
 
 definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq"
 where
   "map f P = bind P (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
-*)
+fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
+where
+  "Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else
+     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))"
+
+
+type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq"
+
+definition pos_empty :: "'a pos_random_dseq"
+where
+  "pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)"
+
+definition pos_single :: "'a => 'a pos_random_dseq"
+where
+  "pos_single x = (%nrandom size seed. Limited_Sequence.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. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
+where
+  "pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_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. Limited_Sequence.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_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
+where
+  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)"
+
+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)"
+
+fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
+  \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> '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 pos_Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
+  \<Rightarrow> 'a pos_random_dseq"
+where
+  "pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
+
+
+type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq"
 
-hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
+definition neg_empty :: "'a neg_random_dseq"
+where
+  "neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)"
+
+definition neg_single :: "'a => 'a neg_random_dseq"
+where
+  "neg_single x = (%nrandom size seed. Limited_Sequence.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. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
+where
+  "neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_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. Limited_Sequence.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_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
+where
+  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)"
 
-hide_type DSequence.dseq random_dseq
-hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
+definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
+where
+  "neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size 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)"
+
+definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
+where
+  "pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))"
+
 
-end
\ No newline at end of file
+hide_const (open)
+  empty single bind union if_random_dseq not_random_dseq map Random
+  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto
+  pos_not_random_dseq pos_map iter pos_Random
+  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto
+  neg_not_random_dseq neg_map
+
+hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def
+  map_def Random.simps
+  pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def
+  pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def
+  neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def
+  neg_iterate_upto_def neg_not_random_dseq_def neg_map_def
+
+end
+
diff -r f90874d3a246 -r df86080de4cb src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Rat.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -1030,7 +1030,7 @@
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
+  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
      let j = Code_Numeral.int_of (denom + 1)
      in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/RealDef.thy	Thu Feb 14 15:27:10 2013 +0100
@@ -1641,7 +1641,7 @@
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
 
 instance ..
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -956,7 +956,7 @@
     val tss = run (#timeout system_config, #prolog_system system_config)
       p (translate_const constant_table' name, args') output_names soln
     val _ = tracing "Restoring terms..."
-    val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
+    val empty = Const(@{const_name bot}, fastype_of t_compr)
     fun mk_insert x S =
       Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
     fun mk_set_compr in_insert [] xs =
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -225,41 +225,41 @@
   @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
 
 fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
-  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
+  [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
   | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
 
-fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
+fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
 
 fun mk_single t =
   let               
     val T = fastype_of t
   in
-    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
+    Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
   end;
 
 fun mk_bind (x, f) =
   let
     val T as (Type ("fun", [_, U])) = fastype_of f
   in
-    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Random_Pred.bind}, fastype_of x --> T --> U) $ x $ f
   end
 
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union}
+val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union}
 
-fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
+fun mk_if cond = Const (@{const_name Random_Pred.if_randompred},
   HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name Quickcheck.iterate_upto},
+  list_comb (Const (@{const_name Random_Pred.iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
     [f, from, to])
 
 fun mk_not t =
   let
     val T = mk_randompredT HOLogic.unitT
-  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
+  in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
   (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
@@ -279,29 +279,29 @@
   Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, mk_dseqT T);
 
 fun mk_single t =
   let val T = fastype_of t
-  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.single}, T --> mk_dseqT T) $ t end;
 
 fun mk_bind (x, f) =
   let val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Limited_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name DSequence.union};
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union};
 
-fun mk_if cond = Const (@{const_name DSequence.if_seq},
+fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq},
   HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
 
 fun mk_not t = let val T = mk_dseqT HOLogic.unitT
-  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
+  in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
   (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
 
 val compfuns = Predicate_Compile_Aux.CompilationFuns
@@ -321,30 +321,30 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
   | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   end;
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
 
-fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
+fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
   HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -355,9 +355,9 @@
     val nT =
       @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
         [Type (@{type_name Option.option}, [@{typ unit}])])
-  in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end
+  in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map},
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
   (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
@@ -382,30 +382,30 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
   | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
 
 fun mk_single t =
   let
     val T = fastype_of t
-  in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
+  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
 
 fun mk_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   end;
   
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
 
-fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
+fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
   HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -416,9 +416,9 @@
     val pT =
       @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
         [@{typ unit}])
-  in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end
+  in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
 
-fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map},
+fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
   (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
@@ -445,34 +445,34 @@
     Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+fun mk_empty T = Const (@{const_name 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;
+  in Const(@{const_name 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
+    Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
 
-fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
+fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq},
   HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
+  list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
         ---> mk_pos_random_dseqT T),
     [f, from, to])
@@ -484,9 +484,9 @@
       @{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
+  in Const (@{const_name 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},
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
   (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
@@ -514,34 +514,34 @@
         [Type (@{type_name Option.option}, [T])])])])])])) = T
   | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
 
-fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+fun mk_empty T = Const (@{const_name 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;
+  in Const(@{const_name 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
+    Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
 fun mk_decr_bind (x, f) =
   let
     val T as Type ("fun", [_, U]) = fastype_of f
   in
-    Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
+    Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   end;
 
-val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
 
-fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
+fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
   HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
 
 fun mk_iterate_upto T (f, from, to) =
-  list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
+  list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
       [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
         ---> mk_neg_random_dseqT T),
     [f, from, to])
@@ -551,9 +551,9 @@
     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
+  in Const (@{const_name 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},
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
   (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
 
 val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -26,8 +26,8 @@
   val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
   val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
     Proof.context -> Proof.context
-  val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
-  val put_dseq_random_result : (unit -> int -> int -> seed -> term DSequence.dseq * seed) ->
+  val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
+  val put_dseq_random_result : (unit -> int -> int -> seed -> term Limited_Sequence.dseq * seed) ->
     Proof.context -> Proof.context
   val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
@@ -325,20 +325,20 @@
   function_name_prefix = "random_",
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Quickcheck.iter},
+  list_comb (Const(@{const_name Random_Pred.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
     Predicate_Comp_Funs.mk_monadT 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"}]
+      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}]
     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"})]
+        Free (seed, @{typ Random.seed})]
     end),
   wrap_compilation = K (K (K (K (K I))))
     : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
@@ -351,21 +351,21 @@
   function_name_prefix = "depth_limited_random_",
   compfuns = Predicate_Comp_Funs.compfuns,
   mk_random = (fn T => fn additional_arguments =>
-  list_comb (Const(@{const_name Quickcheck.iter},
+  list_comb (Const(@{const_name Random_Pred.iter},
   [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
     Predicate_Comp_Funs.mk_monadT 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"}]
+        @{typ Random.seed}]
     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"})]
+        Free (size, @{typ code_numeral}), Free (seed, @{typ Random.seed})]
     end),
   wrap_compilation =
   fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
@@ -423,11 +423,11 @@
   compfuns = Random_Sequence_CompFuns.compfuns,
   mk_random = (fn T => fn _ =>
   let
-    val random = Const ("Quickcheck.random_class.random",
+    val random = Const (@{const_name Quickcheck_Random.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} -->
+    Const (@{const_name 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),
@@ -460,11 +460,11 @@
   compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
   mk_random = (fn T => fn _ =>
   let
-    val random = Const ("Quickcheck.random_class.random",
+    val random = Const (@{const_name Quickcheck_Random.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} -->
+    Const (@{const_name Random_Sequence.pos_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),
@@ -1647,7 +1647,7 @@
 
 structure Dseq_Result = Proof_Data
 (
-  type T = unit -> term DSequence.dseq
+  type T = unit -> term Limited_Sequence.dseq
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Result"
 );
@@ -1655,7 +1655,7 @@
 
 structure Dseq_Random_Result = Proof_Data
 (
-  type T = unit -> int -> int -> seed -> term DSequence.dseq * seed
+  type T = unit -> int -> int -> seed -> term Limited_Sequence.dseq * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Random_Result"
 );
@@ -1843,24 +1843,24 @@
           let
             val [nrandom, size, depth] = arguments
           in
-            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (DSequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
-                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
+                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
               depth true)) ())
           end
       | DSeq =>
-          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (DSequence.yieldn k
+          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              thy NONE DSequence.map t' []) (the_single arguments) true)) ())
+              thy NONE Limited_Sequence.map t' []) (the_single arguments) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = (the_single arguments)
           in
             rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
-              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
+              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
               t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
@@ -1875,7 +1875,7 @@
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
-                    |> Lazy_Sequence.mapa (apfst proc))
+                    |> Lazy_Sequence.map (apfst proc))
                     t' [] nrandom size seed depth))) ()))
             else rpair NONE
               (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
@@ -1883,7 +1883,7 @@
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   thy NONE 
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
-                    |> Lazy_Sequence.mapa proc)
+                    |> Lazy_Sequence.map proc)
                     t' [] nrandom size seed depth))) ())
           end
       | _ =>
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -12,7 +12,7 @@
     (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
       Proof.context -> Proof.context;
   val put_dseq_result :
-    (unit -> int -> int -> seed -> term list DSequence.dseq * seed) ->
+    (unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed) ->
       Proof.context -> Proof.context;
   val put_lseq_result :
     (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
@@ -49,7 +49,7 @@
 
 structure Dseq_Result = Proof_Data
 (
-  type T = unit -> int -> int -> seed -> term list DSequence.dseq * seed
+  type T = unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Result"
 );
@@ -297,11 +297,11 @@
             val compiled_term =
               Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
                 thy4 (SOME target)
-                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
+                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
                 qc_term []
           in
             (fn size => fn nrandom => fn depth =>
-              Option.map fst (DSequence.yield
+              Option.map fst (Limited_Sequence.yield
                 (compiled_term nrandom size |> Random_Engine.run) depth true))
           end
       | New_Pos_Random_DSeq =>
@@ -311,7 +311,7 @@
                 (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
                 thy4 (SOME target)
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
-                  g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
+                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
                   qc_term []
           in
             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
@@ -326,7 +326,7 @@
               Code_Runtime.dynamic_value_strict
                 (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
                 thy4 (SOME target)
-                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.mapa o map) proc)
+                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
                 qc_term []
           in
             fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -243,7 +243,7 @@
     val (T1, T2) = (fastype_of x, fastype_of (e genuine))
     val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2)
   in
-    Const (@{const_name "Quickcheck.catch_match"}, T2 --> T2 --> T2) $ 
+    Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $ 
       (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $
       (if_t $ genuine_only $ none $ safe false)
   end
@@ -337,9 +337,9 @@
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 
   in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
 
-fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
+fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
 
-fun mk_safe_term t = @{term "Quickcheck.catch_match :: term => term => term"}
+fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"}
       $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
 
 fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -309,7 +309,7 @@
     val T = fastype_of then_t
     val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
   in
-    Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $ 
+    Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ 
       (if_t $ cond $ then_t $ else_t genuine) $
       (if_t $ genuine_only $ none $ else_t false)
   end
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -222,7 +222,7 @@
             tc @{typ Random.seed} (SOME T, @{typ Random.seed});
         val tk = if is_rec
           then if k = 0 then size
-            else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
+            else @{term "Quickcheck_Random.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
              $ HOLogic.mk_number @{typ code_numeral} k $ size
           else @{term "1::code_numeral"}
       in (is_rec, HOLogic.mk_prod (tk, t)) end;
@@ -233,7 +233,7 @@
       |> (map o apfst) Type
       |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs));
     fun mk_select (rT, xs) =
-      mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT]
+      mk_const @{const_name Quickcheck_Random.collapse} [@{typ Random.seed}, termifyT rT]
       $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
         $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
           $ seed;
@@ -315,7 +315,7 @@
       mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
-      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   in
     lambda genuine_only
       (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
@@ -333,7 +333,7 @@
     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
     val (assms, concl) = Quickcheck_Common.strip_imp prop'
-    val return = HOLogic.pair_const resultT @{typ "Random.seed"};
+    val return = HOLogic.pair_const resultT @{typ Random.seed};
     fun mk_assms_report i =
       HOLogic.mk_prod (@{term "None :: (bool * term list) option"},
         HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
@@ -361,7 +361,7 @@
       mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
     fun mk_bindclause (_, _, i, T) = mk_scomp_split T
-      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
+      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   in
     lambda genuine_only
       (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -193,9 +193,9 @@
 
 (* FIXME: Ad hoc list *)
 val technical_prefixes =
-  ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
-   "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
-   "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
+  ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
+   "Limited_Sequence", "Meson", "Metis", "Nitpick",
+   "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
    "Random_Sequence", "Sledgehammer", "SMT"]
   |> map (suffix Long_Name.separator)
 
diff -r f90874d3a246 -r df86080de4cb src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Feb 14 17:58:28 2013 +0100
+++ b/src/HOL/Tools/hologic.ML	Thu Feb 14 15:27:10 2013 +0100
@@ -686,7 +686,7 @@
 
 val random_seedT = mk_prodT (code_numeralT, code_numeralT);
 
-fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
+fun mk_random T t = Const ("Quickcheck_Random.random_class.random", code_numeralT
   --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
 
 end;