Theory: probUniform

Parents

• probIndep

Types

Constants

• uniform_tupled  :num # num # (num -> bool) -> num # (num -> bool)
• unif_tupled  :num # (num -> bool) -> num # (num -> bool)
• unif  :num -> (num -> bool) -> num # (num -> bool)
• unif_bound  :num -> num
• uniform  :num -> num -> (num -> bool) -> num # (num -> bool)

Definitions

unif_arg_munge_def

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

unif_bound_primitive_def

|- unif_bound =
   WFREC (@R. WF R /\ !v. R (SUC v DIV 2) (SUC v))
     (\unif_bound' a. num_case 0 (\v1. SUC (unif_bound' (SUC v1 DIV 2))) a)

unif_tupled_primitive_def

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

uniform_arg_munge_def

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

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.
        pair_case
          (\v v1.
             num_case (pair_case (\v3 v4. num_case ARB (\v5. (0,v4)) v3) v1)
               (\v2.
                  pair_case
                    (\v7 v8.
                       num_case ARB
                         (\v9.
                            (let (res,s') = unif v9 v8 in
                               (if res < SUC v9 then
                                  (res,s')
                                else
                                  uniform_tupled' (v2,SUC v9,s')))) v7) v1) v)
          a)

Theorems

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)

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)

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_UNIFORM

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

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_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_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)

SUC_DIV_TWO_ZERO

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

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_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

|- (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_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)))

unif_ind

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

UNIF_RANGE

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

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')))

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)))

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_RANGE

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