1(* ------------------------------------------------------------------------- *)
2(* Coversions for evaluating the pseudo-random number generator.             *)
3(* ------------------------------------------------------------------------- *)
4
5structure prob_pseudoTools :> prob_pseudoTools =
6struct
7
8open HolKernel Parse boolLib reduceLib prob_pseudoTheory;
9
10infix THENC;
11
12val PROB_PSEUDO_SHD_CONV = REWR_CONV SHD_PROB_PSEUDO THENC REDUCE_CONV;
13
14val PROB_PSEUDO_STL_CONV =
15  REWR_CONV STL_PROB_PSEUDO THENC RAND_CONV REDUCE_CONV;
16
17(* Simple ML functions to help find good parameters for the linear
18   congruence pseudo-random bit generator.
19
20fun iterate f 0 x = []
21  | iterate f n x = x::(iterate f (n - 1) (f x));
22
23fun linear a b n x = (a * x + b) mod (2 * n + 1);
24
25val linear1 = linear 103 95 79;
26iterate linear1 200 0;
27*)
28
29end;
30