src/HOL/Quickcheck.thy
author haftmann
Wed, 23 Sep 2009 14:00:12 +0200
changeset 32657 5f13912245ff
parent 32373 c96330408d89
child 33250 5c2af18a3237
child 33561 ab01b72715ef
permissions -rw-r--r--
Code_Eval(uation)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29132
3dac98ebae24 restructured; circumvent sort problem
haftmann
parents: 28965
diff changeset
     1
(* Author: Florian Haftmann, TU Muenchen *)
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     2
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     3
header {* A simple counterexample generator *}
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
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
     6
imports Random Code_Evaluation
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
     7
uses ("Tools/quickcheck_generators.ML")
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     8
begin
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
     9
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    10
notation fcomp (infixl "o>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    11
notation scomp (infixl "o\<rightarrow>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    12
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    13
26265
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    14
subsection {* The @{text random} class *}
4b63b9e9b10d separated Random.thy from Quickcheck.thy
haftmann
parents:
diff changeset
    15
28335
25326092cf9a renamed rtype to typerep
haftmann
parents: 28315
diff changeset
    16
class random = typerep +
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    17
  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
    18
26267
ba710daf77a7 added combinator for interpretation of construction of datatype
haftmann
parents: 26265
diff changeset
    19
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    20
subsection {* Fundamental and numeric types*}
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    21
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    22
instantiation bool :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    23
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    24
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    25
definition
31985
a6e982b1ebba tuned quickcheck generator for bool
haftmann
parents: 31641
diff changeset
    26
  "random i = Random.range 2 o\<rightarrow>
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    27
    (\<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
    28
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    29
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    30
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    31
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    32
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    33
instantiation itself :: (typerep) random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    34
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    35
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    36
definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    37
  "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    38
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    39
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    40
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    41
end
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    42
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    43
instantiation char :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    44
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    45
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    46
definition
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    47
  "random _ = Random.select chars o\<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
    48
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    49
instance ..
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    50
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    51
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    52
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    53
instantiation String.literal :: random
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    54
begin
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    55
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    56
definition 
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    57
  "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
    58
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    59
instance ..
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
end
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
    62
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    63
instantiation nat :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    64
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    65
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    66
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    67
  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    68
     let n = Code_Numeral.nat_of k
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    69
     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    70
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    71
instance ..
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    72
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    73
end
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    74
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    75
instantiation int :: random
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    76
begin
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    77
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    78
definition
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    79
  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    80
     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
    81
     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    82
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    83
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    84
30945
0418e9bffbba separate channel for Quickcheck evaluations
haftmann
parents: 29823
diff changeset
    85
end
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    86
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    87
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    88
subsection {* Complex generators *}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    89
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
    90
text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
    91
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
    92
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
    93
  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
    94
  \<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
    95
31622
b30570327b76 more convenient signature for random_fun_lift
haftmann
parents: 31607
diff changeset
    96
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
b30570327b76 more convenient signature for random_fun_lift
haftmann
parents: 31607
diff changeset
    97
  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32373
diff changeset
    98
  "random_fun_lift f = 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
    99
31985
a6e982b1ebba tuned quickcheck generator for bool
haftmann
parents: 31641
diff changeset
   100
instantiation "fun" :: ("{eq, term_of}", random) random
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   101
begin
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   102
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   103
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
31622
b30570327b76 more convenient signature for random_fun_lift
haftmann
parents: 31607
diff changeset
   104
  "random i = random_fun_lift (random i)"
31603
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   105
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   106
instance ..
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   107
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   108
end
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   109
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   110
text {* Towards type copies and datatypes *}
fa30cd74d7d6 revised interpretation combinator for datatype constructions
haftmann
parents: 31483
diff changeset
   111
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   112
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   113
  "collapse f = (f o\<rightarrow> id)"
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   114
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   115
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   116
  "beyond k l = (if l > k then l else 0)"
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   117
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   118
lemma beyond_zero:
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   119
  "beyond k 0 = 0"
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   120
  by (simp add: beyond_def)
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   121
31483
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   122
lemma random_aux_rec:
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   123
  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   124
  assumes "random_aux 0 = rhs 0"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   125
    and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   126
  shows "random_aux k = rhs k"
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   127
  using assms by (rule code_numeral.induct)
88210717bfc8 added generator for char and trivial generator for String.literal
haftmann
parents: 31267
diff changeset
   128
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   129
use "Tools/quickcheck_generators.ML"
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   130
setup {* Quickcheck_Generators.setup *}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   131
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   132
code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   133
  -- {* With enough criminal energy this can be abused to derive @{prop False};
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   134
  for this reason we use a distinguished target @{text Quickcheck}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   135
  not spoiling the regular trusted code generation *}
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   136
31607
674348914ebc tuned order
haftmann
parents: 31603
diff changeset
   137
code_reserved Quickcheck Quickcheck_Generators
674348914ebc tuned order
haftmann
parents: 31603
diff changeset
   138
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   139
31641
feea4d3d743d hide constant Quickcheck.random
haftmann
parents: 31622
diff changeset
   140
hide (open) const random collapse beyond random_fun_aux random_fun_lift
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   141
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   142
no_notation fcomp (infixl "o>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   143
no_notation scomp (infixl "o\<rightarrow>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   144
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   145
end