author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46976  80123a220219 
child 48273  65233084e9d7 
permissions  rwrr 
41922  1 
(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *) 
26265  2 

41922  3 
header {* A simple counterexample generator performing random testing *} 
26265  4 

5 
theory Quickcheck 

40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
38857
diff
changeset

6 
imports Random Code_Evaluation Enum 
41928
05abcee548a1
adaptions in generators using the common functions
bulwahn
parents:
41923
diff
changeset

7 
uses 
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

8 
("Tools/Quickcheck/quickcheck_common.ML") 
41928
05abcee548a1
adaptions in generators using the common functions
bulwahn
parents:
41923
diff
changeset

9 
("Tools/Quickcheck/random_generators.ML") 
26265  10 
begin 
11 

37751  12 
notation fcomp (infixl "\<circ>>" 60) 
13 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

31179  14 

45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

15 
setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *} 
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

16 

8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

17 
subsection {* Catching Match exceptions *} 
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

18 

45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset

19 
axiomatization catch_match :: "'a => 'a => 'a" 
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

20 

8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

21 
code_const catch_match 
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

22 
(Quickcheck "(_) handle Match => _") 
31179  23 

26265  24 
subsection {* The @{text random} class *} 
25 

28335  26 
class random = typerep + 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

27 
fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 
26265  28 

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

29 

31260  30 
subsection {* Fundamental and numeric types*} 
31179  31 

32 
instantiation bool :: random 

33 
begin 

34 

35 
definition 

37751  36 
"random i = Random.range 2 \<circ>\<rightarrow> 
32657  37 
(\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))" 
31179  38 

39 
instance .. 

40 

41 
end 

42 

43 
instantiation itself :: (typerep) random 

44 
begin 

45 

46975  46 
definition 
47 
random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 

48 
where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" 

31179  49 

50 
instance .. 

51 

52 
end 

53 

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

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

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

56 

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

57 
definition 
37751  58 
"random _ = Random.select chars \<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

59 

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

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

61 

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

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

63 

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

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

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

66 

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

67 
definition 
32657  68 
"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

69 

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

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

71 

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

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

73 

31179  74 
instantiation nat :: random 
75 
begin 

76 

46975  77 
definition random_nat :: "code_numeral \<Rightarrow> Random.seed 
78 
\<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" 

79 
where 

37751  80 
"random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

81 
let n = Code_Numeral.nat_of k 
32657  82 
in (n, \<lambda>_. Code_Evaluation.term_of n)))" 
31194  83 

84 
instance .. 

85 

86 
end 

87 

88 
instantiation int :: random 

89 
begin 

90 

91 
definition 

37751  92 
"random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair ( 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

93 
let j = (if k \<ge> i then Code_Numeral.int_of (k  i) else  Code_Numeral.int_of (i  k)) 
32657  94 
in (j, \<lambda>_. Code_Evaluation.term_of j)))" 
31179  95 

96 
instance .. 

97 

30945  98 
end 
31179  99 

31260  100 

101 
subsection {* Complex generators *} 

102 

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

103 
text {* Towards @{typ "'a \<Rightarrow> 'b"} *} 
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

104 

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

105 
axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
46975  106 
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 
107 
\<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed) 

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

108 
\<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

109 

31622  110 
definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) 
46975  111 
\<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 
112 
where 

113 
"random_fun_lift f = 

114 
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

115 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37751
diff
changeset

116 
instantiation "fun" :: ("{equal, term_of}", random) random 
31603
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

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

118 

46975  119 
definition 
120 
random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" 

121 
where "random i = random_fun_lift (random i)" 

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

122 

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

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

124 

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

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

126 

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

127 
text {* Towards type copies and datatypes *} 
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

128 

46975  129 
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" 
130 
where "collapse f = (f \<circ>\<rightarrow> id)" 

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

131 

46975  132 
definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" 
133 
where "beyond k l = (if l > k then l else 0)" 

31260  134 

46975  135 
lemma beyond_zero: "beyond k 0 = 0" 
31267  136 
by (simp add: beyond_def) 
137 

46311  138 

46975  139 
definition (in term_syntax) [code_unfold]: 
140 
"valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)" 

141 

142 
definition (in term_syntax) [code_unfold]: 

143 
"valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" 

46311  144 

145 
instantiation set :: (random) random 

146 
begin 

147 

148 
primrec random_aux_set 

149 
where 

150 
"random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])" 

46975  151 
 "random_aux_set (Code_Numeral.Suc i) j = 
152 
collapse (Random.select_weight 

153 
[(1, Pair valterm_emptyset), 

154 
(Code_Numeral.Suc i, 

155 
random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" 

46311  156 

157 
lemma [code]: 

46975  158 
"random_aux_set i j = 
159 
collapse (Random.select_weight [(1, Pair valterm_emptyset), 

160 
(i, random j \<circ>\<rightarrow> (%x. random_aux_set (i  1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])" 

46311  161 
proof (induct i rule: code_numeral.induct) 
162 
case zero 

163 
show ?case by (subst select_weight_drop_zero[symmetric]) 

164 
(simp add: filter.simps random_aux_set.simps[simplified]) 

165 
next 

46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset

166 
case (Suc i) 
46311  167 
show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one) 
168 
qed 

169 

46975  170 
definition "random_set i = random_aux_set i i" 
46311  171 

172 
instance .. 

173 

174 
end 

175 

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

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

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

178 
assumes "random_aux 0 = rhs 0" 
46547
d1dcb91a512e
use qualified constant names instead of suffixes (from Florian Haftmann)
huffman
parents:
46311
diff
changeset

179 
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

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

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

182 

45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

183 
subsection {* Deriving random generators for datatypes *} 
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

184 

8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45178
diff
changeset

185 
use "Tools/Quickcheck/quickcheck_common.ML" 
41922  186 
use "Tools/Quickcheck/random_generators.ML" 
41923
f05fc0711bc7
renaming signatures and structures; correcting header
bulwahn
parents:
41922
diff
changeset

187 
setup Random_Generators.setup 
34968
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

188 

ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

189 

ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

190 
subsection {* Code setup *} 
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
32657
diff
changeset

191 

41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset

192 
code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun") 
34968
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

193 
 {* With enough criminal energy this can be abused to derive @{prop False}; 
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

194 
for this reason we use a distinguished target @{text Quickcheck} 
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

195 
not spoiling the regular trusted code generation *} 
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

196 

41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41928
diff
changeset

197 
code_reserved Quickcheck Random_Generators 
34968
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

198 

37751  199 
no_notation fcomp (infixl "\<circ>>" 60) 
200 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

34968
ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

201 

ceeffca32eb0
tuned structure; moved nonrelated quickcheck.setup to Code_Generator.thy
haftmann
parents:
33562
diff
changeset

202 
subsection {* The RandomPredicate Monad *} 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

203 

35880
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

204 
fun iter' :: 
46975  205 
"'a itself => code_numeral => code_numeral => code_numeral * code_numeral 
206 
=> ('a::random) Predicate.pred" 

35880
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

207 
where 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

208 
"iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

209 
let ((x, _), seed') = random sz seed 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

210 
in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom  1) sz seed')))" 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

211 

46975  212 
definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral 
213 
=> ('a::random) Predicate.pred" 

35880
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

214 
where 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

215 
"iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed" 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

216 

2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

217 
lemma [code]: 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

218 
"iter nrandom sz seed = (if nrandom = 0 then bot_class.bot else 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

219 
let ((x, _), seed') = random sz seed 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

220 
in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom  1) sz seed')))" 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

221 
unfolding iter_def iter'.simps[of _ nrandom] .. 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

222 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
42159
diff
changeset

223 
type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)" 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

224 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

225 
definition empty :: "'a randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

226 
where "empty = Pair (bot_class.bot)" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

227 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

228 
definition single :: "'a => 'a randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

229 
where "single x = Pair (Predicate.single x)" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

230 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

231 
definition bind :: "'a randompred \<Rightarrow> ('a \<Rightarrow> 'b randompred) \<Rightarrow> 'b randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

232 
where 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

233 
"bind R f = (\<lambda>s. let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

234 
(P, s') = R s; 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

235 
(s1, s2) = Random.split_seed s' 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

236 
in (Predicate.bind P (%a. fst (f a s1)), s2))" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

237 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

238 
definition union :: "'a randompred \<Rightarrow> 'a randompred \<Rightarrow> 'a randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

239 
where 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

240 
"union R1 R2 = (\<lambda>s. let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

241 
(P1, s') = R1 s; (P2, s'') = R2 s' 
44845  242 
in (sup_class.sup P1 P2, s''))" 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

243 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

244 
definition if_randompred :: "bool \<Rightarrow> unit randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

245 
where 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

246 
"if_randompred b = (if b then single () else empty)" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

247 

36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
35880
diff
changeset

248 
definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred" 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
35880
diff
changeset

249 
where 
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset

250 
"iterate_upto f n m = Pair (Predicate.iterate_upto f n m)" 
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
35880
diff
changeset

251 

33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

252 
definition not_randompred :: "unit randompred \<Rightarrow> unit randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

253 
where 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

254 
"not_randompred P = (\<lambda>s. let 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

255 
(P', s') = P s 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

256 
in if Predicate.eval P' () then (Orderings.bot, s') else (Predicate.single (), s'))" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

257 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

258 
definition Random :: "(Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> 'a randompred" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

259 
where "Random g = scomp g (Pair o (Predicate.single o fst))" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

260 

5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

261 
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

262 
where "map f P = bind P (single o f)" 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
32657
diff
changeset

263 

45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset

264 
hide_fact 
46976
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

265 
random_bool_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

266 
random_itself_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

267 
random_char_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

268 
random_literal_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

269 
random_nat_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

270 
random_int_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

271 
random_fun_lift_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

272 
random_fun_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

273 
collapse_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

274 
beyond_def 
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46975
diff
changeset

275 
beyond_zero 
45801
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset

276 
random_aux_rec 
5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset

277 

5616fbda86e6
hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn
parents:
45733
diff
changeset

278 
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

279 

46975  280 
hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def 
281 
if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36049
diff
changeset

282 
hide_type (open) randompred 
46975  283 
hide_const (open) iter' iter empty single bind union if_randompred 
284 
iterate_upto not_randompred Random map 

31267  285 

31179  286 
end 