equal
deleted
inserted
replaced
3 section \<open>A HOL random engine\<close> |
3 section \<open>A HOL random engine\<close> |
4 |
4 |
5 theory Random |
5 theory Random |
6 imports List Groups_List |
6 imports List Groups_List |
7 begin |
7 begin |
8 |
|
9 notation fcomp (infixl "\<circ>>" 60) |
|
10 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
11 |
|
12 |
8 |
13 subsection \<open>Auxiliary functions\<close> |
9 subsection \<open>Auxiliary functions\<close> |
14 |
10 |
15 fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where |
11 fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where |
16 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" |
12 "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))" |
43 w'' = inc_shift 2147483398 w |
39 w'' = inc_shift 2147483398 w |
44 in ((v'', w'), (v', w'')))" |
40 in ((v'', w'), (v', w'')))" |
45 |
41 |
46 |
42 |
47 subsection \<open>Base selectors\<close> |
43 subsection \<open>Base selectors\<close> |
|
44 |
|
45 context |
|
46 includes state_combinator_syntax |
|
47 begin |
48 |
48 |
49 fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |
49 fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where |
50 "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)" |
50 "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)" |
51 |
51 |
52 definition range :: "natural \<Rightarrow> seed \<Rightarrow> natural \<times> seed" where |
52 definition range :: "natural \<Rightarrow> seed \<Rightarrow> natural \<times> seed" where |
132 ultimately show ?thesis |
132 ultimately show ?thesis |
133 by (auto simp add: select_weight_def select_def scomp_def split_def |
133 by (auto simp add: select_weight_def select_def scomp_def split_def |
134 fun_eq_iff pick_same [symmetric] less_natural_def) |
134 fun_eq_iff pick_same [symmetric] less_natural_def) |
135 qed |
135 qed |
136 |
136 |
|
137 end |
|
138 |
137 |
139 |
138 subsection \<open>\<open>ML\<close> interface\<close> |
140 subsection \<open>\<open>ML\<close> interface\<close> |
139 |
141 |
140 code_reflect Random_Engine |
142 code_reflect Random_Engine |
141 functions range select select_weight |
143 functions range select select_weight |
181 hide_type (open) seed |
183 hide_type (open) seed |
182 hide_const (open) inc_shift minus_shift log "next" split_seed |
184 hide_const (open) inc_shift minus_shift log "next" split_seed |
183 iterate range select pick select_weight |
185 iterate range select pick select_weight |
184 hide_fact (open) range_def |
186 hide_fact (open) range_def |
185 |
187 |
186 no_notation fcomp (infixl "\<circ>>" 60) |
|
187 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
188 |
|
189 end |
188 end |