author  haftmann 
Fri, 15 May 2009 16:39:16 +0200  
changeset 31180  dae7be64d614 
parent 30500  072daf3914c0 
permissions  rwrr 
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 

30495  24 

26265  25 
subsection {* Random seeds *} 
26038  26 

27 
types seed = "index \<times> index" 

22528  28 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

29 
primrec "next" :: "seed \<Rightarrow> index \<times> seed" where 
26265  30 
"next (v, w) = (let 
31 
k = v div 53668; 

32 
v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211); 

33 
l = w div 52774; 

34 
w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791); 

35 
z = minus_shift 2147483562 v' (w' + 1) + 1 

36 
in (z, (v', w')))" 

37 

38 
lemma next_not_0: 

39 
"fst (next s) \<noteq> 0" 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

40 
by (cases s) (auto simp add: minus_shift_def Let_def) 
26265  41 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

42 
primrec seed_invariant :: "seed \<Rightarrow> bool" where 
26265  43 
"seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True" 
44 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

45 
lemma if_same: "(if b then f x else f y) = f (if b then x else y)" 
26265  46 
by (cases b) simp_all 
47 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

48 
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where 
26038  49 
"split_seed s = (let 
50 
(v, w) = s; 

51 
(v', w') = snd (next s); 

26265  52 
v'' = inc_shift 2147483562 v; 
26038  53 
s'' = (v'', w'); 
26265  54 
w'' = inc_shift 2147483398 w; 
26038  55 
s''' = (v', w'') 
56 
in (s'', s'''))" 

57 

58 

26265  59 
subsection {* Base selectors *} 
22528  60 

30500  61 
fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 
30495  62 
"iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k  1) f)" 
22528  63 

30500  64 
definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where 
30495  65 
"range k = iterate (log 2147483561 k) 
66 
(\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

67 
o\<rightarrow> (\<lambda>v. Pair (v mod k))" 
26265  68 

69 
lemma range: 

30495  70 
"k > 0 \<Longrightarrow> fst (range k s) < k" 
71 
by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps) 

26038  72 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

73 
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

74 
"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

75 
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

76 

26265  77 
lemma select: 
78 
assumes "xs \<noteq> []" 

79 
shows "fst (select xs s) \<in> set xs" 

80 
proof  

29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset

81 
from assms have "Code_Index.of_nat (length xs) > 0" by simp 
26265  82 
with range have 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset

83 
"fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best 
26265  84 
then have 
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29806
diff
changeset

85 
"Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp 
26265  86 
then show ?thesis 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

87 
by (simp add: scomp_apply split_beta select_def) 
26265  88 
qed 
22528  89 

31180  90 
primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where 
91 
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i  fst x))" 

92 

93 
lemma pick_member: 

94 
"i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)" 

95 
by (induct xs arbitrary: i) simp_all 

96 

97 
lemma pick_drop_zero: 

98 
"pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs" 

99 
by (induct xs) (auto simp add: expand_fun_eq) 

100 

101 
definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where 

102 
"select_weight xs = range (listsum (map fst xs)) 

103 
o\<rightarrow> (\<lambda>k. Pair (pick xs k))" 

104 

105 
lemma select_weight_member: 

106 
assumes "0 < listsum (map fst xs)" 

107 
shows "fst (select_weight xs s) \<in> set (map snd xs)" 

108 
proof  

109 
from range assms 

110 
have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" . 

111 
with pick_member 

112 
have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" . 

113 
then show ?thesis by (simp add: select_weight_def scomp_def split_def) 

114 
qed 

115 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

116 
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

117 
[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

118 
o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))" 
26265  119 

120 
lemma select_default_zero: 

121 
"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

122 
by (simp add: scomp_apply split_beta select_default_def) 
26038  123 

26265  124 
lemma select_default_code [code]: 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

125 
"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

126 
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

127 
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

128 
proof 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

129 
fix s 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

130 
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

131 
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

132 
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

133 
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

134 
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

135 
by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta) 
26265  136 
qed 
22528  137 

26265  138 

139 
subsection {* @{text ML} interface *} 

22528  140 

141 
ML {* 

26265  142 
structure Random_Engine = 
22528  143 
struct 
144 

26038  145 
type seed = int * int; 
22528  146 

147 
local 

26038  148 

26265  149 
val seed = ref 
150 
(let 

151 
val now = Time.toMilliseconds (Time.now ()); 

26038  152 
val (q, s1) = IntInf.divMod (now, 2147483562); 
153 
val s2 = q mod 2147483398; 

26265  154 
in (s1 + 1, s2 + 1) end); 
155 

22528  156 
in 
26038  157 

158 
fun run f = 

159 
let 

26265  160 
val (x, seed') = f (! seed); 
26038  161 
val _ = seed := seed' 
162 
in x end; 

163 

22528  164 
end; 
165 

166 
end; 

167 
*} 

168 

31180  169 
hide (open) type seed 
170 
hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed 

171 
iterate range select pick select_weight select_default 

172 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

173 
no_notation fcomp (infixl "o>" 60) 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

174 
no_notation scomp (infixl "o\<rightarrow>" 60) 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

175 

26038  176 
end 
28145  177 