author  wenzelm 
Thu, 11 Feb 2010 23:00:22 +0100  
changeset 35115  446c5063e4fd 
parent 33236  ea75c6ea643e 
child 35266  07a56610c00b 
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 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

6 
imports Code_Numeral List 
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 

33236  15 
fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where 
16 
"log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" 

17 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

18 
definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where 
26265  19 
"inc_shift v k = (if v = k then 1 else k + 1)" 
20 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

21 
definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where 
26265  22 
"minus_shift r k l = (if k < l then r + k  l else k  l)" 
23 

30495  24 

26265  25 
subsection {* Random seeds *} 
26038  26 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

27 
types seed = "code_numeral \<times> code_numeral" 
22528  28 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

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

33236  32 
v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211); 
26265  33 
l = w div 52774; 
33236  34 
w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791); 
26265  35 
z = minus_shift 2147483562 v' (w' + 1) + 1 
36 
in (z, (v', w')))" 

37 

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

38 
definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where 
26038  39 
"split_seed s = (let 
40 
(v, w) = s; 

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

26265  42 
v'' = inc_shift 2147483562 v; 
33236  43 
w'' = inc_shift 2147483398 w 
44 
in ((v'', w'), (v', w'')))" 

26038  45 

46 

26265  47 
subsection {* Base selectors *} 
22528  48 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

49 
fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where 
30495  50 
"iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k  1) f)" 
22528  51 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

52 
definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where 
30495  53 
"range k = iterate (log 2147483561 k) 
54 
(\<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

55 
o\<rightarrow> (\<lambda>v. Pair (v mod k))" 
26265  56 

57 
lemma range: 

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

26038  60 

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

61 
definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

62 
"select xs = range (Code_Numeral.of_nat (length xs)) 
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

63 
o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))" 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset

64 

26265  65 
lemma select: 
66 
assumes "xs \<noteq> []" 

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

68 
proof  

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

69 
from assms have "Code_Numeral.of_nat (length xs) > 0" by simp 
26265  70 
with range have 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

71 
"fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best 
26265  72 
then have 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

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

75 
by (simp add: scomp_apply split_beta select_def) 
26265  76 
qed 
22528  77 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

78 
primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where 
31180  79 
"pick (x # xs) i = (if i < fst x then snd x else pick xs (i  fst x))" 
80 

81 
lemma pick_member: 

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

83 
by (induct xs arbitrary: i) simp_all 

84 

85 
lemma pick_drop_zero: 

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

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

88 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

89 
lemma pick_same: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

90 
"l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

91 
proof (induct xs arbitrary: l) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

92 
case Nil then show ?case by simp 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

93 
next 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

94 
case (Cons x xs) then show ?case by (cases l) simp_all 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

95 
qed 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

96 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

97 
definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where 
31180  98 
"select_weight xs = range (listsum (map fst xs)) 
99 
o\<rightarrow> (\<lambda>k. Pair (pick xs k))" 

100 

101 
lemma select_weight_member: 

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

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

104 
proof  

105 
from range assms 

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

107 
with pick_member 

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

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

110 
qed 

111 

31268  112 
lemma select_weight_cons_zero: 
113 
"select_weight ((0, x) # xs) = select_weight xs" 

114 
by (simp add: select_weight_def) 

115 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

116 
lemma select_weigth_drop_zero: 
31261  117 
"select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

118 
proof  
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

119 
have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)" 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

120 
by (induct xs) auto 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

121 
then show ?thesis by (simp only: select_weight_def pick_drop_zero) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

122 
qed 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

123 

5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

124 
lemma select_weigth_select: 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

125 
assumes "xs \<noteq> []" 
31261  126 
shows "select_weight (map (Pair 1) xs) = select xs" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

127 
proof  
31261  128 
have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

129 
using assms by (intro range) simp 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

130 
moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)" 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

131 
by (induct xs) simp_all 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

132 
ultimately show ?thesis 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

133 
by (auto simp add: select_weight_def select_def scomp_def split_def 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

134 
expand_fun_eq pick_same [symmetric]) 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

135 
qed 
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset

136 

26265  137 

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

22528  139 

140 
ML {* 

26265  141 
structure Random_Engine = 
22528  142 
struct 
143 

26038  144 
type seed = int * int; 
22528  145 

146 
local 

26038  147 

32740  148 
val seed = Unsynchronized.ref 
26265  149 
(let 
150 
val now = Time.toMilliseconds (Time.now ()); 

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

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

22528  155 
in 
26038  156 

157 
fun run f = 

158 
let 

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

162 

22528  163 
end; 
164 

165 
end; 

166 
*} 

167 

31180  168 
hide (open) type seed 
33236  169 
hide (open) const inc_shift minus_shift log "next" split_seed 
31636  170 
iterate range select pick select_weight 
31180  171 

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

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

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

174 

26038  175 
end 
28145  176 