author | blanchet |
Wed, 15 Dec 2010 11:26:28 +0100 | |
changeset 41140 | 9c68004b8c9d |
parent 39302 | d7728f65b353 |
child 42163 | 392fd6c4669c |
permissions | -rw-r--r-- |
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 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
28 |
types 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" |
60 |
by (simp add: range_def scomp_apply 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 |
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29815
diff
changeset
|
76 |
by (simp add: scomp_apply 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 |
||
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset
|
117 |
lemma select_weigth_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 |
|
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31196
diff
changeset
|
125 |
lemma select_weigth_select: |
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 |
28145 | 191 |