src/HOL/Quickcheck_Exhaustive.thy
author bulwahn
Tue Dec 20 17:39:56 2011 +0100 (2011-12-20)
changeset 45925 cd4243c025bb
parent 45818 53a697f5454a
child 46193 55a4769d0abe
permissions -rw-r--r--
quickcheck generators for abstract types; tuned
bulwahn@40420
     1
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@40420
     2
bulwahn@41916
     3
header {* A simple counterexample generator performing exhaustive testing *}
bulwahn@40420
     4
bulwahn@41918
     5
theory Quickcheck_Exhaustive
bulwahn@40420
     6
imports Quickcheck
bulwahn@45925
     7
uses
bulwahn@45925
     8
  ("Tools/Quickcheck/exhaustive_generators.ML")
bulwahn@45925
     9
  ("Tools/Quickcheck/abstract_generators.ML")
bulwahn@40420
    10
begin
bulwahn@40420
    11
bulwahn@41916
    12
subsection {* basic operations for exhaustive generators *}
bulwahn@41105
    13
bulwahn@41105
    14
definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
bulwahn@41105
    15
where
bulwahn@41105
    16
  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
bulwahn@40420
    17
bulwahn@41916
    18
subsection {* exhaustive generator type classes *}
bulwahn@40420
    19
bulwahn@41916
    20
class exhaustive = term_of +
bulwahn@45724
    21
  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
bulwahn@42310
    22
  
bulwahn@42310
    23
class full_exhaustive = term_of +
bulwahn@45722
    24
  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
bulwahn@40420
    25
bulwahn@42310
    26
instantiation code_numeral :: full_exhaustive
bulwahn@40639
    27
begin
bulwahn@40639
    28
bulwahn@45722
    29
function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
bulwahn@42304
    30
  where "full_exhaustive_code_numeral' f d i =
bulwahn@42304
    31
    (if d < i then None
bulwahn@42304
    32
    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
bulwahn@42304
    33
by pat_completeness auto
bulwahn@42304
    34
bulwahn@42304
    35
termination
bulwahn@42304
    36
  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
bulwahn@42304
    37
bulwahn@42304
    38
definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
bulwahn@42304
    39
bulwahn@42310
    40
instance ..
bulwahn@42310
    41
bulwahn@42310
    42
end
bulwahn@42310
    43
bulwahn@42310
    44
instantiation code_numeral :: exhaustive
bulwahn@42310
    45
begin
bulwahn@42310
    46
bulwahn@45724
    47
function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
bulwahn@41916
    48
  where "exhaustive_code_numeral' f d i =
bulwahn@41916
    49
    (if d < i then None
bulwahn@42304
    50
    else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
bulwahn@41231
    51
by pat_completeness auto
bulwahn@41231
    52
bulwahn@42304
    53
termination
bulwahn@41231
    54
  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
bulwahn@41231
    55
bulwahn@41916
    56
definition "exhaustive f d = exhaustive_code_numeral' f d 0"
bulwahn@41231
    57
bulwahn@41231
    58
instance ..
bulwahn@41231
    59
bulwahn@41231
    60
end
bulwahn@41231
    61
bulwahn@41916
    62
instantiation nat :: exhaustive
bulwahn@41231
    63
begin
bulwahn@41231
    64
bulwahn@42304
    65
definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
bulwahn@42304
    66
bulwahn@42310
    67
instance ..
bulwahn@42310
    68
bulwahn@42310
    69
end
bulwahn@42310
    70
bulwahn@42310
    71
instantiation nat :: full_exhaustive
bulwahn@42310
    72
begin
bulwahn@42310
    73
bulwahn@42304
    74
definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
bulwahn@41231
    75
bulwahn@41231
    76
instance ..
bulwahn@41231
    77
bulwahn@41231
    78
end
bulwahn@41231
    79
bulwahn@41916
    80
instantiation int :: exhaustive
bulwahn@40639
    81
begin
bulwahn@40639
    82
bulwahn@45724
    83
function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
bulwahn@42304
    84
  where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
bulwahn@40639
    85
by pat_completeness auto
bulwahn@40639
    86
bulwahn@40639
    87
termination 
bulwahn@40639
    88
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
bulwahn@40639
    89
bulwahn@41916
    90
definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
bulwahn@40639
    91
bulwahn@42310
    92
instance ..
bulwahn@42310
    93
bulwahn@42310
    94
end
bulwahn@42310
    95
bulwahn@42310
    96
instantiation int :: full_exhaustive
bulwahn@42310
    97
begin
bulwahn@42310
    98
bulwahn@45722
    99
function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
bulwahn@42304
   100
  where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
bulwahn@42304
   101
by pat_completeness auto
bulwahn@42304
   102
bulwahn@42304
   103
termination 
bulwahn@42304
   104
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
bulwahn@42304
   105
bulwahn@42304
   106
definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
bulwahn@42304
   107
bulwahn@40639
   108
instance ..
bulwahn@40639
   109
bulwahn@40639
   110
end
bulwahn@40639
   111
bulwahn@41916
   112
instantiation prod :: (exhaustive, exhaustive) exhaustive
bulwahn@40639
   113
begin
bulwahn@40899
   114
bulwahn@40639
   115
definition
bulwahn@42304
   116
  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
bulwahn@42304
   117
bulwahn@42310
   118
instance ..
bulwahn@42310
   119
bulwahn@42310
   120
end
bulwahn@42310
   121
bulwahn@42310
   122
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
bulwahn@42310
   123
begin
bulwahn@42310
   124
bulwahn@42304
   125
definition
bulwahn@42304
   126
  "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
bulwahn@41719
   127
    %u. let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
   128
            T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
   129
    in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
   130
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
   131
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
bulwahn@41719
   132
      (t1 ())) (t2 ()))) d) d"
bulwahn@40639
   133
bulwahn@40639
   134
instance ..
bulwahn@40639
   135
bulwahn@40639
   136
end
bulwahn@40639
   137
bulwahn@41916
   138
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
bulwahn@40639
   139
begin
bulwahn@40639
   140
bulwahn@45724
   141
fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
bulwahn@42304
   142
where
bulwahn@42304
   143
  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
bulwahn@42304
   144
   orelse (if i > 1 then
bulwahn@42304
   145
     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
bulwahn@42304
   146
       f (g(a := b))) d) d) (i - 1) d else None)"
bulwahn@42304
   147
bulwahn@45724
   148
definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
bulwahn@40639
   149
where
bulwahn@42304
   150
  "exhaustive_fun f d = exhaustive_fun' f d d" 
bulwahn@42304
   151
bulwahn@42310
   152
instance ..
bulwahn@42310
   153
bulwahn@42310
   154
end
bulwahn@42310
   155
bulwahn@42310
   156
instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
bulwahn@42310
   157
begin
bulwahn@42304
   158
bulwahn@45722
   159
fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
bulwahn@42304
   160
where
bulwahn@42304
   161
  "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
bulwahn@42117
   162
   orelse (if i > 1 then
bulwahn@42304
   163
     full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
bulwahn@42117
   164
       f (g(a := b),
bulwahn@42117
   165
         (%_. let A = (Typerep.typerep (TYPE('a)));
bulwahn@42117
   166
                  B = (Typerep.typerep (TYPE('b)));
bulwahn@42117
   167
                  fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
bulwahn@42117
   168
              in
bulwahn@42117
   169
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
bulwahn@42117
   170
                  (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
bulwahn@42117
   171
                (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
bulwahn@40639
   172
bulwahn@45722
   173
definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
bulwahn@40639
   174
where
bulwahn@42304
   175
  "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
bulwahn@40639
   176
bulwahn@40639
   177
instance ..
bulwahn@40639
   178
bulwahn@40639
   179
end
bulwahn@40639
   180
bulwahn@41085
   181
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
bulwahn@41085
   182
bulwahn@41085
   183
class check_all = enum + term_of +
bulwahn@45722
   184
  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
bulwahn@41177
   185
  fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
bulwahn@41177
   186
  
bulwahn@45722
   187
fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
bulwahn@41085
   188
where
bulwahn@41085
   189
  "check_all_n_lists f n =
bulwahn@41085
   190
     (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
bulwahn@41085
   191
bulwahn@41177
   192
definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
bulwahn@41085
   193
where
bulwahn@41177
   194
  "mk_map_term T1 T2 domm rng =
bulwahn@41177
   195
     (%_. let T1 = T1 ();
bulwahn@41085
   196
              T2 = T2 ();
bulwahn@41085
   197
              update_term = (%g (a, b).
bulwahn@41085
   198
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
bulwahn@41085
   199
                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
bulwahn@41085
   200
                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
bulwahn@41177
   201
                      Typerep.Typerep (STR ''fun'') [T1,
bulwahn@41177
   202
                        Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
bulwahn@41177
   203
                        g) a) b)
bulwahn@41085
   204
          in
bulwahn@41177
   205
             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
bulwahn@41177
   206
bulwahn@41177
   207
instantiation "fun" :: ("{equal, check_all}", check_all) check_all
bulwahn@41177
   208
begin
bulwahn@41085
   209
bulwahn@41085
   210
definition
bulwahn@41177
   211
  "check_all f =
bulwahn@41177
   212
    (let
bulwahn@41177
   213
      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
bulwahn@41177
   214
      enum = (Enum.enum :: 'a list)
bulwahn@41177
   215
    in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))"
bulwahn@41085
   216
bulwahn@41177
   217
definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
bulwahn@41177
   218
where
bulwahn@41177
   219
  "enum_term_of_fun = (%_ _. let
bulwahn@41177
   220
    enum_term_of_a = enum_term_of (TYPE('a));
bulwahn@41177
   221
    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
bulwahn@41177
   222
  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
bulwahn@41177
   223
 
bulwahn@41085
   224
instance ..
bulwahn@41085
   225
bulwahn@41085
   226
end
bulwahn@41085
   227
bulwahn@41105
   228
bulwahn@41105
   229
instantiation unit :: check_all
bulwahn@41105
   230
begin
bulwahn@41105
   231
bulwahn@41105
   232
definition
bulwahn@41105
   233
  "check_all f = f (Code_Evaluation.valtermify ())"
bulwahn@41105
   234
bulwahn@41177
   235
definition enum_term_of_unit :: "unit itself => unit => term list"
bulwahn@41177
   236
where
bulwahn@41177
   237
  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
bulwahn@41177
   238
bulwahn@41105
   239
instance ..
bulwahn@41105
   240
bulwahn@41105
   241
end
bulwahn@41105
   242
bulwahn@41105
   243
bulwahn@41085
   244
instantiation bool :: check_all
bulwahn@41085
   245
begin
bulwahn@41085
   246
bulwahn@41085
   247
definition
bulwahn@41085
   248
  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
bulwahn@41085
   249
bulwahn@41177
   250
definition enum_term_of_bool :: "bool itself => unit => term list"
bulwahn@41177
   251
where
bulwahn@41177
   252
  "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
bulwahn@41177
   253
bulwahn@41085
   254
instance ..
bulwahn@41085
   255
bulwahn@41085
   256
end
bulwahn@41085
   257
bulwahn@41105
   258
bulwahn@41085
   259
instantiation prod :: (check_all, check_all) check_all
bulwahn@41085
   260
begin
bulwahn@41085
   261
bulwahn@41085
   262
definition
bulwahn@41719
   263
  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
bulwahn@41719
   264
    %u. let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
   265
            T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
   266
    in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
   267
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
   268
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
bulwahn@41719
   269
      (t1 ())) (t2 ()))))"
bulwahn@41085
   270
bulwahn@41177
   271
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
bulwahn@41177
   272
where
bulwahn@41719
   273
  "enum_term_of_prod = (%_ _. map (%(x, y).
bulwahn@41719
   274
       let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
   275
           T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
   276
       in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
   277
         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
   278
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
bulwahn@41719
   279
     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
bulwahn@41177
   280
bulwahn@41085
   281
instance ..
bulwahn@41085
   282
bulwahn@41085
   283
end
bulwahn@41085
   284
bulwahn@41105
   285
bulwahn@41105
   286
instantiation sum :: (check_all, check_all) check_all
bulwahn@41105
   287
begin
bulwahn@41105
   288
bulwahn@41105
   289
definition
bulwahn@41722
   290
  "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
bulwahn@41722
   291
     let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   292
         T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   293
       in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
bulwahn@41722
   294
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
bulwahn@41722
   295
             | None => check_all (%(b, t). f (Inr b, %_. let
bulwahn@41722
   296
                 T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   297
                 T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   298
               in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
bulwahn@41722
   299
                 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
bulwahn@41105
   300
bulwahn@41177
   301
definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
bulwahn@41177
   302
where
bulwahn@41722
   303
  "enum_term_of_sum = (%_ _.
bulwahn@41722
   304
     let
bulwahn@41722
   305
       T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   306
       T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   307
     in
bulwahn@41722
   308
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
bulwahn@41722
   309
             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
bulwahn@41722
   310
             (enum_term_of (TYPE('a)) ()) @
bulwahn@41722
   311
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
bulwahn@41722
   312
             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
bulwahn@41722
   313
             (enum_term_of (TYPE('b)) ()))"
bulwahn@41177
   314
bulwahn@41105
   315
instance ..
bulwahn@41105
   316
bulwahn@41105
   317
end
bulwahn@41105
   318
bulwahn@41105
   319
instantiation nibble :: check_all
bulwahn@41105
   320
begin
bulwahn@41105
   321
bulwahn@41105
   322
definition
bulwahn@41105
   323
  "check_all f =
bulwahn@41105
   324
    f (Code_Evaluation.valtermify Nibble0) orelse
bulwahn@41105
   325
    f (Code_Evaluation.valtermify Nibble1) orelse
bulwahn@41105
   326
    f (Code_Evaluation.valtermify Nibble2) orelse
bulwahn@41105
   327
    f (Code_Evaluation.valtermify Nibble3) orelse
bulwahn@41105
   328
    f (Code_Evaluation.valtermify Nibble4) orelse
bulwahn@41105
   329
    f (Code_Evaluation.valtermify Nibble5) orelse
bulwahn@41105
   330
    f (Code_Evaluation.valtermify Nibble6) orelse
bulwahn@41105
   331
    f (Code_Evaluation.valtermify Nibble7) orelse
bulwahn@41105
   332
    f (Code_Evaluation.valtermify Nibble8) orelse
bulwahn@41105
   333
    f (Code_Evaluation.valtermify Nibble9) orelse
bulwahn@41105
   334
    f (Code_Evaluation.valtermify NibbleA) orelse
bulwahn@41105
   335
    f (Code_Evaluation.valtermify NibbleB) orelse
bulwahn@41105
   336
    f (Code_Evaluation.valtermify NibbleC) orelse
bulwahn@41105
   337
    f (Code_Evaluation.valtermify NibbleD) orelse
bulwahn@41105
   338
    f (Code_Evaluation.valtermify NibbleE) orelse
bulwahn@41105
   339
    f (Code_Evaluation.valtermify NibbleF)"
bulwahn@41105
   340
bulwahn@41177
   341
definition enum_term_of_nibble :: "nibble itself => unit => term list"
bulwahn@41177
   342
where
bulwahn@41177
   343
  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
bulwahn@41177
   344
bulwahn@41105
   345
instance ..
bulwahn@41105
   346
bulwahn@41105
   347
end
bulwahn@41105
   348
bulwahn@41105
   349
bulwahn@41105
   350
instantiation char :: check_all
bulwahn@41105
   351
begin
bulwahn@41105
   352
bulwahn@41105
   353
definition
bulwahn@41105
   354
  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
bulwahn@41105
   355
bulwahn@41177
   356
definition enum_term_of_char :: "char itself => unit => term list"
bulwahn@41177
   357
where
bulwahn@41177
   358
  "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
bulwahn@41177
   359
bulwahn@41105
   360
instance ..
bulwahn@41105
   361
bulwahn@41105
   362
end
bulwahn@41105
   363
bulwahn@41105
   364
bulwahn@41105
   365
instantiation option :: (check_all) check_all
bulwahn@41105
   366
begin
bulwahn@41105
   367
bulwahn@41105
   368
definition
bulwahn@41178
   369
  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
bulwahn@41178
   370
    (Code_Evaluation.Const (STR ''Option.option.Some'')
bulwahn@41178
   371
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
bulwahn@41105
   372
bulwahn@41177
   373
definition enum_term_of_option :: "'a option itself => unit => term list"
bulwahn@41177
   374
where
bulwahn@41722
   375
  "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
bulwahn@41722
   376
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
bulwahn@41177
   377
bulwahn@41105
   378
instance ..
bulwahn@41105
   379
bulwahn@41105
   380
end
bulwahn@41105
   381
bulwahn@41105
   382
bulwahn@41085
   383
instantiation Enum.finite_1 :: check_all
bulwahn@41085
   384
begin
bulwahn@41085
   385
bulwahn@41085
   386
definition
bulwahn@41085
   387
  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
bulwahn@41085
   388
bulwahn@41177
   389
definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
bulwahn@41177
   390
where
bulwahn@41177
   391
  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
bulwahn@41177
   392
bulwahn@41085
   393
instance ..
bulwahn@41085
   394
bulwahn@41085
   395
end
bulwahn@41085
   396
bulwahn@41085
   397
instantiation Enum.finite_2 :: check_all
bulwahn@41085
   398
begin
bulwahn@41085
   399
bulwahn@41085
   400
definition
bulwahn@41085
   401
  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
bulwahn@41085
   402
bulwahn@41177
   403
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
bulwahn@41177
   404
where
bulwahn@41177
   405
  "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
bulwahn@41177
   406
bulwahn@41085
   407
instance ..
bulwahn@41085
   408
bulwahn@41085
   409
end
bulwahn@41085
   410
bulwahn@41085
   411
instantiation Enum.finite_3 :: check_all
bulwahn@41085
   412
begin
bulwahn@41085
   413
bulwahn@41085
   414
definition
bulwahn@41085
   415
  "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
bulwahn@41085
   416
bulwahn@41177
   417
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
bulwahn@41177
   418
where
bulwahn@41177
   419
  "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
bulwahn@41177
   420
bulwahn@41085
   421
instance ..
bulwahn@41085
   422
bulwahn@41085
   423
end
bulwahn@41085
   424
bulwahn@42195
   425
subsection {* Bounded universal quantifiers *}
bulwahn@41085
   426
bulwahn@42195
   427
class bounded_forall =
bulwahn@42195
   428
  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
bulwahn@42195
   429
bulwahn@42305
   430
subsection {* Fast exhaustive combinators *}
bulwahn@42305
   431
bulwahn@42305
   432
class fast_exhaustive = term_of +
bulwahn@42305
   433
  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
bulwahn@42305
   434
bulwahn@45818
   435
axiomatization throw_Counterexample :: "term list => unit"
bulwahn@45818
   436
axiomatization catch_Counterexample :: "unit => term list option"
bulwahn@42305
   437
bulwahn@42305
   438
code_const throw_Counterexample
bulwahn@42305
   439
  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
bulwahn@42305
   440
code_const catch_Counterexample
bulwahn@42305
   441
  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
bulwahn@42305
   442
bulwahn@45450
   443
subsection {* Continuation passing style functions as plus monad *}
bulwahn@45450
   444
  
bulwahn@45450
   445
type_synonym 'a cps = "('a => term list option) => term list option"
bulwahn@45450
   446
bulwahn@45450
   447
definition cps_empty :: "'a cps"
bulwahn@45450
   448
where
bulwahn@45450
   449
  "cps_empty = (%cont. None)"
bulwahn@45450
   450
bulwahn@45450
   451
definition cps_single :: "'a => 'a cps"
bulwahn@45450
   452
where
bulwahn@45450
   453
  "cps_single v = (%cont. cont v)"
bulwahn@45450
   454
bulwahn@45450
   455
definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
bulwahn@45450
   456
where
bulwahn@45450
   457
  "cps_bind m f = (%cont. m (%a. (f a) cont))"
bulwahn@45450
   458
bulwahn@45450
   459
definition cps_plus :: "'a cps => 'a cps => 'a cps"
bulwahn@45450
   460
where
bulwahn@45450
   461
  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
bulwahn@45450
   462
bulwahn@45450
   463
definition cps_if :: "bool => unit cps"
bulwahn@45450
   464
where
bulwahn@45450
   465
  "cps_if b = (if b then cps_single () else cps_empty)"
bulwahn@45450
   466
bulwahn@45450
   467
definition cps_not :: "unit cps => unit cps"
bulwahn@45450
   468
where
bulwahn@45450
   469
  "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
bulwahn@45450
   470
bulwahn@45750
   471
type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
bulwahn@45450
   472
bulwahn@45450
   473
definition pos_bound_cps_empty :: "'a pos_bound_cps"
bulwahn@45450
   474
where
bulwahn@45450
   475
  "pos_bound_cps_empty = (%cont i. None)"
bulwahn@45450
   476
bulwahn@45450
   477
definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
bulwahn@45450
   478
where
bulwahn@45450
   479
  "pos_bound_cps_single v = (%cont i. cont v)"
bulwahn@45450
   480
bulwahn@45450
   481
definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
bulwahn@45450
   482
where
bulwahn@45450
   483
  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
bulwahn@45450
   484
bulwahn@45450
   485
definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
bulwahn@45450
   486
where
bulwahn@45450
   487
  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
bulwahn@45450
   488
bulwahn@45450
   489
definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
bulwahn@45450
   490
where
bulwahn@45450
   491
  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
bulwahn@45450
   492
bulwahn@45450
   493
datatype 'a unknown = Unknown | Known 'a
bulwahn@45450
   494
datatype 'a three_valued = Unknown_value | Value 'a | No_value
bulwahn@45450
   495
bulwahn@45450
   496
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
bulwahn@45450
   497
bulwahn@45450
   498
definition neg_bound_cps_empty :: "'a neg_bound_cps"
bulwahn@45450
   499
where
bulwahn@45450
   500
  "neg_bound_cps_empty = (%cont i. No_value)"
bulwahn@45450
   501
bulwahn@45450
   502
definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
bulwahn@45450
   503
where
bulwahn@45450
   504
  "neg_bound_cps_single v = (%cont i. cont (Known v))"
bulwahn@45450
   505
bulwahn@45450
   506
definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
bulwahn@45450
   507
where
bulwahn@45450
   508
  "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
bulwahn@45450
   509
bulwahn@45450
   510
definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
bulwahn@45450
   511
where
bulwahn@45450
   512
  "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))"
bulwahn@45450
   513
bulwahn@45450
   514
definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
bulwahn@45450
   515
where
bulwahn@45450
   516
  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
bulwahn@45450
   517
bulwahn@45450
   518
definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
bulwahn@45450
   519
where
bulwahn@45750
   520
  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
bulwahn@45450
   521
bulwahn@45450
   522
definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
bulwahn@45450
   523
where
bulwahn@45450
   524
  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
bulwahn@45450
   525
bulwahn@45925
   526
subsection {* Defining generators for any first-order data type *}
bulwahn@40420
   527
bulwahn@45697
   528
axiomatization unknown :: 'a
bulwahn@45697
   529
bulwahn@45697
   530
notation (output) unknown  ("?")
bulwahn@45684
   531
 
bulwahn@41920
   532
use "Tools/Quickcheck/exhaustive_generators.ML"
bulwahn@40420
   533
bulwahn@41918
   534
setup {* Exhaustive_Generators.setup *}
bulwahn@40420
   535
bulwahn@43882
   536
declare [[quickcheck_batch_tester = exhaustive]]
bulwahn@40915
   537
bulwahn@45925
   538
subsection {* Defining generators for abstract types *}
bulwahn@45925
   539
bulwahn@45925
   540
use "Tools/Quickcheck/abstract_generators.ML"
bulwahn@45925
   541
bulwahn@45733
   542
hide_fact orelse_def
bulwahn@41105
   543
no_notation orelse (infixr "orelse" 55)
bulwahn@45818
   544
bulwahn@45818
   545
hide_fact
bulwahn@45818
   546
  exhaustive'_def
bulwahn@45818
   547
  exhaustive_code_numeral'_def
bulwahn@45818
   548
bulwahn@45818
   549
hide_const (open)
bulwahn@45818
   550
  exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
bulwahn@45818
   551
  throw_Counterexample catch_Counterexample
bulwahn@45818
   552
  check_all enum_term_of
bulwahn@45818
   553
  orelse unknown mk_map_term check_all_n_lists
bulwahn@40420
   554
bulwahn@45450
   555
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
bulwahn@45450
   556
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
bulwahn@45450
   557
  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
bulwahn@45450
   558
  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
bulwahn@45450
   559
  Unknown Known Unknown_value Value No_value
bulwahn@45450
   560
bulwahn@45450
   561
end