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