1open HolKernel Parse boolLib bossLib; 2open arithmeticTheory numTheory sequenceTheory 3 sequenceTools hurdUtils combinTheory; 4 5val _ = new_theory "prob_pseudo"; 6 7(* ------------------------------------------------------------------------- *) 8(* The definition of the pseudo-random number generator. *) 9(* ------------------------------------------------------------------------- *) 10 11val prob_pseudo_def = Define 12 `prob_pseudo a b n = siter EVEN (\x. (a * x + b) MOD (2 * n + 1))`; 13 14(* ------------------------------------------------------------------------- *) 15(* Theorems to allow pseudo-random bits to be computed. *) 16(* ------------------------------------------------------------------------- *) 17 18val SHD_PROB_PSEUDO = store_thm 19 ("SHD_PROB_PSEUDO", 20 ``!a b n x. shd (prob_pseudo a b n x) = EVEN x``, 21 RW_TAC std_ss [prob_pseudo_def, SHD_SITER]); 22 23val STL_PROB_PSEUDO = store_thm 24 ("STL_PROB_PSEUDO", 25 ``!a b n x. 26 stl (prob_pseudo a b n x) = 27 prob_pseudo a b n ((a * x + b) MOD (2 * n + 1))``, 28 RW_TAC std_ss [prob_pseudo_def, STL_SITER]); 29 30val _ = export_theory (); 31