2 Author: Florian Haftmann, TU Muenchen
5 header {* A HOL random engine *}
8 imports State_Monad Code_Index
11 subsection {* Auxiliary functions *}
14 inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
16 "inc_shift v k = (if v = k then 1 else k + 1)"
19 minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
21 "minus_shift r k l = (if k < l then r + k - l else k - l)"
24 log :: "index \<Rightarrow> index \<Rightarrow> index"
26 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
27 by pat_completeness auto
29 by (relation "measure (nat_of_index o snd)")
30 (auto simp add: index)
33 subsection {* Random seeds *}
35 types seed = "index \<times> index"
38 "next" :: "seed \<Rightarrow> index \<times> seed"
42 v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
44 w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
45 z = minus_shift 2147483562 v' (w' + 1) + 1
49 "fst (next s) \<noteq> 0"
51 apply (auto simp add: minus_shift_def Let_def)
55 seed_invariant :: "seed \<Rightarrow> bool"
57 "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
60 "(if b then f x else f y) = f (if b then x else y)"
63 (*lemma seed_invariant:
64 assumes "seed_invariant (index_of_nat v, index_of_nat w)"
65 and "(index_of_nat z, (index_of_nat v', index_of_nat w')) = next (index_of_nat v, index_of_nat w)"
66 shows "seed_invariant (index_of_nat v', index_of_nat w')"
68 apply (auto simp add: seed_invariant_def)
69 apply (auto simp add: minus_shift_def Let_def)
70 apply (simp_all add: if_same cong del: if_cong)
76 split_seed :: "seed \<Rightarrow> seed \<times> seed"
80 (v', w') = snd (next s);
81 v'' = inc_shift 2147483562 v;
83 w'' = inc_shift 2147483398 w;
88 subsection {* Base selectors *}
91 range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
93 "range_aux k l s = (if k = 0 then (l, s) else
95 in range_aux (k - 1) (v + l * 2147483561) s')"
96 by pat_completeness auto
98 by (relation "measure (nat_of_index o fst)")
99 (auto simp add: index)
102 range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
105 v \<leftarrow> range_aux (log 2147483561 k) 1;
111 shows "fst (range k s) < k"
113 obtain v w where range_aux:
114 "range_aux (log 2147483561 k) 1 s = (v, w)"
115 by (cases "range_aux (log 2147483561 k) 1 s")
116 with assms show ?thesis
117 by (simp add: range_def run_def mbind_def split_def del: range_aux.simps log.simps)
121 select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
124 k \<leftarrow> range (index_of_nat (length xs));
125 return (nth xs (nat_of_index k))
129 assumes "xs \<noteq> []"
130 shows "fst (select xs s) \<in> set xs"
132 from assms have "index_of_nat (length xs) > 0" by simp
134 "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
136 "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
138 by (auto simp add: select_def run_def mbind_def split_def)
142 select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
144 [code func del]: "select_default k x y = (do
145 l \<leftarrow> range k;
146 return (if l + 1 < k then x else y)
149 lemma select_default_zero:
150 "fst (select_default 0 x y s) = y"
151 by (simp add: run_def mbind_def split_def select_default_def)
153 lemma select_default_code [code]:
154 "select_default k x y = (if k = 0 then do
155 _ \<leftarrow> range 1;
158 l \<leftarrow> range k;
159 return (if l + 1 < k then x else y)
161 proof (cases "k = 0")
162 case False then show ?thesis by (simp add: select_default_def)
164 case True then show ?thesis
165 by (simp add: run_def mbind_def split_def select_default_def expand_fun_eq range_def)
169 subsection {* @{text ML} interface *}
172 structure Random_Engine =
175 type seed = int * int;
181 val now = Time.toMilliseconds (Time.now ());
182 val (q, s1) = IntInf.divMod (now, 2147483562);
183 val s2 = q mod 2147483398;
184 in (s1 + 1, s2 + 1) end);
190 val (x, seed') = f (! seed);
191 val _ = seed := seed'