src/HOL/Quickcheck.thy
author webertj
Fri, 19 Oct 2012 15:12:52 +0200
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 49972 f11f8905d9fd
permissions -rw-r--r--
Renamed {left,right}_distrib to distrib_{right,left}.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41922
fc070c5f3a4c adapting Quickcheck theory after moving ML files
bulwahn
parents: 40973
diff changeset
     1
(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     2
41922
fc070c5f3a4c adapting Quickcheck theory after moving ML files
bulwahn
parents: 40973
diff changeset
     3
header {* A simple counterexample generator performing random testing *}
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     4
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     5
theory Quickcheck
40650
d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents: 38857
diff changeset
     6
imports Random Code_Evaluation Enum
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     7
begin
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     8
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
     9
notation fcomp (infixl "\<circ>>" 60)
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    10
notation scomp (infixl "\<circ>\<rightarrow>" 60)
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    11
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    12
setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    13
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    14
subsection {* Catching Match exceptions *}
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    15
45801
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
    16
axiomatization catch_match :: "'a => 'a => 'a"
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    17
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    18
code_const catch_match 
48273
65233084e9d7 improved equality optimisation in Quickcheck
bulwahn
parents: 46976
diff changeset
    19
  (Quickcheck "((_) handle Match => _)")
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    20
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    21
subsection {* The @{text random} class *}
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    22
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28315
diff changeset
    23
class random = typerep +
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    24
  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    25
26267
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26265
diff changeset
    26
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    27
subsection {* Fundamental and numeric types*}
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    28
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    29
instantiation bool :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    30
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    31
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    32
definition
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    33
  "random i = Random.range 2 \<circ>\<rightarrow>
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    34
    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    35
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    36
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    37
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    38
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    39
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    40
instantiation itself :: (typerep) random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    41
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    42
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    43
definition
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    44
  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    45
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    46
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    47
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    48
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    49
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    50
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    51
instantiation char :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    52
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    53
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    54
definition
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    55
  "random _ = Random.select chars \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    56
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    57
instance ..
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    58
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    59
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    60
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    61
instantiation String.literal :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    62
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    63
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    64
definition 
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    65
  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    66
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    67
instance ..
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    68
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    69
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    70
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    71
instantiation nat :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    72
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    73
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    74
definition random_nat :: "code_numeral \<Rightarrow> Random.seed
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    75
  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    76
where
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    77
  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    78
     let n = Code_Numeral.nat_of k
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    79
     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    80
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    81
instance ..
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    82
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    83
end
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    84
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    85
instantiation int :: random
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    86
begin
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    87
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    88
definition
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    89
  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    90
     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    91
     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    92
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    93
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    94
30945
0418e9bffbba separate channel for Quickcheck evaluations
haftmann
parents: 29823
diff changeset
    95
end
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    96
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    97
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    98
subsection {* Complex generators *}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    99
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   100
text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   101
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   102
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   103
  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   104
  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   105
  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   106
31622
b30570327b76 more convenient signature for random_fun_lift
haftmann
parents: 31607
diff changeset
   107
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   108
  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   109
where
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   110
  "random_fun_lift f =
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   111
    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   112
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 37751
diff changeset
   113
instantiation "fun" :: ("{equal, term_of}", random) random
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   114
begin
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   115
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   116
definition
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   117
  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   118
  where "random i = random_fun_lift (random i)"
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   119
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   120
instance ..
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   121
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   122
end
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   123
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   124
text {* Towards type copies and datatypes *}
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   125
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   126
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   127
  where "collapse f = (f \<circ>\<rightarrow> id)"
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   128
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   129
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   130
  where "beyond k l = (if l > k then l else 0)"
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   131
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   132
lemma beyond_zero: "beyond k 0 = 0"
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   133
  by (simp add: beyond_def)
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   134
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   135
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   136
definition (in term_syntax) [code_unfold]:
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   137
  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   138
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   139
definition (in term_syntax) [code_unfold]:
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   140
  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   141
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   142
instantiation set :: (random) random
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   143
begin
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   144
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   145
primrec random_aux_set
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   146
where
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   147
  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   148
| "random_aux_set (Code_Numeral.Suc i) j =
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   149
    collapse (Random.select_weight
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   150
      [(1, Pair valterm_emptyset),
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   151
       (Code_Numeral.Suc i,
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   152
        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   153
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   154
lemma [code]:
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   155
  "random_aux_set i j =
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   156
    collapse (Random.select_weight [(1, Pair valterm_emptyset),
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   157
      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   158
proof (induct i rule: code_numeral.induct)
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   159
  case zero
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   160
  show ?case by (subst select_weight_drop_zero[symmetric])
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   161
    (simp add: filter.simps random_aux_set.simps[simplified])
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   162
next
46547
d1dcb91a512e use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents: 46311
diff changeset
   163
  case (Suc i)
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   164
  show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   165
qed
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   166
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   167
definition "random_set i = random_aux_set i i"
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   168
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   169
instance ..
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   170
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   171
end
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   172
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   173
lemma random_aux_rec:
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   174
  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   175
  assumes "random_aux 0 = rhs 0"
46547
d1dcb91a512e use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents: 46311
diff changeset
   176
    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   177
  shows "random_aux k = rhs k"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   178
  using assms by (rule code_numeral.induct)
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   179
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
   180
subsection {* Deriving random generators for datatypes *}
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
   181
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48273
diff changeset
   182
ML_file "Tools/Quickcheck/quickcheck_common.ML" 
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48273
diff changeset
   183
ML_file "Tools/Quickcheck/random_generators.ML"
41923
f05fc0711bc7 renaming signatures and structures; correcting header
bulwahn
parents: 41922
diff changeset
   184
setup Random_Generators.setup
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   185
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   186
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   187
subsection {* Code setup *}
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 32657
diff changeset
   188
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41928
diff changeset
   189
code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   190
  -- {* With enough criminal energy this can be abused to derive @{prop False};
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   191
  for this reason we use a distinguished target @{text Quickcheck}
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   192
  not spoiling the regular trusted code generation *}
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   193
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41928
diff changeset
   194
code_reserved Quickcheck Random_Generators
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   195
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
   196
no_notation fcomp (infixl "\<circ>>" 60)
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
   197
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   198
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   199
subsection {* The Random-Predicate Monad *} 
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   200
35880
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   201
fun iter' ::
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   202
  "'a itself => code_numeral => code_numeral => code_numeral * code_numeral
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   203
    => ('a::random) Predicate.pred"
35880
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   204
where
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   205
  "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   206
     let ((x, _), seed') = random sz seed
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   207
   in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   208
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   209
definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   210
  => ('a::random) Predicate.pred"
35880
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   211
where
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   212
  "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   213
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   214
lemma [code]:
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   215
  "iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   216
     let ((x, _), seed') = random sz seed
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   217
   in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   218
unfolding iter_def iter'.simps[of _ nrandom] ..
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35028
diff changeset
   219
42163
392fd6c4669c renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents: 42159
diff changeset
   220
type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   221
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   222
definition empty :: "'a randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   223
  where "empty = Pair (bot_class.bot)"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   224
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   225
definition single :: "'a => 'a randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   226
  where "single x = Pair (Predicate.single x)"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   227
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   228
definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   229
  where
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   230
    "bind R f = (\<lambda>s. let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   231
       (P, s') = R s;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   232
       (s1, s2) = Random.split_seed s'
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   233
     in (Predicate.bind P (%a. fst (f a s1)), s2))"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   234
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   235
definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   236
where
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   237
  "union R1 R2 = (\<lambda>s. let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   238
     (P1, s') = R1 s; (P2, s'') = R2 s'
44845
5e51075cbd97 added syntactic classes for "inf" and "sup"
krauss
parents: 42175
diff changeset
   239
   in (sup_class.sup P1 P2, s''))"
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   240
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   241
definition if_randompred :: "bool \<Rightarrow> unit randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   242
where
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   243
  "if_randompred b = (if b then single () else empty)"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   244
36049
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 35880
diff changeset
   245
definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 35880
diff changeset
   246
where
46664
1f6c140f9c72 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents: 46638
diff changeset
   247
  "iterate_upto f n m = Pair (Predicate.iterate_upto f n m)"
36049
0ce5b7a5c2fd adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents: 35880
diff changeset
   248
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   249
definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   250
where
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   251
  "not_randompred P = (\<lambda>s. let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   252
     (P', s') = P s
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   253
   in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   254
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   255
definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   256
  where "Random g = scomp g (Pair o (Predicate.single o fst))"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   257
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   258
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   259
  where "map f P = bind P (single o f)"
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 32657
diff changeset
   260
45801
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   261
hide_fact
46976
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   262
  random_bool_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   263
  random_itself_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   264
  random_char_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   265
  random_literal_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   266
  random_nat_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   267
  random_int_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   268
  random_fun_lift_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   269
  random_fun_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   270
  collapse_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   271
  beyond_def
80123a220219 'definition' no longer exports the foundational "raw_def";
wenzelm
parents: 46975
diff changeset
   272
  beyond_zero
45801
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   273
  random_aux_rec
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   274
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   275
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   276
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   277
hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   278
  if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36049
diff changeset
   279
hide_type (open) randompred
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   280
hide_const (open) iter' iter empty single bind union if_randompred
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   281
  iterate_upto not_randompred Random map
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   282
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   283
end