author  haftmann 
Fri, 14 Mar 2008 08:52:52 +0100  
changeset 26267  ba710daf77a7 
parent 26265  4b63b9e9b10d 
child 26275  014d93dc2199 
permissions  rwrr 
26265  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple counterexample generator *} 

6 

7 
theory Quickcheck 

8 
imports Random Eval 

9 
begin 

10 

11 
subsection {* The @{text random} class *} 

12 

13 
class random = type + 

14 
fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" 

15 

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

16 
text {* Type @{typ "'a itself"} *} 
26265  17 

18 
instantiation itself :: (type) random 

19 
begin 

20 

21 
definition 

22 
"random _ = return TYPE('a)" 

23 

24 
instance .. 

25 

26 
end 

27 

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

28 
text {* Datatypes *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

29 

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

30 
lemma random'_if: 
26265  31 
fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" 
32 
assumes "random' 0 j = undefined" 

33 
and "\<And>i. random' (Suc_index i) j = rhs2 i" 

34 
shows "random' i j s = (if i = 0 then undefined else rhs2 (i  1) s)" 

35 
by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun) 

36 

37 
setup {* 

38 
let 

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

39 
exception REC of string; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

40 
fun mk_collapse thy ty = Sign.mk_const thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

41 
(@{const_name collapse}, [@{typ seed}, ty]); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

42 
fun mk_cons this_ty (c, args) = 
26265  43 
let 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

44 
val tys = map (fst o fst) args; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

45 
val return = StateMonad.return this_ty @{typ seed} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

46 
(list_comb (Const (c, tys > this_ty), 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

47 
map Bound (length tys  1 downto 0))); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

48 
val t = fold_rev (fn ((ty, _), random) => fn t => 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

49 
StateMonad.mbind ty this_ty @{typ seed} random (Abs ("", ty, t))) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

50 
args return; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

51 
val is_rec = exists (snd o fst) args; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

52 
in (is_rec, StateMonad.run this_ty @{typ seed} t) end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

53 
fun mk_conss thy ty [] = NONE 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

54 
 mk_conss thy ty [(_, t)] = SOME t 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

55 
 mk_conss thy ty ts = SOME (mk_collapse thy ty $ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

56 
(Sign.mk_const thy (@{const_name select}, [StateMonad.liftT ty @{typ seed}]) $ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

57 
HOLogic.mk_list (StateMonad.liftT ty @{typ seed}) (map snd ts))); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

58 
fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

60 
val SOME t_atom = mk_conss thy ty ts_atom; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

61 
in case mk_conss thy ty ts_rec 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

62 
of SOME t_rec => mk_collapse thy ty $ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

63 
(Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT ty @{typ seed}]) $ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

64 
@{term "i\<Colon>index"} $ t_rec $ t_atom) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

65 
 NONE => t_atom 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

66 
end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

67 
fun mk_random_eqs thy tycos = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

69 
val (raw_vs, _) = DatatypePackage.the_datatype_spec thy (hd tycos); 
26265  70 
val vs = (map o apsnd) 
71 
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; 

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

72 
val this_ty = Type (hd tycos, map TFree vs); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

73 
val this_ty' = StateMonad.liftT this_ty @{typ seed}; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

74 
val random_name = NameSpace.base @{const_name random}; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

75 
val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

76 
fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

77 
val random' = Free (random'_name, 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

78 
@{typ index} > @{typ index} > this_ty'); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

79 
fun atom ty = ((ty, false), random ty $ @{term "j\<Colon>index"}); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

80 
fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

81 
fun rtyp tyco tys = raise REC 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

82 
("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

83 
val rhss = DatatypePackage.construction_interpretation thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

84 
{ atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

85 
> (map o apsnd o map) (mk_cons this_ty) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

86 
> (map o apsnd) (List.partition fst) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

87 
> map (mk_clauses thy this_ty) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

88 
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

89 
(random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, this_ty')), 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

90 
(random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

91 
]))) rhss; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

92 
in eqss end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

93 
fun random_inst [tyco] thy = 
26265  94 
let 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

95 
val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

96 
val vs = (map o apsnd) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

97 
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

98 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

99 
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy) tyco; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

100 
val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

101 
(Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"}, 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

102 
random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"}) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

103 
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

104 
(fn thm => Context.mapping (Code.del_func thm) I)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

105 
fun add_code simps lthy = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

107 
val thy = ProofContext.theory_of lthy; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

108 
val thm = @{thm random'_if} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

109 
> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

110 
> (fn thm => thm OF simps) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

111 
> singleton (ProofContext.export lthy (ProofContext.init thy)) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

114 
> LocalTheory.theory (PureThy.note Thm.internalK (fst (dest_Free random') ^ "_code", thm) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

115 
#> Code.add_func) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

116 
end; 
26265  117 
in 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

119 
> TheoryTarget.instantiation ([tyco], vs, @{sort random}) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

120 
> PrimrecPackage.add_primrec 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

121 
[(fst (dest_Free random'), SOME (snd (dest_Free random')), NoSyn)] 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

122 
(map (fn eq => (("", [del_func]), eq)) eqs') 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

123 
> add_code 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

124 
> `(fn lthy => Syntax.check_term lthy eq) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

125 
> (fn eq => Specification.definition (NONE, (("", []), eq))) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

126 
> snd 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

127 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

128 
> LocalTheory.exit 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

129 
> ProofContext.theory_of 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

131 
 random_inst tycos thy = raise REC 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

132 
("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

133 
fun add_random_inst tycos thy = random_inst tycos thy 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

134 
handle REC msg => (warning msg; thy); 
26265  135 
in DatatypePackage.interpretation add_random_inst end 
136 
*} 

137 

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

138 
text {* Type @{typ int} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

139 

26265  140 
instantiation int :: random 
141 
begin 

142 

143 
definition 

144 
"random n = (do 

145 
(b, m) \<leftarrow> random n; 

146 
return (if b then int m else  int m) 

147 
done)" 

148 

149 
instance .. 

150 

151 
end 

152 

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

153 
text {* Type @{typ "'a set"} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

154 

26265  155 
instantiation set :: (random) random 
156 
begin 

157 

158 
primrec random_set' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a set \<times> seed" where 

159 
"random_set' 0 j = undefined" 

160 
 "random_set' (Suc_index i) j = collapse (select_default i 

161 
(do x \<leftarrow> random i; xs \<leftarrow> random_set' i j; return (insert x xs) done) 

162 
(return {}))" 

163 

164 
lemma random_set'_code [code func]: 

165 
"random_set' i j s = (if i = 0 then undefined else collapse (select_default (i  1) 

166 
(do x \<leftarrow> random (i  1); xs \<leftarrow> random_set' (i  1) j; return (insert x xs) done) 

167 
(return {})) s)" 

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

168 
by (rule random'_if random_set'.simps)+ 
26265  169 

170 
definition 

171 
"random i = random_set' i i" 

172 

173 
instance .. 

174 

175 
end 

176 

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

177 
text {* Type @{typ "'a \<Rightarrow> 'b"} *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

178 

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

179 
ML {* 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

180 
structure Random_Engine = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

182 

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

183 
open Random_Engine; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

184 

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

185 
fun random_fun (eq : 'a > 'a > bool) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

186 
(random : Random_Engine.seed > 'b * Random_Engine.seed) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

187 
(random_split : Random_Engine.seed > Random_Engine.seed * Random_Engine.seed) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

188 
(seed : Random_Engine.seed) = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

190 
val (seed', seed'') = random_split seed; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

191 
val state = ref (seed', []); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

192 
fun random_fun' x = 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

194 
val (seed, fun_map) = ! state; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

195 
in case AList.lookup (uncurry eq) fun_map x 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

196 
of SOME y => y 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

197 
 NONE => let 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

198 
val (y, seed') = random seed; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

199 
val _ = state := (seed', (x, y) :: fun_map); 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

200 
in y end 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

201 
end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

202 
in (random_fun', seed'') end; 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

203 

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

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

205 
*} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

206 

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

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

208 
random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

209 
\<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

210 

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

211 
code_const random_fun_aux (SML "Random'_Engine.random'_fun") 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

212 

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

213 
instantiation "fun" :: (term_of, term_of) term_of 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

215 

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

216 
instance .. 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

217 

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

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

219 

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

220 
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

221 
(SML "(fn '_ => Const (\"arbitrary\", dummyT))") 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

222 

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

223 
instantiation "fun" :: (eq, "{type, random}") random 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

225 

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

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

227 
"random n = random_fun_aux (op =) (random n) split_seed" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

228 

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

229 
instance .. 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

230 

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

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

232 

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

233 
code_reserved SML Random_Engine 
26265  234 

235 

236 
subsection {* Quickcheck generator *} 

237 

238 
ML {* 

239 
structure Quickcheck = 

240 
struct 

241 

242 
val eval_ref : (unit > int > int * int > term list option * (int * int)) option ref = ref NONE; 

243 

244 
fun mk_generator_expr prop tys = 

245 
let 

246 
val bounds = map_index (fn (i, ty) => (i, ty)) tys; 

247 
val result = list_comb (prop, map (fn (i, _) => Bound (length tys  i  1)) bounds); 

248 
val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty > @{typ term}) $ Bound (length tys  i  1)) bounds; 

249 
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} 

250 
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms); 

251 
val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"}; 

252 
fun mk_bindtyp ty = @{typ seed} > HOLogic.mk_prodT (ty, @{typ seed}); 

253 
fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty 

254 
> (ty > mk_bindtyp @{typ "term list option"}) > mk_bindtyp @{typ "term list option"}) 

255 
$ (Const (@{const_name random}, @{typ index} > mk_bindtyp ty) 

256 
$ Bound i) $ Abs ("a", ty, t); 

257 
val t = fold_rev mk_bindclause bounds (return $ check); 

258 
in Abs ("n", @{typ index}, t) end; 

259 

260 
fun compile_generator_expr thy prop tys = 

261 
let 

262 
val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy 

263 
(mk_generator_expr prop tys) []; 

264 
in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; 

265 

266 
fun VALUE prop tys thy = 

267 
let 

268 
val t = mk_generator_expr prop tys; 

269 
val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t) 

270 
in 

271 
thy 

272 
> TheoryTarget.init NONE 

273 
> Specification.definition (NONE, (("", []), eq)) 

274 
> snd 

275 
> LocalTheory.exit 

276 
> ProofContext.theory_of 

277 
end; 

278 

279 
end 

280 
*} 

281 

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

282 

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

283 
subsection {* Examples *} 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

284 

26265  285 
(*setup {* Quickcheck.VALUE @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *} 
286 
export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML" 

287 
use "~~/../../gen_code/quickcheck.ML" 

288 
ML {* Random_Engine.run (QuickcheckExample.range 1) *}*) 

289 

290 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

291 
@{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *} 

292 

293 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

294 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

295 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

296 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

297 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

298 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

299 
ML {* f 25 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

300 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

301 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

302 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

303 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

304 

305 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

306 
@{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *} 

307 

308 
(*definition "FOO = (True, Suc 0)" 

309 

310 
code_module (test) QuickcheckExample 

311 
file "~~/../../gen_code/quickcheck'.ML" 

312 
contains FOO*) 

313 

314 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

315 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

316 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

317 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

318 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

319 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

320 
ML {* f 25 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

321 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

322 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

323 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

324 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

325 
ML {* f 3 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

326 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

327 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

328 

329 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

330 
@{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"} 

331 
[@{typ "int list"}, @{typ "int list"}] *} 

332 

333 
ML {* f 15 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

334 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

335 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

336 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

337 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

338 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

339 
ML {* f 25 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

340 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

341 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

342 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

343 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

344 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

345 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

346 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

347 
ML {* f 8 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

348 
ML {* f 8 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

349 
ML {* f 8 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

350 
ML {* f 88 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

351 

352 

353 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

354 
@{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *} 

355 

356 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

357 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

358 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

359 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

360 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

361 
ML {* f 20 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

362 

363 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

364 
@{term "\<lambda>(A \<Colon> nat set) B. card (A \<union> B) = card A + card B"} [@{typ "nat set"}, @{typ "nat set"}] *} 

365 

366 
ML {* f 1 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

367 
ML {* f 2 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

368 
ML {* f 3 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

369 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

370 
ML {* f 5 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

371 
ML {* f 6 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

372 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

373 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

374 

375 
ML {* val f = Quickcheck.compile_generator_expr @{theory} 

376 
@{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *} 

377 

378 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

379 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

380 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

381 
ML {* f 4 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

382 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

383 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

384 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

385 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

386 
ML {* f 10 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

387 
ML {* f 8 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

388 
ML {* f 8 > (Option.map o map) (Sign.string_of_term @{theory}) *} 

389 

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

390 
definition "map2 f xs ys = map (split f) (zip xs ys)" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

391 

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

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

393 
assumes "\<And>x. f x x = x" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

394 
shows "map2 f xs xs = xs" 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

395 
by (induct xs) (simp_all add: map2_def assms) 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

396 

26265  397 
end 