1(* ------------------------------------------------------------------------- *) 2(* Load and open relevant theories *) 3(* (Comment out "load" and "quietdec"s for compilation) *) 4(* ------------------------------------------------------------------------- *) 5(* 6app load 7 ["bossLib","realLib","rich_listTheory","stringTheory", 8 "metisLib","posrealLib","expectationTheory","intLib", "wpTheory", "valueTheory", "arithmeticTheory"]; 9quietdec := true; 10*) 11 12open HolKernel Parse boolLib bossLib intLib realLib metisLib; 13open combinTheory listTheory rich_listTheory stringTheory arithmeticTheory 14 integerTheory realTheory posetTheory 15 16open posrealTheory posrealLib expectationTheory syntaxTheory wpTheory 17 valueTheory; 18 19(* 20quietdec := false; 21*) 22 23(* ------------------------------------------------------------------------- *) 24(* Start a new theory called "looprules" *) 25(* ------------------------------------------------------------------------- *) 26 27val _ = new_theory "looprules"; 28 29(* ------------------------------------------------------------------------- *) 30(* Helpful proof tools *) 31(* ------------------------------------------------------------------------- *) 32 33infixr 0 ++ << || THENC ORELSEC ORELSER ##; 34infix 1 >>; 35 36val op ++ = op THEN; 37val op << = op THENL; 38val op >> = op THEN1; 39val op || = op ORELSE; 40val Know = Q_TAC KNOW_TAC; 41val Suff = Q_TAC SUFF_TAC; 42val REVERSE = Tactical.REVERSE; 43val lemma = I prove; 44 45val let_imp_not_infty = store_thm 46 ("let_imp_not_infty", 47 ``!x:posreal. (?y. (y < infty) /\ (x <= y)) ==> 48 (~(x = infty))``, 49 METIS_TAC [let_trans, infty_le, preal_lt_def]); 50 51val le1_imp_not_infty = store_thm 52 ("le1_imp_not_infty", 53 ``!x:posreal. (x <= 1) ==> (~(x = infty))``, 54 `1 < infty` by RW_TAC posreal_ss [preal_lt_def] 55 ++ METIS_TAC [let_imp_not_infty]); 56 57val let_lemma = store_thm 58 ("let_lemma", 59 ``(let x = (a:posreal) in x * y) = a * y``, 60 RW_TAC std_ss []); 61 62val let_lin_lemma = store_thm 63 ("let_lin_lemma", 64 ``(let x = (a:posreal) in x * y + (1 - x) * z) = a * y + (1 - a) * z``, 65 RW_TAC std_ss []); 66 67val wp_assign = store_thm 68 ("wp_assign", 69 ``!v s postE. 70 wp (Assign v s) postE = 71 (\s'. postE (\w. (if w = v then s s' else s' w)))``, 72 RW_TAC std_ss [wp_def, assign_eta]); 73 74val wp_seq = store_thm 75 ("wp_seq", 76 ``!prog prog' postE. 77 wp (Seq prog prog') postE = 78 wp prog (wp prog' postE)``, 79 RW_TAC std_ss [wp_def]); 80 81val while_unwind_lemma = store_thm 82 ("while_unwind_lemma", 83 ``!g body Inv. 84 wp (While g body) Inv = (\s. if g s then wp body (wp (While g body) Inv) s else Inv s)``, 85 REPEAT STRIP_TAC 86 ++ RW_TAC posreal_ss [wp_def, cond_eta] 87 ++ `monotonic (expect,Leq) (\e s. (if g s then wp body e s else Inv s))` 88 by (RW_TAC std_ss [monotonic_def, Leq_def] 89 ++ Cases_on `g s` 90 >> METIS_TAC [wp_mono, Leq_def] 91 ++ RW_TAC posreal_ss [One_def]) 92 ++ `lfp (expect,Leq) (\e s. (if g s then wp body e s else Inv s)) 93 (expect_lfp (\e s. (if g s then wp body e s else Inv s)))` 94 by METIS_TAC [expect_lfp_def] 95 ++ FULL_SIMP_TAC std_ss [Leq_def, wp_def, cond_eta, lfp_def, expect_def]); 96 97val while_unwind_val_lemma = store_thm 98 ("while_unwind_val_lemma", 99 ``wp (While g (body:value command)) Inv = (\s. if g s then wp body (wp (While g body) Inv) s else Inv s)``, 100 REPEAT STRIP_TAC 101 ++ RW_TAC posreal_ss [wp_def, cond_eta] 102 ++ `monotonic (expect,Leq) (\e s. (if g s then wp body e s else Inv s))` 103 by (RW_TAC std_ss [monotonic_def, Leq_def] 104 ++ Cases_on `g s` 105 >> METIS_TAC [wp_mono, Leq_def] 106 ++ RW_TAC posreal_ss [One_def]) 107 ++ `lfp (expect,Leq) (\e s. (if g s then wp body e s else Inv s)) 108 (expect_lfp (\e s. (if g s then wp body e s else Inv s)))` 109 by METIS_TAC [expect_lfp_def] 110 ++ FULL_SIMP_TAC std_ss [Leq_def, wp_def, cond_eta, lfp_def, expect_def]); 111 112val INT_OF_NUM_POSINT_EQ = store_thm 113 ("INT_OF_NUM_POSINT_EQ", 114 ``!(x:int). (0 < x) ==> ((& (Num x)) = x)``, 115 REPEAT STRIP_TAC 116 ++ `?n. x = &n` by METIS_TAC [NUM_POSINT_EXISTS, INT_LT_IMP_LE] 117 ++ ASM_REWRITE_TAC [NUM_OF_INT]); 118 119val expect1_postE_imp_expect1_wp_postE = store_thm 120 ("expect1_postE_imp_expect1_wp_postE", 121 ``!prog postE. (expect1 postE) ==> (expect1 (wp prog postE))``, 122 METIS_TAC [sublinear_expect1, healthy_def, wp_healthy]); 123 124val Term_Leq_One = store_thm 125 ("Term_Leq_One", 126 ``!prog. Leq (wp prog One) One``, 127 `expect1(One)` 128 by RW_TAC posreal_ss [One_def, expect1_def] 129 ++ METIS_TAC [Leq_def, One_def, expect1_def, expect1_postE_imp_expect1_wp_postE]); 130 131val lt_trans = store_thm 132 ("lt_trans", 133 ``!(x:posreal) (y:posreal) (z:posreal). (x<y) /\ (y < z) ==> x < z``, 134 REPEAT STRIP_TAC 135 ++ `(x = 0) \/ (x = infty) \/ 136 ~(x = 0) /\ ?x'. ~(x' = 0) /\ 0 <= x' /\ (x = preal x')` 137 by METIS_TAC [posreal_trich] 138 ++ `(y = 0) \/ (y = infty) \/ 139 ~(y = 0) /\ ?y'. ~(y' = 0) /\ 0 <= y' /\ (y = preal y')` 140 by METIS_TAC [posreal_trich] 141 ++ `(z = 0) \/ (z = infty) \/ 142 ~(z = 0) /\ ?z'. ~(z' = 0) /\ 0 <= z' /\ (z = preal z')` 143 by METIS_TAC [posreal_trich] 144 ++ FULL_SIMP_TAC posreal_ss [preal_lt_def, zero_le, le_infty] 145 ++ Suff `preal x' < preal z'` >> METIS_TAC [preal_lt_def] 146 ++ `preal x' < preal y'` by METIS_TAC [preal_lt_def] 147 ++ `preal y' < preal z'` by METIS_TAC [preal_lt_def] 148 ++ METIS_TAC [lte_trans, lt_le] 149); 150 151val max_swap = store_thm 152 ("max_swap", 153 ``!x y z. (max (max x y) z) = (max y (max x z))``, 154 RW_TAC posreal_ss [preal_max_def, le_trans, le_antisym] 155 ++ METIS_TAC [le_antisym, preal_lt_def, lt_trans, le_total]); 156 157val mul_operands_le1_le1 = store_thm 158 ("mul_operands_le1_le1", 159 ``!(x:posreal)(y:posreal). 160 (x<=1) /\ (y<=1) ==> 161 (x*y <= 1)``, 162 RW_TAC posreal_ss [] 163 ++ `(x = 0) \/ (x = infty) \/ 164 ~(x = 0) /\ ?x'. ~(x' = 0) /\ 0 <= x' /\ (x = preal x')` 165 by METIS_TAC [posreal_trich] 166 ++ FULL_SIMP_TAC posreal_ss [] 167 ++ `(y = 0) \/ (y = infty) \/ 168 ~(y = 0) /\ ?y'. ~(y' = 0) /\ 0 <= y' /\ (y = preal y')` 169 by METIS_TAC [posreal_trich] 170 ++ FULL_SIMP_TAC posreal_ss [preal_mul] 171 ++ `((1:posreal) = (0:posreal)) \/ ((1:posreal) = infty) \/ 172 ~((1:posreal) = (0:posreal)) /\ ?one'. ~(one' = 0) /\ 0 <= one' /\ ((1:posreal) = preal one')` 173 by METIS_TAC [posreal_trich] 174 ++ FULL_SIMP_TAC posreal_ss [preal_le] 175 ++ MATCH_MP_TAC preal_le 176 ++ `one' = one' * one'` 177 by (`preal (one' * one') = preal one' * preal one'` 178 by METIS_TAC [preal_mul] 179 ++ `preal (one' * one') = (1:posreal)` 180 by (`(1:posreal)*(1:posreal)=(1:posreal)` 181 by RW_TAC posreal_ss [] 182 ++ METIS_TAC []) 183 ++ MATCH_MP_TAC preal_inj 184 ++ RW_TAC real_ss [REAL_LE_SQUARE]) 185 ++ Suff `x' * y' <= one' * one'` 186 >> METIS_TAC [] 187 ++ `x' <= one'` 188 by (MATCH_MP_TAC le_preal 189 ++ METIS_TAC []) 190 ++ `y' <= one'` 191 by (MATCH_MP_TAC le_preal 192 ++ METIS_TAC []) 193 ++ METIS_TAC [REAL_LE_MUL2]); 194 195val operand_le_one_imp_mul_le_one = store_thm 196 ("operand_le_one_imp_mul_le_one", 197 ``!(x:posreal)(y:posreal). 198 (x <= 1) ==> 199 (x*y <= y)``, 200 METIS_TAC [le_mul2, le_refl, mul_lone]); 201 202 203val mul_nonzero_operands_imp_nonzero_result = store_thm 204 ("mul_nonzero_operands_imp_nonzero_result", 205 ``!(x:posreal) (y:posreal). (0 < x) /\ (0 < y) ==> (0 < x * y)``, 206 RW_TAC posreal_ss [preal_lt_def, entire] 207 ++ `~(x <= 0)` by METIS_TAC [preal_lt_def] 208 ++ `~(y <= 0)` by METIS_TAC [preal_lt_def] 209 ++ METIS_TAC [le_zero]); 210 211val INT_LE_EQ_LT_ADD1 = store_thm 212 ("INT_LE_EQ_LT_ADD1", 213 ``(x:int) <= (y:int) = x < y + 1``, 214 REPEAT STRIP_TAC 215 ++ `x <= y ==> x < y + 1` by METIS_TAC [INT_LT_ADD1] 216 ++ `x < y + 1 ==> x <= y` 217 by (`(?x'. (x = & x') /\ ~(x' = 0)) \/ (?x'. (x = ~& x') /\ ~(x' = 0)) \/ 218 (x = 0)` by METIS_TAC [INT_NUM_CASES] 219 ++ `(?y'. (y = & y') /\ ~(y' = 0)) \/ (?y'. (y = ~& y') /\ ~(y' = 0)) \/ 220 (y = 0)` by METIS_TAC [INT_NUM_CASES] 221 ++ FULL_SIMP_TAC int_ss [INT_ADD_CALCULATE] 222 ++ Cases_on `y' <= 1` 223 ++ FULL_SIMP_TAC int_ss []) 224 ++ METIS_TAC []); 225 226val posreal_pow_def = Define 227 `(posreal_pow (e:posreal) 0 = 1) /\ 228 (posreal_pow (e:posreal) (SUC n) = e * (posreal_pow e n))`; 229 230val posreal_pow_1bounded_base_1bounded = store_thm 231 ("posreal_pow_1bounded_base_1bounded", 232 ``!e n. (e <= 1) ==> (posreal_pow e n <= 1)``, 233 RW_TAC posreal_ss [] 234 ++ Induct_on `n` 235 ++ RW_TAC posreal_ss [posreal_pow_def] 236 ++ METIS_TAC [mul_operands_le1_le1]); 237 238val posreal_pow_base1_eq_1 = store_thm 239 ("posreal_pow_base1_eq_1", 240 ``!n. posreal_pow 1 n = 1``, 241 Induct 242 ++ METIS_TAC [posreal_pow_def, mul_lone]); 243 244val zero_lt_posreal_pow = store_thm 245 ("zero_lt_posreal_pow", 246 ``!e n. (0 < e) ==> (0 < (posreal_pow e n))``, 247 GEN_TAC 248 ++ Induct_on `n` 249 ++ RW_TAC posreal_ss [posreal_pow_def] 250 ++ `0 < posreal_pow e n` 251 by METIS_TAC [] 252 ++ METIS_TAC [mul_nonzero_operands_imp_nonzero_result]); 253 254val NO_INT_BETWEEN_ZERO_AND_ONE = store_thm 255 ("NO_INT_BETWEEN_ZERO_AND_ONE", 256 ``!(x:int). ~(0<x /\ x < 1)``, 257 `1 = 0 + (1:int)` by RW_TAC int_ss [] 258 ++ METIS_TAC [INT_DISCRETE]); 259 260val variant_rule = store_thm 261 ("variant_rule", 262 ``!(g :'a state -> bool) (body :'a command) (Inv :'a state -> bool) 263 (H :int) (L :int) (e :posreal). 264 (0 :posreal) < e /\ e <= (1 :posreal) /\ 265 Leq 266 (\(s :'a state). 267 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 268 (wp body 269 (\(s :'a state). 270 (if Inv s then (1 :posreal) else (0 :posreal)))) /\ 271 Leq 272 (\(s :'a state). 273 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 274 (\(s :'a state). 275 (if L <= (Var :'a state -> int) s /\ Var s < H then 276 (1 : 277 posreal) 278 else 279 (0 : 280 posreal))) /\ 281 (!(N :int). 282 Leq 283 (\(s :'a state). 284 (if g s /\ Inv s /\ (Var s = N) then e else (0 :posreal))) 285 (wp body 286 (\(s :'a state). 287 (if Var s < N then (1 :posreal) else (0 :posreal))))) ==> 288 Leq 289 (\(s :'a state). 290 (if Inv s then posreal_pow e (Num (H - L)) else (0 :posreal))) 291 (wp (While g body) (One :'a state expect))``, 292RW_TAC std_ss [] 293++ `!(N :int). 294 Leq 295 (\(s :'a state). 296 (if 297 (g :'a state -> bool) s /\ (Inv :'a state -> bool) s /\ 298 ((Var :'a state -> int) s = N) 299 then 300 (e :posreal) 301 else 302 (0 : 303 posreal))) 304 (wp (body :'a command) 305 (\(s :'a state). 306 (if Inv s /\ Var s < N then (1 :posreal) else (0 :posreal))))` 307 by (GEN_TAC 308 ++ `wp (body :'a command) 309 (\(s :'a state). 310 (if 311 (Inv :'a state -> bool) s /\ (Var :'a state -> int) s < (N :int) 312 then 313 (1 : 314 posreal) 315 else 316 (0 : 317 posreal))) = 318 wp body 319 (Conj (\(s :'a state). (if Inv s then (1 :posreal) else (0 :posreal))) 320 (\(s :'a state). 321 (if Var s < N then (1 :posreal) else (0 :posreal))))` 322 by (`(\(s :'a state). 323 (if 324 (Inv :'a state -> bool) s /\ (Var :'a state -> int) s < (N :int) 325 then 326 (1 : 327 posreal) 328 else 329 (0 : 330 posreal))) = 331 Conj (\(s :'a state). (if Inv s then (1 :posreal) else (0 :posreal))) 332 (\(s :'a state). (if Var s < N then (1 :posreal) else (0 :posreal)))` 333 by (RW_TAC std_ss [FUN_EQ_THM, Conj_def] 334 ++ RW_TAC posreal_ss [] 335 ++ FULL_SIMP_TAC std_ss []) 336 ++ RW_TAC std_ss []) 337 ++ RW_TAC std_ss [] 338 ++ POP_ASSUM (K ALL_TAC) 339 ++ `Leq 340 (\(s :'a state). 341 (if 342 (g :'a state -> bool) s /\ (Inv :'a state -> bool) s /\ 343 ((Var :'a state -> int) s = (N :int)) 344 then 345 (e :posreal) 346 else 347 (0 : 348 posreal))) 349 (Conj 350 (\(s :'a state). 351 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 352 (\(s :'a state). 353 (if g s /\ Inv s /\ (Var s = N) then e else (0 :posreal))))` 354 by (RW_TAC std_ss [Leq_def, Conj_def] 355 ++ RW_TAC posreal_ss [add_comm, add_sub] 356 ++ FULL_SIMP_TAC posreal_ss []) 357 ++ Suff `Leq 358 (Conj 359 (\(s :'a state). 360 (if (g :'a state -> bool) s /\ (Inv :'a state -> bool) s then 361 (1 : 362 posreal) 363 else 364 (0 : 365 posreal))) 366 (\(s :'a state). 367 (if g s /\ Inv s /\ ((Var :'a state -> int) s = (N :int)) then 368 (e :posreal) 369 else 370 (0 : 371 posreal)))) 372 (wp (body :'a command) 373 (Conj 374 (\(s :'a state). (if Inv s then (1 :posreal) else (0 :posreal))) 375 (\(s :'a state). 376 (if Var s < N then (1 :posreal) else (0 :posreal)))))` 377 >> METIS_TAC [leq_trans] 378 ++ POP_ASSUM (K ALL_TAC) 379 ++ `Leq (Conj (wp body (\s. if Inv s then 1 else 0)) 380 (wp body (\s. if (Var s < N) then 1 else 0))) 381 (wp body (Conj (\s. (if Inv s then 1 else 0)) 382 (\s. (if Var s < N then 1 else 0))))` 383 by METIS_TAC [wp_conj] 384 ++ Suff `Leq (Conj (\s. (if g s /\ Inv s then 1 else 0)) 385 (\s. (if g s /\ Inv s /\ (Var s = N) then e else 0))) 386 (Conj (wp body (\s. (if Inv s then 1 else 0))) 387 (wp body (\s. (if Var s < N then 1 else 0))))` 388 >> METIS_TAC [leq_trans] 389 ++ POP_ASSUM (K ALL_TAC) 390 ++ FULL_SIMP_TAC std_ss [Leq_def, Conj_def] 391 ++ GEN_TAC 392 ++ MATCH_MP_TAC sub_mono 393 ++ SIMP_TAC posreal_ss [] 394 ++ METIS_TAC [le_add2]) 395++ `!(n :num). 396 Leq 397 (\(s :'a state). 398 (if 399 (Inv :'a state -> bool) s /\ 400 (Var :'a state -> int) s < (L :int) + (& n :int) 401 then 402 posreal_pow (e :posreal) n 403 else 404 (0 : 405 posreal))) 406 (wp 407 (While (\(s :'a state). (g :'a state -> bool) s) 408 (body :'a command)) (One :'a state expect))` 409 by (GEN_TAC 410 ++ Induct_on `n` 411 >> (RW_TAC int_ss [posreal_pow_def] 412 ++ `Leq 413 (\(s :'a state). 414 (if 415 (Inv :'a state -> bool) s /\ (Var :'a state -> int) s < (L :int) 416 then 417 (1 : 418 posreal) 419 else 420 (0 : 421 posreal))) 422 (\(s :'a state). 423 (if ~(g :'a state -> bool) s then (1 :posreal) else (0 :posreal)))` 424 by (FULL_SIMP_TAC std_ss [Leq_def] 425 ++ GEN_TAC 426 ++ RW_TAC posreal_ss [] 427 ++ `(if 428 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s 429 then 430 (1 : 431 posreal) 432 else 433 (0 : 434 posreal)) <= 435 (if (L :int) <= (Var :'a state -> int) s /\ Var s < (H :int) then 436 (1 : 437 posreal) 438 else 439 (0 : 440 posreal))` 441 by METIS_TAC [] 442 ++ `(if 443 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s 444 then 445 (1 : 446 posreal) 447 else 448 (0 : 449 posreal)) = 450 (1 : 451 posreal)` 452 by RW_TAC posreal_ss [] 453 ++ `(if 454 (L :int) <= (Var :'a state -> int) (s :'a state) /\ Var s < (H :int) 455 then 456 (1 : 457 posreal) 458 else 459 (0 : 460 posreal)) = 461 (0 : 462 posreal)` 463 by (RW_TAC posreal_ss [] 464 ++ FULL_SIMP_TAC int_ss [int_le]) 465 ++ `~((1:posreal)<=(0:posreal))` 466 by RW_TAC posreal_ss [le_zero] 467 ++ FULL_SIMP_TAC posreal_ss []) 468 ++ `Leq 469 (\(s :'a state). 470 (if ~(g :'a state -> bool) s then (1 :posreal) else (0 :posreal))) 471 (wp (While (\(s :'a state). g s) (body :'a command)) 472 (One :'a state expect))` 473 by (FULL_SIMP_TAC std_ss [Leq_def] 474 ++ GEN_TAC 475 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 476 ++ `monotonic 477 ((expect :'a state expect -> bool), 478 (Leq :'a state expect -> 'a state expect -> bool)) 479 (\(e :'a state expect) (s :'a state). 480 (if (g :'a state -> bool) s then 481 wp (body :'a command) e s 482 else 483 One s))` 484 by (RW_TAC std_ss [monotonic_def, Leq_def] 485 ++ Cases_on `g s'` 486 >> METIS_TAC [wp_mono, Leq_def] 487 ++ RW_TAC posreal_ss [One_def]) 488 ++ `lfp 489 ((expect :'a state expect -> bool), 490 (Leq :'a state expect -> 'a state expect -> bool)) 491 (\(e :'a state expect) (s :'a state). 492 (if (g :'a state -> bool) s then 493 wp (body :'a command) e s 494 else 495 One s)) 496 (expect_lfp 497 (\(e :'a state expect) (s :'a state). 498 (if g s then wp body e s else One s)))` 499 by METIS_TAC [expect_lfp_def] 500 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 501 ++ Suff `(1 :posreal) <= 502 (\(s :'a state). 503 (if (g :'a state -> bool) s then 504 wp (body :'a command) 505 (expect_lfp 506 (\(e :'a state expect) (s :'a state). 507 (if g s then wp body e s else One s))) s 508 else 509 One s)) (s :'a state)` 510 >> METIS_TAC [] 511 ++ RW_TAC posreal_ss [One_def]) 512 ++ METIS_TAC [leq_trans]) 513 ++ `Leq 514 (\(s :'a state). 515 (if 516 (Inv :'a state -> bool) s /\ 517 (Var :'a state -> int) s < (L :int) + (& (SUC (n :num)) :int) 518 then 519 posreal_pow (e :posreal) (SUC n) 520 else 521 (0 : 522 posreal))) 523 (Max 524 (\(s :'a state). 525 (\(s :'a state). 526 (if (g :'a state -> bool) s then 527 (1 : 528 posreal) 529 else 530 (0 : 531 posreal))) s * 532 (\(s :'a state). 533 (if Inv s /\ Var s < L + (& (SUC n) :int) then 534 posreal_pow e (SUC n) 535 else 536 (0 : 537 posreal))) s) 538 (\(s :'a state). 539 (\(s :'a state). (if ~g s then (1 :posreal) else (0 :posreal))) 540 s * 541 (\(s :'a state). 542 (if Inv s /\ Var s < L + (& (SUC n) :int) then 543 posreal_pow e (SUC n) 544 else 545 (0 : 546 posreal))) s))` 547 by (RW_TAC std_ss [Max_def, Leq_def] 548 ++ Cases_on `g s` 549 ++ RW_TAC posreal_ss []) 550 ++ Suff `Leq 551 (Max 552 (\(s :'a state). 553 (\(s :'a state). 554 (if (g :'a state -> bool) s then 555 (1 : 556 posreal) 557 else 558 (0 : 559 posreal))) s * 560 (\(s :'a state). 561 (if 562 (Inv :'a state -> bool) s /\ 563 (Var :'a state -> int) s < 564 (L :int) + (& (SUC (n :num)) :int) 565 then 566 posreal_pow (e :posreal) (SUC n) 567 else 568 (0 : 569 posreal))) s) 570 (\(s :'a state). 571 (\(s :'a state). (if ~g s then (1 :posreal) else (0 :posreal))) 572 s * 573 (\(s :'a state). 574 (if Inv s /\ Var s < L + (& (SUC n) :int) then 575 posreal_pow e (SUC n) 576 else 577 (0 : 578 posreal))) s)) 579 (wp (While (\(s :'a state). g s) (body :'a command)) 580 (One :'a state expect))` 581 >> METIS_TAC [leq_trans] 582 ++ POP_ASSUM (K ALL_TAC) 583 ++ `Leq 584 (\(s :'a state). 585 (if ~(g :'a state -> bool) s then (1 :posreal) else (0 :posreal))) 586 (wp (While (\(s :'a state). g s) (body :'a command)) 587 (One :'a state expect))` 588 by (FULL_SIMP_TAC std_ss [Leq_def] 589 ++ GEN_TAC 590 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 591 ++ `monotonic 592 ((expect :'a state expect -> bool), 593 (Leq :'a state expect -> 'a state expect -> bool)) 594 (\(e :'a state expect) (s :'a state). 595 (if (g :'a state -> bool) s then 596 wp (body :'a command) e s 597 else 598 One s))` 599 by (RW_TAC std_ss [monotonic_def, Leq_def] 600 ++ Cases_on `g s'` 601 >> METIS_TAC [wp_mono, Leq_def] 602 ++ RW_TAC posreal_ss [One_def]) 603 ++ `lfp 604 ((expect :'a state expect -> bool), 605 (Leq :'a state expect -> 'a state expect -> bool)) 606 (\(e :'a state expect) (s :'a state). 607 (if (g :'a state -> bool) s then 608 wp (body :'a command) e s 609 else 610 One s)) 611 (expect_lfp 612 (\(e :'a state expect) (s :'a state). 613 (if g s then wp body e s else One s)))` 614 by METIS_TAC [expect_lfp_def] 615 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 616 ++ Suff `(1 :posreal) <= 617 (\(s :'a state). 618 (if (g :'a state -> bool) s then 619 wp (body :'a command) 620 (expect_lfp 621 (\(e :'a state expect) (s :'a state). 622 (if g s then wp body e s else One s))) s 623 else 624 One s)) (s :'a state)` 625 >> METIS_TAC [] 626 ++ RW_TAC posreal_ss [One_def]) 627 ++ `Leq 628 (Max 629 (\(s :'a state). 630 (\(s :'a state). 631 (if (g :'a state -> bool) s then 632 (1 : 633 posreal) 634 else 635 (0 : 636 posreal))) s * 637 (\(s :'a state). 638 (if 639 (Inv :'a state -> bool) s /\ 640 (Var :'a state -> int) s < 641 (L :int) + (& (SUC (n :num)) :int) 642 then 643 posreal_pow (e :posreal) (SUC n) 644 else 645 (0 : 646 posreal))) s) 647 (\(s :'a state). 648 (\(s :'a state). (if ~g s then (1 :posreal) else (0 :posreal))) 649 s * 650 (\(s :'a state). 651 (if Inv s /\ Var s < L + (& (SUC n) :int) then 652 posreal_pow e (SUC n) 653 else 654 (0 : 655 posreal))) s)) 656 (Max 657 (\(s :'a state). 658 (\(s :'a state). (if g s then (1 :posreal) else (0 :posreal))) 659 s * 660 (\(s :'a state). 661 (if Inv s /\ Var s < L + (& (SUC n) :int) then 662 posreal_pow e (SUC n) 663 else 664 (0 : 665 posreal))) s) 666 (wp (While (\(s :'a state). g s) (body :'a command)) 667 (One :'a state expect)))` 668 by (RW_TAC posreal_ss [Leq_def, Max_def] 669 ++ Cases_on `g s` 670 ++ RW_TAC posreal_ss [] 671 ++ Suff `posreal_pow (e :posreal) (SUC (n :num)) <= (1 :posreal)` 672 >> (`(1 :posreal) <= 673 wp (While (\(s :'a state). (g :'a state -> bool) s) (body :'a command)) 674 (One :'a state expect) (s :'a state)` 675 by (FULL_SIMP_TAC posreal_ss [Leq_def] 676 ++ METIS_TAC []) 677 ++ METIS_TAC [le_trans]) 678 ++ METIS_TAC [posreal_pow_1bounded_base_1bounded]) 679 ++ Suff `Leq 680 (Max 681 (\(s :'a state). 682 (\(s :'a state). 683 (if (g :'a state -> bool) s then 684 (1 : 685 posreal) 686 else 687 (0 : 688 posreal))) s * 689 (\(s :'a state). 690 (if 691 (Inv :'a state -> bool) s /\ 692 (Var :'a state -> int) s < 693 (L :int) + (& (SUC (n :num)) :int) 694 then 695 posreal_pow (e :posreal) (SUC n) 696 else 697 (0 : 698 posreal))) s) 699 (wp (While (\(s :'a state). g s) (body :'a command)) 700 (One :'a state expect))) 701 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 702 >> METIS_TAC [leq_trans] 703 ++ POP_ASSUM (K ALL_TAC) 704 ++ `Leq 705 (Max 706 (\(s :'a state). 707 (\(s :'a state). 708 (if (g :'a state -> bool) s then 709 (1 : 710 posreal) 711 else 712 (0 : 713 posreal))) s * 714 (\(s :'a state). 715 (if 716 (Inv :'a state -> bool) s /\ 717 (Var :'a state -> int) s < 718 (L :int) + (& (SUC (n :num)) :int) 719 then 720 posreal_pow (e :posreal) (SUC n) 721 else 722 (0 : 723 posreal))) s) 724 (wp (While (\(s :'a state). g s) (body :'a command)) 725 (One :'a state expect))) 726 (Max 727 (Max 728 (\(s :'a state). 729 (if g s /\ Inv s /\ Var s < L + (& n :int) then 730 posreal_pow e (SUC n) 731 else 732 (0 : 733 posreal))) 734 (\(s :'a state). 735 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 736 posreal_pow e (SUC n) 737 else 738 (0 : 739 posreal)))) 740 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 741 by (RW_TAC posreal_ss [Leq_def, Max_def] 742 ++ `(Var :'a state -> int) (s :'a state) < 743 (L :int) + (& (SUC (n :num)) :int) = 744 Var s <= L + (& n :int)` 745 by RW_TAC int_ss [INT, INT_ADD_ASSOC, INT_LE_EQ_LT_ADD1] 746 ++ `(Var :'a state -> int) (s :'a state) <= (L :int) + (& (n :num) :int) = 747 Var s < L + (& n :int) \/ (Var s = L + (& n :int))` 748 by RW_TAC int_ss [INT_LE_LT] 749 ++ ASM_REWRITE_TAC [] 750 ++ POP_ASSUM (K ALL_TAC) 751 ++ POP_ASSUM (K ALL_TAC) 752 ++ Cases_on `Var s < L + &n` 753 ++ ASM_REWRITE_TAC [] 754 ++ Cases_on `g s` 755 ++ ASM_REWRITE_TAC [] 756 ++ RW_TAC int_ss [max_lzero, mul_lone, mul_lzero, max_refl] 757 ++ RW_TAC posreal_ss [zero_lt_posreal_pow]) 758 ++ Suff `Leq 759 (Max 760 (Max 761 (\(s :'a state). 762 (if 763 (g :'a state -> bool) s /\ (Inv :'a state -> bool) s /\ 764 (Var :'a state -> int) s < (L :int) + (& (n :num) :int) 765 then 766 posreal_pow (e :posreal) (SUC n) 767 else 768 (0 : 769 posreal))) 770 (\(s :'a state). 771 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 772 posreal_pow e (SUC n) 773 else 774 (0 : 775 posreal)))) 776 (wp (While (\(s :'a state). g s) (body :'a command)) 777 (One :'a state expect))) 778 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 779 >> METIS_TAC [leq_trans] 780 ++ POP_ASSUM (K ALL_TAC) 781 ++ `Leq 782 (Max 783 (Max 784 (\(s :'a state). 785 (if 786 (g :'a state -> bool) s /\ (Inv :'a state -> bool) s /\ 787 (Var :'a state -> int) s < (L :int) + (& (n :num) :int) 788 then 789 posreal_pow (e :posreal) (SUC n) 790 else 791 (0 : 792 posreal))) 793 (\(s :'a state). 794 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 795 posreal_pow e (SUC n) 796 else 797 (0 : 798 posreal)))) 799 (wp (While (\(s :'a state). g s) (body :'a command)) 800 (One :'a state expect))) 801 (Max 802 (Max 803 (\(s :'a state). 804 e * 805 wp (While (\(s :'a state). g s) body) (One :'a state expect) 806 s) 807 (\(s :'a state). 808 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 809 posreal_pow e (SUC n) 810 else 811 (0 : 812 posreal)))) 813 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 814 by (RW_TAC posreal_ss [Leq_def, Max_def] 815 ++ `!(x :posreal). (e :posreal) * x <= x` 816 by METIS_TAC [mul_lone, le_refl, le_mul2] 817 ++ RW_TAC posreal_ss [] 818 ++ FULL_SIMP_TAC int_ss [DE_MORGAN_THM, INT_LT_IMP_NE, Leq_def] 819 ++ RW_TAC std_ss [posreal_pow_def] 820 ++ `max 821 ((e :posreal) * 822 wp 823 (While (\(s :'a state). (g :'a state -> bool) s) 824 (body :'a command)) (One :'a state expect) (s :'a state)) 825 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s) = 826 wp (While (\(s :'a state). g s) body) (One :'a state expect) s` 827 by METIS_TAC [preal_max_def] 828 ++ `max 829 (max 830 ((e :posreal) * 831 wp 832 (While (\(s :'a state). (g :'a state -> bool) s) 833 (body :'a command)) (One :'a state expect) (s :'a state)) 834 (e * posreal_pow e (n :num))) 835 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s) = 836 max (e * posreal_pow e n) 837 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s)` 838 by METIS_TAC [max_swap, preal_max_def] 839 ++ METIS_TAC [preal_max_def, le_trans, le_refl]) 840 ++ Suff `Leq 841 (Max 842 (Max 843 (\(s :'a state). 844 (e :posreal) * 845 wp 846 (While (\(s :'a state). (g :'a state -> bool) s) 847 (body :'a command)) (One :'a state expect) s) 848 (\(s :'a state). 849 (if 850 g s /\ (Inv :'a state -> bool) s /\ 851 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 852 then 853 posreal_pow e (SUC n) 854 else 855 (0 : 856 posreal)))) 857 (wp (While (\(s :'a state). g s) body) (One :'a state expect))) 858 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 859 >> METIS_TAC [leq_trans] 860 ++ POP_ASSUM (K ALL_TAC) 861 ++ `Leq 862 (Max 863 (Max 864 (\(s :'a state). 865 (e :posreal) * 866 wp 867 (While (\(s :'a state). (g :'a state -> bool) s) 868 (body :'a command)) (One :'a state expect) s) 869 (\(s :'a state). 870 (if 871 g s /\ (Inv :'a state -> bool) s /\ 872 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 873 then 874 posreal_pow e (SUC n) 875 else 876 (0 : 877 posreal)))) 878 (wp (While (\(s :'a state). g s) body) (One :'a state expect))) 879 (Max 880 (\(s :'a state). 881 posreal_pow e n * 882 wp body 883 (\(s :'a state). 884 (if Inv s /\ Var s < L + (& n :int) then 885 (1 : 886 posreal) 887 else 888 (0 : 889 posreal))) s) 890 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 891 by (RW_TAC posreal_ss [Leq_def, Max_def] 892 ++ `!(x :posreal). (e :posreal) * x <= x` 893 by METIS_TAC [mul_lone, le_refl, le_mul2] 894 ++ `max 895 (max 896 ((e :posreal) * 897 wp 898 (While (\(s :'a state). (g :'a state -> bool) s) 899 (body :'a command)) (One :'a state expect) (s :'a state)) 900 (if 901 g s /\ (Inv :'a state -> bool) s /\ 902 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 903 then 904 posreal_pow e (SUC n) 905 else 906 (0 : 907 posreal))) 908 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s) = 909 max 910 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 911 posreal_pow e (SUC n) 912 else 913 (0 : 914 posreal)) 915 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s)` 916 by (`max 917 (max 918 ((e :posreal) * 919 wp 920 (While (\(s :'a state). (g :'a state -> bool) s) 921 (body :'a command)) (One :'a state expect) (s :'a state)) 922 (if 923 g s /\ (Inv :'a state -> bool) s /\ 924 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 925 then 926 posreal_pow e (SUC n) 927 else 928 (0 : 929 posreal))) 930 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s) = 931 max 932 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then 933 posreal_pow e (SUC n) 934 else 935 (0 : 936 posreal)) 937 (max 938 (e * 939 wp (While (\(s :'a state). g s) body) (One :'a state expect) s) 940 (wp (While (\(s :'a state). g s) body) (One :'a state expect) s))` 941 by METIS_TAC [max_swap] 942 ++ METIS_TAC [preal_max_def]) 943 ++ ASM_REWRITE_TAC [] 944 ++ POP_ASSUM (K ALL_TAC) 945 ++ `(if 946 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s /\ 947 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 948 then 949 posreal_pow (e :posreal) (SUC n) 950 else 951 (0 : 952 posreal)) = 953 posreal_pow e n * 954 (if g s /\ Inv s /\ (Var s = L + (& n :int)) then e else (0 :posreal))` 955 by RW_TAC posreal_ss [posreal_pow_def, mul_comm, mul_rzero] 956 ++ ASM_REWRITE_TAC [] 957 ++ POP_ASSUM (K ALL_TAC) 958 ++ `posreal_pow (e :posreal) (n :num) * 959 (if 960 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s /\ 961 ((Var :'a state -> int) s = (L :int) + (& n :int)) 962 then 963 e 964 else 965 (0 : 966 posreal)) <= 967 posreal_pow e n * 968 wp (body :'a command) 969 (\(s :'a state). 970 (if Inv s /\ Var s < L + (& n :int) then 971 (1 : 972 posreal) 973 else 974 (0 : 975 posreal))) s` 976 by (`(if 977 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s /\ 978 ((Var :'a state -> int) s = (L :int) + (& (n :num) :int)) 979 then 980 (e :posreal) 981 else 982 (0 : 983 posreal)) <= 984 wp (body :'a command) 985 (\(s :'a state). 986 (if Inv s /\ Var s < L + (& n :int) then 987 (1 : 988 posreal) 989 else 990 (0 : 991 posreal))) s` 992 by (FULL_SIMP_TAC posreal_ss [Leq_def] 993 ++ METIS_TAC []) 994 ++ METIS_TAC [le_refl, le_mul2]) 995 ++ RW_TAC posreal_ss [preal_max_def, le_refl, le_trans] 996 ++ METIS_TAC [le_trans, le_total]) 997 ++ Suff `Leq 998 (Max 999 (\(s :'a state). 1000 posreal_pow (e :posreal) (n :num) * 1001 wp (body :'a command) 1002 (\(s :'a state). 1003 (if 1004 (Inv :'a state -> bool) s /\ 1005 (Var :'a state -> int) s < (L :int) + (& n :int) 1006 then 1007 (1 : 1008 posreal) 1009 else 1010 (0 : 1011 posreal))) s) 1012 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1013 (One :'a state expect))) 1014 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1015 >> METIS_TAC [leq_trans] 1016 ++ POP_ASSUM (K ALL_TAC) 1017 ++ `(\(s :'a state). 1018 posreal_pow (e :posreal) (n :num) * 1019 wp (body :'a command) 1020 (\(s :'a state). 1021 (if 1022 (Inv :'a state -> bool) s /\ 1023 (Var :'a state -> int) s < (L :int) + (& n :int) 1024 then 1025 (1 : 1026 posreal) 1027 else 1028 (0 : 1029 posreal))) s) = 1030 wp body 1031 (\(s :'a state). 1032 (if Inv s /\ Var s < L + (& n :int) then 1033 posreal_pow e n 1034 else 1035 (0 : 1036 posreal)))` 1037 by (RW_TAC std_ss [FUN_EQ_THM] 1038 ++ `(\(s :'a state). 1039 (if 1040 (Inv :'a state -> bool) s /\ 1041 (Var :'a state -> int) s < (L :int) + (& (n :num) :int) 1042 then 1043 posreal_pow (e :posreal) n 1044 else 1045 (0 : 1046 posreal))) = 1047 (\(s :'a state). 1048 posreal_pow e n * 1049 (if Inv s /\ Var s < L + (& n :int) then 1050 (1 : 1051 posreal) 1052 else 1053 (0 : 1054 posreal)))` 1055 by METIS_TAC [FUN_EQ_THM, mul_rone, mul_rzero] 1056 ++ ASM_REWRITE_TAC [] 1057 ++ POP_ASSUM (K ALL_TAC) 1058 ++ `posreal_pow (e :posreal) (n :num) * 1059 wp (body :'a command) 1060 (\(s :'a state). 1061 (if 1062 (Inv :'a state -> bool) s /\ 1063 (Var :'a state -> int) s < (L :int) + (& n :int) 1064 then 1065 (1 : 1066 posreal) 1067 else 1068 (0 : 1069 posreal))) (s :'a state) = 1070 wp body 1071 (\(s :'a state). 1072 posreal_pow e n * 1073 (\(s :'a state). 1074 (if Inv s /\ Var s < L + (& n :int) then 1075 (1 : 1076 posreal) 1077 else 1078 (0 : 1079 posreal))) s) s` 1080 by METIS_TAC [wp_scale] 1081 ++ METIS_TAC []) 1082 ++ ASM_REWRITE_TAC [] 1083 ++ POP_ASSUM (K ALL_TAC) 1084 ++ `Leq 1085 (Max 1086 (wp (body :'a command) 1087 (\(s :'a state). 1088 (if 1089 (Inv :'a state -> bool) s /\ 1090 (Var :'a state -> int) s < (L :int) + (& (n :num) :int) 1091 then 1092 posreal_pow (e :posreal) n 1093 else 1094 (0 : 1095 posreal)))) 1096 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1097 (One :'a state expect))) 1098 (Max 1099 (wp body 1100 (wp (While (\(s :'a state). g s) body) (One :'a state expect))) 1101 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 1102 by (`Leq 1103 (wp (body :'a command) 1104 (\(s :'a state). 1105 (if 1106 (Inv :'a state -> bool) s /\ 1107 (Var :'a state -> int) s < (L :int) + (& (n :num) :int) 1108 then 1109 posreal_pow (e :posreal) n 1110 else 1111 (0 : 1112 posreal)))) 1113 (wp body 1114 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1115 (One :'a state expect)))` 1116 by METIS_TAC [wp_mono] 1117 ++ RW_TAC posreal_ss [Leq_def, Max_def] 1118 ++ FULL_SIMP_TAC posreal_ss [Leq_def] 1119 ++ RW_TAC posreal_ss [preal_max_def, le_refl, le_trans] 1120 ++ METIS_TAC [le_trans, le_total]) 1121 ++ Suff `Leq 1122 (Max 1123 (wp (body :'a command) 1124 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1125 (One :'a state expect))) 1126 (wp (While (\(s :'a state). g s) body) (One :'a state expect))) 1127 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1128 >> METIS_TAC [leq_trans] 1129 ++ POP_ASSUM (K ALL_TAC) 1130 ++ `Leq 1131 (wp (body :'a command) 1132 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1133 (One :'a state expect))) 1134 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1135 by (`monotonic 1136 ((expect :'a state expect -> bool), 1137 (Leq :'a state expect -> 'a state expect -> bool)) 1138 (\(e :'a state expect) (s :'a state). 1139 (if (g :'a state -> bool) s then 1140 wp (body :'a command) e s 1141 else 1142 One s))` 1143 by (RW_TAC std_ss [monotonic_def, Leq_def] 1144 ++ Cases_on `g s` 1145 >> METIS_TAC [wp_mono, Leq_def] 1146 ++ RW_TAC posreal_ss [One_def]) 1147 ++ `lfp 1148 ((expect :'a state expect -> bool), 1149 (Leq :'a state expect -> 'a state expect -> bool)) 1150 (\(e :'a state expect) (s :'a state). 1151 (if (g :'a state -> bool) s then 1152 wp (body :'a command) e s 1153 else 1154 One s)) 1155 (expect_lfp 1156 (\(e :'a state expect) (s :'a state). 1157 (if g s then wp body e s else One s)))` 1158 by METIS_TAC [expect_lfp_def] 1159 ++ FULL_SIMP_TAC std_ss [Leq_def, wp_def, cond_eta, lfp_def, expect_def] 1160 ++ GEN_TAC 1161 ++ Suff `wp (body :'a command) 1162 (expect_lfp 1163 (\(e :'a state expect) (s :'a state). 1164 (if (g :'a state -> bool) s then wp body e s else One s))) 1165 (s :'a state) <= 1166 (\(s :'a state). 1167 (if g s then 1168 wp body 1169 (expect_lfp 1170 (\(e :'a state expect) (s :'a state). 1171 (if g s then wp body e s else One s))) s 1172 else 1173 One s)) s` 1174 >> METIS_TAC [] 1175 ++ RW_TAC posreal_ss [le_refl, One_def] 1176 ++ `expect_lfp 1177 (\(e :'a state expect) (s :'a state). 1178 (if (g :'a state -> bool) s then 1179 wp (body :'a command) e s 1180 else 1181 (1 : 1182 posreal))) = 1183 wp (While (\(s :'a state). g s) body) (One :'a state expect)` 1184 by RW_TAC posreal_ss [wp_def, cond_eta, One_def] 1185 ++ ASM_REWRITE_TAC [] 1186 ++ POP_ASSUM (K ALL_TAC) 1187 ++ `wp (body :'a command) 1188 (wp (While (\(s :'a state). (g :'a state -> bool) s) body) 1189 (One :'a state expect)) (s :'a state) = 1190 wp (Seq body (While (\(s :'a state). g s) body)) (One :'a state expect) 1191 s` 1192 by RW_TAC posreal_ss [wp_def] 1193 ++ ASM_REWRITE_TAC [] 1194 ++ POP_ASSUM (K ALL_TAC) 1195 ++ METIS_TAC [Leq_def, One_def, Term_Leq_One]) 1196 ++ FULL_SIMP_TAC posreal_ss [Leq_def, Max_def, preal_max_def, le_refl]) 1197++ `(\(s :'a state). 1198 (if (Inv :'a state -> bool) s then 1199 posreal_pow (e :posreal) (Num ((H :int) - (L :int))) 1200 else 1201 (0 : 1202 posreal))) = 1203 Max 1204 (\(s :'a state). 1205 (if (g :'a state -> bool) s /\ Inv s then 1206 posreal_pow e (Num (H - L)) 1207 else 1208 (0 : 1209 posreal))) 1210 (\(s :'a state). 1211 (if ~g s /\ Inv s then 1212 posreal_pow e (Num (H - L)) 1213 else 1214 (0 : 1215 posreal)))` 1216 by (RW_TAC posreal_ss [FUN_EQ_THM, Max_def] 1217 ++ Cases_on `g s` 1218 ++ METIS_TAC [max_lzero, max_rzero]) 1219 ++ ASM_REWRITE_TAC [] 1220 ++ POP_ASSUM (K ALL_TAC) 1221 ++ `Leq 1222 (\(s :'a state). 1223 (if ~(g :'a state -> bool) s then (1 :posreal) else (0 :posreal))) 1224 (wp (While (\(s :'a state). g s) (body :'a command)) 1225 (One :'a state expect))` 1226 by (FULL_SIMP_TAC std_ss [Leq_def] 1227 ++ GEN_TAC 1228 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 1229 ++ `monotonic 1230 ((expect :'a state expect -> bool), 1231 (Leq :'a state expect -> 'a state expect -> bool)) 1232 (\(e :'a state expect) (s :'a state). 1233 (if (g :'a state -> bool) s then 1234 wp (body :'a command) e s 1235 else 1236 One s))` 1237 by (RW_TAC std_ss [monotonic_def, Leq_def] 1238 ++ Cases_on `g s'` 1239 >> METIS_TAC [wp_mono, Leq_def] 1240 ++ RW_TAC posreal_ss [One_def]) 1241 ++ `lfp 1242 ((expect :'a state expect -> bool), 1243 (Leq :'a state expect -> 'a state expect -> bool)) 1244 (\(e :'a state expect) (s :'a state). 1245 (if (g :'a state -> bool) s then 1246 wp (body :'a command) e s 1247 else 1248 One s)) 1249 (expect_lfp 1250 (\(e :'a state expect) (s :'a state). 1251 (if g s then wp body e s else One s)))` 1252 by METIS_TAC [expect_lfp_def] 1253 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 1254 ++ Suff `(1 :posreal) <= 1255 (\(s :'a state). 1256 (if (g :'a state -> bool) s then 1257 wp (body :'a command) 1258 (expect_lfp 1259 (\(e :'a state expect) (s :'a state). 1260 (if g s then wp body e s else One s))) s 1261 else 1262 One s)) (s :'a state)` 1263 >> METIS_TAC [] 1264 ++ RW_TAC posreal_ss [One_def]) 1265 ++ `Leq 1266 (Max 1267 (\(s :'a state). 1268 (if (g :'a state -> bool) s /\ (Inv :'a state -> bool) s then 1269 posreal_pow (e :posreal) (Num ((H :int) - (L :int))) 1270 else 1271 (0 : 1272 posreal))) 1273 (\(s :'a state). 1274 (if ~g s /\ Inv s then 1275 posreal_pow e (Num (H - L)) 1276 else 1277 (0 : 1278 posreal)))) 1279 (Max 1280 (\(s :'a state). 1281 (if g s /\ Inv s then 1282 posreal_pow e (Num (H - L)) 1283 else 1284 (0 : 1285 posreal))) 1286 (wp (While (\(s :'a state). g s) (body :'a command)) 1287 (One :'a state expect)))` 1288 by (FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 1289 ++ GEN_TAC 1290 ++ Cases_on `g s` 1291 ++ RW_TAC posreal_ss [preal_max_def, max_lzero, max_rzero] 1292 ++ METIS_TAC [le_trans, posreal_pow_1bounded_base_1bounded]) 1293 ++ Suff `Leq 1294 (Max 1295 (\(s :'a state). 1296 (if (g :'a state -> bool) s /\ (Inv :'a state -> bool) s then 1297 posreal_pow (e :posreal) (Num ((H :int) - (L :int))) 1298 else 1299 (0 : 1300 posreal))) 1301 (wp (While (\(s :'a state). g s) (body :'a command)) 1302 (One :'a state expect))) 1303 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1304 >> METIS_TAC [leq_trans] 1305 ++ POP_ASSUM (K ALL_TAC) 1306 ++ `Leq 1307 (Max 1308 (\(s :'a state). 1309 (if (g :'a state -> bool) s /\ (Inv :'a state -> bool) s then 1310 posreal_pow (e :posreal) (Num ((H :int) - (L :int))) 1311 else 1312 (0 : 1313 posreal))) 1314 (wp (While (\(s :'a state). g s) (body :'a command)) 1315 (One :'a state expect))) 1316 (Max 1317 (\(s :'a state). 1318 (if Inv s /\ L <= (Var :'a state -> int) s /\ Var s < H then 1319 posreal_pow e (Num (H - L)) 1320 else 1321 (0 : 1322 posreal))) 1323 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 1324 by (FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 1325 ++ GEN_TAC 1326 ++ `(if 1327 (g :'a state -> bool) (s :'a state) /\ (Inv :'a state -> bool) s 1328 then 1329 posreal_pow (e :posreal) (Num ((H :int) - (L :int))) 1330 else 1331 (0 : 1332 posreal)) <= 1333 (if Inv s /\ L <= (Var :'a state -> int) s /\ Var s < H then 1334 posreal_pow e (Num (H - L)) 1335 else 1336 (0 : 1337 posreal))` 1338 by (Cases_on `g s /\ Inv s` 1339 >> (`(L :int) <= (Var :'a state -> int) (s :'a state) /\ Var s < (H :int)` 1340 by (`(1 :posreal) <= 1341 (if 1342 (L :int) <= (Var :'a state -> int) (s :'a state) /\ Var s < (H :int) 1343 then 1344 (1 : 1345 posreal) 1346 else 1347 (0 : 1348 posreal))` 1349 by METIS_TAC [] 1350 ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC 1351 ++ FULL_SIMP_TAC posreal_ss []) 1352 ++ METIS_TAC [le_refl]) 1353 ++ METIS_TAC [zero_le]) 1354 ++ METIS_TAC [max_le2_imp, le_refl]) 1355 ++ Suff `Leq 1356 (Max 1357 (\(s :'a state). 1358 (if 1359 (Inv :'a state -> bool) s /\ 1360 (L :int) <= (Var :'a state -> int) s /\ Var s < (H :int) 1361 then 1362 posreal_pow (e :posreal) (Num (H - L)) 1363 else 1364 (0 : 1365 posreal))) 1366 (wp 1367 (While (\(s :'a state). (g :'a state -> bool) s) 1368 (body :'a command)) (One :'a state expect))) 1369 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1370 >> METIS_TAC [leq_trans] 1371 ++ POP_ASSUM (K ALL_TAC) 1372 ++ `Leq 1373 (Max 1374 (\(s :'a state). 1375 (if 1376 (Inv :'a state -> bool) s /\ 1377 (L :int) <= (Var :'a state -> int) s /\ Var s < (H :int) 1378 then 1379 posreal_pow (e :posreal) (Num (H - L)) 1380 else 1381 (0 : 1382 posreal))) 1383 (wp 1384 (While (\(s :'a state). (g :'a state -> bool) s) 1385 (body :'a command)) (One :'a state expect))) 1386 (Max 1387 (\(s :'a state). 1388 (if Inv s /\ Var s < L + (& (Num (H - L)) :int) then 1389 posreal_pow e (Num (H - L)) 1390 else 1391 (0 : 1392 posreal))) 1393 (wp (While (\(s :'a state). g s) body) (One :'a state expect)))` 1394 by (FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 1395 ++ GEN_TAC 1396 ++ `(if 1397 (Inv :'a state -> bool) (s :'a state) /\ 1398 (L :int) <= (Var :'a state -> int) s /\ Var s < (H :int) 1399 then 1400 posreal_pow (e :posreal) (Num (H - L)) 1401 else 1402 (0 : 1403 posreal)) <= 1404 (if Inv s /\ Var s < L + (& (Num (H - L)) :int) then 1405 posreal_pow e (Num (H - L)) 1406 else 1407 (0 : 1408 posreal))` 1409 by (Cases_on `L < H` 1410 >> (`(0 :int) < (H :int) - (L :int)` by RW_TAC int_ss [INT_SUB_LT] 1411 ++ `(& (Num ((H :int) - (L :int))) :int) = H - L` by METIS_TAC [INT_OF_NUM_POSINT_EQ] 1412 ++ ASM_REWRITE_TAC [INT_SUB_ADD2] 1413 ++ METIS_TAC [le_refl, INT_LT_IMP_LE, zero_le]) 1414 ++ `~((L :int) <= (Var :'a state -> int) (s :'a state) /\ Var s < (H :int))` by METIS_TAC [INT_LET_TRANS, INT_LT_IMP_LE] 1415 ++ METIS_TAC [zero_le]) 1416 ++ METIS_TAC [max_le2_imp, le_refl]) 1417 ++ Suff `Leq 1418 (Max 1419 (\(s :'a state). 1420 (if 1421 (Inv :'a state -> bool) s /\ 1422 (Var :'a state -> int) s < 1423 (L :int) + (& (Num ((H :int) - L)) :int) 1424 then 1425 posreal_pow (e :posreal) (Num (H - L)) 1426 else 1427 (0 : 1428 posreal))) 1429 (wp 1430 (While (\(s :'a state). (g :'a state -> bool) s) 1431 (body :'a command)) (One :'a state expect))) 1432 (wp (While (\(s :'a state). g s) body) (One :'a state expect))` 1433 >> METIS_TAC [leq_trans] 1434 ++ POP_ASSUM (K ALL_TAC) 1435 ++ FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 1436 ++ METIS_TAC [le_refl, max_le]); 1437 1438val variant_rule2 = store_thm 1439 ("variant_rule2", 1440 ``!(g :'a state -> bool) (body :'a command) (Inv :'a state -> bool) 1441 (H :int) (L :int). 1442 Leq 1443 (\(s :'a state). 1444 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 1445 (wp body 1446 (\(s :'a state). 1447 (if Inv s then (1 :posreal) else (0 :posreal)))) /\ 1448 Leq 1449 (\(s :'a state). 1450 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 1451 (\(s :'a state). 1452 (if L <= (Var :'a state -> int) s /\ Var s < H then 1453 (1 : 1454 posreal) 1455 else 1456 (0 : 1457 posreal))) /\ 1458 (!(N :int). 1459 Leq 1460 (\(s :'a state). 1461 (if g s /\ Inv s /\ (Var s = N) then 1462 (1 : 1463 posreal) 1464 else 1465 (0 : 1466 posreal))) 1467 (wp body 1468 (\(s :'a state). 1469 (if Var s < N then 1470 (1 : 1471 posreal) 1472 else 1473 (0 : 1474 posreal))))) ==> 1475 Leq 1476 (\(s :'a state). 1477 (if Inv s then (1 :posreal) else (0 :posreal))) 1478 (wp (While g body) (One :'a state expect))``, 1479 RW_TAC posreal_ss [] 1480 ++ `Leq 1481 (\(s :'a state). 1482 (if (Inv :'a state -> bool) s then 1483 posreal_pow (1 :posreal) (Num ((H :int) - (L :int))) 1484 else 1485 (0 : 1486 posreal))) 1487 (wp (While (g :'a state -> bool) (body :'a command)) 1488 (One :'a state expect))` 1489 by (`(0 :posreal) < (1 :posreal)` by RW_TAC posreal_ss [] 1490 ++ `(1:posreal) <= (1:posreal)` by RW_TAC posreal_ss [le_refl] 1491 ++ METIS_TAC [variant_rule]) 1492 ++ `(\(s :'a state). 1493 (if (Inv :'a state -> bool) s then (1 :posreal) else (0 :posreal))) = 1494 (\(s :'a state). 1495 (if Inv s then 1496 posreal_pow (1 :posreal) (Num ((H :int) - (L :int))) 1497 else 1498 (0 : 1499 posreal)))` 1500 by METIS_TAC [FUN_EQ_THM, posreal_pow_base1_eq_1] 1501 ++ ASM_REWRITE_TAC []); 1502 1503val While_variant_rule = store_thm 1504 ("While_variant_rule", 1505``!(i :string) (n :string) (body :value command). 1506 ~(n = i) /\ 1507 Leq 1508 (\(s :value state). 1509 (if 1510 (\(s :value state). (0 :int) <= int_of_value (s i)) s 1511 then 1512 (1 : 1513 posreal) 1514 else 1515 (0 : 1516 posreal))) 1517 (wp body 1518 (\(s :value state). 1519 (if 1520 (\(s :value state). (0 :int) <= int_of_value (s i)) s 1521 then 1522 (1 : 1523 posreal) 1524 else 1525 (0 : 1526 posreal)))) /\ 1527 (!(N :int). 1528 Leq 1529 (\(s :value state). 1530 (if 1531 (\(s :value state). 1532 int_of_value (s i) < int_of_value (s n)) s /\ 1533 (\(s :value state). (0 :int) <= int_of_value (s i)) 1534 s /\ 1535 ((\(s :value state). 1536 int_of_value (s n) - int_of_value (s i)) s = 1537 N) 1538 then 1539 (1 : 1540 posreal) 1541 else 1542 (0 : 1543 posreal))) 1544 (wp body 1545 (\(s :value state). 1546 (if 1547 (\(s :value state). 1548 int_of_value (s n) - int_of_value (s i)) s <= N 1549 then 1550 (1 : 1551 posreal) 1552 else 1553 (0 : 1554 posreal))))) ==> 1555 Leq 1556 (\(s :value state). 1557 (if 1558 (\(s :value state). (0 :int) <= int_of_value (s i)) s 1559 then 1560 (1 : 1561 posreal) 1562 else 1563 (0 : 1564 posreal))) 1565 (wp 1566 (While 1567 (\(s :value state). 1568 int_of_value (s i) < int_of_value (s n)) 1569 (Seq body 1570 (Assign i 1571 (\(s :value state). 1572 Int (int_of_value (s i) + (1 :int)))))) 1573 (One :value state expect))``, 1574REPEAT GEN_TAC 1575++ Q.ABBREV_TAC `Inv = (\(s :value state). (0 :int) <= int_of_value (s (i :string)))` 1576++ Q.ABBREV_TAC `g = (\(s :value state). 1577 int_of_value (s (i :string)) < 1578 int_of_value (s (n :string)))` 1579++ Q.ABBREV_TAC `Var = (\(s :value state). 1580 int_of_value (s (n :string)) - 1581 int_of_value (s (i :string)))` 1582++ Q.ABBREV_TAC `loopbody = Seq (body :value command) 1583 (Assign (i :string) 1584 (\(s :value state). Int (int_of_value (s i) + (1 :int))))` 1585++ REPEAT STRIP_TAC 1586++ `Leq 1587 (\(s :value state). 1588 (if (g :value state -> bool) s /\ (Inv :value state -> bool) s then 1589 (1 : 1590 posreal) 1591 else 1592 (0 : 1593 posreal))) 1594 (wp (loopbody :value command) 1595 (\(s :value state). 1596 (if Inv s then (1 :posreal) else (0 :posreal))))` 1597 by (Q.UNABBREV_TAC `Inv` 1598 ++ Q.UNABBREV_TAC `g` 1599 ++ Q.UNABBREV_TAC `loopbody` 1600 ++ RW_TAC posreal_ss [wp_def, assign_eta, int_of_value_def] 1601 ++ `Leq 1602 (wp (body :value command) 1603 (\(s :value state). 1604 (if 1605 (\(s :value state). (0 :int) <= int_of_value (s (i :string))) 1606 s 1607 then 1608 (1 : 1609 posreal) 1610 else 1611 (0 : 1612 posreal)))) 1613 (wp body 1614 (\(s :value state). 1615 (if (0 :int) <= int_of_value (s i) + (1 :int) then 1616 (1 : 1617 posreal) 1618 else 1619 (0 : 1620 posreal))))` 1621 by (MATCH_MP_TAC wp_mono 1622 ++ RW_TAC posreal_ss [Leq_def] 1623 ++ RW_TAC posreal_ss [] 1624 ++ METIS_TAC [INT_LE_ADD, INT_LE_01]) 1625 ++ Suff `Leq 1626 (\(s :value state). 1627 (if 1628 int_of_value (s (i :string)) < int_of_value (s (n :string)) /\ 1629 (0 :int) <= int_of_value (s i) 1630 then 1631 (1 : 1632 posreal) 1633 else 1634 (0 : 1635 posreal))) 1636 (\(s :value state). 1637 (if (\(s :value state). (0 :int) <= int_of_value (s i)) s then 1638 (1 : 1639 posreal) 1640 else 1641 (0 : 1642 posreal)))` 1643 >> METIS_TAC [leq_trans] 1644 ++ RW_TAC posreal_ss [Leq_def] 1645 ++ RW_TAC posreal_ss [le_refl]) 1646++ ASM_REWRITE_TAC [] 1647++ `!(N :int). 1648 Leq 1649 (\(s :value state). 1650 (if 1651 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\ 1652 ((Var :value state -> int) s = N) 1653 then 1654 (1 : 1655 posreal) 1656 else 1657 (0 : 1658 posreal))) 1659 (wp (loopbody :value command) 1660 (\(s :value state). 1661 (if Var s < N then (1 :posreal) else (0 :posreal))))` 1662 by (Q.UNABBREV_TAC `Inv` 1663 ++ Q.UNABBREV_TAC `g` 1664 ++ Q.UNABBREV_TAC `loopbody` 1665 ++ Q.UNABBREV_TAC `Var` 1666 ++ RW_TAC posreal_ss [wp_def, assign_eta, int_of_value_def] 1667 ++ FULL_SIMP_TAC posreal_ss [] 1668 ++ `(\(s :value state). 1669 (if 1670 int_of_value (s (n :string)) - 1671 (int_of_value (s (i :string)) + (1 :int)) < (N :int) 1672 then 1673 (1 : 1674 posreal) 1675 else 1676 (0 : 1677 posreal))) = 1678 (\(s :value state). 1679 (if 1680 (\(s :value state). int_of_value (s n) - int_of_value (s i)) s <= 1681 N 1682 then 1683 (1 : 1684 posreal) 1685 else 1686 (0 : 1687 posreal)))` 1688 by (RW_TAC posreal_ss [FUN_EQ_THM] 1689 ++ `int_of_value ((s :value state) (n :string)) - 1690 (int_of_value (s (i :string)) + (1 :int)) = 1691 int_of_value (s n) - int_of_value (s i) + ((0 :int) - (1 :int))` 1692 by (`int_of_value ((s :value state) (n :string)) = 1693 int_of_value (s n) + (0 :int)` by RW_TAC int_ss [] 1694 ++ METIS_TAC [INT_ADD2_SUB2]) 1695 ++ ASM_REWRITE_TAC [] 1696 ++ FULL_SIMP_TAC int_ss [INT_LT_ADDNEG2, INT_LE_EQ_LT_ADD1]) 1697 ++ ASM_REWRITE_TAC [] 1698 ++ METIS_TAC []) 1699++ ASM_REWRITE_TAC [] 1700++ `!(N :int). 1701 Leq 1702 (\(s :value state). 1703 (if 1704 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\ 1705 ((Var :value state -> int) s = N) 1706 then 1707 (1 : 1708 posreal) 1709 else 1710 (0 : 1711 posreal))) 1712 (wp (loopbody :value command) 1713 (\(s :value state). 1714 (if Inv s /\ Var s < N then (1 :posreal) else (0 :posreal))))` 1715 by (GEN_TAC 1716 ++ `wp (loopbody :value command) 1717 (\(s :value state). 1718 (if 1719 (Inv :value state -> bool) s /\ 1720 (Var :value state -> int) s < (N :int) 1721 then 1722 (1 : 1723 posreal) 1724 else 1725 (0 : 1726 posreal))) = 1727 wp loopbody 1728 (Conj 1729 (\(s :value state). (if Inv s then (1 :posreal) else (0 :posreal))) 1730 (\(s :value state). 1731 (if Var s < N then (1 :posreal) else (0 :posreal))))` 1732 by (`(\(s :value state). 1733 (if 1734 (Inv :value state -> bool) s /\ 1735 (Var :value state -> int) s < (N :int) 1736 then 1737 (1 : 1738 posreal) 1739 else 1740 (0 : 1741 posreal))) = 1742 Conj (\(s :value state). (if Inv s then (1 :posreal) else (0 :posreal))) 1743 (\(s :value state). 1744 (if Var s < N then (1 :posreal) else (0 :posreal)))` 1745 by (RW_TAC std_ss [FUN_EQ_THM, Conj_def] 1746 ++ RW_TAC posreal_ss [] 1747 ++ FULL_SIMP_TAC std_ss []) 1748 ++ RW_TAC std_ss []) 1749 ++ RW_TAC std_ss [] 1750 ++ POP_ASSUM (K ALL_TAC) 1751 ++ `Leq 1752 (\(s :value state). 1753 (if 1754 (g :value state -> bool) s /\ (Inv :value state -> bool) s /\ 1755 ((Var :value state -> int) s = (N :int)) 1756 then 1757 (1 : 1758 posreal) 1759 else 1760 (0 : 1761 posreal))) 1762 (Conj 1763 (\(s :value state). 1764 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 1765 (\(s :value state). 1766 (if g s /\ Inv s /\ (Var s = N) then 1767 (1 : 1768 posreal) 1769 else 1770 (0 : 1771 posreal))))` 1772 by (RW_TAC std_ss [Leq_def, Conj_def] 1773 ++ RW_TAC posreal_ss [add_comm, add_sub] 1774 ++ FULL_SIMP_TAC posreal_ss []) 1775 ++ Suff `Leq 1776 (Conj 1777 (\(s :value state). 1778 (if 1779 (g :value state -> bool) s /\ (Inv :value state -> bool) s 1780 then 1781 (1 : 1782 posreal) 1783 else 1784 (0 : 1785 posreal))) 1786 (\(s :value state). 1787 (if 1788 g s /\ Inv s /\ ((Var :value state -> int) s = (N :int)) 1789 then 1790 (1 : 1791 posreal) 1792 else 1793 (0 : 1794 posreal)))) 1795 (wp (loopbody :value command) 1796 (Conj 1797 (\(s :value state). 1798 (if Inv s then (1 :posreal) else (0 :posreal))) 1799 (\(s :value state). 1800 (if Var s < N then (1 :posreal) else (0 :posreal)))))` 1801 >> METIS_TAC [leq_trans] 1802 ++ POP_ASSUM (K ALL_TAC) 1803 ++ `Leq 1804 (Conj 1805 (wp (loopbody :value command) 1806 (\(s :value state). 1807 (if (Inv :value state -> bool) s then 1808 (1 : 1809 posreal) 1810 else 1811 (0 : 1812 posreal)))) 1813 (wp loopbody 1814 (\(s :value state). 1815 (if (Var :value state -> int) s < (N :int) then 1816 (1 : 1817 posreal) 1818 else 1819 (0 : 1820 posreal))))) 1821 (wp loopbody 1822 (Conj 1823 (\(s :value state). 1824 (if Inv s then (1 :posreal) else (0 :posreal))) 1825 (\(s :value state). 1826 (if Var s < N then (1 :posreal) else (0 :posreal)))))` 1827 by METIS_TAC [wp_conj] 1828 ++ Suff `Leq 1829 (Conj 1830 (\(s :value state). 1831 (if 1832 (g :value state -> bool) s /\ (Inv :value state -> bool) s 1833 then 1834 (1 : 1835 posreal) 1836 else 1837 (0 : 1838 posreal))) 1839 (\(s :value state). 1840 (if 1841 g s /\ Inv s /\ ((Var :value state -> int) s = (N :int)) 1842 then 1843 (1 : 1844 posreal) 1845 else 1846 (0 : 1847 posreal)))) 1848 (Conj 1849 (wp (loopbody :value command) 1850 (\(s :value state). 1851 (if Inv s then (1 :posreal) else (0 :posreal)))) 1852 (wp loopbody 1853 (\(s :value state). 1854 (if Var s < N then (1 :posreal) else (0 :posreal)))))` 1855 >> METIS_TAC [leq_trans] 1856 ++ POP_ASSUM (K ALL_TAC) 1857 ++ FULL_SIMP_TAC std_ss [Leq_def, Conj_def] 1858 ++ GEN_TAC 1859 ++ MATCH_MP_TAC sub_mono 1860 ++ SIMP_TAC posreal_ss [] 1861 ++ METIS_TAC [le_add2]) 1862++ `!(N :num). 1863 Leq 1864 (\(s :value state). 1865 (if 1866 (Inv :value state -> bool) s /\ 1867 (Var :value state -> int) s < (1 :int) + (& N :int) 1868 then 1869 posreal_pow (1 :posreal) N 1870 else 1871 (0 : 1872 posreal))) 1873 (wp 1874 (While (\(s :value state). (g :value state -> bool) s) 1875 (loopbody :value command)) (One :value state expect))` 1876 by (GEN_TAC 1877 ++ Induct_on `N` 1878 >> (RW_TAC int_ss [posreal_pow_def] 1879 ++ `Leq 1880 (\(s :value state). 1881 (if 1882 (Inv :value state -> bool) s /\ 1883 (Var :value state -> int) s < (1 :int) 1884 then 1885 (1 : 1886 posreal) 1887 else 1888 (0 : 1889 posreal))) 1890 (\(s :value state). 1891 (if ~(g :value state -> bool) s then 1892 (1 : 1893 posreal) 1894 else 1895 (0 : 1896 posreal)))` 1897 by (Q.UNABBREV_TAC `g` 1898 ++ Q.UNABBREV_TAC `Inv` 1899 ++ Q.UNABBREV_TAC `Var` 1900 ++ FULL_SIMP_TAC std_ss [Leq_def] 1901 ++ GEN_TAC 1902 ++ RW_TAC posreal_ss [] 1903 ++ `(0 :int) + int_of_value ((s :value state) (i :string)) < 1904 int_of_value (s (n :string))` 1905 by RW_TAC int_ss [] 1906 ++ `(0 :int) < 1907 int_of_value ((s :value state) (n :string)) - 1908 int_of_value (s (i :string))` 1909 by METIS_TAC [INT_LT_ADD_SUB] 1910 ++ METIS_TAC [NO_INT_BETWEEN_ZERO_AND_ONE]) 1911 ++ `Leq 1912 (\(s :value state). 1913 (if ~(g :value state -> bool) s then 1914 (1 : 1915 posreal) 1916 else 1917 (0 : 1918 posreal))) 1919 (wp (While (\(s :value state). g s) (loopbody :value command)) 1920 (One :value state expect))` 1921 by (FULL_SIMP_TAC std_ss [Leq_def] 1922 ++ GEN_TAC 1923 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 1924 ++ `monotonic 1925 ((expect :value state expect -> bool), 1926 (Leq :value state expect -> value state expect -> bool)) 1927 (\(e :value state expect) (s :value state). 1928 (if (g :value state -> bool) s then 1929 wp (loopbody :value command) e s 1930 else 1931 One s))` 1932 by (RW_TAC std_ss [monotonic_def, Leq_def] 1933 ++ Cases_on `g s'` 1934 >> METIS_TAC [wp_mono, Leq_def] 1935 ++ RW_TAC posreal_ss [One_def]) 1936 ++ `lfp 1937 ((expect :value state expect -> bool), 1938 (Leq :value state expect -> value state expect -> bool)) 1939 (\(e :value state expect) (s :value state). 1940 (if (g :value state -> bool) s then 1941 wp (loopbody :value command) e s 1942 else 1943 One s)) 1944 (expect_lfp 1945 (\(e :value state expect) (s :value state). 1946 (if g s then wp loopbody e s else One s)))` 1947 by METIS_TAC [expect_lfp_def] 1948 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 1949 ++ Suff `(1 :posreal) <= 1950 (\(s :value state). 1951 (if (g :value state -> bool) s then 1952 wp (loopbody :value command) 1953 (expect_lfp 1954 (\(e :value state expect) (s :value state). 1955 (if g s then wp loopbody e s else One s))) s 1956 else 1957 One s)) (s :value state)` 1958 >> METIS_TAC [] 1959 ++ RW_TAC posreal_ss [One_def]) 1960 ++ METIS_TAC [leq_trans]) 1961 ++ `Leq 1962 (\(s :value state). 1963 (if 1964 (Inv :value state -> bool) s /\ 1965 (Var :value state -> int) s < (1 :int) + (& (SUC (N :num)) :int) 1966 then 1967 posreal_pow (1 :posreal) (SUC N) 1968 else 1969 (0 : 1970 posreal))) 1971 (Max 1972 (\(s :value state). 1973 (\(s :value state). 1974 (if (g :value state -> bool) s then 1975 (1 : 1976 posreal) 1977 else 1978 (0 : 1979 posreal))) s * 1980 (\(s :value state). 1981 (if Inv s /\ Var s < (1 :int) + (& (SUC N) :int) then 1982 posreal_pow (1 :posreal) (SUC N) 1983 else 1984 (0 : 1985 posreal))) s) 1986 (\(s :value state). 1987 (\(s :value state). 1988 (if ~g s then (1 :posreal) else (0 :posreal))) s * 1989 (\(s :value state). 1990 (if Inv s /\ Var s < (1 :int) + (& (SUC N) :int) then 1991 posreal_pow (1 :posreal) (SUC N) 1992 else 1993 (0 : 1994 posreal))) s))` 1995 by (RW_TAC std_ss [Max_def, Leq_def] 1996 ++ Cases_on `g s` 1997 ++ RW_TAC posreal_ss []) 1998 ++ Suff `Leq 1999 (Max 2000 (\(s :value state). 2001 (\(s :value state). 2002 (if (g :value state -> bool) s then 2003 (1 : 2004 posreal) 2005 else 2006 (0 : 2007 posreal))) s * 2008 (\(s :value state). 2009 (if 2010 (Inv :value state -> bool) s /\ 2011 (Var :value state -> int) s < 2012 (1 :int) + (& (SUC (N :num)) :int) 2013 then 2014 posreal_pow (1 :posreal) (SUC N) 2015 else 2016 (0 : 2017 posreal))) s) 2018 (\(s :value state). 2019 (\(s :value state). 2020 (if ~g s then (1 :posreal) else (0 :posreal))) s * 2021 (\(s :value state). 2022 (if Inv s /\ Var s < (1 :int) + (& (SUC N) :int) then 2023 posreal_pow (1 :posreal) (SUC N) 2024 else 2025 (0 : 2026 posreal))) s)) 2027 (wp (While (\(s :value state). g s) (loopbody :value command)) 2028 (One :value state expect))` 2029 >> METIS_TAC [leq_trans] 2030 ++ POP_ASSUM (K ALL_TAC) 2031 ++ `Leq 2032 (\(s :value state). 2033 (if ~(g :value state -> bool) s then 2034 (1 : 2035 posreal) 2036 else 2037 (0 : 2038 posreal))) 2039 (wp (While (\(s :value state). g s) (loopbody :value command)) 2040 (One :value state expect))` 2041 by (FULL_SIMP_TAC std_ss [Leq_def] 2042 ++ GEN_TAC 2043 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 2044 ++ `monotonic 2045 ((expect :value state expect -> bool), 2046 (Leq :value state expect -> value state expect -> bool)) 2047 (\(e :value state expect) (s :value state). 2048 (if (g :value state -> bool) s then 2049 wp (loopbody :value command) e s 2050 else 2051 One s))` 2052 by (RW_TAC std_ss [monotonic_def, Leq_def] 2053 ++ Cases_on `g s'` 2054 >> METIS_TAC [wp_mono, Leq_def] 2055 ++ RW_TAC posreal_ss [One_def]) 2056 ++ `lfp 2057 ((expect :value state expect -> bool), 2058 (Leq :value state expect -> value state expect -> bool)) 2059 (\(e :value state expect) (s :value state). 2060 (if (g :value state -> bool) s then 2061 wp (loopbody :value command) e s 2062 else 2063 One s)) 2064 (expect_lfp 2065 (\(e :value state expect) (s :value state). 2066 (if g s then wp loopbody e s else One s)))` 2067 by METIS_TAC [expect_lfp_def] 2068 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 2069 ++ Suff `(1 :posreal) <= 2070 (\(s :value state). 2071 (if (g :value state -> bool) s then 2072 wp (loopbody :value command) 2073 (expect_lfp 2074 (\(e :value state expect) (s :value state). 2075 (if g s then wp loopbody e s else One s))) s 2076 else 2077 One s)) (s :value state)` 2078 >> METIS_TAC [] 2079 ++ RW_TAC posreal_ss [One_def]) 2080 ++ `Leq 2081 (Max 2082 (\(s :value state). 2083 (\(s :value state). 2084 (if (g :value state -> bool) s then 2085 (1 : 2086 posreal) 2087 else 2088 (0 : 2089 posreal))) s * 2090 (\(s :value state). 2091 (if 2092 (Inv :value state -> bool) s /\ 2093 (Var :value state -> int) s < 2094 (1 :int) + (& (SUC (N :num)) :int) 2095 then 2096 posreal_pow (1 :posreal) (SUC N) 2097 else 2098 (0 : 2099 posreal))) s) 2100 (\(s :value state). 2101 (\(s :value state). 2102 (if ~g s then (1 :posreal) else (0 :posreal))) s * 2103 (\(s :value state). 2104 (if Inv s /\ Var s < (1 :int) + (& (SUC N) :int) then 2105 posreal_pow (1 :posreal) (SUC N) 2106 else 2107 (0 : 2108 posreal))) s)) 2109 (Max 2110 (\(s :value state). 2111 (\(s :value state). 2112 (if g s then (1 :posreal) else (0 :posreal))) s * 2113 (\(s :value state). 2114 (if Inv s /\ Var s < (1 :int) + (& (SUC N) :int) then 2115 posreal_pow (1 :posreal) (SUC N) 2116 else 2117 (0 : 2118 posreal))) s) 2119 (wp (While (\(s :value state). g s) (loopbody :value command)) 2120 (One :value state expect)))` 2121 by (RW_TAC posreal_ss [Leq_def, Max_def] 2122 ++ Cases_on `g s` 2123 ++ RW_TAC posreal_ss [] 2124 ++ Suff `posreal_pow (1 :posreal) (SUC (N :num)) <= (1 :posreal)` 2125 >> (`(1 :posreal) <= 2126 wp 2127 (While (\(s :value state). (g :value state -> bool) s) 2128 (loopbody :value command)) (One :value state expect) 2129 (s :value state)` 2130 by (FULL_SIMP_TAC posreal_ss [Leq_def] 2131 ++ METIS_TAC []) 2132 ++ METIS_TAC [le_trans]) 2133 ++ METIS_TAC [posreal_pow_1bounded_base_1bounded, le_refl]) 2134 ++ Suff `Leq 2135 (Max 2136 (\(s :value state). 2137 (\(s :value state). 2138 (if (g :value state -> bool) s then 2139 (1 : 2140 posreal) 2141 else 2142 (0 : 2143 posreal))) s * 2144 (\(s :value state). 2145 (if 2146 (Inv :value state -> bool) s /\ 2147 (Var :value state -> int) s < 2148 (1 :int) + (& (SUC (N :num)) :int) 2149 then 2150 posreal_pow (1 :posreal) (SUC N) 2151 else 2152 (0 : 2153 posreal))) s) 2154 (wp (While (\(s :value state). g s) (loopbody :value command)) 2155 (One :value state expect))) 2156 (wp (While (\(s :value state). g s) loopbody) 2157 (One :value state expect))` 2158 >> METIS_TAC [leq_trans] 2159 ++ POP_ASSUM (K ALL_TAC) 2160 ++ `Leq 2161 (Max 2162 (\(s :value state). 2163 (\(s :value state). 2164 (if (g :value state -> bool) s then 2165 (1 : 2166 posreal) 2167 else 2168 (0 : 2169 posreal))) s * 2170 (\(s :value state). 2171 (if 2172 (Inv :value state -> bool) s /\ 2173 (Var :value state -> int) s < 2174 (1 :int) + (& (SUC (N :num)) :int) 2175 then 2176 posreal_pow (1 :posreal) (SUC N) 2177 else 2178 (0 : 2179 posreal))) s) 2180 (wp (While (\(s :value state). g s) (loopbody :value command)) 2181 (One :value state expect))) 2182 (Max 2183 (Max 2184 (\(s :value state). 2185 (if g s /\ Inv s /\ Var s < (1 :int) + (& N :int) then 2186 posreal_pow (1 :posreal) (SUC N) 2187 else 2188 (0 : 2189 posreal))) 2190 (\(s :value state). 2191 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2192 posreal_pow (1 :posreal) (SUC N) 2193 else 2194 (0 : 2195 posreal)))) 2196 (wp (While (\(s :value state). g s) loopbody) 2197 (One :value state expect)))` 2198 by (RW_TAC posreal_ss [Leq_def, Max_def] 2199 ++ `(Var :value state -> int) (s :value state) < 2200 (1 :int) + (& (SUC (N :num)) :int) = 2201 Var s <= (1 :int) + (& N :int)` 2202 by RW_TAC int_ss [INT, INT_ADD_ASSOC, INT_LE_EQ_LT_ADD1] 2203 ++ `(Var :value state -> int) (s :value state) <= 2204 (1 :int) + (& (N :num) :int) = 2205 Var s < (1 :int) + (& N :int) \/ (Var s = (1 :int) + (& N :int))` 2206 by RW_TAC int_ss [INT_LE_LT] 2207 ++ ASM_REWRITE_TAC [] 2208 ++ POP_ASSUM (K ALL_TAC) 2209 ++ POP_ASSUM (K ALL_TAC) 2210 ++ Cases_on `Var s < 1 + &N` 2211 ++ ASM_REWRITE_TAC [] 2212 ++ Cases_on `g s` 2213 ++ ASM_REWRITE_TAC [] 2214 ++ RW_TAC int_ss [max_lzero, mul_lone, mul_lzero, max_refl] 2215 ++ RW_TAC posreal_ss [zero_lt_posreal_pow]) 2216 ++ Suff `Leq 2217 (Max 2218 (Max 2219 (\(s :value state). 2220 (if 2221 (g :value state -> bool) s /\ 2222 (Inv :value state -> bool) s /\ 2223 (Var :value state -> int) s < (1 :int) + (& (N :num) :int) 2224 then 2225 posreal_pow (1 :posreal) (SUC N) 2226 else 2227 (0 : 2228 posreal))) 2229 (\(s :value state). 2230 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2231 posreal_pow (1 :posreal) (SUC N) 2232 else 2233 (0 : 2234 posreal)))) 2235 (wp (While (\(s :value state). g s) (loopbody :value command)) 2236 (One :value state expect))) 2237 (wp (While (\(s :value state). g s) loopbody) 2238 (One :value state expect))` 2239 >> METIS_TAC [leq_trans] 2240 ++ POP_ASSUM (K ALL_TAC) 2241 ++ `Leq 2242 (Max 2243 (Max 2244 (\(s :value state). 2245 (if 2246 (g :value state -> bool) s /\ 2247 (Inv :value state -> bool) s /\ 2248 (Var :value state -> int) s < (1 :int) + (& (N :num) :int) 2249 then 2250 posreal_pow (1 :posreal) (SUC N) 2251 else 2252 (0 : 2253 posreal))) 2254 (\(s :value state). 2255 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2256 posreal_pow (1 :posreal) (SUC N) 2257 else 2258 (0 : 2259 posreal)))) 2260 (wp (While (\(s :value state). g s) (loopbody :value command)) 2261 (One :value state expect))) 2262 (Max 2263 (Max 2264 (\(s :value state). 2265 (1 :posreal) * 2266 wp (While (\(s :value state). g s) loopbody) 2267 (One :value state expect) s) 2268 (\(s :value state). 2269 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2270 posreal_pow (1 :posreal) (SUC N) 2271 else 2272 (0 : 2273 posreal)))) 2274 (wp (While (\(s :value state). g s) loopbody) 2275 (One :value state expect)))` 2276 by (RW_TAC posreal_ss [Leq_def, Max_def] 2277 ++ RW_TAC posreal_ss [] 2278 ++ FULL_SIMP_TAC int_ss [DE_MORGAN_THM, INT_LT_IMP_NE, Leq_def] 2279 ++ RW_TAC std_ss [mul_lone, posreal_pow_def] 2280 ++ `max 2281 (wp 2282 (While (\(s :value state). (g :value state -> bool) s) 2283 (loopbody :value command)) (One :value state expect) 2284 (s :value state)) 2285 (wp (While (\(s :value state). g s) loopbody) 2286 (One :value state expect) s) = 2287 wp (While (\(s :value state). g s) loopbody) (One :value state expect) s` 2288 by METIS_TAC [preal_max_def] 2289 ++ `max 2290 (max 2291 (wp 2292 (While (\(s :value state). (g :value state -> bool) s) 2293 (loopbody :value command)) (One :value state expect) 2294 (s :value state)) (posreal_pow (1 :posreal) (N :num))) 2295 (wp (While (\(s :value state). g s) loopbody) 2296 (One :value state expect) s) = 2297 max (posreal_pow (1 :posreal) N) 2298 (wp (While (\(s :value state). g s) loopbody) 2299 (One :value state expect) s)` 2300 by METIS_TAC [max_swap, preal_max_def] 2301 ++ METIS_TAC [preal_max_def, le_trans, le_refl]) 2302 ++ Suff `Leq 2303 (Max 2304 (Max 2305 (\(s :value state). 2306 (1 :posreal) * 2307 wp 2308 (While (\(s :value state). (g :value state -> bool) s) 2309 (loopbody :value command)) (One :value state expect) s) 2310 (\(s :value state). 2311 (if 2312 g s /\ (Inv :value state -> bool) s /\ 2313 ((Var :value state -> int) s = 2314 (1 :int) + (& (N :num) :int)) 2315 then 2316 posreal_pow (1 :posreal) (SUC N) 2317 else 2318 (0 : 2319 posreal)))) 2320 (wp (While (\(s :value state). g s) loopbody) 2321 (One :value state expect))) 2322 (wp (While (\(s :value state). g s) loopbody) 2323 (One :value state expect))` 2324 >> METIS_TAC [leq_trans] 2325 ++ POP_ASSUM (K ALL_TAC) 2326 ++ `Leq 2327 (Max 2328 (Max 2329 (\(s :value state). 2330 (1 :posreal) * 2331 wp 2332 (While (\(s :value state). (g :value state -> bool) s) 2333 (loopbody :value command)) (One :value state expect) s) 2334 (\(s :value state). 2335 (if 2336 g s /\ (Inv :value state -> bool) s /\ 2337 ((Var :value state -> int) s = 2338 (1 :int) + (& (N :num) :int)) 2339 then 2340 posreal_pow (1 :posreal) (SUC N) 2341 else 2342 (0 : 2343 posreal)))) 2344 (wp (While (\(s :value state). g s) loopbody) 2345 (One :value state expect))) 2346 (Max 2347 (\(s :value state). 2348 posreal_pow (1 :posreal) N * 2349 wp loopbody 2350 (\(s :value state). 2351 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2352 (1 : 2353 posreal) 2354 else 2355 (0 : 2356 posreal))) s) 2357 (wp (While (\(s :value state). g s) loopbody) 2358 (One :value state expect)))` 2359 by (RW_TAC posreal_ss [Leq_def, Max_def] 2360 ++ `max 2361 (max 2362 (wp 2363 (While (\(s :value state). (g :value state -> bool) s) 2364 (loopbody :value command)) (One :value state expect) 2365 (s :value state)) 2366 (if 2367 g s /\ (Inv :value state -> bool) s /\ 2368 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int)) 2369 then 2370 posreal_pow (1 :posreal) (SUC N) 2371 else 2372 (0 : 2373 posreal))) 2374 (wp (While (\(s :value state). g s) loopbody) 2375 (One :value state expect) s) = 2376 max 2377 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2378 posreal_pow (1 :posreal) (SUC N) 2379 else 2380 (0 : 2381 posreal)) 2382 (wp (While (\(s :value state). g s) loopbody) 2383 (One :value state expect) s)` 2384 by (`max 2385 (max 2386 (wp 2387 (While (\(s :value state). (g :value state -> bool) s) 2388 (loopbody :value command)) (One :value state expect) 2389 (s :value state)) 2390 (if 2391 g s /\ (Inv :value state -> bool) s /\ 2392 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int)) 2393 then 2394 posreal_pow (1 :posreal) (SUC N) 2395 else 2396 (0 : 2397 posreal))) 2398 (wp (While (\(s :value state). g s) loopbody) 2399 (One :value state expect) s) = 2400 max 2401 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2402 posreal_pow (1 :posreal) (SUC N) 2403 else 2404 (0 : 2405 posreal)) 2406 (max 2407 (wp (While (\(s :value state). g s) loopbody) 2408 (One :value state expect) s) 2409 (wp (While (\(s :value state). g s) loopbody) 2410 (One :value state expect) s))` 2411 by METIS_TAC [max_swap] 2412 ++ METIS_TAC [preal_max_def]) 2413 ++ ASM_REWRITE_TAC [] 2414 ++ POP_ASSUM (K ALL_TAC) 2415 ++ `(if 2416 (g :value state -> bool) (s :value state) /\ 2417 (Inv :value state -> bool) s /\ 2418 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int)) 2419 then 2420 posreal_pow (1 :posreal) (SUC N) 2421 else 2422 (0 : 2423 posreal)) = 2424 posreal_pow (1 :posreal) N * 2425 (if g s /\ Inv s /\ (Var s = (1 :int) + (& N :int)) then 2426 (1 : 2427 posreal) 2428 else 2429 (0 : 2430 posreal))` 2431 by RW_TAC posreal_ss [posreal_pow_def, mul_comm, mul_rzero] 2432 ++ ASM_REWRITE_TAC [] 2433 ++ POP_ASSUM (K ALL_TAC) 2434 ++ `posreal_pow (1 :posreal) (N :num) * 2435 (if 2436 (g :value state -> bool) (s :value state) /\ 2437 (Inv :value state -> bool) s /\ 2438 ((Var :value state -> int) s = (1 :int) + (& N :int)) 2439 then 2440 (1 : 2441 posreal) 2442 else 2443 (0 : 2444 posreal)) <= 2445 posreal_pow (1 :posreal) N * 2446 wp (loopbody :value command) 2447 (\(s :value state). 2448 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2449 (1 : 2450 posreal) 2451 else 2452 (0 : 2453 posreal))) s` 2454 by (`(if 2455 (g :value state -> bool) (s :value state) /\ 2456 (Inv :value state -> bool) s /\ 2457 ((Var :value state -> int) s = (1 :int) + (& (N :num) :int)) 2458 then 2459 (1 : 2460 posreal) 2461 else 2462 (0 : 2463 posreal)) <= 2464 wp (loopbody :value command) 2465 (\(s :value state). 2466 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2467 (1 : 2468 posreal) 2469 else 2470 (0 : 2471 posreal))) s` 2472 by (FULL_SIMP_TAC posreal_ss [Leq_def] 2473 ++ METIS_TAC []) 2474 ++ METIS_TAC [le_refl, le_mul2]) 2475 ++ FULL_SIMP_TAC posreal_ss [posreal_pow_base1_eq_1, mul_lone] 2476 ++ RW_TAC posreal_ss [preal_max_def, le_refl, le_trans] 2477 ++ METIS_TAC [le_trans, le_total]) 2478 ++ Suff `Leq 2479 (Max 2480 (\(s :value state). 2481 posreal_pow (1 :posreal) (N :num) * 2482 wp (loopbody :value command) 2483 (\(s :value state). 2484 (if 2485 (Inv :value state -> bool) s /\ 2486 (Var :value state -> int) s < (1 :int) + (& N :int) 2487 then 2488 (1 : 2489 posreal) 2490 else 2491 (0 : 2492 posreal))) s) 2493 (wp 2494 (While (\(s :value state). (g :value state -> bool) s) loopbody) 2495 (One :value state expect))) 2496 (wp (While (\(s :value state). g s) loopbody) 2497 (One :value state expect))` 2498 >> METIS_TAC [leq_trans] 2499 ++ POP_ASSUM (K ALL_TAC) 2500 ++ `(\(s :value state). 2501 posreal_pow (1 :posreal) (N :num) * 2502 wp (loopbody :value command) 2503 (\(s :value state). 2504 (if 2505 (Inv :value state -> bool) s /\ 2506 (Var :value state -> int) s < (1 :int) + (& N :int) 2507 then 2508 (1 : 2509 posreal) 2510 else 2511 (0 : 2512 posreal))) s) = 2513 wp loopbody 2514 (\(s :value state). 2515 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2516 posreal_pow (1 :posreal) N 2517 else 2518 (0 : 2519 posreal)))` 2520 by (RW_TAC std_ss [FUN_EQ_THM] 2521 ++ `(\(s :value state). 2522 (if 2523 (Inv :value state -> bool) s /\ 2524 (Var :value state -> int) s < (1 :int) + (& (N :num) :int) 2525 then 2526 posreal_pow (1 :posreal) N 2527 else 2528 (0 : 2529 posreal))) = 2530 (\(s :value state). 2531 posreal_pow (1 :posreal) N * 2532 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2533 (1 : 2534 posreal) 2535 else 2536 (0 : 2537 posreal)))` 2538 by METIS_TAC [FUN_EQ_THM, mul_rone, mul_rzero] 2539 ++ ASM_REWRITE_TAC [] 2540 ++ POP_ASSUM (K ALL_TAC) 2541 ++ `posreal_pow (1 :posreal) (N :num) * 2542 wp (loopbody :value command) 2543 (\(s :value state). 2544 (if 2545 (Inv :value state -> bool) s /\ 2546 (Var :value state -> int) s < (1 :int) + (& N :int) 2547 then 2548 (1 : 2549 posreal) 2550 else 2551 (0 : 2552 posreal))) (s :value state) = 2553 wp loopbody 2554 (\(s :value state). 2555 posreal_pow (1 :posreal) N * 2556 (\(s :value state). 2557 (if Inv s /\ Var s < (1 :int) + (& N :int) then 2558 (1 : 2559 posreal) 2560 else 2561 (0 : 2562 posreal))) s) s` 2563 by METIS_TAC [wp_scale] 2564 ++ METIS_TAC []) 2565 ++ ASM_REWRITE_TAC [] 2566 ++ POP_ASSUM (K ALL_TAC) 2567 ++ `Leq 2568 (Max 2569 (wp (loopbody :value command) 2570 (\(s :value state). 2571 (if 2572 (Inv :value state -> bool) s /\ 2573 (Var :value state -> int) s < (1 :int) + (& (N :num) :int) 2574 then 2575 posreal_pow (1 :posreal) N 2576 else 2577 (0 : 2578 posreal)))) 2579 (wp 2580 (While (\(s :value state). (g :value state -> bool) s) loopbody) 2581 (One :value state expect))) 2582 (Max 2583 (wp loopbody 2584 (wp (While (\(s :value state). g s) loopbody) 2585 (One :value state expect))) 2586 (wp (While (\(s :value state). g s) loopbody) 2587 (One :value state expect)))` 2588 by (`Leq 2589 (wp (loopbody :value command) 2590 (\(s :value state). 2591 (if 2592 (Inv :value state -> bool) s /\ 2593 (Var :value state -> int) s < (1 :int) + (& (N :num) :int) 2594 then 2595 posreal_pow (1 :posreal) N 2596 else 2597 (0 : 2598 posreal)))) 2599 (wp loopbody 2600 (wp 2601 (While (\(s :value state). (g :value state -> bool) s) loopbody) 2602 (One :value state expect)))` 2603 by METIS_TAC [wp_mono] 2604 ++ RW_TAC posreal_ss [Leq_def, Max_def] 2605 ++ FULL_SIMP_TAC posreal_ss [Leq_def] 2606 ++ RW_TAC posreal_ss [preal_max_def, le_refl, le_trans] 2607 ++ METIS_TAC [le_trans, le_total]) 2608 ++ Suff `Leq 2609 (Max 2610 (wp (loopbody :value command) 2611 (wp 2612 (While (\(s :value state). (g :value state -> bool) s) 2613 loopbody) (One :value state expect))) 2614 (wp (While (\(s :value state). g s) loopbody) 2615 (One :value state expect))) 2616 (wp (While (\(s :value state). g s) loopbody) 2617 (One :value state expect))` 2618 >> METIS_TAC [leq_trans] 2619 ++ POP_ASSUM (K ALL_TAC) 2620 ++ `Leq 2621 (wp (loopbody :value command) 2622 (wp 2623 (While (\(s :value state). (g :value state -> bool) s) loopbody) 2624 (One :value state expect))) 2625 (wp (While (\(s :value state). g s) loopbody) 2626 (One :value state expect))` 2627 by (`monotonic 2628 ((expect :value state expect -> bool), 2629 (Leq :value state expect -> value state expect -> bool)) 2630 (\(e :value state expect) (s :value state). 2631 (if (g :value state -> bool) s then 2632 wp (loopbody :value command) e s 2633 else 2634 One s))` 2635 by (RW_TAC std_ss [monotonic_def, Leq_def] 2636 ++ Cases_on `g s` 2637 >> METIS_TAC [wp_mono, Leq_def] 2638 ++ RW_TAC posreal_ss [One_def]) 2639 ++ `lfp 2640 ((expect :value state expect -> bool), 2641 (Leq :value state expect -> value state expect -> bool)) 2642 (\(e :value state expect) (s :value state). 2643 (if (g :value state -> bool) s then 2644 wp (loopbody :value command) e s 2645 else 2646 One s)) 2647 (expect_lfp 2648 (\(e :value state expect) (s :value state). 2649 (if g s then wp loopbody e s else One s)))` 2650 by METIS_TAC [expect_lfp_def] 2651 ++ FULL_SIMP_TAC std_ss [Leq_def, wp_def, cond_eta, lfp_def, expect_def] 2652 ++ GEN_TAC 2653 ++ Suff `wp (loopbody :value command) 2654 (expect_lfp 2655 (\(e :value state expect) (s :value state). 2656 (if (g :value state -> bool) s then 2657 wp loopbody e s 2658 else 2659 One s))) (s :value state) <= 2660 (\(s :value state). 2661 (if g s then 2662 wp loopbody 2663 (expect_lfp 2664 (\(e :value state expect) (s :value state). 2665 (if g s then wp loopbody e s else One s))) s 2666 else 2667 One s)) s` 2668 >> METIS_TAC [] 2669 ++ RW_TAC posreal_ss [le_refl, One_def] 2670 ++ `expect_lfp 2671 (\(e :value state expect) (s :value state). 2672 (if (g :value state -> bool) s then 2673 wp (loopbody :value command) e s 2674 else 2675 (1 : 2676 posreal))) = 2677 wp (While (\(s :value state). g s) loopbody) (One :value state expect)` 2678 by RW_TAC posreal_ss [wp_def, cond_eta, One_def] 2679 ++ ASM_REWRITE_TAC [] 2680 ++ POP_ASSUM (K ALL_TAC) 2681 ++ `wp (loopbody :value command) 2682 (wp (While (\(s :value state). (g :value state -> bool) s) loopbody) 2683 (One :value state expect)) (s :value state) = 2684 wp (Seq loopbody (While (\(s :value state). g s) loopbody)) 2685 (One :value state expect) s` 2686 by RW_TAC posreal_ss [wp_def] 2687 ++ ASM_REWRITE_TAC [] 2688 ++ POP_ASSUM (K ALL_TAC) 2689 ++ METIS_TAC [Leq_def, One_def, Term_Leq_One]) 2690 ++ FULL_SIMP_TAC posreal_ss [Leq_def, Max_def, preal_max_def, le_refl]) 2691++ `!(N :num). 2692 Leq 2693 (\(s :value state). 2694 (if 2695 (Inv :value state -> bool) s /\ 2696 (Var :value state -> int) s < (1 :int) + (& N :int) 2697 then 2698 (1 : 2699 posreal) 2700 else 2701 (0 : 2702 posreal))) 2703 (wp 2704 (While (\(s :value state). (g :value state -> bool) s) 2705 (loopbody :value command)) (One :value state expect))` 2706 by METIS_TAC [posreal_pow_base1_eq_1] 2707++ `(\(s :value state). 2708 (if (Inv :value state -> bool) s then 2709 (1 : 2710 posreal) 2711 else 2712 (0 : 2713 posreal))) = 2714 Max 2715 (\(s :value state). 2716 (if (g :value state -> bool) s /\ Inv s then 2717 (1 : 2718 posreal) 2719 else 2720 (0 : 2721 posreal))) 2722 (\(s :value state). 2723 (if ~g s /\ Inv s then (1 :posreal) else (0 :posreal)))` 2724 by (RW_TAC posreal_ss [FUN_EQ_THM, Max_def] 2725 ++ Cases_on `g s` 2726 ++ METIS_TAC [max_lzero, max_rzero]) 2727++ ASM_REWRITE_TAC [] 2728++ POP_ASSUM (K ALL_TAC) 2729++ `Leq 2730 (Max 2731 (\(s :value state). 2732 (if 2733 (g :value state -> bool) s /\ (Inv :value state -> bool) s 2734 then 2735 (1 : 2736 posreal) 2737 else 2738 (0 : 2739 posreal))) 2740 (\(s :value state). 2741 (if ~g s /\ Inv s then (1 :posreal) else (0 :posreal)))) 2742 (Max 2743 (\(s :value state). 2744 (if g s /\ Inv s then (1 :posreal) else (0 :posreal))) 2745 (wp (While (\(s :value state). g s) (loopbody :value command)) 2746 (One :value state expect)))` 2747 by (`Leq 2748 (\(s :value state). 2749 (if ~(g :value state -> bool) s then 2750 (1 : 2751 posreal) 2752 else 2753 (0 : 2754 posreal))) 2755 (wp (While (\(s :value state). g s) (loopbody :value command)) 2756 (One :value state expect))` 2757 by (FULL_SIMP_TAC std_ss [Leq_def] 2758 ++ GEN_TAC 2759 ++ RW_TAC posreal_ss [zero_le, wp_def, cond_eta] 2760 ++ `monotonic 2761 ((expect :value state expect -> bool), 2762 (Leq :value state expect -> value state expect -> bool)) 2763 (\(e :value state expect) (s :value state). 2764 (if (g :value state -> bool) s then 2765 wp (loopbody :value command) e s 2766 else 2767 One s))` 2768 by (RW_TAC std_ss [monotonic_def, Leq_def] 2769 ++ Cases_on `g s'` 2770 >> METIS_TAC [wp_mono, Leq_def] 2771 ++ RW_TAC posreal_ss [One_def]) 2772 ++ `lfp 2773 ((expect :value state expect -> bool), 2774 (Leq :value state expect -> value state expect -> bool)) 2775 (\(e :value state expect) (s :value state). 2776 (if (g :value state -> bool) s then 2777 wp (loopbody :value command) e s 2778 else 2779 One s)) 2780 (expect_lfp 2781 (\(e :value state expect) (s :value state). 2782 (if g s then wp loopbody e s else One s)))` 2783 by METIS_TAC [expect_lfp_def] 2784 ++ FULL_SIMP_TAC std_ss [lfp_def, expect_def] 2785 ++ Suff `(1 :posreal) <= 2786 (\(s :value state). 2787 (if (g :value state -> bool) s then 2788 wp (loopbody :value command) 2789 (expect_lfp 2790 (\(e :value state expect) (s :value state). 2791 (if g s then wp loopbody e s else One s))) s 2792 else 2793 One s)) (s :value state)` 2794 >> METIS_TAC [] 2795 ++ RW_TAC posreal_ss [One_def]) 2796 ++ FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 2797 ++ GEN_TAC 2798 ++ Cases_on `g s` 2799 ++ RW_TAC posreal_ss [preal_max_def, max_lzero, max_rzero] 2800 ++ METIS_TAC [le_trans, posreal_pow_1bounded_base_1bounded]) 2801++ Suff `Leq 2802 (Max 2803 (\(s :value state). 2804 (if 2805 (g :value state -> bool) s /\ (Inv :value state -> bool) s 2806 then 2807 (1 : 2808 posreal) 2809 else 2810 (0 : 2811 posreal))) 2812 (wp (While (\(s :value state). g s) (loopbody :value command)) 2813 (One :value state expect))) 2814 (wp (While (\(s :value state). g s) loopbody) 2815 (One :value state expect))` 2816>> METIS_TAC [leq_trans] 2817++ POP_ASSUM (K ALL_TAC) 2818++ Suff `Leq 2819 (\(s :value state). 2820 (if (g :value state -> bool) s /\ (Inv :value state -> bool) s then 2821 (1 : 2822 posreal) 2823 else 2824 (0 : 2825 posreal))) 2826 (wp (While (\(s :value state). g s) (loopbody :value command)) 2827 (One :value state expect))` 2828>> (FULL_SIMP_TAC posreal_ss [Leq_def, Max_def] 2829 ++ METIS_TAC [le_refl, max_le]) 2830++ FULL_SIMP_TAC posreal_ss [Leq_def] 2831++ GEN_TAC 2832++ Q.UNABBREV_TAC `Inv` 2833++ Q.UNABBREV_TAC `g` 2834++ Q.UNABBREV_TAC `loopbody` 2835++ Q.UNABBREV_TAC `Var` 2836++ FULL_SIMP_TAC posreal_ss [] 2837++ Cases_on `0 <= int_of_value (s i)` 2838>> (Cases_on `int_of_value (s i) < int_of_value (s n)` 2839 >> (`?(n'' :num). int_of_value ((s :value state) (n :string)) = (& n'' :int)` by METIS_TAC [NUM_POSINT_EXISTS, INT_LT_IMP_LE, INT_LE_TRANS] 2840 ++ `(if 2841 int_of_value ((s :value state) (i :string)) < 2842 int_of_value (s (n :string)) /\ (0 :int) <= int_of_value (s i) 2843 then 2844 (1 : 2845 posreal) 2846 else 2847 (0 : 2848 posreal)) <= 2849 (if 2850 (0 :int) <= int_of_value (s i) /\ 2851 int_of_value (s n) - int_of_value (s i) < 2852 (1 :int) + int_of_value (s n) 2853 then 2854 (1 : 2855 posreal) 2856 else 2857 (0 : 2858 posreal))` 2859 by (POP_ASSUM (K ALL_TAC) 2860 ++ POP_ASSUM (K ALL_TAC) 2861 ++ POP_ASSUM (K ALL_TAC) 2862 ++ Q.ABBREV_TAC `n' = int_of_value (s n)` 2863 ++ Q.ABBREV_TAC `i' = int_of_value (s i)` 2864 ++ SIMP_TAC int_ss [INT_LT_SUB_RADD] 2865 ++ `(if (0 :int) <= (i' :int) /\ (n' :int) < (1 :int) + n' + i' then 2866 (1 : 2867 posreal) 2868 else 2869 (0 : 2870 posreal)) = 2871 (if (0 :int) <= i' /\ (0 :int) + n' < (1 :int) + n' + i' then 2872 (1 : 2873 posreal) 2874 else 2875 (0 : 2876 posreal))` by RW_TAC int_ss [] 2877 ++ ASM_REWRITE_TAC [] 2878 ++ POP_ASSUM (K ALL_TAC) 2879 ++ `(if 2880 (0 :int) <= (i' :int) /\ (0 :int) + (n' :int) < (1 :int) + n' + i' 2881 then 2882 (1 : 2883 posreal) 2884 else 2885 (0 : 2886 posreal)) = 2887 (if (0 :int) <= i' /\ (0 :int) < (1 :int) + n' + i' - n' then 2888 (1 : 2889 posreal) 2890 else 2891 (0 : 2892 posreal))` 2893 by METIS_TAC [INT_LT_ADD_SUB] 2894 ++ ASM_REWRITE_TAC [] 2895 ++ POP_ASSUM (K ALL_TAC) 2896 ++ `(1 :int) + (n' :int) + (i' :int) - n' = (1 :int) + i' + n' - n'` 2897 by METIS_TAC [INT_ADD_COMM, INT_ADD_ASSOC] 2898 ++ ASM_REWRITE_TAC [] 2899 ++ POP_ASSUM (K ALL_TAC) 2900 ++ `(1 :int) + (i' :int) + (n' :int) - n' = i' + (1 :int)` 2901 by RW_TAC int_ss [INT_SUB_REFL, INT_ADD_COMM] 2902 ++ ASM_REWRITE_TAC [] 2903 ++ POP_ASSUM (K ALL_TAC) 2904 ++ `(0 :int) <= (i' :int) ==> (0 :int) < i' + (1 :int)` by METIS_TAC [INT_LT_ADD1] 2905 ++ RW_TAC posreal_ss [] 2906 ++ FULL_SIMP_TAC int_ss []) 2907 ++ Suff `(if 2908 (0 :int) <= int_of_value ((s :value state) (i :string)) /\ 2909 int_of_value (s (n :string)) - int_of_value (s i) < 2910 (1 :int) + int_of_value (s n) 2911 then 2912 (1 : 2913 posreal) 2914 else 2915 (0 : 2916 posreal)) <= 2917 wp 2918 (While (\(s :value state). int_of_value (s i) < int_of_value (s n)) 2919 (Seq (body :value command) 2920 (Assign i 2921 (\(s :value state). Int (int_of_value (s i) + (1 :int)))))) 2922 (One :value state expect) s` 2923 >> METIS_TAC [le_trans] 2924 ++ POP_ASSUM (K ALL_TAC) 2925 ++ METIS_TAC []) 2926 ++ METIS_TAC [zero_le]) 2927++ METIS_TAC [zero_le]); 2928 2929val For_i_0_to_n_variant_rule = store_thm 2930 ("For_i_0_to_n_variant_rule", 2931``!(i :string) (n :string) (body :value command list). 2932 ~(n = i) /\ 2933 Leq 2934 (\(s :value state). 2935 (if 2936 (\(s :value state). (0 :int) <= int_of_value (s i)) s 2937 then 2938 (1 : 2939 posreal) 2940 else 2941 (0 : 2942 posreal))) 2943 (wp (Program body) 2944 (\(s :value state). 2945 (if 2946 (\(s :value state). (0 :int) <= int_of_value (s i)) s 2947 then 2948 (1 : 2949 posreal) 2950 else 2951 (0 : 2952 posreal)))) /\ 2953 (!(N :int). 2954 Leq 2955 (\(s :value state). 2956 (if 2957 (\(s :value state). 2958 int_of_value (s i) < int_of_value (s n)) s /\ 2959 (\(s :value state). (0 :int) <= int_of_value (s i)) 2960 s /\ 2961 ((\(s :value state). 2962 int_of_value (s n) - int_of_value (s i)) s = 2963 N) 2964 then 2965 (1 : 2966 posreal) 2967 else 2968 (0 : 2969 posreal))) 2970 (wp (Program body) 2971 (\(s :value state). 2972 (if 2973 (\(s :value state). 2974 int_of_value (s n) - int_of_value (s i)) s <= N 2975 then 2976 (1 : 2977 posreal) 2978 else 2979 (0 : 2980 posreal))))) ==> 2981 (wp (For_0_to_n i n body) (One :value state expect) = 2982 (One :value state expect))``, 2983RW_TAC posreal_ss [For_0_to_n_def, For_def] 2984++ MATCH_MP_TAC leq_antisym 2985++ SIMP_TAC std_ss [Term_Leq_One] 2986++ `wp 2987 (Seq (Assign (i :string) (\(s :value state). Int (0 :int))) 2988 (While 2989 (\(s :value state). 2990 int_of_value (s i) < int_of_value (s (n :string))) 2991 (Seq (Program (body :value command list)) 2992 (Assign i 2993 (\(s :value state). 2994 Int (int_of_value (s i) + (1 :int))))))) = 2995 (\(s :value state expect). 2996 wp (Assign i (\(s :value state). Int (0 :int))) 2997 (wp 2998 (While 2999 (\(s :value state). int_of_value (s i) < int_of_value (s n)) 3000 (Seq (Program body) 3001 (Assign i 3002 (\(s :value state). 3003 Int (int_of_value (s i) + (1 :int)))))) s))` 3004 by METIS_TAC [wp_def] 3005++ ASM_REWRITE_TAC [] 3006++ POP_ASSUM (K ALL_TAC) 3007++ SIMP_TAC std_ss [] 3008++ `wp (Assign (i :string) (\(s :value state). Int (0 :int))) = 3009 (\(r :value state expect) (s :value state). 3010 r (assign i (\(s :value state). Int (0 :int)) s))` 3011 by METIS_TAC [wp_def] 3012++ ASM_REWRITE_TAC [] 3013++ POP_ASSUM (K ALL_TAC) 3014++ SIMP_TAC std_ss [assign_eta, Leq_def] 3015++ GEN_TAC 3016++ `Leq 3017 (\(s :value state). 3018 (if (0 :int) <= int_of_value (s (i :string)) then 3019 (1 : 3020 posreal) 3021 else 3022 (0 : 3023 posreal))) 3024 (wp 3025 (While 3026 (\(s :value state). 3027 int_of_value (s i) < int_of_value (s (n :string))) 3028 (Seq (Program (body :value command list)) 3029 (Assign i 3030 (\(s :value state). 3031 Int (int_of_value (s i) + (1 :int)))))) 3032 (One :value state expect))` 3033 by METIS_TAC [While_variant_rule] 3034++ `!(s :value state). 3035 (\(s :value state). 3036 (if (0 :int) <= int_of_value (s (i :string)) then 3037 (1 : 3038 posreal) 3039 else 3040 (0 : 3041 posreal))) s <= 3042 wp 3043 (While 3044 (\(s :value state). 3045 int_of_value (s i) < int_of_value (s (n :string))) 3046 (Seq (Program (body :value command list)) 3047 (Assign i 3048 (\(s :value state). Int (int_of_value (s i) + (1 :int)))))) 3049 (One :value state expect) s` 3050 by FULL_SIMP_TAC std_ss [Leq_def] 3051++ `(\(s :value state). 3052 (if (0 :int) <= int_of_value (s (i :string)) then 3053 (1 : 3054 posreal) 3055 else 3056 (0 : 3057 posreal))) 3058 (\(w :string). 3059 (if w = i then Int (0 :int) else (s :value state) w)) <= 3060 wp 3061 (While 3062 (\(s :value state). 3063 int_of_value (s i) < int_of_value (s (n :string))) 3064 (Seq (Program (body :value command list)) 3065 (Assign i 3066 (\(s :value state). Int (int_of_value (s i) + (1 :int)))))) 3067 (One :value state expect) 3068 (\(w :string). (if w = i then Int (0 :int) else s w))` 3069 by ASM_REWRITE_TAC [] 3070++ Suff `One (s :value state) <= 3071 (\(s :value state). 3072 (if (0 :int) <= int_of_value (s (i :string)) then 3073 (1 : 3074 posreal) 3075 else 3076 (0 : 3077 posreal))) (\(w :string). (if w = i then Int (0 :int) else s w))` 3078>> METIS_TAC [le_trans] 3079++ SIMP_TAC posreal_ss [One_def, int_of_value_def, INT_LE_REFL]); 3080 3081val bool_Inv_rule = store_thm 3082 ("bool_Inv_rule", 3083 ``!(Inv :num -> 'a state -> bool) (g :'a state -> bool) 3084 (body :'a command). 3085 (!(v :num). 3086 Leq (bool_exp (\(s :'a state). g s /\ Inv v s)) 3087 (wp body 3088 (bool_exp 3089 (\(s :'a state). 3090 ?(v' :num). Inv v' s /\ v' < v)))) ==> 3091 !(v :num). 3092 Leq (bool_exp (Inv v)) 3093 (wp (While g body) 3094 (bool_exp (\(s :'a state). ?(v' :num). Inv v' s /\ ~g s)))``, 3095 REPEAT STRIP_TAC 3096 ++ completeInduct_on `v` 3097 ++ ONCE_REWRITE_TAC [while_unwind_lemma] 3098 ++ RW_TAC posreal_ss [Leq_def] 3099 ++ Cases_on `~(g s)` 3100 >> (FULL_SIMP_TAC bool_ss [] 3101 ++ RW_TAC posreal_ss [bool_exp_def] 3102 ++ METIS_TAC []) 3103 ++ FULL_SIMP_TAC bool_ss [] 3104 ++ RW_TAC posreal_ss [bool_exp_def, zero_le] 3105 ++ FULL_SIMP_TAC posreal_ss [Leq_def, bool_exp_def] 3106 ++ `(1 :posreal) <= 3107 wp (body :'a command) 3108 (\(s :'a state). 3109 (if 3110 ?(v' :num). (Inv :num -> 'a state -> bool) v' s /\ v' < (v :num) 3111 then 3112 (1 : 3113 posreal) 3114 else 3115 (0 : 3116 posreal))) (s :'a state)` 3117 by METIS_TAC [le_refl, zero_le] 3118 ++ `Leq 3119 (\(s :'a state). 3120 (if 3121 ?(v' :num). (Inv :num -> 'a state -> bool) v' s /\ v' < (v :num) 3122 then 3123 (1 : 3124 posreal) 3125 else 3126 (0 : 3127 posreal))) 3128 (wp (While (g :'a state -> bool) (body :'a command)) 3129 (\(s :'a state). 3130 (if ?(v' :num). Inv v' s /\ ~g s then 3131 (1 : 3132 posreal) 3133 else 3134 (0 : 3135 posreal))))` 3136 by (RW_TAC std_ss [Leq_def] 3137 ++ RW_TAC posreal_ss [zero_le, le_refl] 3138 ++ METIS_TAC [zero_le, le_refl]) 3139 ++ `!(prog :'a command) (e0 :'a state expect) (e1 :'a state expect). 3140 Leq e0 e1 ==> Leq (wp prog e0) (wp prog e1)` by METIS_TAC [wp_mono] 3141 ++ FULL_SIMP_TAC posreal_ss [Leq_def] 3142 ++ `!(s :'a state). 3143 (\(s :'a state). 3144 (if 3145 ?(v' :num). (Inv :num -> 'a state -> bool) v' s /\ v' < (v :num) 3146 then 3147 (1 : 3148 posreal) 3149 else 3150 (0 : 3151 posreal))) s <= 3152 wp (While (g :'a state -> bool) (body :'a command)) 3153 (\(s :'a state). 3154 (if ?(v' :num). Inv v' s /\ ~g s then 3155 (1 : 3156 posreal) 3157 else 3158 (0 : 3159 posreal))) s` 3160 by ASM_SIMP_TAC std_ss [] 3161 ++`!(s :'a state). 3162 wp (body :'a command) 3163 (\(s :'a state). 3164 (if 3165 ?(v' :num). 3166 (Inv :num -> 'a state -> bool) v' s /\ v' < (v :num) 3167 then 3168 (1 : 3169 posreal) 3170 else 3171 (0 : 3172 posreal))) s <= 3173 wp body 3174 (wp (While (g :'a state -> bool) body) 3175 (\(s :'a state). 3176 (if ?(v' :num). Inv v' s /\ ~g s then 3177 (1 : 3178 posreal) 3179 else 3180 (0 : 3181 posreal)))) s` 3182 by RW_TAC posreal_ss [] 3183 ++ METIS_TAC [le_trans]); 3184 3185val assign_while_immediate_term = store_thm 3186 ("assign_while_immediate_term", 3187 ``!(i :string) (body :value command) (n :num) 3188 (postE :value state expect). 3189 wp (Assign i (\(s :value state). Int (& n :int))) 3190 (wp 3191 (While (\(s :value state). int_of_value (s i) < (& n :int)) 3192 body) postE) = 3193 wp (Assign i (\(s :value state). Int (& n :int))) postE``, 3194 REPEAT GEN_TAC 3195 ++ Q.ABBREV_TAC `g = (\(s :value state). 3196 int_of_value (s (i :string)) < (& (n :num) :int))` 3197 ++ `wp (While (g :value state -> bool) (body :value command)) 3198 (postE :value state expect) = 3199 (\(s :value state). 3200 (if g s then wp body (wp (While g body) postE) s else postE s))` 3201 by METIS_TAC [while_unwind_lemma] 3202 ++ Q.ABBREV_TAC `foo = (\(s :value state). 3203 (if (g :value state -> bool) s then 3204 wp (body :value command) 3205 (wp (While g body) (postE :value state expect)) s 3206 else 3207 postE s))` 3208 ++ ASM_REWRITE_TAC [] 3209 ++ Q.UNABBREV_TAC `foo` 3210 ++ POP_ASSUM (K ALL_TAC) 3211 ++ Q.UNABBREV_TAC `g` 3212 ++ RW_TAC int_ss [int_of_value_def, wp_assign]); 3213 3214val while_reverse_unwind_part1 = store_thm 3215 ("while_reverse_unwind_part1", 3216 ``!(body :value command) (i :string) (postE :'a). 3217 (!(postE :value state expect) (m :num). 3218 (\(s :value state). 3219 wp body 3220 (\(s :value state). 3221 postE 3222 (\(w :string). 3223 (if w = i then 3224 Int (& (m + (1 :num)) :int) 3225 else 3226 s w))) 3227 (\(w :string). 3228 (if w = i then Int (& m :int) else s w))) = 3229 (\(s :value state). 3230 wp body 3231 (\(s :value state). 3232 postE 3233 (\(w :string). 3234 (if w = i then 3235 Int (int_of_value (s i) + (1 :int)) 3236 else 3237 s w))) 3238 (\(w :string). 3239 (if w = i then Int (& m :int) else s w)))) ==> 3240 !(m :num) (n :num) (postE :value state expect). 3241 m < n ==> 3242 (wp (Assign i (\(s :value state). Int (& m :int))) 3243 (wp 3244 (While 3245 (\(s :value state). int_of_value (s i) < (& n :int)) 3246 (Seq body 3247 (Assign i 3248 (\(s :value state). 3249 Int (int_of_value (s i) + (1 :int)))))) 3250 postE) = 3251 wp (Assign i (\(s :value state). Int (& m :int))) 3252 (wp body 3253 (wp 3254 (Assign i 3255 (\(s :value state). Int (& (m + (1 :num)) :int))) 3256 (wp 3257 (While 3258 (\(s :value state). 3259 int_of_value (s i) < (& n :int)) 3260 (Seq body 3261 (Assign i 3262 (\(s :value state). 3263 Int (int_of_value (s i) + (1 :int)))))) 3264 postE))))``, 3265 REPEAT STRIP_TAC 3266 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3267 (wp 3268 (While (\(s :value state). int_of_value (s i) < (& (n :num) :int)) 3269 (Seq (body :value command) 3270 (Assign i 3271 (\(s :value state). 3272 Int (int_of_value (s i) + (1 :int)))))) 3273 (postE :value state expect)) = 3274 wp (Assign i (\(s :value state). Int (& m :int))) 3275 (\(s :value state). 3276 (if (\(s :value state). int_of_value (s i) < (& n :int)) s then 3277 wp 3278 (Seq body 3279 (Assign i 3280 (\(s :value state). 3281 Int (int_of_value (s i) + (1 :int))))) 3282 (wp 3283 (While (\(s :value state). int_of_value (s i) < (& n :int)) 3284 (Seq body 3285 (Assign i 3286 (\(s :value state). 3287 Int (int_of_value (s i) + (1 :int)))))) postE) 3288 s 3289 else 3290 postE s))` 3291 by (`wp 3292 (While 3293 (\(s :value state). 3294 int_of_value (s (i :string)) < (& (n :num) :int)) 3295 (Seq (body :value command) 3296 (Assign i 3297 (\(s :value state). Int (int_of_value (s i) + (1 :int)))))) 3298 (postE :value state expect) = 3299 (\(s :value state). 3300 (if (\(s :value state). int_of_value (s i) < (& n :int)) s then 3301 wp 3302 (Seq body 3303 (Assign i 3304 (\(s :value state). Int (int_of_value (s i) + (1 :int))))) 3305 (wp 3306 (While (\(s :value state). int_of_value (s i) < (& n :int)) 3307 (Seq body 3308 (Assign i 3309 (\(s :value state). 3310 Int (int_of_value (s i) + (1 :int)))))) postE) s 3311 else 3312 postE s))` 3313 by (Q.ABBREV_TAC `g = (\(s :value state). 3314 int_of_value (s (i :string)) < (& (n :num) :int))` 3315 ++ METIS_TAC [while_unwind_lemma]) 3316 ++ Q.ABBREV_TAC `foo = 3317 (\(s :value state). 3318 (if 3319 (\(s :value state). 3320 int_of_value (s (i :string)) < (& (n :num) :int)) s 3321 then 3322 wp 3323 (Seq (body :value command) 3324 (Assign i 3325 (\(s :value state). 3326 Int (int_of_value (s i) + (1 :int))))) 3327 (wp 3328 (While 3329 (\(s :value state). 3330 int_of_value (s i) < (& n :int)) 3331 (Seq body 3332 (Assign i 3333 (\(s :value state). 3334 Int (int_of_value (s i) + (1 :int)))))) 3335 (postE :value state expect)) s 3336 else 3337 postE s))` 3338 ++ ASM_REWRITE_TAC []) 3339 ++ ASM_REWRITE_TAC [] 3340 ++ POP_ASSUM (K ALL_TAC) 3341 ++ RW_TAC std_ss [int_of_value_def, wp_seq, wp_assign] 3342 ++ `(& (m :num) :int) < (& (n :num) :int)` by RW_TAC int_ss [] 3343 ++ ASM_REWRITE_TAC []); 3344 3345val while_reverse_unwind_lemma = store_thm 3346 ("while_reverse_unwind_lemma", 3347 ``!(n :num) (m :num) (body :value command) (i :string) 3348 (postE :value state expect). 3349 (!(postE :value state expect) (m :num). 3350 (\(s :value state). 3351 wp body 3352 (\(s :value state). 3353 postE 3354 (\(w :string). 3355 (if w = i then 3356 Int (& (m + (1 :num)) :int) 3357 else 3358 s w))) 3359 (\(w :string). 3360 (if w = i then Int (& m :int) else s w))) = 3361 (\(s :value state). 3362 wp body 3363 (\(s :value state). 3364 postE 3365 (\(w :string). 3366 (if w = i then 3367 Int (int_of_value (s i) + (1 :int)) 3368 else 3369 s w))) 3370 (\(w :string). 3371 (if w = i then Int (& m :int) else s w)))) /\ 3372 m <= n ==> 3373 (wp 3374 (Seq (Assign i (\(s :value state). Int (& m :int))) 3375 (While 3376 (\(s :value state). 3377 int_of_value (s i) < (& (SUC n) :int)) 3378 (Seq body 3379 (Assign i 3380 (\(s :value state). 3381 Int (int_of_value (s i) + (1 :int))))))) 3382 postE = 3383 wp 3384 (Seq (Assign i (\(s :value state). Int (& m :int))) 3385 (Seq 3386 (While 3387 (\(s :value state). int_of_value (s i) < (& n :int)) 3388 (Seq body 3389 (Assign i 3390 (\(s :value state). 3391 Int (int_of_value (s i) + (1 :int)))))) 3392 (Seq body 3393 (Assign i 3394 (\(s :value state). 3395 Int (int_of_value (s i) + (1 :int))))))) postE)``, 3396 REPEAT STRIP_TAC 3397 ++ `!(m :num) (n :num) (postE :value state expect). 3398 m < n ==> 3399 (wp (Assign (i :string) (\(s :value state). Int (& m :int))) 3400 (wp 3401 (While (\(s :value state). int_of_value (s i) < (& n :int)) 3402 (Seq (body :value command) 3403 (Assign i 3404 (\(s :value state). 3405 Int (int_of_value (s i) + (1 :int)))))) postE) = 3406 wp (Assign i (\(s :value state). Int (& m :int))) 3407 (wp body 3408 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int))) 3409 (wp 3410 (While 3411 (\(s :value state). int_of_value (s i) < (& n :int)) 3412 (Seq body 3413 (Assign i 3414 (\(s :value state). 3415 Int (int_of_value (s i) + (1 :int)))))) 3416 postE))))` 3417 by METIS_TAC [while_reverse_unwind_part1] 3418 ++ Q.ABBREV_TAC `loopbody = Seq (body :value command) 3419 (Assign (i :string) 3420 (\(s :value state). Int (int_of_value (s i) + (1 :int))))` 3421 ++ Induct_on `n - m` 3422 >> (RW_TAC arith_ss [INT] 3423 ++ SIMP_TAC std_ss [wp_seq] 3424 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3425 (wp 3426 (While (\(s :value state). int_of_value (s i) < (& (n :num) :int)) 3427 (loopbody :value command)) 3428 (wp loopbody (postE :value state expect))) = 3429 wp (Assign i (\(s :value state). Int (& m :int))) (wp loopbody postE)` 3430 by (`(m :num) = (n :num)` by RW_TAC arith_ss [LESS_EQ_ANTISYM] 3431 ++ METIS_TAC [assign_while_immediate_term]) 3432 ++ ASM_REWRITE_TAC [] 3433 ++ POP_ASSUM (K ALL_TAC) 3434 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3435 (wp 3436 (While 3437 (\(s :value state). 3438 int_of_value (s i) < (& (n :num) :int) + (1 :int)) 3439 (loopbody :value command)) (postE :value state expect)) = 3440 wp (Assign i (\(s :value state). Int (& m :int))) 3441 (wp (body :value command) 3442 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int))) 3443 postE))` 3444 by (`wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3445 (wp 3446 (While 3447 (\(s :value state). 3448 int_of_value (s i) < (& (n :num) :int) + (1 :int)) 3449 (loopbody :value command)) (postE :value state expect)) = 3450 wp (Assign i (\(s :value state). Int (& n :int))) 3451 (wp (body :value command) 3452 (wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) 3453 (wp 3454 (While 3455 (\(s :value state). 3456 int_of_value (s i) < (& (n + (1 :num)) :int)) loopbody) 3457 postE)))` 3458 by (`(m :num) = (n :num)` by RW_TAC arith_ss [LESS_EQ_ANTISYM] 3459 ++ `(& ((n :num) + (1 :num)) :int) = (& n :int) + (1 :int)` by RW_TAC int_ss [INT_ADD] 3460 ++ `(n :num) < n + (1 :num)` by RW_TAC arith_ss [] 3461 ++ METIS_TAC []) 3462 ++ `wp 3463 (Assign (i :string) 3464 (\(s :value state). Int (& ((n :num) + (1 :num)) :int))) 3465 (wp 3466 (While 3467 (\(s :value state). 3468 int_of_value (s i) < (& (n + (1 :num)) :int)) 3469 (loopbody :value command)) (postE :value state expect)) = 3470 wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) postE` 3471 by METIS_TAC [assign_while_immediate_term] 3472 ++ `(m:num) = (n:num)` by RW_TAC arith_ss [LESS_EQ_ANTISYM] 3473 ++ ASM_REWRITE_TAC []) 3474 ++ ASM_REWRITE_TAC [] 3475 ++ POP_ASSUM (K ALL_TAC) 3476 ++ Q.UNABBREV_TAC `loopbody` 3477 ++ RW_TAC std_ss [int_of_value_def, wp_seq, wp_assign]) 3478 ++ REPEAT STRIP_TAC 3479 ++ FULL_SIMP_TAC std_ss [INT] 3480 ++ `(v :num) = (n :num) - ((m :num) + (1 :num))` 3481 by RW_TAC arith_ss [] 3482 ++ `(m :num) + (1 :num) <= (n :num) ==> 3483 (wp 3484 (Seq 3485 (Assign (i :string) 3486 (\(s :value state). Int (& (m + (1 :num)) :int))) 3487 (While 3488 (\(s :value state). int_of_value (s i) < (& n :int) + (1 :int)) 3489 (loopbody :value command))) (postE :value state expect) = 3490 wp 3491 (Seq (Assign i (\(s :value state). Int (& (m + (1 :num)) :int))) 3492 (Seq 3493 (While (\(s :value state). int_of_value (s i) < (& n :int)) 3494 loopbody) loopbody)) postE)` 3495 by METIS_TAC [] 3496 ++ Cases_on `m < n` 3497 >> (`(m :num) + (1 :num) <= (n :num)` by RW_TAC arith_ss [] 3498 ++ FULL_SIMP_TAC std_ss [wp_seq] 3499 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3500 (wp 3501 (While 3502 (\(s :value state). 3503 int_of_value (s i) < (& (n :num) :int) + (1 :int)) 3504 (loopbody :value command)) (postE :value state expect)) = 3505 wp (Assign i (\(s :value state). Int (& m :int))) 3506 (wp (body :value command) 3507 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int))) 3508 (wp 3509 (While 3510 (\(s :value state). 3511 int_of_value (s i) < (& n :int) + (1 :int)) loopbody) 3512 postE)))` 3513 by (`(m :num) < (n :num) + (1 :num)` by RW_TAC arith_ss [] 3514 ++ `wp (Assign (i :string) (\(s :value state). Int (& (m :num) :int))) 3515 (wp 3516 (While 3517 (\(s :value state). 3518 int_of_value (s i) < (& ((n :num) + (1 :num)) :int)) 3519 (loopbody :value command)) (postE :value state expect)) = 3520 wp (Assign i (\(s :value state). Int (& m :int))) 3521 (wp (body :value command) 3522 (wp (Assign i (\(s :value state). Int (& (m + (1 :num)) :int))) 3523 (wp 3524 (While 3525 (\(s :value state). 3526 int_of_value (s i) < (& (n + (1 :num)) :int)) loopbody) 3527 postE)))` by METIS_TAC [] 3528 ++ `(& ((n :num) + (1 :num)) :int) = (& n :int) + (1 :int)` by RW_TAC int_ss [INT_ADD] 3529 ++ FULL_SIMP_TAC std_ss []) 3530 ++ ASM_REWRITE_TAC []) 3531 ++ `(m:num) = (n:num)` by RW_TAC arith_ss [] 3532 ++ ASM_REWRITE_TAC [assign_while_immediate_term, wp_seq] 3533 ++ POP_ASSUM (K ALL_TAC) 3534 ++ `wp (Assign (i :string) (\(s :value state). Int (& (n :num) :int))) 3535 (wp 3536 (While 3537 (\(s :value state). 3538 int_of_value (s i) < (& (n + (1 :num)) :int)) 3539 (loopbody :value command)) (postE :value state expect)) = 3540 wp (Assign i (\(s :value state). Int (& n :int))) 3541 (wp (body :value command) 3542 (wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) 3543 (wp 3544 (While 3545 (\(s :value state). 3546 int_of_value (s i) < (& (n + (1 :num)) :int)) loopbody) 3547 postE)))` 3548 by (`(n :num) < n + (1 :num)` by RW_TAC arith_ss [] 3549 ++ METIS_TAC []) 3550 ++ `wp 3551 (Assign (i :string) 3552 (\(s :value state). Int (& ((n :num) + (1 :num)) :int))) 3553 (wp 3554 (While 3555 (\(s :value state). 3556 int_of_value (s i) < (& (n + (1 :num)) :int)) 3557 (loopbody :value command)) (postE :value state expect)) = 3558 wp (Assign i (\(s :value state). Int (& (n + (1 :num)) :int))) postE` 3559 by METIS_TAC [assign_while_immediate_term] 3560 ++ FULL_SIMP_TAC std_ss [] 3561 ++ POP_ASSUM (K ALL_TAC) 3562 ++ `While 3563 (\(s :value state). 3564 int_of_value (s (i :string)) < (& ((n :num) + (1 :num)) :int)) 3565 (loopbody :value command) = 3566 While (\(s :value state). int_of_value (s i) < (& n :int) + (1 :int)) 3567 loopbody` 3568 by (`(& ((n :num) + (1 :num)) :int) = (& n :int) + (1 :int)` by RW_TAC int_ss [INT_ADD] 3569 ++ METIS_TAC []) 3570 ++ FULL_SIMP_TAC std_ss [] 3571 ++ POP_ASSUM (K ALL_TAC) 3572 ++ POP_ASSUM (K ALL_TAC) 3573 ++ Q.UNABBREV_TAC `loopbody` 3574 ++ RW_TAC std_ss [int_of_value_def, wp_seq, wp_assign]); 3575 3576val For_reverse_unwind_lemma = store_thm 3577 ("For_reverse_unwind_lemma", 3578 ``!(n :num) (m :num) (body :value command) (i :string) 3579 (postE :value state expect). 3580 (!(postE :value state expect) (m :num). 3581 (\(s :value state). 3582 wp body 3583 (\(s :value state). 3584 postE 3585 (\(w :string). 3586 (if w = i then 3587 Int (& (m + (1 :num)) :int) 3588 else 3589 s w))) 3590 (\(w :string). 3591 (if w = i then Int (& m :int) else s w))) = 3592 (\(s :value state). 3593 wp body 3594 (\(s :value state). 3595 postE 3596 (\(w :string). 3597 (if w = i then 3598 Int (int_of_value (s i) + (1 :int)) 3599 else 3600 s w))) 3601 (\(w :string). 3602 (if w = i then Int (& m :int) else s w)))) /\ 3603 m <= n ==> 3604 (wp 3605 (For i (\(s :value state). Int (& m :int)) 3606 (\(s :value state). int_of_value (s i) < (& (SUC n) :int)) 3607 (\(s :value state). Int (int_of_value (s i) + (1 :int))) 3608 [body]) postE = 3609 wp 3610 (Seq 3611 (For i (\(s :value state). Int (& m :int)) 3612 (\(s :value state). int_of_value (s i) < (& n :int)) 3613 (\(s :value state). Int (int_of_value (s i) + (1 :int))) 3614 [body]) 3615 (Seq body 3616 (Assign i 3617 (\(s :value state). 3618 Int (int_of_value (s i) + (1 :int)))))) postE)``, 3619 RW_TAC std_ss [For_def, Program_def] 3620 ++ METIS_TAC [while_reverse_unwind_lemma, wp_seq]); 3621 3622val For_0_to_n_reverse_unwind_lemma = store_thm 3623 ("For_0_to_n_reverse_unwind_lemma", 3624 ``!(n :num) (body :value command) (i :string) 3625 (postE :value state expect). 3626 (!(postE :value state expect) (m :num). 3627 (\(s :value state). 3628 wp body 3629 (\(s :value state). 3630 postE 3631 (\(w :string). 3632 (if w = i then 3633 Int (& (m + (1 :num)) :int) 3634 else 3635 s w))) 3636 (\(w :string). 3637 (if w = i then Int (& m :int) else s w))) = 3638 (\(s :value state). 3639 wp body 3640 (\(s :value state). 3641 postE 3642 (\(w :string). 3643 (if w = i then 3644 Int (int_of_value (s i) + (1 :int)) 3645 else 3646 s w))) 3647 (\(w :string). 3648 (if w = i then Int (& m :int) else s w)))) ==> 3649 (wp 3650 (For i (\(s :value state). Int (0 :int)) 3651 (\(s :value state). int_of_value (s i) < (& (SUC n) :int)) 3652 (\(s :value state). Int (int_of_value (s i) + (1 :int))) 3653 [body]) postE = 3654 wp 3655 (Seq 3656 (For i (\(s :value state). Int (0 :int)) 3657 (\(s :value state). int_of_value (s i) < (& n :int)) 3658 (\(s :value state). Int (int_of_value (s i) + (1 :int))) 3659 [body]) 3660 (Seq body 3661 (Assign i 3662 (\(s :value state). 3663 Int (int_of_value (s i) + (1 :int)))))) postE)``, 3664 REPEAT STRIP_TAC 3665 ++ `(0 :num) <= (n :num)` by RW_TAC arith_ss [] 3666 ++ `0 = &0` by RW_TAC int_ss [] 3667 ++ METIS_TAC [For_reverse_unwind_lemma]); 3668 3669val _ = export_theory(); 3670