src/HOL/Quickcheck_Exhaustive.thy
author bulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 41918 d2ab869f8b0b
parent 41916 80060d5f864a
child 41920 d4fb7a418152
permissions -rw-r--r--
replacing naming of small by exhaustive
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@41916
     7
uses ("Tools/exhaustive_generators.ML")
bulwahn@40420
     8
begin
bulwahn@40420
     9
bulwahn@41916
    10
subsection {* basic operations for exhaustive generators *}
bulwahn@41105
    11
bulwahn@41105
    12
definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
bulwahn@41105
    13
where
bulwahn@41105
    14
  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
bulwahn@40420
    15
bulwahn@41916
    16
subsection {* exhaustive generator type classes *}
bulwahn@40420
    17
bulwahn@41916
    18
class exhaustive = term_of +
bulwahn@41916
    19
fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
bulwahn@40420
    20
bulwahn@41916
    21
instantiation unit :: exhaustive
bulwahn@40420
    22
begin
bulwahn@40420
    23
bulwahn@41916
    24
definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
bulwahn@40420
    25
bulwahn@40420
    26
instance ..
bulwahn@40420
    27
bulwahn@40420
    28
end
bulwahn@40420
    29
bulwahn@41916
    30
instantiation code_numeral :: exhaustive
bulwahn@40639
    31
begin
bulwahn@40639
    32
bulwahn@41916
    33
function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
bulwahn@41916
    34
  where "exhaustive_code_numeral' f d i =
bulwahn@41916
    35
    (if d < i then None
bulwahn@41916
    36
    else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
bulwahn@41231
    37
by pat_completeness auto
bulwahn@41231
    38
bulwahn@41231
    39
termination 
bulwahn@41231
    40
  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
bulwahn@41231
    41
bulwahn@41916
    42
definition "exhaustive f d = exhaustive_code_numeral' f d 0"
bulwahn@41231
    43
bulwahn@41231
    44
instance ..
bulwahn@41231
    45
bulwahn@41231
    46
end
bulwahn@41231
    47
bulwahn@41916
    48
instantiation nat :: exhaustive
bulwahn@41231
    49
begin
bulwahn@41231
    50
bulwahn@41916
    51
definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
bulwahn@41231
    52
bulwahn@41231
    53
instance ..
bulwahn@41231
    54
bulwahn@41231
    55
end
bulwahn@41231
    56
bulwahn@41916
    57
instantiation int :: exhaustive
bulwahn@40639
    58
begin
bulwahn@40639
    59
bulwahn@41916
    60
function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
bulwahn@41916
    61
  where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
bulwahn@40639
    62
by pat_completeness auto
bulwahn@40639
    63
bulwahn@40639
    64
termination 
bulwahn@40639
    65
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
bulwahn@40639
    66
bulwahn@41916
    67
definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
bulwahn@40639
    68
bulwahn@40639
    69
instance ..
bulwahn@40639
    70
bulwahn@40639
    71
end
bulwahn@40639
    72
bulwahn@41916
    73
instantiation prod :: (exhaustive, exhaustive) exhaustive
bulwahn@40639
    74
begin
bulwahn@40899
    75
bulwahn@40639
    76
definition
bulwahn@41916
    77
  "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
bulwahn@41719
    78
    %u. let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
    79
            T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
    80
    in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
    81
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
    82
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
bulwahn@41719
    83
      (t1 ())) (t2 ()))) d) d"
bulwahn@40639
    84
bulwahn@40639
    85
instance ..
bulwahn@40639
    86
bulwahn@40639
    87
end
bulwahn@40639
    88
bulwahn@41916
    89
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
bulwahn@40639
    90
begin
bulwahn@40639
    91
bulwahn@41916
    92
fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
bulwahn@40639
    93
where
bulwahn@41916
    94
  "exhaustive_fun' f i d = (if i > 1 then
bulwahn@41916
    95
    exhaustive (%(a, at). exhaustive (%(b, bt).
bulwahn@41916
    96
      exhaustive_fun' (%(g, gt). f (g(a := b),
bulwahn@40899
    97
        (%_. let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@40899
    98
                 T2 = (Typerep.typerep (TYPE('b)))
bulwahn@40899
    99
             in
bulwahn@40899
   100
               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
bulwahn@40899
   101
                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
bulwahn@40899
   102
                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
bulwahn@40899
   103
                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
bulwahn@40899
   104
               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
bulwahn@40899
   105
  else (if i > 0 then
bulwahn@41916
   106
    exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
bulwahn@40639
   107
bulwahn@41916
   108
definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
bulwahn@40639
   109
where
bulwahn@41916
   110
  "exhaustive_fun f d = exhaustive_fun' f d d" 
bulwahn@40639
   111
bulwahn@40639
   112
instance ..
bulwahn@40639
   113
bulwahn@40639
   114
end
bulwahn@40639
   115
bulwahn@41085
   116
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
bulwahn@41085
   117
bulwahn@41085
   118
class check_all = enum + term_of +
bulwahn@41177
   119
  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
bulwahn@41177
   120
  fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
bulwahn@41177
   121
  
bulwahn@41085
   122
fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
bulwahn@41085
   123
where
bulwahn@41085
   124
  "check_all_n_lists f n =
bulwahn@41085
   125
     (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
   126
bulwahn@41177
   127
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
   128
where
bulwahn@41177
   129
  "mk_map_term T1 T2 domm rng =
bulwahn@41177
   130
     (%_. let T1 = T1 ();
bulwahn@41085
   131
              T2 = T2 ();
bulwahn@41085
   132
              update_term = (%g (a, b).
bulwahn@41085
   133
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
bulwahn@41085
   134
                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
bulwahn@41085
   135
                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
bulwahn@41177
   136
                      Typerep.Typerep (STR ''fun'') [T1,
bulwahn@41177
   137
                        Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
bulwahn@41177
   138
                        g) a) b)
bulwahn@41085
   139
          in
bulwahn@41177
   140
             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
bulwahn@41177
   141
bulwahn@41177
   142
instantiation "fun" :: ("{equal, check_all}", check_all) check_all
bulwahn@41177
   143
begin
bulwahn@41085
   144
bulwahn@41085
   145
definition
bulwahn@41177
   146
  "check_all f =
bulwahn@41177
   147
    (let
bulwahn@41177
   148
      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
bulwahn@41177
   149
      enum = (Enum.enum :: 'a list)
bulwahn@41177
   150
    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
   151
bulwahn@41177
   152
definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
bulwahn@41177
   153
where
bulwahn@41177
   154
  "enum_term_of_fun = (%_ _. let
bulwahn@41177
   155
    enum_term_of_a = enum_term_of (TYPE('a));
bulwahn@41177
   156
    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
bulwahn@41177
   157
  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
bulwahn@41177
   158
 
bulwahn@41085
   159
instance ..
bulwahn@41085
   160
bulwahn@41085
   161
end
bulwahn@41085
   162
bulwahn@41105
   163
bulwahn@41105
   164
instantiation unit :: check_all
bulwahn@41105
   165
begin
bulwahn@41105
   166
bulwahn@41105
   167
definition
bulwahn@41105
   168
  "check_all f = f (Code_Evaluation.valtermify ())"
bulwahn@41105
   169
bulwahn@41177
   170
definition enum_term_of_unit :: "unit itself => unit => term list"
bulwahn@41177
   171
where
bulwahn@41177
   172
  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
bulwahn@41177
   173
bulwahn@41105
   174
instance ..
bulwahn@41105
   175
bulwahn@41105
   176
end
bulwahn@41105
   177
bulwahn@41105
   178
bulwahn@41085
   179
instantiation bool :: check_all
bulwahn@41085
   180
begin
bulwahn@41085
   181
bulwahn@41085
   182
definition
bulwahn@41085
   183
  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
bulwahn@41085
   184
bulwahn@41177
   185
definition enum_term_of_bool :: "bool itself => unit => term list"
bulwahn@41177
   186
where
bulwahn@41177
   187
  "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
bulwahn@41177
   188
bulwahn@41085
   189
instance ..
bulwahn@41085
   190
bulwahn@41085
   191
end
bulwahn@41085
   192
bulwahn@41105
   193
bulwahn@41085
   194
instantiation prod :: (check_all, check_all) check_all
bulwahn@41085
   195
begin
bulwahn@41085
   196
bulwahn@41085
   197
definition
bulwahn@41719
   198
  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
bulwahn@41719
   199
    %u. let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
   200
            T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
   201
    in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
   202
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
   203
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
bulwahn@41719
   204
      (t1 ())) (t2 ()))))"
bulwahn@41085
   205
bulwahn@41177
   206
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
bulwahn@41177
   207
where
bulwahn@41719
   208
  "enum_term_of_prod = (%_ _. map (%(x, y).
bulwahn@41719
   209
       let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41719
   210
           T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41719
   211
       in Code_Evaluation.App (Code_Evaluation.App (
bulwahn@41719
   212
         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
bulwahn@41719
   213
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
bulwahn@41719
   214
     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
bulwahn@41177
   215
bulwahn@41085
   216
instance ..
bulwahn@41085
   217
bulwahn@41085
   218
end
bulwahn@41085
   219
bulwahn@41105
   220
bulwahn@41105
   221
instantiation sum :: (check_all, check_all) check_all
bulwahn@41105
   222
begin
bulwahn@41105
   223
bulwahn@41105
   224
definition
bulwahn@41722
   225
  "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
bulwahn@41722
   226
     let T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   227
         T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   228
       in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
bulwahn@41722
   229
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
bulwahn@41722
   230
             | None => check_all (%(b, t). f (Inr b, %_. let
bulwahn@41722
   231
                 T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   232
                 T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   233
               in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
bulwahn@41722
   234
                 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
bulwahn@41105
   235
bulwahn@41177
   236
definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
bulwahn@41177
   237
where
bulwahn@41722
   238
  "enum_term_of_sum = (%_ _.
bulwahn@41722
   239
     let
bulwahn@41722
   240
       T1 = (Typerep.typerep (TYPE('a)));
bulwahn@41722
   241
       T2 = (Typerep.typerep (TYPE('b)))
bulwahn@41722
   242
     in
bulwahn@41722
   243
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
bulwahn@41722
   244
             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
bulwahn@41722
   245
             (enum_term_of (TYPE('a)) ()) @
bulwahn@41722
   246
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
bulwahn@41722
   247
             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
bulwahn@41722
   248
             (enum_term_of (TYPE('b)) ()))"
bulwahn@41177
   249
bulwahn@41105
   250
instance ..
bulwahn@41105
   251
bulwahn@41105
   252
end
bulwahn@41105
   253
bulwahn@41105
   254
instantiation nibble :: check_all
bulwahn@41105
   255
begin
bulwahn@41105
   256
bulwahn@41105
   257
definition
bulwahn@41105
   258
  "check_all f =
bulwahn@41105
   259
    f (Code_Evaluation.valtermify Nibble0) orelse
bulwahn@41105
   260
    f (Code_Evaluation.valtermify Nibble1) orelse
bulwahn@41105
   261
    f (Code_Evaluation.valtermify Nibble2) orelse
bulwahn@41105
   262
    f (Code_Evaluation.valtermify Nibble3) orelse
bulwahn@41105
   263
    f (Code_Evaluation.valtermify Nibble4) orelse
bulwahn@41105
   264
    f (Code_Evaluation.valtermify Nibble5) orelse
bulwahn@41105
   265
    f (Code_Evaluation.valtermify Nibble6) orelse
bulwahn@41105
   266
    f (Code_Evaluation.valtermify Nibble7) orelse
bulwahn@41105
   267
    f (Code_Evaluation.valtermify Nibble8) orelse
bulwahn@41105
   268
    f (Code_Evaluation.valtermify Nibble9) orelse
bulwahn@41105
   269
    f (Code_Evaluation.valtermify NibbleA) orelse
bulwahn@41105
   270
    f (Code_Evaluation.valtermify NibbleB) orelse
bulwahn@41105
   271
    f (Code_Evaluation.valtermify NibbleC) orelse
bulwahn@41105
   272
    f (Code_Evaluation.valtermify NibbleD) orelse
bulwahn@41105
   273
    f (Code_Evaluation.valtermify NibbleE) orelse
bulwahn@41105
   274
    f (Code_Evaluation.valtermify NibbleF)"
bulwahn@41105
   275
bulwahn@41177
   276
definition enum_term_of_nibble :: "nibble itself => unit => term list"
bulwahn@41177
   277
where
bulwahn@41177
   278
  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
bulwahn@41177
   279
bulwahn@41105
   280
instance ..
bulwahn@41105
   281
bulwahn@41105
   282
end
bulwahn@41105
   283
bulwahn@41105
   284
bulwahn@41105
   285
instantiation char :: check_all
bulwahn@41105
   286
begin
bulwahn@41105
   287
bulwahn@41105
   288
definition
bulwahn@41105
   289
  "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
   290
bulwahn@41177
   291
definition enum_term_of_char :: "char itself => unit => term list"
bulwahn@41177
   292
where
bulwahn@41177
   293
  "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
bulwahn@41177
   294
bulwahn@41105
   295
instance ..
bulwahn@41105
   296
bulwahn@41105
   297
end
bulwahn@41105
   298
bulwahn@41105
   299
bulwahn@41105
   300
instantiation option :: (check_all) check_all
bulwahn@41105
   301
begin
bulwahn@41105
   302
bulwahn@41105
   303
definition
bulwahn@41178
   304
  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
bulwahn@41178
   305
    (Code_Evaluation.Const (STR ''Option.option.Some'')
bulwahn@41178
   306
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
bulwahn@41105
   307
bulwahn@41177
   308
definition enum_term_of_option :: "'a option itself => unit => term list"
bulwahn@41177
   309
where
bulwahn@41722
   310
  "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
bulwahn@41722
   311
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
bulwahn@41177
   312
bulwahn@41105
   313
instance ..
bulwahn@41105
   314
bulwahn@41105
   315
end
bulwahn@41105
   316
bulwahn@41105
   317
bulwahn@41085
   318
instantiation Enum.finite_1 :: check_all
bulwahn@41085
   319
begin
bulwahn@41085
   320
bulwahn@41085
   321
definition
bulwahn@41085
   322
  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
bulwahn@41085
   323
bulwahn@41177
   324
definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
bulwahn@41177
   325
where
bulwahn@41177
   326
  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
bulwahn@41177
   327
bulwahn@41085
   328
instance ..
bulwahn@41085
   329
bulwahn@41085
   330
end
bulwahn@41085
   331
bulwahn@41085
   332
instantiation Enum.finite_2 :: check_all
bulwahn@41085
   333
begin
bulwahn@41085
   334
bulwahn@41085
   335
definition
bulwahn@41085
   336
  "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
   337
bulwahn@41177
   338
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
bulwahn@41177
   339
where
bulwahn@41177
   340
  "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
bulwahn@41177
   341
bulwahn@41085
   342
instance ..
bulwahn@41085
   343
bulwahn@41085
   344
end
bulwahn@41085
   345
bulwahn@41085
   346
instantiation Enum.finite_3 :: check_all
bulwahn@41085
   347
begin
bulwahn@41085
   348
bulwahn@41085
   349
definition
bulwahn@41085
   350
  "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
   351
bulwahn@41177
   352
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
bulwahn@41177
   353
where
bulwahn@41177
   354
  "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
bulwahn@41177
   355
bulwahn@41085
   356
instance ..
bulwahn@41085
   357
bulwahn@41085
   358
end
bulwahn@41085
   359
bulwahn@41085
   360
bulwahn@41085
   361
huffman@40620
   362
subsection {* Defining combinators for any first-order data type *}
bulwahn@40420
   363
bulwahn@40420
   364
definition catch_match :: "term list option => term list option => term list option"
bulwahn@40420
   365
where
bulwahn@40420
   366
  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
bulwahn@40420
   367
bulwahn@40420
   368
code_const catch_match 
bulwahn@40420
   369
  (SML "(_) handle Match => _")
bulwahn@40420
   370
bulwahn@41918
   371
use "Tools/exhaustive_generators.ML"
bulwahn@40420
   372
bulwahn@41918
   373
setup {* Exhaustive_Generators.setup *}
bulwahn@40420
   374
bulwahn@40915
   375
declare [[quickcheck_tester = exhaustive]]
bulwahn@40915
   376
bulwahn@40899
   377
hide_fact orelse_def catch_match_def
bulwahn@41105
   378
no_notation orelse (infixr "orelse" 55)
bulwahn@41085
   379
hide_const (open) orelse catch_match mk_map_term check_all_n_lists
bulwahn@40420
   380
bulwahn@40420
   381
end