author  haftmann 
Fri, 06 Feb 2009 15:15:32 +0100  
changeset 29823  0ab754d13ccd 
parent 29815  9e94b7078fa5 
child 30495  a5f1e4f46d14 
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 

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 