src/HOL/Quickcheck_Random.thy
author blanchet
Fri Sep 19 13:27:04 2014 +0200 (2014-09-19)
changeset 58389 ee1f45ca0d73
parent 58152 6fe60a9a5bad
child 58826 2ed2eaabe3df
permissions -rw-r--r--
made new 'primrec' bootstrapping-capable
bulwahn@41922
     1
(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
haftmann@26265
     2
bulwahn@41922
     3
header {* A simple counterexample generator performing random testing *}
haftmann@26265
     4
haftmann@51126
     5
theory Quickcheck_Random
bulwahn@40650
     6
imports Random Code_Evaluation Enum
haftmann@26265
     7
begin
haftmann@26265
     8
haftmann@37751
     9
notation fcomp (infixl "\<circ>>" 60)
haftmann@37751
    10
notation scomp (infixl "\<circ>\<rightarrow>" 60)
haftmann@31179
    11
haftmann@55147
    12
setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, I)) *}
bulwahn@45718
    13
bulwahn@45718
    14
subsection {* Catching Match exceptions *}
bulwahn@45718
    15
bulwahn@45801
    16
axiomatization catch_match :: "'a => 'a => 'a"
bulwahn@45718
    17
haftmann@52435
    18
code_printing
haftmann@52435
    19
  constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
haftmann@31179
    20
haftmann@26265
    21
subsection {* The @{text random} class *}
haftmann@26265
    22
haftmann@28335
    23
class random = typerep +
haftmann@51143
    24
  fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
haftmann@26265
    25
haftmann@26267
    26
haftmann@31260
    27
subsection {* Fundamental and numeric types*}
haftmann@31179
    28
haftmann@31179
    29
instantiation bool :: random
haftmann@31179
    30
begin
haftmann@31179
    31
haftmann@31179
    32
definition
haftmann@37751
    33
  "random i = Random.range 2 \<circ>\<rightarrow>
haftmann@32657
    34
    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
haftmann@31179
    35
haftmann@31179
    36
instance ..
haftmann@31179
    37
haftmann@31179
    38
end
haftmann@31179
    39
haftmann@31179
    40
instantiation itself :: (typerep) random
haftmann@31179
    41
begin
haftmann@31179
    42
wenzelm@46975
    43
definition
haftmann@51143
    44
  random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
wenzelm@46975
    45
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
haftmann@31179
    46
haftmann@31179
    47
instance ..
haftmann@31179
    48
haftmann@31179
    49
end
haftmann@31179
    50
haftmann@31483
    51
instantiation char :: random
haftmann@31483
    52
begin
haftmann@31483
    53
haftmann@31483
    54
definition
haftmann@49972
    55
  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
haftmann@31483
    56
haftmann@31483
    57
instance ..
haftmann@31483
    58
haftmann@31483
    59
end
haftmann@31483
    60
haftmann@31483
    61
instantiation String.literal :: random
haftmann@31483
    62
begin
haftmann@31483
    63
haftmann@31483
    64
definition 
haftmann@32657
    65
  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
haftmann@31483
    66
haftmann@31483
    67
instance ..
haftmann@31483
    68
haftmann@31483
    69
end
haftmann@31483
    70
haftmann@31179
    71
instantiation nat :: random
haftmann@31179
    72
begin
haftmann@31179
    73
haftmann@51143
    74
definition random_nat :: "natural \<Rightarrow> Random.seed
wenzelm@46975
    75
  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
wenzelm@46975
    76
where
haftmann@37751
    77
  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
haftmann@51143
    78
     let n = nat_of_natural k
haftmann@32657
    79
     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
haftmann@31194
    80
haftmann@31194
    81
instance ..
haftmann@31194
    82
haftmann@31194
    83
end
haftmann@31194
    84
haftmann@31194
    85
instantiation int :: random
haftmann@31194
    86
begin
haftmann@31194
    87
haftmann@31194
    88
definition
haftmann@37751
    89
  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
haftmann@51143
    90
     let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k))))
haftmann@32657
    91
     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
haftmann@31179
    92
haftmann@31179
    93
instance ..
haftmann@31179
    94
haftmann@30945
    95
end
haftmann@31179
    96
haftmann@51143
    97
instantiation natural :: random
haftmann@51143
    98
begin
haftmann@51143
    99
haftmann@51143
   100
definition random_natural :: "natural \<Rightarrow> Random.seed
haftmann@51143
   101
  \<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
haftmann@51143
   102
where
haftmann@51143
   103
  "random_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>n. Pair (n, \<lambda>_. Code_Evaluation.term_of n))"
haftmann@51143
   104
haftmann@51143
   105
instance ..
haftmann@51143
   106
haftmann@51143
   107
end
haftmann@51143
   108
haftmann@51143
   109
instantiation integer :: random
haftmann@51143
   110
begin
haftmann@51143
   111
haftmann@51143
   112
definition random_integer :: "natural \<Rightarrow> Random.seed
haftmann@51143
   113
  \<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
haftmann@51143
   114
where
haftmann@51143
   115
  "random_integer i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
haftmann@51143
   116
     let j = (if k \<ge> i then integer_of_natural (k - i) else - (integer_of_natural (i - k)))
haftmann@51143
   117
      in (j, \<lambda>_. Code_Evaluation.term_of j)))"
haftmann@51143
   118
haftmann@51143
   119
instance ..
haftmann@51143
   120
haftmann@51143
   121
end
haftmann@51143
   122
haftmann@31260
   123
haftmann@31260
   124
subsection {* Complex generators *}
haftmann@31260
   125
haftmann@31603
   126
text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
haftmann@31603
   127
haftmann@31603
   128
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
wenzelm@46975
   129
  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
wenzelm@46975
   130
  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
haftmann@31603
   131
  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
haftmann@31603
   132
haftmann@31622
   133
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
wenzelm@46975
   134
  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
wenzelm@46975
   135
where
wenzelm@46975
   136
  "random_fun_lift f =
wenzelm@46975
   137
    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
haftmann@31603
   138
haftmann@38857
   139
instantiation "fun" :: ("{equal, term_of}", random) random
haftmann@31603
   140
begin
haftmann@31603
   141
wenzelm@46975
   142
definition
haftmann@51143
   143
  random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
wenzelm@46975
   144
  where "random i = random_fun_lift (random i)"
haftmann@31603
   145
haftmann@31603
   146
instance ..
haftmann@31603
   147
haftmann@31603
   148
end
haftmann@31603
   149
haftmann@31603
   150
text {* Towards type copies and datatypes *}
haftmann@31603
   151
wenzelm@46975
   152
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
wenzelm@46975
   153
  where "collapse f = (f \<circ>\<rightarrow> id)"
haftmann@31223
   154
haftmann@51143
   155
definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural"
wenzelm@46975
   156
  where "beyond k l = (if l > k then l else 0)"
haftmann@31260
   157
wenzelm@46975
   158
lemma beyond_zero: "beyond k 0 = 0"
haftmann@31267
   159
  by (simp add: beyond_def)
haftmann@31267
   160
bulwahn@46311
   161
wenzelm@46975
   162
definition (in term_syntax) [code_unfold]:
wenzelm@46975
   163
  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
wenzelm@46975
   164
wenzelm@46975
   165
definition (in term_syntax) [code_unfold]:
wenzelm@46975
   166
  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
bulwahn@46311
   167
bulwahn@46311
   168
instantiation set :: (random) random
bulwahn@46311
   169
begin
bulwahn@46311
   170
blanchet@58389
   171
fun random_aux_set
bulwahn@46311
   172
where
bulwahn@46311
   173
  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
wenzelm@46975
   174
| "random_aux_set (Code_Numeral.Suc i) j =
wenzelm@46975
   175
    collapse (Random.select_weight
wenzelm@46975
   176
      [(1, Pair valterm_emptyset),
wenzelm@46975
   177
       (Code_Numeral.Suc i,
wenzelm@46975
   178
        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
bulwahn@46311
   179
bulwahn@46311
   180
lemma [code]:
wenzelm@46975
   181
  "random_aux_set i j =
wenzelm@46975
   182
    collapse (Random.select_weight [(1, Pair valterm_emptyset),
wenzelm@46975
   183
      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
haftmann@51143
   184
proof (induct i rule: natural.induct)
bulwahn@46311
   185
  case zero
haftmann@50046
   186
  show ?case by (subst select_weight_drop_zero [symmetric])
haftmann@51143
   187
    (simp add: random_aux_set.simps [simplified] less_natural_def)
bulwahn@46311
   188
next
huffman@46547
   189
  case (Suc i)
haftmann@51143
   190
  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one)
bulwahn@46311
   191
qed
bulwahn@46311
   192
wenzelm@46975
   193
definition "random_set i = random_aux_set i i"
bulwahn@46311
   194
bulwahn@46311
   195
instance ..
bulwahn@46311
   196
bulwahn@46311
   197
end
bulwahn@46311
   198
haftmann@31483
   199
lemma random_aux_rec:
haftmann@51143
   200
  fixes random_aux :: "natural \<Rightarrow> 'a"
haftmann@31483
   201
  assumes "random_aux 0 = rhs 0"
huffman@46547
   202
    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
haftmann@31483
   203
  shows "random_aux k = rhs k"
haftmann@51143
   204
  using assms by (rule natural.induct)
haftmann@31483
   205
bulwahn@45718
   206
subsection {* Deriving random generators for datatypes *}
bulwahn@45718
   207
wenzelm@48891
   208
ML_file "Tools/Quickcheck/quickcheck_common.ML" 
wenzelm@48891
   209
ML_file "Tools/Quickcheck/random_generators.ML"
bulwahn@41923
   210
setup Random_Generators.setup
haftmann@34968
   211
haftmann@34968
   212
haftmann@34968
   213
subsection {* Code setup *}
blanchet@33561
   214
haftmann@52435
   215
code_printing
haftmann@52435
   216
  constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
haftmann@34968
   217
  -- {* With enough criminal energy this can be abused to derive @{prop False};
haftmann@34968
   218
  for this reason we use a distinguished target @{text Quickcheck}
haftmann@34968
   219
  not spoiling the regular trusted code generation *}
haftmann@34968
   220
bulwahn@41935
   221
code_reserved Quickcheck Random_Generators
haftmann@34968
   222
haftmann@37751
   223
no_notation fcomp (infixl "\<circ>>" 60)
haftmann@37751
   224
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
haftmann@51126
   225
    
bulwahn@45801
   226
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
bulwahn@45801
   227
haftmann@51126
   228
hide_fact (open) collapse_def beyond_def random_fun_lift_def
haftmann@31267
   229
haftmann@31179
   230
end