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