Theory "prob_uniform"

Signature

Definitions

unif_bound_primitive_def

|- unif_bound =
   WFREC (@R. WF R /\ !v. R (SUC v DIV 2) (SUC v))
     (\unif_bound a.
        case a of 0 -> I 0 || SUC v1 -> I (SUC (unif_bound (SUC v1 DIV 2))))

unif_tupled_primitive_def

|- unif_tupled =
   WFREC (@R. WF R /\ !s v2. R (SUC v2 DIV 2,s) (SUC v2,s))
     (\unif_tupled a.
        case a of
           (0,s) -> I (0,s)
        || (SUC v3,s) ->
             I
               (let (m,s') = unif_tupled (SUC v3 DIV 2,s) in
                  ((if SHD s' then 2 * m + 1 else 2 * m),STL s')))

unif_curried_def

|- !x x1. unif x x1 = unif_tupled (x,x1)

uniform_tupled_primitive_def

|- uniform_tupled =
   WFREC
     (@R.
        WF R /\
        !t s n res s'.
          ((res,s') = unif n s) /\ ~(res < SUC n) ==>
          R (t,SUC n,s') (SUC t,SUC n,s))
     (\uniform_tupled a.
        case a of
           (0,0,s) -> ARB
        || (0,SUC n,s) -> I (0,s)
        || (SUC t,0,s') -> ARB
        || (SUC t,SUC n',s') ->
             I
               (let (res,s') = unif n' s' in
                  (if res < SUC n' then
                     (res,s')
                   else
                     uniform_tupled (t,SUC n',s'))))

uniform_curried_def

|- !x x1 x2. uniform x x1 x2 = uniform_tupled (x,x1,x2)

Theorems

unif_bound_def

|- (unif_bound 0 = 0) /\ (unif_bound (SUC v) = SUC (unif_bound (SUC v DIV 2)))

unif_bound_ind

|- !P. P 0 /\ (!v. P (SUC v DIV 2) ==> P (SUC v)) ==> !v. P v

unif_def

|- (unif 0 s = (0,s)) /\
   (unif (SUC v2) s =
    (let (m,s') = unif (SUC v2 DIV 2) s in
       ((if SHD s' then 2 * m + 1 else 2 * m),STL s')))

unif_ind

|- !P.
     (!s. P 0 s) /\ (!v2 s. P (SUC v2 DIV 2) s ==> P (SUC v2) s) ==>
     !v v1. P v v1

uniform_ind

|- !P.
     (!t v10. P (SUC t) 0 v10) /\ (!v6. P 0 0 v6) /\ (!n s. P 0 (SUC n) s) /\
     (!t n s.
        (!res s'.
           ((res,s') = unif n s) /\ ~(res < SUC n) ==> P t (SUC n) s') ==>
        P (SUC t) (SUC n) s) ==>
     !v v1 v2. P v v1 v2

uniform_def

|- (uniform 0 (SUC n) s = (0,s)) /\
   (uniform (SUC t) (SUC n) s =
    (let (res,s') = unif n s in
       (if res < SUC n then (res,s') else uniform t (SUC n) s')))

SUC_DIV_TWO_ZERO

|- !n. (SUC n DIV 2 = 0) = (n = 0)

UNIF_BOUND_LOWER

|- !n. n < 2 ** unif_bound n

UNIF_BOUND_LOWER_SUC

|- !n. SUC n <= 2 ** unif_bound n

UNIF_BOUND_UPPER

|- !n. ~(n = 0) ==> 2 ** unif_bound n <= 2 * n

UNIF_BOUND_UPPER_SUC

|- !n. 2 ** unif_bound n <= SUC (2 * n)

UNIF_DEF_MONAD

|- (unif 0 = UNIT 0) /\
   !n.
     unif (SUC n) =
     BIND (unif (SUC n DIV 2))
       (\m. BIND SDEST (\b. UNIT (if b then 2 * m + 1 else 2 * m)))

UNIFORM_DEF_MONAD

|- (!n. uniform 0 (SUC n) = UNIT 0) /\
   !t n.
     uniform (SUC t) (SUC n) =
     BIND (unif n) (\m. (if m < SUC n then UNIT m else uniform t (SUC n)))

INDEP_UNIF

|- !n. indep (unif n)

INDEP_UNIFORM

|- !t n. indep (uniform t (SUC n))

PROB_UNIF

|- !n k.
     prob (\s. FST (unif n s) = k) =
     (if k < 2 ** unif_bound n then (1 / 2) pow unif_bound n else 0)

UNIF_RANGE

|- !n s. FST (unif n s) < 2 ** unif_bound n

PROB_UNIF_PAIR

|- !n k k'.
     (prob (\s. FST (unif n s) = k) = prob (\s. FST (unif n s) = k')) =
     (k < 2 ** unif_bound n = k' < 2 ** unif_bound n)

PROB_UNIF_BOUND

|- !n k.
     k <= 2 ** unif_bound n ==>
     (prob (\s. FST (unif n s) < k) = & k * (1 / 2) pow unif_bound n)

PROB_UNIF_GOOD

|- !n. 1 / 2 <= prob (\s. FST (unif n s) < SUC n)

UNIFORM_RANGE

|- !t n s. FST (uniform t (SUC n) s) < SUC n

PROB_UNIFORM_LOWER_BOUND

|- !b.
     (!k. k < SUC n ==> prob (\s. FST (uniform t (SUC n) s) = k) < b) ==>
     !m.
       m < SUC n ==>
       prob (\s. FST (uniform t (SUC n) s) < SUC m) < & (SUC m) * b

PROB_UNIFORM_UPPER_BOUND

|- !b.
     (!k. k < SUC n ==> b < prob (\s. FST (uniform t (SUC n) s) = k)) ==>
     !m.
       m < SUC n ==>
       & (SUC m) * b < prob (\s. FST (uniform t (SUC n) s) < SUC m)

PROB_UNIFORM_PAIR_SUC

|- !t n k k'.
     k < SUC n /\ k' < SUC n ==>
     abs
       (prob (\s. FST (uniform t (SUC n) s) = k) -
        prob (\s. FST (uniform t (SUC n) s) = k')) <= (1 / 2) pow t

PROB_UNIFORM_SUC

|- !t n k.
     k < SUC n ==>
     abs (prob (\s. FST (uniform t (SUC n) s) = k) - 1 / & (SUC n)) <=
     (1 / 2) pow t

PROB_UNIFORM

|- !t n k.
     k < n ==>
     abs (prob (\s. FST (uniform t n s) = k) - 1 / & n) <= (1 / 2) pow t