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