author  haftmann 
Mon, 18 Dec 2006 08:21:32 +0100  
changeset 21876  96a601bc59d8 
parent 21545  54cc492d80a9 
child 21912  ff45788e7bf9 
permissions  rwrr 
20400  1 
(* ID: $Id$ 
2 
Author: Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A simple random engine *} 

6 

7 
theory CodeRandom 

21192  8 
imports State_Monad 
20400  9 
begin 
10 

11 
section {* A simple random engine *} 

12 

13 
consts 

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

15 

16 
primrec 

17 
"pick (x#xs) n = (let (k, v) = x in 

18 
if n < k then v else pick xs (n  k))" 

19 

20 
lemma pick_def [code, simp]: 

21 
"pick ((k, v)#xs) n = (if n < k then v else pick xs (n  k))" by simp 

22 
declare pick.simps [simp del, code del] 

23 

24 
typedecl randseed 

25 

21113  26 
axiomatization 
20400  27 
random_shift :: "randseed \<Rightarrow> randseed" 
21113  28 

29 
axiomatization 

20400  30 
random_seed :: "randseed \<Rightarrow> nat" 
31 

32 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21192
diff
changeset

33 
random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed" where 
20400  34 
"random n s = (random_seed s mod n, random_shift s)" 
35 

36 
lemma random_bound: 

37 
assumes "0 < n" 

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

39 
proof  

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

41 
then show ?thesis unfolding random_def by simp 

42 
qed 

43 

44 
lemma random_random_seed [simp]: 

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

46 

47 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21192
diff
changeset

48 
select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where 
21192  49 
[simp]: "select xs = (do 
50 
n \<leftarrow> random (length xs); 

51 
return (nth xs n) 

52 
done)" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21192
diff
changeset

53 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21192
diff
changeset

54 
select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed" where 
21192  55 
[simp]: "select_weight xs = (do 
56 
n \<leftarrow> random (foldl (op +) 0 (map fst xs)); 

57 
return (pick xs n) 

58 
done)" 

20400  59 

60 
lemma 

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

62 
proof (induct xs) 

21192  63 
case Nil show ?case by (simp add: monad_collapse random_def) 
20400  64 
next 
65 
have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y" 

66 
proof  

67 
fix xs 

68 
fix y 

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

70 
by (induct xs) simp_all 

71 
qed 

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

73 
proof  

74 
fix xs 

75 
fix n 

76 
assume "n < length xs" 

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

20503  78 
proof (induct xs arbitrary: n) 
20400  79 
case Nil then show ?case by simp 
80 
next 

81 
case (Cons x xs) show ?case 

82 
proof (cases n) 

83 
case 0 then show ?thesis by simp 

84 
next 

85 
case (Suc _) 

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

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

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

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

90 
with Suc show ?thesis by auto 

91 
qed 

92 
qed 

93 
qed 

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

95 
proof  

96 
have replicate_append: 

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

98 
by (simp add: replicate_app_Cons_same) 

99 
fix xs 

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

101 
unfolding map_fst_Pair proof (induct xs) 

102 
case Nil show ?case by simp 

103 
next 

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

105 
qed 

106 
qed 

107 
have pick_nth_random: 

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

109 
proof  

110 
fix s 

111 
fix x 

112 
fix xs 

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

114 
from pick_nth [OF bound] show 

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

116 
qed 

21192  117 
have pick_nth_random_do: 
118 
"!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s = 

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

120 
unfolding monad_collapse split_def unfolding pick_nth_random .. 

20400  121 
case (Cons x xs) then show ?case 
21192  122 
unfolding select_weight_def sum_length pick_nth_random_do 
123 
by simp 

20400  124 
qed 
125 

126 
definition 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21192
diff
changeset

127 
random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed" where 
21192  128 
"random_int k = (do n \<leftarrow> random (nat k); return (int n) done)" 
20400  129 

130 
lemma random_nat [code]: 

21192  131 
"random n = (do k \<leftarrow> random_int (int n); return (nat k) done)" 
132 
unfolding random_int_def by simp 

20400  133 

21113  134 
axiomatization 
135 
run_random :: "(randseed \<Rightarrow> 'a * randseed) \<Rightarrow> 'a" 

136 

20400  137 
ML {* 
138 
signature RANDOM = 

139 
sig 

140 
type seed = IntInf.int; 

141 
val seed: unit > seed; 

142 
val value: IntInf.int > seed > IntInf.int * seed; 

143 
end; 

144 

145 
structure Random : RANDOM = 

146 
struct 

147 

20406  148 
open IntInf; 
149 

20400  150 
exception RANDOM; 
151 

20406  152 
type seed = int; 
20400  153 

154 
local 

20406  155 
val a = fromInt 16807; 
156 
(*greetings to SML/NJ*) 

157 
val m = (the o fromString) "2147483647"; 

20400  158 
in 
20406  159 
fun next s = (a * s) mod m; 
20400  160 
end; 
161 

162 
local 

20406  163 
val seed_ref = ref (fromInt 1); 
20400  164 
in 
165 
fun seed () = 

166 
let 

167 
val r = next (!seed_ref) 

168 
in 

169 
(seed_ref := r; r) 

170 
end; 

171 
end; 

172 

173 
fun value h s = 

174 
if h < 1 then raise RANDOM 

20406  175 
else (s mod (h  1), seed ()); 
20400  176 

177 
end; 

178 
*} 

179 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20406
diff
changeset

180 
code_type randseed 
21113  181 
(SML "Random.seed") 
20400  182 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20406
diff
changeset

183 
code_const random_int 
21113  184 
(SML "Random.value") 
185 

186 
code_const run_random 

187 
(SML "case _ (Random.seed ()) of (x, '_) => x") 

20400  188 

20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20406
diff
changeset

189 
code_gen select select_weight 
21545  190 
(SML #) 
20400  191 

192 
end 