src/HOL/Quickcheck_Exhaustive.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58152 6fe60a9a5bad
child 58310 91ea607a34d8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* A simple counterexample generator performing exhaustive testing *}
     4 
     5 theory Quickcheck_Exhaustive
     6 imports Quickcheck_Random
     7 keywords "quickcheck_generator" :: thy_decl
     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> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    20   
    21 class full_exhaustive = term_of +
    22   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    23 
    24 instantiation natural :: full_exhaustive
    25 begin
    26 
    27 function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
    28   where "full_exhaustive_natural' f d i =
    29     (if d < i then None
    30     else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
    31 by pat_completeness auto
    32 
    33 termination
    34   by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    35     (auto simp add: less_natural_def)
    36 
    37 definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
    38 
    39 instance ..
    40 
    41 end
    42 
    43 instantiation natural :: exhaustive
    44 begin
    45 
    46 function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option"
    47   where "exhaustive_natural' f d i =
    48     (if d < i then None
    49     else (f i orelse exhaustive_natural' f d (i + 1)))"
    50 by pat_completeness auto
    51 
    52 termination
    53   by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    54     (auto simp add: less_natural_def)
    55 
    56 definition "exhaustive f d = exhaustive_natural' f d 0"
    57 
    58 instance ..
    59 
    60 end
    61 
    62 instantiation integer :: exhaustive
    63 begin
    64 
    65 function exhaustive_integer' :: "(integer => (bool * term list) option) => integer => integer => (bool * term list) option"
    66   where "exhaustive_integer' f d i = (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
    67 by pat_completeness auto
    68 
    69 termination 
    70   by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
    71     (auto simp add: less_integer_def nat_of_integer_def)
    72 
    73 definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    74 
    75 instance ..
    76 
    77 end
    78 
    79 instantiation integer :: full_exhaustive
    80 begin
    81 
    82 function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option"
    83   where "full_exhaustive_integer' 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_integer' f d (i + 1)))"
    84 by pat_completeness auto
    85 
    86 termination 
    87   by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
    88     (auto simp add: less_integer_def nat_of_integer_def)
    89 
    90 definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    91 
    92 instance ..
    93 
    94 end
    95 
    96 instantiation nat :: exhaustive
    97 begin
    98 
    99 definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d"
   100 
   101 instance ..
   102 
   103 end
   104 
   105 instantiation nat :: full_exhaustive
   106 begin
   107 
   108 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d"
   109 
   110 instance ..
   111 
   112 end
   113 
   114 instantiation int :: exhaustive
   115 begin
   116 
   117 function exhaustive_int' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
   118   where "exhaustive_int' f d i = (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
   119 by pat_completeness auto
   120 
   121 termination 
   122   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   123 
   124 definition "exhaustive f d = exhaustive_int' f (int_of_integer (integer_of_natural d))
   125   (- (int_of_integer (integer_of_natural d)))"
   126 
   127 instance ..
   128 
   129 end
   130 
   131 instantiation int :: full_exhaustive
   132 begin
   133 
   134 function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
   135   where "full_exhaustive_int' 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_int' f d (i + 1)))"
   136 by pat_completeness auto
   137 
   138 termination 
   139   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   140 
   141 definition "full_exhaustive f d = full_exhaustive_int' f (int_of_integer (integer_of_natural d))
   142   (- (int_of_integer (integer_of_natural d)))"
   143 
   144 instance ..
   145 
   146 end
   147 
   148 instantiation prod :: (exhaustive, exhaustive) exhaustive
   149 begin
   150 
   151 definition
   152   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
   153 
   154 instance ..
   155 
   156 end
   157 
   158 definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\<cdot>} x {\<cdot>} y"
   159 
   160 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
   161 begin
   162 
   163 definition
   164   "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d"
   165 
   166 instance ..
   167 
   168 end
   169 
   170 instantiation set :: (exhaustive) exhaustive
   171 begin
   172 
   173 fun exhaustive_set
   174 where
   175   "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
   176 
   177 instance ..
   178 
   179 end
   180 
   181 instantiation set :: (full_exhaustive) full_exhaustive
   182 begin
   183 
   184 fun full_exhaustive_set 
   185 where
   186   "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))"
   187 
   188 instance ..
   189 
   190 end
   191 
   192 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   193 begin
   194 
   195 fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option"
   196 where
   197   "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   198    orelse (if i > 1 then
   199      exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   200        f (g(a := b))) d) d) (i - 1) d else None)"
   201 
   202 definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => natural => (bool * term list) option"
   203 where
   204   "exhaustive_fun f d = exhaustive_fun' f d d" 
   205 
   206 instance ..
   207 
   208 end
   209 
   210 definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
   211 
   212 definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
   213 
   214 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
   215 begin
   216 
   217 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
   218 where
   219   "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
   220    orelse (if i > 1 then
   221      full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
   222        f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
   223 
   224 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
   225 where
   226   "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   227 
   228 instance ..
   229 
   230 end
   231 
   232 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   233 
   234 class check_all = enum + term_of +
   235   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
   236   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   237   
   238 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   239 where
   240   "check_all_n_lists f n =
   241      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   242 
   243 definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
   244 
   245 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"
   246 where
   247   "mk_map_term T1 T2 domm rng =
   248      (%_. let T1 = T1 ();
   249               T2 = T2 ();
   250               update_term = (%g (a, b).
   251                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   252                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   253                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   254                       Typerep.Typerep (STR ''fun'') [T1,
   255                         Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   256                         g) a) b)
   257           in
   258              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   259 
   260 instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   261 begin
   262 
   263 definition
   264   "check_all f =
   265     (let
   266       mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   267       enum = (Enum.enum :: 'a list)
   268     in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (natural_of_nat (length enum)))"
   269 
   270 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   271 where
   272   "enum_term_of_fun = (%_ _. let
   273     enum_term_of_a = enum_term_of (TYPE('a));
   274     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   275   in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   276  
   277 instance ..
   278 
   279 end
   280 
   281 fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option"
   282 where
   283   "check_all_subsets f [] = f valterm_emptyset"
   284 | "check_all_subsets f (x # xs) = check_all_subsets (%s. case f s of Some ts => Some ts | None => f (valtermify_insert x s)) xs"
   285 
   286 
   287 definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
   288 definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set)  <\<cdot>> x <\<cdot>> s"
   289 
   290 definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
   291 where
   292   "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
   293 
   294 instantiation set :: (check_all) check_all
   295 begin
   296 
   297 definition
   298   "check_all_set f =
   299      check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
   300 
   301 definition enum_term_of_set :: "'a set itself => unit => term list"
   302 where
   303   "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
   304 
   305 instance ..
   306 
   307 end
   308 
   309 instantiation unit :: check_all
   310 begin
   311 
   312 definition
   313   "check_all f = f (Code_Evaluation.valtermify ())"
   314 
   315 definition enum_term_of_unit :: "unit itself => unit => term list"
   316 where
   317   "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   318 
   319 instance ..
   320 
   321 end
   322 
   323 
   324 instantiation bool :: check_all
   325 begin
   326 
   327 definition
   328   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   329 
   330 definition enum_term_of_bool :: "bool itself => unit => term list"
   331 where
   332   "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   333 
   334 instance ..
   335 
   336 end
   337 
   338 definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\<cdot>> x <\<cdot>> y"
   339 
   340 instantiation prod :: (check_all, check_all) check_all
   341 begin
   342 
   343 definition
   344   "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))"
   345 
   346 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   347 where
   348   "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
   349      (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   350 
   351 instance ..
   352 
   353 end
   354 
   355 definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x"
   356 definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x"
   357 
   358 instantiation sum :: (check_all, check_all) check_all
   359 begin
   360 
   361 definition
   362   "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))"
   363 
   364 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   365 where
   366   "enum_term_of_sum = (%_ _.
   367      let
   368        T1 = (Typerep.typerep (TYPE('a)));
   369        T2 = (Typerep.typerep (TYPE('b)))
   370      in
   371        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   372              (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   373              (enum_term_of (TYPE('a)) ()) @
   374        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   375              (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   376              (enum_term_of (TYPE('b)) ()))"
   377 
   378 instance ..
   379 
   380 end
   381 
   382 instantiation nibble :: check_all
   383 begin
   384 
   385 definition
   386   "check_all f =
   387     f (Code_Evaluation.valtermify Nibble0) orelse
   388     f (Code_Evaluation.valtermify Nibble1) orelse
   389     f (Code_Evaluation.valtermify Nibble2) orelse
   390     f (Code_Evaluation.valtermify Nibble3) orelse
   391     f (Code_Evaluation.valtermify Nibble4) orelse
   392     f (Code_Evaluation.valtermify Nibble5) orelse
   393     f (Code_Evaluation.valtermify Nibble6) orelse
   394     f (Code_Evaluation.valtermify Nibble7) orelse
   395     f (Code_Evaluation.valtermify Nibble8) orelse
   396     f (Code_Evaluation.valtermify Nibble9) orelse
   397     f (Code_Evaluation.valtermify NibbleA) orelse
   398     f (Code_Evaluation.valtermify NibbleB) orelse
   399     f (Code_Evaluation.valtermify NibbleC) orelse
   400     f (Code_Evaluation.valtermify NibbleD) orelse
   401     f (Code_Evaluation.valtermify NibbleE) orelse
   402     f (Code_Evaluation.valtermify NibbleF)"
   403 
   404 definition enum_term_of_nibble :: "nibble itself => unit => term list"
   405 where
   406   "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   407 
   408 instance ..
   409 
   410 end
   411 
   412 
   413 instantiation char :: check_all
   414 begin
   415 
   416 definition
   417   "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 ()))))"
   418 
   419 definition enum_term_of_char :: "char itself => unit => term list"
   420 where
   421   "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   422 
   423 instance ..
   424 
   425 end
   426 
   427 
   428 instantiation option :: (check_all) check_all
   429 begin
   430 
   431 definition
   432   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   433     (Code_Evaluation.Const (STR ''Option.option.Some'')
   434       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   435 
   436 definition enum_term_of_option :: "'a option itself => unit => term list"
   437 where
   438   "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
   439       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
   440 
   441 instance ..
   442 
   443 end
   444 
   445 
   446 instantiation Enum.finite_1 :: check_all
   447 begin
   448 
   449 definition
   450   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
   451 
   452 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   453 where
   454   "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
   455 
   456 instance ..
   457 
   458 end
   459 
   460 instantiation Enum.finite_2 :: check_all
   461 begin
   462 
   463 definition
   464   "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
   465     orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
   466 
   467 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   468 where
   469   "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   470 
   471 instance ..
   472 
   473 end
   474 
   475 instantiation Enum.finite_3 :: check_all
   476 begin
   477 
   478 definition
   479   "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
   480     orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
   481     orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
   482 
   483 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   484 where
   485   "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   486 
   487 instance ..
   488 
   489 end
   490 
   491 instantiation Enum.finite_4 :: check_all
   492 begin
   493 
   494 definition
   495   "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
   496     orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
   497     orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
   498     orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
   499 
   500 definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
   501 where
   502   "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
   503 
   504 instance ..
   505 
   506 end
   507 
   508 subsection {* Bounded universal quantifiers *}
   509 
   510 class bounded_forall =
   511   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
   512 
   513 subsection {* Fast exhaustive combinators *}
   514 
   515 class fast_exhaustive = term_of +
   516   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
   517 
   518 axiomatization throw_Counterexample :: "term list => unit"
   519 axiomatization catch_Counterexample :: "unit => term list option"
   520 
   521 code_printing
   522   constant throw_Counterexample \<rightharpoonup>
   523     (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
   524 | constant catch_Counterexample \<rightharpoonup>
   525     (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
   526 
   527 subsection {* Continuation passing style functions as plus monad *}
   528   
   529 type_synonym 'a cps = "('a => term list option) => term list option"
   530 
   531 definition cps_empty :: "'a cps"
   532 where
   533   "cps_empty = (%cont. None)"
   534 
   535 definition cps_single :: "'a => 'a cps"
   536 where
   537   "cps_single v = (%cont. cont v)"
   538 
   539 definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
   540 where
   541   "cps_bind m f = (%cont. m (%a. (f a) cont))"
   542 
   543 definition cps_plus :: "'a cps => 'a cps => 'a cps"
   544 where
   545   "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
   546 
   547 definition cps_if :: "bool => unit cps"
   548 where
   549   "cps_if b = (if b then cps_single () else cps_empty)"
   550 
   551 definition cps_not :: "unit cps => unit cps"
   552 where
   553   "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
   554 
   555 type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => natural => (bool * term list) option"
   556 
   557 definition pos_bound_cps_empty :: "'a pos_bound_cps"
   558 where
   559   "pos_bound_cps_empty = (%cont i. None)"
   560 
   561 definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
   562 where
   563   "pos_bound_cps_single v = (%cont i. cont v)"
   564 
   565 definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
   566 where
   567   "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
   568 
   569 definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
   570 where
   571   "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
   572 
   573 definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
   574 where
   575   "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   576 
   577 datatype_new (dead 'a) unknown = Unknown | Known 'a
   578 datatype_new (dead 'a) three_valued = Unknown_value | Value 'a | No_value
   579 
   580 type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
   581 
   582 definition neg_bound_cps_empty :: "'a neg_bound_cps"
   583 where
   584   "neg_bound_cps_empty = (%cont i. No_value)"
   585 
   586 definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
   587 where
   588   "neg_bound_cps_single v = (%cont i. cont (Known v))"
   589 
   590 definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
   591 where
   592   "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
   593 
   594 definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
   595 where
   596   "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))"
   597 
   598 definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
   599 where
   600   "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   601 
   602 definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
   603 where
   604   "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
   605 
   606 definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
   607 where
   608   "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
   609 
   610 subsection {* Defining generators for any first-order data type *}
   611 
   612 axiomatization unknown :: 'a
   613 
   614 notation (output) unknown  ("?")
   615 
   616 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   617 
   618 setup {* Exhaustive_Generators.setup *}
   619 
   620 declare [[quickcheck_batch_tester = exhaustive]]
   621 
   622 subsection {* Defining generators for abstract types *}
   623 
   624 ML_file "Tools/Quickcheck/abstract_generators.ML"
   625 
   626 hide_fact (open) orelse_def
   627 no_notation orelse (infixr "orelse" 55)
   628 
   629 hide_fact
   630   exhaustive_int'_def
   631   exhaustive_integer'_def
   632   exhaustive_natural'_def
   633 
   634 hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
   635   valtermify_Inl valtermify_Inr
   636   termify_fun_upd term_emptyset termify_insert termify_pair setify
   637 
   638 hide_const (open)
   639   exhaustive full_exhaustive
   640   exhaustive_int' full_exhaustive_int'
   641   exhaustive_integer' full_exhaustive_integer'
   642   exhaustive_natural' full_exhaustive_natural'
   643   throw_Counterexample catch_Counterexample
   644   check_all enum_term_of
   645   orelse unknown mk_map_term check_all_n_lists check_all_subsets
   646 
   647 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   648 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   649   pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   650   neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   651   Unknown Known Unknown_value Value No_value
   652 
   653 end