author  haftmann 
Mon, 15 Jun 2009 16:13:03 +0200  
changeset 31641  feea4d3d743d 
parent 31622  b30570327b76 
child 31985  a6e982b1ebba 
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 

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  96 
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 
97 
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 

98 
"random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed" 

31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

99 

fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

100 
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random 
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  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  112 
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 
113 
"collapse f = (f o\<rightarrow> id)" 

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

114 

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

117 

31267  118 
lemma beyond_zero: 
119 
"beyond k 0 = 0" 

120 
by (simp add: beyond_def) 

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  129 
use "Tools/quickcheck_generators.ML" 
130 
setup {* Quickcheck_Generators.setup *} 

131 

132 
code_const random_fun_aux (Quickcheck "Quickcheck'_Generators.random'_fun") 

133 
 {* With enough criminal energy this can be abused to derive @{prop False}; 

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

135 
not spoiling the regular trusted code generation *} 

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

136 

31607  137 
code_reserved Quickcheck Quickcheck_Generators 
138 

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

139 

31641  140 
hide (open) const random collapse beyond random_fun_aux random_fun_lift 
31267  141 

31179  142 
no_notation fcomp (infixl "o>" 60) 
143 
no_notation scomp (infixl "o\<rightarrow>" 60) 

144 

145 
end 