bulwahn@42776
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen *)
|
bulwahn@42776
|
2 |
|
bulwahn@44227
|
3 |
header {* Counterexample generator performing narrowing-based testing *}
|
bulwahn@42776
|
4 |
|
bulwahn@42801
|
5 |
theory Quickcheck_Narrowing
|
bulwahn@44183
|
6 |
imports Quickcheck_Exhaustive
|
bulwahn@42833
|
7 |
uses
|
wenzelm@44576
|
8 |
("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
|
wenzelm@44576
|
9 |
("Tools/Quickcheck/Narrowing_Engine.hs")
|
wenzelm@44576
|
10 |
("Tools/Quickcheck/narrowing_generators.ML")
|
bulwahn@42776
|
11 |
begin
|
bulwahn@42776
|
12 |
|
bulwahn@42776
|
13 |
subsection {* Counterexample generator *}
|
bulwahn@42776
|
14 |
|
bulwahn@44179
|
15 |
text {* We create a new target for the necessary code generation setup. *}
|
bulwahn@44179
|
16 |
|
bulwahn@44179
|
17 |
setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
|
bulwahn@44179
|
18 |
|
bulwahn@42780
|
19 |
subsubsection {* Code generation setup *}
|
bulwahn@42780
|
20 |
|
bulwahn@42780
|
21 |
code_type typerep
|
bulwahn@44179
|
22 |
(Haskell_Quickcheck "Typerep")
|
bulwahn@42780
|
23 |
|
bulwahn@42780
|
24 |
code_const Typerep.Typerep
|
bulwahn@44179
|
25 |
(Haskell_Quickcheck "Typerep")
|
bulwahn@42780
|
26 |
|
bulwahn@44179
|
27 |
code_reserved Haskell_Quickcheck Typerep
|
bulwahn@42780
|
28 |
|
hoelzl@44198
|
29 |
subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
|
bulwahn@42779
|
30 |
|
bulwahn@42779
|
31 |
typedef (open) code_int = "UNIV \<Colon> int set"
|
bulwahn@42779
|
32 |
morphisms int_of of_int by rule
|
bulwahn@42779
|
33 |
|
bulwahn@42892
|
34 |
lemma of_int_int_of [simp]:
|
bulwahn@42892
|
35 |
"of_int (int_of k) = k"
|
bulwahn@42892
|
36 |
by (rule int_of_inverse)
|
bulwahn@42892
|
37 |
|
bulwahn@42892
|
38 |
lemma int_of_of_int [simp]:
|
bulwahn@42892
|
39 |
"int_of (of_int n) = n"
|
bulwahn@42892
|
40 |
by (rule of_int_inverse) (rule UNIV_I)
|
bulwahn@42892
|
41 |
|
bulwahn@42892
|
42 |
lemma code_int:
|
bulwahn@42892
|
43 |
"(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))"
|
bulwahn@42892
|
44 |
proof
|
bulwahn@42892
|
45 |
fix n :: int
|
bulwahn@42892
|
46 |
assume "\<And>n\<Colon>code_int. PROP P n"
|
bulwahn@42892
|
47 |
then show "PROP P (of_int n)" .
|
bulwahn@42892
|
48 |
next
|
bulwahn@42892
|
49 |
fix n :: code_int
|
bulwahn@42892
|
50 |
assume "\<And>n\<Colon>int. PROP P (of_int n)"
|
bulwahn@42892
|
51 |
then have "PROP P (of_int (int_of n))" .
|
bulwahn@42892
|
52 |
then show "PROP P n" by simp
|
bulwahn@42892
|
53 |
qed
|
bulwahn@42892
|
54 |
|
bulwahn@42892
|
55 |
|
bulwahn@42779
|
56 |
lemma int_of_inject [simp]:
|
bulwahn@42779
|
57 |
"int_of k = int_of l \<longleftrightarrow> k = l"
|
bulwahn@42779
|
58 |
by (rule int_of_inject)
|
bulwahn@42779
|
59 |
|
bulwahn@42892
|
60 |
lemma of_int_inject [simp]:
|
bulwahn@42892
|
61 |
"of_int n = of_int m \<longleftrightarrow> n = m"
|
bulwahn@42892
|
62 |
by (rule of_int_inject) (rule UNIV_I)+
|
bulwahn@42892
|
63 |
|
bulwahn@42892
|
64 |
instantiation code_int :: equal
|
bulwahn@42892
|
65 |
begin
|
bulwahn@42892
|
66 |
|
bulwahn@42892
|
67 |
definition
|
bulwahn@42892
|
68 |
"HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)"
|
bulwahn@42892
|
69 |
|
bulwahn@42892
|
70 |
instance proof
|
bulwahn@42892
|
71 |
qed (auto simp add: equal_code_int_def equal_int_def eq_int_refl)
|
bulwahn@42892
|
72 |
|
bulwahn@42892
|
73 |
end
|
bulwahn@42892
|
74 |
|
bulwahn@42892
|
75 |
instantiation code_int :: number
|
bulwahn@42892
|
76 |
begin
|
bulwahn@42892
|
77 |
|
bulwahn@42892
|
78 |
definition
|
bulwahn@42892
|
79 |
"number_of = of_int"
|
bulwahn@42892
|
80 |
|
bulwahn@42892
|
81 |
instance ..
|
bulwahn@42892
|
82 |
|
bulwahn@42892
|
83 |
end
|
bulwahn@42892
|
84 |
|
bulwahn@42892
|
85 |
lemma int_of_number [simp]:
|
bulwahn@42892
|
86 |
"int_of (number_of k) = number_of k"
|
bulwahn@42892
|
87 |
by (simp add: number_of_code_int_def number_of_is_id)
|
bulwahn@42892
|
88 |
|
bulwahn@42892
|
89 |
|
bulwahn@42783
|
90 |
definition nat_of :: "code_int => nat"
|
bulwahn@42783
|
91 |
where
|
bulwahn@42783
|
92 |
"nat_of i = nat (int_of i)"
|
bulwahn@42779
|
93 |
|
bulwahn@43821
|
94 |
|
bulwahn@43888
|
95 |
code_datatype "number_of \<Colon> int \<Rightarrow> code_int"
|
bulwahn@43821
|
96 |
|
bulwahn@43821
|
97 |
|
bulwahn@42892
|
98 |
instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
|
bulwahn@42779
|
99 |
begin
|
bulwahn@42779
|
100 |
|
bulwahn@42779
|
101 |
definition [simp, code del]:
|
bulwahn@42779
|
102 |
"0 = of_int 0"
|
bulwahn@42779
|
103 |
|
bulwahn@42779
|
104 |
definition [simp, code del]:
|
bulwahn@42779
|
105 |
"1 = of_int 1"
|
bulwahn@42779
|
106 |
|
bulwahn@42779
|
107 |
definition [simp, code del]:
|
bulwahn@42892
|
108 |
"n + m = of_int (int_of n + int_of m)"
|
bulwahn@42892
|
109 |
|
bulwahn@42892
|
110 |
definition [simp, code del]:
|
bulwahn@42779
|
111 |
"n - m = of_int (int_of n - int_of m)"
|
bulwahn@42779
|
112 |
|
bulwahn@42779
|
113 |
definition [simp, code del]:
|
bulwahn@42892
|
114 |
"n * m = of_int (int_of n * int_of m)"
|
bulwahn@42892
|
115 |
|
bulwahn@42892
|
116 |
definition [simp, code del]:
|
bulwahn@42892
|
117 |
"n div m = of_int (int_of n div int_of m)"
|
bulwahn@42892
|
118 |
|
bulwahn@42892
|
119 |
definition [simp, code del]:
|
bulwahn@42892
|
120 |
"n mod m = of_int (int_of n mod int_of m)"
|
bulwahn@42892
|
121 |
|
bulwahn@42892
|
122 |
definition [simp, code del]:
|
bulwahn@42779
|
123 |
"n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
|
bulwahn@42779
|
124 |
|
bulwahn@42779
|
125 |
definition [simp, code del]:
|
bulwahn@42779
|
126 |
"n < m \<longleftrightarrow> int_of n < int_of m"
|
bulwahn@42779
|
127 |
|
bulwahn@42779
|
128 |
|
bulwahn@42892
|
129 |
instance proof
|
bulwahn@42892
|
130 |
qed (auto simp add: code_int left_distrib zmult_zless_mono2)
|
bulwahn@42779
|
131 |
|
bulwahn@42779
|
132 |
end
|
bulwahn@43821
|
133 |
|
bulwahn@42779
|
134 |
lemma zero_code_int_code [code, code_unfold]:
|
bulwahn@42779
|
135 |
"(0\<Colon>code_int) = Numeral0"
|
bulwahn@43821
|
136 |
by (simp add: number_of_code_int_def Pls_def)
|
bulwahn@43821
|
137 |
lemma [code_post]: "Numeral0 = (0\<Colon>code_int)"
|
bulwahn@43821
|
138 |
using zero_code_int_code ..
|
bulwahn@42779
|
139 |
|
bulwahn@43821
|
140 |
lemma one_code_int_code [code, code_unfold]:
|
bulwahn@42779
|
141 |
"(1\<Colon>code_int) = Numeral1"
|
bulwahn@43821
|
142 |
by (simp add: number_of_code_int_def Pls_def Bit1_def)
|
bulwahn@42779
|
143 |
lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
|
bulwahn@43821
|
144 |
using one_code_int_code ..
|
bulwahn@43821
|
145 |
|
bulwahn@42779
|
146 |
|
bulwahn@42892
|
147 |
definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
|
bulwahn@42892
|
148 |
[code del]: "div_mod_code_int n m = (n div m, n mod m)"
|
bulwahn@42892
|
149 |
|
bulwahn@42892
|
150 |
lemma [code]:
|
bulwahn@42892
|
151 |
"div_mod_code_int n m = (if m = 0 then (0, n) else (n div m, n mod m))"
|
bulwahn@42892
|
152 |
unfolding div_mod_code_int_def by auto
|
bulwahn@42892
|
153 |
|
bulwahn@42892
|
154 |
lemma [code]:
|
bulwahn@42892
|
155 |
"n div m = fst (div_mod_code_int n m)"
|
bulwahn@42892
|
156 |
unfolding div_mod_code_int_def by simp
|
bulwahn@42892
|
157 |
|
bulwahn@42892
|
158 |
lemma [code]:
|
bulwahn@42892
|
159 |
"n mod m = snd (div_mod_code_int n m)"
|
bulwahn@42892
|
160 |
unfolding div_mod_code_int_def by simp
|
bulwahn@42892
|
161 |
|
bulwahn@42892
|
162 |
lemma int_of_code [code]:
|
bulwahn@42892
|
163 |
"int_of k = (if k = 0 then 0
|
bulwahn@42892
|
164 |
else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
|
bulwahn@42892
|
165 |
proof -
|
bulwahn@42892
|
166 |
have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k"
|
bulwahn@42892
|
167 |
by (rule mod_div_equality)
|
bulwahn@42892
|
168 |
have "int_of k mod 2 = 0 \<or> int_of k mod 2 = 1" by auto
|
bulwahn@42892
|
169 |
from this show ?thesis
|
bulwahn@42892
|
170 |
apply auto
|
bulwahn@42892
|
171 |
apply (insert 1) by (auto simp add: mult_ac)
|
bulwahn@42892
|
172 |
qed
|
bulwahn@42892
|
173 |
|
bulwahn@42892
|
174 |
|
bulwahn@42892
|
175 |
code_instance code_numeral :: equal
|
bulwahn@44179
|
176 |
(Haskell_Quickcheck -)
|
bulwahn@42892
|
177 |
|
bulwahn@42892
|
178 |
setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int}
|
bulwahn@44179
|
179 |
false Code_Printer.literal_numeral) ["Haskell_Quickcheck"] *}
|
bulwahn@42892
|
180 |
|
bulwahn@42779
|
181 |
code_const "0 \<Colon> code_int"
|
bulwahn@44179
|
182 |
(Haskell_Quickcheck "0")
|
bulwahn@42779
|
183 |
|
bulwahn@42779
|
184 |
code_const "1 \<Colon> code_int"
|
bulwahn@44179
|
185 |
(Haskell_Quickcheck "1")
|
bulwahn@42779
|
186 |
|
bulwahn@42779
|
187 |
code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
|
bulwahn@44179
|
188 |
(Haskell_Quickcheck "(_/ -/ _)")
|
bulwahn@42779
|
189 |
|
bulwahn@42892
|
190 |
code_const div_mod_code_int
|
bulwahn@44179
|
191 |
(Haskell_Quickcheck "divMod")
|
bulwahn@42892
|
192 |
|
bulwahn@42892
|
193 |
code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
|
bulwahn@44179
|
194 |
(Haskell_Quickcheck infix 4 "==")
|
bulwahn@42892
|
195 |
|
bulwahn@42779
|
196 |
code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
|
bulwahn@44179
|
197 |
(Haskell_Quickcheck infix 4 "<=")
|
bulwahn@42779
|
198 |
|
bulwahn@42779
|
199 |
code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
|
bulwahn@44179
|
200 |
(Haskell_Quickcheck infix 4 "<")
|
bulwahn@42779
|
201 |
|
bulwahn@42779
|
202 |
code_type code_int
|
bulwahn@44179
|
203 |
(Haskell_Quickcheck "Int")
|
bulwahn@42779
|
204 |
|
bulwahn@42892
|
205 |
code_abort of_int
|
bulwahn@42892
|
206 |
|
bulwahn@42832
|
207 |
subsubsection {* Narrowing's deep representation of types and terms *}
|
bulwahn@42776
|
208 |
|
bulwahn@43888
|
209 |
datatype narrowing_type = SumOfProd "narrowing_type list list"
|
bulwahn@43888
|
210 |
datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
|
bulwahn@43888
|
211 |
datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
|
bulwahn@42776
|
212 |
|
bulwahn@44227
|
213 |
primrec map_cons :: "('a => 'b) => 'a cons => 'b cons"
|
bulwahn@44227
|
214 |
where
|
bulwahn@44227
|
215 |
"map_cons f (C ty cs) = C ty (map (%c. f o c) cs)"
|
bulwahn@44227
|
216 |
|
hoelzl@44198
|
217 |
subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
|
bulwahn@43821
|
218 |
|
bulwahn@43821
|
219 |
class partial_term_of = typerep +
|
bulwahn@43888
|
220 |
fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
|
bulwahn@43888
|
221 |
|
bulwahn@43888
|
222 |
lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
|
bulwahn@43888
|
223 |
by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
|
bulwahn@44227
|
224 |
|
bulwahn@42835
|
225 |
subsubsection {* Auxilary functions for Narrowing *}
|
bulwahn@42776
|
226 |
|
bulwahn@42779
|
227 |
consts nth :: "'a list => code_int => 'a"
|
bulwahn@42776
|
228 |
|
bulwahn@44179
|
229 |
code_const nth (Haskell_Quickcheck infixl 9 "!!")
|
bulwahn@42776
|
230 |
|
bulwahn@42779
|
231 |
consts error :: "char list => 'a"
|
bulwahn@42776
|
232 |
|
bulwahn@44179
|
233 |
code_const error (Haskell_Quickcheck "error")
|
bulwahn@42776
|
234 |
|
bulwahn@42779
|
235 |
consts toEnum :: "code_int => char"
|
bulwahn@42776
|
236 |
|
bulwahn@44179
|
237 |
code_const toEnum (Haskell_Quickcheck "toEnum")
|
bulwahn@42776
|
238 |
|
bulwahn@44187
|
239 |
consts marker :: "char"
|
bulwahn@42779
|
240 |
|
bulwahn@44187
|
241 |
code_const marker (Haskell_Quickcheck "''\\0'")
|
bulwahn@44187
|
242 |
|
bulwahn@42832
|
243 |
subsubsection {* Narrowing's basic operations *}
|
bulwahn@42776
|
244 |
|
bulwahn@42832
|
245 |
type_synonym 'a narrowing = "code_int => 'a cons"
|
bulwahn@42776
|
246 |
|
bulwahn@42832
|
247 |
definition empty :: "'a narrowing"
|
bulwahn@42776
|
248 |
where
|
bulwahn@42776
|
249 |
"empty d = C (SumOfProd []) []"
|
bulwahn@42776
|
250 |
|
bulwahn@42832
|
251 |
definition cons :: "'a => 'a narrowing"
|
bulwahn@42776
|
252 |
where
|
bulwahn@42776
|
253 |
"cons a d = (C (SumOfProd [[]]) [(%_. a)])"
|
bulwahn@42776
|
254 |
|
bulwahn@43888
|
255 |
fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
|
bulwahn@42776
|
256 |
where
|
bulwahn@44187
|
257 |
"conv cs (Var p _) = error (marker # map toEnum p)"
|
bulwahn@42776
|
258 |
| "conv cs (Ctr i xs) = (nth cs i) xs"
|
bulwahn@42776
|
259 |
|
bulwahn@43888
|
260 |
fun nonEmpty :: "narrowing_type => bool"
|
bulwahn@42776
|
261 |
where
|
bulwahn@42776
|
262 |
"nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
|
bulwahn@42776
|
263 |
|
bulwahn@42832
|
264 |
definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
|
bulwahn@42776
|
265 |
where
|
bulwahn@42776
|
266 |
"apply f a d =
|
bulwahn@42776
|
267 |
(case f d of C (SumOfProd ps) cfs =>
|
bulwahn@42776
|
268 |
case a (d - 1) of C ta cas =>
|
bulwahn@42776
|
269 |
let
|
bulwahn@42776
|
270 |
shallow = (d > 0 \<and> nonEmpty ta);
|
bulwahn@42776
|
271 |
cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
|
bulwahn@42776
|
272 |
in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
|
bulwahn@42776
|
273 |
|
bulwahn@42832
|
274 |
definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
|
bulwahn@42776
|
275 |
where
|
bulwahn@42776
|
276 |
"sum a b d =
|
bulwahn@42776
|
277 |
(case a d of C (SumOfProd ssa) ca =>
|
bulwahn@42776
|
278 |
case b d of C (SumOfProd ssb) cb =>
|
bulwahn@42776
|
279 |
C (SumOfProd (ssa @ ssb)) (ca @ cb))"
|
bulwahn@42776
|
280 |
|
bulwahn@42783
|
281 |
lemma [fundef_cong]:
|
bulwahn@42783
|
282 |
assumes "a d = a' d" "b d = b' d" "d = d'"
|
bulwahn@42783
|
283 |
shows "sum a b d = sum a' b' d'"
|
bulwahn@43888
|
284 |
using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
|
bulwahn@42783
|
285 |
|
bulwahn@42783
|
286 |
lemma [fundef_cong]:
|
bulwahn@42783
|
287 |
assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
|
bulwahn@42783
|
288 |
assumes "d = d'"
|
bulwahn@42783
|
289 |
shows "apply f a d = apply f' a' d'"
|
bulwahn@42783
|
290 |
proof -
|
bulwahn@42783
|
291 |
note assms moreover
|
bulwahn@42801
|
292 |
have "int_of (of_int 0) < int_of d' ==> int_of (of_int 0) <= int_of (of_int (int_of d' - int_of (of_int 1)))"
|
bulwahn@42783
|
293 |
by (simp add: of_int_inverse)
|
bulwahn@42783
|
294 |
moreover
|
bulwahn@42801
|
295 |
have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
|
bulwahn@42783
|
296 |
by (simp add: of_int_inverse)
|
bulwahn@42783
|
297 |
ultimately show ?thesis
|
bulwahn@43888
|
298 |
unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
|
bulwahn@42783
|
299 |
qed
|
bulwahn@42783
|
300 |
|
bulwahn@42832
|
301 |
subsubsection {* Narrowing generator type class *}
|
bulwahn@42776
|
302 |
|
bulwahn@42832
|
303 |
class narrowing =
|
bulwahn@42832
|
304 |
fixes narrowing :: "code_int => 'a cons"
|
bulwahn@42776
|
305 |
|
bulwahn@44078
|
306 |
datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
|
bulwahn@44078
|
307 |
|
bulwahn@44078
|
308 |
(* FIXME: hard-wired maximal depth of 100 here *)
|
bulwahn@44186
|
309 |
definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
|
bulwahn@44078
|
310 |
where
|
bulwahn@44078
|
311 |
"exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
|
bulwahn@44078
|
312 |
|
bulwahn@44186
|
313 |
definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
|
bulwahn@44078
|
314 |
where
|
bulwahn@44078
|
315 |
"all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
|
bulwahn@44078
|
316 |
|
wenzelm@42814
|
317 |
subsubsection {* class @{text is_testable} *}
|
bulwahn@42776
|
318 |
|
wenzelm@42814
|
319 |
text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
|
bulwahn@42776
|
320 |
|
bulwahn@42776
|
321 |
class is_testable
|
bulwahn@42776
|
322 |
|
bulwahn@42776
|
323 |
instance bool :: is_testable ..
|
bulwahn@42776
|
324 |
|
bulwahn@43888
|
325 |
instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable ..
|
bulwahn@42776
|
326 |
|
bulwahn@42776
|
327 |
definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
|
bulwahn@42776
|
328 |
where
|
bulwahn@42776
|
329 |
"ensure_testable f = f"
|
bulwahn@42776
|
330 |
|
bulwahn@42781
|
331 |
|
bulwahn@42893
|
332 |
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
|
bulwahn@42893
|
333 |
|
bulwahn@42893
|
334 |
datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
|
bulwahn@42893
|
335 |
|
bulwahn@42893
|
336 |
primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
|
bulwahn@42893
|
337 |
where
|
bulwahn@42893
|
338 |
"eval_ffun (Constant c) x = c"
|
bulwahn@42893
|
339 |
| "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)"
|
bulwahn@42893
|
340 |
|
bulwahn@42893
|
341 |
hide_type (open) ffun
|
bulwahn@42893
|
342 |
hide_const (open) Constant Update eval_ffun
|
bulwahn@42893
|
343 |
|
bulwahn@42895
|
344 |
datatype 'b cfun = Constant 'b
|
bulwahn@42895
|
345 |
|
bulwahn@42895
|
346 |
primrec eval_cfun :: "'b cfun => 'a => 'b"
|
bulwahn@42895
|
347 |
where
|
bulwahn@42895
|
348 |
"eval_cfun (Constant c) y = c"
|
bulwahn@42895
|
349 |
|
bulwahn@42895
|
350 |
hide_type (open) cfun
|
bulwahn@42895
|
351 |
hide_const (open) Constant eval_cfun
|
bulwahn@42895
|
352 |
|
bulwahn@42895
|
353 |
subsubsection {* Setting up the counterexample generator *}
|
bulwahn@44078
|
354 |
|
wenzelm@44576
|
355 |
use "Tools/Quickcheck/narrowing_generators.ML"
|
bulwahn@42895
|
356 |
|
bulwahn@42895
|
357 |
setup {* Narrowing_Generators.setup *}
|
bulwahn@42895
|
358 |
|
bulwahn@45863
|
359 |
definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
|
bulwahn@45863
|
360 |
where
|
bulwahn@45863
|
361 |
"narrowing_dummy_partial_term_of = partial_term_of"
|
bulwahn@45863
|
362 |
|
bulwahn@45863
|
363 |
definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
|
bulwahn@45863
|
364 |
where
|
bulwahn@45863
|
365 |
"narrowing_dummy_narrowing = narrowing"
|
bulwahn@45863
|
366 |
|
bulwahn@45863
|
367 |
lemma [code]:
|
bulwahn@45863
|
368 |
"ensure_testable f =
|
bulwahn@45863
|
369 |
(let
|
bulwahn@45863
|
370 |
x = narrowing_dummy_narrowing :: code_int => bool cons;
|
bulwahn@45863
|
371 |
y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
|
bulwahn@45863
|
372 |
z = (conv :: _ => _ => unit) in f)"
|
bulwahn@45863
|
373 |
unfolding Let_def ensure_testable_def ..
|
bulwahn@45863
|
374 |
|
bulwahn@45863
|
375 |
|
bulwahn@44227
|
376 |
subsection {* Narrowing for integers *}
|
bulwahn@44227
|
377 |
|
bulwahn@44227
|
378 |
|
bulwahn@44227
|
379 |
definition drawn_from :: "'a list => 'a cons"
|
bulwahn@44227
|
380 |
where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
|
bulwahn@44227
|
381 |
|
bulwahn@44227
|
382 |
function around_zero :: "int => int list"
|
bulwahn@44227
|
383 |
where
|
bulwahn@44227
|
384 |
"around_zero i = (if i < 0 then [] else (if i = 0 then [0] else around_zero (i - 1) @ [i, -i]))"
|
bulwahn@44227
|
385 |
by pat_completeness auto
|
bulwahn@44227
|
386 |
termination by (relation "measure nat") auto
|
bulwahn@44227
|
387 |
|
bulwahn@44227
|
388 |
declare around_zero.simps[simp del]
|
bulwahn@44227
|
389 |
|
bulwahn@44227
|
390 |
lemma length_around_zero:
|
bulwahn@44227
|
391 |
assumes "i >= 0"
|
bulwahn@44227
|
392 |
shows "length (around_zero i) = 2 * nat i + 1"
|
bulwahn@44227
|
393 |
proof (induct rule: int_ge_induct[OF assms])
|
bulwahn@44227
|
394 |
case 1
|
bulwahn@44227
|
395 |
from 1 show ?case by (simp add: around_zero.simps)
|
bulwahn@44227
|
396 |
next
|
bulwahn@44227
|
397 |
case (2 i)
|
bulwahn@44227
|
398 |
from 2 show ?case
|
bulwahn@44227
|
399 |
by (simp add: around_zero.simps[of "i + 1"])
|
bulwahn@44227
|
400 |
qed
|
bulwahn@44227
|
401 |
|
bulwahn@44227
|
402 |
instantiation int :: narrowing
|
bulwahn@44227
|
403 |
begin
|
bulwahn@44227
|
404 |
|
bulwahn@44227
|
405 |
definition
|
bulwahn@44227
|
406 |
"narrowing_int d = (let (u :: _ => _ => unit) = conv; i = Quickcheck_Narrowing.int_of d in drawn_from (around_zero i))"
|
bulwahn@44227
|
407 |
|
bulwahn@44227
|
408 |
instance ..
|
bulwahn@44227
|
409 |
|
bulwahn@44227
|
410 |
end
|
bulwahn@44227
|
411 |
|
bulwahn@44227
|
412 |
lemma [code, code del]: "partial_term_of (ty :: int itself) t == undefined"
|
bulwahn@44227
|
413 |
by (rule partial_term_of_anything)+
|
bulwahn@44227
|
414 |
|
bulwahn@44227
|
415 |
lemma [code]:
|
bulwahn@44227
|
416 |
"partial_term_of (ty :: int itself) (Var p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
|
bulwahn@44227
|
417 |
"partial_term_of (ty :: int itself) (Ctr i []) == (if i mod 2 = 0 then
|
bulwahn@44227
|
418 |
Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
|
bulwahn@44227
|
419 |
by (rule partial_term_of_anything)+
|
bulwahn@44227
|
420 |
|
bulwahn@44227
|
421 |
text {* Defining integers by positive and negative copy of naturals *}
|
bulwahn@44227
|
422 |
(*
|
bulwahn@44227
|
423 |
datatype simple_int = Positive nat | Negative nat
|
bulwahn@44227
|
424 |
|
bulwahn@44227
|
425 |
primrec int_of_simple_int :: "simple_int => int"
|
bulwahn@44227
|
426 |
where
|
bulwahn@44227
|
427 |
"int_of_simple_int (Positive n) = int n"
|
bulwahn@44227
|
428 |
| "int_of_simple_int (Negative n) = (-1 - int n)"
|
bulwahn@44227
|
429 |
|
bulwahn@44227
|
430 |
instantiation int :: narrowing
|
bulwahn@44227
|
431 |
begin
|
bulwahn@44227
|
432 |
|
bulwahn@44227
|
433 |
definition narrowing_int :: "code_int => int cons"
|
bulwahn@44227
|
434 |
where
|
bulwahn@44227
|
435 |
"narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)"
|
bulwahn@44227
|
436 |
|
bulwahn@44227
|
437 |
instance ..
|
bulwahn@44227
|
438 |
|
bulwahn@44227
|
439 |
end
|
bulwahn@44227
|
440 |
|
bulwahn@44227
|
441 |
text {* printing the partial terms *}
|
bulwahn@44227
|
442 |
|
bulwahn@44227
|
443 |
lemma [code]:
|
bulwahn@44227
|
444 |
"partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'')
|
bulwahn@44227
|
445 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
|
bulwahn@44227
|
446 |
by (rule partial_term_of_anything)
|
bulwahn@44227
|
447 |
|
bulwahn@44227
|
448 |
*)
|
bulwahn@44227
|
449 |
|
bulwahn@44186
|
450 |
hide_type code_int narrowing_type narrowing_term cons property
|
bulwahn@44758
|
451 |
hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists
|
bulwahn@44758
|
452 |
hide_const (open) Var Ctr "apply" sum cons
|
bulwahn@44186
|
453 |
hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
|
bulwahn@42893
|
454 |
|
bulwahn@44227
|
455 |
|
bulwahn@45863
|
456 |
end
|