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