src/HOL/Quickcheck_Exhaustive.thy
changeset 41915 fba21941bdc5
parent 41722 9575694d2da5
child 41916 80060d5f864a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:12 2011 +0100
     1.3 @@ -0,0 +1,420 @@
     1.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     1.5 +
     1.6 +header {* Another simple counterexample generator *}
     1.7 +
     1.8 +theory Smallcheck
     1.9 +imports Quickcheck
    1.10 +uses ("Tools/smallvalue_generators.ML")
    1.11 +begin
    1.12 +
    1.13 +subsection {* basic operations for generators *}
    1.14 +
    1.15 +definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    1.16 +where
    1.17 +  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    1.18 +
    1.19 +subsection {* small value generator type classes *}
    1.20 +
    1.21 +class small = term_of +
    1.22 +fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.23 +
    1.24 +instantiation unit :: small
    1.25 +begin
    1.26 +
    1.27 +definition "small f d = f ()"
    1.28 +
    1.29 +instance ..
    1.30 +
    1.31 +end
    1.32 +
    1.33 +instantiation int :: small
    1.34 +begin
    1.35 +
    1.36 +function small' :: "(int => term list option) => int => int => term list option"
    1.37 +where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))"
    1.38 +by pat_completeness auto
    1.39 +
    1.40 +termination 
    1.41 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    1.42 +
    1.43 +definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.44 +
    1.45 +instance ..
    1.46 +
    1.47 +end
    1.48 +
    1.49 +instantiation prod :: (small, small) small
    1.50 +begin
    1.51 +
    1.52 +definition
    1.53 +  "small f d = small (%x. small (%y. f (x, y)) d) d"
    1.54 +
    1.55 +instance ..
    1.56 +
    1.57 +end
    1.58 +
    1.59 +subsection {* full small value generator type classes *}
    1.60 +
    1.61 +class full_small = term_of +
    1.62 +fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.63 +
    1.64 +instantiation unit :: full_small
    1.65 +begin
    1.66 +
    1.67 +definition "full_small f d = f (Code_Evaluation.valtermify ())"
    1.68 +
    1.69 +instance ..
    1.70 +
    1.71 +end
    1.72 +
    1.73 +instantiation code_numeral :: full_small
    1.74 +begin
    1.75 +
    1.76 +function full_small_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.77 +  where "full_small_code_numeral' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small_code_numeral' f d (i + 1)))"
    1.78 +by pat_completeness auto
    1.79 +
    1.80 +termination 
    1.81 +  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.82 +
    1.83 +definition "full_small f d = full_small_code_numeral' f d 0"
    1.84 +
    1.85 +instance ..
    1.86 +
    1.87 +end
    1.88 +
    1.89 +instantiation nat :: full_small
    1.90 +begin
    1.91 +
    1.92 +definition "full_small f d = full_small (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.93 +
    1.94 +instance ..
    1.95 +
    1.96 +end
    1.97 +
    1.98 +instantiation int :: full_small
    1.99 +begin
   1.100 +
   1.101 +function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
   1.102 +  where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
   1.103 +by pat_completeness auto
   1.104 +
   1.105 +termination 
   1.106 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.107 +
   1.108 +definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   1.109 +
   1.110 +instance ..
   1.111 +
   1.112 +end
   1.113 +
   1.114 +instantiation prod :: (full_small, full_small) full_small
   1.115 +begin
   1.116 +
   1.117 +definition
   1.118 +  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
   1.119 +    %u. let T1 = (Typerep.typerep (TYPE('a)));
   1.120 +            T2 = (Typerep.typerep (TYPE('b)))
   1.121 +    in Code_Evaluation.App (Code_Evaluation.App (
   1.122 +      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   1.123 +      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   1.124 +      (t1 ())) (t2 ()))) d) d"
   1.125 +
   1.126 +instance ..
   1.127 +
   1.128 +end
   1.129 +
   1.130 +instantiation "fun" :: ("{equal, full_small}", full_small) full_small
   1.131 +begin
   1.132 +
   1.133 +fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   1.134 +where
   1.135 +  "full_small_fun' f i d = (if i > 1 then
   1.136 +    full_small (%(a, at). full_small (%(b, bt).
   1.137 +      full_small_fun' (%(g, gt). f (g(a := b),
   1.138 +        (%_. let T1 = (Typerep.typerep (TYPE('a)));
   1.139 +                 T2 = (Typerep.typerep (TYPE('b)))
   1.140 +             in
   1.141 +               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   1.142 +                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   1.143 +                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   1.144 +                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   1.145 +               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
   1.146 +  else (if i > 0 then
   1.147 +    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   1.148 +
   1.149 +definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.150 +where
   1.151 +  "full_small_fun f d = full_small_fun' f d d" 
   1.152 +
   1.153 +instance ..
   1.154 +
   1.155 +end
   1.156 +
   1.157 +subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   1.158 +
   1.159 +
   1.160 +class check_all = enum + term_of +
   1.161 +  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   1.162 +  fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   1.163 +  
   1.164 +fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
   1.165 +where
   1.166 +  "check_all_n_lists f n =
   1.167 +     (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   1.168 +
   1.169 +definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
   1.170 +where
   1.171 +  "mk_map_term T1 T2 domm rng =
   1.172 +     (%_. let T1 = T1 ();
   1.173 +              T2 = T2 ();
   1.174 +              update_term = (%g (a, b).
   1.175 +                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   1.176 +                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   1.177 +                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   1.178 +                      Typerep.Typerep (STR ''fun'') [T1,
   1.179 +                        Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   1.180 +                        g) a) b)
   1.181 +          in
   1.182 +             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   1.183 +
   1.184 +instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   1.185 +begin
   1.186 +
   1.187 +definition
   1.188 +  "check_all f =
   1.189 +    (let
   1.190 +      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   1.191 +      enum = (Enum.enum :: 'a list)
   1.192 +    in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))"
   1.193 +
   1.194 +definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   1.195 +where
   1.196 +  "enum_term_of_fun = (%_ _. let
   1.197 +    enum_term_of_a = enum_term_of (TYPE('a));
   1.198 +    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   1.199 +  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   1.200 + 
   1.201 +instance ..
   1.202 +
   1.203 +end
   1.204 +
   1.205 +
   1.206 +instantiation unit :: check_all
   1.207 +begin
   1.208 +
   1.209 +definition
   1.210 +  "check_all f = f (Code_Evaluation.valtermify ())"
   1.211 +
   1.212 +definition enum_term_of_unit :: "unit itself => unit => term list"
   1.213 +where
   1.214 +  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   1.215 +
   1.216 +instance ..
   1.217 +
   1.218 +end
   1.219 +
   1.220 +
   1.221 +instantiation bool :: check_all
   1.222 +begin
   1.223 +
   1.224 +definition
   1.225 +  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   1.226 +
   1.227 +definition enum_term_of_bool :: "bool itself => unit => term list"
   1.228 +where
   1.229 +  "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   1.230 +
   1.231 +instance ..
   1.232 +
   1.233 +end
   1.234 +
   1.235 +
   1.236 +instantiation prod :: (check_all, check_all) check_all
   1.237 +begin
   1.238 +
   1.239 +definition
   1.240 +  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
   1.241 +    %u. let T1 = (Typerep.typerep (TYPE('a)));
   1.242 +            T2 = (Typerep.typerep (TYPE('b)))
   1.243 +    in Code_Evaluation.App (Code_Evaluation.App (
   1.244 +      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   1.245 +      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   1.246 +      (t1 ())) (t2 ()))))"
   1.247 +
   1.248 +definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   1.249 +where
   1.250 +  "enum_term_of_prod = (%_ _. map (%(x, y).
   1.251 +       let T1 = (Typerep.typerep (TYPE('a)));
   1.252 +           T2 = (Typerep.typerep (TYPE('b)))
   1.253 +       in Code_Evaluation.App (Code_Evaluation.App (
   1.254 +         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   1.255 +           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
   1.256 +     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
   1.257 +
   1.258 +instance ..
   1.259 +
   1.260 +end
   1.261 +
   1.262 +
   1.263 +instantiation sum :: (check_all, check_all) check_all
   1.264 +begin
   1.265 +
   1.266 +definition
   1.267 +  "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
   1.268 +     let T1 = (Typerep.typerep (TYPE('a)));
   1.269 +         T2 = (Typerep.typerep (TYPE('b)))
   1.270 +       in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   1.271 +           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
   1.272 +             | None => check_all (%(b, t). f (Inr b, %_. let
   1.273 +                 T1 = (Typerep.typerep (TYPE('a)));
   1.274 +                 T2 = (Typerep.typerep (TYPE('b)))
   1.275 +               in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   1.276 +                 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
   1.277 +
   1.278 +definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   1.279 +where
   1.280 +  "enum_term_of_sum = (%_ _.
   1.281 +     let
   1.282 +       T1 = (Typerep.typerep (TYPE('a)));
   1.283 +       T2 = (Typerep.typerep (TYPE('b)))
   1.284 +     in
   1.285 +       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   1.286 +             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.287 +             (enum_term_of (TYPE('a)) ()) @
   1.288 +       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   1.289 +             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.290 +             (enum_term_of (TYPE('b)) ()))"
   1.291 +
   1.292 +instance ..
   1.293 +
   1.294 +end
   1.295 +
   1.296 +instantiation nibble :: check_all
   1.297 +begin
   1.298 +
   1.299 +definition
   1.300 +  "check_all f =
   1.301 +    f (Code_Evaluation.valtermify Nibble0) orelse
   1.302 +    f (Code_Evaluation.valtermify Nibble1) orelse
   1.303 +    f (Code_Evaluation.valtermify Nibble2) orelse
   1.304 +    f (Code_Evaluation.valtermify Nibble3) orelse
   1.305 +    f (Code_Evaluation.valtermify Nibble4) orelse
   1.306 +    f (Code_Evaluation.valtermify Nibble5) orelse
   1.307 +    f (Code_Evaluation.valtermify Nibble6) orelse
   1.308 +    f (Code_Evaluation.valtermify Nibble7) orelse
   1.309 +    f (Code_Evaluation.valtermify Nibble8) orelse
   1.310 +    f (Code_Evaluation.valtermify Nibble9) orelse
   1.311 +    f (Code_Evaluation.valtermify NibbleA) orelse
   1.312 +    f (Code_Evaluation.valtermify NibbleB) orelse
   1.313 +    f (Code_Evaluation.valtermify NibbleC) orelse
   1.314 +    f (Code_Evaluation.valtermify NibbleD) orelse
   1.315 +    f (Code_Evaluation.valtermify NibbleE) orelse
   1.316 +    f (Code_Evaluation.valtermify NibbleF)"
   1.317 +
   1.318 +definition enum_term_of_nibble :: "nibble itself => unit => term list"
   1.319 +where
   1.320 +  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   1.321 +
   1.322 +instance ..
   1.323 +
   1.324 +end
   1.325 +
   1.326 +
   1.327 +instantiation char :: check_all
   1.328 +begin
   1.329 +
   1.330 +definition
   1.331 +  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   1.332 +
   1.333 +definition enum_term_of_char :: "char itself => unit => term list"
   1.334 +where
   1.335 +  "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   1.336 +
   1.337 +instance ..
   1.338 +
   1.339 +end
   1.340 +
   1.341 +
   1.342 +instantiation option :: (check_all) check_all
   1.343 +begin
   1.344 +
   1.345 +definition
   1.346 +  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   1.347 +    (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.348 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   1.349 +
   1.350 +definition enum_term_of_option :: "'a option itself => unit => term list"
   1.351 +where
   1.352 +  "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.353 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
   1.354 +
   1.355 +instance ..
   1.356 +
   1.357 +end
   1.358 +
   1.359 +
   1.360 +instantiation Enum.finite_1 :: check_all
   1.361 +begin
   1.362 +
   1.363 +definition
   1.364 +  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
   1.365 +
   1.366 +definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   1.367 +where
   1.368 +  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
   1.369 +
   1.370 +instance ..
   1.371 +
   1.372 +end
   1.373 +
   1.374 +instantiation Enum.finite_2 :: check_all
   1.375 +begin
   1.376 +
   1.377 +definition
   1.378 +  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
   1.379 +
   1.380 +definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   1.381 +where
   1.382 +  "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   1.383 +
   1.384 +instance ..
   1.385 +
   1.386 +end
   1.387 +
   1.388 +instantiation Enum.finite_3 :: check_all
   1.389 +begin
   1.390 +
   1.391 +definition
   1.392 +  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
   1.393 +
   1.394 +definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   1.395 +where
   1.396 +  "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   1.397 +
   1.398 +instance ..
   1.399 +
   1.400 +end
   1.401 +
   1.402 +
   1.403 +
   1.404 +subsection {* Defining combinators for any first-order data type *}
   1.405 +
   1.406 +definition catch_match :: "term list option => term list option => term list option"
   1.407 +where
   1.408 +  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
   1.409 +
   1.410 +code_const catch_match 
   1.411 +  (SML "(_) handle Match => _")
   1.412 +
   1.413 +use "Tools/smallvalue_generators.ML"
   1.414 +
   1.415 +setup {* Smallvalue_Generators.setup *}
   1.416 +
   1.417 +declare [[quickcheck_tester = exhaustive]]
   1.418 +
   1.419 +hide_fact orelse_def catch_match_def
   1.420 +no_notation orelse (infixr "orelse" 55)
   1.421 +hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   1.422 +
   1.423 +end
   1.424 \ No newline at end of file