author | haftmann |
Thu, 14 Feb 2013 15:27:10 +0100 | |
changeset 51126 | df86080de4cb |
parent 50046 | src/HOL/Quickcheck.thy@0051dc4f301f |
child 51143 | 0a2371e7ced3 |
permissions | -rw-r--r-- |
41922 | 1 |
(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *) |
26265 | 2 |
|
41922 | 3 |
header {* A simple counterexample generator performing random testing *} |
26265 | 4 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
5 |
theory Quickcheck_Random |
40650
d40b347d5b0b
adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents:
38857
diff
changeset
|
6 |
imports Random Code_Evaluation Enum |
26265 | 7 |
begin |
8 |
||
37751 | 9 |
notation fcomp (infixl "\<circ>>" 60) |
10 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
31179 | 11 |
|
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
12 |
setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} |
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
13 |
|
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
14 |
subsection {* Catching Match exceptions *} |
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
15 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
16 |
axiomatization catch_match :: "'a => 'a => 'a" |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
17 |
|
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
18 |
code_const catch_match |
48273 | 19 |
(Quickcheck "((_) handle Match => _)") |
31179 | 20 |
|
26265 | 21 |
subsection {* The @{text random} class *} |
22 |
||
28335 | 23 |
class random = typerep + |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
24 |
fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
26265 | 25 |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset
|
26 |
|
31260 | 27 |
subsection {* Fundamental and numeric types*} |
31179 | 28 |
|
29 |
instantiation bool :: random |
|
30 |
begin |
|
31 |
||
32 |
definition |
|
37751 | 33 |
"random i = Random.range 2 \<circ>\<rightarrow> |
32657 | 34 |
(\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" |
31179 | 35 |
|
36 |
instance .. |
|
37 |
||
38 |
end |
|
39 |
||
40 |
instantiation itself :: (typerep) random |
|
41 |
begin |
|
42 |
||
46975 | 43 |
definition |
44 |
random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
|
45 |
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" |
|
31179 | 46 |
|
47 |
instance .. |
|
48 |
||
49 |
end |
|
50 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
51 |
instantiation char :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
52 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
53 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
54 |
definition |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
48891
diff
changeset
|
55 |
"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
|
56 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
57 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
58 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
59 |
end |
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 |
instantiation String.literal :: random |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
62 |
begin |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
63 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
64 |
definition |
32657 | 65 |
"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
|
66 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
67 |
instance .. |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
68 |
|
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
69 |
end |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
70 |
|
31179 | 71 |
instantiation nat :: random |
72 |
begin |
|
73 |
||
46975 | 74 |
definition random_nat :: "code_numeral \<Rightarrow> Random.seed |
75 |
\<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" |
|
76 |
where |
|
37751 | 77 |
"random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
78 |
let n = Code_Numeral.nat_of k |
32657 | 79 |
in (n, \<lambda>_. Code_Evaluation.term_of n)))" |
31194 | 80 |
|
81 |
instance .. |
|
82 |
||
83 |
end |
|
84 |
||
85 |
instantiation int :: random |
|
86 |
begin |
|
87 |
||
88 |
definition |
|
37751 | 89 |
"random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
90 |
let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k)) |
32657 | 91 |
in (j, \<lambda>_. Code_Evaluation.term_of j)))" |
31179 | 92 |
|
93 |
instance .. |
|
94 |
||
30945 | 95 |
end |
31179 | 96 |
|
31260 | 97 |
|
98 |
subsection {* Complex generators *} |
|
99 |
||
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
100 |
text {* Towards @{typ "'a \<Rightarrow> 'b"} *} |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
101 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
102 |
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) |
46975 | 103 |
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
104 |
\<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) |
|
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
105 |
\<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
|
106 |
|
31622 | 107 |
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) |
46975 | 108 |
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
109 |
where |
|
110 |
"random_fun_lift f = |
|
111 |
random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed" |
|
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
112 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37751
diff
changeset
|
113 |
instantiation "fun" :: ("{equal, term_of}", random) random |
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
114 |
begin |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
115 |
|
46975 | 116 |
definition |
117 |
random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
|
118 |
where "random i = random_fun_lift (random i)" |
|
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
119 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
120 |
instance .. |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
121 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
122 |
end |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
123 |
|
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
124 |
text {* Towards type copies and datatypes *} |
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset
|
125 |
|
46975 | 126 |
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" |
127 |
where "collapse f = (f \<circ>\<rightarrow> id)" |
|
31223
87bde6b5f793
re-added corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset
|
128 |
|
46975 | 129 |
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
130 |
where "beyond k l = (if l > k then l else 0)" |
|
31260 | 131 |
|
46975 | 132 |
lemma beyond_zero: "beyond k 0 = 0" |
31267 | 133 |
by (simp add: beyond_def) |
134 |
||
46311 | 135 |
|
46975 | 136 |
definition (in term_syntax) [code_unfold]: |
137 |
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" |
|
138 |
||
139 |
definition (in term_syntax) [code_unfold]: |
|
140 |
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" |
|
46311 | 141 |
|
142 |
instantiation set :: (random) random |
|
143 |
begin |
|
144 |
||
145 |
primrec random_aux_set |
|
146 |
where |
|
147 |
"random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])" |
|
46975 | 148 |
| "random_aux_set (Code_Numeral.Suc i) j = |
149 |
collapse (Random.select_weight |
|
150 |
[(1, Pair valterm_emptyset), |
|
151 |
(Code_Numeral.Suc i, |
|
152 |
random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" |
|
46311 | 153 |
|
154 |
lemma [code]: |
|
46975 | 155 |
"random_aux_set i j = |
156 |
collapse (Random.select_weight [(1, Pair valterm_emptyset), |
|
157 |
(i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" |
|
46311 | 158 |
proof (induct i rule: code_numeral.induct) |
159 |
case zero |
|
50046 | 160 |
show ?case by (subst select_weight_drop_zero [symmetric]) |
161 |
(simp add: random_aux_set.simps [simplified]) |
|
46311 | 162 |
next |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
163 |
case (Suc i) |
50046 | 164 |
show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one) |
46311 | 165 |
qed |
166 |
||
46975 | 167 |
definition "random_set i = random_aux_set i i" |
46311 | 168 |
|
169 |
instance .. |
|
170 |
||
171 |
end |
|
172 |
||
31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
173 |
lemma random_aux_rec: |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
174 |
fixes random_aux :: "code_numeral \<Rightarrow> 'a" |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
175 |
assumes "random_aux 0 = rhs 0" |
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset
|
176 |
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
|
177 |
shows "random_aux k = rhs k" |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
178 |
using assms by (rule code_numeral.induct) |
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset
|
179 |
|
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
180 |
subsection {* Deriving random generators for datatypes *} |
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset
|
181 |
|
48891 | 182 |
ML_file "Tools/Quickcheck/quickcheck_common.ML" |
183 |
ML_file "Tools/Quickcheck/random_generators.ML" |
|
41923
f05fc0711bc7
renaming signatures and structures; correcting header
bulwahn
parents:
41922
diff
changeset
|
184 |
setup Random_Generators.setup |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
185 |
|
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
186 |
|
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
187 |
subsection {* Code setup *} |
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
32657
diff
changeset
|
188 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
189 |
code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun") |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
190 |
-- {* With enough criminal energy this can be abused to derive @{prop False}; |
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
191 |
for this reason we use a distinguished target @{text Quickcheck} |
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
192 |
not spoiling the regular trusted code generation *} |
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
193 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset
|
194 |
code_reserved Quickcheck Random_Generators |
34968
ceeffca32eb0
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset
|
195 |
|
37751 | 196 |
no_notation fcomp (infixl "\<circ>>" 60) |
197 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
198 |
|
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset
|
199 |
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
|
200 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50046
diff
changeset
|
201 |
hide_fact (open) collapse_def beyond_def random_fun_lift_def |
31267 | 202 |
|
31179 | 203 |
end |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
48891
diff
changeset
|
204 |