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