22528

1 
(* ID: $Id$


2 
Author: Florian Haftmann, TU Muenchen


3 
*)


4 

26038

5 
header {* A simple term generator *}

22528

6 


7 
theory Random

26038

8 
imports State_Monad Code_Index List Eval

22528

9 
begin


10 

26038

11 
subsection {* The random engine *}


12 


13 
types seed = "index \<times> index"

22528

14 

26038

15 
definition


16 
"next" :: "seed \<Rightarrow> index \<times> seed"


17 
where


18 
"next s = (let


19 
(v, w) = s;


20 
k = v div 53668;


21 
v' = 40014 * (v  k * 53668)  k * 12211;


22 
v'' = (if v' < 0 then v' + 2147483563 else v');


23 
l = w div 52774;


24 
w' = 40692 * (w  l * 52774)  l * 3791;


25 
w'' = (if w' < 0 then w' + 2147483399 else w');


26 
z = v''  w'';


27 
z' = (if z < 1 then z + 2147483562 else z)


28 
in (z', (v'', w'')))"

22528

29 


30 
definition

26038

31 
split_seed :: "seed \<Rightarrow> seed \<times> seed"


32 
where


33 
"split_seed s = (let


34 
(v, w) = s;


35 
(v', w') = snd (next s);


36 
v'' = (if v = 2147483562 then 1 else v + 1);


37 
s'' = (v'', w');


38 
w'' = (if w = 2147483398 then 1 else w + 1);


39 
s''' = (v', w'')


40 
in (s'', s'''))"


41 


42 
text {* Base selectors *}


43 


44 
primrec

26142

45 
pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a"

26038

46 
where


47 
"pick (x#xs) n = (if n < fst x then snd x else pick xs (n  fst x))"

22528

48 

26038

49 
function


50 
iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"


51 
where


52 
"iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"


53 
by pat_completeness auto


54 
termination


55 
by (relation "measure (nat_of_index o snd)")


56 
(auto simp add: index)

22528

57 

26038

58 
function


59 
range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"


60 
where


61 
"range_aux k l s = (if k = 0 then (l, s) else


62 
let (v, s') = next s


63 
in range_aux (k  1) (v + l * 2147483561) s')"


64 
by pat_completeness auto


65 
termination


66 
by (relation "measure (nat_of_index o fst)")


67 
(auto simp add: index)

22528

68 


69 
definition

26038

70 
range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"


71 
where


72 
"range k s = (let


73 
b = 2147483561;


74 
n = iLogBase b k;


75 
(v, s') = range_aux n 1 s


76 
in (v mod k, s'))"


77 

22528

78 
definition

26038

79 
select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"


80 
where


81 
[simp]: "select xs s = (let


82 
(k, s') = range (index_of_nat (length xs)) s


83 
in (nth xs (nat_of_index k), s'))"

22528

84 

26038

85 
definition

26142

86 
select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"

26038

87 
where


88 
[simp]: "select_weight xs s = (let

26142

89 
(k, s') = range (foldr (op + \<circ> fst) xs 0) s


90 
in (pick xs k, s'))"

26038

91 


92 
(*lemma

22528

93 
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"


94 
proof (induct xs)

26038

95 
case Nil show ?case apply (auto simp add: Let_def split_def)

22528

96 
next


97 
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"


98 
proof 


99 
fix xs


100 
fix y


101 
show "map fst (map (Pair y) xs) = replicate (length xs) y"


102 
by (induct xs) simp_all


103 
qed


104 
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"


105 
proof 


106 
fix xs


107 
fix n


108 
assume "n < length xs"


109 
then show "pick (map (Pair 1) xs) n = nth xs n"


110 
proof (induct xs arbitrary: n)


111 
case Nil then show ?case by simp


112 
next


113 
case (Cons x xs) show ?case


114 
proof (cases n)


115 
case 0 then show ?thesis by simp


116 
next


117 
case (Suc _)


118 
from Cons have "n < length (x # xs)" by auto


119 
then have "n < Suc (length xs)" by simp


120 
with Suc have "n  1 < Suc (length xs)  1" by auto


121 
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n  1) = xs ! (n  1)" by auto


122 
with Suc show ?thesis by auto


123 
qed


124 
qed


125 
qed


126 
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"


127 
proof 


128 
have replicate_append:


129 
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"


130 
by (simp add: replicate_app_Cons_same)


131 
fix xs


132 
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"


133 
unfolding map_fst_Pair proof (induct xs)


134 
case Nil show ?case by simp


135 
next


136 
case (Cons x xs) then show ?case unfolding replicate_append by simp


137 
qed


138 
qed


139 
have pick_nth_random:


140 
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"


141 
proof 


142 
fix s


143 
fix x


144 
fix xs


145 
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp


146 
from pick_nth [OF bound] show


147 
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .


148 
qed


149 
have pick_nth_random_do:


150 
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =


151 
(do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"


152 
unfolding monad_collapse split_def unfolding pick_nth_random ..


153 
case (Cons x xs) then show ?case


154 
unfolding select_weight_def sum_length pick_nth_random_do


155 
by simp

26038

156 
qed*)

22528

157 

26038

158 
text {* The @{text ML} interface *}

22528

159 


160 
ML {*

26038

161 
structure Quickcheck =

22528

162 
struct


163 

26038

164 
type seed = int * int;

22528

165 


166 
local

26038

167 


168 
val seed = ref (0, 0);


169 


170 
fun init () =


171 
let


172 
val now = Time.toNanoseconds (Time.now ());


173 
val (q, s1) = IntInf.divMod (now, 2147483562);


174 
val s2 = q mod 2147483398;


175 
in seed := (s1 + 1, s2 + 1) end;


176 

22528

177 
in

26038

178 


179 
val seed = seed; (* FIXME *)


180 


181 
fun run f =


182 
let


183 
val (x, seed') = f (!seed);


184 
val _ = seed := seed'


185 
val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then


186 
(warning "broken random seed"; init ())


187 
else ()


188 
in x end;


189 

22528

190 
end;


191 


192 
end;


193 
*}


194 

26038

195 


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


197 

26042

198 
class random =


199 
fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed"

26038

200 

26261

201 
instantiation itself :: (type) random

26038

202 
begin


203 


204 
definition

26261

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

26038

206 


207 
instance ..


208 


209 
end


210 

26261

211 
lemma random_aux_if:


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


213 
assumes "random' 0 j = undefined"


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


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


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

26038

217 

26261

218 
setup {*


219 
let


220 
fun random_inst tyco thy =


221 
let


222 
val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;


223 
val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;


224 
val vs = (map o apsnd)


225 
(curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;


226 
val ty = Type (tyco, map TFree vs);


227 
val typ_of = DatatypeAux.typ_of_dtyp descr vs;


228 
val SOME (_, _, constrs) = AList.lookup (op =) descr index;


229 
val randomN = NameSpace.base @{const_name random};


230 
val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";


231 
fun lift_ty ty = StateMonad.liftT ty @{typ seed};


232 
val ty_aux = @{typ index} > @{typ index} > lift_ty ty;


233 
fun random ty =


234 
Const (@{const_name random}, @{typ index} > lift_ty ty);


235 
val random_aux = Free (random_aux_name, ty_aux);


236 
fun add_cons_arg dty (is_rec, t) =


237 
let


238 
val ty' = typ_of dty;


239 
val random' = if can DatatypeAux.dest_DtRec dty


240 
then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}


241 
else random ty' $ @{term "j\<Colon>index"}


242 
val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;


243 
val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))


244 
in (is_rec', t') end;


245 
fun mk_cons_t (c, dtys) =


246 
let


247 
val ty' = map typ_of dtys > ty;


248 
val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),


249 
map Bound (length dtys  1 downto 0)));


250 
val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);


251 
in (is_rec, StateMonad.run ty @{typ seed} t') end;


252 
fun check_empty [] = NONE


253 
 check_empty xs = SOME xs;


254 
fun bundle_cons_ts cons_ts =


255 
let


256 
val ts = map snd cons_ts;


257 
val t = HOLogic.mk_list (lift_ty ty) ts;


258 
val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) > lift_ty (lift_ty ty)) $ t;


259 
val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) > lift_ty ty) $ t';


260 
in t'' end;


261 
fun bundle_conss (some_rec_t, nonrec_t) =


262 
let


263 
val rec' = case some_rec_t


264 
of SOME rec_t => SOME (HOLogic.mk_prod (@{term "i\<Colon>index"}, rec_t))


265 
 NONE => NONE;


266 
val nonrec' = HOLogic.mk_prod (@{term "1\<Colon>index"}, nonrec_t);


267 
val i_ty = HOLogic.mk_prodT (@{typ index}, lift_ty ty);


268 
val t = HOLogic.mk_list i_ty (the_list rec' @ single nonrec');


269 
val t' = Const (@{const_name select_weight}, HOLogic.listT i_ty > lift_ty (lift_ty ty)) $ t;


270 
val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) > lift_ty ty) $ t';


271 
in t'' end;


272 
val random_rhs = constrs


273 
> map mk_cons_t


274 
> List.partition fst


275 
> apfst (Option.map bundle_cons_ts o check_empty)


276 
> apsnd bundle_cons_ts


277 
> bundle_conss;


278 
val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)


279 
(random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))


280 
val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)


281 
(random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);


282 
val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},


283 
@{typ index} > lift_ty ty) $ @{term "i\<Colon>index"},


284 
random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});


285 
val del_func = Attrib.internal (fn _ => Thm.declaration_attribute


286 
(fn thm => Context.mapping (Code.del_func thm) I));


287 
fun add_code simps lthy =


288 
let


289 
val thy = ProofContext.theory_of lthy;


290 
val thm = @{thm random_aux_if}


291 
> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]


292 
> (fn thm => thm OF simps)


293 
> singleton (ProofContext.export lthy (ProofContext.init thy))


294 
in


295 
lthy


296 
> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)


297 
#> Code.add_func)


298 
end;


299 
in


300 
thy


301 
> TheoryTarget.instantiation ([tyco], vs, @{sort random})


302 
> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]


303 
[(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]


304 
> add_code


305 
> `(fn lthy => Syntax.check_term lthy random_eq)


306 
> (fn eq => Specification.definition (NONE, (("", []), eq)))


307 
> snd


308 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))


309 
> LocalTheory.exit


310 
> ProofContext.theory_of


311 
end;


312 
fun add_random_inst [tyco] = (fn thy => case try (random_inst tyco) thy


313 
of SOME thy => thy


314 
 NONE => (warning ("Failed to generate random elements for type" ^ tyco); thy))


315 
 add_random_inst tycos = tap (fn _ => warning


316 
("Will not generated random elements for mutual recursive types " ^ commas (map quote tycos)));


317 
in DatatypePackage.interpretation add_random_inst end


318 
*}

26038

319 


320 
instantiation int :: random


321 
begin


322 


323 
definition


324 
"random n = (do


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


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


327 
done)"


328 


329 
instance ..


330 


331 
end


332 


333 
code_reserved SML Quickcheck


334 


335 


336 
subsection {* Quickcheck generator *}


337 


338 
ML {*


339 
structure Quickcheck =


340 
struct


341 


342 
open Quickcheck;


343 


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


345 


346 
fun mk_generator_expr prop tys =


347 
let


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


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


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


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


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


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


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


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


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


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


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


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


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


361 


362 
fun compile_generator_expr thy prop tys =


363 
let


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


365 
(mk_generator_expr prop tys) [];


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


367 

26261

368 
fun VALUE prop tys thy =


369 
let


370 
val t = mk_generator_expr prop tys;


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


372 
in


373 
thy


374 
> TheoryTarget.init NONE


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


376 
> snd


377 
> LocalTheory.exit


378 
> ProofContext.theory_of


379 
end;


380 

26038

381 
end


382 
*}


383 


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


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


386 


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


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


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


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


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


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


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


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


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


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


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


398 


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


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


401 

26261

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


403 


404 
export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"


405 


406 
definition "FOO = (True, Suc 0)"


407 


408 
code_module (test) QuickcheckExample


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


410 
contains FOO*)


411 

26038

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


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


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


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


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


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


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


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


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


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


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

26261

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


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


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

26038

426 

26142

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

26261

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


429 
[@{typ "nat list"}, @{typ "nat list"}] *}

26142

430 


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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

26261

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

26038

449 


450 
subsection {* Incremental function generator *}


451 


452 
ML {*


453 
structure Quickcheck =


454 
struct


455 


456 
open Quickcheck;


457 


458 
fun random_fun (eq : 'a > 'a > bool)


459 
(random : seed > 'b * seed)


460 
(random_split : seed > seed * seed)


461 
(seed : seed) =


462 
let


463 
val (seed', seed'') = random_split seed;


464 
val state = ref (seed', []);


465 
fun random_fun' x =


466 
let


467 
val (seed, fun_map) = ! state;


468 
in case AList.lookup (uncurry eq) fun_map x


469 
of SOME y => y


470 
 NONE => let


471 
val (y, seed') = random seed;


472 
val _ = state := (seed', (x, y) :: fun_map);


473 
in y end


474 
end;


475 
in (random_fun', seed'') end;


476 


477 
end


478 
*}


479 


480 
axiomatization


481 
random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)


482 
\<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"


483 


484 
code_const random_fun_aux (SML "Quickcheck.random'_fun")


485 


486 
instantiation "fun" :: (term_of, term_of) term_of


487 
begin


488 


489 
instance ..


490 


491 
end


492 


493 
code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"


494 
(SML "(fn '_ => Const (\"arbitrary\", dummyT))")


495 

26042

496 
instantiation "fun" :: (eq, "{type, random}") random

26038

497 
begin


498 


499 
definition


500 
"random n = random_fun_aux (op =) (random n) split_seed"


501 


502 
instance ..


503 


504 
end


505 


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


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


508 


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


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


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


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


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


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


515 


516 
end
