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