src/HOL/Quickcheck_Exhaustive.thy
author blanchet
Tue, 16 Sep 2014 19:23:37 +0200
changeset 58350 919149921e46
parent 58334 7553a1bcecb7
child 58813 625d04d4fd2a
permissions -rw-r--r--
added 'extraction' plugins -- this might help 'HOL-Proofs'
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
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 49948
diff changeset
     6
imports Quickcheck_Random
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46417
diff changeset
     7
keywords "quickcheck_generator" :: thy_decl
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 +
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    19
  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * 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 +
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    22
  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    23
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    24
instantiation natural :: 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
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    27
function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    28
  where "full_exhaustive_natural' f d i =
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    29
    (if d < i then None
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    30
    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
42304
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
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    34
  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    35
    (auto simp add: less_natural_def)
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    36
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    37
definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    38
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    39
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    40
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    41
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    42
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    43
instantiation natural :: exhaustive
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    44
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    45
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    46
function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    47
  where "exhaustive_natural' f d i =
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    48
    (if d < i then None
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    49
    else (f i orelse exhaustive_natural' f d (i + 1)))"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    50
by pat_completeness auto
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    51
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    52
termination
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    53
  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    54
    (auto simp add: less_natural_def)
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    55
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    56
definition "exhaustive f d = exhaustive_natural' f d 0"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    57
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    58
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    59
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    60
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    61
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    62
instantiation integer :: exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    63
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    64
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    65
function exhaustive_integer' :: "(integer => (bool * term list) option) => integer => integer => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    66
  where "exhaustive_integer' f d i = (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    67
by pat_completeness auto
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    68
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    69
termination 
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    70
  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    71
    (auto simp add: less_integer_def nat_of_integer_def)
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    72
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    73
definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    74
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    75
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    76
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    77
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    78
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    79
instantiation integer :: full_exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    80
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    81
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    82
function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    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)))"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    84
by pat_completeness auto
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    85
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    86
termination 
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    87
  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    88
    (auto simp add: less_integer_def nat_of_integer_def)
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    89
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    90
definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    91
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    92
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    93
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    94
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    95
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    96
instantiation nat :: exhaustive
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    97
begin
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    98
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    99
definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   100
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   101
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   102
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   103
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   104
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   105
instantiation nat :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   106
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   107
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   108
definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d"
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   109
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   110
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   111
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   112
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   113
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   114
instantiation int :: exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   115
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   116
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   117
function exhaustive_int' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   118
  where "exhaustive_int' f d i = (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   119
by pat_completeness auto
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   120
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   121
termination 
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   122
  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
   123
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   124
definition "exhaustive f d = exhaustive_int' f (int_of_integer (integer_of_natural d))
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   125
  (- (int_of_integer (integer_of_natural d)))"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   126
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   127
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   128
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   129
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   130
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   131
instantiation int :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   132
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   133
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   134
function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   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)))"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   136
by pat_completeness auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   137
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   138
termination 
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   139
  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   140
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   141
definition "full_exhaustive f d = full_exhaustive_int' f (int_of_integer (integer_of_natural d))
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   142
  (- (int_of_integer (integer_of_natural d)))"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   143
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   144
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   145
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   146
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   147
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   148
instantiation prod :: (exhaustive, exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   149
begin
40899
ef6fde932f4c improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents: 40639
diff changeset
   150
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   151
definition
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   152
  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   153
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   154
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   155
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   156
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   157
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   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"
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   159
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   160
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   161
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   162
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   163
definition
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   164
  "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   165
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   166
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   167
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   168
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   169
46193
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   170
instantiation set :: (exhaustive) exhaustive
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   171
begin
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   172
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   173
fun exhaustive_set
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   174
where
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   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)))"
46193
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   176
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   177
instance ..
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   178
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   179
end
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   180
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   181
instantiation set :: (full_exhaustive) full_exhaustive
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   182
begin
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   183
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   184
fun full_exhaustive_set 
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   185
where
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   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)))"
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   187
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   188
instance ..
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   189
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   190
end
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   191
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   192
instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   193
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   194
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   195
fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   196
where
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   197
  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   198
   orelse (if i > 1 then
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   199
     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   200
       f (g(a := b))) d) d) (i - 1) d else None)"
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   201
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   202
definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => natural => (bool * term list) option"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   203
where
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   204
  "exhaustive_fun f d = exhaustive_fun' f d d" 
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   205
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   206
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   207
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   208
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   209
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   210
definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   211
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   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"
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   213
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   214
instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   215
begin
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   216
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   217
fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   218
where
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   219
  "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
42117
306713ec55c3 changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
bulwahn
parents: 41920
diff changeset
   220
   orelse (if i > 1 then
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   221
     full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   222
       f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   223
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   224
definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   225
where
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   226
  "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
   227
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   228
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   229
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   230
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   231
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   232
subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   233
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   234
class check_all = enum + term_of +
45722
63b42a7db003 changing the exhaustive generator signatures;
bulwahn
parents: 45718
diff changeset
   235
  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   236
  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
   237
  
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   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"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   239
where
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   240
  "check_all_n_lists f n =
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   241
     (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
   242
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   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)"
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   244
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   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"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   246
where
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   247
  "mk_map_term T1 T2 domm rng =
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   248
     (%_. let T1 = T1 ();
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   249
              T2 = T2 ();
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   250
              update_term = (%g (a, b).
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   251
                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   252
                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   253
                   (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
   254
                      Typerep.Typerep (STR ''fun'') [T1,
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   255
                        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
   256
                        g) a) b)
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   257
          in
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   258
             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
   259
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   260
instantiation "fun" :: ("{equal, check_all}", check_all) check_all
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   261
begin
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   262
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   263
definition
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   264
  "check_all f =
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   265
    (let
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   266
      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
   267
      enum = (Enum.enum :: 'a list)
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   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)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   269
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   270
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
   271
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   272
  "enum_term_of_fun = (%_ _. let
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   273
    enum_term_of_a = enum_term_of (TYPE('a));
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   274
    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
49948
744934b818c7 moved quite generic material from theory Enum to more appropriate places
haftmann
parents: 48891
diff changeset
   275
  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   276
 
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   277
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   278
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   279
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   280
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   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"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   282
where
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   283
  "check_all_subsets f [] = f valterm_emptyset"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   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"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   285
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   286
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   287
definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   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"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   289
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   290
definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   291
where
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   292
  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   293
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   294
instantiation set :: (check_all) check_all
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   295
begin
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   296
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   297
definition
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   298
  "check_all_set f =
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   299
     check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   300
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   301
definition enum_term_of_set :: "'a set itself => unit => term list"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   302
where
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   303
  "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   304
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   305
instance ..
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   306
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   307
end
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   308
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   309
instantiation unit :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   310
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   311
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   312
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   313
  "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
   314
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   315
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
   316
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   317
  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   318
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   319
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   320
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   321
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   322
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   323
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   324
instantiation bool :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   325
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   326
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   327
definition
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   328
  "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
   329
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   330
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
   331
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   332
  "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
   333
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   334
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   335
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   336
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   337
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   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"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   339
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   340
instantiation prod :: (check_all, check_all) check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   341
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   342
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   343
definition
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   344
  "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   345
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   346
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
   347
where
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   348
  "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
49948
744934b818c7 moved quite generic material from theory Enum to more appropriate places
haftmann
parents: 48891
diff changeset
   349
     (List.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
   350
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   351
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   352
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   353
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   354
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   355
definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x"
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   356
definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   357
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   358
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
   359
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   360
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   361
definition
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   362
  "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   363
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   364
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
   365
where
41722
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   366
  "enum_term_of_sum = (%_ _.
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   367
     let
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   368
       T1 = (Typerep.typerep (TYPE('a)));
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   369
       T2 = (Typerep.typerep (TYPE('b)))
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   370
     in
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   371
       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
   372
             (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
   373
             (enum_term_of (TYPE('a)) ()) @
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   374
       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
   375
             (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
   376
             (enum_term_of (TYPE('b)) ()))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   377
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   378
instance ..
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
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   381
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   382
instantiation nibble :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   383
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   384
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   385
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   386
  "check_all f =
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   387
    f (Code_Evaluation.valtermify Nibble0) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   388
    f (Code_Evaluation.valtermify Nibble1) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   389
    f (Code_Evaluation.valtermify Nibble2) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   390
    f (Code_Evaluation.valtermify Nibble3) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   391
    f (Code_Evaluation.valtermify Nibble4) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   392
    f (Code_Evaluation.valtermify Nibble5) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   393
    f (Code_Evaluation.valtermify Nibble6) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   394
    f (Code_Evaluation.valtermify Nibble7) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   395
    f (Code_Evaluation.valtermify Nibble8) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   396
    f (Code_Evaluation.valtermify Nibble9) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   397
    f (Code_Evaluation.valtermify NibbleA) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   398
    f (Code_Evaluation.valtermify NibbleB) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   399
    f (Code_Evaluation.valtermify NibbleC) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   400
    f (Code_Evaluation.valtermify NibbleD) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   401
    f (Code_Evaluation.valtermify NibbleE) orelse
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   402
    f (Code_Evaluation.valtermify NibbleF)"
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   403
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   404
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
   405
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   406
  "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
   407
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   408
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   409
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   410
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   411
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   412
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   413
instantiation char :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   414
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   415
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   416
definition
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   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 ()))))"
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   418
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   419
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
   420
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   421
  "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
   422
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   423
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   424
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   425
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   426
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   427
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   428
instantiation option :: (check_all) check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   429
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   430
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   431
definition
41178
f4d3acf0c4cc adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
bulwahn
parents: 41177
diff changeset
   432
  "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
   433
    (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
   434
      (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
   435
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   436
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
   437
where
41722
9575694d2da5 improving sum type and option type term constructions for correct presentation in Smallcheck
bulwahn
parents: 41719
diff changeset
   438
  "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
   439
      (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
   440
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   441
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   442
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   443
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   444
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   445
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   446
instantiation Enum.finite_1 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   447
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   448
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   449
definition
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   450
  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   451
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   452
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
   453
where
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   454
  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   455
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   456
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   457
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   458
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   459
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   460
instantiation Enum.finite_2 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   461
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   462
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   463
definition
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   464
  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   465
    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   466
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   467
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
   468
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   469
  "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
   470
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   471
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   472
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   473
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   474
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   475
instantiation Enum.finite_3 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   476
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   477
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   478
definition
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   479
  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   480
    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   481
    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   482
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   483
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
   484
where
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   485
  "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
   486
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   487
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   488
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   489
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   490
46417
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   491
instantiation Enum.finite_4 :: check_all
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   492
begin
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   493
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   494
definition
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   495
  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   496
    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   497
    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 52435
diff changeset
   498
    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
46417
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   499
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   500
definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   501
where
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   502
  "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   503
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   504
instance ..
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   505
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   506
end
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   507
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   508
subsection {* Bounded universal quantifiers *}
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   509
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   510
class bounded_forall =
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   511
  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   512
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   513
subsection {* Fast exhaustive combinators *}
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   514
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   515
class fast_exhaustive = term_of +
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   516
  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   517
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   518
axiomatization throw_Counterexample :: "term list => unit"
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   519
axiomatization catch_Counterexample :: "unit => term list option"
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   520
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   521
code_printing
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   522
  constant throw_Counterexample \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   523
    (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   524
| constant catch_Counterexample \<rightharpoonup>
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   525
    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   526
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   527
subsection {* Continuation passing style functions as plus monad *}
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   528
  
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   529
type_synonym 'a cps = "('a => term list option) => term list option"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   530
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   531
definition cps_empty :: "'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   532
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   533
  "cps_empty = (%cont. None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   534
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   535
definition cps_single :: "'a => 'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   536
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   537
  "cps_single v = (%cont. cont v)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   538
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   539
definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   540
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   541
  "cps_bind m f = (%cont. m (%a. (f a) cont))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   542
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   543
definition cps_plus :: "'a cps => 'a cps => 'a cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   544
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   545
  "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
   546
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   547
definition cps_if :: "bool => unit cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   548
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   549
  "cps_if b = (if b then cps_single () else cps_empty)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   550
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   551
definition cps_not :: "unit cps => unit cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   552
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   553
  "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
   554
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   555
type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => natural => (bool * term list) option"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   556
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   557
definition pos_bound_cps_empty :: "'a pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   558
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   559
  "pos_bound_cps_empty = (%cont i. None)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   560
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   561
definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   562
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   563
  "pos_bound_cps_single v = (%cont i. cont v)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   564
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   565
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
   566
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   567
  "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
   568
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   569
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
   570
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   571
  "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
   572
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   573
definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   574
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   575
  "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
   576
58350
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   577
datatype (plugins only: code extraction) (dead 'a) unknown =
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   578
  Unknown | Known 'a
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   579
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   580
datatype (plugins only: code extraction) (dead 'a) three_valued =
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   581
  Unknown_value | Value 'a | No_value
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   582
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   583
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   584
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   585
definition neg_bound_cps_empty :: "'a neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   586
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   587
  "neg_bound_cps_empty = (%cont i. No_value)"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   588
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   589
definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   590
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   591
  "neg_bound_cps_single v = (%cont i. cont (Known v))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   592
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   593
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
   594
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   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))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   596
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   597
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
   598
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   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))"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   600
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   601
definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   602
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   603
  "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
   604
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   605
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
   606
where
45750
17100f4ce0b5 adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents: 45733
diff changeset
   607
  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   608
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   609
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
   610
where
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   611
  "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
   612
45925
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   613
subsection {* Defining generators 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
   614
45697
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   615
axiomatization unknown :: 'a
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   616
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   617
notation (output) unknown  ("?")
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   618
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47203
diff changeset
   619
ML_file "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
   620
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41916
diff changeset
   621
setup {* Exhaustive_Generators.setup *}
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   622
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 42310
diff changeset
   623
declare [[quickcheck_batch_tester = exhaustive]]
40915
a4c956d1f91f declaring quickcheck testers as default after their setup
bulwahn
parents: 40914
diff changeset
   624
45925
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   625
subsection {* Defining generators for abstract types *}
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   626
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47203
diff changeset
   627
ML_file "Tools/Quickcheck/abstract_generators.ML"
45925
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   628
47203
ac625d8346b2 hiding fact not so aggressively
bulwahn
parents: 46950
diff changeset
   629
hide_fact (open) orelse_def
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   630
no_notation orelse (infixr "orelse" 55)
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   631
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   632
hide_fact
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   633
  exhaustive_int'_def
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   634
  exhaustive_integer'_def
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   635
  exhaustive_natural'_def
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   636
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   637
hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   638
  valtermify_Inl valtermify_Inr
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   639
  termify_fun_upd term_emptyset termify_insert termify_pair setify
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   640
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   641
hide_const (open)
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   642
  exhaustive full_exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   643
  exhaustive_int' full_exhaustive_int'
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   644
  exhaustive_integer' full_exhaustive_integer'
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   645
  exhaustive_natural' full_exhaustive_natural'
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   646
  throw_Counterexample catch_Counterexample
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   647
  check_all enum_term_of
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   648
  orelse unknown mk_map_term check_all_n_lists check_all_subsets
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   649
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   650
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
   651
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
   652
  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
   653
  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
   654
  Unknown Known Unknown_value Value No_value
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   655
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   656
end