author  haftmann 
Fri, 12 Oct 2007 08:21:09 +0200  
changeset 24994  c385c4eabb3b 
parent 24630  351a308ab58d 
child 26038  55a02586776d 
permissions  rwrr 
22528  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple random engine *} 

6 

7 
theory Random 

24994
c385c4eabb3b
consolidated naming conventions for code generator theories
haftmann
parents:
24630
diff
changeset

8 
imports State_Monad Code_Integer 
22528  9 
begin 
10 

11 
fun 

12 
pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a" 

13 
where 

14 
pick_undef: "pick [] n = undefined" 

15 
 pick_simp: "pick ((k, v)#xs) n = (if n < k then v else pick xs (n  k))" 

22845  16 
lemmas [code func del] = pick_undef 
22528  17 

18 
typedecl randseed 

19 

20 
axiomatization 

21 
random_shift :: "randseed \<Rightarrow> randseed" 

22 

23 
axiomatization 

24 
random_seed :: "randseed \<Rightarrow> nat" 

25 

26 
definition 

27 
random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where 

28 
"random n s = (random_seed s mod n, random_shift s)" 

29 

30 
lemma random_bound: 

31 
assumes "0 < n" 

32 
shows "fst (random n s) < n" 

33 
proof  

34 
from prems mod_less_divisor have "!!m .m mod n < n" by auto 

35 
then show ?thesis unfolding random_def by simp 

36 
qed 

37 

38 
lemma random_random_seed [simp]: 

39 
"snd (random n s) = random_shift s" unfolding random_def by simp 

40 

41 
definition 

42 
select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where 

43 
[simp]: "select xs = (do 

44 
n \<leftarrow> random (length xs); 

45 
return (nth xs n) 

46 
done)" 

47 
definition 

48 
select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where 

49 
[simp]: "select_weight xs = (do 

50 
n \<leftarrow> random (foldl (op +) 0 (map fst xs)); 

51 
return (pick xs n) 

52 
done)" 

53 

54 
lemma 

55 
"select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s" 

56 
proof (induct xs) 

57 
case Nil show ?case by (simp add: monad_collapse random_def) 

58 
next 

59 
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y" 

60 
proof  

61 
fix xs 

62 
fix y 

63 
show "map fst (map (Pair y) xs) = replicate (length xs) y" 

64 
by (induct xs) simp_all 

65 
qed 

66 
have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n" 

67 
proof  

68 
fix xs 

69 
fix n 

70 
assume "n < length xs" 

71 
then show "pick (map (Pair 1) xs) n = nth xs n" 

72 
proof (induct xs arbitrary: n) 

73 
case Nil then show ?case by simp 

74 
next 

75 
case (Cons x xs) show ?case 

76 
proof (cases n) 

77 
case 0 then show ?thesis by simp 

78 
next 

79 
case (Suc _) 

80 
from Cons have "n < length (x # xs)" by auto 

81 
then have "n < Suc (length xs)" by simp 

82 
with Suc have "n  1 < Suc (length xs)  1" by auto 

83 
with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n  1) = xs ! (n  1)" by auto 

84 
with Suc show ?thesis by auto 

85 
qed 

86 
qed 

87 
qed 

88 
have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs" 

89 
proof  

90 
have replicate_append: 

91 
"!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]" 

92 
by (simp add: replicate_app_Cons_same) 

93 
fix xs 

94 
show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs" 

95 
unfolding map_fst_Pair proof (induct xs) 

96 
case Nil show ?case by simp 

97 
next 

98 
case (Cons x xs) then show ?case unfolding replicate_append by simp 

99 
qed 

100 
qed 

101 
have pick_nth_random: 

102 
"!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" 

103 
proof  

104 
fix s 

105 
fix x 

106 
fix xs 

107 
have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp 

108 
from pick_nth [OF bound] show 

109 
"pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" . 

110 
qed 

111 
have pick_nth_random_do: 

112 
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s = 

113 
(do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s" 

114 
unfolding monad_collapse split_def unfolding pick_nth_random .. 

115 
case (Cons x xs) then show ?case 

116 
unfolding select_weight_def sum_length pick_nth_random_do 

117 
by simp 

118 
qed 

119 

120 
definition 

121 
random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where 

122 
"random_int k = (do n \<leftarrow> random (nat k); return (int n) done)" 

123 

124 
lemma random_nat [code]: 

125 
"random n = (do k \<leftarrow> random_int (int n); return (nat k) done)" 

126 
unfolding random_int_def by simp 

127 

128 
axiomatization 

129 
run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a" 

130 

131 
ML {* 

132 
signature RANDOM = 

133 
sig 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24226
diff
changeset

134 
type seed = int; 
22528  135 
val seed: unit > seed; 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24226
diff
changeset

136 
val value: int > seed > int * seed; 
22528  137 
end; 
138 

139 
structure Random : RANDOM = 

140 
struct 

141 

142 
exception RANDOM; 

143 

144 
type seed = int; 

145 

146 
local 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24226
diff
changeset

147 
val a = 16807; 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24226
diff
changeset

148 
val m = 2147483647; 
22528  149 
in 
150 
fun next s = (a * s) mod m; 

151 
end; 

152 

153 
local 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24226
diff
changeset

154 
val seed_ref = ref 1; 
22528  155 
in 
24043  156 
fun seed () = CRITICAL (fn () => 
22528  157 
let 
158 
val r = next (!seed_ref) 

159 
in 

160 
(seed_ref := r; r) 

24043  161 
end); 
22528  162 
end; 
163 

164 
fun value h s = 

165 
if h < 1 then raise RANDOM 

166 
else (s mod (h  1), seed ()); 

167 

168 
end; 

169 
*} 

170 

24226  171 
code_reserved SML Random 
172 

22528  173 
code_type randseed 
174 
(SML "Random.seed") 

24226  175 
types_code randseed ("Random.seed") 
22528  176 

177 
code_const random_int 

178 
(SML "Random.value") 

24226  179 
consts_code random_int ("Random.value") 
22528  180 

181 
code_const run_random 

24226  182 
(SML "case (Random.seed ()) of (x, '_) => _ x") 
183 
consts_code run_random ("case (Random.seed ()) of (x, '_) => _ x") 

22528  184 

185 
end 