author | wenzelm |
Fri, 05 Apr 2019 17:05:32 +0200 | |
changeset 70067 | 9b34dbeb1103 |
parent 69605 | a96320074298 |
child 72607 | feebdaa346e5 |
permissions | -rw-r--r-- |
62979 | 1 |
(* Title: HOL/Quickcheck_Exhaustive.thy |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
3 |
*) |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
4 |
|
60758 | 5 |
section \<open>A simple counterexample generator performing exhaustive testing\<close> |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
6 |
|
41918 | 7 |
theory Quickcheck_Exhaustive |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
49948
diff
changeset
|
8 |
imports Quickcheck_Random |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46417
diff
changeset
|
9 |
keywords "quickcheck_generator" :: thy_decl |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
10 |
begin |
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
11 |
|
62979 | 12 |
subsection \<open>Basic operations for exhaustive generators\<close> |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
13 |
|
62979 | 14 |
definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" (infixr "orelse" 55) |
15 |
where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)" |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
16 |
|
62979 | 17 |
|
18 |
subsection \<open>Exhaustive generator type classes\<close> |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
19 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
20 |
class exhaustive = term_of + |
62979 | 21 |
fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
22 |
||
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
23 |
class full_exhaustive = term_of + |
62979 | 24 |
fixes full_exhaustive :: |
25 |
"('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
26 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
27 |
instantiation natural :: full_exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
28 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
29 |
|
62979 | 30 |
function full_exhaustive_natural' :: |
31 |
"(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
32 |
natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
33 |
where "full_exhaustive_natural' f d i = |
42304 | 34 |
(if d < i then None |
62979 | 35 |
else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))" |
42304 | 36 |
by pat_completeness auto |
37 |
||
38 |
termination |
|
62979 | 39 |
by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) |
42304 | 40 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
41 |
definition "full_exhaustive f d = full_exhaustive_natural' f d 0" |
42304 | 42 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
43 |
instance .. |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
44 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
45 |
end |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
46 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
47 |
instantiation natural :: exhaustive |
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
48 |
begin |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
49 |
|
62979 | 50 |
function exhaustive_natural' :: |
51 |
"(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
52 |
where "exhaustive_natural' f d i = |
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
53 |
(if d < i then None |
62979 | 54 |
else (f i orelse exhaustive_natural' f d (i + 1)))" |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
55 |
by pat_completeness auto |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
56 |
|
42304 | 57 |
termination |
62979 | 58 |
by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
59 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
60 |
definition "exhaustive f d = exhaustive_natural' f d 0" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
61 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
62 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
63 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
64 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
65 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
66 |
instantiation integer :: exhaustive |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
67 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
68 |
|
62979 | 69 |
function exhaustive_integer' :: |
70 |
"(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option" |
|
71 |
where "exhaustive_integer' f d i = |
|
72 |
(if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
73 |
by pat_completeness auto |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
74 |
|
62979 | 75 |
termination |
76 |
by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))") |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
77 |
(auto simp add: less_integer_def nat_of_integer_def) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
78 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
79 |
definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
80 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
81 |
instance .. |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
82 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
83 |
end |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
84 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
85 |
instantiation integer :: full_exhaustive |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
86 |
begin |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
87 |
|
62979 | 88 |
function full_exhaustive_integer' :: |
89 |
"(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
90 |
integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option" |
|
91 |
where "full_exhaustive_integer' f d i = |
|
92 |
(if d < i then None |
|
93 |
else |
|
94 |
(case f (i, \<lambda>_. Code_Evaluation.term_of i) of |
|
95 |
Some t \<Rightarrow> Some t |
|
96 |
| None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
97 |
by pat_completeness auto |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
98 |
|
62979 | 99 |
termination |
100 |
by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))") |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
101 |
(auto simp add: less_integer_def nat_of_integer_def) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
102 |
|
62979 | 103 |
definition "full_exhaustive f d = |
104 |
full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" |
|
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
105 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
106 |
instance .. |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
107 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
108 |
end |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
109 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
110 |
instantiation nat :: exhaustive |
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
111 |
begin |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
112 |
|
62979 | 113 |
definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d" |
42304 | 114 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
115 |
instance .. |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
116 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
117 |
end |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
118 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
119 |
instantiation nat :: full_exhaustive |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
120 |
begin |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
121 |
|
62979 | 122 |
definition "full_exhaustive f d = |
123 |
full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. Code_Evaluation.term_of (nat_of_natural x))) d" |
|
41231
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
124 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
125 |
instance .. |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
126 |
|
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
127 |
end |
2e901158675e
adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents:
41178
diff
changeset
|
128 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
129 |
instantiation int :: exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
130 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
131 |
|
62979 | 132 |
function exhaustive_int' :: |
133 |
"(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option" |
|
134 |
where "exhaustive_int' f d i = |
|
135 |
(if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))" |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
136 |
by pat_completeness auto |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
137 |
|
62979 | 138 |
termination |
139 |
by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
140 |
|
62979 | 141 |
definition "exhaustive f d = |
142 |
exhaustive_int' f (int_of_integer (integer_of_natural d)) |
|
143 |
(- (int_of_integer (integer_of_natural d)))" |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
144 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
145 |
instance .. |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
146 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
147 |
end |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
148 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
149 |
instantiation int :: full_exhaustive |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
150 |
begin |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
151 |
|
62979 | 152 |
function full_exhaustive_int' :: |
153 |
"(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
154 |
int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option" |
|
155 |
where "full_exhaustive_int' f d i = |
|
156 |
(if d < i then None |
|
157 |
else |
|
158 |
(case f (i, \<lambda>_. Code_Evaluation.term_of i) of |
|
159 |
Some t \<Rightarrow> Some t |
|
160 |
| None \<Rightarrow> full_exhaustive_int' f d (i + 1)))" |
|
42304 | 161 |
by pat_completeness auto |
162 |
||
62979 | 163 |
termination |
164 |
by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto |
|
42304 | 165 |
|
62979 | 166 |
definition "full_exhaustive f d = |
167 |
full_exhaustive_int' f (int_of_integer (integer_of_natural d)) |
|
168 |
(- (int_of_integer (integer_of_natural d)))" |
|
42304 | 169 |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
170 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
171 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
172 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
173 |
|
41916
80060d5f864a
renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents:
41915
diff
changeset
|
174 |
instantiation prod :: (exhaustive, exhaustive) exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
175 |
begin |
40899
ef6fde932f4c
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents:
40639
diff
changeset
|
176 |
|
62979 | 177 |
definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d" |
42304 | 178 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
179 |
instance .. |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
180 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
181 |
end |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
182 |
|
62979 | 183 |
definition (in term_syntax) |
184 |
[code_unfold]: "valtermify_pair x y = |
|
185 |
Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y" |
|
46307
ec8f975c059b
shortened definitions by adding some termify constants
bulwahn
parents:
46305
diff
changeset
|
186 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
187 |
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
188 |
begin |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
189 |
|
62979 | 190 |
definition "full_exhaustive f d = |
191 |
full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d" |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
192 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
193 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
194 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
195 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
196 |
|
46193
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
197 |
instantiation set :: (exhaustive) exhaustive |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
198 |
begin |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
199 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
200 |
fun exhaustive_set |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
201 |
where |
62979 | 202 |
"exhaustive_set f i = |
203 |
(if i = 0 then None |
|
204 |
else |
|
205 |
f {} orelse |
|
206 |
exhaustive_set |
|
207 |
(\<lambda>A. f A orelse exhaustive (\<lambda>x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1))" |
|
46193
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
208 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
209 |
instance .. |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
210 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
211 |
end |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
212 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
213 |
instantiation set :: (full_exhaustive) full_exhaustive |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
214 |
begin |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
215 |
|
62979 | 216 |
fun full_exhaustive_set |
46193
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
217 |
where |
62979 | 218 |
"full_exhaustive_set f i = |
219 |
(if i = 0 then None |
|
220 |
else |
|
221 |
f valterm_emptyset orelse |
|
222 |
full_exhaustive_set |
|
223 |
(\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive |
|
224 |
(\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))" |
|
46193
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
225 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
226 |
instance .. |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
227 |
|
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
228 |
end |
55a4769d0abe
adding exhaustive instances for type constructor set
bulwahn
parents:
45925
diff
changeset
|
229 |
|
62979 | 230 |
instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive |
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
231 |
begin |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
232 |
|
62979 | 233 |
fun exhaustive_fun' :: |
234 |
"(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
42304 | 235 |
where |
62979 | 236 |
"exhaustive_fun' f i d = |
237 |
(exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse |
|
238 |
(if i > 1 then |
|
239 |
exhaustive_fun' |
|
240 |
(\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)" |
|
42304 | 241 |
|
62979 | 242 |
definition exhaustive_fun :: |
243 |
"(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
244 |
where "exhaustive_fun f d = exhaustive_fun' f d d" |
|
42304 | 245 |
|
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
246 |
instance .. |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
247 |
|
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
248 |
end |
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
249 |
|
62979 | 250 |
definition [code_unfold]: |
251 |
"valtermify_absdummy = |
|
252 |
(\<lambda>(v, t). |
|
253 |
(\<lambda>_::'a. v, |
|
254 |
\<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))" |
|
46307
ec8f975c059b
shortened definitions by adding some termify constants
bulwahn
parents:
46305
diff
changeset
|
255 |
|
62979 | 256 |
definition (in term_syntax) |
257 |
[code_unfold]: "valtermify_fun_upd g a b = |
|
258 |
Code_Evaluation.valtermify |
|
259 |
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b" |
|
46307
ec8f975c059b
shortened definitions by adding some termify constants
bulwahn
parents:
46305
diff
changeset
|
260 |
|
62979 | 261 |
instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive |
42310
c664cc5cc5e9
splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents:
42305
diff
changeset
|
262 |
begin |
42304 | 263 |
|
62979 | 264 |
fun full_exhaustive_fun' :: |
265 |
"(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
266 |
natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" |
|
42304 | 267 |
where |
62979 | 268 |
"full_exhaustive_fun' f i d = |
269 |
full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse |
|
270 |
(if i > 1 then |
|
271 |
full_exhaustive_fun' |
|
272 |
(\<lambda>g. full_exhaustive |
|
273 |
(\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d |
|
274 |
else None)" |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
275 |
|
62979 | 276 |
definition full_exhaustive_fun :: |
277 |
"(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
278 |
natural \<Rightarrow> (bool \<times> term list) option" |
|
279 |
where "full_exhaustive_fun f d = full_exhaustive_fun' f d d" |
|
40639
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
280 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
281 |
instance .. |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
282 |
|
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
283 |
end |
f1f0e6adca0a
adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents:
40620
diff
changeset
|
284 |
|
60758 | 285 |
subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close> |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
286 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
287 |
class check_all = enum + term_of + |
62979 | 288 |
fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option" |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
289 |
fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list" |
62979 | 290 |
|
291 |
fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow> |
|
292 |
(bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
293 |
where |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
294 |
"check_all_n_lists f n = |
62979 | 295 |
(if n = 0 then f ([], (\<lambda>_. [])) |
296 |
else check_all (\<lambda>(x, xt). |
|
297 |
check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))" |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
298 |
|
62979 | 299 |
definition (in term_syntax) |
300 |
[code_unfold]: "termify_fun_upd g a b = |
|
301 |
(Code_Evaluation.termify |
|
302 |
(fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)" |
|
46307
ec8f975c059b
shortened definitions by adding some termify constants
bulwahn
parents:
46305
diff
changeset
|
303 |
|
62979 | 304 |
definition mk_map_term :: |
305 |
"(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> |
|
306 |
(unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term" |
|
307 |
where "mk_map_term T1 T2 domm rng = |
|
308 |
(\<lambda>_. |
|
309 |
let |
|
310 |
T1 = T1 (); |
|
311 |
T2 = T2 (); |
|
312 |
update_term = |
|
313 |
(\<lambda>g (a, b). |
|
314 |
Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App |
|
315 |
(Code_Evaluation.Const (STR ''Fun.fun_upd'') |
|
316 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], |
|
317 |
Typerep.Typerep (STR ''fun'') [T1, |
|
318 |
Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) |
|
319 |
g) a) b) |
|
320 |
in |
|
321 |
List.foldl update_term |
|
322 |
(Code_Evaluation.Abs (STR ''x'') T1 |
|
323 |
(Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
324 |
|
62979 | 325 |
instantiation "fun" :: ("{equal,check_all}", check_all) check_all |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
326 |
begin |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
327 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
328 |
definition |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
329 |
"check_all f = |
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
330 |
(let |
62979 | 331 |
mk_term = |
332 |
mk_map_term |
|
333 |
(\<lambda>_. Typerep.typerep (TYPE('a))) |
|
334 |
(\<lambda>_. Typerep.typerep (TYPE('b))) |
|
335 |
(enum_term_of (TYPE('a))); |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
336 |
enum = (Enum.enum :: 'a list) |
62979 | 337 |
in |
338 |
check_all_n_lists |
|
67091 | 339 |
(\<lambda>(ys, yst). f (the \<circ> map_of (zip enum ys), mk_term yst)) |
62979 | 340 |
(natural_of_nat (length enum)))" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
341 |
|
62979 | 342 |
definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list" |
343 |
where "enum_term_of_fun = |
|
344 |
(\<lambda>_ _. |
|
345 |
let |
|
346 |
enum_term_of_a = enum_term_of (TYPE('a)); |
|
347 |
mk_term = |
|
348 |
mk_map_term |
|
349 |
(\<lambda>_. Typerep.typerep (TYPE('a))) |
|
350 |
(\<lambda>_. Typerep.typerep (TYPE('b))) |
|
351 |
enum_term_of_a |
|
352 |
in |
|
353 |
map (\<lambda>ys. mk_term (\<lambda>_. ys) ()) |
|
354 |
(List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" |
|
355 |
||
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
356 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
357 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
358 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
359 |
|
62979 | 360 |
fun (in term_syntax) check_all_subsets :: |
361 |
"(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> |
|
362 |
('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option" |
|
46305 | 363 |
where |
364 |
"check_all_subsets f [] = f valterm_emptyset" |
|
62979 | 365 |
| "check_all_subsets f (x # xs) = |
366 |
check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs" |
|
46305 | 367 |
|
368 |
||
62979 | 369 |
definition (in term_syntax) |
370 |
[code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)" |
|
46305 | 371 |
|
62979 | 372 |
definition (in term_syntax) |
373 |
[code_unfold]: "termify_insert x s = |
|
374 |
Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set) <\<cdot>> x <\<cdot>> s" |
|
375 |
||
376 |
definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term" |
|
46305 | 377 |
where |
62979 | 378 |
"setify T ts = foldr (termify_insert T) ts (term_emptyset T)" |
46305 | 379 |
|
380 |
instantiation set :: (check_all) check_all |
|
381 |
begin |
|
382 |
||
383 |
definition |
|
384 |
"check_all_set f = |
|
62979 | 385 |
check_all_subsets f |
386 |
(zip (Enum.enum :: 'a list) |
|
387 |
(map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))" |
|
46305 | 388 |
|
62979 | 389 |
definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list" |
390 |
where "enum_term_of_set _ _ = |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
64670
diff
changeset
|
391 |
map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))" |
46305 | 392 |
|
393 |
instance .. |
|
394 |
||
395 |
end |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
396 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
397 |
instantiation unit :: check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
398 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
399 |
|
62979 | 400 |
definition "check_all f = f (Code_Evaluation.valtermify ())" |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
401 |
|
62979 | 402 |
definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list" |
403 |
where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
404 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
405 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
406 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
407 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
408 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
409 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
410 |
instantiation bool :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
411 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
412 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
413 |
definition |
62979 | 414 |
"check_all f = |
415 |
(case f (Code_Evaluation.valtermify False) of |
|
416 |
Some x' \<Rightarrow> Some x' |
|
417 |
| None \<Rightarrow> f (Code_Evaluation.valtermify True))" |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
418 |
|
62979 | 419 |
definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list" |
420 |
where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
421 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
422 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
423 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
424 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
425 |
|
62979 | 426 |
definition (in term_syntax) [code_unfold]: |
427 |
"termify_pair x y = |
|
428 |
Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y" |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
429 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
430 |
instantiation prod :: (check_all, check_all) check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
431 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
432 |
|
62979 | 433 |
definition "check_all f = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
434 |
|
62979 | 435 |
definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list" |
436 |
where "enum_term_of_prod = |
|
437 |
(\<lambda>_ _. |
|
438 |
map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y) |
|
439 |
(List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
440 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
441 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
442 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
443 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
444 |
|
62979 | 445 |
definition (in term_syntax) |
446 |
[code_unfold]: "valtermify_Inl x = |
|
447 |
Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x" |
|
448 |
||
449 |
definition (in term_syntax) |
|
450 |
[code_unfold]: "valtermify_Inr x = |
|
451 |
Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x" |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
452 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
453 |
instantiation sum :: (check_all, check_all) check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
454 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
455 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
456 |
definition |
62979 | 457 |
"check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))" |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
458 |
|
62979 | 459 |
definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list" |
460 |
where "enum_term_of_sum = |
|
461 |
(\<lambda>_ _. |
|
462 |
let |
|
463 |
T1 = Typerep.typerep (TYPE('a)); |
|
464 |
T2 = Typerep.typerep (TYPE('b)) |
|
465 |
in |
|
466 |
map |
|
467 |
(Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') |
|
468 |
(Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) |
|
469 |
(enum_term_of (TYPE('a)) ()) @ |
|
470 |
map |
|
471 |
(Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') |
|
472 |
(Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) |
|
473 |
(enum_term_of (TYPE('b)) ()))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
474 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
475 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
476 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
477 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
478 |
|
64670
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
479 |
instantiation char :: check_all |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
480 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
481 |
|
64670
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
482 |
primrec check_all_char' :: |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
483 |
"(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option" |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
484 |
where "check_all_char' f [] = None" |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
485 |
| "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c) |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
486 |
orelse check_all_char' f cs" |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
487 |
|
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
488 |
definition check_all_char :: |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
489 |
"(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option" |
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
490 |
where "check_all f = check_all_char' f Enum.enum" |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
491 |
|
62979 | 492 |
definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list" |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
493 |
where |
62979 | 494 |
"enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))" |
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
495 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
496 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
497 |
|
64670
f77b946d18aa
restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents:
62979
diff
changeset
|
498 |
end |
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
499 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
500 |
instantiation option :: (check_all) check_all |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
501 |
begin |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
502 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
503 |
definition |
62979 | 504 |
"check_all f = |
505 |
f (Code_Evaluation.valtermify (None :: 'a option)) orelse |
|
506 |
check_all |
|
507 |
(\<lambda>(x, t). |
|
508 |
f |
|
509 |
(Some x, |
|
510 |
\<lambda>_. Code_Evaluation.App |
|
511 |
(Code_Evaluation.Const (STR ''Option.option.Some'') |
|
512 |
(Typerep.Typerep (STR ''fun'') |
|
513 |
[Typerep.typerep TYPE('a), |
|
514 |
Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))" |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
515 |
|
62979 | 516 |
definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list" |
517 |
where "enum_term_of_option = |
|
518 |
(\<lambda> _ _. |
|
519 |
Code_Evaluation.term_of (None :: 'a option) # |
|
520 |
(map |
|
521 |
(Code_Evaluation.App |
|
522 |
(Code_Evaluation.Const (STR ''Option.option.Some'') |
|
523 |
(Typerep.Typerep (STR ''fun'') |
|
524 |
[Typerep.typerep TYPE('a), |
|
525 |
Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) |
|
526 |
(enum_term_of (TYPE('a)) ())))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
527 |
|
41105
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
528 |
instance .. |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
529 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
530 |
end |
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
531 |
|
a76ee71c3313
adding check_all instances for a few more finite types in smallcheck
bulwahn
parents:
41104
diff
changeset
|
532 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
533 |
instantiation Enum.finite_1 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
534 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
535 |
|
62979 | 536 |
definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)" |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
537 |
|
62979 | 538 |
definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list" |
539 |
where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
540 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
541 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
542 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
543 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
544 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
545 |
instantiation Enum.finite_2 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
546 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
547 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
548 |
definition |
62979 | 549 |
"check_all f = |
550 |
(f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse |
|
551 |
f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))" |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
552 |
|
62979 | 553 |
definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list" |
554 |
where "enum_term_of_finite_2 = |
|
555 |
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
556 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
557 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
558 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
559 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
560 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
561 |
instantiation Enum.finite_3 :: check_all |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
562 |
begin |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
563 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
564 |
definition |
62979 | 565 |
"check_all f = |
566 |
(f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse |
|
567 |
f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse |
|
568 |
f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))" |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
569 |
|
62979 | 570 |
definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list" |
571 |
where "enum_term_of_finite_3 = |
|
572 |
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" |
|
41177
810a885decee
added enum_term_of to correct present nested functions
bulwahn
parents:
41105
diff
changeset
|
573 |
|
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
574 |
instance .. |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
575 |
|
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
576 |
end |
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
577 |
|
46417
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
578 |
instantiation Enum.finite_4 :: check_all |
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
579 |
begin |
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
580 |
|
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
581 |
definition |
62979 | 582 |
"check_all f = |
583 |
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse |
|
584 |
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse |
|
585 |
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse |
|
586 |
f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)" |
|
46417
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
587 |
|
62979 | 588 |
definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list" |
589 |
where "enum_term_of_finite_4 = |
|
590 |
(\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))" |
|
46417
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
591 |
|
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
592 |
instance .. |
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
593 |
|
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
594 |
end |
1a68fcb80b62
beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents:
46311
diff
changeset
|
595 |
|
60758 | 596 |
subsection \<open>Bounded universal quantifiers\<close> |
41085
a549ff1d4070
adding a smarter enumeration scheme for finite functions
bulwahn
parents:
40915
diff
changeset
|
597 |
|
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42117
diff
changeset
|
598 |
class bounded_forall = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
599 |
fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool" |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42117
diff
changeset
|
600 |
|
62979 | 601 |
|
60758 | 602 |
subsection \<open>Fast exhaustive combinators\<close> |
42305
494c31fdec95
theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents:
42304
diff
changeset
|
603 |
|
494c31fdec95
theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents:
42304
diff
changeset
|
604 |
class fast_exhaustive = term_of + |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
605 |
fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit" |
42305
494c31fdec95
theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents:
42304
diff
changeset
|
606 |
|
62979 | 607 |
axiomatization throw_Counterexample :: "term list \<Rightarrow> unit" |
608 |
axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option" |
|
42305
494c31fdec95
theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents:
42304
diff
changeset
|
609 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
610 |
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
|
611 |
constant throw_Counterexample \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
612 |
(Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51143
diff
changeset
|
613 |
| constant catch_Counterexample \<rightharpoonup> |
62979 | 614 |
(Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)" |
615 |
||
42305
494c31fdec95
theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents:
42304
diff
changeset
|
616 |
|
60758 | 617 |
subsection \<open>Continuation passing style functions as plus monad\<close> |
62979 | 618 |
|
619 |
type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option" |
|
45450 | 620 |
|
621 |
definition cps_empty :: "'a cps" |
|
62979 | 622 |
where "cps_empty = (\<lambda>cont. None)" |
45450 | 623 |
|
62979 | 624 |
definition cps_single :: "'a \<Rightarrow> 'a cps" |
625 |
where "cps_single v = (\<lambda>cont. cont v)" |
|
45450 | 626 |
|
62979 | 627 |
definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps" |
628 |
where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))" |
|
45450 | 629 |
|
62979 | 630 |
definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps" |
631 |
where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)" |
|
632 |
||
633 |
definition cps_if :: "bool \<Rightarrow> unit cps" |
|
634 |
where "cps_if b = (if b then cps_single () else cps_empty)" |
|
45450 | 635 |
|
62979 | 636 |
definition cps_not :: "unit cps \<Rightarrow> unit cps" |
637 |
where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)" |
|
45450 | 638 |
|
62979 | 639 |
type_synonym 'a pos_bound_cps = |
640 |
"('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" |
|
45450 | 641 |
|
642 |
definition pos_bound_cps_empty :: "'a pos_bound_cps" |
|
62979 | 643 |
where "pos_bound_cps_empty = (\<lambda>cont i. None)" |
45450 | 644 |
|
62979 | 645 |
definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps" |
646 |
where "pos_bound_cps_single v = (\<lambda>cont i. cont v)" |
|
45450 | 647 |
|
62979 | 648 |
definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps" |
649 |
where "pos_bound_cps_bind m f = (\<lambda>cont i. if i = 0 then None else (m (\<lambda>a. (f a) cont i) (i - 1)))" |
|
45450 | 650 |
|
62979 | 651 |
definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps" |
652 |
where "pos_bound_cps_plus a b = (\<lambda>c i. case a c i of None \<Rightarrow> b c i | Some x \<Rightarrow> Some x)" |
|
45450 | 653 |
|
62979 | 654 |
definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps" |
655 |
where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" |
|
45450 | 656 |
|
58350
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
657 |
datatype (plugins only: code extraction) (dead 'a) unknown = |
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
658 |
Unknown | Known 'a |
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
659 |
|
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
660 |
datatype (plugins only: code extraction) (dead 'a) three_valued = |
919149921e46
added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents:
58334
diff
changeset
|
661 |
Unknown_value | Value 'a | No_value |
45450 | 662 |
|
62979 | 663 |
type_synonym 'a neg_bound_cps = |
664 |
"('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued" |
|
45450 | 665 |
|
666 |
definition neg_bound_cps_empty :: "'a neg_bound_cps" |
|
62979 | 667 |
where "neg_bound_cps_empty = (\<lambda>cont i. No_value)" |
668 |
||
669 |
definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps" |
|
670 |
where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))" |
|
45450 | 671 |
|
62979 | 672 |
definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps" |
673 |
where "neg_bound_cps_bind m f = |
|
674 |
(\<lambda>cont i. |
|
675 |
if i = 0 then cont Unknown |
|
676 |
else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))" |
|
45450 | 677 |
|
62979 | 678 |
definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps" |
679 |
where "neg_bound_cps_plus a b = |
|
680 |
(\<lambda>c i. |
|
681 |
case a c i of |
|
682 |
No_value \<Rightarrow> b c i |
|
683 |
| Value x \<Rightarrow> Value x |
|
684 |
| Unknown_value \<Rightarrow> |
|
685 |
(case b c i of |
|
686 |
No_value \<Rightarrow> Unknown_value |
|
687 |
| Value x \<Rightarrow> Value x |
|
688 |
| Unknown_value \<Rightarrow> Unknown_value))" |
|
45450 | 689 |
|
62979 | 690 |
definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps" |
691 |
where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)" |
|
45450 | 692 |
|
62979 | 693 |
definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps" |
694 |
where "neg_bound_cps_not n = |
|
695 |
(\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)" |
|
696 |
||
697 |
definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps" |
|
698 |
where "pos_bound_cps_not n = |
|
699 |
(\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)" |
|
700 |
||
45450 | 701 |
|
60758 | 702 |
subsection \<open>Defining generators for any first-order data type\<close> |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
703 |
|
45697
3b7c35a08723
more stable introduction of the internally used unknown term
bulwahn
parents:
45684
diff
changeset
|
704 |
axiomatization unknown :: 'a |
3b7c35a08723
more stable introduction of the internally used unknown term
bulwahn
parents:
45684
diff
changeset
|
705 |
|
3b7c35a08723
more stable introduction of the internally used unknown term
bulwahn
parents:
45684
diff
changeset
|
706 |
notation (output) unknown ("?") |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
707 |
|
69605 | 708 |
ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close> |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
709 |
|
43882
05d5696f177f
renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents:
42310
diff
changeset
|
710 |
declare [[quickcheck_batch_tester = exhaustive]] |
40915
a4c956d1f91f
declaring quickcheck testers as default after their setup
bulwahn
parents:
40914
diff
changeset
|
711 |
|
62979 | 712 |
|
60758 | 713 |
subsection \<open>Defining generators for abstract types\<close> |
45925 | 714 |
|
69605 | 715 |
ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close> |
45925 | 716 |
|
47203 | 717 |
hide_fact (open) orelse_def |
62979 | 718 |
no_notation orelse (infixr "orelse" 55) |
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45750
diff
changeset
|
719 |
|
62979 | 720 |
hide_const valtermify_absdummy valtermify_fun_upd |
721 |
valterm_emptyset valtermify_insert |
|
722 |
valtermify_pair valtermify_Inl valtermify_Inr |
|
46307
ec8f975c059b
shortened definitions by adding some termify constants
bulwahn
parents:
46305
diff
changeset
|
723 |
termify_fun_upd term_emptyset termify_insert termify_pair setify |
46305 | 724 |
|
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45750
diff
changeset
|
725 |
hide_const (open) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
726 |
exhaustive full_exhaustive |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
727 |
exhaustive_int' full_exhaustive_int' |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
728 |
exhaustive_integer' full_exhaustive_integer' |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
729 |
exhaustive_natural' full_exhaustive_natural' |
45818
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45750
diff
changeset
|
730 |
throw_Counterexample catch_Counterexample |
53a697f5454a
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents:
45750
diff
changeset
|
731 |
check_all enum_term_of |
46305 | 732 |
orelse unknown mk_map_term check_all_n_lists check_all_subsets |
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff
changeset
|
733 |
|
45450 | 734 |
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued |
62979 | 735 |
|
45450 | 736 |
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not |
62979 | 737 |
pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind |
738 |
pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not |
|
739 |
neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind |
|
740 |
neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not |
|
45450 | 741 |
Unknown Known Unknown_value Value No_value |
742 |
||
743 |
end |