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