author  bulwahn 
Wed, 19 Oct 2011 08:37:24 +0200  
changeset 45178  fe9993491317 
parent 45159  3f1d1ce024cb 
child 45718  8979b2463fc8 
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 
05abcee548a1
adaptions in generators using the common functions
bulwahn
parents:
41923
diff
changeset

8 
"Tools/Quickcheck/quickcheck_common.ML" 
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 

15 

26265  16 
subsection {* The @{text random} class *} 
17 

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

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

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

21 

31260  22 
subsection {* Fundamental and numeric types*} 
31179  23 

24 
instantiation bool :: random 

25 
begin 

26 

27 
definition 

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

31 
instance .. 

32 

33 
end 

34 

35 
instantiation itself :: (typerep) random 

36 
begin 

37 

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

38 
definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 
32657  39 
"random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))" 
31179  40 

41 
instance .. 

42 

43 
end 

44 

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

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

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

47 

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

48 
definition 
37751  49 
"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

50 

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

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

54 

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

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

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

57 

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

58 
definition 
32657  59 
"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

60 

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

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

62 

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

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

64 

31179  65 
instantiation nat :: random 
66 
begin 

67 

32657  68 
definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where 
37751  69 
"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

70 
let n = Code_Numeral.nat_of k 
32657  71 
in (n, \<lambda>_. Code_Evaluation.term_of n)))" 
31194  72 

73 
instance .. 

74 

75 
end 

76 

77 
instantiation int :: random 

78 
begin 

79 

80 
definition 

37751  81 
"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

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

85 
instance .. 

86 

30945  87 
end 
31179  88 

31260  89 

90 
subsection {* Complex generators *} 

91 

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

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

93 

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

94 
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

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

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

97 

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

32657  100 
"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

101 

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

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

103 
begin 
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 
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where 
31622  106 
"random i = random_fun_lift (random i)" 
31603
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 
instance .. 
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 
end 
fa30cd74d7d6
revised interpretation combinator for datatype constructions
haftmann
parents:
31483
diff
changeset

111 

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

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

113 

31260  114 
definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 
37751  115 
"collapse f = (f \<circ>\<rightarrow> id)" 
31223
87bde6b5f793
readded corrected version of type copy quickcheck generator
haftmann
parents:
31211
diff
changeset

116 

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

119 

31267  120 
lemma beyond_zero: 
121 
"beyond k 0 = 0" 

122 
by (simp add: beyond_def) 

123 

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

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

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

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

127 
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

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

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

130 

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

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

133 

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

134 

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

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

136 

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

137 
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

138 
 {* 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

139 
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

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

141 

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

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

143 

37751  144 
no_notation fcomp (infixl "\<circ>>" 60) 
145 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

146 

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

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

148 

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

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

150 
"'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred" 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

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

152 
"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

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

154 
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

155 

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

156 
definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred" 
2623b23e41fc
a new simpler random compilation for the predicate compiler
bulwahn
parents:
35028
diff
changeset

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

158 
"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

159 

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

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

161 
"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

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

163 
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

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

165 

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

166 
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

167 

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

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

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

170 

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

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

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

173 

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

174 
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

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

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

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

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

179 
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

180 

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

181 
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

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

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

184 
(P1, s') = R1 s; (P2, s'') = R2 s' 
44845  185 
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

186 

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

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

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

189 
"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

190 

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

191 
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

192 
where 
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

193 
"iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)" 
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

194 

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

195 
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

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

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

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

199 
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

200 

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

201 
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

202 
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

203 

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

204 
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

205 
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

206 

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

207 
hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def 
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

208 
hide_type (open) randompred 
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

209 
hide_const (open) random collapse beyond random_fun_aux random_fun_lift 
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

210 
iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map 
31267  211 

31179  212 
end 