src/HOL/Quickcheck_Exhaustive.thy
author wenzelm
Thu Apr 14 15:33:51 2016 +0200 (2016-04-14)
changeset 62979 1e527c40ae40
parent 62597 b3f2b8c906a6
child 64670 f77b946d18aa
permissions -rw-r--r--
misc tuning and standardization;
     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))) (sublists (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 (* FIXME instantiation char :: check_all
   480 begin
   481 
   482 definition
   483   "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
   484      f (Char x y, \<lambda>_. Code_Evaluation.App
   485        (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   486 
   487 definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
   488 where
   489   "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   490 
   491 instance ..
   492 
   493 end *)
   494 
   495 instantiation option :: (check_all) check_all
   496 begin
   497 
   498 definition
   499   "check_all f =
   500     f (Code_Evaluation.valtermify (None :: 'a option)) orelse
   501     check_all
   502       (\<lambda>(x, t).
   503         f
   504           (Some x,
   505             \<lambda>_. Code_Evaluation.App
   506               (Code_Evaluation.Const (STR ''Option.option.Some'')
   507                 (Typerep.Typerep (STR ''fun'')
   508                 [Typerep.typerep TYPE('a),
   509                  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   510 
   511 definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list"
   512   where "enum_term_of_option =
   513     (\<lambda> _ _.
   514       Code_Evaluation.term_of (None :: 'a option) #
   515       (map
   516         (Code_Evaluation.App
   517           (Code_Evaluation.Const (STR ''Option.option.Some'')
   518             (Typerep.Typerep (STR ''fun'')
   519               [Typerep.typerep TYPE('a),
   520                Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
   521         (enum_term_of (TYPE('a)) ())))"
   522 
   523 instance ..
   524 
   525 end
   526 
   527 
   528 instantiation Enum.finite_1 :: check_all
   529 begin
   530 
   531 definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
   532 
   533 definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list"
   534   where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
   535 
   536 instance ..
   537 
   538 end
   539 
   540 instantiation Enum.finite_2 :: check_all
   541 begin
   542 
   543 definition
   544   "check_all f =
   545     (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse
   546      f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
   547 
   548 definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list"
   549   where "enum_term_of_finite_2 =
   550     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   551 
   552 instance ..
   553 
   554 end
   555 
   556 instantiation Enum.finite_3 :: check_all
   557 begin
   558 
   559 definition
   560   "check_all f =
   561     (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse
   562      f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse
   563      f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
   564 
   565 definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list"
   566   where "enum_term_of_finite_3 =
   567     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   568 
   569 instance ..
   570 
   571 end
   572 
   573 instantiation Enum.finite_4 :: check_all
   574 begin
   575 
   576 definition
   577   "check_all f =
   578     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse
   579     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse
   580     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse
   581     f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)"
   582 
   583 definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list"
   584   where "enum_term_of_finite_4 =
   585     (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
   586 
   587 instance ..
   588 
   589 end
   590 
   591 subsection \<open>Bounded universal quantifiers\<close>
   592 
   593 class bounded_forall =
   594   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
   595 
   596 
   597 subsection \<open>Fast exhaustive combinators\<close>
   598 
   599 class fast_exhaustive = term_of +
   600   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
   601 
   602 axiomatization throw_Counterexample :: "term list \<Rightarrow> unit"
   603 axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option"
   604 
   605 code_printing
   606   constant throw_Counterexample \<rightharpoonup>
   607     (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
   608 | constant catch_Counterexample \<rightharpoonup>
   609     (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)"
   610 
   611 
   612 subsection \<open>Continuation passing style functions as plus monad\<close>
   613 
   614 type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option"
   615 
   616 definition cps_empty :: "'a cps"
   617   where "cps_empty = (\<lambda>cont. None)"
   618 
   619 definition cps_single :: "'a \<Rightarrow> 'a cps"
   620   where "cps_single v = (\<lambda>cont. cont v)"
   621 
   622 definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps"
   623   where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))"
   624 
   625 definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps"
   626   where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)"
   627 
   628 definition cps_if :: "bool \<Rightarrow> unit cps"
   629   where "cps_if b = (if b then cps_single () else cps_empty)"
   630 
   631 definition cps_not :: "unit cps \<Rightarrow> unit cps"
   632   where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)"
   633 
   634 type_synonym 'a pos_bound_cps =
   635   "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   636 
   637 definition pos_bound_cps_empty :: "'a pos_bound_cps"
   638   where "pos_bound_cps_empty = (\<lambda>cont i. None)"
   639 
   640 definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps"
   641   where "pos_bound_cps_single v = (\<lambda>cont i. cont v)"
   642 
   643 definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps"
   644   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)))"
   645 
   646 definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps"
   647   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)"
   648 
   649 definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps"
   650   where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   651 
   652 datatype (plugins only: code extraction) (dead 'a) unknown =
   653   Unknown | Known 'a
   654 
   655 datatype (plugins only: code extraction) (dead 'a) three_valued =
   656   Unknown_value | Value 'a | No_value
   657 
   658 type_synonym 'a neg_bound_cps =
   659   "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued"
   660 
   661 definition neg_bound_cps_empty :: "'a neg_bound_cps"
   662   where "neg_bound_cps_empty = (\<lambda>cont i. No_value)"
   663 
   664 definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps"
   665   where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))"
   666 
   667 definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps"
   668   where "neg_bound_cps_bind m f =
   669     (\<lambda>cont i.
   670       if i = 0 then cont Unknown
   671       else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))"
   672 
   673 definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps"
   674   where "neg_bound_cps_plus a b =
   675     (\<lambda>c i.
   676       case a c i of
   677         No_value \<Rightarrow> b c i
   678       | Value x \<Rightarrow> Value x
   679       | Unknown_value \<Rightarrow>
   680           (case b c i of
   681             No_value \<Rightarrow> Unknown_value
   682           | Value x \<Rightarrow> Value x
   683           | Unknown_value \<Rightarrow> Unknown_value))"
   684 
   685 definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps"
   686   where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   687 
   688 definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps"
   689   where "neg_bound_cps_not n =
   690     (\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)"
   691 
   692 definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps"
   693   where "pos_bound_cps_not n =
   694     (\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)"
   695 
   696 
   697 subsection \<open>Defining generators for any first-order data type\<close>
   698 
   699 axiomatization unknown :: 'a
   700 
   701 notation (output) unknown  ("?")
   702 
   703 ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   704 
   705 declare [[quickcheck_batch_tester = exhaustive]]
   706 
   707 
   708 subsection \<open>Defining generators for abstract types\<close>
   709 
   710 ML_file "Tools/Quickcheck/abstract_generators.ML"
   711 
   712 (* FIXME instantiation char :: full_exhaustive
   713 begin
   714 
   715 definition full_exhaustive_char
   716 where
   717   "full_exhaustive f i =
   718      (if 0 < i then full_exhaustive_class.full_exhaustive
   719        (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
   720           (\<lambda>(c, d).
   721             f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
   722               \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
   723                  (Code_Evaluation.Const (STR ''String.char.Char'')
   724                    (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   725                       (b ())) (d ()))) (i - 1)) (i - 1)
   726     else None)"
   727 
   728 instance ..
   729 
   730 end *)
   731 
   732 hide_fact (open) orelse_def
   733 no_notation orelse  (infixr "orelse" 55)
   734 
   735 hide_const valtermify_absdummy valtermify_fun_upd
   736   valterm_emptyset valtermify_insert
   737   valtermify_pair valtermify_Inl valtermify_Inr
   738   termify_fun_upd term_emptyset termify_insert termify_pair setify
   739 
   740 hide_const (open)
   741   exhaustive full_exhaustive
   742   exhaustive_int' full_exhaustive_int'
   743   exhaustive_integer' full_exhaustive_integer'
   744   exhaustive_natural' full_exhaustive_natural'
   745   throw_Counterexample catch_Counterexample
   746   check_all enum_term_of
   747   orelse unknown mk_map_term check_all_n_lists check_all_subsets
   748 
   749 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   750 
   751 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   752   pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
   753   pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   754   neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
   755   neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   756   Unknown Known Unknown_value Value No_value
   757 
   758 end