reform of predicate compiler / quickcheck theories:
authorhaftmann
Thu Feb 14 15:27:10 2013 +0100 (2013-02-14)
changeset 51126df86080de4cb
parent 51125 f90874d3a246
child 51127 5cf1604b9ef5
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
src/HOL/Code_Evaluation.thy
src/HOL/DSequence.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/DAList.thy
src/HOL/Library/Multiset.thy
src/HOL/Limited_Sequence.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile.thy
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Random_Pred.thy
src/HOL/Random_Sequence.thy
src/HOL/Rat.thy
src/HOL/RealDef.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Feb 14 17:58:28 2013 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Feb 14 15:27:10 2013 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Term evaluation using the generic code generator *}
     1.5  
     1.6  theory Code_Evaluation
     1.7 -imports Typerep New_DSequence
     1.8 +imports Typerep Limited_Sequence
     1.9  begin
    1.10  
    1.11  subsection {* Term representation *}
     2.1 --- a/src/HOL/DSequence.thy	Thu Feb 14 17:58:28 2013 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,113 +0,0 @@
     2.4 -
     2.5 -(* Author: Lukas Bulwahn, TU Muenchen *)
     2.6 -
     2.7 -header {* Depth-Limited Sequences with failure element *}
     2.8 -
     2.9 -theory DSequence
    2.10 -imports Lazy_Sequence
    2.11 -begin
    2.12 -
    2.13 -type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    2.14 -
    2.15 -definition empty :: "'a dseq"
    2.16 -where
    2.17 -  "empty = (%i pol. Some Lazy_Sequence.empty)"
    2.18 -
    2.19 -definition single :: "'a => 'a dseq"
    2.20 -where
    2.21 -  "single x = (%i pol. Some (Lazy_Sequence.single x))"
    2.22 -
    2.23 -fun eval :: "'a dseq => code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
    2.24 -where
    2.25 -  "eval f i pol = f i pol"
    2.26 -
    2.27 -definition yield :: "'a dseq => code_numeral => bool => ('a * 'a dseq) option" 
    2.28 -where
    2.29 -  "yield dseq i pol = (case eval dseq i pol of
    2.30 -    None => None
    2.31 -  | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
    2.32 -
    2.33 -definition yieldn :: "code_numeral \<Rightarrow> 'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a list \<times> 'a dseq"
    2.34 -where
    2.35 -  "yieldn n dseq i pol = (case dseq i pol of
    2.36 -    None \<Rightarrow> ([], \<lambda>i pol. None)
    2.37 -  | Some s \<Rightarrow> let (xs, s') = Lazy_Sequence.yieldn n s in (xs, \<lambda>i pol. Some s'))"
    2.38 -
    2.39 -fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
    2.40 -where
    2.41 -  "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    2.42 -    None => Some Lazy_Sequence.empty
    2.43 -  | Some (x, xq') => (case eval (f x) i pol of
    2.44 -      None => None
    2.45 -    | Some yq => (case map_seq f xq' i pol of
    2.46 -        None => None
    2.47 -      | Some zq => Some (Lazy_Sequence.append yq zq))))"
    2.48 -
    2.49 -definition bind :: "'a dseq => ('a => 'b dseq) => 'b dseq"
    2.50 -where
    2.51 -  "bind x f = (%i pol. 
    2.52 -     if i = 0 then
    2.53 -       (if pol then Some Lazy_Sequence.empty else None)
    2.54 -     else
    2.55 -       (case x (i - 1) pol of
    2.56 -         None => None
    2.57 -       | Some xq => map_seq f xq i pol))"
    2.58 -
    2.59 -definition union :: "'a dseq => 'a dseq => 'a dseq"
    2.60 -where
    2.61 -  "union x y = (%i pol. case (x i pol, y i pol) of
    2.62 -      (Some xq, Some yq) => Some (Lazy_Sequence.append xq yq)
    2.63 -    | _ => None)"
    2.64 -
    2.65 -definition if_seq :: "bool => unit dseq"
    2.66 -where
    2.67 -  "if_seq b = (if b then single () else empty)"
    2.68 -
    2.69 -definition not_seq :: "unit dseq => unit dseq"
    2.70 -where
    2.71 -  "not_seq x = (%i pol. case x i (\<not>pol) of
    2.72 -    None => Some Lazy_Sequence.empty
    2.73 -  | Some xq => (case Lazy_Sequence.yield xq of
    2.74 -      None => Some (Lazy_Sequence.single ())
    2.75 -    | Some _ => Some (Lazy_Sequence.empty)))"
    2.76 -
    2.77 -definition map :: "('a => 'b) => 'a dseq => 'b dseq"
    2.78 -where
    2.79 -  "map f g = (%i pol. case g i pol of
    2.80 -     None => None
    2.81 -   | Some xq => Some (Lazy_Sequence.map f xq))"
    2.82 -
    2.83 -ML {*
    2.84 -signature DSEQUENCE =
    2.85 -sig
    2.86 -  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    2.87 -  val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
    2.88 -  val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
    2.89 -  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
    2.90 -end;
    2.91 -
    2.92 -structure DSequence : DSEQUENCE =
    2.93 -struct
    2.94 -
    2.95 -type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    2.96 -
    2.97 -val yield = @{code yield}
    2.98 -val yieldn = @{code yieldn}
    2.99 -val map = @{code map}
   2.100 -
   2.101 -end;
   2.102 -*}
   2.103 -
   2.104 -code_reserved Eval DSequence
   2.105 -(*
   2.106 -hide_type Sequence.seq
   2.107 -
   2.108 -hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single
   2.109 -  Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq
   2.110 -*)
   2.111 -hide_const (open) empty single eval map_seq bind union if_seq not_seq map
   2.112 -hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def
   2.113 -  if_seq_def not_seq_def map_def
   2.114 -
   2.115 -end
   2.116 -
     3.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
     3.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
     3.3 @@ -7,158 +7,230 @@
     3.4  imports Predicate
     3.5  begin
     3.6  
     3.7 -datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
     3.8 +subsection {* Type of lazy sequences *}
     3.9  
    3.10 -definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence"
    3.11 -where
    3.12 -  "Lazy_Sequence f = (case f () of None => Empty | Some (x, xq) => Insert x xq)"
    3.13 +datatype 'a lazy_sequence = lazy_sequence_of_list "'a list"
    3.14  
    3.15 -code_datatype Lazy_Sequence 
    3.16 -
    3.17 -primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option"
    3.18 +primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
    3.19  where
    3.20 -  "yield Empty = None"
    3.21 -| "yield (Insert x xq) = Some (x, xq)"
    3.22 +  "list_of_lazy_sequence (lazy_sequence_of_list xs) = xs"
    3.23 +
    3.24 +lemma lazy_sequence_of_list_of_lazy_sequence [simp]:
    3.25 +  "lazy_sequence_of_list (list_of_lazy_sequence xq) = xq"
    3.26 +  by (cases xq) simp_all
    3.27 +
    3.28 +lemma lazy_sequence_eqI:
    3.29 +  "list_of_lazy_sequence xq = list_of_lazy_sequence yq \<Longrightarrow> xq = yq"
    3.30 +  by (cases xq, cases yq) simp
    3.31 +
    3.32 +lemma lazy_sequence_eq_iff:
    3.33 +  "xq = yq \<longleftrightarrow> list_of_lazy_sequence xq = list_of_lazy_sequence yq"
    3.34 +  by (auto intro: lazy_sequence_eqI)
    3.35  
    3.36 -lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
    3.37 -by (cases xq) auto
    3.38 +lemma lazy_sequence_size_eq:
    3.39 +  "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
    3.40 +  by (cases xq) simp
    3.41 +
    3.42 +lemma size_lazy_sequence_eq [code]:
    3.43 +  "size (xq :: 'a lazy_sequence) = 0"
    3.44 +  by (cases xq) simp
    3.45 +
    3.46 +lemma lazy_sequence_case [simp]:
    3.47 +  "lazy_sequence_case f xq = f (list_of_lazy_sequence xq)"
    3.48 +  by (cases xq) auto
    3.49 +
    3.50 +lemma lazy_sequence_rec [simp]:
    3.51 +  "lazy_sequence_rec f xq = f (list_of_lazy_sequence xq)"
    3.52 +  by (cases xq) auto
    3.53  
    3.54 -lemma yield_Seq [code]:
    3.55 -  "yield (Lazy_Sequence f) = f ()"
    3.56 -unfolding Lazy_Sequence_def by (cases "f ()") auto
    3.57 +definition Lazy_Sequence :: "(unit \<Rightarrow> ('a \<times> 'a lazy_sequence) option) \<Rightarrow> 'a lazy_sequence"
    3.58 +where
    3.59 +  "Lazy_Sequence f = lazy_sequence_of_list (case f () of
    3.60 +    None \<Rightarrow> []
    3.61 +  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
    3.62 +
    3.63 +code_datatype Lazy_Sequence
    3.64 +
    3.65 +declare list_of_lazy_sequence.simps [code del]
    3.66 +declare lazy_sequence.cases [code del]
    3.67 +declare lazy_sequence.recs [code del]
    3.68  
    3.69 -lemma Seq_yield:
    3.70 -  "Lazy_Sequence (%u. yield f) = f"
    3.71 -unfolding Lazy_Sequence_def by (cases f) auto
    3.72 +lemma list_of_Lazy_Sequence [simp]:
    3.73 +  "list_of_lazy_sequence (Lazy_Sequence f) = (case f () of
    3.74 +    None \<Rightarrow> []
    3.75 +  | Some (x, xq) \<Rightarrow> x # list_of_lazy_sequence xq)"
    3.76 +  by (simp add: Lazy_Sequence_def)
    3.77 +
    3.78 +definition yield :: "'a lazy_sequence \<Rightarrow> ('a \<times> 'a lazy_sequence) option"
    3.79 +where
    3.80 +  "yield xq = (case list_of_lazy_sequence xq of
    3.81 +    [] \<Rightarrow> None
    3.82 +  | x # xs \<Rightarrow> Some (x, lazy_sequence_of_list xs))" 
    3.83 +
    3.84 +lemma yield_Seq [simp, code]:
    3.85 +  "yield (Lazy_Sequence f) = f ()"
    3.86 +  by (cases "f ()") (simp_all add: yield_def split_def)
    3.87 +
    3.88 +lemma case_yield_eq [simp]: "option_case g h (yield xq) =
    3.89 +  list_case g (\<lambda>x. curry h x \<circ> lazy_sequence_of_list) (list_of_lazy_sequence xq)"
    3.90 +  by (cases "list_of_lazy_sequence xq") (simp_all add: yield_def)
    3.91  
    3.92  lemma lazy_sequence_size_code [code]:
    3.93 -  "lazy_sequence_size s xq = (case yield xq of None => 0 | Some (x, xq') => s x + lazy_sequence_size s xq' + 1)"
    3.94 -by (cases xq) auto
    3.95 +  "lazy_sequence_size s xq = (case yield xq of
    3.96 +    None \<Rightarrow> 1
    3.97 +  | Some (x, xq') \<Rightarrow> Suc (s x + lazy_sequence_size s xq'))"
    3.98 +  by (cases "list_of_lazy_sequence xq") (simp_all add: lazy_sequence_size_eq)
    3.99  
   3.100 -lemma size_code [code]:
   3.101 -  "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
   3.102 -by (cases xq) auto
   3.103 -
   3.104 -lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
   3.105 -  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
   3.106 -apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
   3.107 -apply (cases yq) apply (auto simp add: equal_eq) done
   3.108 +lemma equal_lazy_sequence_code [code]:
   3.109 +  "HOL.equal xq yq = (case (yield xq, yield yq) of
   3.110 +    (None, None) \<Rightarrow> True
   3.111 +  | (Some (x, xq'), Some (y, yq')) \<Rightarrow> HOL.equal x y \<and> HOL.equal xq yq
   3.112 +  | _ \<Rightarrow> False)"
   3.113 +  by (simp_all add: lazy_sequence_eq_iff equal_eq split: list.splits)
   3.114  
   3.115  lemma [code nbe]:
   3.116    "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
   3.117    by (fact equal_refl)
   3.118  
   3.119 -lemma seq_case [code]:
   3.120 -  "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
   3.121 -by (cases xq) auto
   3.122 -
   3.123 -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'))"
   3.124 -by (cases xq) auto
   3.125 -
   3.126  definition empty :: "'a lazy_sequence"
   3.127  where
   3.128 -  [code]: "empty = Lazy_Sequence (%u. None)"
   3.129 +  "empty = lazy_sequence_of_list []"
   3.130  
   3.131 -definition single :: "'a => 'a lazy_sequence"
   3.132 -where
   3.133 -  [code]: "single x = Lazy_Sequence (%u. Some (x, empty))"
   3.134 +lemma list_of_lazy_sequence_empty [simp]:
   3.135 +  "list_of_lazy_sequence empty = []"
   3.136 +  by (simp add: empty_def)
   3.137  
   3.138 -primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence"
   3.139 -where
   3.140 -  "append Empty yq = yq"
   3.141 -| "append (Insert x xq) yq = Insert x (append xq yq)"
   3.142 +lemma empty_code [code]:
   3.143 +  "empty = Lazy_Sequence (\<lambda>_. None)"
   3.144 +  by (simp add: lazy_sequence_eq_iff)
   3.145  
   3.146 -lemma [code]:
   3.147 -  "append xq yq = Lazy_Sequence (%u. case yield xq of
   3.148 -     None => yield yq
   3.149 -  | Some (x, xq') => Some (x, append xq' yq))"
   3.150 -unfolding Lazy_Sequence_def
   3.151 -apply (cases "xq")
   3.152 -apply auto
   3.153 -apply (cases "yq")
   3.154 -apply auto
   3.155 -done
   3.156 +definition single :: "'a \<Rightarrow> 'a lazy_sequence"
   3.157 +where
   3.158 +  "single x = lazy_sequence_of_list [x]"
   3.159  
   3.160 -primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence"
   3.161 +lemma list_of_lazy_sequence_single [simp]:
   3.162 +  "list_of_lazy_sequence (single x) = [x]"
   3.163 +  by (simp add: single_def)
   3.164 +
   3.165 +lemma single_code [code]:
   3.166 +  "single x = Lazy_Sequence (\<lambda>_. Some (x, empty))"
   3.167 +  by (simp add: lazy_sequence_eq_iff)
   3.168 +
   3.169 +definition append :: "'a lazy_sequence \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a lazy_sequence"
   3.170  where
   3.171 -  "flat Empty = Empty"
   3.172 -| "flat (Insert xq xqq) = append xq (flat xqq)"
   3.173 - 
   3.174 -lemma [code]:
   3.175 -  "flat xqq = Lazy_Sequence (%u. case yield xqq of
   3.176 -    None => None
   3.177 -  | Some (xq, xqq') => yield (append xq (flat xqq')))"
   3.178 -apply (cases "xqq")
   3.179 -apply (auto simp add: Seq_yield)
   3.180 -unfolding Lazy_Sequence_def
   3.181 -by auto
   3.182 +  "append xq yq = lazy_sequence_of_list (list_of_lazy_sequence xq @ list_of_lazy_sequence yq)"
   3.183 +
   3.184 +lemma list_of_lazy_sequence_append [simp]:
   3.185 +  "list_of_lazy_sequence (append xq yq) = list_of_lazy_sequence xq @ list_of_lazy_sequence yq"
   3.186 +  by (simp add: append_def)
   3.187  
   3.188 -primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence"
   3.189 +lemma append_code [code]:
   3.190 +  "append xq yq = Lazy_Sequence (\<lambda>_. case yield xq of
   3.191 +    None \<Rightarrow> yield yq
   3.192 +  | Some (x, xq') \<Rightarrow> Some (x, append xq' yq))"
   3.193 +  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
   3.194 +
   3.195 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b lazy_sequence"
   3.196  where
   3.197 -  "map f Empty = Empty"
   3.198 -| "map f (Insert x xq) = Insert (f x) (map f xq)"
   3.199 +  "map f xq = lazy_sequence_of_list (List.map f (list_of_lazy_sequence xq))"
   3.200 +
   3.201 +lemma list_of_lazy_sequence_map [simp]:
   3.202 +  "list_of_lazy_sequence (map f xq) = List.map f (list_of_lazy_sequence xq)"
   3.203 +  by (simp add: map_def)
   3.204 +
   3.205 +lemma map_code [code]:
   3.206 +  "map f xq =
   3.207 +    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (f x, map f xq')) (yield xq))"
   3.208 +  by (simp_all add: lazy_sequence_eq_iff split: list.splits)
   3.209 +
   3.210 +definition flat :: "'a lazy_sequence lazy_sequence \<Rightarrow> 'a lazy_sequence"
   3.211 +where
   3.212 +  "flat xqq = lazy_sequence_of_list (concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq)))"
   3.213  
   3.214 -lemma [code]:
   3.215 -  "map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))"
   3.216 -apply (cases xq)
   3.217 -apply (auto simp add: Seq_yield)
   3.218 -unfolding Lazy_Sequence_def
   3.219 -apply auto
   3.220 -done
   3.221 +lemma list_of_lazy_sequence_flat [simp]:
   3.222 +  "list_of_lazy_sequence (flat xqq) = concat (List.map list_of_lazy_sequence (list_of_lazy_sequence xqq))"
   3.223 +  by (simp add: flat_def)
   3.224  
   3.225 -definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence"
   3.226 +lemma flat_code [code]:
   3.227 +  "flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
   3.228 +    None \<Rightarrow> None
   3.229 +  | Some (xq, xqq') \<Rightarrow> yield (append xq (flat xqq')))"
   3.230 +  by (simp add: lazy_sequence_eq_iff split: list.splits)
   3.231 +
   3.232 +definition bind :: "'a lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b lazy_sequence) \<Rightarrow> 'b lazy_sequence"
   3.233  where
   3.234 -  [code]: "bind xq f = flat (map f xq)"
   3.235 +  "bind xq f = flat (map f xq)"
   3.236  
   3.237 -definition if_seq :: "bool => unit lazy_sequence"
   3.238 +definition if_seq :: "bool \<Rightarrow> unit lazy_sequence"
   3.239  where
   3.240    "if_seq b = (if b then single () else empty)"
   3.241  
   3.242 -function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
   3.243 +definition those :: "'a option lazy_sequence \<Rightarrow> 'a lazy_sequence option"
   3.244  where
   3.245 -  "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))"
   3.246 -by pat_completeness auto
   3.247 +  "those xq = Option.map lazy_sequence_of_list (List.those (list_of_lazy_sequence xq))"
   3.248 +  
   3.249 +function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a lazy_sequence"
   3.250 +where
   3.251 +  "iterate_upto f n m =
   3.252 +    Lazy_Sequence (\<lambda>_. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
   3.253 +  by pat_completeness auto
   3.254  
   3.255  termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
   3.256  
   3.257 -definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
   3.258 +definition not_seq :: "unit lazy_sequence \<Rightarrow> unit lazy_sequence"
   3.259  where
   3.260 -  "not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
   3.261 -
   3.262 -subsection {* Code setup *}
   3.263 +  "not_seq xq = (case yield xq of
   3.264 +    None \<Rightarrow> single ()
   3.265 +  | Some ((), xq) \<Rightarrow> empty)"
   3.266  
   3.267 -fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
   3.268 -  "anamorph f k x = (if k = 0 then ([], x)
   3.269 -    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
   3.270 -      let (vs, z) = anamorph f (k - 1) y
   3.271 -    in (v # vs, z))"
   3.272 -
   3.273 -definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
   3.274 -  "yieldn = anamorph yield"
   3.275 +  
   3.276 +subsection {* Code setup *}
   3.277  
   3.278  code_reflect Lazy_Sequence
   3.279    datatypes lazy_sequence = Lazy_Sequence
   3.280 -  functions map yield yieldn
   3.281 +
   3.282 +ML {*
   3.283 +signature LAZY_SEQUENCE =
   3.284 +sig
   3.285 +  datatype 'a lazy_sequence = Lazy_Sequence of (unit -> ('a * 'a Lazy_Sequence.lazy_sequence) option)
   3.286 +  val map: ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
   3.287 +  val yield: 'a lazy_sequence -> ('a * 'a lazy_sequence) option
   3.288 +  val yieldn: int -> 'a lazy_sequence -> 'a list * 'a lazy_sequence
   3.289 +end;
   3.290 +
   3.291 +structure Lazy_Sequence : LAZY_SEQUENCE =
   3.292 +struct
   3.293 +
   3.294 +datatype lazy_sequence = datatype Lazy_Sequence.lazy_sequence;
   3.295 +
   3.296 +fun map f = @{code Lazy_Sequence.map} f;
   3.297 +
   3.298 +fun yield P = @{code Lazy_Sequence.yield} P;
   3.299 +
   3.300 +fun yieldn k = Predicate.anamorph yield k;
   3.301 +
   3.302 +end;
   3.303 +*}
   3.304 +
   3.305  
   3.306  subsection {* Generator Sequences *}
   3.307  
   3.308 -
   3.309  subsubsection {* General lazy sequence operation *}
   3.310  
   3.311 -definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence"
   3.312 +definition product :: "'a lazy_sequence \<Rightarrow> 'b lazy_sequence \<Rightarrow> ('a \<times> 'b) lazy_sequence"
   3.313  where
   3.314 -  "product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))"
   3.315 +  "product s1 s2 = bind s1 (\<lambda>a. bind s2 (\<lambda>b. single (a, b)))"
   3.316  
   3.317  
   3.318  subsubsection {* Small lazy typeclasses *}
   3.319  
   3.320  class small_lazy =
   3.321 -  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
   3.322 +  fixes small_lazy :: "code_numeral \<Rightarrow> 'a lazy_sequence"
   3.323  
   3.324  instantiation unit :: small_lazy
   3.325  begin
   3.326  
   3.327 -definition "small_lazy d = Lazy_Sequence.single ()"
   3.328 +definition "small_lazy d = single ()"
   3.329  
   3.330  instance ..
   3.331  
   3.332 @@ -170,15 +242,17 @@
   3.333  text {* maybe optimise this expression -> append (single x) xs == cons x xs 
   3.334  Performance difference? *}
   3.335  
   3.336 -function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence"
   3.337 -where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else
   3.338 -  Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))"
   3.339 -by pat_completeness auto
   3.340 +function small_lazy' :: "int \<Rightarrow> int \<Rightarrow> int lazy_sequence"
   3.341 +where
   3.342 +  "small_lazy' d i = (if d < i then empty
   3.343 +    else append (single i) (small_lazy' d (i + 1)))"
   3.344 +    by pat_completeness auto
   3.345  
   3.346  termination 
   3.347    by (relation "measure (%(d, i). nat (d + 1 - i))") auto
   3.348  
   3.349 -definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   3.350 +definition
   3.351 +  "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   3.352  
   3.353  instance ..
   3.354  
   3.355 @@ -197,9 +271,11 @@
   3.356  instantiation list :: (small_lazy) small_lazy
   3.357  begin
   3.358  
   3.359 -fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
   3.360 +fun small_lazy_list :: "code_numeral \<Rightarrow> 'a list lazy_sequence"
   3.361  where
   3.362 -  "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)"
   3.363 +  "small_lazy_list d = append (single [])
   3.364 +    (if d > 0 then bind (product (small_lazy (d - 1))
   3.365 +      (small_lazy (d - 1))) (\<lambda>(x, xs). single (x # xs)) else empty)"
   3.366  
   3.367  instance ..
   3.368  
   3.369 @@ -212,56 +288,61 @@
   3.370  
   3.371  definition hit_bound :: "'a hit_bound_lazy_sequence"
   3.372  where
   3.373 -  [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
   3.374 +  "hit_bound = Lazy_Sequence (\<lambda>_. Some (None, empty))"
   3.375  
   3.376 -definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
   3.377 +lemma list_of_lazy_sequence_hit_bound [simp]:
   3.378 +  "list_of_lazy_sequence hit_bound = [None]"
   3.379 +  by (simp add: hit_bound_def)
   3.380 +  
   3.381 +definition hb_single :: "'a \<Rightarrow> 'a hit_bound_lazy_sequence"
   3.382  where
   3.383 -  [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
   3.384 +  "hb_single x = Lazy_Sequence (\<lambda>_. Some (Some x, empty))"
   3.385  
   3.386 -primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
   3.387 +definition hb_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a hit_bound_lazy_sequence \<Rightarrow> 'b hit_bound_lazy_sequence"
   3.388  where
   3.389 -  "hb_flat Empty = Empty"
   3.390 -| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
   3.391 +  "hb_map f xq = map (Option.map f) xq"
   3.392 +
   3.393 +lemma hb_map_code [code]:
   3.394 +  "hb_map f xq =
   3.395 +    Lazy_Sequence (\<lambda>_. Option.map (\<lambda>(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
   3.396 +  using map_code [of "Option.map f" xq] by (simp add: hb_map_def)
   3.397  
   3.398 -lemma [code]:
   3.399 -  "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
   3.400 -    None => None
   3.401 -  | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
   3.402 -apply (cases "xqq")
   3.403 -apply (auto simp add: Seq_yield)
   3.404 -unfolding Lazy_Sequence_def
   3.405 -by auto
   3.406 +definition hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence \<Rightarrow> 'a hit_bound_lazy_sequence"
   3.407 +where
   3.408 +  "hb_flat xqq = lazy_sequence_of_list (concat
   3.409 +    (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)))"
   3.410  
   3.411 -primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
   3.412 -where
   3.413 -  "hb_map f Empty = Empty"
   3.414 -| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
   3.415 +lemma list_of_lazy_sequence_hb_flat [simp]:
   3.416 +  "list_of_lazy_sequence (hb_flat xqq) =
   3.417 +    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))"
   3.418 +  by (simp add: hb_flat_def)
   3.419  
   3.420 -lemma [code]:
   3.421 -  "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
   3.422 -apply (cases xq)
   3.423 -apply (auto simp add: Seq_yield)
   3.424 -unfolding Lazy_Sequence_def
   3.425 -apply auto
   3.426 -done
   3.427 +lemma hb_flat_code [code]:
   3.428 +  "hb_flat xqq = Lazy_Sequence (\<lambda>_. case yield xqq of
   3.429 +    None \<Rightarrow> None
   3.430 +  | Some (xq, xqq') \<Rightarrow> yield
   3.431 +     (append (case xq of None \<Rightarrow> hit_bound | Some xq \<Rightarrow> xq) (hb_flat xqq')))"
   3.432 +  by (simp add: lazy_sequence_eq_iff split: list.splits option.splits)
   3.433  
   3.434 -definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
   3.435 +definition hb_bind :: "'a hit_bound_lazy_sequence \<Rightarrow> ('a \<Rightarrow> 'b hit_bound_lazy_sequence) \<Rightarrow> 'b hit_bound_lazy_sequence"
   3.436  where
   3.437 -  [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
   3.438 +  "hb_bind xq f = hb_flat (hb_map f xq)"
   3.439  
   3.440 -definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
   3.441 +definition hb_if_seq :: "bool \<Rightarrow> unit hit_bound_lazy_sequence"
   3.442  where
   3.443    "hb_if_seq b = (if b then hb_single () else empty)"
   3.444  
   3.445 -definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
   3.446 +definition hb_not_seq :: "unit hit_bound_lazy_sequence \<Rightarrow> unit lazy_sequence"
   3.447  where
   3.448 -  "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
   3.449 +  "hb_not_seq xq = (case yield xq of
   3.450 +    None \<Rightarrow> single ()
   3.451 +  | Some (x, xq) \<Rightarrow> empty)"
   3.452  
   3.453 -hide_type (open) lazy_sequence
   3.454 -hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq
   3.455 -  iterate_upto not_seq product
   3.456 -  
   3.457 -hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def
   3.458 -  iterate_upto.simps product_def if_seq_def not_seq_def
   3.459 +hide_const (open) yield empty single append flat map bind
   3.460 +  if_seq those iterate_upto not_seq product
   3.461 +
   3.462 +hide_fact (open) yield_def empty_def single_def append_def flat_def map_def bind_def
   3.463 +  if_seq_def those_def not_seq_def product_def 
   3.464  
   3.465  end
   3.466 +
     4.1 --- a/src/HOL/Library/DAList.thy	Thu Feb 14 17:58:28 2013 +0100
     4.2 +++ b/src/HOL/Library/DAList.thy	Thu Feb 14 15:27:10 2013 +0100
     4.3 @@ -117,7 +117,7 @@
     4.4  
     4.5  fun (in term_syntax) random_aux_alist 
     4.6  where
     4.7 -  "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)]))"
     4.8 +  "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)]))"
     4.9  
    4.10  instantiation alist :: (random, random) random
    4.11  begin
     5.1 --- a/src/HOL/Library/Multiset.thy	Thu Feb 14 17:58:28 2013 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Thu Feb 14 15:27:10 2013 +0100
     5.3 @@ -1314,7 +1314,7 @@
     5.4  begin
     5.5  
     5.6  definition
     5.7 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
     5.8 +  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
     5.9  
    5.10  instance ..
    5.11  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Limited_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
     6.3 @@ -0,0 +1,216 @@
     6.4 +
     6.5 +(* Author: Lukas Bulwahn, TU Muenchen *)
     6.6 +
     6.7 +header {* Depth-Limited Sequences with failure element *}
     6.8 +
     6.9 +theory Limited_Sequence
    6.10 +imports Lazy_Sequence
    6.11 +begin
    6.12 +
    6.13 +subsection {* Depth-Limited Sequence *}
    6.14 +
    6.15 +type_synonym 'a dseq = "code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
    6.16 +
    6.17 +definition empty :: "'a dseq"
    6.18 +where
    6.19 +  "empty = (\<lambda>_ _. Some Lazy_Sequence.empty)"
    6.20 +
    6.21 +definition single :: "'a \<Rightarrow> 'a dseq"
    6.22 +where
    6.23 +  "single x = (\<lambda>_ _. Some (Lazy_Sequence.single x))"
    6.24 +
    6.25 +definition eval :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> 'a lazy_sequence option"
    6.26 +where
    6.27 +  [simp]: "eval f i pol = f i pol"
    6.28 +
    6.29 +definition yield :: "'a dseq \<Rightarrow> code_numeral \<Rightarrow> bool \<Rightarrow> ('a \<times> 'a dseq) option" 
    6.30 +where
    6.31 +  "yield f i pol = (case eval f i pol of
    6.32 +    None \<Rightarrow> None
    6.33 +  | Some s \<Rightarrow> (Option.map \<circ> apsnd) (\<lambda>r _ _. Some r) (Lazy_Sequence.yield s))"
    6.34 +
    6.35 +definition map_seq :: "('a \<Rightarrow> 'b dseq) \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'b dseq"
    6.36 +where
    6.37 +  "map_seq f xq i pol = Option.map Lazy_Sequence.flat
    6.38 +    (Lazy_Sequence.those (Lazy_Sequence.map (\<lambda>x. f x i pol) xq))"
    6.39 +
    6.40 +lemma map_seq_code [code]:
    6.41 +  "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    6.42 +    None \<Rightarrow> Some Lazy_Sequence.empty
    6.43 +  | Some (x, xq') \<Rightarrow> (case eval (f x) i pol of
    6.44 +      None \<Rightarrow> None
    6.45 +    | Some yq \<Rightarrow> (case map_seq f xq' i pol of
    6.46 +        None \<Rightarrow> None
    6.47 +      | Some zq \<Rightarrow> Some (Lazy_Sequence.append yq zq))))"
    6.48 +  by (cases xq)
    6.49 +    (auto simp add: map_seq_def Lazy_Sequence.those_def lazy_sequence_eq_iff split: list.splits option.splits)
    6.50 +
    6.51 +definition bind :: "'a dseq \<Rightarrow> ('a \<Rightarrow> 'b dseq) \<Rightarrow> 'b dseq"
    6.52 +where
    6.53 +  "bind x f = (\<lambda>i pol. 
    6.54 +     if i = 0 then
    6.55 +       (if pol then Some Lazy_Sequence.empty else None)
    6.56 +     else
    6.57 +       (case x (i - 1) pol of
    6.58 +         None \<Rightarrow> None
    6.59 +       | Some xq \<Rightarrow> map_seq f xq i pol))"
    6.60 +
    6.61 +definition union :: "'a dseq \<Rightarrow> 'a dseq \<Rightarrow> 'a dseq"
    6.62 +where
    6.63 +  "union x y = (\<lambda>i pol. case (x i pol, y i pol) of
    6.64 +      (Some xq, Some yq) \<Rightarrow> Some (Lazy_Sequence.append xq yq)
    6.65 +    | _ \<Rightarrow> None)"
    6.66 +
    6.67 +definition if_seq :: "bool \<Rightarrow> unit dseq"
    6.68 +where
    6.69 +  "if_seq b = (if b then single () else empty)"
    6.70 +
    6.71 +definition not_seq :: "unit dseq \<Rightarrow> unit dseq"
    6.72 +where
    6.73 +  "not_seq x = (\<lambda>i pol. case x i (\<not> pol) of
    6.74 +    None \<Rightarrow> Some Lazy_Sequence.empty
    6.75 +  | Some xq \<Rightarrow> (case Lazy_Sequence.yield xq of
    6.76 +      None \<Rightarrow> Some (Lazy_Sequence.single ())
    6.77 +    | Some _ \<Rightarrow> Some (Lazy_Sequence.empty)))"
    6.78 +
    6.79 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dseq \<Rightarrow> 'b dseq"
    6.80 +where
    6.81 +  "map f g = (\<lambda>i pol. case g i pol of
    6.82 +     None \<Rightarrow> None
    6.83 +   | Some xq \<Rightarrow> Some (Lazy_Sequence.map f xq))"
    6.84 +
    6.85 +
    6.86 +subsection {* Positive Depth-Limited Sequence *}
    6.87 +
    6.88 +type_synonym 'a pos_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
    6.89 +
    6.90 +definition pos_empty :: "'a pos_dseq"
    6.91 +where
    6.92 +  "pos_empty = (\<lambda>i. Lazy_Sequence.empty)"
    6.93 +
    6.94 +definition pos_single :: "'a \<Rightarrow> 'a pos_dseq"
    6.95 +where
    6.96 +  "pos_single x = (\<lambda>i. Lazy_Sequence.single x)"
    6.97 +
    6.98 +definition pos_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
    6.99 +where
   6.100 +  "pos_bind x f = (\<lambda>i. Lazy_Sequence.bind (x i) (\<lambda>a. f a i))"
   6.101 +
   6.102 +definition pos_decr_bind :: "'a pos_dseq \<Rightarrow> ('a \<Rightarrow> 'b pos_dseq) \<Rightarrow> 'b pos_dseq"
   6.103 +where
   6.104 +  "pos_decr_bind x f = (\<lambda>i. 
   6.105 +     if i = 0 then
   6.106 +       Lazy_Sequence.empty
   6.107 +     else
   6.108 +       Lazy_Sequence.bind (x (i - 1)) (\<lambda>a. f a i))"
   6.109 +
   6.110 +definition pos_union :: "'a pos_dseq \<Rightarrow> 'a pos_dseq \<Rightarrow> 'a pos_dseq"
   6.111 +where
   6.112 +  "pos_union xq yq = (\<lambda>i. Lazy_Sequence.append (xq i) (yq i))"
   6.113 +
   6.114 +definition pos_if_seq :: "bool \<Rightarrow> unit pos_dseq"
   6.115 +where
   6.116 +  "pos_if_seq b = (if b then pos_single () else pos_empty)"
   6.117 +
   6.118 +definition pos_iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a pos_dseq"
   6.119 +where
   6.120 +  "pos_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto f n m)"
   6.121 + 
   6.122 +definition pos_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pos_dseq \<Rightarrow> 'b pos_dseq"
   6.123 +where
   6.124 +  "pos_map f xq = (\<lambda>i. Lazy_Sequence.map f (xq i))"
   6.125 +
   6.126 +
   6.127 +subsection {* Negative Depth-Limited Sequence *}
   6.128 +
   6.129 +type_synonym 'a neg_dseq = "code_numeral \<Rightarrow> 'a Lazy_Sequence.hit_bound_lazy_sequence"
   6.130 +
   6.131 +definition neg_empty :: "'a neg_dseq"
   6.132 +where
   6.133 +  "neg_empty = (\<lambda>i. Lazy_Sequence.empty)"
   6.134 +
   6.135 +definition neg_single :: "'a \<Rightarrow> 'a neg_dseq"
   6.136 +where
   6.137 +  "neg_single x = (\<lambda>i. Lazy_Sequence.hb_single x)"
   6.138 +
   6.139 +definition neg_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
   6.140 +where
   6.141 +  "neg_bind x f = (\<lambda>i. hb_bind (x i) (\<lambda>a. f a i))"
   6.142 +
   6.143 +definition neg_decr_bind :: "'a neg_dseq \<Rightarrow> ('a \<Rightarrow> 'b neg_dseq) \<Rightarrow> 'b neg_dseq"
   6.144 +where
   6.145 +  "neg_decr_bind x f = (\<lambda>i. 
   6.146 +     if i = 0 then
   6.147 +       Lazy_Sequence.hit_bound
   6.148 +     else
   6.149 +       hb_bind (x (i - 1)) (\<lambda>a. f a i))"
   6.150 +
   6.151 +definition neg_union :: "'a neg_dseq \<Rightarrow> 'a neg_dseq \<Rightarrow> 'a neg_dseq"
   6.152 +where
   6.153 +  "neg_union x y = (\<lambda>i. Lazy_Sequence.append (x i) (y i))"
   6.154 +
   6.155 +definition neg_if_seq :: "bool \<Rightarrow> unit neg_dseq"
   6.156 +where
   6.157 +  "neg_if_seq b = (if b then neg_single () else neg_empty)"
   6.158 +
   6.159 +definition neg_iterate_upto 
   6.160 +where
   6.161 +  "neg_iterate_upto f n m = (\<lambda>i. Lazy_Sequence.iterate_upto (\<lambda>i. Some (f i)) n m)"
   6.162 +
   6.163 +definition neg_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a neg_dseq \<Rightarrow> 'b neg_dseq"
   6.164 +where
   6.165 +  "neg_map f xq = (\<lambda>i. Lazy_Sequence.hb_map f (xq i))"
   6.166 +
   6.167 +
   6.168 +subsection {* Negation *}
   6.169 +
   6.170 +definition pos_not_seq :: "unit neg_dseq \<Rightarrow> unit pos_dseq"
   6.171 +where
   6.172 +  "pos_not_seq xq = (\<lambda>i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
   6.173 +
   6.174 +definition neg_not_seq :: "unit pos_dseq \<Rightarrow> unit neg_dseq"
   6.175 +where
   6.176 +  "neg_not_seq x = (\<lambda>i. case Lazy_Sequence.yield (x i) of
   6.177 +    None => Lazy_Sequence.hb_single ()
   6.178 +  | Some ((), xq) => Lazy_Sequence.empty)"
   6.179 +
   6.180 +
   6.181 +ML {*
   6.182 +signature LIMITED_SEQUENCE =
   6.183 +sig
   6.184 +  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
   6.185 +  val map : ('a -> 'b) -> 'a dseq -> 'b dseq
   6.186 +  val yield : 'a dseq -> int -> bool -> ('a * 'a dseq) option
   6.187 +  val yieldn : int -> 'a dseq -> int -> bool -> 'a list * 'a dseq
   6.188 +end;
   6.189 +
   6.190 +structure Limited_Sequence : LIMITED_SEQUENCE =
   6.191 +struct
   6.192 +
   6.193 +type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
   6.194 +
   6.195 +fun map f = @{code Limited_Sequence.map} f;
   6.196 +
   6.197 +fun yield f = @{code Limited_Sequence.yield} f;
   6.198 +
   6.199 +fun yieldn n f i pol = (case f i pol of
   6.200 +    NONE => ([], fn _ => fn _ => NONE)
   6.201 +  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn _ => fn _ => SOME s') end);
   6.202 +
   6.203 +end;
   6.204 +*}
   6.205 +
   6.206 +code_reserved Eval Limited_Sequence
   6.207 +
   6.208 +
   6.209 +hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
   6.210 +  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
   6.211 +  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
   6.212 +
   6.213 +hide_fact (open) yield_def empty_def single_def eval_def map_seq_def bind_def union_def
   6.214 +  if_seq_def not_seq_def map_def
   6.215 +  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
   6.216 +  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
   6.217 +
   6.218 +end
   6.219 +
     7.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Feb 14 17:58:28 2013 +0100
     7.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Feb 14 15:27:10 2013 +0100
     7.3 @@ -269,7 +269,7 @@
     7.4   @{const_name transfer_morphism},
     7.5   @{const_name enum_prod_inst.enum_all_prod},
     7.6   @{const_name enum_prod_inst.enum_ex_prod},
     7.7 - @{const_name Quickcheck.catch_match},
     7.8 + @{const_name Quickcheck_Random.catch_match},
     7.9   @{const_name Quickcheck_Exhaustive.unknown},
    7.10   @{const_name Num.Bit0}, @{const_name Num.Bit1}
    7.11   (*@{const_name "==>"}, @{const_name "=="}*)]
     8.1 --- a/src/HOL/New_DSequence.thy	Thu Feb 14 17:58:28 2013 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,111 +0,0 @@
     8.4 -
     8.5 -(* Author: Lukas Bulwahn, TU Muenchen *)
     8.6 -
     8.7 -header {* Depth-Limited Sequences with failure element *}
     8.8 -
     8.9 -theory New_DSequence
    8.10 -imports DSequence
    8.11 -begin
    8.12 -
    8.13 -subsection {* Positive Depth-Limited Sequence *}
    8.14 -
    8.15 -type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
    8.16 -
    8.17 -definition pos_empty :: "'a pos_dseq"
    8.18 -where
    8.19 -  "pos_empty = (%i. Lazy_Sequence.empty)"
    8.20 -
    8.21 -definition pos_single :: "'a => 'a pos_dseq"
    8.22 -where
    8.23 -  "pos_single x = (%i. Lazy_Sequence.single x)"
    8.24 -
    8.25 -definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
    8.26 -where
    8.27 -  "pos_bind x f = (%i. Lazy_Sequence.bind (x i) (%a. f a i))"
    8.28 -
    8.29 -definition pos_decr_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
    8.30 -where
    8.31 -  "pos_decr_bind x f = (%i. 
    8.32 -     if i = 0 then
    8.33 -       Lazy_Sequence.empty
    8.34 -     else
    8.35 -       Lazy_Sequence.bind (x (i - 1)) (%a. f a i))"
    8.36 -
    8.37 -definition pos_union :: "'a pos_dseq => 'a pos_dseq => 'a pos_dseq"
    8.38 -where
    8.39 -  "pos_union xq yq = (%i. Lazy_Sequence.append (xq i) (yq i))"
    8.40 -
    8.41 -definition pos_if_seq :: "bool => unit pos_dseq"
    8.42 -where
    8.43 -  "pos_if_seq b = (if b then pos_single () else pos_empty)"
    8.44 -
    8.45 -definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_dseq"
    8.46 -where
    8.47 -  "pos_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto f n m)"
    8.48 - 
    8.49 -definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
    8.50 -where
    8.51 -  "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    8.52 -
    8.53 -subsection {* Negative Depth-Limited Sequence *}
    8.54 -
    8.55 -type_synonym 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    8.56 -
    8.57 -definition neg_empty :: "'a neg_dseq"
    8.58 -where
    8.59 -  "neg_empty = (%i. Lazy_Sequence.empty)"
    8.60 -
    8.61 -definition neg_single :: "'a => 'a neg_dseq"
    8.62 -where
    8.63 -  "neg_single x = (%i. Lazy_Sequence.hb_single x)"
    8.64 -
    8.65 -definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
    8.66 -where
    8.67 -  "neg_bind x f = (%i. hb_bind (x i) (%a. f a i))"
    8.68 -
    8.69 -definition neg_decr_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
    8.70 -where
    8.71 -  "neg_decr_bind x f = (%i. 
    8.72 -     if i = 0 then
    8.73 -       Lazy_Sequence.hit_bound
    8.74 -     else
    8.75 -       hb_bind (x (i - 1)) (%a. f a i))"
    8.76 -
    8.77 -definition neg_union :: "'a neg_dseq => 'a neg_dseq => 'a neg_dseq"
    8.78 -where
    8.79 -  "neg_union x y = (%i. Lazy_Sequence.append (x i) (y i))"
    8.80 -
    8.81 -definition neg_if_seq :: "bool => unit neg_dseq"
    8.82 -where
    8.83 -  "neg_if_seq b = (if b then neg_single () else neg_empty)"
    8.84 -
    8.85 -definition neg_iterate_upto 
    8.86 -where
    8.87 -  "neg_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto (%i. Some (f i)) n m)"
    8.88 -
    8.89 -definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
    8.90 -where
    8.91 -  "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    8.92 -
    8.93 -subsection {* Negation *}
    8.94 -
    8.95 -definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
    8.96 -where
    8.97 -  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
    8.98 -
    8.99 -definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
   8.100 -where
   8.101 -  "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of
   8.102 -    None => Lazy_Sequence.hb_single ()
   8.103 -  | Some ((), xq) => Lazy_Sequence.empty)"
   8.104 -
   8.105 -hide_type (open) pos_dseq neg_dseq
   8.106 -
   8.107 -hide_const (open)
   8.108 -  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
   8.109 -  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
   8.110 -hide_fact (open)
   8.111 -  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
   8.112 -  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
   8.113 -
   8.114 -end
     9.1 --- a/src/HOL/New_Random_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,114 +0,0 @@
     9.4 -
     9.5 -(* Author: Lukas Bulwahn, TU Muenchen *)
     9.6 -
     9.7 -theory New_Random_Sequence
     9.8 -imports Random_Sequence
     9.9 -begin
    9.10 -
    9.11 -type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
    9.12 -type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
    9.13 -
    9.14 -definition pos_empty :: "'a pos_random_dseq"
    9.15 -where
    9.16 -  "pos_empty = (%nrandom size seed. New_DSequence.pos_empty)"
    9.17 -
    9.18 -definition pos_single :: "'a => 'a pos_random_dseq"
    9.19 -where
    9.20 -  "pos_single x = (%nrandom size seed. New_DSequence.pos_single x)"
    9.21 -
    9.22 -definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
    9.23 -where
    9.24 -  "pos_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    9.25 -
    9.26 -definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
    9.27 -where
    9.28 -  "pos_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    9.29 -
    9.30 -definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
    9.31 -where
    9.32 -  "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
    9.33 -
    9.34 -definition pos_if_random_dseq :: "bool => unit pos_random_dseq"
    9.35 -where
    9.36 -  "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
    9.37 -
    9.38 -definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
    9.39 -where
    9.40 -  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)"
    9.41 -
    9.42 -definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
    9.43 -where
    9.44 -  "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))"
    9.45 -
    9.46 -fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
    9.47 -where
    9.48 -  "iter random nrandom seed =
    9.49 -    (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')))"
    9.50 -
    9.51 -definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
    9.52 -where
    9.53 -  "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
    9.54 -
    9.55 -definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
    9.56 -where
    9.57 -  "pos_map f P = pos_bind P (pos_single o f)"
    9.58 -
    9.59 -
    9.60 -definition neg_empty :: "'a neg_random_dseq"
    9.61 -where
    9.62 -  "neg_empty = (%nrandom size seed. New_DSequence.neg_empty)"
    9.63 -
    9.64 -definition neg_single :: "'a => 'a neg_random_dseq"
    9.65 -where
    9.66 -  "neg_single x = (%nrandom size seed. New_DSequence.neg_single x)"
    9.67 -
    9.68 -definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
    9.69 -where
    9.70 -  "neg_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    9.71 -
    9.72 -definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
    9.73 -where
    9.74 -  "neg_decr_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
    9.75 -
    9.76 -definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
    9.77 -where
    9.78 -  "neg_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
    9.79 -
    9.80 -definition neg_if_random_dseq :: "bool => unit neg_random_dseq"
    9.81 -where
    9.82 -  "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
    9.83 -
    9.84 -definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
    9.85 -where
    9.86 -  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)"
    9.87 -
    9.88 -definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
    9.89 -where
    9.90 -  "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))"
    9.91 -(*
    9.92 -fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
    9.93 -where
    9.94 -  "iter random nrandom seed =
    9.95 -    (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')))"
    9.96 -
    9.97 -definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
    9.98 -where
    9.99 -  "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
   9.100 -*)
   9.101 -definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
   9.102 -where
   9.103 -  "neg_map f P = neg_bind P (neg_single o f)"
   9.104 -(*
   9.105 -hide_const DSequence.empty DSequence.single DSequence.eval
   9.106 -  DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   9.107 -  DSequence.map
   9.108 -*)
   9.109 -
   9.110 -hide_const (open)
   9.111 -  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
   9.112 -  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
   9.113 -hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
   9.114 -(* FIXME: hide facts *)
   9.115 -(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
   9.116 -
   9.117 -end
   9.118 \ No newline at end of file
    10.1 --- a/src/HOL/Predicate.thy	Thu Feb 14 17:58:28 2013 +0100
    10.2 +++ b/src/HOL/Predicate.thy	Thu Feb 14 15:27:10 2013 +0100
    10.3 @@ -600,25 +600,34 @@
    10.4  
    10.5  code_reflect Predicate
    10.6    datatypes pred = Seq and seq = Empty | Insert | Join
    10.7 -  functions map
    10.8  
    10.9  ML {*
   10.10  signature PREDICATE =
   10.11  sig
   10.12 +  val anamorph: ('a -> ('b * 'a) option) -> int -> 'a -> 'b list * 'a
   10.13    datatype 'a pred = Seq of (unit -> 'a seq)
   10.14    and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
   10.15 +  val map: ('a -> 'b) -> 'a pred -> 'b pred
   10.16    val yield: 'a pred -> ('a * 'a pred) option
   10.17    val yieldn: int -> 'a pred -> 'a list * 'a pred
   10.18 -  val map: ('a -> 'b) -> 'a pred -> 'b pred
   10.19  end;
   10.20  
   10.21  structure Predicate : PREDICATE =
   10.22  struct
   10.23  
   10.24 +fun anamorph f k x =
   10.25 + (if k = 0 then ([], x)
   10.26 +  else case f x
   10.27 +   of NONE => ([], x)
   10.28 +    | SOME (v, y) => let
   10.29 +        val k' = k - 1;
   10.30 +        val (vs, z) = anamorph f k' y
   10.31 +      in (v :: vs, z) end);
   10.32 +
   10.33  datatype pred = datatype Predicate.pred
   10.34  datatype seq = datatype Predicate.seq
   10.35  
   10.36 -fun map f = Predicate.map f;
   10.37 +fun map f = @{code Predicate.map} f;
   10.38  
   10.39  fun yield (Seq f) = next (f ())
   10.40  and next Empty = NONE
   10.41 @@ -627,14 +636,7 @@
   10.42       of NONE => next xq
   10.43        | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq))));
   10.44  
   10.45 -fun anamorph f k x = (if k = 0 then ([], x)
   10.46 -  else case f x
   10.47 -   of NONE => ([], x)
   10.48 -    | SOME (v, y) => let
   10.49 -        val (vs, z) = anamorph f (k - 1) y
   10.50 -      in (v :: vs, z) end);
   10.51 -
   10.52 -fun yieldn P = anamorph yield P;
   10.53 +fun yieldn k = anamorph yield k;
   10.54  
   10.55  end;
   10.56  *}
    11.1 --- a/src/HOL/Predicate_Compile.thy	Thu Feb 14 17:58:28 2013 +0100
    11.2 +++ b/src/HOL/Predicate_Compile.thy	Thu Feb 14 15:27:10 2013 +0100
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* A compiler for predicates defined by introduction rules *}
    11.5  
    11.6  theory Predicate_Compile
    11.7 -imports New_Random_Sequence Quickcheck_Exhaustive
    11.8 +imports Random_Sequence Quickcheck_Exhaustive
    11.9  keywords "code_pred" :: thy_goal and "values" :: diag
   11.10  begin
   11.11  
    12.1 --- a/src/HOL/Quickcheck.thy	Thu Feb 14 17:58:28 2013 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,284 +0,0 @@
    12.4 -(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
    12.5 -
    12.6 -header {* A simple counterexample generator performing random testing *}
    12.7 -
    12.8 -theory Quickcheck
    12.9 -imports Random Code_Evaluation Enum
   12.10 -begin
   12.11 -
   12.12 -notation fcomp (infixl "\<circ>>" 60)
   12.13 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
   12.14 -
   12.15 -setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
   12.16 -
   12.17 -subsection {* Catching Match exceptions *}
   12.18 -
   12.19 -axiomatization catch_match :: "'a => 'a => 'a"
   12.20 -
   12.21 -code_const catch_match 
   12.22 -  (Quickcheck "((_) handle Match => _)")
   12.23 -
   12.24 -subsection {* The @{text random} class *}
   12.25 -
   12.26 -class random = typerep +
   12.27 -  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   12.28 -
   12.29 -
   12.30 -subsection {* Fundamental and numeric types*}
   12.31 -
   12.32 -instantiation bool :: random
   12.33 -begin
   12.34 -
   12.35 -definition
   12.36 -  "random i = Random.range 2 \<circ>\<rightarrow>
   12.37 -    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
   12.38 -
   12.39 -instance ..
   12.40 -
   12.41 -end
   12.42 -
   12.43 -instantiation itself :: (typerep) random
   12.44 -begin
   12.45 -
   12.46 -definition
   12.47 -  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   12.48 -where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
   12.49 -
   12.50 -instance ..
   12.51 -
   12.52 -end
   12.53 -
   12.54 -instantiation char :: random
   12.55 -begin
   12.56 -
   12.57 -definition
   12.58 -  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
   12.59 -
   12.60 -instance ..
   12.61 -
   12.62 -end
   12.63 -
   12.64 -instantiation String.literal :: random
   12.65 -begin
   12.66 -
   12.67 -definition 
   12.68 -  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
   12.69 -
   12.70 -instance ..
   12.71 -
   12.72 -end
   12.73 -
   12.74 -instantiation nat :: random
   12.75 -begin
   12.76 -
   12.77 -definition random_nat :: "code_numeral \<Rightarrow> Random.seed
   12.78 -  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
   12.79 -where
   12.80 -  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
   12.81 -     let n = Code_Numeral.nat_of k
   12.82 -     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
   12.83 -
   12.84 -instance ..
   12.85 -
   12.86 -end
   12.87 -
   12.88 -instantiation int :: random
   12.89 -begin
   12.90 -
   12.91 -definition
   12.92 -  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
   12.93 -     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
   12.94 -     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
   12.95 -
   12.96 -instance ..
   12.97 -
   12.98 -end
   12.99 -
  12.100 -
  12.101 -subsection {* Complex generators *}
  12.102 -
  12.103 -text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
  12.104 -
  12.105 -axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
  12.106 -  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  12.107 -  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
  12.108 -  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  12.109 -
  12.110 -definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  12.111 -  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  12.112 -where
  12.113 -  "random_fun_lift f =
  12.114 -    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
  12.115 -
  12.116 -instantiation "fun" :: ("{equal, term_of}", random) random
  12.117 -begin
  12.118 -
  12.119 -definition
  12.120 -  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  12.121 -  where "random i = random_fun_lift (random i)"
  12.122 -
  12.123 -instance ..
  12.124 -
  12.125 -end
  12.126 -
  12.127 -text {* Towards type copies and datatypes *}
  12.128 -
  12.129 -definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
  12.130 -  where "collapse f = (f \<circ>\<rightarrow> id)"
  12.131 -
  12.132 -definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
  12.133 -  where "beyond k l = (if l > k then l else 0)"
  12.134 -
  12.135 -lemma beyond_zero: "beyond k 0 = 0"
  12.136 -  by (simp add: beyond_def)
  12.137 -
  12.138 -
  12.139 -definition (in term_syntax) [code_unfold]:
  12.140 -  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
  12.141 -
  12.142 -definition (in term_syntax) [code_unfold]:
  12.143 -  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
  12.144 -
  12.145 -instantiation set :: (random) random
  12.146 -begin
  12.147 -
  12.148 -primrec random_aux_set
  12.149 -where
  12.150 -  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
  12.151 -| "random_aux_set (Code_Numeral.Suc i) j =
  12.152 -    collapse (Random.select_weight
  12.153 -      [(1, Pair valterm_emptyset),
  12.154 -       (Code_Numeral.Suc i,
  12.155 -        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
  12.156 -
  12.157 -lemma [code]:
  12.158 -  "random_aux_set i j =
  12.159 -    collapse (Random.select_weight [(1, Pair valterm_emptyset),
  12.160 -      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
  12.161 -proof (induct i rule: code_numeral.induct)
  12.162 -  case zero
  12.163 -  show ?case by (subst select_weight_drop_zero [symmetric])
  12.164 -    (simp add: random_aux_set.simps [simplified])
  12.165 -next
  12.166 -  case (Suc i)
  12.167 -  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
  12.168 -qed
  12.169 -
  12.170 -definition "random_set i = random_aux_set i i"
  12.171 -
  12.172 -instance ..
  12.173 -
  12.174 -end
  12.175 -
  12.176 -lemma random_aux_rec:
  12.177 -  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
  12.178 -  assumes "random_aux 0 = rhs 0"
  12.179 -    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
  12.180 -  shows "random_aux k = rhs k"
  12.181 -  using assms by (rule code_numeral.induct)
  12.182 -
  12.183 -subsection {* Deriving random generators for datatypes *}
  12.184 -
  12.185 -ML_file "Tools/Quickcheck/quickcheck_common.ML" 
  12.186 -ML_file "Tools/Quickcheck/random_generators.ML"
  12.187 -setup Random_Generators.setup
  12.188 -
  12.189 -
  12.190 -subsection {* Code setup *}
  12.191 -
  12.192 -code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
  12.193 -  -- {* With enough criminal energy this can be abused to derive @{prop False};
  12.194 -  for this reason we use a distinguished target @{text Quickcheck}
  12.195 -  not spoiling the regular trusted code generation *}
  12.196 -
  12.197 -code_reserved Quickcheck Random_Generators
  12.198 -
  12.199 -no_notation fcomp (infixl "\<circ>>" 60)
  12.200 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
  12.201 -
  12.202 -subsection {* The Random-Predicate Monad *} 
  12.203 -
  12.204 -fun iter' ::
  12.205 -  "'a itself => code_numeral => code_numeral => code_numeral * code_numeral
  12.206 -    => ('a::random) Predicate.pred"
  12.207 -where
  12.208 -  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
  12.209 -     let ((x, _), seed') = random sz seed
  12.210 -   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
  12.211 -
  12.212 -definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral
  12.213 -  => ('a::random) Predicate.pred"
  12.214 -where
  12.215 -  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
  12.216 -
  12.217 -lemma [code]:
  12.218 -  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
  12.219 -     let ((x, _), seed') = random sz seed
  12.220 -   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
  12.221 -unfolding iter_def iter'.simps[of _ nrandom] ..
  12.222 -
  12.223 -type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
  12.224 -
  12.225 -definition empty :: "'a randompred"
  12.226 -  where "empty = Pair (bot_class.bot)"
  12.227 -
  12.228 -definition single :: "'a => 'a randompred"
  12.229 -  where "single x = Pair (Predicate.single x)"
  12.230 -
  12.231 -definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
  12.232 -  where
  12.233 -    "bind R f = (\<lambda>s. let
  12.234 -       (P, s') = R s;
  12.235 -       (s1, s2) = Random.split_seed s'
  12.236 -     in (Predicate.bind P (%a. fst (f a s1)), s2))"
  12.237 -
  12.238 -definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
  12.239 -where
  12.240 -  "union R1 R2 = (\<lambda>s. let
  12.241 -     (P1, s') = R1 s; (P2, s'') = R2 s'
  12.242 -   in (sup_class.sup P1 P2, s''))"
  12.243 -
  12.244 -definition if_randompred :: "bool \<Rightarrow> unit randompred"
  12.245 -where
  12.246 -  "if_randompred b = (if b then single () else empty)"
  12.247 -
  12.248 -definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
  12.249 -where
  12.250 -  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
  12.251 -
  12.252 -definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
  12.253 -where
  12.254 -  "not_randompred P = (\<lambda>s. let
  12.255 -     (P', s') = P s
  12.256 -   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
  12.257 -
  12.258 -definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
  12.259 -  where "Random g = scomp g (Pair o (Predicate.single o fst))"
  12.260 -
  12.261 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
  12.262 -  where "map f P = bind P (single o f)"
  12.263 -
  12.264 -hide_fact
  12.265 -  random_bool_def
  12.266 -  random_itself_def
  12.267 -  random_char_def
  12.268 -  random_literal_def
  12.269 -  random_nat_def
  12.270 -  random_int_def
  12.271 -  random_fun_lift_def
  12.272 -  random_fun_def
  12.273 -  collapse_def
  12.274 -  beyond_def
  12.275 -  beyond_zero
  12.276 -  random_aux_rec
  12.277 -
  12.278 -hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
  12.279 -
  12.280 -hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def
  12.281 -  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
  12.282 -hide_type (open) randompred
  12.283 -hide_const (open) iter' iter empty single bind union if_randompred
  12.284 -  iterate_upto not_randompred Random map
  12.285 -
  12.286 -end
  12.287 -
    13.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 14 17:58:28 2013 +0100
    13.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 14 15:27:10 2013 +0100
    13.3 @@ -3,7 +3,7 @@
    13.4  header {* A simple counterexample generator performing exhaustive testing *}
    13.5  
    13.6  theory Quickcheck_Exhaustive
    13.7 -imports Quickcheck
    13.8 +imports Quickcheck_Random
    13.9  keywords "quickcheck_generator" :: thy_decl
   13.10  begin
   13.11  
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Quickcheck_Random.thy	Thu Feb 14 15:27:10 2013 +0100
    14.3 @@ -0,0 +1,204 @@
    14.4 +(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
    14.5 +
    14.6 +header {* A simple counterexample generator performing random testing *}
    14.7 +
    14.8 +theory Quickcheck_Random
    14.9 +imports Random Code_Evaluation Enum
   14.10 +begin
   14.11 +
   14.12 +notation fcomp (infixl "\<circ>>" 60)
   14.13 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
   14.14 +
   14.15 +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
   14.16 +
   14.17 +subsection {* Catching Match exceptions *}
   14.18 +
   14.19 +axiomatization catch_match :: "'a => 'a => 'a"
   14.20 +
   14.21 +code_const catch_match 
   14.22 +  (Quickcheck "((_) handle Match => _)")
   14.23 +
   14.24 +subsection {* The @{text random} class *}
   14.25 +
   14.26 +class random = typerep +
   14.27 +  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   14.28 +
   14.29 +
   14.30 +subsection {* Fundamental and numeric types*}
   14.31 +
   14.32 +instantiation bool :: random
   14.33 +begin
   14.34 +
   14.35 +definition
   14.36 +  "random i = Random.range 2 \<circ>\<rightarrow>
   14.37 +    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
   14.38 +
   14.39 +instance ..
   14.40 +
   14.41 +end
   14.42 +
   14.43 +instantiation itself :: (typerep) random
   14.44 +begin
   14.45 +
   14.46 +definition
   14.47 +  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   14.48 +where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
   14.49 +
   14.50 +instance ..
   14.51 +
   14.52 +end
   14.53 +
   14.54 +instantiation char :: random
   14.55 +begin
   14.56 +
   14.57 +definition
   14.58 +  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
   14.59 +
   14.60 +instance ..
   14.61 +
   14.62 +end
   14.63 +
   14.64 +instantiation String.literal :: random
   14.65 +begin
   14.66 +
   14.67 +definition 
   14.68 +  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
   14.69 +
   14.70 +instance ..
   14.71 +
   14.72 +end
   14.73 +
   14.74 +instantiation nat :: random
   14.75 +begin
   14.76 +
   14.77 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed
   14.78 +  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
   14.79 +where
   14.80 +  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
   14.81 +     let n = Code_Numeral.nat_of k
   14.82 +     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
   14.83 +
   14.84 +instance ..
   14.85 +
   14.86 +end
   14.87 +
   14.88 +instantiation int :: random
   14.89 +begin
   14.90 +
   14.91 +definition
   14.92 +  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
   14.93 +     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
   14.94 +     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
   14.95 +
   14.96 +instance ..
   14.97 +
   14.98 +end
   14.99 +
  14.100 +
  14.101 +subsection {* Complex generators *}
  14.102 +
  14.103 +text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
  14.104 +
  14.105 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
  14.106 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  14.107 +  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
  14.108 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  14.109 +
  14.110 +definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  14.111 +  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  14.112 +where
  14.113 +  "random_fun_lift f =
  14.114 +    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
  14.115 +
  14.116 +instantiation "fun" :: ("{equal, term_of}", random) random
  14.117 +begin
  14.118 +
  14.119 +definition
  14.120 +  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
  14.121 +  where "random i = random_fun_lift (random i)"
  14.122 +
  14.123 +instance ..
  14.124 +
  14.125 +end
  14.126 +
  14.127 +text {* Towards type copies and datatypes *}
  14.128 +
  14.129 +definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
  14.130 +  where "collapse f = (f \<circ>\<rightarrow> id)"
  14.131 +
  14.132 +definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
  14.133 +  where "beyond k l = (if l > k then l else 0)"
  14.134 +
  14.135 +lemma beyond_zero: "beyond k 0 = 0"
  14.136 +  by (simp add: beyond_def)
  14.137 +
  14.138 +
  14.139 +definition (in term_syntax) [code_unfold]:
  14.140 +  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
  14.141 +
  14.142 +definition (in term_syntax) [code_unfold]:
  14.143 +  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
  14.144 +
  14.145 +instantiation set :: (random) random
  14.146 +begin
  14.147 +
  14.148 +primrec random_aux_set
  14.149 +where
  14.150 +  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
  14.151 +| "random_aux_set (Code_Numeral.Suc i) j =
  14.152 +    collapse (Random.select_weight
  14.153 +      [(1, Pair valterm_emptyset),
  14.154 +       (Code_Numeral.Suc i,
  14.155 +        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
  14.156 +
  14.157 +lemma [code]:
  14.158 +  "random_aux_set i j =
  14.159 +    collapse (Random.select_weight [(1, Pair valterm_emptyset),
  14.160 +      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
  14.161 +proof (induct i rule: code_numeral.induct)
  14.162 +  case zero
  14.163 +  show ?case by (subst select_weight_drop_zero [symmetric])
  14.164 +    (simp add: random_aux_set.simps [simplified])
  14.165 +next
  14.166 +  case (Suc i)
  14.167 +  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
  14.168 +qed
  14.169 +
  14.170 +definition "random_set i = random_aux_set i i"
  14.171 +
  14.172 +instance ..
  14.173 +
  14.174 +end
  14.175 +
  14.176 +lemma random_aux_rec:
  14.177 +  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
  14.178 +  assumes "random_aux 0 = rhs 0"
  14.179 +    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
  14.180 +  shows "random_aux k = rhs k"
  14.181 +  using assms by (rule code_numeral.induct)
  14.182 +
  14.183 +subsection {* Deriving random generators for datatypes *}
  14.184 +
  14.185 +ML_file "Tools/Quickcheck/quickcheck_common.ML" 
  14.186 +ML_file "Tools/Quickcheck/random_generators.ML"
  14.187 +setup Random_Generators.setup
  14.188 +
  14.189 +
  14.190 +subsection {* Code setup *}
  14.191 +
  14.192 +code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
  14.193 +  -- {* With enough criminal energy this can be abused to derive @{prop False};
  14.194 +  for this reason we use a distinguished target @{text Quickcheck}
  14.195 +  not spoiling the regular trusted code generation *}
  14.196 +
  14.197 +code_reserved Quickcheck Random_Generators
  14.198 +
  14.199 +no_notation fcomp (infixl "\<circ>>" 60)
  14.200 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
  14.201 +    
  14.202 +hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
  14.203 +
  14.204 +hide_fact (open) collapse_def beyond_def random_fun_lift_def
  14.205 +
  14.206 +end
  14.207 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Random_Pred.thy	Thu Feb 14 15:27:10 2013 +0100
    15.3 @@ -0,0 +1,76 @@
    15.4 +
    15.5 +(* Author: Lukas Bulwahn, TU Muenchen *)
    15.6 +
    15.7 +header {* The Random-Predicate Monad *}
    15.8 +
    15.9 +theory Random_Pred
   15.10 +imports Quickcheck_Random
   15.11 +begin
   15.12 +
   15.13 +fun iter' :: "'a itself \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
   15.14 +where
   15.15 +  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
   15.16 +     let ((x, _), seed') = Quickcheck_Random.random sz seed
   15.17 +   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
   15.18 +
   15.19 +definition iter :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a::random) Predicate.pred"
   15.20 +where
   15.21 +  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
   15.22 +
   15.23 +lemma [code]:
   15.24 +  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
   15.25 +     let ((x, _), seed') = Quickcheck_Random.random sz seed
   15.26 +   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
   15.27 +   unfolding iter_def iter'.simps [of _ nrandom] ..
   15.28 +
   15.29 +type_synonym 'a random_pred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
   15.30 +
   15.31 +definition empty :: "'a random_pred"
   15.32 +  where "empty = Pair bot"
   15.33 +
   15.34 +definition single :: "'a => 'a random_pred"
   15.35 +  where "single x = Pair (Predicate.single x)"
   15.36 +
   15.37 +definition bind :: "'a random_pred \<Rightarrow> ('a \<Rightarrow> 'b random_pred) \<Rightarrow> 'b random_pred"
   15.38 +  where
   15.39 +    "bind R f = (\<lambda>s. let
   15.40 +       (P, s') = R s;
   15.41 +       (s1, s2) = Random.split_seed s'
   15.42 +     in (Predicate.bind P (%a. fst (f a s1)), s2))"
   15.43 +
   15.44 +definition union :: "'a random_pred \<Rightarrow> 'a random_pred \<Rightarrow> 'a random_pred"
   15.45 +where
   15.46 +  "union R1 R2 = (\<lambda>s. let
   15.47 +     (P1, s') = R1 s; (P2, s'') = R2 s'
   15.48 +   in (sup_class.sup P1 P2, s''))"
   15.49 +
   15.50 +definition if_randompred :: "bool \<Rightarrow> unit random_pred"
   15.51 +where
   15.52 +  "if_randompred b = (if b then single () else empty)"
   15.53 +
   15.54 +definition iterate_upto :: "(code_numeral \<Rightarrow> 'a) => code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a random_pred"
   15.55 +where
   15.56 +  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
   15.57 +
   15.58 +definition not_randompred :: "unit random_pred \<Rightarrow> unit random_pred"
   15.59 +where
   15.60 +  "not_randompred P = (\<lambda>s. let
   15.61 +     (P', s') = P s
   15.62 +   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
   15.63 +
   15.64 +definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a random_pred"
   15.65 +  where "Random g = scomp g (Pair o (Predicate.single o fst))"
   15.66 +
   15.67 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a random_pred \<Rightarrow> 'b random_pred"
   15.68 +  where "map f P = bind P (single o f)"
   15.69 +
   15.70 +hide_const (open) iter' iter empty single bind union if_randompred
   15.71 +  iterate_upto not_randompred Random map
   15.72 +
   15.73 +hide_fact iter'.simps
   15.74 +  
   15.75 +hide_fact (open) iter_def empty_def single_def bind_def union_def
   15.76 +  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
   15.77 +
   15.78 +end
   15.79 +
    16.1 --- a/src/HOL/Random_Sequence.thy	Thu Feb 14 17:58:28 2013 +0100
    16.2 +++ b/src/HOL/Random_Sequence.thy	Thu Feb 14 15:27:10 2013 +0100
    16.3 @@ -1,32 +1,34 @@
    16.4  
    16.5  (* Author: Lukas Bulwahn, TU Muenchen *)
    16.6  
    16.7 +header {* Various kind of sequences inside the random monad *}
    16.8 +
    16.9  theory Random_Sequence
   16.10 -imports Quickcheck
   16.11 +imports Random_Pred
   16.12  begin
   16.13  
   16.14 -type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
   16.15 +type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a Limited_Sequence.dseq \<times> Random.seed)"
   16.16  
   16.17  definition empty :: "'a random_dseq"
   16.18  where
   16.19 -  "empty = (%nrandom size. Pair (DSequence.empty))"
   16.20 +  "empty = (%nrandom size. Pair (Limited_Sequence.empty))"
   16.21  
   16.22  definition single :: "'a => 'a random_dseq"
   16.23  where
   16.24 -  "single x = (%nrandom size. Pair (DSequence.single x))"
   16.25 +  "single x = (%nrandom size. Pair (Limited_Sequence.single x))"
   16.26  
   16.27  definition bind :: "'a random_dseq => ('a \<Rightarrow> 'b random_dseq) \<Rightarrow> 'b random_dseq"
   16.28  where
   16.29    "bind R f = (\<lambda>nrandom size s. let
   16.30       (P, s') = R nrandom size s;
   16.31       (s1, s2) = Random.split_seed s'
   16.32 -  in (DSequence.bind P (%a. fst (f a nrandom size s1)), s2))"
   16.33 +  in (Limited_Sequence.bind P (%a. fst (f a nrandom size s1)), s2))"
   16.34  
   16.35  definition union :: "'a random_dseq => 'a random_dseq => 'a random_dseq"
   16.36  where
   16.37    "union R1 R2 = (\<lambda>nrandom size s. let
   16.38       (S1, s') = R1 nrandom size s; (S2, s'') = R2 nrandom size s'
   16.39 -  in (DSequence.union S1 S2, s''))"
   16.40 +  in (Limited_Sequence.union S1 S2, s''))"
   16.41  
   16.42  definition if_random_dseq :: "bool => unit random_dseq"
   16.43  where
   16.44 @@ -36,26 +38,120 @@
   16.45  where
   16.46    "not_random_dseq R = (\<lambda>nrandom size s. let
   16.47       (S, s') = R nrandom size s
   16.48 -   in (DSequence.not_seq S, s'))"
   16.49 -
   16.50 -fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
   16.51 -where
   16.52 -  "Random g nrandom = (%size. if nrandom <= 0 then (Pair DSequence.empty) else
   16.53 -     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (DSequence.union (DSequence.single (fst r)) rs)))))"
   16.54 +   in (Limited_Sequence.not_seq S, s'))"
   16.55  
   16.56  definition map :: "('a => 'b) => 'a random_dseq => 'b random_dseq"
   16.57  where
   16.58    "map f P = bind P (single o f)"
   16.59  
   16.60 -(*
   16.61 -hide_const DSequence.empty DSequence.single DSequence.eval
   16.62 -  DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   16.63 -  DSequence.map
   16.64 -*)
   16.65 +fun Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a random_dseq"
   16.66 +where
   16.67 +  "Random g nrandom = (%size. if nrandom <= 0 then (Pair Limited_Sequence.empty) else
   16.68 +     (scomp (g size) (%r. scomp (Random g (nrandom - 1) size) (%rs. Pair (Limited_Sequence.union (Limited_Sequence.single (fst r)) rs)))))"
   16.69 +
   16.70 +
   16.71 +type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.pos_dseq"
   16.72 +
   16.73 +definition pos_empty :: "'a pos_random_dseq"
   16.74 +where
   16.75 +  "pos_empty = (%nrandom size seed. Limited_Sequence.pos_empty)"
   16.76 +
   16.77 +definition pos_single :: "'a => 'a pos_random_dseq"
   16.78 +where
   16.79 +  "pos_single x = (%nrandom size seed. Limited_Sequence.pos_single x)"
   16.80 +
   16.81 +definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
   16.82 +where
   16.83 +  "pos_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
   16.84 +
   16.85 +definition pos_decr_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
   16.86 +where
   16.87 +  "pos_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.pos_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
   16.88 +
   16.89 +definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
   16.90 +where
   16.91 +  "pos_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
   16.92 +
   16.93 +definition pos_if_random_dseq :: "bool => unit pos_random_dseq"
   16.94 +where
   16.95 +  "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
   16.96 +
   16.97 +definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
   16.98 +where
   16.99 +  "pos_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.pos_iterate_upto f n m)"
  16.100 +
  16.101 +definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
  16.102 +where
  16.103 +  "pos_map f P = pos_bind P (pos_single o f)"
  16.104 +
  16.105 +fun iter :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  16.106 +  \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
  16.107 +where
  16.108 +  "iter random nrandom seed =
  16.109 +    (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')))"
  16.110 +
  16.111 +definition pos_Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
  16.112 +  \<Rightarrow> 'a pos_random_dseq"
  16.113 +where
  16.114 +  "pos_Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
  16.115 +
  16.116 +
  16.117 +type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a Limited_Sequence.neg_dseq"
  16.118  
  16.119 -hide_const (open) empty single bind union if_random_dseq not_random_dseq Random map
  16.120 +definition neg_empty :: "'a neg_random_dseq"
  16.121 +where
  16.122 +  "neg_empty = (%nrandom size seed. Limited_Sequence.neg_empty)"
  16.123 +
  16.124 +definition neg_single :: "'a => 'a neg_random_dseq"
  16.125 +where
  16.126 +  "neg_single x = (%nrandom size seed. Limited_Sequence.neg_single x)"
  16.127 +
  16.128 +definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
  16.129 +where
  16.130 +  "neg_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
  16.131 +
  16.132 +definition neg_decr_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
  16.133 +where
  16.134 +  "neg_decr_bind R f = (\<lambda>nrandom size seed. Limited_Sequence.neg_decr_bind (R nrandom size seed) (%a. f a nrandom size seed))"
  16.135 +
  16.136 +definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
  16.137 +where
  16.138 +  "neg_union R1 R2 = (\<lambda>nrandom size seed. Limited_Sequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
  16.139 +
  16.140 +definition neg_if_random_dseq :: "bool => unit neg_random_dseq"
  16.141 +where
  16.142 +  "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
  16.143 +
  16.144 +definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
  16.145 +where
  16.146 +  "neg_iterate_upto f n m = (\<lambda>nrandom size seed. Limited_Sequence.neg_iterate_upto f n m)"
  16.147  
  16.148 -hide_type DSequence.dseq random_dseq
  16.149 -hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def
  16.150 +definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
  16.151 +where
  16.152 +  "neg_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.neg_not_seq (R nrandom size seed))"
  16.153 +
  16.154 +definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
  16.155 +where
  16.156 +  "neg_map f P = neg_bind P (neg_single o f)"
  16.157 +
  16.158 +definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
  16.159 +where
  16.160 +  "pos_not_random_dseq R = (\<lambda>nrandom size seed. Limited_Sequence.pos_not_seq (R nrandom size seed))"
  16.161 +
  16.162  
  16.163 -end
  16.164 \ No newline at end of file
  16.165 +hide_const (open)
  16.166 +  empty single bind union if_random_dseq not_random_dseq map Random
  16.167 +  pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_random_dseq pos_iterate_upto
  16.168 +  pos_not_random_dseq pos_map iter pos_Random
  16.169 +  neg_empty neg_single neg_bind neg_decr_bind neg_union neg_if_random_dseq neg_iterate_upto
  16.170 +  neg_not_random_dseq neg_map
  16.171 +
  16.172 +hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def
  16.173 +  map_def Random.simps
  16.174 +  pos_empty_def pos_single_def pos_bind_def pos_decr_bind_def pos_union_def pos_if_random_dseq_def
  16.175 +  pos_iterate_upto_def pos_not_random_dseq_def pos_map_def iter.simps pos_Random_def
  16.176 +  neg_empty_def neg_single_def neg_bind_def neg_decr_bind_def neg_union_def neg_if_random_dseq_def
  16.177 +  neg_iterate_upto_def neg_not_random_dseq_def neg_map_def
  16.178 +
  16.179 +end
  16.180 +
    17.1 --- a/src/HOL/Rat.thy	Thu Feb 14 17:58:28 2013 +0100
    17.2 +++ b/src/HOL/Rat.thy	Thu Feb 14 15:27:10 2013 +0100
    17.3 @@ -1030,7 +1030,7 @@
    17.4  begin
    17.5  
    17.6  definition
    17.7 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
    17.8 +  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>num. Random.range i \<circ>\<rightarrow> (\<lambda>denom. Pair (
    17.9       let j = Code_Numeral.int_of (denom + 1)
   17.10       in valterm_fract num (j, \<lambda>u. Code_Evaluation.term_of j))))"
   17.11  
    18.1 --- a/src/HOL/RealDef.thy	Thu Feb 14 17:58:28 2013 +0100
    18.2 +++ b/src/HOL/RealDef.thy	Thu Feb 14 15:27:10 2013 +0100
    18.3 @@ -1641,7 +1641,7 @@
    18.4  begin
    18.5  
    18.6  definition
    18.7 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
    18.8 +  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
    18.9  
   18.10  instance ..
   18.11  
    19.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 14 17:58:28 2013 +0100
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 14 15:27:10 2013 +0100
    19.3 @@ -956,7 +956,7 @@
    19.4      val tss = run (#timeout system_config, #prolog_system system_config)
    19.5        p (translate_const constant_table' name, args') output_names soln
    19.6      val _ = tracing "Restoring terms..."
    19.7 -    val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
    19.8 +    val empty = Const(@{const_name bot}, fastype_of t_compr)
    19.9      fun mk_insert x S =
   19.10        Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S 
   19.11      fun mk_set_compr in_insert [] xs =
    20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 14 17:58:28 2013 +0100
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Thu Feb 14 15:27:10 2013 +0100
    20.3 @@ -225,41 +225,41 @@
    20.4    @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
    20.5  
    20.6  fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
    20.7 -  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
    20.8 +  [Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
    20.9    | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
   20.10  
   20.11 -fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
   20.12 +fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
   20.13  
   20.14  fun mk_single t =
   20.15    let               
   20.16      val T = fastype_of t
   20.17    in
   20.18 -    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
   20.19 +    Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
   20.20    end;
   20.21  
   20.22  fun mk_bind (x, f) =
   20.23    let
   20.24      val T as (Type ("fun", [_, U])) = fastype_of f
   20.25    in
   20.26 -    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
   20.27 +    Const (@{const_name Random_Pred.bind}, fastype_of x --> T --> U) $ x $ f
   20.28    end
   20.29  
   20.30 -val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union}
   20.31 +val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union}
   20.32  
   20.33 -fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
   20.34 +fun mk_if cond = Const (@{const_name Random_Pred.if_randompred},
   20.35    HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
   20.36  
   20.37  fun mk_iterate_upto T (f, from, to) =
   20.38 -  list_comb (Const (@{const_name Quickcheck.iterate_upto},
   20.39 +  list_comb (Const (@{const_name Random_Pred.iterate_upto},
   20.40        [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
   20.41      [f, from, to])
   20.42  
   20.43  fun mk_not t =
   20.44    let
   20.45      val T = mk_randompredT HOLogic.unitT
   20.46 -  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
   20.47 +  in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end
   20.48  
   20.49 -fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
   20.50 +fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
   20.51    (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
   20.52  
   20.53  val compfuns = Predicate_Compile_Aux.CompilationFuns
   20.54 @@ -279,29 +279,29 @@
   20.55    Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   20.56    | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
   20.57  
   20.58 -fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   20.59 +fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, mk_dseqT T);
   20.60  
   20.61  fun mk_single t =
   20.62    let val T = fastype_of t
   20.63 -  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
   20.64 +  in Const(@{const_name Limited_Sequence.single}, T --> mk_dseqT T) $ t end;
   20.65  
   20.66  fun mk_bind (x, f) =
   20.67    let val T as Type ("fun", [_, U]) = fastype_of f
   20.68    in
   20.69 -    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   20.70 +    Const (@{const_name Limited_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   20.71    end;
   20.72  
   20.73 -val mk_plus = HOLogic.mk_binop @{const_name DSequence.union};
   20.74 +val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union};
   20.75  
   20.76 -fun mk_if cond = Const (@{const_name DSequence.if_seq},
   20.77 +fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq},
   20.78    HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
   20.79  
   20.80  fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
   20.81  
   20.82  fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   20.83 -  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
   20.84 +  in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end
   20.85  
   20.86 -fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
   20.87 +fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
   20.88    (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
   20.89  
   20.90  val compfuns = Predicate_Compile_Aux.CompilationFuns
   20.91 @@ -321,30 +321,30 @@
   20.92      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
   20.93    | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
   20.94  
   20.95 -fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
   20.96 +fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
   20.97  
   20.98  fun mk_single t =
   20.99    let
  20.100      val T = fastype_of t
  20.101 -  in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
  20.102 +  in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
  20.103  
  20.104  fun mk_bind (x, f) =
  20.105    let
  20.106      val T as Type ("fun", [_, U]) = fastype_of f
  20.107    in
  20.108 -    Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
  20.109 +    Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
  20.110    end;
  20.111    
  20.112  fun mk_decr_bind (x, f) =
  20.113    let
  20.114      val T as Type ("fun", [_, U]) = fastype_of f
  20.115    in
  20.116 -    Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.117 +    Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.118    end;
  20.119  
  20.120 -val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
  20.121 +val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
  20.122  
  20.123 -fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
  20.124 +fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
  20.125    HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
  20.126  
  20.127  fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
  20.128 @@ -355,9 +355,9 @@
  20.129      val nT =
  20.130        @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
  20.131          [Type (@{type_name Option.option}, [@{typ unit}])])
  20.132 -  in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end
  20.133 +  in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
  20.134  
  20.135 -fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map},
  20.136 +fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
  20.137    (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
  20.138  
  20.139  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
  20.140 @@ -382,30 +382,30 @@
  20.141      Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
  20.142    | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
  20.143  
  20.144 -fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
  20.145 +fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
  20.146  
  20.147  fun mk_single t =
  20.148    let
  20.149      val T = fastype_of t
  20.150 -  in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
  20.151 +  in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
  20.152  
  20.153  fun mk_bind (x, f) =
  20.154    let
  20.155      val T as Type ("fun", [_, U]) = fastype_of f
  20.156    in
  20.157 -    Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
  20.158 +    Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
  20.159    end;
  20.160    
  20.161  fun mk_decr_bind (x, f) =
  20.162    let
  20.163      val T as Type ("fun", [_, U]) = fastype_of f
  20.164    in
  20.165 -    Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.166 +    Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.167    end;
  20.168  
  20.169 -val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
  20.170 +val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
  20.171  
  20.172 -fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
  20.173 +fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
  20.174    HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
  20.175  
  20.176  fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
  20.177 @@ -416,9 +416,9 @@
  20.178      val pT =
  20.179        @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
  20.180          [@{typ unit}])
  20.181 -  in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end
  20.182 +  in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
  20.183  
  20.184 -fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map},
  20.185 +fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
  20.186    (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
  20.187  
  20.188  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
  20.189 @@ -445,34 +445,34 @@
  20.190      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
  20.191    | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
  20.192  
  20.193 -fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
  20.194 +fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
  20.195  
  20.196  fun mk_single t =
  20.197    let
  20.198      val T = fastype_of t
  20.199 -  in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
  20.200 +  in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
  20.201  
  20.202  fun mk_bind (x, f) =
  20.203    let
  20.204      val T as Type ("fun", [_, U]) = fastype_of f
  20.205    in
  20.206 -    Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
  20.207 +    Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
  20.208    end;
  20.209  
  20.210  fun mk_decr_bind (x, f) =
  20.211    let
  20.212      val T as Type ("fun", [_, U]) = fastype_of f
  20.213    in
  20.214 -    Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.215 +    Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.216    end;
  20.217  
  20.218 -val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
  20.219 +val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
  20.220  
  20.221 -fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
  20.222 +fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq},
  20.223    HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
  20.224  
  20.225  fun mk_iterate_upto T (f, from, to) =
  20.226 -  list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
  20.227 +  list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto},
  20.228        [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
  20.229          ---> mk_pos_random_dseqT T),
  20.230      [f, from, to])
  20.231 @@ -484,9 +484,9 @@
  20.232        @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
  20.233          [Type (@{type_name Option.option}, [@{typ unit}])])
  20.234  
  20.235 -  in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
  20.236 +  in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
  20.237  
  20.238 -fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
  20.239 +fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
  20.240    (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
  20.241  
  20.242  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
  20.243 @@ -514,34 +514,34 @@
  20.244          [Type (@{type_name Option.option}, [T])])])])])])) = T
  20.245    | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
  20.246  
  20.247 -fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
  20.248 +fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
  20.249  
  20.250  fun mk_single t =
  20.251    let
  20.252      val T = fastype_of t
  20.253 -  in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
  20.254 +  in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
  20.255  
  20.256  fun mk_bind (x, f) =
  20.257    let
  20.258      val T as Type ("fun", [_, U]) = fastype_of f
  20.259    in
  20.260 -    Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
  20.261 +    Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
  20.262    end;
  20.263  
  20.264  fun mk_decr_bind (x, f) =
  20.265    let
  20.266      val T as Type ("fun", [_, U]) = fastype_of f
  20.267    in
  20.268 -    Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.269 +    Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
  20.270    end;
  20.271  
  20.272 -val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
  20.273 +val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
  20.274  
  20.275 -fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
  20.276 +fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
  20.277    HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
  20.278  
  20.279  fun mk_iterate_upto T (f, from, to) =
  20.280 -  list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
  20.281 +  list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
  20.282        [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
  20.283          ---> mk_neg_random_dseqT T),
  20.284      [f, from, to])
  20.285 @@ -551,9 +551,9 @@
  20.286      val nT = mk_neg_random_dseqT HOLogic.unitT
  20.287      val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
  20.288      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
  20.289 -  in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
  20.290 +  in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
  20.291  
  20.292 -fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
  20.293 +fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
  20.294    (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
  20.295  
  20.296  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
    21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 14 17:58:28 2013 +0100
    21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Feb 14 15:27:10 2013 +0100
    21.3 @@ -26,8 +26,8 @@
    21.4    val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
    21.5    val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
    21.6      Proof.context -> Proof.context
    21.7 -  val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
    21.8 -  val put_dseq_random_result : (unit -> int -> int -> seed -> term DSequence.dseq * seed) ->
    21.9 +  val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
   21.10 +  val put_dseq_random_result : (unit -> int -> int -> seed -> term Limited_Sequence.dseq * seed) ->
   21.11      Proof.context -> Proof.context
   21.12    val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
   21.13      Proof.context -> Proof.context
   21.14 @@ -325,20 +325,20 @@
   21.15    function_name_prefix = "random_",
   21.16    compfuns = Predicate_Comp_Funs.compfuns,
   21.17    mk_random = (fn T => fn additional_arguments =>
   21.18 -  list_comb (Const(@{const_name Quickcheck.iter},
   21.19 +  list_comb (Const(@{const_name Random_Pred.iter},
   21.20    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   21.21      Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
   21.22    modify_funT = (fn T =>
   21.23      let
   21.24        val (Ts, U) = strip_type T
   21.25 -      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
   21.26 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}]
   21.27      in (Ts @ Ts') ---> U end),
   21.28    additional_arguments = (fn names =>
   21.29      let
   21.30        val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
   21.31      in
   21.32        [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
   21.33 -        Free (seed, @{typ "code_numeral * code_numeral"})]
   21.34 +        Free (seed, @{typ Random.seed})]
   21.35      end),
   21.36    wrap_compilation = K (K (K (K (K I))))
   21.37      : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   21.38 @@ -351,21 +351,21 @@
   21.39    function_name_prefix = "depth_limited_random_",
   21.40    compfuns = Predicate_Comp_Funs.compfuns,
   21.41    mk_random = (fn T => fn additional_arguments =>
   21.42 -  list_comb (Const(@{const_name Quickcheck.iter},
   21.43 +  list_comb (Const(@{const_name Random_Pred.iter},
   21.44    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   21.45      Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
   21.46    modify_funT = (fn T =>
   21.47      let
   21.48        val (Ts, U) = strip_type T
   21.49        val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
   21.50 -        @{typ "code_numeral * code_numeral"}]
   21.51 +        @{typ Random.seed}]
   21.52      in (Ts @ Ts') ---> U end),
   21.53    additional_arguments = (fn names =>
   21.54      let
   21.55        val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
   21.56      in
   21.57        [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
   21.58 -        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
   21.59 +        Free (size, @{typ code_numeral}), Free (seed, @{typ Random.seed})]
   21.60      end),
   21.61    wrap_compilation =
   21.62    fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
   21.63 @@ -423,11 +423,11 @@
   21.64    compfuns = Random_Sequence_CompFuns.compfuns,
   21.65    mk_random = (fn T => fn _ =>
   21.66    let
   21.67 -    val random = Const ("Quickcheck.random_class.random",
   21.68 +    val random = Const (@{const_name Quickcheck_Random.random},
   21.69        @{typ code_numeral} --> @{typ Random.seed} -->
   21.70          HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   21.71    in
   21.72 -    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   21.73 +    Const (@{const_name Random_Sequence.Random}, (@{typ code_numeral} --> @{typ Random.seed} -->
   21.74        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   21.75        Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   21.76    end),
   21.77 @@ -460,11 +460,11 @@
   21.78    compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
   21.79    mk_random = (fn T => fn _ =>
   21.80    let
   21.81 -    val random = Const ("Quickcheck.random_class.random",
   21.82 +    val random = Const (@{const_name Quickcheck_Random.random},
   21.83        @{typ code_numeral} --> @{typ Random.seed} -->
   21.84          HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   21.85    in
   21.86 -    Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   21.87 +    Const (@{const_name Random_Sequence.pos_Random}, (@{typ code_numeral} --> @{typ Random.seed} -->
   21.88        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   21.89        New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
   21.90    end),
   21.91 @@ -1647,7 +1647,7 @@
   21.92  
   21.93  structure Dseq_Result = Proof_Data
   21.94  (
   21.95 -  type T = unit -> term DSequence.dseq
   21.96 +  type T = unit -> term Limited_Sequence.dseq
   21.97    (* FIXME avoid user error with non-user text *)
   21.98    fun init _ () = error "Dseq_Result"
   21.99  );
  21.100 @@ -1655,7 +1655,7 @@
  21.101  
  21.102  structure Dseq_Random_Result = Proof_Data
  21.103  (
  21.104 -  type T = unit -> int -> int -> seed -> term DSequence.dseq * seed
  21.105 +  type T = unit -> int -> int -> seed -> term Limited_Sequence.dseq * seed
  21.106    (* FIXME avoid user error with non-user text *)
  21.107    fun init _ () = error "Dseq_Random_Result"
  21.108  );
  21.109 @@ -1843,24 +1843,24 @@
  21.110            let
  21.111              val [nrandom, size, depth] = arguments
  21.112            in
  21.113 -            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (DSequence.yieldn k
  21.114 +            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
  21.115                (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
  21.116 -                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
  21.117 +                thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
  21.118                    t' [] nrandom size
  21.119                  |> Random_Engine.run)
  21.120                depth true)) ())
  21.121            end
  21.122        | DSeq =>
  21.123 -          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (DSequence.yieldn k
  21.124 +          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
  21.125              (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
  21.126 -              thy NONE DSequence.map t' []) (the_single arguments) true)) ())
  21.127 +              thy NONE Limited_Sequence.map t' []) (the_single arguments) true)) ())
  21.128        | Pos_Generator_DSeq =>
  21.129            let
  21.130              val depth = (the_single arguments)
  21.131            in
  21.132              rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
  21.133                (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
  21.134 -              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
  21.135 +              thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
  21.136                t' [] depth))) ())
  21.137            end
  21.138        | New_Pos_Random_DSeq =>
  21.139 @@ -1875,7 +1875,7 @@
  21.140                    (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
  21.141                    thy NONE
  21.142                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
  21.143 -                    |> Lazy_Sequence.mapa (apfst proc))
  21.144 +                    |> Lazy_Sequence.map (apfst proc))
  21.145                      t' [] nrandom size seed depth))) ()))
  21.146              else rpair NONE
  21.147                (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
  21.148 @@ -1883,7 +1883,7 @@
  21.149                    (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
  21.150                    thy NONE 
  21.151                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
  21.152 -                    |> Lazy_Sequence.mapa proc)
  21.153 +                    |> Lazy_Sequence.map proc)
  21.154                      t' [] nrandom size seed depth))) ())
  21.155            end
  21.156        | _ =>
    22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Feb 14 17:58:28 2013 +0100
    22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Feb 14 15:27:10 2013 +0100
    22.3 @@ -12,7 +12,7 @@
    22.4      (unit -> int -> int -> int -> seed -> term list Predicate.pred) ->
    22.5        Proof.context -> Proof.context;
    22.6    val put_dseq_result :
    22.7 -    (unit -> int -> int -> seed -> term list DSequence.dseq * seed) ->
    22.8 +    (unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed) ->
    22.9        Proof.context -> Proof.context;
   22.10    val put_lseq_result :
   22.11      (unit -> int -> int -> seed -> int -> term list Lazy_Sequence.lazy_sequence) ->
   22.12 @@ -49,7 +49,7 @@
   22.13  
   22.14  structure Dseq_Result = Proof_Data
   22.15  (
   22.16 -  type T = unit -> int -> int -> seed -> term list DSequence.dseq * seed
   22.17 +  type T = unit -> int -> int -> seed -> term list Limited_Sequence.dseq * seed
   22.18    (* FIXME avoid user error with non-user text *)
   22.19    fun init _ () = error "Dseq_Result"
   22.20  );
   22.21 @@ -297,11 +297,11 @@
   22.22              val compiled_term =
   22.23                Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
   22.24                  thy4 (SOME target)
   22.25 -                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
   22.26 +                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
   22.27                  qc_term []
   22.28            in
   22.29              (fn size => fn nrandom => fn depth =>
   22.30 -              Option.map fst (DSequence.yield
   22.31 +              Option.map fst (Limited_Sequence.yield
   22.32                  (compiled_term nrandom size |> Random_Engine.run) depth true))
   22.33            end
   22.34        | New_Pos_Random_DSeq =>
   22.35 @@ -311,7 +311,7 @@
   22.36                  (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
   22.37                  thy4 (SOME target)
   22.38                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
   22.39 -                  g nrandom size s depth |> (Lazy_Sequence.mapa o map) proc)
   22.40 +                  g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
   22.41                    qc_term []
   22.42            in
   22.43              fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield 
   22.44 @@ -326,7 +326,7 @@
   22.45                Code_Runtime.dynamic_value_strict
   22.46                  (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
   22.47                  thy4 (SOME target)
   22.48 -                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.mapa o map) proc)
   22.49 +                (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
   22.50                  qc_term []
   22.51            in
   22.52              fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
    23.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Feb 14 17:58:28 2013 +0100
    23.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Feb 14 15:27:10 2013 +0100
    23.3 @@ -243,7 +243,7 @@
    23.4      val (T1, T2) = (fastype_of x, fastype_of (e genuine))
    23.5      val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2)
    23.6    in
    23.7 -    Const (@{const_name "Quickcheck.catch_match"}, T2 --> T2 --> T2) $ 
    23.8 +    Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $ 
    23.9        (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $
   23.10        (if_t $ genuine_only $ none $ safe false)
   23.11    end
   23.12 @@ -337,9 +337,9 @@
   23.13      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 
   23.14    in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
   23.15  
   23.16 -fun mk_unknown_term T = HOLogic.reflect_term (Const ("Quickcheck_Exhaustive.unknown", T))
   23.17 +fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
   23.18  
   23.19 -fun mk_safe_term t = @{term "Quickcheck.catch_match :: term => term => term"}
   23.20 +fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"}
   23.21        $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
   23.22  
   23.23  fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
    24.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Feb 14 17:58:28 2013 +0100
    24.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Feb 14 15:27:10 2013 +0100
    24.3 @@ -309,7 +309,7 @@
    24.4      val T = fastype_of then_t
    24.5      val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
    24.6    in
    24.7 -    Const (@{const_name "Quickcheck.catch_match"}, T --> T --> T) $ 
    24.8 +    Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ 
    24.9        (if_t $ cond $ then_t $ else_t genuine) $
   24.10        (if_t $ genuine_only $ none $ else_t false)
   24.11    end
    25.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Feb 14 17:58:28 2013 +0100
    25.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Feb 14 15:27:10 2013 +0100
    25.3 @@ -222,7 +222,7 @@
    25.4              tc @{typ Random.seed} (SOME T, @{typ Random.seed});
    25.5          val tk = if is_rec
    25.6            then if k = 0 then size
    25.7 -            else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    25.8 +            else @{term "Quickcheck_Random.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    25.9               $ HOLogic.mk_number @{typ code_numeral} k $ size
   25.10            else @{term "1::code_numeral"}
   25.11        in (is_rec, HOLogic.mk_prod (tk, t)) end;
   25.12 @@ -233,7 +233,7 @@
   25.13        |> (map o apfst) Type
   25.14        |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs));
   25.15      fun mk_select (rT, xs) =
   25.16 -      mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT]
   25.17 +      mk_const @{const_name Quickcheck_Random.collapse} [@{typ Random.seed}, termifyT rT]
   25.18        $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
   25.19          $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
   25.20            $ seed;
   25.21 @@ -315,7 +315,7 @@
   25.22        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   25.23          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   25.24      fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   25.25 -      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   25.26 +      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   25.27    in
   25.28      lambda genuine_only
   25.29        (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
   25.30 @@ -333,7 +333,7 @@
   25.31      val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
   25.32      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
   25.33      val (assms, concl) = Quickcheck_Common.strip_imp prop'
   25.34 -    val return = HOLogic.pair_const resultT @{typ "Random.seed"};
   25.35 +    val return = HOLogic.pair_const resultT @{typ Random.seed};
   25.36      fun mk_assms_report i =
   25.37        HOLogic.mk_prod (@{term "None :: (bool * term list) option"},
   25.38          HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT
   25.39 @@ -361,7 +361,7 @@
   25.40        mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
   25.41          (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
   25.42      fun mk_bindclause (_, _, i, T) = mk_scomp_split T
   25.43 -      (Sign.mk_const thy (@{const_name Quickcheck.random}, [T]) $ Bound i);
   25.44 +      (Sign.mk_const thy (@{const_name Quickcheck_Random.random}, [T]) $ Bound i);
   25.45    in
   25.46      lambda genuine_only
   25.47        (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true)))
    26.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 14 17:58:28 2013 +0100
    26.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 14 15:27:10 2013 +0100
    26.3 @@ -193,9 +193,9 @@
    26.4  
    26.5  (* FIXME: Ad hoc list *)
    26.6  val technical_prefixes =
    26.7 -  ["ATP", "Code_Evaluation", "Datatype", "DSequence", "Enum", "Lazy_Sequence",
    26.8 -   "Meson", "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence",
    26.9 -   "Quickcheck", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   26.10 +  ["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence",
   26.11 +   "Limited_Sequence", "Meson", "Metis", "Nitpick",
   26.12 +   "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
   26.13     "Random_Sequence", "Sledgehammer", "SMT"]
   26.14    |> map (suffix Long_Name.separator)
   26.15  
    27.1 --- a/src/HOL/Tools/hologic.ML	Thu Feb 14 17:58:28 2013 +0100
    27.2 +++ b/src/HOL/Tools/hologic.ML	Thu Feb 14 15:27:10 2013 +0100
    27.3 @@ -686,7 +686,7 @@
    27.4  
    27.5  val random_seedT = mk_prodT (code_numeralT, code_numeralT);
    27.6  
    27.7 -fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
    27.8 +fun mk_random T t = Const ("Quickcheck_Random.random_class.random", code_numeralT
    27.9    --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
   27.10  
   27.11  end;