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