src/HOL/Quickcheck_Exhaustive.thy
author bulwahn
Wed, 30 Nov 2011 15:07:10 +0100
changeset 45697 3b7c35a08723
parent 45684 3d6ee9c7d7ef
child 45718 8979b2463fc8
permissions -rw-r--r--
more stable introduction of the internally used unknown term
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     1
(* Author: Lukas Bulwahn, TU Muenchen *)
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     2
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
     3
header {* A simple counterexample generator performing exhaustive testing *}
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     4
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41916
diff changeset
     5
theory Quickcheck_Exhaustive
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     6
imports Quickcheck
41920
d4fb7a418152 moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents: 41918
diff changeset
     7
uses ("Tools/Quickcheck/exhaustive_generators.ML")
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     8
begin
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     9
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    10
subsection {* basic operations for exhaustive generators *}
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
    11
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
    12
definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
    13
where
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
    14
  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    15
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    16
subsection {* exhaustive generator type classes *}
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    17
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    18
class exhaustive = term_of +
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    19
  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    20
  
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    21
class full_exhaustive = term_of +
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    22
  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    23
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    24
instantiation code_numeral :: full_exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    25
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    26
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    27
function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    28
  where "full_exhaustive_code_numeral' f d i =
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    29
    (if d < i then None
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    30
    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    31
by pat_completeness auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    32
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    33
termination
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    34
  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    35
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    36
definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    37
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    38
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    39
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    40
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    41
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    42
instantiation code_numeral :: exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    43
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    44
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    45
function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    46
  where "exhaustive_code_numeral' f d i =
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    47
    (if d < i then None
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    48
    else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    49
by pat_completeness auto
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    50
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    51
termination
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    52
  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    53
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    54
definition "exhaustive f d = exhaustive_code_numeral' f d 0"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    55
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    56
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    57
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    58
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    59
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    60
instantiation nat :: exhaustive
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    61
begin
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    62
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    63
definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    64
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    65
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    66
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    67
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    68
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    69
instantiation nat :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    70
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    71
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    72
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"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    73
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    74
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    75
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    76
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    77
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    78
instantiation int :: exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    79
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    80
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    81
function exhaustive' :: "(int => term list option) => int => int => term list option"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    82
  where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    83
by pat_completeness auto
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    84
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    85
termination 
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    86
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    87
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    88
definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    89
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    90
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    91
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    92
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    93
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    94
instantiation int :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    95
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    96
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    97
function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    98
  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)))"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    99
by pat_completeness auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   100
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   101
termination 
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   102
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   103
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   104
definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   105
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   106
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   107
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   108
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   109
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   110
instantiation prod :: (exhaustive, exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   111
begin
40899
ef6fde932f4c improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents: 40639
diff changeset
   112
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   113
definition
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   114
  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   115
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   116
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   117
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   118
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   119
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   120
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   121
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   122
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   123
definition
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   124
  "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
41719
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   125
    %u. let T1 = (Typerep.typerep (TYPE('a)));
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   126
            T2 = (Typerep.typerep (TYPE('b)))
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   127
    in Code_Evaluation.App (Code_Evaluation.App (
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   128
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   129
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   130
      (t1 ())) (t2 ()))) d) d"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   131
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   132
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   133
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   134
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   135
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   136
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   137
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   138
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   139
fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   140
where
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   141
  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   142
   orelse (if i > 1 then
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   143
     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   144
       f (g(a := b))) d) d) (i - 1) d else None)"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   145
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   146
definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   147
where
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   148
  "exhaustive_fun f d = exhaustive_fun' f d d" 
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   149
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   150
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   151
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   152
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   153
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   154
instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   155
begin
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   156
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   157
fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   158
where
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   159
  "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
42117
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   160
   orelse (if i > 1 then
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   161
     full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
42117
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   162
       f (g(a := b),
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   163
         (%_. let A = (Typerep.typerep (TYPE('a)));
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   164
                  B = (Typerep.typerep (TYPE('b)));
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   165
                  fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   166
              in
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   167
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   168
                  (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   169
                (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   170
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   171
definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   172
where
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   173
  "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   174
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   175
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   176
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   177
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   178
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   179
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   180
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   181
class check_all = enum + term_of +
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   182
  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   183
  fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   184
  
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   185
fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   186
where
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   187
  "check_all_n_lists f n =
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   188
     (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   189
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   190
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"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   191
where
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   192
  "mk_map_term T1 T2 domm rng =
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   193
     (%_. let T1 = T1 ();
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   194
              T2 = T2 ();
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   195
              update_term = (%g (a, b).
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   196
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   197
                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   198
                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   199
                      Typerep.Typerep (STR ''fun'') [T1,
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   200
                        Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   201
                        g) a) b)
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   202
          in
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   203
             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   204
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   205
instantiation "fun" :: ("{equal, check_all}", check_all) check_all
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   206
begin
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   207
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   208
definition
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   209
  "check_all f =
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   210
    (let
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   211
      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   212
      enum = (Enum.enum :: 'a list)
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   213
    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)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   214
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   215
definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   216
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   217
  "enum_term_of_fun = (%_ _. let
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   218
    enum_term_of_a = enum_term_of (TYPE('a));
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   219
    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   220
  in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   221
 
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   222
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   223
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   224
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   225
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   226
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   227
instantiation unit :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   228
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   229
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   230
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   231
  "check_all f = f (Code_Evaluation.valtermify ())"
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   232
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   233
definition enum_term_of_unit :: "unit itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   234
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   235
  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   236
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   237
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   238
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   239
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   240
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   241
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   242
instantiation bool :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   243
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   244
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   245
definition
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   246
  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   247
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   248
definition enum_term_of_bool :: "bool itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   249
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   250
  "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   251
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   252
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   253
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   254
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   255
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   256
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   257
instantiation prod :: (check_all, check_all) check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   258
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   259
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   260
definition
41719
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   261
  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   262
    %u. let T1 = (Typerep.typerep (TYPE('a)));
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   263
            T2 = (Typerep.typerep (TYPE('b)))
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   264
    in Code_Evaluation.App (Code_Evaluation.App (
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   265
      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   266
      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   267
      (t1 ())) (t2 ()))))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   268
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   269
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   270
where
41719
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   271
  "enum_term_of_prod = (%_ _. map (%(x, y).
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   272
       let T1 = (Typerep.typerep (TYPE('a)));
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   273
           T2 = (Typerep.typerep (TYPE('b)))
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   274
       in Code_Evaluation.App (Code_Evaluation.App (
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   275
         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   276
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
91c2510e19c5 improving term construction of product types in Smallcheck which enables correct presentation of counterexamples
bulwahn
parents: 41231
diff changeset
   277
     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   278
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   279
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   280
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   281
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   282
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   283
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   284
instantiation sum :: (check_all, check_all) check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   285
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   286
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   287
definition
41722
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   288
  "check_all f = (case check_all (%(a, t). f (Inl a, %_. 
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   289
     let T1 = (Typerep.typerep (TYPE('a)));
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   290
         T2 = (Typerep.typerep (TYPE('b)))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   291
       in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   292
           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   293
             | None => check_all (%(b, t). f (Inr b, %_. let
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   294
                 T1 = (Typerep.typerep (TYPE('a)));
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   295
                 T2 = (Typerep.typerep (TYPE('b)))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   296
               in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   297
                 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   298
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   299
definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   300
where
41722
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   301
  "enum_term_of_sum = (%_ _.
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   302
     let
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   303
       T1 = (Typerep.typerep (TYPE('a)));
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   304
       T2 = (Typerep.typerep (TYPE('b)))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   305
     in
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   306
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   307
             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   308
             (enum_term_of (TYPE('a)) ()) @
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   309
       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   310
             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   311
             (enum_term_of (TYPE('b)) ()))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   312
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   313
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   314
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   315
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   316
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   317
instantiation nibble :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   318
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   319
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   320
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   321
  "check_all f =
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   322
    f (Code_Evaluation.valtermify Nibble0) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   323
    f (Code_Evaluation.valtermify Nibble1) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   324
    f (Code_Evaluation.valtermify Nibble2) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   325
    f (Code_Evaluation.valtermify Nibble3) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   326
    f (Code_Evaluation.valtermify Nibble4) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   327
    f (Code_Evaluation.valtermify Nibble5) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   328
    f (Code_Evaluation.valtermify Nibble6) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   329
    f (Code_Evaluation.valtermify Nibble7) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   330
    f (Code_Evaluation.valtermify Nibble8) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   331
    f (Code_Evaluation.valtermify Nibble9) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   332
    f (Code_Evaluation.valtermify NibbleA) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   333
    f (Code_Evaluation.valtermify NibbleB) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   334
    f (Code_Evaluation.valtermify NibbleC) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   335
    f (Code_Evaluation.valtermify NibbleD) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   336
    f (Code_Evaluation.valtermify NibbleE) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   337
    f (Code_Evaluation.valtermify NibbleF)"
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   338
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   339
definition enum_term_of_nibble :: "nibble itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   340
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   341
  "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   342
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   343
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   344
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   345
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   346
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   347
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   348
instantiation char :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   349
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   350
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   351
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   352
  "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 ()))))"
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   353
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   354
definition enum_term_of_char :: "char itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   355
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   356
  "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   357
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   358
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   359
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   360
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   361
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   362
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   363
instantiation option :: (check_all) check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   364
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   365
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   366
definition
41178
f4d3acf0c4cc adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents: 41177
diff changeset
   367
  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
f4d3acf0c4cc adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents: 41177
diff changeset
   368
    (Code_Evaluation.Const (STR ''Option.option.Some'')
f4d3acf0c4cc adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents: 41177
diff changeset
   369
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   370
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   371
definition enum_term_of_option :: "'a option itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   372
where
41722
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   373
  "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   374
      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   375
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   376
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   377
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   378
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   379
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   380
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   381
instantiation Enum.finite_1 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   382
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   383
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   384
definition
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   385
  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   386
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   387
definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   388
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   389
  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   390
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   391
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   392
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   393
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   394
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   395
instantiation Enum.finite_2 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   396
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   397
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   398
definition
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   399
  "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))"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   400
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   401
definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   402
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   403
  "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   404
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   405
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   406
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   407
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   408
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   409
instantiation Enum.finite_3 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   410
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   411
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   412
definition
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   413
  "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)))"
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   414
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   415
definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   416
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   417
  "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   418
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   419
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   420
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   421
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   422
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   423
subsection {* Bounded universal quantifiers *}
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   424
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   425
class bounded_forall =
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   426
  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   427
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   428
subsection {* Fast exhaustive combinators *}
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   429
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   430
class fast_exhaustive = term_of +
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   431
  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   432
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   433
consts throw_Counterexample :: "term list => unit"
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   434
consts catch_Counterexample :: "unit => term list option"
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   435
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   436
code_const throw_Counterexample
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   437
  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   438
code_const catch_Counterexample
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   439
  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   440
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   441
subsection {* Continuation passing style functions as plus monad *}
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   442
  
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   443
type_synonym 'a cps = "('a => term list option) => term list option"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   444
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   445
definition cps_empty :: "'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   446
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   447
  "cps_empty = (%cont. None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   448
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   449
definition cps_single :: "'a => 'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   450
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   451
  "cps_single v = (%cont. cont v)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   452
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   453
definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   454
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   455
  "cps_bind m f = (%cont. m (%a. (f a) cont))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   456
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   457
definition cps_plus :: "'a cps => 'a cps => 'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   458
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   459
  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   460
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   461
definition cps_if :: "bool => unit cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   462
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   463
  "cps_if b = (if b then cps_single () else cps_empty)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   464
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   465
definition cps_not :: "unit cps => unit cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   466
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   467
  "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   468
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   469
type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   470
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   471
definition pos_bound_cps_empty :: "'a pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   472
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   473
  "pos_bound_cps_empty = (%cont i. None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   474
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   475
definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   476
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   477
  "pos_bound_cps_single v = (%cont i. cont v)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   478
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   479
definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   480
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   481
  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   482
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   483
definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   484
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   485
  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   486
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   487
definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   488
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   489
  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   490
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   491
datatype 'a unknown = Unknown | Known 'a
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   492
datatype 'a three_valued = Unknown_value | Value 'a | No_value
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   493
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   494
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   495
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   496
definition neg_bound_cps_empty :: "'a neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   497
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   498
  "neg_bound_cps_empty = (%cont i. No_value)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   499
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   500
definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   501
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   502
  "neg_bound_cps_single v = (%cont i. cont (Known v))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   503
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   504
definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   505
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   506
  "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))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   507
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   508
definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   509
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   510
  "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))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   511
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   512
definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   513
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   514
  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   515
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   516
definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   517
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   518
  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   519
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   520
definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   521
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   522
  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   523
40620
7a9278de19ad section -> subsection
huffman
parents: 40420
diff changeset
   524
subsection {* Defining combinators for any first-order data type *}
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   525
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   526
definition catch_match :: "term list option => term list option => term list option"
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   527
where
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   528
  [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   529
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   530
code_const catch_match 
41920
d4fb7a418152 moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents: 41918
diff changeset
   531
  (Quickcheck "(_) handle Match => _")
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   532
45684
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   533
definition catch_match' :: "term => term => term"
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   534
where
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   535
  [code del]: "catch_match' t1 t2 = (SOME t. t = t1 \<or> t = t2)"
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   536
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   537
code_const catch_match'
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   538
  (Quickcheck "(_) handle Match => _")
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   539
45697
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   540
axiomatization unknown :: 'a
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   541
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   542
notation (output) unknown  ("?")
45684
3d6ee9c7d7ef adding a exception-safe term reification step in quickcheck; adding examples
bulwahn
parents: 45450
diff changeset
   543
 
41920
d4fb7a418152 moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents: 41918
diff changeset
   544
use "Tools/Quickcheck/exhaustive_generators.ML"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   545
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41916
diff changeset
   546
setup {* Exhaustive_Generators.setup *}
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   547
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 42310
diff changeset
   548
declare [[quickcheck_batch_tester = exhaustive]]
40915
a4c956d1f91f declaring quickcheck testers as default after their setup
bulwahn
parents: 40914
diff changeset
   549
40899
ef6fde932f4c improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents: 40639
diff changeset
   550
hide_fact orelse_def catch_match_def
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   551
no_notation orelse (infixr "orelse" 55)
45697
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   552
hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists 
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   553
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   554
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   555
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   556
  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   557
  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   558
  Unknown Known Unknown_value Value No_value
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   559
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   560
end