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