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