author | wenzelm |
Fri, 05 Apr 2019 17:05:32 +0200 | |
changeset 70067 | 9b34dbeb1103 |
parent 69605 | a96320074298 |
child 72581 | de581f98a3a1 |
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 |
||
37751 | 11 |
notation fcomp (infixl "\<circ>>" 60) |
12 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
31179 | 13 |
|
60758 | 14 |
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
|
15 |
|
60758 | 16 |
subsection \<open>Catching Match exceptions\<close> |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
17 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
18 |
axiomatization catch_match :: "'a => 'a => 'a" |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
19 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
20 |
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
|
21 |
constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)" |
31179 | 22 |
|
68587
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
23 |
code_reserved Quickcheck Match |
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
24 |
|
61799 | 25 |
subsection \<open>The \<open>random\<close> class\<close> |
26265 | 26 |
|
28335 | 27 |
class random = typerep + |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
28 |
fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
26265 | 29 |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset
|
30 |
|
60758 | 31 |
subsection \<open>Fundamental and numeric types\<close> |
31179 | 32 |
|
33 |
instantiation bool :: random |
|
34 |
begin |
|
35 |
||
36 |
definition |
|
37751 | 37 |
"random i = Random.range 2 \<circ>\<rightarrow> |
32657 | 38 |
(\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" |
31179 | 39 |
|
40 |
instance .. |
|
41 |
||
42 |
end |
|
43 |
||
44 |
instantiation itself :: (typerep) random |
|
45 |
begin |
|
46 |
||
46975 | 47 |
definition |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
48 |
random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 49 |
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" |
31179 | 50 |
|
51 |
instance .. |
|
52 |
||
53 |
end |
|
54 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
55 |
instantiation char :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
56 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
57 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
58 |
definition |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
48891
diff
changeset
|
59 |
"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
|
60 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
61 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
62 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
63 |
end |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
64 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
65 |
instantiation String.literal :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
66 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
67 |
|
68587
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
68 |
definition |
32657 | 69 |
"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
|
70 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
71 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
72 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
73 |
end |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
74 |
|
31179 | 75 |
instantiation nat :: random |
76 |
begin |
|
77 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
78 |
definition random_nat :: "natural \<Rightarrow> Random.seed |
46975 | 79 |
\<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" |
80 |
where |
|
37751 | 81 |
"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
|
82 |
let n = nat_of_natural k |
32657 | 83 |
in (n, \<lambda>_. Code_Evaluation.term_of n)))" |
31194 | 84 |
|
85 |
instance .. |
|
86 |
||
87 |
end |
|
88 |
||
89 |
instantiation int :: random |
|
90 |
begin |
|
91 |
||
92 |
definition |
|
37751 | 93 |
"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
|
94 |
let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k)))) |
32657 | 95 |
in (j, \<lambda>_. Code_Evaluation.term_of j)))" |
31179 | 96 |
|
97 |
instance .. |
|
98 |
||
30945 | 99 |
end |
31179 | 100 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
101 |
instantiation natural :: random |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
102 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
103 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
104 |
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
|
105 |
\<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
|
106 |
where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
107 |
"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
|
108 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
109 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
110 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
111 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
112 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
113 |
instantiation integer :: random |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
114 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
115 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
116 |
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
|
117 |
\<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
|
118 |
where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
119 |
"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
|
120 |
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
|
121 |
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
|
122 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
123 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
124 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
125 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
126 |
|
31260 | 127 |
|
60758 | 128 |
subsection \<open>Complex generators\<close> |
31260 | 129 |
|
69593 | 130 |
text \<open>Towards \<^typ>\<open>'a \<Rightarrow> 'b\<close>\<close> |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
131 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
132 |
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
46975 | 133 |
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
134 |
\<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) |
|
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
135 |
\<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
|
136 |
|
31622 | 137 |
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
61076 | 138 |
\<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 139 |
where |
140 |
"random_fun_lift f = |
|
67399 | 141 |
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
|
142 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37751
diff
changeset
|
143 |
instantiation "fun" :: ("{equal, term_of}", random) random |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
144 |
begin |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
145 |
|
46975 | 146 |
definition |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
147 |
random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
46975 | 148 |
where "random i = random_fun_lift (random i)" |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
149 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
150 |
instance .. |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
151 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
152 |
end |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
153 |
|
60758 | 154 |
text \<open>Towards type copies and datatypes\<close> |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
155 |
|
46975 | 156 |
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" |
157 |
where "collapse f = (f \<circ>\<rightarrow> id)" |
|
31223
87bde6b5f793
re-added corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset
|
158 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
159 |
definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural" |
46975 | 160 |
where "beyond k l = (if l > k then l else 0)" |
31260 | 161 |
|
46975 | 162 |
lemma beyond_zero: "beyond k 0 = 0" |
31267 | 163 |
by (simp add: beyond_def) |
164 |
||
46311 | 165 |
|
46975 | 166 |
definition (in term_syntax) [code_unfold]: |
167 |
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" |
|
168 |
||
169 |
definition (in term_syntax) [code_unfold]: |
|
170 |
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" |
|
46311 | 171 |
|
172 |
instantiation set :: (random) random |
|
173 |
begin |
|
174 |
||
58389 | 175 |
fun random_aux_set |
46311 | 176 |
where |
177 |
"random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])" |
|
46975 | 178 |
| "random_aux_set (Code_Numeral.Suc i) j = |
179 |
collapse (Random.select_weight |
|
180 |
[(1, Pair valterm_emptyset), |
|
181 |
(Code_Numeral.Suc i, |
|
182 |
random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" |
|
46311 | 183 |
|
184 |
lemma [code]: |
|
46975 | 185 |
"random_aux_set i j = |
186 |
collapse (Random.select_weight [(1, Pair valterm_emptyset), |
|
187 |
(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
|
188 |
proof (induct i rule: natural.induct) |
46311 | 189 |
case zero |
50046 | 190 |
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
|
191 |
(simp add: random_aux_set.simps [simplified] less_natural_def) |
46311 | 192 |
next |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
193 |
case (Suc i) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
194 |
show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one) |
46311 | 195 |
qed |
196 |
||
46975 | 197 |
definition "random_set i = random_aux_set i i" |
46311 | 198 |
|
199 |
instance .. |
|
200 |
||
201 |
end |
|
202 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
203 |
lemma random_aux_rec: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
204 |
fixes random_aux :: "natural \<Rightarrow> 'a" |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
205 |
assumes "random_aux 0 = rhs 0" |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
206 |
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
|
207 |
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
|
208 |
using assms by (rule natural.induct) |
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
209 |
|
60758 | 210 |
subsection \<open>Deriving random generators for datatypes\<close> |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
211 |
|
69605 | 212 |
ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close> |
213 |
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
|
214 |
|
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
215 |
|
60758 | 216 |
subsection \<open>Code setup\<close> |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
32657
diff
changeset
|
217 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
218 |
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
|
219 |
constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun" |
69593 | 220 |
\<comment> \<open>With enough criminal energy this can be abused to derive \<^prop>\<open>False\<close>; |
61799 | 221 |
for this reason we use a distinguished target \<open>Quickcheck\<close> |
60758 | 222 |
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
|
223 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
224 |
code_reserved Quickcheck Random_Generators |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
225 |
|
37751 | 226 |
no_notation fcomp (infixl "\<circ>>" 60) |
227 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
68587
1148f63304f4
avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents:
67399
diff
changeset
|
228 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
229 |
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
|
230 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
231 |
hide_fact (open) collapse_def beyond_def random_fun_lift_def |
31267 | 232 |
|
31179 | 233 |
end |