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