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 arithmeticTheory pred_setTheory 10 listTheory sequenceTheory state_transformerTheory 11 HurdUseful extra_numTheory combinTheory 12 pairTheory realTheory realLib extra_boolTheory 13 extra_pred_setTheory extra_realTheory extra_pred_setTools numTheory 14 simpLib seqTheory sequenceTools subtypeTheory res_quanTheory; 15 16open util_probTheory measureTheory probabilityTheory; 17open prob_algebraTheory probTheory; 18 19(* interactive mode 20quietdec := false; 21*) 22 23val _ = new_theory "prob_geometric"; 24 25val EXISTS_DEF = boolTheory.EXISTS_DEF; 26val std_ss' = std_ss ++ boolSimps.ETA_ss; 27val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 28val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 29val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC; 30val Cond = 31 DISCH_THEN 32 (fn mp_th => 33 let 34 val cond = fst (dest_imp (concl mp_th)) 35 in 36 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 37 end); 38 39(* ------------------------------------------------------------------------- *) 40(* The definition of the geometric(1/2) random number generator. *) 41(* ------------------------------------------------------------------------- *) 42 43val prob_geometric_iter_def = Define 44 `prob_geometric_iter s = BIND sdest (\b. UNIT (b, SUC (SND s)))`; 45 46val prob_geometric_loop_def = Define 47 `prob_geometric_loop = prob_while FST prob_geometric_iter`; 48 49val prob_geometric_def = Define 50 `prob_geometric = 51 BIND (BIND (UNIT (T, 0)) prob_geometric_loop) (\s. UNIT (SND s - 1))`; 52 53(* ------------------------------------------------------------------------- *) 54(* Theorems leading to: *) 55(* 1. prob_geometric IN indep_fn *) 56(* 2. !n. prob {s | FST (prob_geometric s) = n} = (1 / 2) pow (n + 1) *) 57(* ------------------------------------------------------------------------- *) 58 59val INDEP_FN_PROB_GEOMETRIC_ITER = store_thm 60 ("INDEP_FN_PROB_GEOMETRIC_ITER", 61 ``!a. prob_geometric_iter a IN indep_fn``, 62 RW_TAC std_ss [prob_geometric_iter_def, INDEP_FN_SDEST, INDEP_FN_BIND, 63 INDEP_FN_UNIT]); 64 65val PROB_GEOMETRIC_LOOP_TERMINATES = store_thm 66 ("PROB_GEOMETRIC_LOOP_TERMINATES", 67 ``prob_while_terminates FST prob_geometric_iter``, 68 MATCH_MP_TAC PROB_WHILE_TERMINATES_SUFFICIENT 69 >> RW_TAC std_ss [INDEP_FN_PROB_GEOMETRIC_ITER, possibly_bern_def, 70 possibly_def] \\ 71 ( RW_TAC std_ss [prob_geometric_iter_def, UNIT_DEF, BIND_DEF, o_DEF, 72 UNCURRY] 73 >> Suff `{s | ~FST (sdest s)} = halfspace F` 74 >- (RW_TAC std_ss [EVENTS_BERN_HALFSPACE, PROB_BERN_HALFSPACE] 75 >> PROVE_TAC [REAL_LT_LE, HALF_POS]) 76 >> SET_EQ_TAC 77 >> RW_TAC std_ss [GSPECIFICATION, IN_HALFSPACE, sdest_def] )); 78 79val INDEP_FN_PROB_GEOMETRIC_LOOP = store_thm 80 ("INDEP_FN_PROB_GEOMETRIC_LOOP", 81 ``!a. prob_geometric_loop a IN indep_fn``, 82 RW_TAC std_ss [prob_geometric_loop_def, INDEP_FN_PROB_WHILE, 83 PROB_GEOMETRIC_LOOP_TERMINATES, 84 INDEP_FN_PROB_GEOMETRIC_ITER]); 85 86val INDEP_FN_PROB_GEOMETRIC = store_thm 87 ("INDEP_FN_PROB_GEOMETRIC", 88 ``prob_geometric IN indep_fn``, 89 RW_TAC std_ss [prob_geometric_def, INDEP_FN_BIND, INDEP_FN_UNIT, 90 INDEP_FN_PROB_GEOMETRIC_LOOP]); 91 92val PROB_GEOMETRIC_LOOP_F = store_thm 93 ("PROB_GEOMETRIC_LOOP_F", 94 ``!n. !*s. FST (prob_geometric_loop (F, n) s) = (F, n)``, 95 RW_TAC std_ss [prob_geometric_loop_def] 96 >> MP_TAC (Q.ISPEC `\w : bool # num. w = (F, n)` PROB_WHILE) 97 >> RW_TAC std_ss [] 98 >> POP_ASSUM MATCH_MP_TAC 99 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES, 100 INDEP_FN_PROB_GEOMETRIC_ITER] 101 >> MATCH_MP_TAC DEFINITELY_PROBABLY 102 >> Cases_on `n'` 103 >> RW_TAC std_ss [prob_while_cut_def, BIND_DEF, o_THM, UNCURRY, 104 prob_geometric_iter_def, UNIT_DEF, sdest_def]); 105 106val PROB_GEOMETRIC_LOOP_T_RANGE = store_thm 107 ("PROB_GEOMETRIC_LOOP_T_RANGE", 108 ``!n. !*s. n < SND (FST (prob_geometric_loop (T,n) s))``, 109 RW_TAC std_ss [prob_geometric_loop_def] 110 >> MP_TAC (Q.ISPEC `\w : bool # num. n < SND w` PROB_WHILE) 111 >> RW_TAC std_ss [] 112 >> POP_ASSUM MATCH_MP_TAC 113 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES, 114 INDEP_FN_PROB_GEOMETRIC_ITER] 115 >> MATCH_MP_TAC DEFINITELY_PROBABLY 116 >> Q.SPEC_TAC (`n`, `n`) 117 >> Induct_on `n'` >- RW_TAC std_ss [prob_while_cut_def, UNIT_DEF] 118 >> REPEAT GEN_TAC 119 >> (REVERSE (Cases_on `shd s`) 120 >> RW_TAC std_ss [prob_while_cut_def, BIND_DEF, o_THM, UNCURRY, 121 prob_geometric_iter_def, UNIT_DEF, sdest_def]) 122 >- (POP_ASSUM MP_TAC 123 >> Cases_on `n'` 124 >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF]) 125 >> MATCH_MP_TAC LESS_TRANS 126 >> Q.EXISTS_TAC `SUC n` 127 >> CONJ_TAC >- DECIDE_TAC 128 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 129 >> RW_TAC std_ss []); 130 131val PROB_GEOMETRIC_LOOP_STOPS = store_thm 132 ("PROB_GEOMETRIC_LOOP_STOPS", 133 ``!n. !*s. (SND (FST (prob_geometric_loop (b,n) s)) = n) = ~b``, 134 RW_TAC std_ss [prob_geometric_loop_def] 135 >> MP_TAC (Q.ISPEC `\w : bool # num. (SND w = n) = ~b` PROB_WHILE) 136 >> RW_TAC std_ss [] 137 >> POP_ASSUM MATCH_MP_TAC 138 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES, 139 INDEP_FN_PROB_GEOMETRIC_ITER] 140 >> Cases_on `n'` 141 >- (RW_TAC std_ss [prob_while_cut_def, UNIT_DEF] 142 >> MATCH_MP_TAC DEFINITELY_PROBABLY 143 >> RW_TAC std_ss []) 144 >> RW_TAC std_ss [prob_while_cut_def, UNIT_DEF, PROBABLY_TRUE, BIND_DEF, 145 UNCURRY, o_THM, prob_geometric_iter_def, sdest_def] 146 >> MATCH_MP_TAC DEFINITELY_PROBABLY 147 >> RW_TAC std_ss [] 148 >> KILL_TAC 149 >> Know `!a b : num. b < a ==> ~(a = b)` >- DECIDE_TAC 150 >> DISCH_THEN MATCH_MP_TAC 151 >> Know `n < SUC n` >- DECIDE_TAC 152 >> Q.SPEC_TAC (`SUC n`, `m`) 153 >> Q.SPEC_TAC (`shd s`, `b`) 154 >> Q.SPEC_TAC (`stl s`, `s`) 155 >> Induct_on `n''` >- RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF] 156 >> RW_TAC arith_ss [prob_while_cut_def, BIND_DEF, UNIT_DEF, UNCURRY, o_THM, 157 prob_geometric_iter_def, sdest_def]); 158 159val PROB_BERN_GEOMETRIC_LOOP_LEMMA = store_thm 160 ("PROB_BERN_GEOMETRIC_LOOP_LEMMA", 161 ``!d n. 162 prob bern 163 ((\x. SND x = n + SUC d) o FST o 164 BIND sdest (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop)) = 165 1 / 2 * 166 prob bern 167 ((\x. SND x = n + SUC d) o FST o 168 (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop) T) + 169 1 / 2 * 170 prob bern 171 ((\x. SND x = n + SUC d) o FST o 172 (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop) F)``, 173 REPEAT GEN_TAC 174 >> (MP_TAC o 175 Q.SPECL 176 [`sdest`, 177 `\a. BIND (UNIT (a,SUC n)) (prob_while FST prob_geometric_iter)`, 178 `1 / 2`, 179 `\x. SND x = n + SUC d`] o 180 INST_TYPE [alpha |-> ``:bool # num``]) 181 PROB_BERN_BIND_BOOL 182 >> Cond 183 >- (REVERSE (RW_TAC std_ss [INDEP_FN_SDEST]) 184 >- (Suff `FST o sdest = halfspace T` 185 >- RW_TAC std_ss [PROB_BERN_HALFSPACE] 186 >> SET_EQ_TAC 187 >> RW_TAC std_ss [IN_HALFSPACE, sdest_def, IN_o] 188 >> RW_TAC std_ss [SPECIFICATION]) 189 >> MATCH_MP_TAC INDEP_FN_BIND 190 >> RW_TAC std_ss [INDEP_FN_UNIT] 191 >> MATCH_MP_TAC INDEP_FN_PROB_WHILE 192 >> RW_TAC std_ss [INDEP_FN_PROB_GEOMETRIC_ITER, 193 PROB_GEOMETRIC_LOOP_TERMINATES]) 194 >> RW_TAC std_ss [ONE_MINUS_HALF, prob_geometric_loop_def]); 195 196val PROB_BERN_GEOMETRIC_LOOP = store_thm 197 ("PROB_BERN_GEOMETRIC_LOOP", 198 ``!n d. 199 prob bern {s | SND (FST (prob_geometric_loop (T,n) s)) = n + SUC d} = 200 (1 / 2) pow SUC d``, 201 RW_TAC std_ss [prob_geometric_loop_def] 202 >> RW_TAC std_ss [PROB_WHILE_ADVANCE, INDEP_FN_PROB_GEOMETRIC_ITER, 203 PROB_GEOMETRIC_LOOP_TERMINATES, prob_geometric_iter_def, 204 GSYM BIND_ASSOC] 205 >> Know 206 `!f : (num -> bool) -> (bool # num) # (num -> bool). 207 {s | SND (FST (f s)) = n + SUC d} = (\x. SND x = n + SUC d) o FST o f` 208 >- (SET_EQ_TAC 209 >> PSET_TAC [] 210 >> RW_TAC std_ss [SPECIFICATION, o_THM]) 211 >> Rewr 212 >> RW_TAC std_ss [GSYM prob_geometric_loop_def] 213 >> Q.SPEC_TAC (`n`, `n`) 214 >> Induct_on `d` 215 >- (RW_TAC std_ss [PROB_BERN_GEOMETRIC_LOOP_LEMMA] 216 >> RW_TAC real_ss [ADD_CLAUSES, pow, o_DEF, BIND_DEF, UNCURRY, UNIT_DEF, 217 prob_geometric_loop_def] 218 >> Know 219 `prob bern 220 (\x. 221 SND (FST (prob_while FST prob_geometric_iter (F,SUC n) x)) = 222 n + 1) = 223 prob bern UNIV` 224 >- (REWRITE_TAC [GSYM ADD1] 225 >> MATCH_MP_TAC PROB_BERN_UNIVERSAL 226 >> Q.EXISTS_TAC 227 `\s. (SND (FST (prob_geometric_loop (F, SUC n) s)) = SUC n) = ~F` 228 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_STOPS, EVENTS_BERN_UNIV, 229 IN_UNIV] 230 >- (RW_TAC std_ss [SYM prob_geometric_loop_def] 231 >> Suff 232 `(\x. SND (FST (prob_geometric_loop (F,SUC n) x)) = SUC n) = 233 (\x. SND x = SUC n) o FST o prob_geometric_loop (F, SUC n)` 234 >- (Rewr 235 >> PROVE_TAC [INDEP_FN_FST_EVENTS, 236 INDEP_FN_PROB_GEOMETRIC_LOOP]) 237 >> FUN_EQ_TAC 238 >> RW_TAC std_ss [o_DEF]) 239 >> RW_TAC std_ss [SPECIFICATION, GSYM prob_geometric_loop_def]) 240 >> Rewr 241 >> Know 242 `prob bern 243 (\x. 244 SND (FST (prob_while FST prob_geometric_iter (T,SUC n) x)) = 245 n + 1) = 246 prob bern {}` 247 >- (REWRITE_TAC [GSYM ADD1] 248 >> MATCH_MP_TAC PROB_BERN_UNIVERSAL 249 >> Q.EXISTS_TAC 250 `\s. (SND (FST (prob_geometric_loop (T, SUC n) s)) = SUC n) = ~T` 251 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_STOPS, EVENTS_BERN_EMPTY, 252 NOT_IN_EMPTY] 253 >- (RW_TAC std_ss [SYM prob_geometric_loop_def] 254 >> Suff 255 `(\x. SND (FST (prob_geometric_loop (T,SUC n) x)) = SUC n) = 256 (\x. SND x = SUC n) o FST o prob_geometric_loop (T, SUC n)` 257 >- (Rewr 258 >> PROVE_TAC [INDEP_FN_FST_EVENTS, 259 INDEP_FN_PROB_GEOMETRIC_LOOP]) 260 >> FUN_EQ_TAC 261 >> RW_TAC std_ss [o_DEF]) 262 >> RW_TAC std_ss [SPECIFICATION, GSYM prob_geometric_loop_def]) 263 >> Rewr 264 >> RW_TAC real_ss [PROB_BERN_BASIC]) 265 >> RW_TAC std_ss [PROB_BERN_GEOMETRIC_LOOP_LEMMA] 266 >> RW_TAC std_ss [prob_geometric_loop_def, BIND_DEF, o_DEF, UNCURRY, 267 UNIT_DEF] 268 >> RW_TAC std_ss [PROB_WHILE_ADVANCE, INDEP_FN_PROB_GEOMETRIC_ITER, 269 PROB_GEOMETRIC_LOOP_TERMINATES, prob_geometric_iter_def, 270 GSYM BIND_ASSOC, UNIT_DEF] 271 >> Know `!n d. (SUC n = n + SUC (SUC d)) = F` >- DECIDE_TAC 272 >> Rewr 273 >> RW_TAC bool_ss [GSYM EMPTY_DEF, PROB_BERN_EMPTY, REAL_MUL_RZERO, 274 GSYM prob_geometric_loop_def, REAL_ADD_RID] 275 >> ONCE_REWRITE_TAC [pow] 276 >> RW_TAC std_ss [REAL_EQ_MUL_LCANCEL] 277 >> DISJ2_TAC 278 >> Suff 279 `(\x. 280 SND 281 (FST 282 (BIND sdest 283 (\a. BIND (\s. ((a,SUC (SUC n)),s)) prob_geometric_loop) x)) = 284 n + SUC (SUC d)) = 285 ((\x. SND x = SUC n + SUC d) o FST o 286 BIND sdest (\a. BIND (UNIT (a,SUC (SUC n))) prob_geometric_loop))` 287 >- (Rewr 288 >> RW_TAC std_ss []) 289 >> FUN_EQ_TAC 290 >> RW_TAC std_ss [BIND_DEF, UNIT_DEF, o_DEF, UNCURRY, ADD_CLAUSES]); 291 292val PROB_BERN_GEOMETRIC = store_thm 293 ("PROB_BERN_GEOMETRIC", 294 ``!n. prob bern {s | FST (prob_geometric s) = n} = (1 / 2) pow (n + 1)``, 295 RW_TAC std_ss [prob_geometric_def, BIND_DEF, o_THM, UNCURRY, UNIT_DEF] 296 >> Suff 297 `prob bern {s | SND (FST (prob_geometric_loop (T,0) s)) - 1 = n} = 298 prob bern {s | SND (FST (prob_geometric_loop (T,0) s)) = 0 + (n + 1)}` 299 >- (Rewr 300 >> RW_TAC bool_ss [GSYM ADD1, PROB_BERN_GEOMETRIC_LOOP]) 301 >> MATCH_MP_TAC PROB_BERN_UNIVERSAL 302 >> Q.EXISTS_TAC `\s. 0 < SND (FST (prob_geometric_loop (T,0) s))` 303 >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_T_RANGE] >| 304 [Suff 305 `{s | SND (FST (prob_geometric_loop (T,0) s)) - 1 = n} = 306 (\x. SND x - 1 = n) o FST o prob_geometric_loop (T, 0)` 307 >- (Rewr 308 >> PROVE_TAC [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_GEOMETRIC_LOOP]) 309 >> SET_EQ_TAC 310 >> PSET_TAC [] 311 >> RW_TAC std_ss [SPECIFICATION, o_DEF], 312 Suff 313 `{s | SND (FST (prob_geometric_loop (T,0) s)) = n + 1} = 314 (\x. SND x = n + 1) o FST o prob_geometric_loop (T, 0)` 315 >- (Rewr 316 >> PROVE_TAC [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_GEOMETRIC_LOOP]) 317 >> SET_EQ_TAC 318 >> PSET_TAC [] 319 >> RW_TAC std_ss [SPECIFICATION, o_DEF], 320 RW_TAC std_ss [GSPECIFICATION] 321 >> DECIDE_TAC]); 322 323val _ = export_theory (); 324