src/HOL/Quickcheck_Exhaustive.thy
author haftmann
Fri, 23 Dec 2016 20:12:27 +0100
changeset 64670 f77b946d18aa
parent 62979 1e527c40ae40
child 65956 639eb3617a86
permissions -rw-r--r--
restored instance for char, which got ancidentally lost in b3f2b8c906a6
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
     1
(*  Title:      HOL/Quickcheck_Exhaustive.thy
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
     3
*)
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
     5
section \<open>A simple counterexample generator performing exhaustive testing\<close>
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
     6
41918
d2ab869f8b0b replacing naming of small by exhaustive
bulwahn
parents: 41916
diff changeset
     7
theory Quickcheck_Exhaustive
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 49948
diff changeset
     8
imports Quickcheck_Random
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46417
diff changeset
     9
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
    10
begin
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    11
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    12
subsection \<open>Basic operations for exhaustive generators\<close>
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
    13
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    14
definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"  (infixr "orelse" 55)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    15
  where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    16
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    17
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    18
subsection \<open>Exhaustive generator type classes\<close>
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    19
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    20
class exhaustive = term_of +
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    21
  fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    22
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    23
class full_exhaustive = term_of +
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    24
  fixes full_exhaustive ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    25
    "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
    26
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    27
instantiation natural :: full_exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    28
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
    29
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    30
function full_exhaustive_natural' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    31
    "(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    32
      natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    33
  where "full_exhaustive_natural' f d i =
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    34
    (if d < i then None
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    35
     else (f (i, \<lambda>_. 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
    36
by pat_completeness auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    37
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    38
termination
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    39
  by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    40
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    41
definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    42
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    43
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    44
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    45
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    46
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    47
instantiation natural :: exhaustive
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    48
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
    49
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    50
function exhaustive_natural' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    51
    "(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    52
  where "exhaustive_natural' f d i =
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
    53
    (if d < i then None
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    54
     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
    55
by pat_completeness auto
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    56
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
    57
termination
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    58
  by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
51143
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
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
    61
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    62
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    63
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    64
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    65
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    66
instantiation integer :: exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    67
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    68
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    69
function exhaustive_integer' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    70
    "(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    71
  where "exhaustive_integer' f d i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    72
    (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    73
by pat_completeness auto
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
    74
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    75
termination
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    76
  by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    77
    (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
    78
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    79
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
    80
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    81
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    82
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    83
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    84
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    85
instantiation integer :: full_exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    86
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    87
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    88
function full_exhaustive_integer' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    89
    "(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    90
      integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    91
  where "full_exhaustive_integer' f d i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    92
    (if d < i then None
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    93
     else
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    94
      (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    95
        Some t \<Rightarrow> Some t
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    96
      | None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    97
by pat_completeness auto
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    98
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
    99
termination
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   100
  by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   101
    (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
   102
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   103
definition "full_exhaustive f d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   104
  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
   105
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   106
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   107
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   108
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   109
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   110
instantiation nat :: exhaustive
41231
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   111
begin
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   112
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   113
definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   114
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   115
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   116
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   117
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   118
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   119
instantiation nat :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   120
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   121
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   122
definition "full_exhaustive f d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   123
  full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. 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
   124
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   125
instance ..
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   126
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   127
end
2e901158675e adding exhaustive tester instances for numeric types: code_numeral, nat, rat and real
bulwahn
parents: 41178
diff changeset
   128
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   129
instantiation int :: exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   130
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   131
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   132
function exhaustive_int' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   133
    "(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   134
  where "exhaustive_int' f d i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   135
    (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
   136
by pat_completeness auto
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   137
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   138
termination
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   139
  by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   140
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   141
definition "exhaustive f d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   142
  exhaustive_int' f (int_of_integer (integer_of_natural d))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   143
    (- (int_of_integer (integer_of_natural d)))"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   144
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   145
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   146
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   147
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   148
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   149
instantiation int :: full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   150
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   151
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   152
function full_exhaustive_int' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   153
    "(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   154
      int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   155
  where "full_exhaustive_int' f d i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   156
    (if d < i then None
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   157
     else
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   158
      (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   159
        Some t \<Rightarrow> Some t
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   160
       | None \<Rightarrow> full_exhaustive_int' f d (i + 1)))"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   161
by pat_completeness auto
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   162
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   163
termination
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   164
  by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   165
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   166
definition "full_exhaustive f d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   167
  full_exhaustive_int' f (int_of_integer (integer_of_natural d))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   168
    (- (int_of_integer (integer_of_natural d)))"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   169
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   170
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   171
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   172
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   173
41916
80060d5f864a renaming constants in Quickcheck_Exhaustive theory
bulwahn
parents: 41915
diff changeset
   174
instantiation prod :: (exhaustive, exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   175
begin
40899
ef6fde932f4c improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
bulwahn
parents: 40639
diff changeset
   176
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   177
definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   178
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   179
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   180
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   181
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   182
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   183
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   184
  [code_unfold]: "valtermify_pair x y =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   185
    Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   186
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   187
instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   188
begin
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   189
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   190
definition "full_exhaustive f d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   191
  full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>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
   192
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   193
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   194
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   195
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   196
46193
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   197
instantiation set :: (exhaustive) exhaustive
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   198
begin
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   199
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   200
fun exhaustive_set
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   201
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   202
  "exhaustive_set f i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   203
    (if i = 0 then None
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   204
     else
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   205
      f {} orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   206
      exhaustive_set
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   207
        (\<lambda>A. f A orelse exhaustive (\<lambda>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
   208
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   209
instance ..
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   210
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   211
end
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   212
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   213
instantiation set :: (full_exhaustive) full_exhaustive
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   214
begin
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   215
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   216
fun full_exhaustive_set
46193
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   217
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   218
  "full_exhaustive_set f i =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   219
    (if i = 0 then None
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   220
     else
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   221
      f valterm_emptyset orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   222
      full_exhaustive_set
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   223
        (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   224
          (\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))"
46193
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   225
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   226
instance ..
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   227
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   228
end
55a4769d0abe adding exhaustive instances for type constructor set
bulwahn
parents: 45925
diff changeset
   229
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   230
instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   231
begin
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   232
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   233
fun exhaustive_fun' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   234
  "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   235
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   236
  "exhaustive_fun' f i d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   237
    (exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   238
      (if i > 1 then
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   239
        exhaustive_fun'
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   240
          (\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   241
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   242
definition exhaustive_fun ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   243
  "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   244
  where "exhaustive_fun f d = exhaustive_fun' f d d"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   245
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   246
instance ..
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   247
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   248
end
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   249
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   250
definition [code_unfold]:
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   251
  "valtermify_absdummy =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   252
    (\<lambda>(v, t).
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   253
      (\<lambda>_::'a. v,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   254
        \<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   255
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   256
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   257
  [code_unfold]: "valtermify_fun_upd g a b =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   258
    Code_Evaluation.valtermify
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   259
      (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   260
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   261
instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
42310
c664cc5cc5e9 splitting exhaustive and full_exhaustive into separate type classes
bulwahn
parents: 42305
diff changeset
   262
begin
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   263
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   264
fun full_exhaustive_fun' ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   265
  "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   266
    natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
42304
34366f39d32d new compilation for exhaustive quickcheck
bulwahn
parents: 42274
diff changeset
   267
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   268
  "full_exhaustive_fun' f i d =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   269
    full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   270
    (if i > 1 then
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   271
      full_exhaustive_fun'
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   272
        (\<lambda>g. full_exhaustive
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   273
          (\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   274
     else None)"
40639
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   275
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   276
definition full_exhaustive_fun ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   277
  "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   278
    natural \<Rightarrow> (bool \<times> term list) option"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   279
  where "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
   280
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   281
instance ..
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   282
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   283
end
f1f0e6adca0a adding function generation to SmallCheck; activating exhaustive search space testing
bulwahn
parents: 40620
diff changeset
   284
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   285
subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   286
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   287
class check_all = enum + term_of +
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   288
  fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   289
  fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   290
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   291
fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   292
  (bool \<times> 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
   293
where
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   294
  "check_all_n_lists f n =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   295
    (if n = 0 then f ([], (\<lambda>_. []))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   296
     else check_all (\<lambda>(x, xt).
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   297
      check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   298
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   299
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   300
  [code_unfold]: "termify_fun_upd g a b =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   301
    (Code_Evaluation.termify
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   302
      (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   303
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   304
definition mk_map_term ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   305
  "(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   306
    (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   307
  where "mk_map_term T1 T2 domm rng =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   308
    (\<lambda>_.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   309
      let
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   310
        T1 = T1 ();
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   311
        T2 = T2 ();
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   312
        update_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   313
          (\<lambda>g (a, b).
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   314
            Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   315
             (Code_Evaluation.Const (STR ''Fun.fun_upd'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   316
               (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   317
                  Typerep.Typerep (STR ''fun'') [T1,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   318
                    Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   319
                    g) a) b)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   320
      in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   321
        List.foldl update_term
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   322
          (Code_Evaluation.Abs (STR ''x'') T1
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   323
            (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   324
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   325
instantiation "fun" :: ("{equal,check_all}", check_all) check_all
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   326
begin
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   327
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   328
definition
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   329
  "check_all f =
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   330
    (let
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   331
      mk_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   332
        mk_map_term
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   333
          (\<lambda>_. Typerep.typerep (TYPE('a)))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   334
          (\<lambda>_. Typerep.typerep (TYPE('b)))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   335
          (enum_term_of (TYPE('a)));
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   336
      enum = (Enum.enum :: 'a list)
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   337
    in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   338
      check_all_n_lists
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   339
        (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   340
        (natural_of_nat (length enum)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   341
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   342
definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   343
  where "enum_term_of_fun =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   344
    (\<lambda>_ _.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   345
      let
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   346
        enum_term_of_a = enum_term_of (TYPE('a));
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   347
        mk_term =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   348
          mk_map_term
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   349
            (\<lambda>_. Typerep.typerep (TYPE('a)))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   350
            (\<lambda>_. Typerep.typerep (TYPE('b)))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   351
            enum_term_of_a
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   352
      in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   353
        map (\<lambda>ys. mk_term (\<lambda>_. ys) ())
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   354
          (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   355
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   356
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   357
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   358
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   359
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   360
fun (in term_syntax) check_all_subsets ::
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   361
  "(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   362
    ('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   363
where
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   364
  "check_all_subsets f [] = f valterm_emptyset"
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   365
| "check_all_subsets f (x # xs) =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   366
    check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   367
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   368
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   369
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   370
  [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   371
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   372
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   373
  [code_unfold]: "termify_insert x s =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   374
    Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set)  <\<cdot>> x <\<cdot>> s"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   375
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   376
definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   377
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   378
  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   379
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   380
instantiation set :: (check_all) check_all
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   381
begin
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   382
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   383
definition
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   384
  "check_all_set f =
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   385
     check_all_subsets f
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   386
      (zip (Enum.enum :: 'a list)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   387
        (map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   388
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   389
definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   390
  where "enum_term_of_set _ _ =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   391
    map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   392
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   393
instance ..
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   394
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   395
end
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   396
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   397
instantiation unit :: check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   398
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   399
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   400
definition "check_all f = f (Code_Evaluation.valtermify ())"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   401
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   402
definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   403
  where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   404
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   405
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   406
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   407
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   408
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   409
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   410
instantiation bool :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   411
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   412
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   413
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   414
  "check_all f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   415
    (case f (Code_Evaluation.valtermify False) of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   416
      Some x' \<Rightarrow> Some x'
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   417
    | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   418
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   419
definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   420
  where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   421
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   422
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   423
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   424
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   425
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   426
definition (in term_syntax) [code_unfold]:
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   427
  "termify_pair x y =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   428
    Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> '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
   429
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   430
instantiation prod :: (check_all, check_all) check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   431
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   432
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   433
definition "check_all f = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))"
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   434
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   435
definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   436
  where "enum_term_of_prod =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   437
    (\<lambda>_ _.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   438
      map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   439
        (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
   440
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   441
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   442
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   443
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   444
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   445
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   446
  [code_unfold]: "valtermify_Inl x =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   447
    Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   448
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   449
definition (in term_syntax)
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   450
  [code_unfold]: "valtermify_Inr x =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   451
    Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   452
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   453
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
   454
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   455
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   456
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   457
  "check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   458
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   459
definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   460
  where "enum_term_of_sum =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   461
    (\<lambda>_ _.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   462
      let
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   463
        T1 = Typerep.typerep (TYPE('a));
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   464
        T2 = Typerep.typerep (TYPE('b))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   465
      in
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   466
        map
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   467
          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   468
            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   469
          (enum_term_of (TYPE('a)) ()) @
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   470
        map
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   471
          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   472
            (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   473
          (enum_term_of (TYPE('b)) ()))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   474
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   475
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   476
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   477
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   478
64670
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   479
instantiation char :: check_all
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   480
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   481
64670
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   482
primrec check_all_char' ::
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   483
  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option"
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   484
  where "check_all_char' f [] = None"
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   485
  | "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c)
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   486
      orelse check_all_char' f cs"
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   487
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   488
definition check_all_char ::
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   489
  "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option"
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   490
  where "check_all f = check_all_char' f Enum.enum"
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   491
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   492
definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   493
where
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   494
  "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   495
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   496
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   497
64670
f77b946d18aa restored instance for char, which got ancidentally lost in b3f2b8c906a6
haftmann
parents: 62979
diff changeset
   498
end
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   499
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   500
instantiation option :: (check_all) check_all
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   501
begin
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   502
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   503
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   504
  "check_all f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   505
    f (Code_Evaluation.valtermify (None :: 'a option)) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   506
    check_all
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   507
      (\<lambda>(x, t).
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   508
        f
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   509
          (Some x,
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   510
            \<lambda>_. Code_Evaluation.App
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   511
              (Code_Evaluation.Const (STR ''Option.option.Some'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   512
                (Typerep.Typerep (STR ''fun'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   513
                [Typerep.typerep TYPE('a),
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   514
                 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
   515
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   516
definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   517
  where "enum_term_of_option =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   518
    (\<lambda> _ _.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   519
      Code_Evaluation.term_of (None :: 'a option) #
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   520
      (map
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   521
        (Code_Evaluation.App
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   522
          (Code_Evaluation.Const (STR ''Option.option.Some'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   523
            (Typerep.Typerep (STR ''fun'')
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   524
              [Typerep.typerep TYPE('a),
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   525
               Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   526
        (enum_term_of (TYPE('a)) ())))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   527
41105
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   528
instance ..
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   529
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   530
end
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   531
a76ee71c3313 adding check_all instances for a few more finite types in smallcheck
bulwahn
parents: 41104
diff changeset
   532
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   533
instantiation Enum.finite_1 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   534
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   535
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   536
definition "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
   537
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   538
definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   539
  where "enum_term_of_finite_1 = (\<lambda>_ _. [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
   540
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   541
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   542
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   543
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   544
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   545
instantiation Enum.finite_2 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   546
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   547
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   548
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   549
  "check_all f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   550
    (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   551
     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
   552
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   553
definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   554
  where "enum_term_of_finite_2 =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   555
    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   556
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   557
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   558
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   559
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   560
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   561
instantiation Enum.finite_3 :: check_all
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   562
begin
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   563
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   564
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   565
  "check_all f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   566
    (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   567
     f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   568
     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
   569
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   570
definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   571
  where "enum_term_of_finite_3 =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   572
    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
41177
810a885decee added enum_term_of to correct present nested functions
bulwahn
parents: 41105
diff changeset
   573
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   574
instance ..
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   575
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   576
end
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   577
46417
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   578
instantiation Enum.finite_4 :: check_all
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   579
begin
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   580
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   581
definition
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   582
  "check_all f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   583
    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   584
    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   585
    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   586
    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
   587
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   588
definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   589
  where "enum_term_of_finite_4 =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   590
    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
46417
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   591
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   592
instance ..
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   593
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   594
end
1a68fcb80b62 beautifying definitions of check_all and adding instance for finite_4
bulwahn
parents: 46311
diff changeset
   595
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   596
subsection \<open>Bounded universal quantifiers\<close>
41085
a549ff1d4070 adding a smarter enumeration scheme for finite functions
bulwahn
parents: 40915
diff changeset
   597
42195
1e7b62c93f5d adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents: 42117
diff changeset
   598
class bounded_forall =
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   599
  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
   600
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   601
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   602
subsection \<open>Fast exhaustive combinators\<close>
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   603
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   604
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
   605
  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   606
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   607
axiomatization throw_Counterexample :: "term list \<Rightarrow> unit"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   608
axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option"
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   609
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   610
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
   611
  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
   612
    (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
   613
| constant catch_Counterexample \<rightharpoonup>
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   614
    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   615
42305
494c31fdec95 theory definitions for fast exhaustive quickcheck compilation
bulwahn
parents: 42304
diff changeset
   616
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   617
subsection \<open>Continuation passing style functions as plus monad\<close>
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   618
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   619
type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   620
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   621
definition cps_empty :: "'a cps"
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   622
  where "cps_empty = (\<lambda>cont. None)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   623
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   624
definition cps_single :: "'a \<Rightarrow> 'a cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   625
  where "cps_single v = (\<lambda>cont. cont v)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   626
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   627
definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   628
  where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   629
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   630
definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   631
  where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   632
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   633
definition cps_if :: "bool \<Rightarrow> unit cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   634
  where "cps_if b = (if b then cps_single () else cps_empty)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   635
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   636
definition cps_not :: "unit cps \<Rightarrow> unit cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   637
  where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   638
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   639
type_synonym 'a pos_bound_cps =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   640
  "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   641
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   642
definition pos_bound_cps_empty :: "'a pos_bound_cps"
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   643
  where "pos_bound_cps_empty = (\<lambda>cont i. None)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   644
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   645
definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   646
  where "pos_bound_cps_single v = (\<lambda>cont i. cont v)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   647
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   648
definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   649
  where "pos_bound_cps_bind m f = (\<lambda>cont i. if i = 0 then None else (m (\<lambda>a. (f a) cont i) (i - 1)))"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   650
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   651
definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   652
  where "pos_bound_cps_plus a b = (\<lambda>c i. case a c i of None \<Rightarrow> b c i | Some x \<Rightarrow> Some x)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   653
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   654
definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   655
  where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   656
58350
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   657
datatype (plugins only: code extraction) (dead 'a) unknown =
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   658
  Unknown | Known 'a
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   659
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   660
datatype (plugins only: code extraction) (dead 'a) three_valued =
919149921e46 added 'extraction' plugins -- this might help 'HOL-Proofs'
blanchet
parents: 58334
diff changeset
   661
  Unknown_value | Value 'a | No_value
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   662
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   663
type_synonym 'a neg_bound_cps =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   664
  "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   665
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   666
definition neg_bound_cps_empty :: "'a neg_bound_cps"
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   667
  where "neg_bound_cps_empty = (\<lambda>cont i. No_value)"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   668
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   669
definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   670
  where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   671
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   672
definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   673
  where "neg_bound_cps_bind m f =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   674
    (\<lambda>cont i.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   675
      if i = 0 then cont Unknown
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   676
      else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   677
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   678
definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   679
  where "neg_bound_cps_plus a b =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   680
    (\<lambda>c i.
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   681
      case a c i of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   682
        No_value \<Rightarrow> b c i
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   683
      | Value x \<Rightarrow> Value x
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   684
      | Unknown_value \<Rightarrow>
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   685
          (case b c i of
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   686
            No_value \<Rightarrow> Unknown_value
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   687
          | Value x \<Rightarrow> Value x
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   688
          | Unknown_value \<Rightarrow> Unknown_value))"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   689
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   690
definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   691
  where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   692
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   693
definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   694
  where "neg_bound_cps_not n =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   695
    (\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   696
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   697
definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   698
  where "pos_bound_cps_not n =
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   699
    (\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)"
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   700
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   701
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   702
subsection \<open>Defining generators for any first-order data type\<close>
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
diff changeset
   703
45697
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   704
axiomatization unknown :: 'a
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   705
3b7c35a08723 more stable introduction of the internally used unknown term
bulwahn
parents: 45684
diff changeset
   706
notation (output) unknown  ("?")
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   707
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47203
diff changeset
   708
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
   709
43882
05d5696f177f renaming quickcheck_tester to quickcheck_batch_tester; tuned
bulwahn
parents: 42310
diff changeset
   710
declare [[quickcheck_batch_tester = exhaustive]]
40915
a4c956d1f91f declaring quickcheck testers as default after their setup
bulwahn
parents: 40914
diff changeset
   711
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   712
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59484
diff changeset
   713
subsection \<open>Defining generators for abstract types\<close>
45925
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   714
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47203
diff changeset
   715
ML_file "Tools/Quickcheck/abstract_generators.ML"
45925
cd4243c025bb quickcheck generators for abstract types; tuned
bulwahn
parents: 45818
diff changeset
   716
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 62364
diff changeset
   717
(* FIXME instantiation char :: full_exhaustive
62364
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   718
begin
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   719
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   720
definition full_exhaustive_char
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   721
where
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   722
  "full_exhaustive f i =
59484
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   723
     (if 0 < i then full_exhaustive_class.full_exhaustive
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   724
       (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   725
          (\<lambda>(c, d).
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   726
            f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   727
              \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   728
                 (Code_Evaluation.Const (STR ''String.char.Char'')
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   729
                   (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   730
                      (b ())) (d ()))) (i - 1)) (i - 1)
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   731
    else None)"
62364
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   732
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   733
instance ..
9209770bdcdf more direct bootstrap of char type, still retaining the nibble representation for syntax
haftmann
parents: 61121
diff changeset
   734
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 62364
diff changeset
   735
end *)
59484
a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler
haftmann
parents: 58889
diff changeset
   736
47203
ac625d8346b2 hiding fact not so aggressively
bulwahn
parents: 46950
diff changeset
   737
hide_fact (open) orelse_def
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   738
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
   739
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   740
hide_const valtermify_absdummy valtermify_fun_upd
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   741
  valterm_emptyset valtermify_insert
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   742
  valtermify_pair valtermify_Inl valtermify_Inr
46307
ec8f975c059b shortened definitions by adding some termify constants
bulwahn
parents: 46305
diff changeset
   743
  termify_fun_upd term_emptyset termify_insert termify_pair setify
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   744
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   745
hide_const (open)
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   746
  exhaustive full_exhaustive
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   747
  exhaustive_int' full_exhaustive_int'
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   748
  exhaustive_integer' full_exhaustive_integer'
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   749
  exhaustive_natural' full_exhaustive_natural'
45818
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   750
  throw_Counterexample catch_Counterexample
53a697f5454a hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn
parents: 45750
diff changeset
   751
  check_all enum_term_of
46305
8ea02e499d53 adding check_all instance for sets; tuned
bulwahn
parents: 46193
diff changeset
   752
  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
   753
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   754
hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   755
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   756
hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   757
  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   758
  pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   759
  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 62597
diff changeset
   760
  neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   761
  Unknown Known Unknown_value Value No_value
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   762
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 43882
diff changeset
   763
end