author  haftmann 
Mon, 08 Jun 2009 08:38:51 +0200  
changeset 31483  88210717bfc8 
parent 31267  4a85a4afc97d 
child 31603  fa30cd74d7d6 
permissions  rwrr 
29132  1 
(* Author: Florian Haftmann, TU Muenchen *) 
26265  2 

3 
header {* A simple counterexample generator *} 

4 

5 
theory Quickcheck 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31194
diff
changeset

6 
imports Random Code_Eval 
31260  7 
uses ("Tools/quickcheck_generators.ML") 
26265  8 
begin 
9 

31179  10 
notation fcomp (infixl "o>" 60) 
11 
notation scomp (infixl "o\<rightarrow>" 60) 

12 

13 

26265  14 
subsection {* The @{text random} class *} 
15 

28335  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  18 

26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

19 

31260  20 
subsection {* Fundamental and numeric types*} 
31179  21 

22 
instantiation bool :: random 

23 
begin 

24 

25 
definition 

31194  26 
"random i = Random.range i o\<rightarrow> 
27 
(\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))" 

31179  28 

29 
instance .. 

30 

31 
end 

32 

33 
instantiation itself :: (typerep) random 

34 
begin 

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  37 
"random_itself _ = Pair (Code_Eval.valtermify TYPE('a))" 
31179  38 

39 
instance .. 

40 

41 
end 

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 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

47 
"random _ = Random.select chars o\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Eval.term_of c))" 
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 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

57 
"random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))" 
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  63 
instantiation nat :: random 
64 
begin 

65 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

66 
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where 
31194  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 
31194  69 
in (n, \<lambda>_. Code_Eval.term_of n)))" 
70 

71 
instance .. 

72 

73 
end 

74 

75 
instantiation int :: random 

76 
begin 

77 

78 
definition 

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)) 
31194  81 
in (j, \<lambda>_. Code_Eval.term_of j)))" 
31179  82 

83 
instance .. 

84 

30945  85 
end 
31179  86 

31260  87 

88 
subsection {* Complex generators *} 

89 

90 
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 

91 
"collapse f = (f o\<rightarrow> id)" 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

92 

31260  93 
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where 
94 
"beyond k l = (if l > k then l else 0)" 

95 

31267  96 
lemma beyond_zero: 
97 
"beyond k 0 = 0" 

98 
by (simp add: beyond_def) 

99 

31483
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

100 
lemma random_aux_rec: 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

101 
fixes random_aux :: "code_numeral \<Rightarrow> 'a" 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

102 
assumes "random_aux 0 = rhs 0" 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

103 
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

104 
shows "random_aux k = rhs k" 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

105 
using assms by (rule code_numeral.induct) 
88210717bfc8
added generator for char and trivial generator for String.literal
haftmann
parents:
31267
diff
changeset

106 

31260  107 
use "Tools/quickcheck_generators.ML" 
108 
setup {* Quickcheck_Generators.setup *} 

109 

110 
code_reserved Quickcheck Quickcheck_Generators 

111 

112 
text {* Type @{typ "'a \<Rightarrow> 'b"} *} 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

113 

31260  114 
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
115 
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) 

116 
\<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

117 

31260  118 
code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun") 
119 
 {* With enough criminal energy this can be abused to derive @{prop False}; 

120 
for this reason we use a distinguished target @{text Quickcheck} 

121 
not spoiling the regular trusted code generation *} 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

122 

31260  123 
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random 
124 
begin 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

125 

31260  126 
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 
127 
"random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed" 

128 

129 
instance .. 

31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

130 

87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

131 
end 
31245  132 

133 

31267  134 
hide (open) const collapse beyond 
135 

31179  136 
no_notation fcomp (infixl "o>" 60) 
137 
no_notation scomp (infixl "o\<rightarrow>" 60) 

138 

139 
end 