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