src/HOL/Quickcheck.thy
author haftmann
Wed, 27 May 2009 22:11:05 +0200
changeset 31267 4a85a4afc97d
parent 31260 4d273d043d59
child 31483 88210717bfc8
permissions -rw-r--r--
added lemma beyond_zero; hide constants
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
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31194
diff changeset
     6
imports Random Code_Eval
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
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    26
  "random i = Random.range i o\<rightarrow>
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    27
    (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
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
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    37
  "random_itself _ = Pair (Code_Eval.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
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    43
instantiation nat :: random
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    44
begin
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    45
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
    46
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    47
  "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
    48
     let n = Code_Numeral.nat_of k
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    49
     in (n, \<lambda>_. Code_Eval.term_of n)))"
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    50
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    51
instance ..
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    52
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    53
end
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    54
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    55
instantiation int :: random
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    56
begin
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    57
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    58
definition
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    59
  "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
    60
     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
31194
1d6926f96440 added quickcheck support for numeric types
haftmann
parents: 31186
diff changeset
    61
     in (j, \<lambda>_. Code_Eval.term_of j)))"
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    62
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    63
instance ..
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    64
30945
0418e9bffbba separate channel for Quickcheck evaluations
haftmann
parents: 29823
diff changeset
    65
end
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
    66
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    67
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    68
subsection {* Complex generators *}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    69
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    70
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
    71
  "collapse f = (f o\<rightarrow> id)"
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
    72
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    73
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    74
  "beyond k l = (if l > k then l else 0)"
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    75
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
    76
lemma beyond_zero:
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
    77
  "beyond k 0 = 0"
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
    78
  by (simp add: beyond_def)
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
    79
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    80
use "Tools/quickcheck_generators.ML"
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    81
setup {* Quickcheck_Generators.setup *}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    82
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    83
code_reserved Quickcheck Quickcheck_Generators
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    84
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    85
text {* Type @{typ "'a \<Rightarrow> 'b"} *}
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
    86
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    87
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    88
  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    89
  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
    90
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    91
code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun")
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    92
  -- {* With enough criminal energy this can be abused to derive @{prop False};
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    93
  for this reason we use a distinguished target @{text Quickcheck}
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    94
  not spoiling the regular trusted code generation *}
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
    95
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    96
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    97
begin
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
    98
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
    99
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   100
  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   101
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31245
diff changeset
   102
instance ..
31223
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   103
87bde6b5f793 re-added corrected version of type copy quickcheck generator
haftmann
parents: 31211
diff changeset
   104
end
31245
haftmann
parents: 31223
diff changeset
   105
haftmann
parents: 31223
diff changeset
   106
31267
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   107
hide (open) const collapse beyond
4a85a4afc97d added lemma beyond_zero; hide constants
haftmann
parents: 31260
diff changeset
   108
31179
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   109
no_notation fcomp (infixl "o>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   110
no_notation scomp (infixl "o\<rightarrow>" 60)
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   111
ced817160283 experimental addition of quickcheck
haftmann
parents: 31153
diff changeset
   112
end