1(* interactive mode 2loadPath := ["../ho_prover","../subtypes","../formalize"] @ !loadPath; 3app load 4 ["bossLib","realLib","ho_proverTools","extra_pred_setTools", 5 "sequenceTools","prob_canonTools","prob_algebraTheory","probTheory"]; 6quietdec := true; 7*) 8 9open HolKernel Parse boolLib bossLib; 10 11open arithmeticTheory pred_setTheory 12 listTheory sequenceTheory state_transformerTheory 13 HurdUseful extra_numTheory combinTheory 14 pairTheory realTheory realLib extra_boolTheory 15 extra_pred_setTheory extra_realTheory extra_pred_setTools numTheory 16 simpLib; 17 18open util_probTheory measureTheory probabilityTheory; 19open prob_algebraTheory probTheory; 20 21(* interactive mode 22quietdec := false; 23*) 24 25val _ = new_theory "prob_uniform"; 26 27val std_ss' = std_ss ++ boolSimps.ETA_ss; 28val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 29val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 30val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC; 31val Cond = 32 DISCH_THEN 33 (fn mp_th => 34 let 35 val cond = fst (dest_imp (concl mp_th)) 36 in 37 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 38 end); 39 40(* ------------------------------------------------------------------------- *) 41(* The definition of the uniform random number generator. *) 42(* ------------------------------------------------------------------------- *) 43 44val (prob_unif_def, prob_unif_ind) = Defn.tprove 45 let val d = Hol_defn "prob_unif" 46 `(prob_unif 0 s = (0:num, s)) 47 /\ (prob_unif n s = let (m, s') = prob_unif (n DIV 2) s 48 in (if shd s' then 2 * m + 1 else 2 * m, stl s'))` 49 val g = `measure (\(x,y). x)` 50 in (d, WF_REL_TAC g >> STRIP_TAC) 51 end; 52 53val _ = save_thm ("prob_unif_def", prob_unif_def); 54val _ = save_thm ("prob_unif_ind", prob_unif_ind); 55 56val prob_uniform_cut_def = Define 57 `(prob_uniform_cut 0 (SUC n) s = (0, s)) /\ 58 (prob_uniform_cut (SUC t) (SUC n) s = 59 let (res, s') = prob_unif n s 60 in if res < SUC n then (res, s') else prob_uniform_cut t (SUC n) s')`; 61 62val prob_uniform_def = Define 63 `prob_uniform (SUC n) = prob_until (prob_unif n) (\x. x < SUC n)`; 64 65(* ------------------------------------------------------------------------- *) 66(* Theorems leading to: *) 67(* k < n ==> *) 68(* abs (prob (\s. FST (prob_uniform_cut t n s) = k) - 1 / & n) <= *) 69(* (1 / 2) pow t *) 70(* ------------------------------------------------------------------------- *) 71 72val PROB_UNIF_MONAD = store_thm 73 ("PROB_UNIF_MONAD", 74 ``(prob_unif 0 = UNIT 0) /\ 75 (!n. 76 prob_unif (SUC n) = 77 BIND (prob_unif (SUC n DIV 2)) 78 (\m. BIND sdest (\b. UNIT (if b then 2 * m + 1 else 2 * m))))``, 79 FUN_EQ_TAC 80 >> RW_TAC arith_ss [BIND_DEF, UNIT_DEF, o_THM, prob_unif_def, sdest_def, 81 LET_DEF, UNCURRY, FST, SND]); 82 83val PROB_UNIFORM_CUT_MONAD = store_thm 84 ("PROB_UNIFORM_CUT_MONAD", 85 ``(!n. prob_uniform_cut 0 (SUC n) = UNIT 0) /\ 86 (!t n. 87 prob_uniform_cut (SUC t) (SUC n) = 88 BIND (prob_unif n) 89 (\m. if m < SUC n then UNIT m else prob_uniform_cut t (SUC n)))``, 90 FUN_EQ_TAC 91 >> RW_TAC std_ss [BIND_DEF, UNIT_DEF, o_DEF, prob_uniform_cut_def, 92 sdest_def, LET_DEF, UNCURRY]); 93 94val INDEP_FN_PROB_UNIF = store_thm 95 ("INDEP_FN_PROB_UNIF", 96 ``!n. prob_unif n IN indep_fn``, 97 recInduct log2_ind 98 >> RW_TAC std_ss [PROB_UNIF_MONAD, INDEP_FN_UNIT] 99 >> MATCH_MP_TAC INDEP_FN_BIND 100 >> RW_TAC std_ss [] 101 >> MATCH_MP_TAC INDEP_FN_BIND 102 >> RW_TAC std_ss [INDEP_FN_UNIT, INDEP_FN_SDEST]); 103 104val INDEP_FN_PROB_UNIFORM_CUT = store_thm 105 ("INDEP_FN_PROB_UNIFORM_CUT", 106 ``!t n. prob_uniform_cut t (SUC n) IN indep_fn``, 107 Induct >- RW_TAC std_ss [PROB_UNIFORM_CUT_MONAD, INDEP_FN_UNIT] 108 >> RW_TAC std_ss [PROB_UNIFORM_CUT_MONAD] 109 >> MATCH_MP_TAC INDEP_FN_BIND 110 >> RW_TAC std_ss [INDEP_FN_PROB_UNIF, INDEP_FN_UNIT]); 111 112val PROB_BERN_UNIF = store_thm 113 ("PROB_BERN_UNIF", 114 ``!n k. 115 prob bern {s | FST (prob_unif n s) = k} = 116 if k < 2 EXP log2 n then (1 / 2) pow log2 n else 0``, 117 recInduct log2_ind 118 >> REPEAT STRIP_TAC 119 >- (Know `(0 = k) = k < 1` >- DECIDE_TAC 120 >> RW_TAC std_ss [prob_unif_def, log2_def, EXP, pow, GEMPTY, GUNIV, 121 PROB_BERN_BASIC]) 122 >> Suff 123 `prob bern {s | FST (prob_unif (SUC v) s) = k} = 124 (1 / 2) * prob bern {s | FST (prob_unif (SUC v DIV 2) s) = k DIV 2}` 125 >- (STRIP_TAC 126 >> ASM_REWRITE_TAC [] 127 >> KILL_TAC 128 >> RW_TAC std_ss [log2_def, pow, DIV_TWO_EXP] 129 >> RW_TAC real_ss []) 130 >> KILL_TAC 131 >> RW_TAC bool_ss [prob_unif_def] 132 >> Know 133 `!s. 134 prob_unif (SUC v DIV 2) s = 135 (FST (prob_unif (SUC v DIV 2) s), SND (prob_unif (SUC v DIV 2) s))` 136 >- RW_TAC bool_ss [PAIR] 137 >> Rewr' 138 >> RW_TAC bool_ss [] 139 >> (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [EQ_SYM_EQ] 140 >> RW_TAC bool_ss [COND_RAND, COND_EXPAND] 141 >> (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [EQ_SYM_EQ] 142 >> RW_TAC bool_ss [LEFT_AND_OVER_OR, RIGHT_AND_OVER_OR] 143 >> Know `!x. ~x /\ x = F` >- PROVE_TAC [] 144 >> Rewr 145 >> Know `!m n : num. (m + 1 = n) /\ (m = n) = F` >- DECIDE_TAC 146 >> Rewr 147 >> RW_TAC bool_ss [] 148 >> MP_TAC (Q.SPEC `k` EVEN_ODD_EXISTS_EQ) 149 >> MP_TAC (Q.SPEC `k` EVEN_OR_ODD) 150 >> (STRIP_TAC >> RW_TAC bool_ss [] >> RW_TAC bool_ss [DIV_TWO_CANCEL]) >| 151 [Know `!k. ~(2 * k + 1 = 2 * m)` 152 >- (STRIP_TAC 153 >> Suff `~(SUC (2 * k) = 2 * m)` >- DECIDE_TAC 154 >> PROVE_TAC [EVEN_DOUBLE, ODD_DOUBLE, EVEN_ODD]) 155 >> Rewr 156 >> Know `!a b : num. (2 * a = 2 * b) = (a = b)` >- DECIDE_TAC 157 >> Rewr 158 >> KILL_TAC 159 >> Q.SPEC_TAC (`SUC v DIV 2`, `n`) 160 >> STRIP_TAC 161 >> Suff 162 `prob bern 163 (($= m o FST o prob_unif n) INTER halfspace F o SND o prob_unif n) = 164 1 / 2 * prob bern {s | FST (prob_unif n s) = m}` 165 >- (DISCH_THEN (MP_TAC o SYM) 166 >> Rewr 167 >> RW_TAC std_ss [] 168 >> AP_TERM_TAC 169 >> ONCE_REWRITE_TAC [EXTENSION] 170 >> RW_TAC bool_ss [IN_INTER, IN_o, IN_HALFSPACE, o_THM, GSPECIFICATION] 171 >> RW_TAC std_ss [SPECIFICATION] 172 >> METIS_TAC [PAIR, FST, SND]) 173 >> MP_TAC (Q.SPECL [`prob_unif n`, `$= m`, `halfspace F`] 174 (INST_TYPE [alpha |-> numSyntax.num] INDEP_FN_PROB)) 175 >> RW_TAC bool_ss [INDEP_FN_PROB_UNIF, EVENTS_BERN_BASIC, PROB_BERN_BASIC] 176 >> RW_TAC real_ss [] 177 >> KILL_TAC 178 >> Suff `$= m o FST o prob_unif n = {s | FST (prob_unif n s) = m}` 179 >- METIS_TAC [REAL_MUL_COMM] 180 >> SET_EQ_TAC 181 >> RW_TAC std_ss [GSPECIFICATION] 182 >> RW_TAC std_ss [SPECIFICATION, o_THM] 183 >> PROVE_TAC [], 184 Know `!k. ~(2 * k = SUC (2 * m))` 185 >- PROVE_TAC [EVEN_DOUBLE, ODD_DOUBLE, EVEN_ODD] 186 >> Rewr 187 >> Know `!a b. (2 * a + 1 = SUC (2 * b)) = (a = b)` >- DECIDE_TAC 188 >> Rewr 189 >> KILL_TAC 190 >> Q.SPEC_TAC (`SUC v DIV 2`, `n`) 191 >> STRIP_TAC 192 >> Suff 193 `prob bern 194 (($= m o FST o prob_unif n) INTER halfspace T o SND o prob_unif n) = 195 1 / 2 * prob bern {s | FST (prob_unif n s) = m}` 196 >- (DISCH_THEN (MP_TAC o SYM) 197 >> Rewr 198 >> RW_TAC std_ss [] 199 >> AP_TERM_TAC 200 >> ONCE_REWRITE_TAC [EXTENSION] 201 >> RW_TAC bool_ss [IN_INTER, IN_o, IN_HALFSPACE, o_THM, GSPECIFICATION] 202 >> RW_TAC std_ss [SPECIFICATION] 203 >> METIS_TAC [PAIR, FST, SND]) 204 >> MP_TAC (Q.SPECL [`prob_unif n`, `$= m`, `halfspace T`] 205 (INST_TYPE [alpha |-> numSyntax.num] INDEP_FN_PROB)) 206 >> RW_TAC std_ss [INDEP_FN_PROB_UNIF, EVENTS_BERN_BASIC, PROB_BERN_BASIC] 207 >> RW_TAC real_ss [] 208 >> KILL_TAC 209 >> Suff `$= m o FST o prob_unif n = {s | FST (prob_unif n s) = m}` 210 >- METIS_TAC [REAL_MUL_COMM] 211 >> SET_EQ_TAC 212 >> RW_TAC std_ss [GSPECIFICATION] 213 >> RW_TAC std_ss [SPECIFICATION, o_THM] 214 >> PROVE_TAC []]); 215 216val PROB_UNIF_RANGE = store_thm 217 ("PROB_UNIF_RANGE", 218 ``!n s. FST (prob_unif n s) < 2 EXP log2 n``, 219 recInduct log2_ind 220 >> RW_TAC arith_ss [prob_unif_def, log2_def, EXP] 221 >> Q.PAT_X_ASSUM `!s. P s` (MP_TAC o Q.SPEC `s`) 222 >> RW_TAC arith_ss []); 223 224val PROB_BERN_UNIF_PAIR = store_thm 225 ("PROB_BERN_UNIF_PAIR", 226 ``!n k k'. 227 (prob bern {s | FST (prob_unif n s) = k} = 228 prob bern {s | FST (prob_unif n s) = k'}) = 229 (k < 2 EXP log2 n = k' < 2 EXP log2 n)``, 230 RW_TAC std_ss [PROB_BERN_UNIF] 231 >> PROVE_TAC [POW_HALF_POS, REAL_LT_LE]); 232 233val PROB_BERN_UNIF_LT = store_thm 234 ("PROB_BERN_UNIF_LT", 235 ``!n k. 236 k <= 2 EXP log2 n ==> 237 (prob bern {s | FST (prob_unif n s) < k} = &k * (1 / 2) pow log2 n)``, 238 STRIP_TAC 239 >> Induct 240 >- (RW_TAC arith_ss [GEMPTY, PROB_BERN_BASIC] 241 >> RW_TAC real_ss []) 242 >> RW_TAC std_ss [] 243 >> Q.PAT_X_ASSUM `X ==> Y` MP_TAC 244 >> Cond >- RW_TAC arith_ss [] 245 >> RW_TAC std_ss' [INDEP_FN_PROB_FST_SUC, INDEP_FN_PROB_UNIF] 246 >> Know `k < 2 EXP log2 n` >- DECIDE_TAC 247 >> POP_ASSUM (fn th => RW_TAC std_ss [th, o_DEF, PROB_BERN_UNIF]) 248 >> RW_TAC bool_ss [ADD1, REAL_ADD_RDISTRIB, GSYM REAL_ADD] 249 >> RW_TAC real_ss []); 250 251val PROB_BERN_UNIF_GOOD = store_thm 252 ("PROB_BERN_UNIF_GOOD", 253 ``!n. 1 / 2 <= prob bern {s | FST (prob_unif n s) < SUC n}``, 254 RW_TAC std_ss [] 255 >> MP_TAC (Q.SPECL [`n`, `SUC n`] PROB_BERN_UNIF_LT) 256 >> RW_TAC std_ss [LOG2_LOWER_SUC] 257 >> KILL_TAC 258 >> ONCE_REWRITE_TAC [GSYM REAL_INVINV_ALL] 259 >> MATCH_MP_TAC REAL_LE_INV_LE 260 >> Know `~(&(SUC n) = (0 :real)) /\ ~(((1 :real) / 2) pow log2 n = 0)` 261 >- PROVE_TAC [POW_HALF_POS, REAL_INJ, REAL_LT_LE, NOT_SUC] 262 >> RW_TAC std_ss [REAL_INV_MUL] 263 >- (MATCH_MP_TAC REAL_LT_MUL 264 >> CONJ_TAC >- PROVE_TAC [INV_SUC_POS, REAL_INV_1OVER] 265 >> PROVE_TAC [POW_HALF_POS, REAL_INV_POS]) 266 >> RW_TAC std_ss [POW_HALF_EXP, REAL_INVINV_ALL, GSYM REAL_INV_1OVER] 267 >> Know 268 `!x y : real. (0:real) < &(SUC n) /\ &(SUC n) * x <= &(SUC n) * y ==> x <= y` 269 >- PROVE_TAC [REAL_LE_LMUL] 270 >> DISCH_THEN MATCH_MP_TAC 271 >> RW_TAC arith_ss [REAL_LT, REAL_MUL_RINV, REAL_MUL_ASSOC, REAL_MUL_LID] 272 >> RW_TAC std_ss [REAL_LE, REAL_MUL] 273 >> Suff `SUC (2 * n) <= SUC n * 2` 274 >- PROVE_TAC [LOG2_UPPER_SUC, LESS_EQ_TRANS] 275 >> DECIDE_TAC); 276 277val PROB_UNIFORM_CUT_RANGE = store_thm 278 ("PROB_UNIFORM_CUT_RANGE", 279 ``!t n s. FST (prob_uniform_cut t (SUC n) s) < SUC n``, 280 Induct >- RW_TAC arith_ss [prob_uniform_cut_def] 281 >> RW_TAC arith_ss [prob_uniform_cut_def] 282 >> Cases_on `prob_unif n s` 283 >> RW_TAC arith_ss []); 284 285val PROB_BERN_UNIFORM_CUT_LOWER_BOUND = store_thm 286 ("PROB_BERN_UNIFORM_CUT_LOWER_BOUND", 287 ``!b. 288 (!k. 289 k < SUC n ==> 290 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k} < b) ==> 291 !m. 292 m < SUC n ==> 293 prob bern 294 {s | FST (prob_uniform_cut t (SUC n) s) < SUC m} < &(SUC m) * b``, 295 NTAC 2 STRIP_TAC 296 >> Induct 297 >- (RW_TAC arith_ss [] 298 >> POP_ASSUM (MP_TAC o Q.SPEC `0`) 299 >> Know `!m : num. m < 1 = (m = 0)` >- DECIDE_TAC 300 >> Know `!n. 0 < SUC n` >- DECIDE_TAC 301 >> RW_TAC std_ss [GSYM ONE] 302 >> RW_TAC real_ss []) 303 >> RW_TAC arith_ss [] 304 >> ASSUME_TAC (Q.SPECL [`t`, `n`] INDEP_FN_PROB_UNIFORM_CUT) 305 >> Q.PAT_X_ASSUM `X ==> Y` MP_TAC 306 >> RW_TAC arith_ss [] 307 >> MP_TAC 308 (Q.SPECL [`prob_uniform_cut t (SUC n)`, `SUC m`] INDEP_FN_PROB_FST_SUC) 309 >> ASM_REWRITE_TAC [] 310 >> Rewr 311 >> Know `&(SUC (SUC m)) = &(SUC m) + (1 :real)` 312 >- (RW_TAC arith_ss [REAL_ADD, REAL_INJ] 313 >> DECIDE_TAC) 314 >> Rewr 315 >> RW_TAC std_ss [REAL_ADD_RDISTRIB] 316 >> MATCH_MP_TAC REAL_LT_ADD2 317 >> RW_TAC real_ss []); 318 319val PROB_BERN_UNIFORM_CUT_UPPER_BOUND = store_thm 320 ("PROB_BERN_UNIFORM_CUT_UPPER_BOUND", 321 ``!b. 322 (!k. 323 k < SUC n ==> 324 b < prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k}) ==> 325 (!m. 326 m < SUC n ==> 327 &(SUC m) * b < 328 prob bern {s | FST (prob_uniform_cut t (SUC n) s) < SUC m})``, 329 NTAC 2 STRIP_TAC 330 >> Induct 331 >- (RW_TAC arith_ss [] 332 >> POP_ASSUM (MP_TAC o Q.SPEC `0`) 333 >> Know `!m. m < SUC 0 = (m = 0)` >- DECIDE_TAC 334 >> STRIP_TAC 335 >> RW_TAC real_ss [DECIDE ``(x:num) < 1 = (x = 0)``]) 336 >> RW_TAC arith_ss [] 337 >> ASSUME_TAC (Q.SPECL [`t`, `n`] INDEP_FN_PROB_UNIFORM_CUT) 338 >> Q.PAT_X_ASSUM `X ==> Y` MP_TAC 339 >> RW_TAC arith_ss [] 340 >> MP_TAC (Q.SPECL [`prob_uniform_cut t (SUC n)`, `SUC m`] 341 INDEP_FN_PROB_FST_SUC) 342 >> ASM_REWRITE_TAC [] 343 >> RW_TAC std_ss [] 344 >> Know `&(SUC (SUC m)) = &(SUC m) + (1 :real)` 345 >- (RW_TAC arith_ss [REAL_ADD,REAL_INJ] >> DECIDE_TAC) 346 >> RW_TAC std_ss [REAL_ADD_RDISTRIB] 347 >> MATCH_MP_TAC REAL_LT_ADD2 348 >> RW_TAC real_ss []); 349 350val PROB_BERN_UNIFORM_CUT_PAIR = store_thm 351 ("PROB_BERN_UNIFORM_CUT_PAIR", 352 ``!t n k k'. 353 k < SUC n /\ k' < SUC n ==> 354 abs 355 (prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k} - 356 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k'}) <= 357 (1 / 2) pow t``, 358 RW_TAC std_ss [] 359 >> Induct_on `t` 360 >- (RW_TAC bool_ss [prob_uniform_cut_def, pow] 361 >> MATCH_MP_TAC ABS_UNIT_INTERVAL 362 >> Cases_on `k` 363 >> Cases_on `k'` 364 >> RW_TAC std_ss [GEMPTY, GUNIV, PROB_BERN_BASIC] 365 >> REAL_ARITH_TAC) 366 >> RW_TAC std_ss [prob_uniform_cut_def, LET_DEF] 367 >> Know `!s. prob_unif n s = (FST (prob_unif n s), SND (prob_unif n s))` 368 >- RW_TAC std_ss [PAIR] 369 >> Rewr' 370 >> (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [EQ_SYM_EQ] 371 >> RW_TAC std_ss [COND_RAND, COND_EXPAND] 372 >> (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV) [EQ_SYM_EQ] 373 >> RW_TAC std_ss [LEFT_AND_OVER_OR, RIGHT_AND_OVER_OR] 374 >> Know `!x. ~x /\ x = F` >- PROVE_TAC [] 375 >> Rewr 376 >> Know `!m. (m = k) /\ (m < SUC n) = (m = k)` >- DECIDE_TAC 377 >> Know `!m. (m = k') /\ (m < SUC n) = (m = k')` >- RW_TAC arith_ss [] 378 >> Know `!x y. x \/ (x /\ y) = x` >- PROVE_TAC [] 379 >> RW_TAC std_ss [] 380 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 381 >> Know 382 `{s | 383 ~(FST (prob_unif n s) < SUC n) /\ 384 (FST (prob_uniform_cut t (SUC n) (SND (prob_unif n s))) = k) \/ 385 (FST (prob_unif n s) = k)} = 386 (\m. ~(m < SUC n)) o FST o prob_unif n INTER 387 (\m. m = k) o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n UNION 388 (\m. m = k) o FST o prob_unif n` 389 >- (PSET_TAC [o_DEF, EXTENSION] 390 >> RW_TAC std_ss [SPECIFICATION, GSYM EXTENSION]) 391 >> Rewr 392 >> Know 393 `prob bern 394 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 395 (\m. m = k) o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n UNION 396 (\m. m = k) o FST o prob_unif n) = 397 prob bern 398 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 399 (\m. m = k) o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n) + 400 prob bern ((\m. m = k) o FST o prob_unif n)` 401 >- (MATCH_MP_TAC PROB_ADDITIVE 402 >> ASSUME_TAC (Q.SPEC `n` INDEP_FN_PROB_UNIF) 403 >> ASSUME_TAC (Q.SPECL [`t`, `n`] INDEP_FN_PROB_UNIFORM_CUT) 404 >> RW_TAC std_ss [PROB_SPACE_BERN] >| 405 [MATCH_MP_TAC EVENTS_INTER 406 >> RW_TAC bool_ss [INDEP_FN_FST_EVENTS', PROB_SPACE_BERN, 407 INDEP_FN_SND_EVENTS', o_ASSOC], 408 RW_TAC bool_ss [INDEP_FN_FST_EVENTS], 409 RW_TAC bool_ss [IN_DISJOINT, IN_INTER, IN_o, o_THM] 410 >> RW_TAC bool_ss [SPECIFICATION] 411 >> PROVE_TAC []]) 412 >> Rewr 413 >> Know 414 `prob bern 415 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 416 (\m. m = k) o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n) = 417 prob bern ((\m. ~(m < SUC n)) o FST o prob_unif n) * 418 prob bern ((\m. m = k) o FST o prob_uniform_cut t (SUC n))` 419 >- (MP_TAC (Q.ISPEC `prob_unif n` INDEP_FN_PROB) 420 >> MP_TAC (Q.SPEC `n` INDEP_FN_PROB_UNIF) 421 >> RW_TAC bool_ss [o_ASSOC] 422 >> POP_ASSUM MATCH_MP_TAC 423 >> RW_TAC bool_ss [INDEP_FN_FST_EVENTS', INDEP_FN_PROB_UNIFORM_CUT]) 424 >> Rewr 425 >> Know 426 `{s | 427 ~(FST (prob_unif n s) < SUC n) /\ 428 (FST (prob_uniform_cut t (SUC n) (SND (prob_unif n s))) = k') \/ 429 (FST (prob_unif n s) = k')} = 430 (\m. ~(m < SUC n)) o FST o prob_unif n INTER 431 (\m. m = k') o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n UNION 432 (\m. m = k') o FST o prob_unif n` 433 >- (PSET_TAC [o_DEF, EXTENSION] 434 >> RW_TAC std_ss [SPECIFICATION, GSYM EXTENSION]) 435 >> Rewr 436 >> Know 437 `prob bern 438 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 439 (\m. m = k') o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n 440 UNION (\m. m = k') o FST o prob_unif n) = 441 prob bern 442 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 443 (\m. m = k') o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n) + 444 prob bern ((\m. m = k') o FST o prob_unif n)` 445 >- (MATCH_MP_TAC PROB_ADDITIVE 446 >> ASSUME_TAC (Q.SPEC `n` INDEP_FN_PROB_UNIF) 447 >> ASSUME_TAC (Q.SPECL [`t`, `n`] INDEP_FN_PROB_UNIFORM_CUT) 448 >> RW_TAC bool_ss [PROB_SPACE_BERN] >| 449 [MATCH_MP_TAC EVENTS_INTER 450 >> RW_TAC bool_ss [INDEP_FN_FST_EVENTS', PROB_SPACE_BERN, 451 INDEP_FN_SND_EVENTS', o_ASSOC], 452 RW_TAC bool_ss [INDEP_FN_FST_EVENTS], 453 RW_TAC bool_ss [IN_DISJOINT, IN_INTER, IN_o, o_THM] 454 >> RW_TAC bool_ss [SPECIFICATION] 455 >> PROVE_TAC []]) 456 >> Rewr 457 >> Know 458 `prob bern 459 ((\m. ~(m < SUC n)) o FST o prob_unif n INTER 460 (\m. m = k') o FST o prob_uniform_cut t (SUC n) o SND o prob_unif n) = 461 prob bern ((\m. ~(m < SUC n)) o FST o prob_unif n) * 462 prob bern ((\m. m = k') o FST o prob_uniform_cut t (SUC n))` 463 >- (MP_TAC (Q.ISPEC `prob_unif n` INDEP_FN_PROB) 464 >> MP_TAC (Q.SPEC `n` INDEP_FN_PROB_UNIF) 465 >> RW_TAC bool_ss [o_ASSOC] 466 >> POP_ASSUM MATCH_MP_TAC 467 >> RW_TAC bool_ss [INDEP_FN_FST_EVENTS', INDEP_FN_PROB_UNIFORM_CUT]) 468 >> Rewr 469 >> Know 470 `prob bern ((\m. m = k) o FST o prob_unif n) = 471 prob bern ((\m. m = k') o FST o prob_unif n)` 472 >- (Know 473 `!k. ((\m. m = k) o FST o prob_unif n) = {s | FST (prob_unif n s) = k}` 474 >- (PSET_TAC [EXTENSION] 475 >> RW_TAC bool_ss [o_THM, SPECIFICATION, GSYM EXTENSION]) 476 >> Rewr 477 >> RW_TAC bool_ss [o_DEF, Q.SPECL [`n`, `k`, `k'`] PROB_BERN_UNIF_PAIR] 478 >> MP_TAC (Q.SPEC `n` LOG2_LOWER) 479 >> DECIDE_TAC) 480 >> Rewr 481 >> RW_TAC bool_ss [REAL_ADD2_SUB2, REAL_SUB_REFL, REAL_ADD_RID] 482 >> RW_TAC bool_ss [GSYM REAL_SUB_LDISTRIB, ABS_MUL, pow] 483 >> MATCH_MP_TAC REAL_LE_MUL2 484 >> REVERSE (RW_TAC bool_ss [ABS_POS]) 485 >- (POP_ASSUM MP_TAC 486 >> RW_TAC bool_ss [o_DEF, GSPEC_DEST]) 487 >> KILL_TAC 488 >> RW_TAC bool_ss [ABS_PROB, PROB_SPACE_BERN, INDEP_FN_FST_EVENTS, 489 INDEP_FN_PROB_UNIF] 490 >> Know 491 `(\m. ~(m < SUC n)) o FST o prob_unif n = 492 COMPL ((\m. m < SUC n) o FST o prob_unif n)` 493 >- (PSET_TAC [o_DEF, EXTENSION] 494 >> RW_TAC bool_ss [SPECIFICATION]) 495 >> Rewr 496 >> ASSUME_TAC (Q.ISPECL [`bern`, `(\m. m < SUC n) o FST o prob_unif n`, `(1 :real) / 2`] 497 PROB_COMPL_LE1) 498 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [PROB_SPACE_BERN, SPACE_BERN_UNIV, GSYM COMPL_DEF])) 499 >> MP_TAC (Q.ISPEC `prob_unif n` INDEP_FN_FST_EVENTS) 500 >> RW_TAC bool_ss [INDEP_FN_PROB_UNIF, o_ASSOC, PROB_SPACE_BERN] 501 >> KILL_TAC 502 >> MP_TAC (Q.SPEC `n` PROB_BERN_UNIF_GOOD) 503 >> RW_TAC real_ss [o_DEF, GSPEC_DEST] 504 >> RW_TAC bool_ss [ONE_MINUS_HALF]); 505 506val PROB_BERN_UNIFORM_CUT_SUC = store_thm 507 ("PROB_BERN_UNIFORM_CUT_SUC", 508 ``!t n k. 509 k < SUC n ==> 510 abs 511 (prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k} - 1 / & (SUC n)) 512 <= (1 / 2) pow t``, 513 RW_TAC bool_ss [GSYM ABS_BETWEEN_LE] 514 >> REWRITE_TAC [real_lte] >| (* 3 sub-goals here *) 515 [ (* goal 1 (of 3) *) 516 PROVE_TAC [POW_HALF_POS, REAL_LT_LE, real_lte], 517 (* goal 2 (of 3) *) 518 STRIP_TAC 519 >> Know 520 `!k. 521 k < SUC n ==> 522 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k} < 523 1 / & (SUC n)` 524 >- (RW_TAC bool_ss [real_lt] 525 >> STRIP_TAC 526 >> Know 527 `(1 / 2) pow t < 528 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k'} - 529 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k}` 530 >- (Q.PAT_X_ASSUM `x < y - z` MP_TAC 531 >> RW_TAC bool_ss [GSYM REAL_LT_ADD_SUB] 532 >> PROVE_TAC [REAL_ADD_SYM, REAL_LTE_TRANS]) 533 >> STRIP_TAC 534 >> MP_TAC (Q.SPECL [`t`, `n`, `k'`, `k`] PROB_BERN_UNIFORM_CUT_PAIR) 535 >> RW_TAC bool_ss [GSYM real_lt, abs] 536 >> Suff `F` >- PROVE_TAC [] 537 >> POP_ASSUM MP_TAC 538 >> RW_TAC bool_ss [] 539 >> PROVE_TAC [POW_HALF_POS, REAL_LT_TRANS, REAL_LT_LE]) 540 >> STRIP_TAC 541 >> Suff `prob bern {s | FST (prob_uniform_cut t (SUC n) s) < SUC n} < 1` 542 >- RW_TAC bool_ss [PROB_UNIFORM_CUT_RANGE, GUNIV, PROB_BERN_BASIC, 543 REAL_LT_REFL] 544 >> MP_TAC (Q.SPEC `1 / &(SUC n)` PROB_BERN_UNIFORM_CUT_LOWER_BOUND) 545 >> ASM_REWRITE_TAC [] 546 >> DISCH_THEN (MP_TAC o Q.SPEC `n`) 547 >> Know `~(& (SUC n) = (0 :real))` >- RW_TAC arith_ss [REAL_INJ] 548 >> RW_TAC arith_ss [GSYM REAL_INV_1OVER, REAL_MUL_RINV], 549 (* goal 3 (of 3) *) 550 STRIP_TAC 551 >> Know 552 `!k. 553 k < SUC n ==> 554 1 / & (SUC n) < 555 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k}` 556 >- (RW_TAC bool_ss [real_lt] 557 >> STRIP_TAC 558 >> Know 559 `(1 / 2) pow t < 560 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k} - 561 prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k'}` 562 >- (RW_TAC bool_ss [GSYM REAL_LT_ADD_SUB] 563 >> ONCE_REWRITE_TAC [REAL_ADD_SYM] 564 >> MP_TAC 565 (Q.SPECL 566 [`prob bern {s | FST (prob_uniform_cut t (SUC n) s) = k'}`, 567 `1 / & (SUC n)`, `(1 / 2) pow t`] 568 REAL_LE_RADD) 569 >> RW_TAC bool_ss [] 570 >> PROVE_TAC [REAL_ADD_SYM, REAL_LET_TRANS]) 571 >> STRIP_TAC 572 >> MP_TAC (Q.SPECL [`t`, `n`, `k`, `k'`] PROB_BERN_UNIFORM_CUT_PAIR) 573 >> RW_TAC bool_ss [GSYM real_lt, abs] 574 >> Suff `F` >- PROVE_TAC [] 575 >> POP_ASSUM MP_TAC 576 >> RW_TAC bool_ss [] 577 >> PROVE_TAC [POW_HALF_POS, REAL_LT_TRANS, REAL_LT_LE]) 578 >> STRIP_TAC 579 >> Suff `1 < prob bern {s | FST (prob_uniform_cut t (SUC n) s) < SUC n}` 580 >- RW_TAC bool_ss [PROB_UNIFORM_CUT_RANGE, GUNIV, PROB_BERN_BASIC, 581 REAL_LT_REFL] 582 >> MP_TAC (Q.SPEC `1 / &(SUC n)` PROB_BERN_UNIFORM_CUT_UPPER_BOUND) 583 >> ASM_REWRITE_TAC [] 584 >> DISCH_THEN (MP_TAC o Q.SPEC `n`) 585 >> Know `~(& (SUC n) = (0 :real))` >- RW_TAC arith_ss [REAL_INJ] 586 >> RW_TAC arith_ss [GSYM REAL_INV_1OVER, REAL_MUL_RINV]]); 587 588val PROB_BERN_UNIFORM_CUT = store_thm 589 ("PROB_BERN_UNIFORM_CUT", 590 ``!t n k. 591 k < n ==> 592 abs (prob bern {s | FST (prob_uniform_cut t n s) = k} - 1 / &n) <= 593 (1 / 2) pow t``, 594 NTAC 3 STRIP_TAC 595 >> Cases_on `n` >- RW_TAC arith_ss [] 596 >> RW_TAC bool_ss [PROB_BERN_UNIFORM_CUT_SUC]); 597 598val PROB_PROB_UNIFORM_CUT_LOWER_SUC = store_thm 599 ("PROB_PROB_UNIFORM_CUT_LOWER_SUC", 600 ``!t n k. 601 k < n /\ 2 * log2 (n + 1) <= t ==> 602 1 / (&n + 1) <= prob bern {s | FST (prob_uniform_cut t n s) = k}``, 603 REPEAT STRIP_TAC 604 >> MP_TAC (Q.SPECL [`t`, `n`, `k`] PROB_BERN_UNIFORM_CUT) 605 >> ASM_REWRITE_TAC [GSYM ABS_BETWEEN_LE] 606 >> REPEAT STRIP_TAC 607 >> POP_ASSUM K_TAC 608 >> Suff `((1 :real) / 2) pow t <= 1 / &n - 1 / (&n + 1)` 609 >- (POP_ASSUM MP_TAC 610 >> REAL_ARITH_TAC) 611 >> POP_ASSUM K_TAC 612 >> Know `0 < n` >- DECIDE_TAC 613 >> PROVE_TAC [LOG2_SUC]); 614 615val PROB_BERN_UNIFORM_CUT_CARD_LOWER = store_thm 616 ("PROB_BERN_UNIFORM_CUT_CARD_LOWER", 617 ``!t n a. 618 0 < n /\ a SUBSET count n ==> 619 &(CARD a) * (1 / &n - (1 / 2) pow t) <= 620 prob bern {s | FST (prob_uniform_cut t n s) IN a}``, 621 REPEAT STRIP_TAC 622 >> Know `FINITE a` 623 >- PROVE_TAC [FINITE_COUNT, SUBSET_FINITE] 624 >> STRIP_TAC 625 >> Q.PAT_X_ASSUM `a SUBSET x` MP_TAC 626 >> POP_ASSUM MP_TAC 627 >> Q.SPEC_TAC (`a`, `a`) 628 >> HO_MATCH_MP_TAC FINITE_INDUCT 629 >> CONJ_TAC 630 >- RW_TAC real_ss [CARD_EMPTY, PROB_BERN_BASIC, NOT_IN_EMPTY, GEMPTY, 631 REAL_LE_REFL] 632 >> POP_ASSUM MP_TAC 633 >> Cases_on `n` >- RW_TAC std_ss [] 634 >> MP_TAC (Q.ISPEC `prob_uniform_cut t (SUC n')` INDEP_FN_PROB_FST_INSERT) 635 >> RW_TAC std_ss [INDEP_FN_PROB_UNIFORM_CUT] 636 >> RW_TAC bool_ss [CARD_INSERT, ADD1, GSYM REAL_ADD, REAL_RDISTRIB] 637 >> Know `!a b c d : real. a <= d /\ b <= c ==> a + b <= c + d` 638 >- REAL_ARITH_TAC 639 >> DISCH_THEN MATCH_MP_TAC 640 >> RW_TAC bool_ss [GSYM ADD1, REAL_ADD] 641 >- (Q.PAT_X_ASSUM `x ==> y` MATCH_MP_TAC 642 >> POP_ASSUM MP_TAC 643 >> RW_TAC bool_ss [SUBSET_DEF, IN_INSERT]) 644 >> Suff 645 `abs 646 (prob bern {s | FST (prob_uniform_cut t (SUC n') s) = e} - 1 / &(SUC n')) 647 <= (1 / 2) pow t` 648 >- RW_TAC bool_ss [REAL_MUL_LID, GSYM ABS_BETWEEN_LE] 649 >> MATCH_MP_TAC PROB_BERN_UNIFORM_CUT 650 >> Suff `e IN count (SUC n')` >- RW_TAC bool_ss [SPECIFICATION, IN_COUNT] 651 >> PROVE_TAC [IN_INSERT, SUBSET_DEF]); 652 653val PROB_BERN_UNIFORM_CUT_CARD_LOWER_SUC = store_thm 654 ("PROB_BERN_UNIFORM_CUT_CARD_LOWER_SUC", 655 ``!t n a. 656 0 < n /\ a SUBSET count n /\ 2 * log2 (n + 1) <= t ==> 657 &(CARD a) * (1 / &(n + 1)) <= 658 prob bern {s | FST (prob_uniform_cut t n s) IN a}``, 659 REPEAT STRIP_TAC 660 >> Cases_on `a = {}` 661 >- RW_TAC real_ss [CARD_EMPTY, PROB_BERN_BASIC, NOT_IN_EMPTY, GEMPTY, 662 REAL_LE_REFL] 663 >> MP_TAC (Q.SPECL [`t`, `n`, `a`] PROB_BERN_UNIFORM_CUT_CARD_LOWER) 664 >> MP_TAC (Q.SPECL [`n`, `t`] LOG2_SUC) 665 >> ASM_REWRITE_TAC [] 666 >> MP_TAC (Q.SPEC `&(CARD (a : num -> bool))` REAL_MULT_LE_CANCEL) 667 >> Know `FINITE (a : num -> bool)` 668 >- PROVE_TAC [FINITE_COUNT, SUBSET_FINITE] 669 >> STRIP_TAC 670 >> Know `(0 :real) < &(CARD (a : num -> bool))` 671 >- (MATCH_MP_TAC REAL_NZ_IMP_LT 672 >> RW_TAC bool_ss [REAL_INJ, CARD_EQ_0]) 673 >> DISCH_THEN (REWRITE_TAC o wrap) 674 >> DISCH_THEN (REWRITE_TAC o wrap) 675 >> Q.SPEC_TAC (`(1 / 2) pow t`, `x`) 676 >> Q.SPEC_TAC 677 (`inv (&(CARD a)) * prob bern {s | FST (prob_uniform_cut t n s) IN a}`, 678 `y`) 679 >> KILL_TAC 680 >> REWRITE_TAC [REAL_ADD] 681 >> REAL_ARITH_TAC); 682 683val PROB_UNIFORM_TERMINATES = store_thm 684 ("PROB_UNIFORM_TERMINATES", 685 ``!n. ?*s. FST (prob_unif n s) < SUC n``, 686 RW_TAC bool_ss [possibly_bern_def, possibly_def] 687 >- (Suff 688 `{s | FST (prob_unif n s) < SUC n} = {x | x < SUC n} o FST o prob_unif n` 689 >- RW_TAC bool_ss [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_UNIF] 690 >> SET_EQ_TAC 691 >> PSET_TAC [o_THM]) 692 >> MP_TAC (Q.SPECL [`n`, `SUC n`] PROB_BERN_UNIF_LT) 693 >> Cond >- RW_TAC bool_ss [LOG2_LOWER_SUC] 694 >> Rewr 695 >> RW_TAC bool_ss [REAL_ENTIRE, REAL_INJ] 696 >> PROVE_TAC [POW_HALF_POS, REAL_LT_LE]); 697 698val INDEP_FN_PROB_UNIFORM = store_thm 699 ("INDEP_FN_PROB_UNIFORM", 700 ``!n. prob_uniform (SUC n) IN indep_fn``, 701 RW_TAC bool_ss [prob_uniform_def, INDEP_FN_PROB_UNTIL, INDEP_FN_PROB_UNIF, 702 PROB_UNIFORM_TERMINATES]); 703 704val PROB_BERN_UNIFORM = store_thm 705 ("PROB_BERN_UNIFORM", 706 ``!n k. k < n ==> (prob bern {s | FST (prob_uniform n s) = k} = 1 / &n)``, 707 Cases >- RW_TAC arith_ss [] 708 >> RW_TAC bool_ss [prob_uniform_def] 709 >> (MP_TAC o 710 Q.SPECL [`{k}`, `prob_unif n'`, `\x. x < SUC n'`] o 711 INST_TYPE [alpha |-> ``:num``]) 712 PROB_BERN_UNTIL 713 >> Cond >- RW_TAC bool_ss [INDEP_FN_PROB_UNIF, PROB_UNIFORM_TERMINATES] 714 >> Know 715 `{k} o FST o prob_until (prob_unif n') (\x. x < SUC n') = 716 {s | FST (prob_until (prob_unif n') (\x. x < SUC n') s) = k}` 717 >- (SET_EQ_TAC 718 >> PSET_TAC [o_THM]) 719 >> Rewr 720 >> Rewr 721 >> Know 722 `({k} INTER {x | (\x. x < SUC n') x}) o FST o prob_unif n' = 723 {s | FST (prob_unif n' s) = k}` 724 >- (SET_EQ_TAC 725 >> PSET_TAC [o_THM] 726 >> RW_TAC arith_ss []) 727 >> Rewr 728 >> Know 729 `{x | (\x. x < SUC n') x} o FST o prob_unif n' = 730 {s | FST (prob_unif n' s) < SUC n'}` 731 >- (SET_EQ_TAC 732 >> PSET_TAC [o_THM]) 733 >> Rewr 734 >> MP_TAC (Q.SPECL [`n'`, `SUC n'`] PROB_BERN_UNIF_LT) 735 >> MP_TAC (Q.SPEC `n'` LOG2_LOWER_SUC) 736 >> STRIP_TAC 737 >> ASM_REWRITE_TAC [] 738 >> Rewr 739 >> MP_TAC (Q.SPECL [`n'`, `k`] PROB_BERN_UNIF) 740 >> RW_TAC arith_ss [] 741 >> MATCH_MP_TAC REAL_DIV_EQ 742 >> RW_TAC bool_ss [REAL_ENTIRE, REAL_INJ, REAL_MUL_LID] 743 >- PROVE_TAC [POW_HALF_POS, REAL_LT_LE] 744 >> RW_TAC bool_ss [REAL_MUL_SYM]); 745 746val PROB_UNIFORM_RANGE = store_thm 747 ("PROB_UNIFORM_RANGE", 748 ``!n. !*s. FST (prob_uniform (SUC n) s) < SUC n``, 749 RW_TAC bool_ss [prob_uniform_def] 750 >> MP_TAC (Q.ISPECL [`prob_unif n`, `\x. x < SUC n`] PROB_UNTIL_POST) 751 >> RW_TAC bool_ss [PROB_UNIFORM_TERMINATES, INDEP_FN_PROB_UNIF]); 752 753val _ = export_theory (); 754