author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46311  56fae81902ce 
child 51143  0a2371e7ced3 
permissions  rwrr 
36020
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

1 

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

2 
(* Author: Florian Haftmann, TU Muenchen *) 
22528  3 

26265  4 
header {* A HOL random engine *} 
22528  5 

6 
theory Random 

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

7 
imports Code_Numeral List 
22528  8 
begin 
9 

37751  10 
notation fcomp (infixl "\<circ>>" 60) 
11 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

12 

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

13 

26265  14 
subsection {* Auxiliary functions *} 
15 

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

18 

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

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

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

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

30495  25 

26265  26 
subsection {* Random seeds *} 
26038  27 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
39302
diff
changeset

28 
type_synonym seed = "code_numeral \<times> code_numeral" 
22528  29 

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

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

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

38 

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

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

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

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

26038  46 

47 

26265  48 
subsection {* Base selectors *} 
22528  49 

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

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

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

53 
definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where 
30495  54 
"range k = iterate (log 2147483561 k) 
37751  55 
(\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1 
56 
\<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))" 

26265  57 

58 
lemma range: 

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

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

62 
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

63 
"select xs = range (Code_Numeral.of_nat (length xs)) 
37751  64 
\<circ>\<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

65 

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

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

69 
proof  

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

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

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

74 
"Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp 
26265  75 
then show ?thesis 
44921  76 
by (simp add: split_beta select_def) 
26265  77 
qed 
22528  78 

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

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

82 
lemma pick_member: 

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

84 
by (induct xs arbitrary: i) simp_all 

85 

86 
lemma pick_drop_zero: 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

88 
by (induct xs) (auto simp add: fun_eq_iff) 
31180  89 

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

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

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

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

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

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

95 
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

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

97 

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

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

102 
lemma select_weight_member: 

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

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

105 
proof  

106 
from range assms 

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

108 
with pick_member 

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

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

111 
qed 

112 

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

115 
by (simp add: select_weight_def) 

116 

46311  117 
lemma select_weight_drop_zero: 
31261  118 
"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

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

120 
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

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

122 
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

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

124 

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

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

128 
proof  
31261  129 
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

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

131 
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

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

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

134 
by (auto simp add: select_weight_def select_def scomp_def split_def 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

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

137 

26265  138 

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

22528  140 

36538
4fe16d49283b
make random engine persistent using code_reflect
haftmann
parents:
36176
diff
changeset

141 
code_reflect Random_Engine 
4fe16d49283b
make random engine persistent using code_reflect
haftmann
parents:
36176
diff
changeset

142 
functions range select select_weight 
4fe16d49283b
make random engine persistent using code_reflect
haftmann
parents:
36176
diff
changeset

143 

22528  144 
ML {* 
26265  145 
structure Random_Engine = 
22528  146 
struct 
147 

36538
4fe16d49283b
make random engine persistent using code_reflect
haftmann
parents:
36176
diff
changeset

148 
open Random_Engine; 
4fe16d49283b
make random engine persistent using code_reflect
haftmann
parents:
36176
diff
changeset

149 

26038  150 
type seed = int * int; 
22528  151 

152 
local 

26038  153 

32740  154 
val seed = Unsynchronized.ref 
26265  155 
(let 
156 
val now = Time.toMilliseconds (Time.now ()); 

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

26265  159 
in (s1 + 1, s2 + 1) end); 
160 

22528  161 
in 
26038  162 

36020
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

163 
fun next_seed () = 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

164 
let 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

165 
val (seed1, seed') = @{code split_seed} (! seed) 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

166 
val _ = seed := seed' 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

167 
in 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

168 
seed1 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

169 
end 
3ee4c29ead7f
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
bulwahn
parents:
35266
diff
changeset

170 

26038  171 
fun run f = 
172 
let 

26265  173 
val (x, seed') = f (! seed); 
26038  174 
val _ = seed := seed' 
175 
in x end; 

176 

22528  177 
end; 
178 

179 
end; 

180 
*} 

181 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36020
diff
changeset

182 
hide_type (open) seed 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36020
diff
changeset

183 
hide_const (open) inc_shift minus_shift log "next" split_seed 
31636  184 
iterate range select pick select_weight 
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36020
diff
changeset

185 
hide_fact (open) range_def 
31180  186 

37751  187 
no_notation fcomp (infixl "\<circ>>" 60) 
188 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 

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

189 

26038  190 
end 