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