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