src/HOL/Quickcheck_Random.thy
author wenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70067 9b34dbeb1103
parent 69605 a96320074298
child 72581 de581f98a3a1
permissions -rw-r--r--
auxiliary operation for common uses of 'compile_generated_files';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62979
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61799
diff changeset
     1
(*  Title:      HOL/Quickcheck_Random.thy
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61799
diff changeset
     2
    Author:     Florian Haftmann & Lukas Bulwahn, TU Muenchen
1e527c40ae40 misc tuning and standardization;
wenzelm
parents: 61799
diff changeset
     3
*)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
     5
section \<open>A simple counterexample generator performing random testing\<close>
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     6
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50046
diff changeset
     7
theory Quickcheck_Random
40650
d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents: 38857
diff changeset
     8
imports Random Code_Evaluation Enum
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     9
begin
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    10
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    11
notation fcomp (infixl "\<circ>>" 60)
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    12
notation scomp (infixl "\<circ>\<rightarrow>" 60)
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    13
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
    14
setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close>
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    15
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
    16
subsection \<open>Catching Match exceptions\<close>
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    17
45801
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
    18
axiomatization catch_match :: "'a => 'a => 'a"
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
    19
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
    20
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
    21
  constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    22
68587
1148f63304f4 avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    23
code_reserved Quickcheck Match
1148f63304f4 avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    24
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
    25
subsection \<open>The \<open>random\<close> class\<close>
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    26
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28315
diff changeset
    27
class random = typerep +
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    28
  fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    29
26267
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26265
diff changeset
    30
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
    31
subsection \<open>Fundamental and numeric types\<close>
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    32
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    33
instantiation bool :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    34
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    35
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    36
definition
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    37
  "random i = Random.range 2 \<circ>\<rightarrow>
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    38
    (\<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
    39
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    40
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    41
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    42
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    43
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    44
instantiation itself :: (typerep) random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    45
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    46
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    47
definition
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    48
  random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    49
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    50
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    51
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    52
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    53
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    54
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    55
instantiation char :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    56
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    57
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    58
definition
49972
f11f8905d9fd incorporated constant chars into instantiation proof for enum;
haftmann
parents: 48891
diff changeset
    59
  "random _ = Random.select (Enum.enum :: char list) \<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
    60
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    61
instance ..
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    62
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    63
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    64
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    65
instantiation String.literal :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    66
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    67
68587
1148f63304f4 avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
    68
definition
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    69
  "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
    70
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    71
instance ..
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    72
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    73
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    74
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    75
instantiation nat :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    76
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    77
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    78
definition random_nat :: "natural \<Rightarrow> Random.seed
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    79
  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
    80
where
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    81
  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    82
     let n = nat_of_natural k
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    83
     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
31194
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
instance ..
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    86
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    87
end
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    88
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    89
instantiation int :: random
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    90
begin
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    91
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    92
definition
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
    93
  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
    94
     let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k))))
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    95
     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    96
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    97
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    98
30945
0418e9bffbba separate channel for Quickcheck evaluations
haftmann
parents: 29823
diff changeset
    99
end
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   100
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   101
instantiation natural :: random
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   102
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   103
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   104
definition random_natural :: "natural \<Rightarrow> Random.seed
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   105
  \<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   106
where
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   107
  "random_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>n. Pair (n, \<lambda>_. Code_Evaluation.term_of n))"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   108
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   109
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   110
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   111
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   112
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   113
instantiation integer :: random
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   114
begin
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   115
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   116
definition random_integer :: "natural \<Rightarrow> Random.seed
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   117
  \<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   118
where
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   119
  "random_integer i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   120
     let j = (if k \<ge> i then integer_of_natural (k - i) else - (integer_of_natural (i - k)))
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   121
      in (j, \<lambda>_. Code_Evaluation.term_of j)))"
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   122
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   123
instance ..
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   124
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   125
end
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   126
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   127
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
   128
subsection \<open>Complex generators\<close>
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   129
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68587
diff changeset
   130
text \<open>Towards \<^typ>\<open>'a \<Rightarrow> 'b\<close>\<close>
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   131
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   132
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
   133
  \<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
   134
  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   135
  \<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
   136
31622
b30570327b76 more convenient signature for random_fun_lift
haftmann
parents: 31607
diff changeset
   137
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   138
  \<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   139
where
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   140
  "random_fun_lift f =
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 62979
diff changeset
   141
    random_fun_aux TYPEREP('a) TYPEREP('b) (=) Code_Evaluation.term_of f Random.split_seed"
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   142
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 37751
diff changeset
   143
instantiation "fun" :: ("{equal, term_of}", random) random
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   144
begin
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   145
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   146
definition
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   147
  random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   148
  where "random i = random_fun_lift (random i)"
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   149
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   150
instance ..
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   151
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   152
end
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   153
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
   154
text \<open>Towards type copies and datatypes\<close>
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   155
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   156
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
   157
  where "collapse f = (f \<circ>\<rightarrow> id)"
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   158
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   159
definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural"
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   160
  where "beyond k l = (if l > k then l else 0)"
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   161
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   162
lemma beyond_zero: "beyond k 0 = 0"
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   163
  by (simp add: beyond_def)
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   164
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   165
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   166
definition (in term_syntax) [code_unfold]:
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   167
  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   168
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   169
definition (in term_syntax) [code_unfold]:
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   170
  "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
   171
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   172
instantiation set :: (random) random
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   173
begin
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   174
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58152
diff changeset
   175
fun random_aux_set
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   176
where
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   177
  "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
   178
| "random_aux_set (Code_Numeral.Suc i) j =
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   179
    collapse (Random.select_weight
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   180
      [(1, Pair valterm_emptyset),
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   181
       (Code_Numeral.Suc i,
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   182
        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
   183
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   184
lemma [code]:
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   185
  "random_aux_set i j =
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   186
    collapse (Random.select_weight [(1, Pair valterm_emptyset),
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   187
      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   188
proof (induct i rule: natural.induct)
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   189
  case zero
50046
0051dc4f301f dropped dead code;
haftmann
parents: 49972
diff changeset
   190
  show ?case by (subst select_weight_drop_zero [symmetric])
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   191
    (simp add: random_aux_set.simps [simplified] less_natural_def)
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   192
next
46547
d1dcb91a512e use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents: 46311
diff changeset
   193
  case (Suc i)
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   194
  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one)
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   195
qed
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   196
46975
c54ca5717f73 some attempts to fit source on screen;
wenzelm
parents: 46664
diff changeset
   197
definition "random_set i = random_aux_set i i"
46311
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   198
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   199
instance ..
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   200
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   201
end
56fae81902ce random instance for sets
bulwahn
parents: 45801
diff changeset
   202
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   203
lemma random_aux_rec:
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   204
  fixes random_aux :: "natural \<Rightarrow> 'a"
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   205
  assumes "random_aux 0 = rhs 0"
46547
d1dcb91a512e use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents: 46311
diff changeset
   206
    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
   207
  shows "random_aux k = rhs k"
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 51126
diff changeset
   208
  using assms by (rule natural.induct)
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   209
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
   210
subsection \<open>Deriving random generators for datatypes\<close>
45718
8979b2463fc8 quickcheck random can also find potential counterexamples;
bulwahn
parents: 45178
diff changeset
   211
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   212
ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
   213
ML_file \<open>Tools/Quickcheck/random_generators.ML\<close>
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   214
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   215
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
   216
subsection \<open>Code setup\<close>
33561
ab01b72715ef introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents: 32657
diff changeset
   217
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51143
diff changeset
   218
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
   219
  constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 68587
diff changeset
   220
  \<comment> \<open>With enough criminal energy this can be abused to derive \<^prop>\<open>False\<close>;
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61076
diff changeset
   221
  for this reason we use a distinguished target \<open>Quickcheck\<close>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59104
diff changeset
   222
  not spoiling the regular trusted code generation\<close>
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   223
41935
d786a8a3dc47 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents: 41928
diff changeset
   224
code_reserved Quickcheck Random_Generators
34968
ceeffca32eb0 tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
haftmann
parents: 33562
diff changeset
   225
37751
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
   226
no_notation fcomp (infixl "\<circ>>" 60)
89e16802b6cc nicer xsymbol syntax for fcomp and scomp
haftmann
parents: 36176
diff changeset
   227
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
68587
1148f63304f4 avoid clashes in quickcheck [random]
Lars Hupel <lars.hupel@mytum.de>
parents: 67399
diff changeset
   228
45801
5616fbda86e6 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents: 45733
diff changeset
   229
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
   230
51126
df86080de4cb reform of predicate compiler / quickcheck theories:
haftmann
parents: 50046
diff changeset
   231
hide_fact (open) collapse_def beyond_def random_fun_lift_def
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   232
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   233
end