author  haftmann 
Mon, 22 Sep 2008 13:56:04 +0200  
changeset 28315  d3cf88fe77bc 
parent 28309  c24bc53c815c 
child 28335  25326092cf9a 
permissions  rwrr 
26265  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple counterexample generator *} 

6 

7 
theory Quickcheck 

28228  8 
imports Random Code_Eval 
26265  9 
begin 
10 

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

12 

26325  13 
class random = rtype + 
14 
fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" 

26265  15 

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

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

26325  18 
instantiation itself :: ("{type, rtype}") random 
26265  19 
begin 
20 

21 
definition 

28228  22 
"random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))" 
26265  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 

28145  30 
definition 
31 
collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 

32 
"collapse f = (do g \<leftarrow> f; g done)" 

33 

34 
ML {* 

35 
structure StateMonad = 

36 
struct 

37 

38 
fun liftT T sT = sT > HOLogic.mk_prodT (T, sT); 

39 
fun liftT' sT = sT > sT; 

40 

41 
fun return T sT x = Const (@{const_name return}, T > liftT T sT) $ x; 

42 

43 
fun scomp T1 T2 sT f g = Const (@{const_name scomp}, 

44 
liftT T1 sT > (T1 > liftT T2 sT) > liftT T2 sT) $ f $ g; 

45 

46 
end; 

47 
*} 

48 

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

49 
lemma random'_if: 
26325  50 
fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed" 
26265  51 
assumes "random' 0 j = undefined" 
52 
and "\<And>i. random' (Suc_index i) j = rhs2 i" 

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

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

55 

56 
setup {* 

57 
let 

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

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

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

60 
(@{const_name collapse}, [@{typ seed}, ty]); 
26325  61 
fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); 
62 
fun mk_split thy ty ty' = Sign.mk_const thy 

63 
(@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]); 

26589  64 
fun mk_scomp_split thy ty ty' t t' = 
65 
StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t 

26325  66 
(mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))) 
67 
fun mk_cons thy this_ty (c, args) = 

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

69 
val tys = map (fst o fst) args; 
26325  70 
val c_ty = tys > this_ty; 
71 
val c = Const (c, tys > this_ty); 

72 
val t_indices = map (curry ( op * ) 2) (length tys  1 downto 0); 

73 
val c_indices = map (curry ( op + ) 1) t_indices; 

74 
val c_t = list_comb (c, map Bound c_indices); 

75 
val t_t = Abs ("", @{typ unit}, Eval.mk_term Free RType.rtype 

76 
(list_comb (c, map (fn k => Bound (k + 1)) t_indices)) 

77 
> map_aterms (fn t as Bound _ => t $ @{term "()"}  t => t)); 

78 
val return = StateMonad.return (term_ty this_ty) @{typ seed} 

79 
(HOLogic.mk_prod (c_t, t_t)); 

80 
val t = fold_rev (fn ((ty, _), random) => 

26589  81 
mk_scomp_split thy ty this_ty random) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

83 
val is_rec = exists (snd o fst) args; 
28145  84 
in (is_rec, t) end; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

86 
 mk_conss thy ty [(_, t)] = SOME t 
26325  87 
 mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ 
88 
(Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ 

89 
HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts))); 

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

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

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

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

93 
in case mk_conss thy ty ts_rec 
26325  94 
of SOME t_rec => mk_collapse thy (term_ty ty) $ 
95 
(Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ 

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

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

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

98 
end; 
26325  99 
fun mk_random_eqs thy vs tycos = 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

101 
val this_ty = Type (hd tycos, map TFree vs); 
26325  102 
val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

105 
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

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

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

108 
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

109 
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

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

111 
("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

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

113 
{ atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos 
26325  114 
> (map o apsnd o map) (mk_cons thy this_ty) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

117 
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

118 
(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

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

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

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

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

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

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

126 
(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

127 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; 
26325  128 
val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

130 
(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

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

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

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

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

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

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

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

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

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

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

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

142 
lthy 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27683
diff
changeset

143 
> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

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

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

149 
> PrimrecPackage.add_primrec 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28054
diff
changeset

150 
[(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] 
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
28054
diff
changeset

151 
(map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs') 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

153 
> `(fn lthy => Syntax.check_term lthy eq) 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

154 
> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq))) 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

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

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

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

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

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

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

163 
handle REC msg => (warning msg; thy); 
26265  164 
in DatatypePackage.interpretation add_random_inst end 
165 
*} 

166 

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

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

168 

26265  169 
instantiation int :: random 
170 
begin 

171 

172 
definition 

173 
"random n = (do 

26325  174 
(b, _) \<leftarrow> random n; 
175 
(m, t) \<leftarrow> random n; 

28228  176 
return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ())) 
177 
else ( int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int)) 

178 
(Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ())))) 

26265  179 
done)" 
180 

181 
instance .. 

182 

183 
end 

184 

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

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

186 

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

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

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

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

190 

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

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

192 

26325  193 
fun random_fun (T1 : typ) (T2 : typ) (eq : 'a > 'a > bool) (term_of : 'a > term) 
194 
(random : Random_Engine.seed > ('b * (unit > term)) * Random_Engine.seed) 

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

195 
(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

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

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

198 
val (seed', seed'') = random_split seed; 
26325  199 
val state = ref (seed', [], Const (@{const_name arbitrary}, T1 > T2)); 
200 
val fun_upd = Const (@{const_name fun_upd}, 

201 
(T1 > T2) > T1 > T2 > T1 > T2); 

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

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

203 
let 
26325  204 
val (seed, fun_map, f_t) = ! state; 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

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

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

207 
 NONE => let 
26325  208 
val t1 = term_of x; 
209 
val ((y, t2), seed') = random seed; 

210 
val fun_map' = (x, y) :: fun_map; 

211 
val f_t' = fun_upd $ f_t $ t1 $ t2 (); 

212 
val _ = state := (seed', fun_map', f_t'); 

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

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

214 
end; 
26325  215 
fun term_fun' () = #3 (! state); 
216 
in ((random_fun', term_fun'), seed'') end; 

26267
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 

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

221 
axiomatization 
26325  222 
random_fun_aux :: "rtype \<Rightarrow> rtype \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term) 
223 
\<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) 

224 
\<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" 

26267
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 
code_const random_fun_aux (SML "Random'_Engine.random'_fun") 
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

227 

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

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

230 

26325  231 
definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where 
28228  232 
"random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed" 
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26265
diff
changeset

233 

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

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

235 

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

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

237 

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

238 
code_reserved SML Random_Engine 
26265  239 

240 

241 
subsection {* Quickcheck generator *} 

242 

243 
ML {* 

244 
structure Quickcheck = 

245 
struct 

246 

28309  247 
open Quickcheck; 
248 

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

26325  251 
fun mk_generator_expr thy prop tys = 
26265  252 
let 
26325  253 
val bound_max = length tys  1; 
254 
val bounds = map_index (fn (i, ty) => 

255 
(2 * (bound_max  i) + 1, 2 * (bound_max  i), 2 * i, ty)) tys; 

256 
val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); 

257 
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); 

26265  258 
val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} 
26325  259 
$ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms); 
26265  260 
val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"}; 
26325  261 
fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"}); 
262 
fun mk_split ty = Sign.mk_const thy 

263 
(@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]); 

26589  264 
fun mk_scomp_split ty t t' = 
265 
StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*) 

26325  266 
(mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t'))); 
26589  267 
fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty 
26325  268 
(Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i) 
26265  269 
val t = fold_rev mk_bindclause bounds (return $ check); 
270 
in Abs ("n", @{typ index}, t) end; 

271 

28309  272 
fun compile_generator_expr thy t = 
26265  273 
let 
28309  274 
val tys = (map snd o fst o strip_abs) t; 
275 
val t' = mk_generator_expr thy t tys; 

276 
val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' []; 

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

26265  278 

279 
end 

280 
*} 

281 

28309  282 
setup {* 
283 
Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of) 

284 
*} 

285 

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

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

287 

28315  288 
theorem "map g (map f xs) = map (g o f) xs" 
289 
quickcheck [generator = code] 

290 
by (induct xs) simp_all 

26325  291 

28315  292 
theorem "map g (map f xs) = map (f o g) xs" 
293 
quickcheck [generator = code] 

294 
oops 

295 

296 
theorem "rev (xs @ ys) = rev ys @ rev xs" 

297 
quickcheck [generator = code] 

298 
by simp 

26265  299 

28315  300 
theorem "rev (xs @ ys) = rev xs @ rev ys" 
301 
quickcheck [generator = code] 

302 
oops 

303 

304 
theorem "rev (rev xs) = xs" 

305 
quickcheck [generator = code] 

306 
by simp 

307 

308 
theorem "rev xs = xs" 

309 
quickcheck [generator = code] 

310 
oops 

311 

312 
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where 

313 
"app [] x = x" 

314 
 "app (f # fs) x = app fs (f x)" 

26265  315 

28315  316 
lemma "app (fs @ gs) x = app gs (app fs x)" 
317 
quickcheck [generator = code] 

318 
by (induct fs arbitrary: x) simp_all 

319 

320 
lemma "app (fs @ gs) x = app fs (app gs x)" 

321 
quickcheck [generator = code] 

322 
oops 

323 

324 
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where 

325 
"occurs a [] = 0" 

326 
 "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" 

26265  327 

28315  328 
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
329 
"del1 a [] = []" 

330 
 "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" 

331 

332 
lemma "Suc (occurs a (del1 a xs)) = occurs a xs" 

333 
 {* Wrong. Precondition needed.*} 

334 
quickcheck [generator = code] 

335 
oops 

26265  336 

28315  337 
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 
338 
quickcheck [generator = code] 

339 
 {* Also wrong.*} 

340 
oops 

341 

342 
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs" 

343 
quickcheck [generator = code] 

344 
by (induct xs) auto 

26265  345 

28315  346 
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
347 
"replace a b [] = []" 

348 
 "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 

349 
else (x#(replace a b xs)))" 

350 

351 
lemma "occurs a xs = occurs b (replace a b xs)" 

352 
quickcheck [generator = code] 

353 
 {* Wrong. Precondition needed.*} 

354 
oops 

355 

356 
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)" 

357 
quickcheck [generator = code] 

358 
by (induct xs) simp_all 

359 

360 

361 
subsection {* Trees *} 

362 

363 
datatype 'a tree = Twig  Leaf 'a  Branch "'a tree" "'a tree" 

364 

365 
primrec leaves :: "'a tree \<Rightarrow> 'a list" where 

366 
"leaves Twig = []" 

367 
 "leaves (Leaf a) = [a]" 

368 
 "leaves (Branch l r) = (leaves l) @ (leaves r)" 

369 

370 
primrec plant :: "'a list \<Rightarrow> 'a tree" where 

371 
"plant [] = Twig " 

372 
 "plant (x#xs) = Branch (Leaf x) (plant xs)" 

26265  373 

28315  374 
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where 
375 
"mirror (Twig) = Twig " 

376 
 "mirror (Leaf a) = Leaf a " 

377 
 "mirror (Branch l r) = Branch (mirror r) (mirror l)" 

26265  378 

28315  379 
theorem "plant (rev (leaves xt)) = mirror xt" 
380 
quickcheck [generator = code] 

381 
{* Wrong! *} 

382 
oops 

383 

384 
theorem "plant (leaves xt @ leaves yt) = Branch xt yt" 

385 
quickcheck [generator = code] 

386 
{* Wrong! *} 

387 
oops 

388 

389 
datatype 'a ntree = Tip "'a"  Node "'a" "'a ntree" "'a ntree" 

26265  390 

28315  391 
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where 
392 
"inOrder (Tip a)= [a]" 

393 
 "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" 

394 

395 
primrec root :: "'a ntree \<Rightarrow> 'a" where 

396 
"root (Tip a) = a" 

397 
 "root (Node f x y) = f" 

26265  398 

28315  399 
theorem "hd (inOrder xt) = root xt" 
400 
quickcheck [generator = code] 

401 
{* Wrong! *} 

402 
oops 

26325  403 

28315  404 
lemma "int (f k) = k" 
405 
quickcheck [generator = code] 

406 
oops 

26325  407 

26265  408 
end 