src/HOL/Quickcheck_Exhaustive.thy
author bulwahn
Sun Dec 04 20:05:08 2011 +0100 (2011-12-04)
changeset 45750 17100f4ce0b5
parent 45733 6bb30ae1abfe
child 45818 53a697f5454a
permissions -rw-r--r--
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
     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> (bool * term list) option) \<Rightarrow> code_numeral \<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> code_numeral \<Rightarrow> (bool * term list) option"
    23 
    24 instantiation code_numeral :: full_exhaustive
    25 begin
    26 
    27 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    28   where "full_exhaustive_code_numeral' f d i =
    29     (if d < i then None
    30     else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    31 by pat_completeness auto
    32 
    33 termination
    34   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    35 
    36 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    37 
    38 instance ..
    39 
    40 end
    41 
    42 instantiation code_numeral :: exhaustive
    43 begin
    44 
    45 function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    46   where "exhaustive_code_numeral' f d i =
    47     (if d < i then None
    48     else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    49 by pat_completeness auto
    50 
    51 termination
    52   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    53 
    54 definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    55 
    56 instance ..
    57 
    58 end
    59 
    60 instantiation nat :: exhaustive
    61 begin
    62 
    63 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
    64 
    65 instance ..
    66 
    67 end
    68 
    69 instantiation nat :: full_exhaustive
    70 begin
    71 
    72 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"
    73 
    74 instance ..
    75 
    76 end
    77 
    78 instantiation int :: exhaustive
    79 begin
    80 
    81 function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
    82   where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    83 by pat_completeness auto
    84 
    85 termination 
    86   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    87 
    88 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    89 
    90 instance ..
    91 
    92 end
    93 
    94 instantiation int :: full_exhaustive
    95 begin
    96 
    97 function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
    98   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)))"
    99 by pat_completeness auto
   100 
   101 termination 
   102   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   103 
   104 definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   105 
   106 instance ..
   107 
   108 end
   109 
   110 instantiation prod :: (exhaustive, exhaustive) exhaustive
   111 begin
   112 
   113 definition
   114   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
   115 
   116 instance ..
   117 
   118 end
   119 
   120 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
   121 begin
   122 
   123 definition
   124   "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
   125     %u. let T1 = (Typerep.typerep (TYPE('a)));
   126             T2 = (Typerep.typerep (TYPE('b)))
   127     in Code_Evaluation.App (Code_Evaluation.App (
   128       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   129       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   130       (t1 ())) (t2 ()))) d) d"
   131 
   132 instance ..
   133 
   134 end
   135 
   136 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   137 begin
   138 
   139 fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   140 where
   141   "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   142    orelse (if i > 1 then
   143      exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   144        f (g(a := b))) d) d) (i - 1) d else None)"
   145 
   146 definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
   147 where
   148   "exhaustive_fun f d = exhaustive_fun' f d d" 
   149 
   150 instance ..
   151 
   152 end
   153 
   154 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
   155 begin
   156 
   157 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   158 where
   159   "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   160    orelse (if i > 1 then
   161      full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
   162        f (g(a := b),
   163          (%_. let A = (Typerep.typerep (TYPE('a)));
   164                   B = (Typerep.typerep (TYPE('b)));
   165                   fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
   166               in
   167                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   168                   (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
   169                 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
   170 
   171 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   172 where
   173   "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   174 
   175 instance ..
   176 
   177 end
   178 
   179 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   180 
   181 class check_all = enum + term_of +
   182   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
   183   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   184   
   185 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
   186 where
   187   "check_all_n_lists f n =
   188      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   189 
   190 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"
   191 where
   192   "mk_map_term T1 T2 domm rng =
   193      (%_. let T1 = T1 ();
   194               T2 = T2 ();
   195               update_term = (%g (a, b).
   196                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   197                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   198                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   199                       Typerep.Typerep (STR ''fun'') [T1,
   200                         Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   201                         g) a) b)
   202           in
   203              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   204 
   205 instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   206 begin
   207 
   208 definition
   209   "check_all f =
   210     (let
   211       mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   212       enum = (Enum.enum :: 'a list)
   213     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)))"
   214 
   215 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   216 where
   217   "enum_term_of_fun = (%_ _. let
   218     enum_term_of_a = enum_term_of (TYPE('a));
   219     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   220   in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   221  
   222 instance ..
   223 
   224 end
   225 
   226 
   227 instantiation unit :: check_all
   228 begin
   229 
   230 definition
   231   "check_all f = f (Code_Evaluation.valtermify ())"
   232 
   233 definition enum_term_of_unit :: "unit itself => unit => term list"
   234 where
   235   "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   236 
   237 instance ..
   238 
   239 end
   240 
   241 
   242 instantiation bool :: check_all
   243 begin
   244 
   245 definition
   246   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   247 
   248 definition enum_term_of_bool :: "bool itself => unit => term list"
   249 where
   250   "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   251 
   252 instance ..
   253 
   254 end
   255 
   256 
   257 instantiation prod :: (check_all, check_all) check_all
   258 begin
   259 
   260 definition
   261   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
   262     %u. let T1 = (Typerep.typerep (TYPE('a)));
   263             T2 = (Typerep.typerep (TYPE('b)))
   264     in Code_Evaluation.App (Code_Evaluation.App (
   265       Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   266       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
   267       (t1 ())) (t2 ()))))"
   268 
   269 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   270 where
   271   "enum_term_of_prod = (%_ _. map (%(x, y).
   272        let T1 = (Typerep.typerep (TYPE('a)));
   273            T2 = (Typerep.typerep (TYPE('b)))
   274        in Code_Evaluation.App (Code_Evaluation.App (
   275          Code_Evaluation.Const (STR ''Product_Type.Pair'') 
   276            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
   277      (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
   278 
   279 instance ..
   280 
   281 end
   282 
   283 
   284 instantiation sum :: (check_all, check_all) check_all
   285 begin
   286 
   287 definition
   288   "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
   289      let T1 = (Typerep.typerep (TYPE('a)));
   290          T2 = (Typerep.typerep (TYPE('b)))
   291        in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   292            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
   293              | None => check_all (%(b, t). f (Inr b, %_. let
   294                  T1 = (Typerep.typerep (TYPE('a)));
   295                  T2 = (Typerep.typerep (TYPE('b)))
   296                in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   297                  (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
   298 
   299 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   300 where
   301   "enum_term_of_sum = (%_ _.
   302      let
   303        T1 = (Typerep.typerep (TYPE('a)));
   304        T2 = (Typerep.typerep (TYPE('b)))
   305      in
   306        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   307              (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   308              (enum_term_of (TYPE('a)) ()) @
   309        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   310              (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   311              (enum_term_of (TYPE('b)) ()))"
   312 
   313 instance ..
   314 
   315 end
   316 
   317 instantiation nibble :: check_all
   318 begin
   319 
   320 definition
   321   "check_all f =
   322     f (Code_Evaluation.valtermify Nibble0) orelse
   323     f (Code_Evaluation.valtermify Nibble1) orelse
   324     f (Code_Evaluation.valtermify Nibble2) orelse
   325     f (Code_Evaluation.valtermify Nibble3) orelse
   326     f (Code_Evaluation.valtermify Nibble4) orelse
   327     f (Code_Evaluation.valtermify Nibble5) orelse
   328     f (Code_Evaluation.valtermify Nibble6) orelse
   329     f (Code_Evaluation.valtermify Nibble7) orelse
   330     f (Code_Evaluation.valtermify Nibble8) orelse
   331     f (Code_Evaluation.valtermify Nibble9) orelse
   332     f (Code_Evaluation.valtermify NibbleA) orelse
   333     f (Code_Evaluation.valtermify NibbleB) orelse
   334     f (Code_Evaluation.valtermify NibbleC) orelse
   335     f (Code_Evaluation.valtermify NibbleD) orelse
   336     f (Code_Evaluation.valtermify NibbleE) orelse
   337     f (Code_Evaluation.valtermify NibbleF)"
   338 
   339 definition enum_term_of_nibble :: "nibble itself => unit => term list"
   340 where
   341   "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   342 
   343 instance ..
   344 
   345 end
   346 
   347 
   348 instantiation char :: check_all
   349 begin
   350 
   351 definition
   352   "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 ()))))"
   353 
   354 definition enum_term_of_char :: "char itself => unit => term list"
   355 where
   356   "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   357 
   358 instance ..
   359 
   360 end
   361 
   362 
   363 instantiation option :: (check_all) check_all
   364 begin
   365 
   366 definition
   367   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   368     (Code_Evaluation.Const (STR ''Option.option.Some'')
   369       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   370 
   371 definition enum_term_of_option :: "'a option itself => unit => term list"
   372 where
   373   "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
   374       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
   375 
   376 instance ..
   377 
   378 end
   379 
   380 
   381 instantiation Enum.finite_1 :: check_all
   382 begin
   383 
   384 definition
   385   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
   386 
   387 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   388 where
   389   "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
   390 
   391 instance ..
   392 
   393 end
   394 
   395 instantiation Enum.finite_2 :: check_all
   396 begin
   397 
   398 definition
   399   "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))"
   400 
   401 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   402 where
   403   "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   404 
   405 instance ..
   406 
   407 end
   408 
   409 instantiation Enum.finite_3 :: check_all
   410 begin
   411 
   412 definition
   413   "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)))"
   414 
   415 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   416 where
   417   "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   418 
   419 instance ..
   420 
   421 end
   422 
   423 subsection {* Bounded universal quantifiers *}
   424 
   425 class bounded_forall =
   426   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
   427 
   428 subsection {* Fast exhaustive combinators *}
   429 
   430 class fast_exhaustive = term_of +
   431   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
   432 
   433 consts throw_Counterexample :: "term list => unit"
   434 consts catch_Counterexample :: "unit => term list option"
   435 
   436 code_const throw_Counterexample
   437   (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
   438 code_const catch_Counterexample
   439   (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
   440 
   441 subsection {* Continuation passing style functions as plus monad *}
   442   
   443 type_synonym 'a cps = "('a => term list option) => term list option"
   444 
   445 definition cps_empty :: "'a cps"
   446 where
   447   "cps_empty = (%cont. None)"
   448 
   449 definition cps_single :: "'a => 'a cps"
   450 where
   451   "cps_single v = (%cont. cont v)"
   452 
   453 definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
   454 where
   455   "cps_bind m f = (%cont. m (%a. (f a) cont))"
   456 
   457 definition cps_plus :: "'a cps => 'a cps => 'a cps"
   458 where
   459   "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
   460 
   461 definition cps_if :: "bool => unit cps"
   462 where
   463   "cps_if b = (if b then cps_single () else cps_empty)"
   464 
   465 definition cps_not :: "unit cps => unit cps"
   466 where
   467   "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
   468 
   469 type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
   470 
   471 definition pos_bound_cps_empty :: "'a pos_bound_cps"
   472 where
   473   "pos_bound_cps_empty = (%cont i. None)"
   474 
   475 definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
   476 where
   477   "pos_bound_cps_single v = (%cont i. cont v)"
   478 
   479 definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
   480 where
   481   "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
   482 
   483 definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
   484 where
   485   "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
   486 
   487 definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
   488 where
   489   "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   490 
   491 datatype 'a unknown = Unknown | Known 'a
   492 datatype 'a three_valued = Unknown_value | Value 'a | No_value
   493 
   494 type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
   495 
   496 definition neg_bound_cps_empty :: "'a neg_bound_cps"
   497 where
   498   "neg_bound_cps_empty = (%cont i. No_value)"
   499 
   500 definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
   501 where
   502   "neg_bound_cps_single v = (%cont i. cont (Known v))"
   503 
   504 definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
   505 where
   506   "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))"
   507 
   508 definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
   509 where
   510   "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))"
   511 
   512 definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
   513 where
   514   "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   515 
   516 definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
   517 where
   518   "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
   519 
   520 definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
   521 where
   522   "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
   523 
   524 subsection {* Defining combinators for any first-order data type *}
   525 
   526 axiomatization unknown :: 'a
   527 
   528 notation (output) unknown  ("?")
   529  
   530 use "Tools/Quickcheck/exhaustive_generators.ML"
   531 
   532 setup {* Exhaustive_Generators.setup *}
   533 
   534 declare [[quickcheck_batch_tester = exhaustive]]
   535 
   536 hide_fact orelse_def
   537 no_notation orelse (infixr "orelse" 55)
   538 hide_const (open) orelse unknown mk_map_term check_all_n_lists 
   539 
   540 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   541 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   542   pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   543   neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   544   Unknown Known Unknown_value Value No_value
   545 
   546 end