equal
deleted
inserted
replaced
2 |
2 |
3 header {* A simple counterexample generator performing random testing *} |
3 header {* A simple counterexample generator performing random testing *} |
4 |
4 |
5 theory Quickcheck |
5 theory Quickcheck |
6 imports Random Code_Evaluation Enum |
6 imports Random Code_Evaluation Enum |
7 uses |
|
8 ("Tools/Quickcheck/quickcheck_common.ML") |
|
9 ("Tools/Quickcheck/random_generators.ML") |
|
10 begin |
7 begin |
11 |
8 |
12 notation fcomp (infixl "\<circ>>" 60) |
9 notation fcomp (infixl "\<circ>>" 60) |
13 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
10 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
14 |
11 |
180 shows "random_aux k = rhs k" |
177 shows "random_aux k = rhs k" |
181 using assms by (rule code_numeral.induct) |
178 using assms by (rule code_numeral.induct) |
182 |
179 |
183 subsection {* Deriving random generators for datatypes *} |
180 subsection {* Deriving random generators for datatypes *} |
184 |
181 |
185 use "Tools/Quickcheck/quickcheck_common.ML" |
182 ML_file "Tools/Quickcheck/quickcheck_common.ML" |
186 use "Tools/Quickcheck/random_generators.ML" |
183 ML_file "Tools/Quickcheck/random_generators.ML" |
187 setup Random_Generators.setup |
184 setup Random_Generators.setup |
188 |
185 |
189 |
186 |
190 subsection {* Code setup *} |
187 subsection {* Code setup *} |
191 |
188 |