author  haftmann 
Thu, 12 Mar 2009 18:01:25 +0100  
changeset 30495  a5f1e4f46d14 
parent 29823  0ab754d13ccd 
child 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 

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

22528  63 

30495  64 
definition %quote range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where 
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 

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

90 
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

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

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

94 
lemma select_default_zero: 

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

96 
by (simp add: scomp_apply split_beta select_default_def) 
26038  97 

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

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

100 
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

101 
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

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

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

104 
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

105 
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

106 
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

107 
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

108 
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

109 
by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta) 
26265  110 
qed 
22528  111 

26265  112 

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

22528  114 

115 
ML {* 

26265  116 
structure Random_Engine = 
22528  117 
struct 
118 

26038  119 
type seed = int * int; 
22528  120 

121 
local 

26038  122 

26265  123 
val seed = ref 
124 
(let 

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

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

26265  128 
in (s1 + 1, s2 + 1) end); 
129 

22528  130 
in 
26038  131 

132 
fun run f = 

133 
let 

26265  134 
val (x, seed') = f (! seed); 
26038  135 
val _ = seed := seed' 
136 
in x end; 

137 

22528  138 
end; 
139 

140 
end; 

141 
*} 

142 

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

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

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

145 

26038  146 
end 
28145  147 