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