author | paulson <lp15@cam.ac.uk> |
Mon, 30 May 2022 12:46:11 +0100 | |
changeset 75494 | eded3fe9e600 |
parent 72607 | feebdaa346e5 |
permissions | -rw-r--r-- |
62979 | 1 |
(* Title: HOL/Quickcheck_Random.thy |
2 |
Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen |
|
3 |
*) |
|
26265 | 4 |
|
60758 | 5 |
section \<open>A simple counterexample generator performing random testing\<close> |
26265 | 6 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
7 |
theory Quickcheck_Random |
40650
d40b347d5b0b
adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents:
38857
diff
changeset
|
8 |
imports Random Code_Evaluation Enum |
26265 | 9 |
begin |
10 |
||
60758 | 11 |
setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close> |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
12 |
|
60758 | 13 |
subsection \<open>Catching Match exceptions\<close> |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
14 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
15 |
axiomatization catch_match :: "'a => 'a => 'a" |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
16 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
17 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
18 |
constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)" |
31179 | 19 |
|
68587
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
20 |
code_reserved Quickcheck Match |
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
21 |
|
61799 | 22 |
subsection \<open>The \<open>random\<close> class\<close> |
26265 | 23 |
|
28335 | 24 |
class random = typerep + |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
25 |
fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
26265 | 26 |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset
|
27 |
|
60758 | 28 |
subsection \<open>Fundamental and numeric types\<close> |
31179 | 29 |
|
30 |
instantiation bool :: random |
|
31 |
begin |
|
32 |
||
72581 | 33 |
context |
34 |
includes state_combinator_syntax |
|
35 |
begin |
|
36 |
||
31179 | 37 |
definition |
37751 | 38 |
"random i = Random.range 2 \<circ>\<rightarrow> |
32657 | 39 |
(\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" |
31179 | 40 |
|
41 |
instance .. |
|
42 |
||
43 |
end |
|
44 |
||
72581 | 45 |
end |
46 |
||
31179 | 47 |
instantiation itself :: (typerep) random |
48 |
begin |
|
49 |
||
46975 | 50 |
definition |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
51 |
random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 52 |
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" |
31179 | 53 |
|
54 |
instance .. |
|
55 |
||
56 |
end |
|
57 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
58 |
instantiation char :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
59 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
60 |
|
72581 | 61 |
context |
62 |
includes state_combinator_syntax |
|
63 |
begin |
|
64 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
65 |
definition |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
48891
diff
changeset
|
66 |
"random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))" |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
67 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
68 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
69 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
70 |
end |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
71 |
|
72581 | 72 |
end |
73 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
74 |
instantiation String.literal :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
75 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
76 |
|
68587
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
77 |
definition |
32657 | 78 |
"random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))" |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
79 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
80 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
81 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
82 |
end |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
83 |
|
31179 | 84 |
instantiation nat :: random |
85 |
begin |
|
86 |
||
72581 | 87 |
context |
88 |
includes state_combinator_syntax |
|
89 |
begin |
|
90 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
91 |
definition random_nat :: "natural \<Rightarrow> Random.seed |
46975 | 92 |
\<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" |
93 |
where |
|
37751 | 94 |
"random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
95 |
let n = nat_of_natural k |
32657 | 96 |
in (n, \<lambda>_. Code_Evaluation.term_of n)))" |
31194 | 97 |
|
98 |
instance .. |
|
99 |
||
100 |
end |
|
101 |
||
72581 | 102 |
end |
103 |
||
31194 | 104 |
instantiation int :: random |
105 |
begin |
|
106 |
||
72581 | 107 |
context |
108 |
includes state_combinator_syntax |
|
109 |
begin |
|
110 |
||
31194 | 111 |
definition |
37751 | 112 |
"random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
113 |
let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k)))) |
32657 | 114 |
in (j, \<lambda>_. Code_Evaluation.term_of j)))" |
31179 | 115 |
|
116 |
instance .. |
|
117 |
||
30945 | 118 |
end |
31179 | 119 |
|
72581 | 120 |
end |
121 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
122 |
instantiation natural :: random |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
123 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
124 |
|
72581 | 125 |
context |
126 |
includes state_combinator_syntax |
|
127 |
begin |
|
128 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
129 |
definition random_natural :: "natural \<Rightarrow> Random.seed |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
130 |
\<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
131 |
where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
132 |
"random_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>n. Pair (n, \<lambda>_. Code_Evaluation.term_of n))" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
133 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
134 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
135 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
136 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
137 |
|
72581 | 138 |
end |
139 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
140 |
instantiation integer :: random |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
141 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
142 |
|
72581 | 143 |
context |
144 |
includes state_combinator_syntax |
|
145 |
begin |
|
146 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
147 |
definition random_integer :: "natural \<Rightarrow> Random.seed |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
148 |
\<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
149 |
where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
150 |
"random_integer i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
151 |
let j = (if k \<ge> i then integer_of_natural (k - i) else - (integer_of_natural (i - k))) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
152 |
in (j, \<lambda>_. Code_Evaluation.term_of j)))" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
153 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
154 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
155 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
156 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
157 |
|
72581 | 158 |
end |
159 |
||
31260 | 160 |
|
60758 | 161 |
subsection \<open>Complex generators\<close> |
31260 | 162 |
|
69593 | 163 |
text \<open>Towards \<^typ>\<open>'a \<Rightarrow> 'b\<close>\<close> |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
164 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
165 |
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
46975 | 166 |
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
167 |
\<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) |
|
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
168 |
\<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
169 |
|
31622 | 170 |
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
61076 | 171 |
\<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 172 |
where |
173 |
"random_fun_lift f = |
|
67399 | 174 |
random_fun_aux TYPEREP('a) TYPEREP('b) (=) Code_Evaluation.term_of f Random.split_seed" |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
175 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37751
diff
changeset
|
176 |
instantiation "fun" :: ("{equal, term_of}", random) random |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
177 |
begin |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
178 |
|
46975 | 179 |
definition |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
180 |
random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 181 |
where "random i = random_fun_lift (random i)" |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
182 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
183 |
instance .. |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
184 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
185 |
end |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
186 |
|
60758 | 187 |
text \<open>Towards type copies and datatypes\<close> |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
188 |
|
72581 | 189 |
context |
190 |
includes state_combinator_syntax |
|
191 |
begin |
|
192 |
||
46975 | 193 |
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" |
194 |
where "collapse f = (f \<circ>\<rightarrow> id)" |
|
31223
87bde6b5f793
re-added corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset
|
195 |
|
72581 | 196 |
end |
197 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
198 |
definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural" |
46975 | 199 |
where "beyond k l = (if l > k then l else 0)" |
31260 | 200 |
|
46975 | 201 |
lemma beyond_zero: "beyond k 0 = 0" |
31267 | 202 |
by (simp add: beyond_def) |
203 |
||
72607 | 204 |
context |
205 |
includes term_syntax |
|
206 |
begin |
|
46311 | 207 |
|
72607 | 208 |
definition [code_unfold]: |
46975 | 209 |
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" |
210 |
||
72607 | 211 |
definition [code_unfold]: |
46975 | 212 |
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" |
46311 | 213 |
|
72607 | 214 |
end |
215 |
||
46311 | 216 |
instantiation set :: (random) random |
217 |
begin |
|
218 |
||
72581 | 219 |
context |
220 |
includes state_combinator_syntax |
|
221 |
begin |
|
222 |
||
58389 | 223 |
fun random_aux_set |
46311 | 224 |
where |
225 |
"random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])" |
|
46975 | 226 |
| "random_aux_set (Code_Numeral.Suc i) j = |
227 |
collapse (Random.select_weight |
|
228 |
[(1, Pair valterm_emptyset), |
|
229 |
(Code_Numeral.Suc i, |
|
230 |
random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" |
|
46311 | 231 |
|
232 |
lemma [code]: |
|
46975 | 233 |
"random_aux_set i j = |
234 |
collapse (Random.select_weight [(1, Pair valterm_emptyset), |
|
235 |
(i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
236 |
proof (induct i rule: natural.induct) |
46311 | 237 |
case zero |
50046 | 238 |
show ?case by (subst select_weight_drop_zero [symmetric]) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
239 |
(simp add: random_aux_set.simps [simplified] less_natural_def) |
46311 | 240 |
next |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
241 |
case (Suc i) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
242 |
show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one) |
46311 | 243 |
qed |
244 |
||
46975 | 245 |
definition "random_set i = random_aux_set i i" |
46311 | 246 |
|
247 |
instance .. |
|
248 |
||
249 |
end |
|
250 |
||
72581 | 251 |
end |
252 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
253 |
lemma random_aux_rec: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
254 |
fixes random_aux :: "natural \<Rightarrow> 'a" |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
255 |
assumes "random_aux 0 = rhs 0" |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
256 |
and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)" |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
257 |
shows "random_aux k = rhs k" |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
258 |
using assms by (rule natural.induct) |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
259 |
|
60758 | 260 |
subsection \<open>Deriving random generators for datatypes\<close> |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
261 |
|
69605 | 262 |
ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close> |
263 |
ML_file \<open>Tools/Quickcheck/random_generators.ML\<close> |
|
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
264 |
|
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
265 |
|
60758 | 266 |
subsection \<open>Code setup\<close> |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
32657
diff
changeset
|
267 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
268 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
269 |
constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun" |
69593 | 270 |
\<comment> \<open>With enough criminal energy this can be abused to derive \<^prop>\<open>False\<close>; |
61799 | 271 |
for this reason we use a distinguished target \<open>Quickcheck\<close> |
60758 | 272 |
not spoiling the regular trusted code generation\<close> |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
273 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
274 |
code_reserved Quickcheck Random_Generators |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
275 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
276 |
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift |
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
277 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
278 |
hide_fact (open) collapse_def beyond_def random_fun_lift_def |
31267 | 279 |
|
31179 | 280 |
end |