20400
|
1 |
(* ID: $Id$
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* A simple random engine *}
|
|
6 |
|
|
7 |
theory CodeRandom
|
|
8 |
imports CodeRevappl
|
|
9 |
begin
|
|
10 |
|
|
11 |
section {* A simple random engine *}
|
|
12 |
|
|
13 |
consts
|
|
14 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
|
|
15 |
|
|
16 |
primrec
|
|
17 |
"pick (x#xs) n = (let (k, v) = x in
|
|
18 |
if n < k then v else pick xs (n - k))"
|
|
19 |
|
|
20 |
lemma pick_def [code, simp]:
|
|
21 |
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
|
|
22 |
declare pick.simps [simp del, code del]
|
|
23 |
|
|
24 |
typedecl randseed
|
|
25 |
|
|
26 |
consts
|
|
27 |
random_shift :: "randseed \<Rightarrow> randseed"
|
|
28 |
random_seed :: "randseed \<Rightarrow> nat"
|
|
29 |
|
|
30 |
definition
|
|
31 |
random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed"
|
|
32 |
"random n s = (random_seed s mod n, random_shift s)"
|
|
33 |
|
|
34 |
lemma random_bound:
|
|
35 |
assumes "0 < n"
|
|
36 |
shows "fst (random n s) < n"
|
|
37 |
proof -
|
|
38 |
from prems mod_less_divisor have "!!m .m mod n < n" by auto
|
|
39 |
then show ?thesis unfolding random_def by simp
|
|
40 |
qed
|
|
41 |
|
|
42 |
lemma random_random_seed [simp]:
|
|
43 |
"snd (random n s) = random_shift s" unfolding random_def by simp
|
|
44 |
|
|
45 |
definition
|
|
46 |
select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
|
|
47 |
[simp]: "select xs s =
|
|
48 |
s
|
|
49 |
\<triangleright> random (length xs)
|
|
50 |
\<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
|
|
51 |
select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
|
|
52 |
[simp]: "select_weight xs s =
|
|
53 |
s
|
|
54 |
\<triangleright> random (foldl (op +) 0 (map fst xs))
|
|
55 |
\<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
|
|
56 |
|
|
57 |
lemma
|
|
58 |
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
|
|
59 |
proof (induct xs)
|
|
60 |
case Nil show ?case by (simp add: revappl random_def)
|
|
61 |
next
|
|
62 |
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
|
|
63 |
proof -
|
|
64 |
fix xs
|
|
65 |
fix y
|
|
66 |
show "map fst (map (Pair y) xs) = replicate (length xs) y"
|
|
67 |
by (induct xs) simp_all
|
|
68 |
qed
|
|
69 |
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
|
|
70 |
proof -
|
|
71 |
fix xs
|
|
72 |
fix n
|
|
73 |
assume "n < length xs"
|
|
74 |
then show "pick (map (Pair 1) xs) n = nth xs n"
|
|
75 |
proof (induct xs fixing: n)
|
|
76 |
case Nil then show ?case by simp
|
|
77 |
next
|
|
78 |
case (Cons x xs) show ?case
|
|
79 |
proof (cases n)
|
|
80 |
case 0 then show ?thesis by simp
|
|
81 |
next
|
|
82 |
case (Suc _)
|
|
83 |
from Cons have "n < length (x # xs)" by auto
|
|
84 |
then have "n < Suc (length xs)" by simp
|
|
85 |
with Suc have "n - 1 < Suc (length xs) - 1" by auto
|
|
86 |
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
|
|
87 |
with Suc show ?thesis by auto
|
|
88 |
qed
|
|
89 |
qed
|
|
90 |
qed
|
|
91 |
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
|
|
92 |
proof -
|
|
93 |
have replicate_append:
|
|
94 |
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
|
|
95 |
by (simp add: replicate_app_Cons_same)
|
|
96 |
fix xs
|
|
97 |
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
|
|
98 |
unfolding map_fst_Pair proof (induct xs)
|
|
99 |
case Nil show ?case by simp
|
|
100 |
next
|
|
101 |
case (Cons x xs) then show ?case unfolding replicate_append by simp
|
|
102 |
qed
|
|
103 |
qed
|
|
104 |
have pick_nth_random:
|
|
105 |
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
|
|
106 |
proof -
|
|
107 |
fix s
|
|
108 |
fix x
|
|
109 |
fix xs
|
|
110 |
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
|
|
111 |
from pick_nth [OF bound] show
|
|
112 |
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
|
|
113 |
qed
|
|
114 |
case (Cons x xs) then show ?case
|
|
115 |
unfolding select_weight_def sum_length revappl_split pick_nth_random
|
|
116 |
by (simp add: revappl_split)
|
|
117 |
qed
|
|
118 |
|
|
119 |
definition
|
|
120 |
random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
|
|
121 |
"random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
|
|
122 |
|
|
123 |
lemma random_nat [code]:
|
|
124 |
"random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
|
|
125 |
unfolding random_int_def Let_def split_def random_def by simp
|
|
126 |
|
|
127 |
ML {*
|
|
128 |
signature RANDOM =
|
|
129 |
sig
|
|
130 |
type seed = IntInf.int;
|
|
131 |
val seed: unit -> seed;
|
|
132 |
val value: IntInf.int -> seed -> IntInf.int * seed;
|
|
133 |
end;
|
|
134 |
|
|
135 |
structure Random : RANDOM =
|
|
136 |
struct
|
|
137 |
|
|
138 |
exception RANDOM;
|
|
139 |
|
|
140 |
type seed = IntInf.int;
|
|
141 |
|
|
142 |
local
|
|
143 |
val a = 16807;
|
|
144 |
val m = 2147483647;
|
|
145 |
in
|
|
146 |
fun next s = IntInf.mod (a * s, m)
|
|
147 |
end;
|
|
148 |
|
|
149 |
local
|
|
150 |
val seed_ref = ref 1;
|
|
151 |
in
|
|
152 |
fun seed () =
|
|
153 |
let
|
|
154 |
val r = next (!seed_ref)
|
|
155 |
in
|
|
156 |
(seed_ref := r; r)
|
|
157 |
end;
|
|
158 |
end;
|
|
159 |
|
|
160 |
fun value h s =
|
|
161 |
if h < 1 then raise RANDOM
|
|
162 |
else (IntInf.mod (s, h - 1), seed ());
|
|
163 |
|
|
164 |
end;
|
|
165 |
*}
|
|
166 |
|
|
167 |
code_typapp randseed
|
|
168 |
ml (target_atom "Random.seed")
|
|
169 |
|
|
170 |
code_constapp random_int
|
|
171 |
ml (target_atom "Random.value")
|
|
172 |
|
|
173 |
code_serialize ml select select_weight (-)
|
|
174 |
|
|
175 |
end |