src/HOL/Quickcheck_Exhaustive.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 65956 639eb3617a86
child 67076 fc877448602e
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Quickcheck_Exhaustive.thy
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 section \<open>A simple counterexample generator performing exhaustive testing\<close>
     6 
     7 theory Quickcheck_Exhaustive
     8 imports Quickcheck_Random
     9 keywords "quickcheck_generator" :: thy_decl
    10 begin
    11 
    12 subsection \<open>Basic operations for exhaustive generators\<close>
    13 
    14 definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"  (infixr "orelse" 55)
    15   where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)"
    16 
    17 
    18 subsection \<open>Exhaustive generator type classes\<close>
    19 
    20 class exhaustive = term_of +
    21   fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    22 
    23 class full_exhaustive = term_of +
    24   fixes full_exhaustive ::
    25     "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    26 
    27 instantiation natural :: full_exhaustive
    28 begin
    29 
    30 function full_exhaustive_natural' ::
    31     "(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
    32       natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    33   where "full_exhaustive_natural' f d i =
    34     (if d < i then None
    35      else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
    36 by pat_completeness auto
    37 
    38 termination
    39   by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
    40 
    41 definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
    42 
    43 instance ..
    44 
    45 end
    46 
    47 instantiation natural :: exhaustive
    48 begin
    49 
    50 function exhaustive_natural' ::
    51     "(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    52   where "exhaustive_natural' f d i =
    53     (if d < i then None
    54      else (f i orelse exhaustive_natural' f d (i + 1)))"
    55 by pat_completeness auto
    56 
    57 termination
    58   by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
    59 
    60 definition "exhaustive f d = exhaustive_natural' f d 0"
    61 
    62 instance ..
    63 
    64 end
    65 
    66 instantiation integer :: exhaustive
    67 begin
    68 
    69 function exhaustive_integer' ::
    70     "(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
    71   where "exhaustive_integer' f d i =
    72     (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
    73 by pat_completeness auto
    74 
    75 termination
    76   by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
    77     (auto simp add: less_integer_def nat_of_integer_def)
    78 
    79 definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    80 
    81 instance ..
    82 
    83 end
    84 
    85 instantiation integer :: full_exhaustive
    86 begin
    87 
    88 function full_exhaustive_integer' ::
    89     "(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
    90       integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
    91   where "full_exhaustive_integer' f d i =
    92     (if d < i then None
    93      else
    94       (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
    95         Some t \<Rightarrow> Some t
    96       | None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))"
    97 by pat_completeness auto
    98 
    99 termination
   100   by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
   101     (auto simp add: less_integer_def nat_of_integer_def)
   102 
   103 definition "full_exhaustive f d =
   104   full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
   105 
   106 instance ..
   107 
   108 end
   109 
   110 instantiation nat :: exhaustive
   111 begin
   112 
   113 definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d"
   114 
   115 instance ..
   116 
   117 end
   118 
   119 instantiation nat :: full_exhaustive
   120 begin
   121 
   122 definition "full_exhaustive f d =
   123   full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. Code_Evaluation.term_of (nat_of_natural x))) d"
   124 
   125 instance ..
   126 
   127 end
   128 
   129 instantiation int :: exhaustive
   130 begin
   131 
   132 function exhaustive_int' ::
   133     "(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
   134   where "exhaustive_int' f d i =
   135     (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
   136 by pat_completeness auto
   137 
   138 termination
   139   by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
   140 
   141 definition "exhaustive f d =
   142   exhaustive_int' f (int_of_integer (integer_of_natural d))
   143     (- (int_of_integer (integer_of_natural d)))"
   144 
   145 instance ..
   146 
   147 end
   148 
   149 instantiation int :: full_exhaustive
   150 begin
   151 
   152 function full_exhaustive_int' ::
   153     "(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   154       int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
   155   where "full_exhaustive_int' f d i =
   156     (if d < i then None
   157      else
   158       (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
   159         Some t \<Rightarrow> Some t
   160        | None \<Rightarrow> full_exhaustive_int' f d (i + 1)))"
   161 by pat_completeness auto
   162 
   163 termination
   164   by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
   165 
   166 definition "full_exhaustive f d =
   167   full_exhaustive_int' f (int_of_integer (integer_of_natural d))
   168     (- (int_of_integer (integer_of_natural d)))"
   169 
   170 instance ..
   171 
   172 end
   173 
   174 instantiation prod :: (exhaustive, exhaustive) exhaustive
   175 begin
   176 
   177 definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d"
   178 
   179 instance ..
   180 
   181 end
   182 
   183 definition (in term_syntax)
   184   [code_unfold]: "valtermify_pair x y =
   185     Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
   186 
   187 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
   188 begin
   189 
   190 definition "full_exhaustive f d =
   191   full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d"
   192 
   193 instance ..
   194 
   195 end
   196 
   197 instantiation set :: (exhaustive) exhaustive
   198 begin
   199 
   200 fun exhaustive_set
   201 where
   202   "exhaustive_set f i =
   203     (if i = 0 then None
   204      else
   205       f {} orelse
   206       exhaustive_set
   207         (\<lambda>A. f A orelse exhaustive (\<lambda>x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1))"
   208 
   209 instance ..
   210 
   211 end
   212 
   213 instantiation set :: (full_exhaustive) full_exhaustive
   214 begin
   215 
   216 fun full_exhaustive_set
   217 where
   218   "full_exhaustive_set f i =
   219     (if i = 0 then None
   220      else
   221       f valterm_emptyset orelse
   222       full_exhaustive_set
   223         (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive
   224           (\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))"
   225 
   226 instance ..
   227 
   228 end
   229 
   230 instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive
   231 begin
   232 
   233 fun exhaustive_fun' ::
   234   "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   235 where
   236   "exhaustive_fun' f i d =
   237     (exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse
   238       (if i > 1 then
   239         exhaustive_fun'
   240           (\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)"
   241 
   242 definition exhaustive_fun ::
   243   "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   244   where "exhaustive_fun f d = exhaustive_fun' f d d"
   245 
   246 instance ..
   247 
   248 end
   249 
   250 definition [code_unfold]:
   251   "valtermify_absdummy =
   252     (\<lambda>(v, t).
   253       (\<lambda>_::'a. v,
   254         \<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
   255 
   256 definition (in term_syntax)
   257   [code_unfold]: "valtermify_fun_upd g a b =
   258     Code_Evaluation.valtermify
   259       (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
   260 
   261 instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
   262 begin
   263 
   264 fun full_exhaustive_fun' ::
   265   "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   266     natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   267 where
   268   "full_exhaustive_fun' f i d =
   269     full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse
   270     (if i > 1 then
   271       full_exhaustive_fun'
   272         (\<lambda>g. full_exhaustive
   273           (\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d
   274      else None)"
   275 
   276 definition full_exhaustive_fun ::
   277   "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   278     natural \<Rightarrow> (bool \<times> term list) option"
   279   where "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
   280 
   281 instance ..
   282 
   283 end
   284 
   285 subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
   286 
   287 class check_all = enum + term_of +
   288   fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option"
   289   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   290 
   291 fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow>
   292   (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   293 where
   294   "check_all_n_lists f n =
   295     (if n = 0 then f ([], (\<lambda>_. []))
   296      else check_all (\<lambda>(x, xt).
   297       check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
   298 
   299 definition (in term_syntax)
   300   [code_unfold]: "termify_fun_upd g a b =
   301     (Code_Evaluation.termify
   302       (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
   303 
   304 definition mk_map_term ::
   305   "(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
   306     (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
   307   where "mk_map_term T1 T2 domm rng =
   308     (\<lambda>_.
   309       let
   310         T1 = T1 ();
   311         T2 = T2 ();
   312         update_term =
   313           (\<lambda>g (a, b).
   314             Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   315              (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   316                (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   317                   Typerep.Typerep (STR ''fun'') [T1,
   318                     Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   319                     g) a) b)
   320       in
   321         List.foldl update_term
   322           (Code_Evaluation.Abs (STR ''x'') T1
   323             (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   324 
   325 instantiation "fun" :: ("{equal,check_all}", check_all) check_all
   326 begin
   327 
   328 definition
   329   "check_all f =
   330     (let
   331       mk_term =
   332         mk_map_term
   333           (\<lambda>_. Typerep.typerep (TYPE('a)))
   334           (\<lambda>_. Typerep.typerep (TYPE('b)))
   335           (enum_term_of (TYPE('a)));
   336       enum = (Enum.enum :: 'a list)
   337     in
   338       check_all_n_lists
   339         (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst))
   340         (natural_of_nat (length enum)))"
   341 
   342 definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   343   where "enum_term_of_fun =
   344     (\<lambda>_ _.
   345       let
   346         enum_term_of_a = enum_term_of (TYPE('a));
   347         mk_term =
   348           mk_map_term
   349             (\<lambda>_. Typerep.typerep (TYPE('a)))
   350             (\<lambda>_. Typerep.typerep (TYPE('b)))
   351             enum_term_of_a
   352       in
   353         map (\<lambda>ys. mk_term (\<lambda>_. ys) ())
   354           (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   355 
   356 instance ..
   357 
   358 end
   359 
   360 fun (in term_syntax) check_all_subsets ::
   361   "(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   362     ('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
   363 where
   364   "check_all_subsets f [] = f valterm_emptyset"
   365 | "check_all_subsets f (x # xs) =
   366     check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
   367 
   368 
   369 definition (in term_syntax)
   370   [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
   371 
   372 definition (in term_syntax)
   373   [code_unfold]: "termify_insert x s =
   374     Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set)  <\<cdot>> x <\<cdot>> s"
   375 
   376 definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
   377 where
   378   "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
   379 
   380 instantiation set :: (check_all) check_all
   381 begin
   382 
   383 definition
   384   "check_all_set f =
   385      check_all_subsets f
   386       (zip (Enum.enum :: 'a list)
   387         (map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
   388 
   389 definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
   390   where "enum_term_of_set _ _ =
   391     map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
   392 
   393 instance ..
   394 
   395 end
   396 
   397 instantiation unit :: check_all
   398 begin
   399 
   400 definition "check_all f = f (Code_Evaluation.valtermify ())"
   401 
   402 definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list"
   403   where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])"
   404 
   405 instance ..
   406 
   407 end
   408 
   409 
   410 instantiation bool :: check_all
   411 begin
   412 
   413 definition
   414   "check_all f =
   415     (case f (Code_Evaluation.valtermify False) of
   416       Some x' \<Rightarrow> Some x'
   417     | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   418 
   419 definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list"
   420   where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   421 
   422 instance ..
   423 
   424 end
   425 
   426 definition (in term_syntax) [code_unfold]:
   427   "termify_pair x y =
   428     Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y"
   429 
   430 instantiation prod :: (check_all, check_all) check_all
   431 begin
   432 
   433 definition "check_all f = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))"
   434 
   435 definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   436   where "enum_term_of_prod =
   437     (\<lambda>_ _.
   438       map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y)
   439         (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   440 
   441 instance ..
   442 
   443 end
   444 
   445 definition (in term_syntax)
   446   [code_unfold]: "valtermify_Inl x =
   447     Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
   448 
   449 definition (in term_syntax)
   450   [code_unfold]: "valtermify_Inr x =
   451     Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
   452 
   453 instantiation sum :: (check_all, check_all) check_all
   454 begin
   455 
   456 definition
   457   "check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))"
   458 
   459 definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   460   where "enum_term_of_sum =
   461     (\<lambda>_ _.
   462       let
   463         T1 = Typerep.typerep (TYPE('a));
   464         T2 = Typerep.typerep (TYPE('b))
   465       in
   466         map
   467           (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
   468             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   469           (enum_term_of (TYPE('a)) ()) @
   470         map
   471           (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
   472             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   473           (enum_term_of (TYPE('b)) ()))"
   474 
   475 instance ..
   476 
   477 end
   478 
   479 instantiation char :: check_all
   480 begin
   481 
   482 primrec check_all_char' ::
   483   "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option"
   484   where "check_all_char' f [] = None"
   485   | "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c)
   486       orelse check_all_char' f cs"
   487 
   488 definition check_all_char ::
   489   "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option"
   490   where "check_all f = check_all_char' f Enum.enum"
   491 
   492 definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
   493 where
   494   "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   495 
   496 instance ..
   497 
   498 end
   499 
   500 instantiation option :: (check_all) check_all
   501 begin
   502 
   503 definition
   504   "check_all f =
   505     f (Code_Evaluation.valtermify (None :: 'a option)) orelse
   506     check_all
   507       (\<lambda>(x, t).
   508         f
   509           (Some x,
   510             \<lambda>_. Code_Evaluation.App
   511               (Code_Evaluation.Const (STR ''Option.option.Some'')
   512                 (Typerep.Typerep (STR ''fun'')
   513                 [Typerep.typerep TYPE('a),
   514                  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   515 
   516 definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list"
   517   where "enum_term_of_option =
   518     (\<lambda> _ _.
   519       Code_Evaluation.term_of (None :: 'a option) #
   520       (map
   521         (Code_Evaluation.App
   522           (Code_Evaluation.Const (STR ''Option.option.Some'')
   523             (Typerep.Typerep (STR ''fun'')
   524               [Typerep.typerep TYPE('a),
   525                Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
   526         (enum_term_of (TYPE('a)) ())))"
   527 
   528 instance ..
   529 
   530 end
   531 
   532 
   533 instantiation Enum.finite_1 :: check_all
   534 begin
   535 
   536 definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
   537 
   538 definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list"
   539   where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
   540 
   541 instance ..
   542 
   543 end
   544 
   545 instantiation Enum.finite_2 :: check_all
   546 begin
   547 
   548 definition
   549   "check_all f =
   550     (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse
   551      f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
   552 
   553 definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list"
   554   where "enum_term_of_finite_2 =
   555     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   556 
   557 instance ..
   558 
   559 end
   560 
   561 instantiation Enum.finite_3 :: check_all
   562 begin
   563 
   564 definition
   565   "check_all f =
   566     (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse
   567      f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse
   568      f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
   569 
   570 definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list"
   571   where "enum_term_of_finite_3 =
   572     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   573 
   574 instance ..
   575 
   576 end
   577 
   578 instantiation Enum.finite_4 :: check_all
   579 begin
   580 
   581 definition
   582   "check_all f =
   583     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse
   584     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse
   585     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse
   586     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)"
   587 
   588 definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list"
   589   where "enum_term_of_finite_4 =
   590     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
   591 
   592 instance ..
   593 
   594 end
   595 
   596 subsection \<open>Bounded universal quantifiers\<close>
   597 
   598 class bounded_forall =
   599   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
   600 
   601 
   602 subsection \<open>Fast exhaustive combinators\<close>
   603 
   604 class fast_exhaustive = term_of +
   605   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
   606 
   607 axiomatization throw_Counterexample :: "term list \<Rightarrow> unit"
   608 axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option"
   609 
   610 code_printing
   611   constant throw_Counterexample \<rightharpoonup>
   612     (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
   613 | constant catch_Counterexample \<rightharpoonup>
   614     (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)"
   615 
   616 
   617 subsection \<open>Continuation passing style functions as plus monad\<close>
   618 
   619 type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option"
   620 
   621 definition cps_empty :: "'a cps"
   622   where "cps_empty = (\<lambda>cont. None)"
   623 
   624 definition cps_single :: "'a \<Rightarrow> 'a cps"
   625   where "cps_single v = (\<lambda>cont. cont v)"
   626 
   627 definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps"
   628   where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))"
   629 
   630 definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps"
   631   where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)"
   632 
   633 definition cps_if :: "bool \<Rightarrow> unit cps"
   634   where "cps_if b = (if b then cps_single () else cps_empty)"
   635 
   636 definition cps_not :: "unit cps \<Rightarrow> unit cps"
   637   where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)"
   638 
   639 type_synonym 'a pos_bound_cps =
   640   "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   641 
   642 definition pos_bound_cps_empty :: "'a pos_bound_cps"
   643   where "pos_bound_cps_empty = (\<lambda>cont i. None)"
   644 
   645 definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps"
   646   where "pos_bound_cps_single v = (\<lambda>cont i. cont v)"
   647 
   648 definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps"
   649   where "pos_bound_cps_bind m f = (\<lambda>cont i. if i = 0 then None else (m (\<lambda>a. (f a) cont i) (i - 1)))"
   650 
   651 definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps"
   652   where "pos_bound_cps_plus a b = (\<lambda>c i. case a c i of None \<Rightarrow> b c i | Some x \<Rightarrow> Some x)"
   653 
   654 definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps"
   655   where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   656 
   657 datatype (plugins only: code extraction) (dead 'a) unknown =
   658   Unknown | Known 'a
   659 
   660 datatype (plugins only: code extraction) (dead 'a) three_valued =
   661   Unknown_value | Value 'a | No_value
   662 
   663 type_synonym 'a neg_bound_cps =
   664   "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued"
   665 
   666 definition neg_bound_cps_empty :: "'a neg_bound_cps"
   667   where "neg_bound_cps_empty = (\<lambda>cont i. No_value)"
   668 
   669 definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps"
   670   where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))"
   671 
   672 definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps"
   673   where "neg_bound_cps_bind m f =
   674     (\<lambda>cont i.
   675       if i = 0 then cont Unknown
   676       else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))"
   677 
   678 definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps"
   679   where "neg_bound_cps_plus a b =
   680     (\<lambda>c i.
   681       case a c i of
   682         No_value \<Rightarrow> b c i
   683       | Value x \<Rightarrow> Value x
   684       | Unknown_value \<Rightarrow>
   685           (case b c i of
   686             No_value \<Rightarrow> Unknown_value
   687           | Value x \<Rightarrow> Value x
   688           | Unknown_value \<Rightarrow> Unknown_value))"
   689 
   690 definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps"
   691   where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   692 
   693 definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps"
   694   where "neg_bound_cps_not n =
   695     (\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)"
   696 
   697 definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps"
   698   where "pos_bound_cps_not n =
   699     (\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)"
   700 
   701 
   702 subsection \<open>Defining generators for any first-order data type\<close>
   703 
   704 axiomatization unknown :: 'a
   705 
   706 notation (output) unknown  ("?")
   707 
   708 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   709 
   710 declare [[quickcheck_batch_tester = exhaustive]]
   711 
   712 
   713 subsection \<open>Defining generators for abstract types\<close>
   714 
   715 ML_file "Tools/Quickcheck/abstract_generators.ML"
   716 
   717 (* FIXME instantiation char :: full_exhaustive
   718 begin
   719 
   720 definition full_exhaustive_char
   721 where
   722   "full_exhaustive f i =
   723      (if 0 < i then full_exhaustive_class.full_exhaustive
   724        (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
   725           (\<lambda>(c, d).
   726             f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
   727               \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
   728                  (Code_Evaluation.Const (STR ''String.char.Char'')
   729                    (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   730                       (b ())) (d ()))) (i - 1)) (i - 1)
   731     else None)"
   732 
   733 instance ..
   734 
   735 end *)
   736 
   737 hide_fact (open) orelse_def
   738 no_notation orelse  (infixr "orelse" 55)
   739 
   740 hide_const valtermify_absdummy valtermify_fun_upd
   741   valterm_emptyset valtermify_insert
   742   valtermify_pair valtermify_Inl valtermify_Inr
   743   termify_fun_upd term_emptyset termify_insert termify_pair setify
   744 
   745 hide_const (open)
   746   exhaustive full_exhaustive
   747   exhaustive_int' full_exhaustive_int'
   748   exhaustive_integer' full_exhaustive_integer'
   749   exhaustive_natural' full_exhaustive_natural'
   750   throw_Counterexample catch_Counterexample
   751   check_all enum_term_of
   752   orelse unknown mk_map_term check_all_n_lists check_all_subsets
   753 
   754 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   755 
   756 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   757   pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
   758   pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   759   neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
   760   neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   761   Unknown Known Unknown_value Value No_value
   762 
   763 end