author | haftmann |
Mon, 09 Mar 2009 14:43:51 +0100 | |
changeset 30387 | 0affb9975547 |
parent 29823 | 0ab754d13ccd |
child 30495 | a5f1e4f46d14 |
permissions | -rw-r--r-- |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU Muenchen *) |
22528 | 2 |
|
26265 | 3 |
header {* A HOL random engine *} |
22528 | 4 |
|
5 |
theory Random |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
6 |
imports Code_Index |
22528 | 7 |
begin |
8 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
9 |
notation fcomp (infixl "o>" 60) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
10 |
notation scomp (infixl "o\<rightarrow>" 60) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
11 |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
12 |
|
26265 | 13 |
subsection {* Auxiliary functions *} |
14 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
15 |
definition inc_shift :: "index \<Rightarrow> index \<Rightarrow> index" where |
26265 | 16 |
"inc_shift v k = (if v = k then 1 else k + 1)" |
17 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
18 |
definition minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index" where |
26265 | 19 |
"minus_shift r k l = (if k < l then r + k - l else k - l)" |
20 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
21 |
fun log :: "index \<Rightarrow> index \<Rightarrow> index" where |
26265 | 22 |
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" |
23 |
||
24 |
subsection {* Random seeds *} |
|
26038 | 25 |
|
26 |
types seed = "index \<times> index" |
|
22528 | 27 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
28 |
primrec "next" :: "seed \<Rightarrow> index \<times> seed" where |
26265 | 29 |
"next (v, w) = (let |
30 |
k = v div 53668; |
|
31 |
v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211); |
|
32 |
l = w div 52774; |
|
33 |
w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791); |
|
34 |
z = minus_shift 2147483562 v' (w' + 1) + 1 |
|
35 |
in (z, (v', w')))" |
|
36 |
||
37 |
lemma next_not_0: |
|
38 |
"fst (next s) \<noteq> 0" |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
39 |
by (cases s) (auto simp add: minus_shift_def Let_def) |
26265 | 40 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
41 |
primrec seed_invariant :: "seed \<Rightarrow> bool" where |
26265 | 42 |
"seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True" |
43 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
44 |
lemma if_same: "(if b then f x else f y) = f (if b then x else y)" |
26265 | 45 |
by (cases b) simp_all |
46 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
47 |
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where |
26038 | 48 |
"split_seed s = (let |
49 |
(v, w) = s; |
|
50 |
(v', w') = snd (next s); |
|
26265 | 51 |
v'' = inc_shift 2147483562 v; |
26038 | 52 |
s'' = (v'', w'); |
26265 | 53 |
w'' = inc_shift 2147483398 w; |
26038 | 54 |
s''' = (v', w'') |
55 |
in (s'', s'''))" |
|
56 |
||
57 |
||
26265 | 58 |
subsection {* Base selectors *} |
22528 | 59 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
60 |
function range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where |
26038 | 61 |
"range_aux k l s = (if k = 0 then (l, s) else |
62 |
let (v, s') = next s |
|
63 |
in range_aux (k - 1) (v + l * 2147483561) s')" |
|
64 |
by pat_completeness auto |
|
65 |
termination |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset
|
66 |
by (relation "measure (Code_Index.nat_of o fst)") |
26038 | 67 |
(auto simp add: index) |
22528 | 68 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
69 |
definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
70 |
"range k = range_aux (log 2147483561 k) 1 |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
71 |
o\<rightarrow> (\<lambda>v. Pair (v mod k))" |
26265 | 72 |
|
73 |
lemma range: |
|
74 |
assumes "k > 0" |
|
75 |
shows "fst (range k s) < k" |
|
76 |
proof - |
|
77 |
obtain v w where range_aux: |
|
78 |
"range_aux (log 2147483561 k) 1 s = (v, w)" |
|
79 |
by (cases "range_aux (log 2147483561 k) 1 s") |
|
80 |
with assms show ?thesis |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
81 |
by (simp add: scomp_apply range_def del: range_aux.simps log.simps) |
26265 | 82 |
qed |
26038 | 83 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
84 |
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
85 |
"select xs = range (Code_Index.of_nat (length xs)) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
86 |
o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))" |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
87 |
|
26265 | 88 |
lemma select: |
89 |
assumes "xs \<noteq> []" |
|
90 |
shows "fst (select xs s) \<in> set xs" |
|
91 |
proof - |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset
|
92 |
from assms have "Code_Index.of_nat (length xs) > 0" by simp |
26265 | 93 |
with range have |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset
|
94 |
"fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best |
26265 | 95 |
then have |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset
|
96 |
"Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp |
26265 | 97 |
then show ?thesis |
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
98 |
by (simp add: scomp_apply split_beta select_def) |
26265 | 99 |
qed |
22528 | 100 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
101 |
definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
102 |
[code del]: "select_default k x y = range k |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
103 |
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))" |
26265 | 104 |
|
105 |
lemma select_default_zero: |
|
106 |
"fst (select_default 0 x y s) = y" |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
107 |
by (simp add: scomp_apply split_beta select_default_def) |
26038 | 108 |
|
26265 | 109 |
lemma select_default_code [code]: |
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
110 |
"select_default k x y = (if k = 0 |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
111 |
then range 1 o\<rightarrow> (\<lambda>_. Pair y) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
112 |
else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))" |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
113 |
proof |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
114 |
fix s |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
115 |
have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)" |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
116 |
by (simp add: range_def scomp_Pair scomp_apply split_beta) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
117 |
then show "select_default k x y s = (if k = 0 |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
118 |
then range 1 o\<rightarrow> (\<lambda>_. Pair y) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
119 |
else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s" |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
120 |
by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta) |
26265 | 121 |
qed |
22528 | 122 |
|
26265 | 123 |
|
124 |
subsection {* @{text ML} interface *} |
|
22528 | 125 |
|
126 |
ML {* |
|
26265 | 127 |
structure Random_Engine = |
22528 | 128 |
struct |
129 |
||
26038 | 130 |
type seed = int * int; |
22528 | 131 |
|
132 |
local |
|
26038 | 133 |
|
26265 | 134 |
val seed = ref |
135 |
(let |
|
136 |
val now = Time.toMilliseconds (Time.now ()); |
|
26038 | 137 |
val (q, s1) = IntInf.divMod (now, 2147483562); |
138 |
val s2 = q mod 2147483398; |
|
26265 | 139 |
in (s1 + 1, s2 + 1) end); |
140 |
||
22528 | 141 |
in |
26038 | 142 |
|
143 |
fun run f = |
|
144 |
let |
|
26265 | 145 |
val (x, seed') = f (! seed); |
26038 | 146 |
val _ = seed := seed' |
147 |
in x end; |
|
148 |
||
22528 | 149 |
end; |
150 |
||
151 |
end; |
|
152 |
*} |
|
153 |
||
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
154 |
no_notation fcomp (infixl "o>" 60) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
155 |
no_notation scomp (infixl "o\<rightarrow>" 60) |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
156 |
|
26038 | 157 |
end |
28145 | 158 |