1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* A HOL random engine *}
6 imports State_Monad Code_Index
9 subsection {* Auxiliary functions *}
12 inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
14 "inc_shift v k = (if v = k then 1 else k + 1)"
17 minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
19 "minus_shift r k l = (if k < l then r + k - l else k - l)"
22 log :: "index \<Rightarrow> index \<Rightarrow> index"
24 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
26 subsection {* Random seeds *}
28 types seed = "index \<times> index"
31 "next" :: "seed \<Rightarrow> index \<times> seed"
35 v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
37 w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
38 z = minus_shift 2147483562 v' (w' + 1) + 1
42 "fst (next s) \<noteq> 0"
44 apply (auto simp add: minus_shift_def Let_def)
48 seed_invariant :: "seed \<Rightarrow> bool"
50 "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
53 "(if b then f x else f y) = f (if b then x else y)"
57 split_seed :: "seed \<Rightarrow> seed \<times> seed"
61 (v', w') = snd (next s);
62 v'' = inc_shift 2147483562 v;
64 w'' = inc_shift 2147483398 w;
69 subsection {* Base selectors *}
72 range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
74 "range_aux k l s = (if k = 0 then (l, s) else
76 in range_aux (k - 1) (v + l * 2147483561) s')"
77 by pat_completeness auto
79 by (relation "measure (Code_Index.nat_of o fst)")
80 (auto simp add: index)
83 range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
86 v \<leftarrow> range_aux (log 2147483561 k) 1;
92 shows "fst (range k s) < k"
94 obtain v w where range_aux:
95 "range_aux (log 2147483561 k) 1 s = (v, w)"
96 by (cases "range_aux (log 2147483561 k) 1 s")
97 with assms show ?thesis
98 by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
102 select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
105 k \<leftarrow> range (Code_Index.of_nat (length xs));
106 return (nth xs (Code_Index.nat_of k))
110 assumes "xs \<noteq> []"
111 shows "fst (select xs s) \<in> set xs"
113 from assms have "Code_Index.of_nat (length xs) > 0" by simp
115 "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
117 "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
119 by (auto simp add: monad_collapse select_def)
123 select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
125 [code del]: "select_default k x y = (do
126 l \<leftarrow> range k;
127 return (if l + 1 < k then x else y)
130 lemma select_default_zero:
131 "fst (select_default 0 x y s) = y"
132 by (simp add: monad_collapse select_default_def)
134 lemma select_default_code [code]:
135 "select_default k x y = (if k = 0 then do
136 _ \<leftarrow> range 1;
139 l \<leftarrow> range k;
140 return (if l + 1 < k then x else y)
142 proof (cases "k = 0")
143 case False then show ?thesis by (simp add: select_default_def)
145 case True then show ?thesis
146 by (simp add: monad_collapse select_default_def range_def)
150 subsection {* @{text ML} interface *}
153 structure Random_Engine =
156 type seed = int * int;
162 val now = Time.toMilliseconds (Time.now ());
163 val (q, s1) = IntInf.divMod (now, 2147483562);
164 val s2 = q mod 2147483398;
165 in (s1 + 1, s2 + 1) end);
171 val (x, seed') = f (! seed);
172 val _ = seed := seed'