author | haftmann |
Fri, 20 Jul 2007 14:28:25 +0200 | |
changeset 23881 | 851c74f1bb69 |
parent 22845 | 5f9138bcb3d7 |
child 24043 | 9b156986a4e9 |
permissions | -rw-r--r-- |
22528 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* A simple random engine *} |
|
6 |
||
7 |
theory Random |
|
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22528
diff
changeset
|
8 |
imports State_Monad Pretty_Int |
22528 | 9 |
begin |
10 |
||
11 |
fun |
|
12 |
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" |
|
13 |
where |
|
14 |
pick_undef: "pick [] n = undefined" |
|
15 |
| pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" |
|
22845 | 16 |
lemmas [code func del] = pick_undef |
22528 | 17 |
|
18 |
typedecl randseed |
|
19 |
||
20 |
axiomatization |
|
21 |
random_shift :: "randseed \<Rightarrow> randseed" |
|
22 |
||
23 |
axiomatization |
|
24 |
random_seed :: "randseed \<Rightarrow> nat" |
|
25 |
||
26 |
definition |
|
27 |
random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where |
|
28 |
"random n s = (random_seed s mod n, random_shift s)" |
|
29 |
||
30 |
lemma random_bound: |
|
31 |
assumes "0 < n" |
|
32 |
shows "fst (random n s) < n" |
|
33 |
proof - |
|
34 |
from prems mod_less_divisor have "!!m .m mod n < n" by auto |
|
35 |
then show ?thesis unfolding random_def by simp |
|
36 |
qed |
|
37 |
||
38 |
lemma random_random_seed [simp]: |
|
39 |
"snd (random n s) = random_shift s" unfolding random_def by simp |
|
40 |
||
41 |
definition |
|
42 |
select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where |
|
43 |
[simp]: "select xs = (do |
|
44 |
n \<leftarrow> random (length xs); |
|
45 |
return (nth xs n) |
|
46 |
done)" |
|
47 |
definition |
|
48 |
select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where |
|
49 |
[simp]: "select_weight xs = (do |
|
50 |
n \<leftarrow> random (foldl (op +) 0 (map fst xs)); |
|
51 |
return (pick xs n) |
|
52 |
done)" |
|
53 |
||
54 |
lemma |
|
55 |
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s" |
|
56 |
proof (induct xs) |
|
57 |
case Nil show ?case by (simp add: monad_collapse random_def) |
|
58 |
next |
|
59 |
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y" |
|
60 |
proof - |
|
61 |
fix xs |
|
62 |
fix y |
|
63 |
show "map fst (map (Pair y) xs) = replicate (length xs) y" |
|
64 |
by (induct xs) simp_all |
|
65 |
qed |
|
66 |
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n" |
|
67 |
proof - |
|
68 |
fix xs |
|
69 |
fix n |
|
70 |
assume "n < length xs" |
|
71 |
then show "pick (map (Pair 1) xs) n = nth xs n" |
|
72 |
proof (induct xs arbitrary: n) |
|
73 |
case Nil then show ?case by simp |
|
74 |
next |
|
75 |
case (Cons x xs) show ?case |
|
76 |
proof (cases n) |
|
77 |
case 0 then show ?thesis by simp |
|
78 |
next |
|
79 |
case (Suc _) |
|
80 |
from Cons have "n < length (x # xs)" by auto |
|
81 |
then have "n < Suc (length xs)" by simp |
|
82 |
with Suc have "n - 1 < Suc (length xs) - 1" by auto |
|
83 |
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto |
|
84 |
with Suc show ?thesis by auto |
|
85 |
qed |
|
86 |
qed |
|
87 |
qed |
|
88 |
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs" |
|
89 |
proof - |
|
90 |
have replicate_append: |
|
91 |
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]" |
|
92 |
by (simp add: replicate_app_Cons_same) |
|
93 |
fix xs |
|
94 |
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs" |
|
95 |
unfolding map_fst_Pair proof (induct xs) |
|
96 |
case Nil show ?case by simp |
|
97 |
next |
|
98 |
case (Cons x xs) then show ?case unfolding replicate_append by simp |
|
99 |
qed |
|
100 |
qed |
|
101 |
have pick_nth_random: |
|
102 |
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" |
|
103 |
proof - |
|
104 |
fix s |
|
105 |
fix x |
|
106 |
fix xs |
|
107 |
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp |
|
108 |
from pick_nth [OF bound] show |
|
109 |
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" . |
|
110 |
qed |
|
111 |
have pick_nth_random_do: |
|
112 |
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s = |
|
113 |
(do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s" |
|
114 |
unfolding monad_collapse split_def unfolding pick_nth_random .. |
|
115 |
case (Cons x xs) then show ?case |
|
116 |
unfolding select_weight_def sum_length pick_nth_random_do |
|
117 |
by simp |
|
118 |
qed |
|
119 |
||
120 |
definition |
|
121 |
random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where |
|
122 |
"random_int k = (do n \<leftarrow> random (nat k); return (int n) done)" |
|
123 |
||
124 |
lemma random_nat [code]: |
|
125 |
"random n = (do k \<leftarrow> random_int (int n); return (nat k) done)" |
|
126 |
unfolding random_int_def by simp |
|
127 |
||
128 |
axiomatization |
|
129 |
run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a" |
|
130 |
||
131 |
ML {* |
|
132 |
signature RANDOM = |
|
133 |
sig |
|
134 |
type seed = IntInf.int; |
|
135 |
val seed: unit -> seed; |
|
136 |
val value: IntInf.int -> seed -> IntInf.int * seed; |
|
137 |
end; |
|
138 |
||
139 |
structure Random : RANDOM = |
|
140 |
struct |
|
141 |
||
142 |
open IntInf; |
|
143 |
||
144 |
exception RANDOM; |
|
145 |
||
146 |
type seed = int; |
|
147 |
||
148 |
local |
|
149 |
val a = fromInt 16807; |
|
150 |
(*greetings to SML/NJ*) |
|
151 |
val m = (the o fromString) "2147483647"; |
|
152 |
in |
|
153 |
fun next s = (a * s) mod m; |
|
154 |
end; |
|
155 |
||
156 |
local |
|
157 |
val seed_ref = ref (fromInt 1); |
|
158 |
in |
|
159 |
fun seed () = |
|
160 |
let |
|
161 |
val r = next (!seed_ref) |
|
162 |
in |
|
163 |
(seed_ref := r; r) |
|
164 |
end; |
|
165 |
end; |
|
166 |
||
167 |
fun value h s = |
|
168 |
if h < 1 then raise RANDOM |
|
169 |
else (s mod (h - 1), seed ()); |
|
170 |
||
171 |
end; |
|
172 |
*} |
|
173 |
||
174 |
code_type randseed |
|
175 |
(SML "Random.seed") |
|
176 |
||
177 |
code_const random_int |
|
178 |
(SML "Random.value") |
|
179 |
||
180 |
code_const run_random |
|
181 |
(SML "case _ (Random.seed ()) of (x, '_) => x") |
|
182 |
||
183 |
end |