# HG changeset patch # User haftmann # Date 1202118760 -3600 # Node ID 55a02586776d964fd0755dafd6724aa5dcf18ab7 # Parent 8bf9e480a7b81144496350436700925313b2ad3c towards quickcheck diff -r 8bf9e480a7b8 -r 55a02586776d src/HOL/ex/Random.thy --- a/src/HOL/ex/Random.thy Mon Feb 04 10:52:39 2008 +0100 +++ b/src/HOL/ex/Random.thy Mon Feb 04 10:52:40 2008 +0100 @@ -2,59 +2,97 @@ Author: Florian Haftmann, TU Muenchen *) -header {* A simple random engine *} +header {* A simple term generator *} theory Random -imports State_Monad Code_Integer +imports State_Monad Code_Index List Eval begin -fun - pick :: "(nat \ 'a) list \ nat \ 'a" -where - pick_undef: "pick [] n = undefined" - | pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" -lemmas [code func del] = pick_undef +subsection {* The random engine *} + +types seed = "index \ index" -typedecl randseed - -axiomatization - random_shift :: "randseed \ randseed" - -axiomatization - random_seed :: "randseed \ nat" +definition + "next" :: "seed \ index \ seed" +where + "next s = (let + (v, w) = s; + k = v div 53668; + v' = 40014 * (v - k * 53668) - k * 12211; + v'' = (if v' < 0 then v' + 2147483563 else v'); + l = w div 52774; + w' = 40692 * (w - l * 52774) - l * 3791; + w'' = (if w' < 0 then w' + 2147483399 else w'); + z = v'' - w''; + z' = (if z < 1 then z + 2147483562 else z) + in (z', (v'', w'')))" definition - random :: "nat \ randseed \ nat \ randseed" where - "random n s = (random_seed s mod n, random_shift s)" + split_seed :: "seed \ seed \ seed" +where + "split_seed s = (let + (v, w) = s; + (v', w') = snd (next s); + v'' = (if v = 2147483562 then 1 else v + 1); + s'' = (v'', w'); + w'' = (if w = 2147483398 then 1 else w + 1); + s''' = (v', w'') + in (s'', s'''))" + +text {* Base selectors *} + +primrec + pick :: "(nat \ 'a) list \ nat \ 'a" +where + "pick (x#xs) n = (if n < fst x then snd x else pick xs (n - fst x))" -lemma random_bound: - assumes "0 < n" - shows "fst (random n s) < n" -proof - - from prems mod_less_divisor have "!!m .m mod n < n" by auto - then show ?thesis unfolding random_def by simp -qed +function + iLogBase :: "index \ index \ index" +where + "iLogBase b i = (if b \ 1 \ i < b then 1 else 1 + iLogBase b (i div b))" +by pat_completeness auto +termination + by (relation "measure (nat_of_index o snd)") + (auto simp add: index) -lemma random_random_seed [simp]: - "snd (random n s) = random_shift s" unfolding random_def by simp +function + range_aux :: "index \ index \ seed \ index \ seed" +where + "range_aux k l s = (if k = 0 then (l, s) else + let (v, s') = next s + in range_aux (k - 1) (v + l * 2147483561) s')" +by pat_completeness auto +termination + by (relation "measure (nat_of_index o fst)") + (auto simp add: index) definition - select :: "'a list \ randseed \ 'a \ randseed" where - [simp]: "select xs = (do - n \ random (length xs); - return (nth xs n) - done)" + range :: "index \ seed \ index \ seed" +where + "range k s = (let + b = 2147483561; + n = iLogBase b k; + (v, s') = range_aux n 1 s + in (v mod k, s'))" + definition - select_weight :: "(nat \ 'a) list \ randseed \ 'a \ randseed" where - [simp]: "select_weight xs = (do - n \ random (foldl (op +) 0 (map fst xs)); - return (pick xs n) - done)" + select :: "'a list \ seed \ 'a \ seed" +where + [simp]: "select xs s = (let + (k, s') = range (index_of_nat (length xs)) s + in (nth xs (nat_of_index k), s'))" -lemma +definition + select_weight :: "(nat \ 'a) list \ seed \ 'a \ seed" +where + [simp]: "select_weight xs s = (let + (k, s') = range (foldr (op + \ index_of_nat \ fst) xs 0) s + in (pick xs (nat_of_index k), s'))" + +(*lemma "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s" proof (induct xs) - case Nil show ?case by (simp add: monad_collapse random_def) + case Nil show ?case apply (auto simp add: Let_def split_def) next have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y" proof - @@ -115,71 +153,300 @@ case (Cons x xs) then show ?case unfolding select_weight_def sum_length pick_nth_random_do by simp -qed - -definition - random_int :: "int \ randseed \ int * randseed" where - "random_int k = (do n \ random (nat k); return (int n) done)" +qed*) -lemma random_nat [code]: - "random n = (do k \ random_int (int n); return (nat k) done)" -unfolding random_int_def by simp - -axiomatization - run_random :: "(randseed \ 'a * randseed) \ 'a" +text {* The @{text ML} interface *} ML {* -signature RANDOM = -sig - type seed = int; - val seed: unit -> seed; - val value: int -> seed -> int * seed; -end; - -structure Random : RANDOM = +structure Quickcheck = struct -exception RANDOM; - -type seed = int; - -local - val a = 16807; - val m = 2147483647; -in - fun next s = (a * s) mod m; -end; +type seed = int * int; local - val seed_ref = ref 1; + +val seed = ref (0, 0); + +fun init () = + let + val now = Time.toNanoseconds (Time.now ()); + val (q, s1) = IntInf.divMod (now, 2147483562); + val s2 = q mod 2147483398; + in seed := (s1 + 1, s2 + 1) end; + in - fun seed () = CRITICAL (fn () => - let - val r = next (!seed_ref) - in - (seed_ref := r; r) - end); + +val seed = seed; (* FIXME *) + +fun run f = + let + val (x, seed') = f (!seed); + val _ = seed := seed' + val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then + (warning "broken random seed"; init ()) + else () + in x end; + end; -fun value h s = - if h < 1 then raise RANDOM - else (s mod (h - 1), seed ()); - end; *} -code_reserved SML Random + +subsection {* The @{text random} class *} + +class random = type + + fixes random :: "index \ seed \ 'a \ seed" + +-- {* FIXME dummy implementations *} + +instantiation nat :: random +begin + +definition + "random k = apfst nat_of_index \ range k" + +instance .. + +end + +instantiation bool :: random +begin + +definition + "random _ = apfst (op = 0) \ range 2" + +instance .. + +end -code_type randseed - (SML "Random.seed") -types_code randseed ("Random.seed") +instantiation unit :: random +begin + +definition + "random _ = Pair ()" + +instance .. + +end + +instantiation "+" :: (random, random) random +begin + +definition + "random n = (do + k \ next; + let l = k div 2; + (if k mod 2 = 0 then do + x \ random l; + return (Inl x) + done else do + x \ random l; + return (Inr x) + done) + done)" + +instance .. + +end -code_const random_int - (SML "Random.value") -consts_code random_int ("Random.value") +instantiation "*" :: (random, random) random +begin + +definition + "random n = (do + x \ random n; + y \ random n; + return (x, y) + done)" + +instance .. + +end + +instantiation int :: random +begin + +definition + "random n = (do + (b, m) \ random n; + return (if b then int m else - int m) + done)" + +instance .. + +end + +instantiation list :: (random) random +begin -code_const run_random - (SML "case (Random.seed ()) of (x, '_) => _ x") -consts_code run_random ("case (Random.seed ()) of (x, '_) => _ x") +primrec + random_list_aux +where + "random_list_aux 0 = Pair []" + | "random_list_aux (Suc n) = (do + x \ random (index_of_nat (Suc n)); + xs \ random_list_aux n; + return (x#xs) + done)" + +definition + [code func del]: "random n = random_list_aux (nat_of_index n)" + +lemma [code func]: + "random n = (if n = 0 then return ([]::'a list) + else do + x \ random n; + xs \ random (n - 1); + return (x#xs) + done)" +unfolding random_list_def +by (cases "nat_of_index n", auto) + (cases n, auto)+ + +(*fun + random_list +where + "random_list n = (if n = 0 then (\_. ([]::'a list)) + else random n \=\<^isub>R (\x::'a. random_list (n - 1) \=\<^isub>R (\(xs::'a list) _. x#xs)))"*) + +instance .. end + +code_reserved SML Quickcheck + + +subsection {* Quickcheck generator *} + +ML {* +structure Quickcheck = +struct + +open Quickcheck; + +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE; + +fun mk_generator_expr prop tys = + let + val bounds = map_index (fn (i, ty) => (i, ty)) tys; + val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds); + val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds; + val check = @{term "If \ bool \ term list option \ term list option \ term list option"} + $ result $ @{term "None \ term list option"} $ (@{term "Some \ term list \ term list option "} $ HOLogic.mk_list @{typ term} terms); + val return = @{term "Pair \ term list option \ seed \ term list option \ seed"}; + fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed}); + fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty + --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"}) + $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty) + $ Bound i) $ Abs ("a", ty, t); + val t = fold_rev mk_bindclause bounds (return $ check); + in Abs ("n", @{typ index}, t) end; + +fun compile_generator_expr thy prop tys = + let + val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy + (mk_generator_expr prop tys) []; + in f #> run #> (Option.map o map) (Code.postprocess_term thy) end; + +end +*} + +ML {* val f = Quickcheck.compile_generator_expr @{theory} + @{term "\(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *} + +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} + +ML {* val f = Quickcheck.compile_generator_expr @{theory} + @{term "\(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *} + +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *} + + +subsection {* Incremental function generator *} + +ML {* +structure Quickcheck = +struct + +open Quickcheck; + +fun random_fun (eq : 'a -> 'a -> bool) + (random : seed -> 'b * seed) + (random_split : seed -> seed * seed) + (seed : seed) = + let + val (seed', seed'') = random_split seed; + val state = ref (seed', []); + fun random_fun' x = + let + val (seed, fun_map) = ! state; + in case AList.lookup (uncurry eq) fun_map x + of SOME y => y + | NONE => let + val (y, seed') = random seed; + val _ = state := (seed', (x, y) :: fun_map); + in y end + end; + in (random_fun', seed'') end; + +end +*} + +axiomatization + random_fun_aux :: "('a \ 'a \ bool) \ (seed \ 'b \ seed) + \ (seed \ seed \ seed) \ seed \ ('a \ 'b) \ seed" + +code_const random_fun_aux (SML "Quickcheck.random'_fun") + +instantiation "fun" :: (term_of, term_of) term_of +begin + +instance .. + +end + +code_const "Eval.term_of :: ('a\term_of \ 'b\term_of) \ _" + (SML "(fn '_ => Const (\"arbitrary\", dummyT))") + +instantiation "fun" :: (eq, random) random +begin + +definition + "random n = random_fun_aux (op =) (random n) split_seed" + +instance .. + +end + +ML {* val f = Quickcheck.compile_generator_expr @{theory} + @{term "\f k. int (f k) = k"} [@{typ "int \ nat"}, @{typ int}] *} + +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *} + +end