1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* Experimental counterexample generators *} |
|
4 |
|
5 theory Quickcheck_Generators |
|
6 imports Quickcheck State_Monad |
|
7 begin |
|
8 |
|
9 subsection {* Datatypes *} |
|
10 |
|
11 definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |
|
12 "collapse f = (do g \<leftarrow> f; g done)" |
|
13 |
|
14 lemma random'_if: |
|
15 fixes random' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" |
|
16 assumes "random' 0 j = (\<lambda>s. undefined)" |
|
17 and "\<And>i. random' (Suc_code_numeral i) j = rhs2 i" |
|
18 shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" |
|
19 by (cases i rule: code_numeral.exhaust) (insert assms, simp_all) |
|
20 |
|
21 setup {* |
|
22 let |
|
23 fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); |
|
24 fun scomp T1 T2 sT f g = Const (@{const_name scomp}, |
|
25 liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; |
|
26 exception REC of string; |
|
27 exception TYP of string; |
|
28 fun mk_collapse thy ty = Sign.mk_const thy |
|
29 (@{const_name collapse}, [@{typ Random.seed}, ty]); |
|
30 fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); |
|
31 fun mk_split thy ty ty' = Sign.mk_const thy |
|
32 (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT (term_ty ty') @{typ Random.seed}]); |
|
33 fun mk_scomp_split thy ty ty' t t' = |
|
34 scomp (term_ty ty) (term_ty ty') @{typ Random.seed} t |
|
35 (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))) |
|
36 fun mk_cons thy this_ty (c, args) = |
|
37 let |
|
38 val tys = map (fst o fst) args; |
|
39 val c_ty = tys ---> this_ty; |
|
40 val c = Const (c, tys ---> this_ty); |
|
41 val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); |
|
42 val c_indices = map (curry ( op + ) 1) t_indices; |
|
43 val c_t = list_comb (c, map Bound c_indices); |
|
44 val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term |
|
45 (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) |
|
46 |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); |
|
47 val return = HOLogic.mk_return (term_ty this_ty) @{typ Random.seed} |
|
48 (HOLogic.mk_prod (c_t, t_t)); |
|
49 val t = fold_rev (fn ((ty, _), random) => |
|
50 mk_scomp_split thy ty this_ty random) |
|
51 args return; |
|
52 val is_rec = exists (snd o fst) args; |
|
53 in (is_rec, t) end; |
|
54 fun mk_conss thy ty [] = NONE |
|
55 | mk_conss thy ty [(_, t)] = SOME t |
|
56 | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ |
|
57 (Sign.mk_const thy (@{const_name Random.select}, [liftT (term_ty ty) @{typ Random.seed}]) $ |
|
58 HOLogic.mk_list (liftT (term_ty ty) @{typ Random.seed}) (map snd ts))); |
|
59 fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = |
|
60 let |
|
61 val SOME t_atom = mk_conss thy ty ts_atom; |
|
62 in case mk_conss thy ty ts_rec |
|
63 of SOME t_rec => mk_collapse thy (term_ty ty) $ |
|
64 (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $ |
|
65 @{term "i\<Colon>code_numeral"} $ t_rec $ t_atom) |
|
66 | NONE => t_atom |
|
67 end; |
|
68 fun mk_random_eqs thy vs tycos = |
|
69 let |
|
70 val this_ty = Type (hd tycos, map TFree vs); |
|
71 val this_ty' = liftT (term_ty this_ty) @{typ Random.seed}; |
|
72 val random_name = Long_Name.base_name @{const_name random}; |
|
73 val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; |
|
74 fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); |
|
75 val random' = Free (random'_name, |
|
76 @{typ code_numeral} --> @{typ code_numeral} --> this_ty'); |
|
77 fun atom ty = if Sign.of_sort thy (ty, @{sort random}) |
|
78 then ((ty, false), random ty $ @{term "j\<Colon>code_numeral"}) |
|
79 else raise TYP |
|
80 ("Will not generate random elements for type(s) " ^ quote (hd tycos)); |
|
81 fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"}); |
|
82 fun rtyp (tyco, Ts) _ = raise REC |
|
83 ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); |
|
84 val rhss = DatatypePackage.construction_interpretation thy |
|
85 { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos |
|
86 |> fst |
|
87 |> (map o apsnd o map) (mk_cons thy this_ty) |
|
88 |> (map o apsnd) (List.partition fst) |
|
89 |> map (mk_clauses thy this_ty) |
|
90 val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ |
|
91 (random' $ @{term "0\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"}, Abs ("s", @{typ Random.seed}, |
|
92 Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))), |
|
93 (random' $ @{term "Suc_code_numeral i"} $ @{term "j\<Colon>code_numeral"}, rhs) |
|
94 ]))) rhss; |
|
95 in eqss end; |
|
96 fun random_inst [tyco] thy = |
|
97 let |
|
98 val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; |
|
99 val vs = (map o apsnd) |
|
100 (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; |
|
101 val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; |
|
102 val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
|
103 (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>code_numeral"}, |
|
104 random' $ @{term "max (i\<Colon>code_numeral) 1"} $ @{term "i\<Colon>code_numeral"}) |
|
105 val del_func = Attrib.internal (fn _ => Thm.declaration_attribute |
|
106 (fn thm => Context.mapping (Code.del_eqn thm) I)); |
|
107 fun add_code simps lthy = |
|
108 let |
|
109 val thy = ProofContext.theory_of lthy; |
|
110 val thm = @{thm random'_if} |
|
111 |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] |
|
112 |> (fn thm => thm OF simps) |
|
113 |> singleton (ProofContext.export lthy (ProofContext.init thy)); |
|
114 val c = (fst o dest_Const o fst o strip_comb o fst |
|
115 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; |
|
116 in |
|
117 lthy |
|
118 |> LocalTheory.theory (Code.del_eqns c |
|
119 #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal]) |
|
120 #-> Code.add_eqn) |
|
121 end; |
|
122 in |
|
123 thy |
|
124 |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) |
|
125 |> PrimrecPackage.add_primrec |
|
126 [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] |
|
127 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') |
|
128 |-> add_code |
|
129 |> `(fn lthy => Syntax.check_term lthy eq) |
|
130 |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) |
|
131 |> snd |
|
132 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
133 |> LocalTheory.exit_global |
|
134 end |
|
135 | random_inst tycos thy = raise REC |
|
136 ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); |
|
137 fun add_random_inst [@{type_name bool}] thy = thy |
|
138 | add_random_inst [@{type_name nat}] thy = thy |
|
139 | add_random_inst [@{type_name char}] thy = thy |
|
140 | add_random_inst [@{type_name String.literal}] thy = thy |
|
141 | add_random_inst tycos thy = random_inst tycos thy |
|
142 handle REC msg => (warning msg; thy) |
|
143 | TYP msg => (warning msg; thy) |
|
144 in DatatypePackage.interpretation add_random_inst end |
|
145 *} |
|
146 |
|
147 |
|
148 subsection {* Examples *} |
|
149 |
|
150 theorem "map g (map f xs) = map (g o f) xs" |
|
151 quickcheck [generator = code] |
|
152 by (induct xs) simp_all |
|
153 |
|
154 theorem "map g (map f xs) = map (f o g) xs" |
|
155 quickcheck [generator = code] |
|
156 oops |
|
157 |
|
158 theorem "rev (xs @ ys) = rev ys @ rev xs" |
|
159 quickcheck [generator = code] |
|
160 by simp |
|
161 |
|
162 theorem "rev (xs @ ys) = rev xs @ rev ys" |
|
163 quickcheck [generator = code] |
|
164 oops |
|
165 |
|
166 theorem "rev (rev xs) = xs" |
|
167 quickcheck [generator = code] |
|
168 by simp |
|
169 |
|
170 theorem "rev xs = xs" |
|
171 quickcheck [generator = code] |
|
172 oops |
|
173 |
|
174 primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
175 "app [] x = x" |
|
176 | "app (f # fs) x = app fs (f x)" |
|
177 |
|
178 lemma "app (fs @ gs) x = app gs (app fs x)" |
|
179 quickcheck [generator = code] |
|
180 by (induct fs arbitrary: x) simp_all |
|
181 |
|
182 lemma "app (fs @ gs) x = app fs (app gs x)" |
|
183 quickcheck [generator = code] |
|
184 oops |
|
185 |
|
186 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where |
|
187 "occurs a [] = 0" |
|
188 | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" |
|
189 |
|
190 primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
191 "del1 a [] = []" |
|
192 | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" |
|
193 |
|
194 lemma "Suc (occurs a (del1 a xs)) = occurs a xs" |
|
195 -- {* Wrong. Precondition needed.*} |
|
196 quickcheck [generator = code] |
|
197 oops |
|
198 |
|
199 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
|
200 quickcheck [generator = code] |
|
201 -- {* Also wrong.*} |
|
202 oops |
|
203 |
|
204 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" |
|
205 quickcheck [generator = code] |
|
206 by (induct xs) auto |
|
207 |
|
208 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
209 "replace a b [] = []" |
|
210 | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) |
|
211 else (x#(replace a b xs)))" |
|
212 |
|
213 lemma "occurs a xs = occurs b (replace a b xs)" |
|
214 quickcheck [generator = code] |
|
215 -- {* Wrong. Precondition needed.*} |
|
216 oops |
|
217 |
|
218 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" |
|
219 quickcheck [generator = code] |
|
220 by (induct xs) simp_all |
|
221 |
|
222 |
|
223 subsection {* Trees *} |
|
224 |
|
225 datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree" |
|
226 |
|
227 primrec leaves :: "'a tree \<Rightarrow> 'a list" where |
|
228 "leaves Twig = []" |
|
229 | "leaves (Leaf a) = [a]" |
|
230 | "leaves (Branch l r) = (leaves l) @ (leaves r)" |
|
231 |
|
232 primrec plant :: "'a list \<Rightarrow> 'a tree" where |
|
233 "plant [] = Twig " |
|
234 | "plant (x#xs) = Branch (Leaf x) (plant xs)" |
|
235 |
|
236 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where |
|
237 "mirror (Twig) = Twig " |
|
238 | "mirror (Leaf a) = Leaf a " |
|
239 | "mirror (Branch l r) = Branch (mirror r) (mirror l)" |
|
240 |
|
241 theorem "plant (rev (leaves xt)) = mirror xt" |
|
242 quickcheck [generator = code] |
|
243 --{* Wrong! *} |
|
244 oops |
|
245 |
|
246 theorem "plant (leaves xt @ leaves yt) = Branch xt yt" |
|
247 quickcheck [generator = code] |
|
248 --{* Wrong! *} |
|
249 oops |
|
250 |
|
251 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" |
|
252 |
|
253 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where |
|
254 "inOrder (Tip a)= [a]" |
|
255 | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" |
|
256 |
|
257 primrec root :: "'a ntree \<Rightarrow> 'a" where |
|
258 "root (Tip a) = a" |
|
259 | "root (Node f x y) = f" |
|
260 |
|
261 theorem "hd (inOrder xt) = root xt" |
|
262 quickcheck [generator = code] |
|
263 --{* Wrong! *} |
|
264 oops |
|
265 |
|
266 lemma "int (f k) = k" |
|
267 quickcheck [generator = code] |
|
268 oops |
|
269 |
|
270 lemma "int (nat k) = k" |
|
271 quickcheck [generator = code] |
|
272 oops |
|
273 |
|
274 end |
|