src/HOL/Quickcheck_Exhaustive.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42304 34366f39d32d
parent 42274 50850486f8dc
child 42305 494c31fdec95
permissions -rw-r--r--
new compilation for exhaustive quickcheck
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* A simple counterexample generator performing exhaustive testing *}
     4 
     5 theory Quickcheck_Exhaustive
     6 imports Quickcheck
     7 uses ("Tools/Quickcheck/exhaustive_generators.ML")
     8 begin
     9 
    10 subsection {* basic operations for exhaustive generators *}
    11 
    12 definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    13 where
    14   [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    15 
    16 subsection {* exhaustive generator type classes *}
    17 
    18 class exhaustive = term_of +
    19   fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    20   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    21 
    22 instantiation code_numeral :: exhaustive
    23 begin
    24 
    25 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    26   where "full_exhaustive_code_numeral' f d i =
    27     (if d < i then None
    28     else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    29 by pat_completeness auto
    30 
    31 termination
    32   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    33 
    34 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    35 
    36 function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    37   where "exhaustive_code_numeral' f d i =
    38     (if d < i then None
    39     else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    40 by pat_completeness auto
    41 
    42 termination
    43   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    44 
    45 definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    46 
    47 
    48 instance ..
    49 
    50 end
    51 
    52 instantiation nat :: exhaustive
    53 begin
    54 
    55 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
    56 
    57 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    58 
    59 instance ..
    60 
    61 end
    62 
    63 instantiation int :: exhaustive
    64 begin
    65 
    66 function exhaustive' :: "(int => term list option) => int => int => term list option"
    67   where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    68 by pat_completeness auto
    69 
    70 termination 
    71   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    72 
    73 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    74 
    75 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    76   where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
    77 by pat_completeness auto
    78 
    79 termination 
    80   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    81 
    82 definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    83 
    84 instance ..
    85 
    86 end
    87 
    88 instantiation prod :: (exhaustive, exhaustive) exhaustive
    89 begin
    90 
    91 definition
    92   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
    93 
    94 definition
    95   "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
    96     %u. let T1 = (Typerep.typerep (TYPE('a)));
    97             T2 = (Typerep.typerep (TYPE('b)))
    98     in Code_Evaluation.App (Code_Evaluation.App (
    99       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   100       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   101       (t1 ())) (t2 ()))) d) d"
   102 
   103 instance ..
   104 
   105 end
   106 
   107 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   108 begin
   109 
   110 fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
   111 where
   112   "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   113    orelse (if i > 1 then
   114      exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   115        f (g(a := b))) d) d) (i - 1) d else None)"
   116 
   117 definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
   118 where
   119   "exhaustive_fun f d = exhaustive_fun' f d d" 
   120 
   121 
   122 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   123 where
   124   "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   125    orelse (if i > 1 then
   126      full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
   127        f (g(a := b),
   128          (%_. let A = (Typerep.typerep (TYPE('a)));
   129                   B = (Typerep.typerep (TYPE('b)));
   130                   fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
   131               in
   132                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   133                   (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
   134                 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
   135 
   136 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   137 where
   138   "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   139 
   140 instance ..
   141 
   142 end
   143 
   144 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   145 
   146 class check_all = enum + term_of +
   147   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   148   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   149   
   150 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
   151 where
   152   "check_all_n_lists f n =
   153      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   154 
   155 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"
   156 where
   157   "mk_map_term T1 T2 domm rng =
   158      (%_. let T1 = T1 ();
   159               T2 = T2 ();
   160               update_term = (%g (a, b).
   161                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   162                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   163                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   164                       Typerep.Typerep (STR ''fun'') [T1,
   165                         Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   166                         g) a) b)
   167           in
   168              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   169 
   170 instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   171 begin
   172 
   173 definition
   174   "check_all f =
   175     (let
   176       mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   177       enum = (Enum.enum :: 'a list)
   178     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)))"
   179 
   180 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   181 where
   182   "enum_term_of_fun = (%_ _. let
   183     enum_term_of_a = enum_term_of (TYPE('a));
   184     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   185   in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   186  
   187 instance ..
   188 
   189 end
   190 
   191 
   192 instantiation unit :: check_all
   193 begin
   194 
   195 definition
   196   "check_all f = f (Code_Evaluation.valtermify ())"
   197 
   198 definition enum_term_of_unit :: "unit itself => unit => term list"
   199 where
   200   "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   201 
   202 instance ..
   203 
   204 end
   205 
   206 
   207 instantiation bool :: check_all
   208 begin
   209 
   210 definition
   211   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   212 
   213 definition enum_term_of_bool :: "bool itself => unit => term list"
   214 where
   215   "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   216 
   217 instance ..
   218 
   219 end
   220 
   221 
   222 instantiation prod :: (check_all, check_all) check_all
   223 begin
   224 
   225 definition
   226   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
   227     %u. let T1 = (Typerep.typerep (TYPE('a)));
   228             T2 = (Typerep.typerep (TYPE('b)))
   229     in Code_Evaluation.App (Code_Evaluation.App (
   230       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   231       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   232       (t1 ())) (t2 ()))))"
   233 
   234 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   235 where
   236   "enum_term_of_prod = (%_ _. map (%(x, y).
   237        let T1 = (Typerep.typerep (TYPE('a)));
   238            T2 = (Typerep.typerep (TYPE('b)))
   239        in Code_Evaluation.App (Code_Evaluation.App (
   240          Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   241            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
   242      (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
   243 
   244 instance ..
   245 
   246 end
   247 
   248 
   249 instantiation sum :: (check_all, check_all) check_all
   250 begin
   251 
   252 definition
   253   "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
   254      let T1 = (Typerep.typerep (TYPE('a)));
   255          T2 = (Typerep.typerep (TYPE('b)))
   256        in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   257            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
   258              | None => check_all (%(b, t). f (Inr b, %_. let
   259                  T1 = (Typerep.typerep (TYPE('a)));
   260                  T2 = (Typerep.typerep (TYPE('b)))
   261                in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   262                  (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
   263 
   264 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   265 where
   266   "enum_term_of_sum = (%_ _.
   267      let
   268        T1 = (Typerep.typerep (TYPE('a)));
   269        T2 = (Typerep.typerep (TYPE('b)))
   270      in
   271        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   272              (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   273              (enum_term_of (TYPE('a)) ()) @
   274        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   275              (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   276              (enum_term_of (TYPE('b)) ()))"
   277 
   278 instance ..
   279 
   280 end
   281 
   282 instantiation nibble :: check_all
   283 begin
   284 
   285 definition
   286   "check_all f =
   287     f (Code_Evaluation.valtermify Nibble0) orelse
   288     f (Code_Evaluation.valtermify Nibble1) orelse
   289     f (Code_Evaluation.valtermify Nibble2) orelse
   290     f (Code_Evaluation.valtermify Nibble3) orelse
   291     f (Code_Evaluation.valtermify Nibble4) orelse
   292     f (Code_Evaluation.valtermify Nibble5) orelse
   293     f (Code_Evaluation.valtermify Nibble6) orelse
   294     f (Code_Evaluation.valtermify Nibble7) orelse
   295     f (Code_Evaluation.valtermify Nibble8) orelse
   296     f (Code_Evaluation.valtermify Nibble9) orelse
   297     f (Code_Evaluation.valtermify NibbleA) orelse
   298     f (Code_Evaluation.valtermify NibbleB) orelse
   299     f (Code_Evaluation.valtermify NibbleC) orelse
   300     f (Code_Evaluation.valtermify NibbleD) orelse
   301     f (Code_Evaluation.valtermify NibbleE) orelse
   302     f (Code_Evaluation.valtermify NibbleF)"
   303 
   304 definition enum_term_of_nibble :: "nibble itself => unit => term list"
   305 where
   306   "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   307 
   308 instance ..
   309 
   310 end
   311 
   312 
   313 instantiation char :: check_all
   314 begin
   315 
   316 definition
   317   "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 ()))))"
   318 
   319 definition enum_term_of_char :: "char itself => unit => term list"
   320 where
   321   "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   322 
   323 instance ..
   324 
   325 end
   326 
   327 
   328 instantiation option :: (check_all) check_all
   329 begin
   330 
   331 definition
   332   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   333     (Code_Evaluation.Const (STR ''Option.option.Some'')
   334       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   335 
   336 definition enum_term_of_option :: "'a option itself => unit => term list"
   337 where
   338   "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
   339       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
   340 
   341 instance ..
   342 
   343 end
   344 
   345 
   346 instantiation Enum.finite_1 :: check_all
   347 begin
   348 
   349 definition
   350   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
   351 
   352 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   353 where
   354   "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
   355 
   356 instance ..
   357 
   358 end
   359 
   360 instantiation Enum.finite_2 :: check_all
   361 begin
   362 
   363 definition
   364   "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))"
   365 
   366 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   367 where
   368   "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   369 
   370 instance ..
   371 
   372 end
   373 
   374 instantiation Enum.finite_3 :: check_all
   375 begin
   376 
   377 definition
   378   "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)))"
   379 
   380 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   381 where
   382   "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   383 
   384 instance ..
   385 
   386 end
   387 
   388 subsection {* Bounded universal quantifiers *}
   389 
   390 class bounded_forall =
   391   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
   392 
   393 subsection {* Defining combinators for any first-order data type *}
   394 
   395 definition catch_match :: "term list option => term list option => term list option"
   396 where
   397   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
   398 
   399 code_const catch_match 
   400   (Quickcheck "(_) handle Match => _")
   401 
   402 use "Tools/Quickcheck/exhaustive_generators.ML"
   403 
   404 setup {* Exhaustive_Generators.setup *}
   405 
   406 declare [[quickcheck_tester = exhaustive]]
   407 
   408 hide_fact orelse_def catch_match_def
   409 no_notation orelse (infixr "orelse" 55)
   410 hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   411 
   412 end