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 14 extra_realTheory extra_pred_setTools numTheory 15 simpLib seqTheory sequenceTools subtypeTheory res_quanTheory; 16 17open measureTheory probabilityTheory; 18open prob_algebraTheory probTheory; 19 20(* interactive mode 21quietdec := false; 22*) 23 24val _ = new_theory "prob_walk"; 25 26val EXISTS_DEF = boolTheory.EXISTS_DEF; 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 a simple random walk. *) 42(* ------------------------------------------------------------------------- *) 43 44val random_lurch_def = Define 45 `random_lurch (n:num) = BIND sdest (\b. UNIT (if b then n + 1 else n - 1))`; 46 47val random_walk_def = Define 48 `random_walk n k = 49 BIND (prob_while_cost ($< 0) random_lurch (n, k)) (\x. UNIT (SND x))`; 50 51(* ------------------------------------------------------------------------- *) 52(* Theorems leading to: *) 53(* 1. prob_while_terminates ($< 0) random_lurch *) 54(* 2. !n l. !*s. EVEN (FST (random_walk n s)) = EVEN n *) 55(* ------------------------------------------------------------------------- *) 56 57val RANDOM_LURCHES_TRANSLATION = store_thm 58 ("RANDOM_LURCHES_TRANSLATION", 59 ``!p i n. 60 prob_while_cut ($< p) random_lurch n (p + i) = 61 BIND (prob_while_cut ($< 0) random_lurch n i) (\l. UNIT (p + l))``, 62 RW_TAC std_ss [] 63 >> Know `i = (p + i) - p` >- DECIDE_TAC 64 >> Rewr' 65 >> Know `p <= p + i` >- DECIDE_TAC 66 >> Q.SPEC_TAC (`p + i`, `q`) 67 >> RW_TAC arith_ss [] 68 >> POP_ASSUM MP_TAC 69 >> Q.SPEC_TAC (`q`, `q`) 70 >> Induct_on `n` 71 >- RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, o_DEF] 72 >> FUN_EQ_TAC 73 >> REPEAT STRIP_TAC 74 >> SEQ_CASES_TAC `x` 75 >> BasicProvers.NORM_TAC arith_ss 76 [prob_while_cut_def, random_lurch_def, BIND_DEF, o_THM, 77 sdest_def, SHD_SCONS, STL_SCONS, UNCURRY, UNIT_DEF] 78 >> Suff `F` >- PROVE_TAC [] 79 >> DECIDE_TAC); 80 81val INDEP_FN_RANDOM_LURCH = store_thm 82 ("INDEP_FN_RANDOM_LURCH", 83 ``!a. random_lurch a IN indep_fn``, 84 RW_TAC std_ss [random_lurch_def, INDEP_FN_BIND, INDEP_FN_UNIT, 85 INDEP_FN_SDEST]); 86 87val INDEP_FN_RANDOM_LURCHES = store_thm 88 ("INDEP_FN_RANDOM_LURCHES", 89 ``!a b c. prob_while_cut a random_lurch b c IN indep_fn``, 90 RW_TAC std_ss [INDEP_FN_PROB_WHILE_CUT, INDEP_FN_RANDOM_LURCH]); 91 92val EVENTS_BERN_RANDOM_LURCHES = store_thm 93 ("EVENTS_BERN_RANDOM_LURCHES", 94 ``!a. 95 {s | ?n. FST (prob_while_cut ($< 0) random_lurch n a s) = 0} IN 96 events bern``, 97 RW_TAC std_ss [GBIGUNION_IMAGE] 98 >> MATCH_MP_TAC EVENTS_COUNTABLE_UNION 99 >> RW_TAC std_ss [PROB_SPACE_BERN, COUNTABLE_NUM, image_countable, 100 SUBSET_DEF, IN_IMAGE, IN_UNIV] 101 >> Suff 102 `{s | FST (prob_while_cut ($< 0) random_lurch n a s) = 0} = 103 ($= 0) o FST o prob_while_cut ($< 0) random_lurch n a` 104 >- RW_TAC std_ss [INDEP_FN_FST_EVENTS, INDEP_FN_RANDOM_LURCHES] 105 >> SET_EQ_TAC 106 >> RW_TAC std_ss [GSPECIFICATION, IN_o, o_THM] 107 >> RW_TAC std_ss [SPECIFICATION] 108 >> PROVE_TAC []); 109 110val RANDOM_LURCHES_MULTIPLICATIVE = store_thm 111 ("RANDOM_LURCHES_MULTIPLICATIVE", 112 ``!a. 113 prob bern 114 {s | 115 ?n. FST (prob_while_cut ($< 0) random_lurch n a s) = 0} = 116 (prob bern 117 {s | 118 ?n. FST (prob_while_cut ($< 0) random_lurch n 1 s) = 0}) pow a``, 119 Induct 120 >- (Know `!n s. FST (prob_while_cut ($< 0) random_lurch n 0 s) = 0` 121 >- (Cases 122 >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, 123 o_THM]) 124 >> Rewr 125 >> RW_TAC std_ss [PROB_BERN_UNIV, GUNIV, pow]) 126 >> Know 127 `!s. 128 (?n. FST (prob_while_cut ($< 0) random_lurch n (SUC a) s) = 0) = 129 (?n. (FST (prob_while_cut ($< a) random_lurch n (SUC a) s) = a) /\ 130 (FST (BIND (prob_while_cut ($< a) random_lurch n (SUC a)) 131 (\l. prob_while_cut ($< 0) random_lurch n l) s) = 0))` 132 >- (POP_ASSUM K_TAC 133 >> RW_TAC std_ss' [] 134 >> EQ_TAC >| 135 [RW_TAC std_ss [] 136 >> Q.EXISTS_TAC `n` 137 >> CONJ_TAC >| 138 [POP_ASSUM MP_TAC 139 >> Know `a < SUC a` >- DECIDE_TAC 140 >> Q.SPEC_TAC (`SUC a`, `b`) 141 >> Q.SPEC_TAC (`s`, `s`) 142 >> Induct_on `n` 143 >- RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF] 144 >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, 145 o_THM, random_lurch_def] 146 >> Know `a < b - 1 \/ (a = b - 1)` 147 >- (Q.PAT_X_ASSUM `!x. P x` K_TAC >> DECIDE_TAC) 148 >> RW_TAC std_ss [] >- PROVE_TAC [] 149 >> Cases_on `n` 150 >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, 151 o_THM], 152 Suff 153 `!m. 154 n <= m ==> 155 (FST (BIND (prob_while_cut ($< a) random_lurch n (SUC a)) 156 (prob_while_cut ($< 0) random_lurch m) s) = 0)` 157 >- PROVE_TAC [LESS_EQ_REFL] 158 >> GEN_TAC 159 >> POP_ASSUM MP_TAC 160 >> Q.SPEC_TAC (`SUC a`, `b`) 161 >> Q.SPEC_TAC (`s`, `s`) 162 >> Induct_on `n` 163 >- (RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, 164 o_THM] 165 >> Cases_on `m` 166 >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, 167 UNCURRY, o_THM]) 168 >> REPEAT STRIP_TAC 169 >> Know `n <= m` >- (Q.PAT_X_ASSUM `!x. P x` K_TAC >> DECIDE_TAC) 170 >> STRIP_TAC 171 >> Q.PAT_X_ASSUM `x = y` MP_TAC 172 >> RW_TAC arith_ss [prob_while_cut_def, GSYM BIND_ASSOC] >| 173 [POP_ASSUM MP_TAC 174 >> ONCE_REWRITE_TAC [BIND_DEF] 175 >> RW_TAC std_ss [UNCURRY, UNIT_DEF, o_THM, random_lurch_def], 176 Cases_on `m` >- FULL_SIMP_TAC arith_ss [] 177 >> POP_ASSUM MP_TAC 178 >> Know `!n : num. (n = 0) = ~(0 < n)` >- RW_TAC arith_ss [] 179 >> RW_TAC std_ss [BIND_DEF, UNIT_DEF, o_THM, UNCURRY, 180 prob_while_cut_def] 181 >> MATCH_MP_TAC PROB_WHILE_CUT_MONO 182 >> Q.EXISTS_TAC `n` 183 >> FULL_SIMP_TAC arith_ss [], 184 Know `b = 0` >- RW_TAC arith_ss [] 185 >> Cases_on `m` >- FULL_SIMP_TAC arith_ss [] 186 >> RW_TAC arith_ss [BIND_DEF, UNIT_DEF, UNCURRY, prob_while_cut_def, 187 o_THM]]], 188 RW_TAC std_ss [] 189 >> Q.EXISTS_TAC `n + n` 190 >> Suff 191 `!m n b s. 192 (FST (BIND (prob_while_cut ($< a) random_lurch m b) 193 (prob_while_cut ($< 0) random_lurch n) s) = 0) ==> 194 (FST (prob_while_cut ($< 0) random_lurch (m + n) b s) = 0)` 195 >- PROVE_TAC [] 196 >> POP_ASSUM_LIST K_TAC 197 >> Induct 198 >- RW_TAC arith_ss [prob_while_cut_def, BIND_DEF, UNIT_DEF, UNCURRY, 199 o_THM] 200 >> RW_TAC arith_ss [prob_while_cut_def, BIND_DEF, UNIT_DEF, UNCURRY, 201 o_THM] 202 >- RW_TAC arith_ss [prob_while_cut_def, BIND_DEF, UNIT_DEF, UNCURRY, 203 o_THM, ADD_CLAUSES] 204 >> Q.PAT_X_ASSUM `!x. P x` K_TAC 205 >> Know `!n : num. (n = 0) = ~(0 < n)` >- DECIDE_TAC 206 >> DISCH_THEN (fn th => FULL_SIMP_TAC std_ss [th]) 207 >> MATCH_MP_TAC PROB_WHILE_CUT_MONO 208 >> Q.EXISTS_TAC `n` 209 >> RW_TAC arith_ss []]) 210 >> Rewr 211 >> Know 212 `!n m b s. 213 (FST (prob_while_cut ($< a) random_lurch n b s) = a) /\ 214 (FST (BIND (prob_while_cut ($< a) random_lurch n b) 215 (\l. prob_while_cut ($< 0) random_lurch m l) s) = 0) = 216 (FST (prob_while_cut ($< a) random_lurch n b s) = a) /\ 217 (FST (BIND (prob_while_cut ($< a) random_lurch n b) 218 (\l. prob_while_cut ($< 0) random_lurch m a) s) = 0)` 219 >- (POP_ASSUM K_TAC 220 >> Know `!a b c. (a /\ b = a /\ c) = (a ==> (b = c))` >- DECIDE_TAC 221 >> Rewr 222 >> Induct 223 >- RW_TAC std_ss [prob_while_cut_def, UNIT_DEF, BIND_DEF, UNCURRY, 224 o_THM] 225 >> RW_TAC std_ss [PROB_WHILE_CUT_REV, UNIT_DEF, BIND_DEF, UNCURRY, 226 o_THM]) 227 >> Rewr 228 >> Know 229 `!n s. 230 (FST (prob_while_cut ($< a) random_lurch n (SUC a) s) = a) /\ 231 (FST (BIND (prob_while_cut ($< a) random_lurch n (SUC a)) 232 (\l. prob_while_cut ($< 0) random_lurch n a) s) = 0) = 233 s IN 234 (($= a o FST o prob_while_cut ($< a) random_lurch n (SUC a)) INTER 235 (($= 0 o FST o prob_while_cut ($< 0) random_lurch n a) o 236 SND o prob_while_cut ($< a) random_lurch n (SUC a)))` 237 >- (POP_ASSUM K_TAC 238 >> RW_TAC std_ss [IN_INTER, IN_o, o_THM] 239 >> RW_TAC arith_ss [SPECIFICATION] 240 >> CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) 241 >> Know `!a b c. (a /\ b = a /\ c) = (a ==> (b = c))` >- DECIDE_TAC 242 >> Rewr 243 >> RW_TAC std_ss [UNIT_DEF, BIND_DEF, UNCURRY, o_THM]) 244 >> Rewr 245 >> MATCH_MP_TAC SEQ_UNIQ 246 >> Q.EXISTS_TAC 247 `prob bern o 248 (\n. 249 {s | 250 s IN 251 $= a o FST o prob_while_cut ($< a) random_lurch n (SUC a) INTER 252 ($= 0 o FST o prob_while_cut ($< 0) random_lurch n a) o SND o 253 prob_while_cut ($< a) random_lurch n (SUC a)})` 254 >> CONJ_TAC 255 >- (MATCH_MP_TAC PROB_INCREASING_UNION 256 >> RW_TAC std_ss [GBIGUNION_IMAGE, PROB_SPACE_BERN, IN_FUNSET, IN_UNIV, 257 SUBSET_DEF, GSPECIFICATION, GDEST] >| 258 [MATCH_MP_TAC EVENTS_INTER 259 >> STRONG_CONJ_TAC >- RW_TAC std_ss [PROB_SPACE_BERN] 260 >> POP_ASSUM K_TAC 261 >> METIS_TAC [INDEP_FN_FST_EVENTS, INDEP_FN_RANDOM_LURCHES, 262 INDEP_FN_SND_EVENTS, o_ASSOC], 263 POP_ASSUM MP_TAC 264 >> SIMP_TAC std_ss [IN_INTER, IN_o, o_THM] 265 >> RW_TAC arith_ss [SPECIFICATION, PROB_WHILE_CUT_REV, BIND_DEF, o_THM, 266 UNCURRY, UNIT_DEF]]) 267 >> ONCE_REWRITE_TAC [o_DEF] 268 >> RW_TAC std_ss [GDEST] 269 >> MP_TAC (GEN ``x:num`` 270 (Q.SPECL [`prob_while_cut ($< a) random_lurch x (SUC a)`, 271 `$= a`, 272 `$= 0 o FST o prob_while_cut ($< 0) random_lurch x a`] 273 (INST_TYPE [alpha |-> ``:num``] INDEP_FN_PROB))) 274 >> RW_TAC std_ss [INDEP_FN_RANDOM_LURCHES, INDEP_FN_FST_EVENTS, pow] 275 >> POP_ASSUM K_TAC 276 >> HO_MATCH_MP_TAC SEQ_MUL 277 >> Know `!f. (\x : num. prob bern (f x)) = prob bern o f` 278 >- RW_TAC std_ss [o_DEF] 279 >> DISCH_THEN (CONV_TAC o DEPTH_CONV o HO_REWR_CONV) 280 >> POP_ASSUM (REWRITE_TAC o wrap o SYM) 281 >> RW_TAC std_ss [] >| 282 [MATCH_MP_TAC PROB_INCREASING_UNION 283 >> SET_EQ_TAC 284 >> RW_TAC std_ss [PROB_SPACE_BERN, IN_FUNSET, IN_UNIV, INDEP_FN_FST_EVENTS, 285 INDEP_FN_RANDOM_LURCHES, SUBSET_DEF, 286 IN_BIGUNION_IMAGE, GSPECIFICATION, IN_o, o_THM, 287 PROB_WHILE_CUT_REV, BIND_DEF, UNIT_DEF, UNCURRY] 288 >> FULL_SIMP_TAC arith_ss [SPECIFICATION, ADD1, RANDOM_LURCHES_TRANSLATION, 289 BIND_DEF, UNCURRY, UNIT_DEF, o_THM] 290 >> Suff `!x. (a = a + x) = (x = 0)` >- RW_TAC std_ss [] 291 >> DECIDE_TAC, 292 MATCH_MP_TAC PROB_INCREASING_UNION 293 >> SET_EQ_TAC 294 >> RW_TAC std_ss [PROB_SPACE_BERN, IN_FUNSET, IN_UNIV, INDEP_FN_FST_EVENTS, 295 INDEP_FN_RANDOM_LURCHES, SUBSET_DEF, 296 IN_BIGUNION_IMAGE, GSPECIFICATION, IN_o, o_THM, 297 PROB_WHILE_CUT_REV, BIND_DEF, UNIT_DEF, UNCURRY] 298 >> FULL_SIMP_TAC arith_ss [SPECIFICATION, ADD1, RANDOM_LURCHES_TRANSLATION, 299 BIND_DEF, UNCURRY, UNIT_DEF, o_THM] 300 >> PROVE_TAC []]); 301 302val PROB_TERMINATES_RANDOM_WALK = store_thm 303 ("PROB_TERMINATES_RANDOM_WALK", 304 ``prob_while_terminates ($< 0) random_lurch``, 305 Know `!n : num. ~(0 < n) = (n = 0)` >- DECIDE_TAC 306 >> RW_TAC std_ss [PROB_WHILE_TERMINATES, probably_bern_def, probably_def, 307 EVENTS_BERN_RANDOM_LURCHES] 308 >> POP_ASSUM K_TAC 309 >> ONCE_REWRITE_TAC [RANDOM_LURCHES_MULTIPLICATIVE] 310 >> Know 311 `?p. 312 prob bern {s | ?n. FST (prob_while_cut ($< 0) random_lurch n 1 s) = 0} 313 = p` 314 >- PROVE_TAC [] 315 >> STRIP_TAC 316 >> ASM_SIMP_TAC std_ss [] 317 >> Suff `p = 1` >- RW_TAC std_ss [POW_ONE] 318 >> Suff `p = 1 / 2 * (p * p) + 1 / 2` 319 >- (POP_ASSUM K_TAC 320 >> STRIP_TAC 321 >> Suff `(p - 1) = 0` >- REAL_ARITH_TAC 322 >> MATCH_MP_TAC POW_ZERO 323 >> Q.EXISTS_TAC `2` 324 >> RW_TAC bool_ss [TWO, pow, POW_1, REAL_SUB_LDISTRIB] 325 >> Suff `2 * p = p * p + 1` >- REAL_ARITH_TAC 326 >> Suff `2 * p = 2 * ((1 / 2) * ((p * p) + 1))` 327 >- RW_TAC std_ss [REAL_MUL_ASSOC, HALF_CANCEL, REAL_MUL_LID] 328 >> RW_TAC std_ss [REAL_EQ_LMUL] 329 >> RW_TAC std_ss [REAL_ADD_LDISTRIB, REAL_MUL_RID] 330 >> PROVE_TAC []) 331 >> POP_ASSUM 332 (fn th => CONV_TAC (LAND_CONV (REWR_CONV (SYM th))) >> ASSUME_TAC th) 333 >> MP_TAC 334 (Q.SPEC `{s | ?n. FST (prob_while_cut ($< 0) random_lurch n 1 s) = 0}` 335 (GSYM PROB_BERN_INTER_HALVES)) 336 >> Cond >- RW_TAC std_ss [EVENTS_BERN_RANDOM_LURCHES] 337 >> Rewr' 338 >> Know 339 `!s. 340 (?n. FST (prob_while_cut ($< 0) random_lurch n 1 s) = 0) = 341 (?n. FST (prob_while_cut ($< 0) random_lurch (SUC n) 1 s) = 0)` 342 >- (REVERSE (REPEAT (STRIP_TAC ORELSE EQ_TAC)) >- PROVE_TAC [] 343 >> REVERSE (Cases_on `n`) >- PROVE_TAC [] 344 >> FULL_SIMP_TAC arith_ss [prob_while_cut_def, UNIT_DEF]) 345 >> Rewr 346 >> SIMP_TAC arith_ss [prob_while_cut_def, random_lurch_def, BIND_DEF, 347 UNIT_DEF, UNCURRY, o_THM] 348 >> Know 349 `halfspace T INTER 350 {s | 351 ?n. 352 FST (prob_while_cut ($< 0) random_lurch n 353 (if FST (sdest s) then 2 else 0) (SND (sdest s))) = 0} = 354 halfspace T INTER 355 ({s | ?n. FST (prob_while_cut ($< 0) random_lurch n 2 s) = 0} o stl)` 356 >- (SET_EQ_TAC 357 >> RW_TAC std_ss [IN_INTER, IN_HALFSPACE, GSPECIFICATION, sdest_def, 358 IN_o]) 359 >> Rewr 360 >> Know 361 `halfspace F INTER 362 {s | 363 ?n. 364 FST (prob_while_cut ($< 0) random_lurch n 365 (if FST (sdest s) then 2 else 0) (SND (sdest s))) = 0} = 366 halfspace F INTER 367 ({s | ?n. FST (prob_while_cut ($< 0) random_lurch n 0 s) = 0} o stl)` 368 >- (SET_EQ_TAC 369 >> RW_TAC std_ss [IN_INTER, IN_HALFSPACE, GSPECIFICATION, sdest_def, 370 IN_o]) 371 >> Rewr 372 >> SIMP_TAC std_ss [PROB_BERN_STL_HALFSPACE, EVENTS_BERN_RANDOM_LURCHES] 373 >> ONCE_REWRITE_TAC [RANDOM_LURCHES_MULTIPLICATIVE] 374 >> ASM_SIMP_TAC bool_ss [pow, TWO, POW_1] 375 >> RW_TAC real_ss []); 376 377val RANDOM_LURCHES_PARITY = store_thm 378 ("RANDOM_LURCHES_PARITY", 379 ``!n k. !*s. 380 EVEN (SND (FST (prob_while_cost ($< 0) random_lurch (n, k) s))) = 381 EVEN (n + k)``, 382 RW_TAC std_ss [prob_while_cost_def] 383 >> MP_TAC 384 (Q.SPECL 385 [`\x:num#num. EVEN (SND x) = EVEN (n + k)`, `$< (0:num) o FST`, 386 `prob_cost SUC random_lurch`, `(n,k):num#num`] 387 (INST_TYPE [alpha |-> ``:num#num``] STRONG_PROB_WHILE)) 388 >> BETA_TAC 389 >> DISCH_THEN MATCH_MP_TAC 390 >> RW_TAC std_ss [INDEP_FN_PROB_COST, PROB_TERMINATES_COST, 391 INDEP_FN_RANDOM_LURCH, PROB_TERMINATES_RANDOM_WALK] 392 >> HO_MATCH_MP_TAC UNIVERSAL_PROBABLY 393 >> Q.SPEC_TAC (`n`, `n`) 394 >> Q.SPEC_TAC (`k`, `k`) 395 >> Know `!n : num. ~(0 < n) = (n = 0)` >- DECIDE_TAC 396 >> STRIP_TAC 397 >> Induct_on `n'` 398 >- RW_TAC std_ss [prob_while_cut_def, UNIT_DEF, o_THM, ADD_CLAUSES] 399 >> BasicProvers.NORM_TAC std_ss 400 [prob_while_cut_def, UNIT_DEF, o_THM, random_lurch_def, 401 BIND_DEF, UNCURRY, prob_cost_def] >| 402 [Q.PAT_X_ASSUM `0 < n` MP_TAC 403 >> POP_ASSUM_LIST K_TAC 404 >> RW_TAC arith_ss [GSYM ADD1, ADD_CLAUSES, EVEN], 405 Q.PAT_X_ASSUM `0 < n` MP_TAC 406 >> POP_ASSUM_LIST K_TAC 407 >> RW_TAC arith_ss [ADD1], 408 POP_ASSUM MP_TAC 409 >> RW_TAC arith_ss []]); 410 411val INDEP_FN_RANDOM_WALK = store_thm 412 ("INDEP_FN_RANDOM_WALK", 413 ``!n k. random_walk n k IN indep_fn``, 414 RW_TAC std_ss [random_walk_def] 415 >> MATCH_MP_TAC INDEP_FN_BIND 416 >> RW_TAC std_ss [INDEP_FN_UNIT] 417 >> MATCH_MP_TAC INDEP_FN_PROB_WHILE_COST 418 >> RW_TAC std_ss [INDEP_FN_RANDOM_LURCH, PROB_TERMINATES_RANDOM_WALK]); 419 420val RANDOM_WALK = store_thm 421 ("RANDOM_WALK", 422 ``!n. 423 (random_walk 0 k = UNIT k) /\ 424 (random_walk (SUC n) k = 425 BIND sdest (\b. random_walk (if b then SUC (SUC n) else n) (SUC k)))``, 426 FUN_EQ_TAC 427 >> RW_TAC std_ss [random_walk_def, prob_while_cost_def] 428 >- RW_TAC arith_ss [prob_cost_def, PROB_WHILE_ADVANCE, 429 INDEP_FN_PROB_COST, PROB_TERMINATES_COST, 430 PROB_TERMINATES_RANDOM_WALK, INDEP_FN_RANDOM_LURCH, 431 o_THM, BIND_LEFT_UNIT] 432 >> CONV_TAC 433 (LAND_CONV 434 (SIMP_CONV arith_ss 435 [prob_cost_def, PROB_WHILE_ADVANCE, 436 INDEP_FN_PROB_COST, PROB_TERMINATES_COST, 437 PROB_TERMINATES_RANDOM_WALK, INDEP_FN_RANDOM_LURCH, 438 o_THM, BIND_LEFT_UNIT])) 439 >> RW_TAC arith_ss [BIND_DEF, UNIT_DEF, UNCURRY, o_THM, random_lurch_def, 440 ADD1]); 441 442val RANDOM_WALK_ML = store_thm 443 ("RANDOM_WALK_ML", 444 ``!n k. 445 random_walk n k = 446 if n = 0 then UNIT k 447 else coin_flip (random_walk (n + 1) (k + 1)) 448 (random_walk (n - 1) (k + 1))``, 449 Cases 450 >> RW_TAC (arith_ss ++ boolSimps.COND_elim_ss) 451 [RANDOM_WALK, ADD1, coin_flip_def]); 452 453val RANDOM_WALK_PARITY = store_thm 454 ("RANDOM_WALK_PARITY", 455 ``!n k. !*s. EVEN (FST (random_walk n k s)) = EVEN (n + k)``, 456 RW_TAC std_ss [random_walk_def] 457 >> Suff 458 `!s. 459 FST 460 (BIND 461 (prob_while_cost ($< 0) random_lurch (n,k)) (\x. UNIT (SND x)) s) = 462 SND (FST (prob_while_cost ($< 0) random_lurch (n, k) s))` 463 >- RW_TAC std_ss [RANDOM_LURCHES_PARITY] 464 >> RW_TAC std_ss [BIND_DEF, UNIT_DEF, UNCURRY, o_THM]); 465 466val _ = export_theory (); 467