1(*****************************************************************************) 2(* MachineTransitionScript.sml *) 3(* --------------------------- *) 4(* *) 5(* Script for proving theorems to support DerivedBddRules *) 6(*****************************************************************************) 7(* *) 8(* Revision history: *) 9(* *) 10(* Wed Nov 7 11:29:35 GMT 2001 -- created file *) 11(* *) 12(*****************************************************************************) 13 14open HolKernel Parse boolLib; 15 16open tautLib; 17open bossLib; 18open simpLib; 19open numLib; 20open pairLib; 21open arithmeticTheory; 22open listTheory; 23open pairTheory; 24open Ho_Rewrite; 25open Num_conv; 26 27val _ = new_theory "MachineTransition"; 28 29(* These two don't seem to be used ... 30 31val DEPTH_EXISTS_CONV = unwindLib.DEPTH_EXISTS_CONV 32and EXPAND_AUTO_CONV = unwindLib.EXPAND_AUTO_CONV; 33*) 34 35fun prove_thm(_:string,tm,tac) = prove(tm,tac); 36 37 38(*****************************************************************************) 39(* ``Next R B state'' is true if state can be reached from *) 40(* a state satisfying B in one R-step *) 41(*****************************************************************************) 42 43val Next_def = 44 Define 45 `Next R B state = 46 ?state_. B state_ /\ R(state_,state)`; 47 48(*****************************************************************************) 49(* ``Prev R Q state'' is the set of states from which Q can be reached *) 50(* in one transition *) 51(*****************************************************************************) 52 53val Prev_def = 54 Define 55 `Prev R Q state = ?state'. R(state,state') /\ Q state'`; 56 57(*****************************************************************************) 58(* Characteristic function of a set with just one state *) 59(*****************************************************************************) 60 61val Eq_def = 62 Define 63 `Eq state0 state = (state0 = state)`; 64 65val Prev_Next_Eq = 66 prove_thm 67 ("Prev_Next_Eq", 68 ``!R s s'. Prev R (Eq s') s = Next R (Eq s) s'``, 69 PROVE_TAC[Prev_def,Next_def,Eq_def]); 70 71(*****************************************************************************) 72(* ``ReachIn n R B state'' is true if state can be reached from *) 73(* a state satisfying B in exactly n R-steps *) 74(*****************************************************************************) 75 76val ReachIn_def = 77 Define 78 `(ReachIn R B 0 = B) 79 /\ 80 (ReachIn R B (SUC n) = Next R (ReachIn R B n))`; 81 82val ReachIn_rec = 83 store_thm 84 ("ReachIn_rec", 85 ``(!R B state. 86 ReachIn R B 0 state = B state) 87 /\ 88 (!R B n state. 89 ReachIn R B (SUC n) state = 90 (?state_. ReachIn R B n state_ /\ R(state_,state)))``, 91 PROVE_TAC[ReachIn_def,Next_def]); 92 93val ReachIn_Next = 94 prove_thm 95 ("ReachIn_Next", 96 ``!n. ReachIn R (Next R B) n = ReachIn R B (SUC n)``, 97 Induct 98 THEN RW_TAC std_ss [ReachIn_def,Next_def]); 99 100val ReachIn_expand = 101 prove_thm 102 ("ReachIn_expand", 103 ``!n. ReachIn R (Next R B) n state = 104 (?state_. ReachIn R B n state_ /\ R(state_,state))``, 105 PROVE_TAC[ReachIn_def,Next_def,ReachIn_Next]); 106 107val Next_ReachIn = 108 prove_thm 109 ("Next_ReachIn", 110 ``!n. Next R (ReachIn R B n) = ReachIn R B (SUC n)``, 111 RW_TAC std_ss [ReachIn_def]); 112 113(*****************************************************************************) 114(* ``Reachable R B state'' is true if state can be reached from a *) 115(* state satisfying B in some finite number of R-steps *) 116(*****************************************************************************) 117 118val Reachable_def = 119 Define 120 `Reachable R B state = ?n. ReachIn R B n state`; 121 122val Reachable_eqn = 123 prove_thm 124 ("Reachable_eqn", 125 ``Reachable R B state = 126 B state \/ Reachable R (Next R B) state``, 127 REWRITE_TAC[Reachable_def,ReachIn_def,Next_def] 128 THEN EQ_TAC 129 THEN REPEAT STRIP_TAC 130 THENL[DISJ_CASES_TAC(SPEC ``n:num`` num_CASES) 131 THENL[PROVE_TAC[ReachIn_def], 132 PROVE_TAC[ReachIn_Next]], 133 EXISTS_TAC ``0`` 134 THEN ASM_REWRITE_TAC[ReachIn_def], 135 PROVE_TAC[ReachIn_Next]]); 136 137val ReachBy_def = 138 Define 139 `ReachBy R B n state = 140 ?m. (m <= n) /\ ReachIn R B m state`; 141 142val ReachIn_IMPLIES_ReachBy = 143 prove_thm 144 ("ReachIn_IMPLIES_ReachBy", 145 ``ReachIn R B n state ==> ReachBy R B n state``, 146 PROVE_TAC[ReachBy_def,LESS_EQ_REFL]); 147 148(* Proof of ReachBy_lemma below is gross -- done in zombie mode *) 149 150val ReachBy_lemma = 151 prove_thm 152 ("ReachBy_lemma", 153 ``(!R B state. 154 ReachBy R B 0 state = B state) 155 /\ 156 (!R B n state. 157 ReachBy R B (SUC n) state = 158 ReachBy R B n state 159 \/ 160 Next R (ReachBy R B n) state)``, 161 REWRITE_TAC[ReachBy_def,ReachIn_def,LESS_EQ_0] 162 THEN CONJ_TAC 163 THEN REPEAT GEN_TAC 164 THENL 165 [PROVE_TAC[ReachIn_def], 166 REWRITE_TAC[ReachBy_def] 167 THEN EQ_TAC 168 THEN REPEAT STRIP_TAC 169 THENL 170 [ASSUM_LIST(fn[th1,th2]=> 171 DISJ_CASES_TAC 172 (EQ_MP 173 (DECIDE ``(m <= SUC n) = (m <= n) \/ (m = SUC n)``) 174 th2)) 175 THENL 176 [PROVE_TAC[], 177 DISJ2_TAC 178 THEN REWRITE_TAC[Next_def,ReachBy_def] 179 THEN ASSUM_LIST 180 (fn[th1,th2,th3] => ASSUME_TAC(REWRITE_RULE[th1]th2)) 181 THEN IMP_RES_TAC(REWRITE_RULE[ReachIn_Next]ReachIn_expand) 182 THEN EXISTS_TAC ``state_:'b`` 183 THEN ASM_REWRITE_TAC[] 184 THEN EXISTS_TAC ``n:num`` 185 THEN RW_TAC arith_ss []], 186 PROVE_TAC[DECIDE``(m<=n)==>(m<=SUC n)``], 187 POP_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE[Next_def,ReachBy_def]) 188 THEN IMP_RES_TAC ReachIn_expand 189 THEN EXISTS_TAC ``SUC m`` 190 THEN ASM_REWRITE_TAC 191 [GSYM(ReachIn_Next),DECIDE``(SUC m<=SUC n)=(m<=n)``]]]); 192 193val ReachBy_rec = 194 store_thm 195 ("ReachBy_rec", 196 ``(!R B state. 197 ReachBy R B 0 state = B state) 198 /\ 199 (!R B n state. 200 ReachBy R B (SUC n) state = 201 ReachBy R B n state 202 \/ 203 ?state_. ReachBy R B n state_ /\ R (state_,state))``, 204 PROVE_TAC[ReachBy_lemma,Next_def]); 205 206val ReachBy_ReachIn = 207 store_thm 208 ("ReachBy_ReachIn", 209 ``(!R B state. 210 ReachBy R B 0 state = B state) 211 /\ 212 (!R B n state. 213 ReachBy R B (SUC n) state = 214 ReachBy R B n state \/ ReachIn R B (SUC n) state)``, 215 REWRITE_TAC[ReachBy_def,ReachIn_def,LESS_EQ_0] 216 THEN CONJ_TAC 217 THEN REPEAT GEN_TAC 218 THENL 219 [PROVE_TAC[ReachIn_def], 220 EQ_TAC 221 THEN REPEAT STRIP_TAC 222 THENL 223 [ASSUM_LIST(fn[th1,th2]=> 224 DISJ_CASES_TAC 225 (EQ_MP 226 (DECIDE ``(m <= SUC n) = (m <= n) \/ (m = SUC n)``) 227 th2)) 228 THEN PROVE_TAC[Next_ReachIn], 229 PROVE_TAC[DECIDE ``m <= n ==> m <= SUC n``], 230 EXISTS_TAC ``SUC n`` 231 THEN ASM_REWRITE_TAC[LESS_EQ_REFL,GSYM Next_ReachIn]]]); 232 233val Reachable_ReachBy = 234 store_thm 235 ("Reachable_ReachBy", 236 ``Reachable R B state = ?n. ReachBy R B n state``, 237 PROVE_TAC[Reachable_def,ReachBy_def,LESS_EQ_REFL]); 238 239val ReachBy_mono = 240 prove_thm 241 ("ReachBy_mono", 242 ``!m. ReachBy R B m state 243 ==> 244 !n. ReachBy R B (m+n) state``, 245 REWRITE_TAC[ReachBy_def] 246 THEN GEN_TAC 247 THEN DISCH_TAC 248 THEN Induct 249 THEN ASM_REWRITE_TAC[ADD_CLAUSES] 250 THEN POP_ASSUM STRIP_ASSUME_TAC 251 THEN ASSUM_LIST 252 (fn[th1,th2,th3] 253 => ASSUME_TAC(MP(DECIDE``(m' <= m + n)==>(m'<=SUC(m+n))``)th2)) 254 THEN PROVE_TAC[]); 255 256val ReachBy_mono_cor = 257 prove_thm 258 ("ReachBy_mono_cor", 259 ``ReachBy R B n state 260 ==> 261 ReachBy R B (SUC n) state``, 262 PROVE_TAC[ReachBy_mono,DECIDE``SUC n = n+1``]); 263 264val ReachBy_LESS = 265 prove_thm 266 ("ReachBy_LESS", 267 ``!n m. m <= n /\ ReachIn R B m state 268 ==> ReachBy R B n state``, 269 Induct 270 THEN PROVE_TAC [ReachBy_def]); 271 272val Next_ReachIn_ReachBy = 273 prove_thm 274 ("Next_ReachIn_ReachBy", 275 ``!n. Next R (ReachIn R B n) state 276 ==> 277 Next R (ReachBy R B n) state``, 278 PROVE_TAC[LESS_EQ_REFL,ReachBy_LESS,Next_def]); 279 280val fixedpoint_Next = 281 prove_thm 282 ("fixedpoint_Next", 283 ``(ReachBy R B n = ReachBy R B (SUC n)) 284 ==> 285 (!state'. Next R (ReachBy R B n) state' 286 ==> 287 ReachBy R B n state')``, 288 CONV_TAC(DEPTH_CONV FUN_EQ_CONV) 289 THEN REWRITE_TAC[ReachBy_ReachIn,ReachIn_def,Next_def] 290 THEN REPEAT STRIP_TAC 291 THEN ASSUM_LIST 292 (fn[th1,th2,th3]=> 293 STRIP_ASSUME_TAC 294 (MATCH_MP (DECIDE``(A = A \/ B) ==> (B ==> A)``) 295 (SPEC ``state':'a`` th3))) 296 THEN POP_ASSUM(MAP_EVERY ASSUME_TAC o IMP_CANON) 297 THEN IMP_RES_TAC ReachBy_def 298 THEN IMP_RES_TAC (DECIDE ``(m<=n)==>(m=n) \/(m<n)``) 299 THEN PROVE_TAC 300 [REWRITE_RULE[Next_def]((CONV_RULE(DEPTH_CONV FUN_EQ_CONV))ReachIn_def), 301 DECIDE``(m<n)==>(SUC m<=n)``, 302 ReachBy_LESS]); 303 304val fixedpoint_Next_cor = 305 prove_thm 306 ("fixedpoint_Next_cor", 307 ``(ReachBy R B n = ReachBy R B (SUC n)) 308 ==> 309 (!state'. Next R (ReachBy R B (SUC n)) state' 310 ==> 311 ReachBy R B (SUC n) state')``, 312 PROVE_TAC[fixedpoint_Next]); 313 314val fixedpoint_SUC = 315 prove_thm 316 ("fixedpoint_SUC", 317 ``(ReachBy R B n = ReachBy R B (SUC n)) 318 ==> 319 (ReachBy R B (SUC n) = ReachBy R B (SUC(SUC n)))``, 320 DISCH_TAC 321 THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) 322 THEN GEN_TAC 323 THEN EQ_TAC 324 THEN REPEAT STRIP_TAC 325 THENL 326 [IMP_RES_TAC ReachBy_mono_cor, 327 POP_ASSUM(ASSUME_TAC o ONCE_REWRITE_RULE[ReachBy_ReachIn]) 328 THEN POP_ASSUM(ASSUME_TAC o ONCE_REWRITE_RULE[ReachIn_def]) 329 THEN PROVE_TAC [Next_ReachIn_ReachBy,fixedpoint_Next_cor]]); 330 331val fixedpoint_lemma1 = 332 prove_thm 333 ("fixedpoint_lemma1", 334 ``(ReachBy R B n = ReachBy R B (SUC n)) 335 ==> 336 !m. ReachBy R B (n+m) = ReachBy R B (SUC(n+m))``, 337 DISCH_TAC 338 THEN Induct 339 THEN ASM_REWRITE_TAC[ADD_CLAUSES] 340 THEN IMP_RES_TAC fixedpoint_SUC); 341 342val fixedpoint_lemma2 = 343 prove_thm 344 ("fixedpoint_lemma2", 345 ``(ReachBy R B n = ReachBy R B (SUC n)) 346 ==> 347 !m. ReachBy R B n = ReachBy R B (n+m)``, 348 DISCH_TAC 349 THEN Induct 350 THEN PROVE_TAC[ADD_CLAUSES,fixedpoint_lemma1]); 351 352val ReachBy_fixedpoint = 353 store_thm 354 ("ReachBy_fixedpoint", 355 ``!R B n. 356 (ReachBy R B n = ReachBy R B (SUC n)) 357 ==> 358 (Reachable R B = ReachBy R B n)``, 359 REPEAT STRIP_TAC 360 THEN CONV_TAC(DEPTH_CONV FUN_EQ_CONV) 361 THEN REWRITE_TAC[Reachable_def] 362 THEN GEN_TAC 363 THEN EQ_TAC 364 THEN REPEAT STRIP_TAC 365 THENL 366 [ASM_CASES_TAC ``n'<=n`` 367 THENL 368 [IMP_RES_TAC ReachBy_def, 369 IMP_RES_TAC(DECIDE``~(n' <= n) ==> n < n'``) 370 THEN IMP_RES_TAC(ONCE_REWRITE_RULE[ADD_SYM]LESS_ADD) 371 THEN IMP_RES_TAC ReachIn_IMPLIES_ReachBy 372 THEN PROVE_TAC[fixedpoint_lemma2]], 373 PROVE_TAC[ReachBy_def]]); 374 375val EXISTS_IMP_EQ = 376 store_thm 377 ("EXISTS_IMP_EQ", 378 ``((?x. P x) ==> Q) = (!x. P x ==> Q)``, 379 PROVE_TAC[]); 380 381val LENGTH_EQ_CONS_EXISTS = 382 prove_thm 383 ("LENGTH_EQ_CONS_EXISTS", 384 ``!P. (?l. (LENGTH l = SUC n) /\ P l) 385 = 386 (?l. (LENGTH l = n) /\ ?x. P(CONS x l))``, 387 PROVE_TAC[LENGTH_CONS]); 388 389val LENGTH_EQ_NIL_EXISTS = 390 prove_thm 391 ("LENGTH_EQ_NIL_EXISTS", 392 ``!P. (?l. (LENGTH l = 0) /\ P l) = P[]``, 393 PROVE_TAC[LENGTH_NIL]); 394 395val EQ_COND = 396 store_thm 397 ("EQ_COND", 398 ``((x = (if b then y else z)) = (if b then (x = y) else (x = z))) 399 /\ 400 (((if b then y else z) = x) = (if b then (y = x) else (z = x)))``, 401 ZAP_TAC std_ss []); 402 403val COND_SIMP = 404 store_thm 405 ("COND_SIMP", 406 ``((if b then F else F) = F) /\ 407 ((if b then F else T) = ~b) /\ 408 ((if b then T else F) = b) /\ 409 ((if b then T else T) = T) /\ 410 ((if b then x else x) = x) /\ 411 ((if b then b' else ~b') = (b = b')) /\ 412 ((if b then ~b' else b') = (b = ~b'))``, 413 ZAP_TAC std_ss []); 414 415(*****************************************************************************) 416(* IsTrace R B Q [s0;s1;...;sn] is true if B s0, Q sn and R(si,s(i+1)). *) 417(* In addition [s0;...;sn] is of minimal length to get from B to Q. *) 418(*****************************************************************************) 419 420val IsTrace_def = 421 Define 422 `(IsTrace R B Q [] = F) 423 /\ 424 (IsTrace R B Q [s] = B s /\ Q s) 425 /\ 426 (IsTrace R B Q (s0 :: (s1 :: tr)) = 427 B s0 /\ R(s0,s1) /\ IsTrace R (Eq s1) Q (s1 :: tr))`; 428 429 430(*****************************************************************************) 431(* ``Stable R state'' is true if all R-successors of state *) 432(* are equal to state -- i.e. an R-step doesn't change the state *) 433(*****************************************************************************) 434 435val Stable_def = 436 Define 437 `Stable R state = !state'. R(state,state') ==> (state' = state)`; 438 439val Live_def = 440 Define 441 `Live R = !state. ?state'. R(state,state')`; 442 443val ReachIn_Stable_SUC = 444 prove_thm 445 ("ReachIn_Stable_SUC", 446 ``ReachIn R B n state /\ Stable R state /\ Live R 447 ==> 448 ReachIn R B (SUC n) state``, 449 PROVE_TAC [ReachIn_def,Stable_def,Next_def,Live_def]); 450 451val ReachIn_Stable = 452 prove_thm 453 ("ReachIn_Stable", 454 ``!m. ReachIn R B m state /\ Stable R state /\ Live R 455 ==> 456 !n. m <= n ==> ReachIn R B n state``, 457 GEN_TAC 458 THEN DISCH_TAC 459 THEN Induct 460 THEN PROVE_TAC[LESS_EQ_0,ReachIn_Stable_SUC, 461 DECIDE``(m<=SUC n) = (m<=n)\/(m=SUC n)``]); 462 463val ReachBy_Stable = 464 prove_thm 465 ("ReachBy_Stable", 466 ``Live R 467 ==> 468 (ReachBy R B n state /\ Stable R state = 469 ReachIn R B n state /\ Stable R state)``, 470 PROVE_TAC[ReachBy_def,ReachIn_Stable,LESS_EQ_REFL]); 471 472val Stable_ADD = 473 prove_thm 474 ("Stable_ADD", 475 ``(!state. ReachIn R B m state ==> Stable R state) 476 ==> 477 !n state. 478 ReachIn R B (m+n) state ==> ReachIn R B m state``, 479 DISCH_TAC 480 THEN Induct 481 THENL 482 [PROVE_TAC[ADD_CLAUSES], 483 REWRITE_TAC[ADD_CLAUSES,ReachIn_def,Next_def] 484 THEN REPEAT STRIP_TAC 485 THEN RES_TAC 486 THEN RES_TAC 487 THEN PROVE_TAC[Stable_def]]); 488 489val Reachable_Stable = 490 store_thm 491 ("Reachable_Stable", 492 ``Live R 493 /\ 494 (!state. ReachIn R B n state ==> Stable R state) 495 ==> 496 (!state. 497 Reachable R B state /\ Stable R state = ReachIn R B n state)``, 498 RW_TAC std_ss [Reachable_def] 499 THEN EQ_TAC 500 THEN REPEAT STRIP_TAC 501 THENL 502 [DISJ_CASES_TAC(SPECL[``n':num``,``n:num``]LESS_OR_EQ_ADD) 503 THENL 504 [IMP_RES_TAC(DECIDE``(m<n)==>(m<=n)``) 505 THEN PROVE_TAC[ReachIn_Stable], 506 POP_ASSUM(STRIP_ASSUME_TAC o ONCE_REWRITE_RULE[ADD_SYM]) 507 THEN ASSUM_LIST 508 (fn [th1,th2,th3,th4,th5] => ASSUME_TAC(REWRITE_RULE[th1]th3)) 509 THEN IMP_RES_TAC Stable_ADD], 510 PROVE_TAC[], 511 PROVE_TAC[]]); 512 513val TraceReachIn = 514 store_thm 515 ("TraceReachIn", 516 ``!R B tr. B(tr 0) /\ (!n. R(tr n, tr(n+1))) ==> !n. ReachIn R B n (tr n)``, 517 REPEAT GEN_TAC 518 THEN STRIP_TAC 519 THEN Induct 520 THEN PROVE_TAC[ReachIn_def,Next_def,ADD1]); 521 522val ModelCheckAlways = 523 store_thm 524 ("ModelCheckAlways", 525 ``!R B P. 526 (!s. Reachable R B s ==> P s) 527 ==> 528 !tr. B(tr 0) /\ (!t. R(tr t, tr(t+1))) ==> !t. P(tr t)``, 529 PROVE_TAC[TraceReachIn,Reachable_def]); 530 531val ModelCheckAlwaysCor1 = 532 store_thm 533 ("ModelCheckAlwaysCor1", 534 ``(!s1 s2. Reachable R B (s1,s2) ==> P s1) 535 ==> 536 !tr. B (tr 0) /\ (!t. R (tr t,tr (t + 1))) ==> !t. P(FST(tr t))``, 537 REWRITE_TAC 538 [simpLib.SIMP_RULE 539 bossLib.arith_ss 540 [pairTheory.FORALL_PROD] 541 (ISPECL 542 [``R :('a1#'a2) # ('a1#'a2) -> bool``, 543 ``B :('a1#'a2) -> bool``, 544 ``\p:'a1#'a2. P(FST p):bool``] 545 ModelCheckAlways)]); 546 547val ModelCheckAlwaysCor2 = 548 store_thm 549 ("ModelCheckAlwaysCor2", 550 ``!R B P. 551 (!s1 s2. Reachable R B (s1,s2) ==> P s1) 552 ==> 553 !tr1. (?tr2. B(tr1 0,tr2 0) /\ !t. R((tr1 t,tr2 t), (tr1(t+1),tr2(t+1)))) ==> !t. P(tr1 t)``, 554 REPEAT STRIP_TAC 555 THEN IMP_RES_TAC ModelCheckAlwaysCor1 556 THEN POP_ASSUM(ASSUME_TAC o 557 simpLib.SIMP_RULE bossLib.arith_ss [] o 558 ISPEC ``\n:num. (tr1 n:'a, tr2 n:'b)``) 559 THEN PROVE_TAC[]); 560 561 562val FnPair_def = Define `FnPair f g x = (f x, g x)`; 563 564val FnPairAbs = 565 store_thm 566 ("FnPairAbs", 567 ``(!tr:num->'a#'b. FnPair (\n. FST (tr n)) (\n. SND (tr n)) = tr) 568 /\ 569 (!(tr1:num->'a)(tr2:num->'b). (\n. (tr1 n,tr2 n)) = FnPair tr1 tr2)``, 570 CONJ_TAC 571 THEN REPEAT GEN_TAC 572 THEN CONV_TAC FUN_EQ_CONV 573 THEN simpLib.SIMP_TAC bossLib.arith_ss [FnPair_def]); 574 575val FnPairExists = 576 store_thm 577 ("FnPairExists", 578 ``!P. (?tr:num->'a#'b. P tr) = ?tr1 tr2. P(FnPair tr1 tr2)``, 579 GEN_TAC 580 THEN EQ_TAC 581 THEN REPEAT STRIP_TAC 582 THENL[EXISTS_TAC ``\n. FST((tr:num->'a#'b) n)`` 583 THEN EXISTS_TAC ``\n. SND((tr:num->'a#'b) n)``, 584 EXISTS_TAC ``\n. ((tr1:num->'a) n, (tr2:num->'b) n)``] 585 THEN ASM_REWRITE_TAC[FnPairAbs]); 586 587val FnPairForall = 588 store_thm 589 ("FnPairForall", 590 ``!P. (!tr:num->'a#'b. P tr) = !tr1 tr2. P(FnPair tr1 tr2)``, 591 GEN_TAC 592 THEN EQ_TAC 593 THEN REPEAT STRIP_TAC 594 THENL[ALL_TAC, 595 ONCE_REWRITE_TAC[GSYM(CONJUNCT1 FnPairAbs)]] 596 THEN PROVE_TAC[]); 597 598(*****************************************************************************) 599(* |- !P rep. *) 600(* TYPE_DEFINITION P rep ==> *) 601(* (?abs. (!a. abs (rep a) = a) /\ (!r. P r = rep (abs r) = r)) *) 602(*****************************************************************************) 603 604val ABS_EXISTS_THM = (* Adapted from Hol sources *) 605 let val th1 = ASSUME (``?rep:'b->'a. TYPE_DEFINITION P rep``) 606 and th2 = BETA_RULE 607 (AP_THM 608 (AP_THM TYPE_DEFINITION ``P:'a->bool``) 609 ``rep :'b -> 'a``) 610 val def = EQ_MP (MK_EXISTS(Q.GEN `rep` th2)) th1 611 val asm = ASSUME (#Body(Rsyntax.dest_exists(concl def))) 612 val (asm1,asm2) = CONJ_PAIR asm 613 val rep_eq = 614 let val th1 = DISCH (``a:'b=a'``) 615 (AP_TERM (``rep:'b->'a``) (ASSUME (``a:'b=a'``))) 616 in IMP_ANTISYM_RULE (SPECL [(``a:'b``),(``a':'b``)] asm1) th1 617 end 618 val ABS = (``\r:'a. @a:'b. r = rep a``) 619 val absd = RIGHT_BETA (AP_THM (REFL ABS) (``rep (a:'b):'a``)) 620 val lem = SYM(SELECT_RULE(EXISTS ((``?a':'b.a=a'``),(``a:'b``)) 621 (REFL (``a:'b``)))) 622 val TH1 = GEN (``a:'b``) 623 (TRANS(TRANS absd (SELECT_EQ (``a':'b``) rep_eq)) lem) 624 val t1 = SELECT_RULE(EQ_MP (SPEC (``r:'a``) asm2) 625 (ASSUME (``(P:'a->bool) r``))) 626 val absd2 = RIGHT_BETA (AP_THM (REFL ABS) (``r:'a``)) 627 val imp1 = DISCH (``(P:'a->bool) r``) (SYM (SUBS [SYM absd2] t1)) 628 val t2 = EXISTS ((``?a:'b. r:'a = rep a``), (``^ABS r``)) 629 (SYM(ASSUME (``rep(^ABS (r:'a):'b) = r``))) 630 val imp2 = DISCH (``rep(^ABS (r:'a):'b) = r``) 631 (EQ_MP (SYM (SPEC (``r:'a``) asm2)) t2) 632 val TH2 = GEN (``r:'a``) (IMP_ANTISYM_RULE imp1 imp2) 633 val CTH = CONJ TH1 TH2 634 val ath = subst [ABS |-> Term`abs:'a->'b`] (concl CTH) 635 val eth1 = EXISTS ((``?abs:'a->'b. ^ath``), ABS) CTH 636 in 637 save_thm 638 ("ABS_EXISTS_THM", 639 REWRITE_RULE[GSYM th2](Q.GEN `P` (Q.GEN `rep` (DISCH_ALL eth1)))) 640 end; 641 642val FORALL_REP = 643 store_thm 644 ("FORALL_REP", 645 ``!abs rep P Q. 646 (!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) 647 ==> 648 ((!a. Q a) = (!r. P r ==> Q(abs r)))``, 649 PROVE_TAC[]); 650 651val EXISTS_REP = 652 store_thm 653 ("EXISTS_REP", 654 ``!abs rep P Q. 655 (!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) 656 ==> 657 ((?a. Q a) = (?r. P r /\ Q(abs r)))``, 658 PROVE_TAC[]); 659 660val ABS_ONE_ONE = 661 store_thm 662 ("ABS_ONE_ONE", 663 ``!abs rep. 664 ((!a. abs(rep a) = a) /\ (!r. range r = (rep(abs r) = r))) 665 ==> 666 !r. range r /\ range r' ==> ((abs r = abs r') = (r = r'))``, 667 PROVE_TAC[]); 668 669(*****************************************************************************) 670(* Theorems relating paths and transition relations *) 671(*****************************************************************************) 672 673val Path_def = 674 Define 675 `Path(R,s)f = (f 0 = s) /\ !n. R(f n, f(n+1))`; 676 677val ReachInPath1 = 678 prove_thm 679 ("ReachInPath1", 680 ``(?f s0. B s0 /\ Path(R,s0)f /\ (s = f n)) ==> ReachIn R B n s``, 681 REWRITE_TAC[Path_def] 682 THEN REPEAT STRIP_TAC 683 THEN PROVE_TAC[TraceReachIn]); 684 685val FinPath_def = 686 Define 687 `(FinPath(R,s) f 0 = (f 0 = s)) 688 /\ 689 (FinPath(R,s) f (SUC n) = FinPath(R,s) f n /\ R(f n, f(n+1)))`; 690 691val FinFunEq = 692 store_thm 693 ("FinFunEq", 694 ``(!m. m <= n+1 ==> (f1 m = f2 m)) = (!m. m <= n ==> (f1 m = f2 m)) /\ (f1(n+1) = f2(n+1))``, 695 REWRITE_TAC[ARITH_PROVE ``(m <= n+1) = (m <= n) \/ (m = n+1)``] 696 THEN PROVE_TAC[]); 697 698val FinPathThm = 699 store_thm 700 ("FinPathThm", 701 ``!n. FinPath (R,s) f n = (f 0 = s) /\ !m. (m < n) ==> R(f m, f(m+1))``, 702 Induct 703 THEN RW_TAC arith_ss [FinPath_def,ARITH_PROVE``(m < SUC n) = (m = n) \/ (m < n)``] 704 THEN EQ_TAC 705 THEN REPEAT STRIP_TAC 706 THEN RW_TAC std_ss []); 707 708val FinPathLemma = 709 store_thm 710 ("FinPathLemma", 711 ``!f1 f2 n. 712 (!m. m <= n ==> (f1 m = f2 m)) ==> (FinPath(R,s) f1 n = FinPath(R,s) f2 n)``, 713 STRIP_TAC 714 THEN STRIP_TAC 715 THEN Induct 716 THEN RW_TAC std_ss [FinPath_def,LESS_EQ_REFL,ADD1,ARITH_PROVE``n <= n+1``] 717 THEN PROVE_TAC[FinFunEq]); 718 719local 720val th = 721 MP(SPECL 722 [``f:num->'a``,``\p. (if p <= n then f p else (s':'a))``,``n:num``] 723 FinPathLemma) 724 (prove 725 (``!m. m <= n ==> (f m = (\p. (if p <= n then f p else s')) m)``, 726 RW_TAC std_ss [])) 727in 728val ReachInFinPath1 = 729 prove_thm 730 ("ReachInFinPath1", 731 ``!R B n s. ReachIn R B n s ==> ?f s0. B s0 /\ FinPath(R,s0) f n /\ (s = f n)``, 732 STRIP_TAC 733 THEN STRIP_TAC 734 THEN Induct 735 THEN REWRITE_TAC[FinPath_def,ReachIn_def,Next_def,ADD1] 736 THEN REPEAT STRIP_TAC 737 THENL 738 [EXISTS_TAC ``\n:num. s:'a`` 739 THEN PROVE_TAC[], 740 RES_TAC 741 THEN EXISTS_TAC ``\p. if p<=n then f p else (s:'a)`` 742 THEN EXISTS_TAC ``s0:'a`` 743 THEN RW_TAC std_ss [ARITH_PROVE``~(n+1 <= n) /\ (n <= n)``] 744 THEN IMP_RES_TAC th (* PROVE_TAC[th] crashes *) 745 THEN ASM_REWRITE_TAC[]]) 746end; 747 748val ReachInFinPath2 = 749 prove_thm 750 ("ReachInFinPath2", 751 ``!R B n s. (?f s0. B s0 /\ FinPath(R,s0) f n /\ (s = f n)) ==> ReachIn R B n s``, 752 GEN_TAC 753 THEN GEN_TAC 754 THEN Induct 755 THEN REWRITE_TAC[FinPath_def,ReachIn_def,Next_def,ADD1] 756 THEN PROVE_TAC[]); 757 758val ReachInFinPath = 759 store_thm 760 ("ReachInFinPath", 761 ``!R B n s. ReachIn R B n s = ?f s0. B s0 /\ FinPath(R,s0) f n /\ (s = f n)``, 762 PROVE_TAC[ReachInFinPath1,ReachInFinPath2]); 763 764val ReachableFinPath = 765 store_thm 766 ("ReachableFinPath", 767 ``!R B s. Reachable R B s = ?f s0 n. B s0 /\ FinPath(R,s0) f n /\ (s = f n)``, 768 PROVE_TAC[ReachInFinPath,Reachable_def]); 769 770(* Another gross proof! *) 771val ReachIn_revrec = 772 store_thm 773 ("ReachIn_revrec", 774 ``(!R B state. 775 ReachIn R B 0 state = B state) 776 /\ 777 (!R B n state. 778 ReachIn R B (SUC n) state = 779 (?state1 state2. B state1 /\ R(state1,state2) /\ ReachIn R (Eq state2) n state))``, 780 SIMP_TAC std_ss [CONJUNCT1 ReachIn_rec,ReachInFinPath,FinPathThm,Eq_def] 781 THEN REPEAT STRIP_TAC 782 THEN EQ_TAC 783 THEN RW_TAC std_ss [] 784 THENL 785 [Q.EXISTS_TAC `f 0` 786 THEN Q.EXISTS_TAC `f 1` 787 THEN FIRST_ASSUM (Q.SPEC_THEN `0` (ASSUME_TAC o 788 SIMP_RULE arith_ss [])) 789 THEN ASM_REWRITE_TAC [] 790 THEN Q.EXISTS_TAC `\i. f(i+1):'b` 791 THEN RW_TAC arith_ss [GSYM ADD1] 792 THEN `m + 1 < SUC n` by DECIDE_TAC 793 THEN RW_TAC bool_ss [DECIDE``m + 2 = m + 1 + 1``, ADD1], 794 Q.EXISTS_TAC `\i. if (i=0) then state1 else f(i-1)` 795 THEN RW_TAC std_ss [DECIDE ``(SUC n - 1 = n) /\ (n+1-1 = n)``] 796 THEN FIRST_X_ASSUM (Q.SPEC_THEN `m - 1` MP_TAC) 797 THEN RW_TAC arith_ss []]); 798 799val Total_def = Define `Total R = !s.?s'. R(s,s')`; 800 801val ChoosePath_def = 802 Define 803 `(ChoosePath R s 0 = s) 804 /\ 805 (ChoosePath R s (SUC n) = @s'. R(ChoosePath R s n, s'))`; 806 807val TotalPathExists = 808 store_thm 809 ("TotalPathExists", 810 ``Total R ==> !s. Path (R,s) (ChoosePath R s)``, 811 REWRITE_TAC[Path_def,ChoosePath_def,GSYM ADD1] 812 THEN REPEAT STRIP_TAC 813 THEN CONV_TAC SELECT_CONV 814 THEN IMP_RES_TAC Total_def 815 THEN POP_ASSUM(ACCEPT_TAC o SPEC ``ChoosePath R s n``)); 816 817(*****************************************************************************) 818(* val FinPathChoosePath = *) 819(* |- FinPath (R,s) f n = *) 820(* FinPath (R,s) (\m. (if m <= n then f m else ChoosePath R (f n) m)) n *) 821(*****************************************************************************) 822 823val FinPathChoosePath = 824 REWRITE_RULE 825 [Q.prove(`!m. m <= n ==> 826 (f m = (if m <= n then f m else ChoosePath R (f n) m))`, 827 RW_TAC std_ss [])] 828 (BETA_RULE(Q.SPECL[`f:num->'a`, 829 `\m. if m <= n then (f:num->'a) m else ChoosePath R (f n) m`, 830 `n:num`] FinPathLemma)); 831 832val FinPathPathExists = 833 Q.store_thm 834 ("FinPathPathExists", 835 `!R B f s n. 836 Total R /\ FinPath(R,s) f n 837 ==> 838 ?g. (!m. m <= n ==> (f m = g m)) /\ Path(R,s)g`, 839 REPEAT STRIP_TAC 840 THEN `Path (R, f n) (ChoosePath R (f n))` by PROVE_TAC [TotalPathExists] 841 THEN Q.EXISTS_TAC `\m. if m <= n then f m else ChoosePath R (f n) (m-n)` 842 THEN RW_TAC std_ss [Path_def,ZERO_LESS_EQ] 843 THENL 844 [PROVE_TAC [FinPathThm], 845 IMP_RES_TAC FinPathChoosePath 846 THEN BasicProvers.NORM_TAC std_ss [] 847 THENL 848 [`m < n` by DECIDE_TAC THEN PROVE_TAC [FinPathThm], 849 `m = n` by DECIDE_TAC THEN RW_TAC arith_ss [] 850 THEN PROVE_TAC [Path_def,ADD_CLAUSES], 851 PROVE_TAC [DECIDE (Term`x+1 <=y /\ ~(x <= y) ==> F`)], 852 `n < m` by DECIDE_TAC 853 THEN `m + 1 - n = (m - n) + 1` by DECIDE_TAC 854 THEN PROVE_TAC [Path_def, ADD_CLAUSES]]]); 855 856val ReachInPath = 857 store_thm 858 ("ReachInPath", 859 ``!R B n s. Total R 860 ==> 861 (ReachIn R B n s = ?f s0. B s0 /\ Path(R,s0)f /\ (s = f n))``, 862 REWRITE_TAC[ReachInFinPath] 863 THEN REPEAT STRIP_TAC 864 THEN EQ_TAC 865 THEN REPEAT STRIP_TAC 866 THENL 867 [IMP_RES_TAC FinPathPathExists 868 THEN EXISTS_TAC ``g':num->'a`` 869 THEN EXISTS_TAC ``s0:'a`` 870 THEN PROVE_TAC[LESS_EQ_REFL], 871 EXISTS_TAC ``f:num->'a`` 872 THEN EXISTS_TAC ``s0:'a`` 873 THEN PROVE_TAC[FinPathThm,Path_def]]); 874 875val ReachablePath = 876 store_thm 877 ("ReachablePath", 878 ``!R B s. Total R 879 ==> 880 (Reachable R B s = ?f s0. B s0 /\ Path(R,s0)f /\ ?n. (s = f n))``, 881 PROVE_TAC[ReachInPath,Reachable_def]); 882 883val Totalise_def = 884 Define 885 `Totalise R (s,s') = R(s,s') \/ (~(?s''. R(s,s'')) /\ (s = s'))`; 886 887val TotalTotalise = 888 store_thm 889 ("TotalTotalise", 890 ``Total(Totalise R)``, 891 PROVE_TAC[Total_def,Totalise_def]); 892 893val TotalImpTotaliseLemma = 894 store_thm 895 ("TotalImpTotaliseLemma", 896 ``Total R ==> !s s'. R (s,s') = Totalise R (s,s')``, 897 PROVE_TAC[Total_def,Totalise_def]); 898 899(*****************************************************************************) 900(* val TotalImpTotalise = |- Total R ==> (Totalise R = R) : Thm.thm *) 901(*****************************************************************************) 902 903val TotalImpTotalise = 904 store_thm 905 ("TotalImpTotalise", 906 ``Total R ==> (Totalise R = R)``, 907 REPEAT STRIP_TAC 908 THEN CONV_TAC FUN_EQ_CONV 909 THEN REPEAT STRIP_TAC 910 THEN Cases_on `p` 911 THEN IMP_RES_TAC TotalImpTotaliseLemma 912 THEN RW_TAC std_ss []); 913 914val TotaliseReachBy = 915 store_thm 916 ("TotaliseReachBy", 917 ``!n s. ReachBy (Totalise R) B n s = ReachBy R B n s``, 918 Induct 919 THEN RW_TAC std_ss [ReachBy_rec,Totalise_def,Next_def] 920 THEN PROVE_TAC[]); 921 922val ReachableTotalise = 923 store_thm 924 ("ReachableTotalise", 925 ``Reachable (Totalise R) = Reachable R``, 926 CONV_TAC (REDEPTH_CONV FUN_EQ_CONV) 927 THEN RW_TAC std_ss [Reachable_ReachBy,TotaliseReachBy] 928 THEN PROVE_TAC[]); 929 930(*****************************************************************************) 931(* val ReachablePathThm = *) 932(* |- !R B s. *) 933(* Reachable R B s = *) 934(* ?f s0. B s0 /\ Path (Totalise R,s0) f /\ ?n. s = f n *) 935(*****************************************************************************) 936 937val ReachablePathThm = 938 save_thm 939 ("ReachablePathThm", 940 GEN 941 ``R :'a # 'a -> bool`` 942 (REWRITE_RULE[ReachableTotalise,TotalTotalise] 943 (SPEC ``Totalise R`` ReachablePath))); 944 945val Moore_def = 946 Define 947 `Moore nextfn ((inputs:num->'a),(states:num->'b)) = 948 !t. states(t+1) = nextfn(inputs t,states t)`; 949 950val MooreTrans_def = 951 Define 952 `MooreTrans nextfn (((input:'a),(state:'b)),((input':'a),(state':'b))) = 953 (state' = nextfn(input,state))`; 954 955(*****************************************************************************) 956(* val MooreTransEq = *) 957(* |- MooreTrans nextfn = *) 958(* (\((input,state),input',state'). state' = nextfn (input,state)) *) 959(*****************************************************************************) 960 961val MooreTransEq = 962 store_thm 963 ("MooreTransEq", 964 ``MooreTrans nextfn = 965 \((input,state),input',state'). state' = nextfn (input,state)``, 966 CONV_TAC FUN_EQ_CONV 967 THEN REPEAT GEN_TAC 968 THEN Cases_on `p` 969 THEN Cases_on `q` 970 THEN Cases_on `r` 971 THEN CONV_TAC(DEPTH_CONV PAIRED_BETA_CONV) 972 THEN RW_TAC std_ss [MooreTrans_def]); 973 974val MoorePath = 975 store_thm 976 ("MoorePath", 977 ``Moore nextfn (inputs,states) = 978 Path 979 (MooreTrans nextfn, (inputs 0,states 0)) 980 (\t. (inputs t, states t))``, 981 RW_TAC std_ss [Path_def,MooreTrans_def,Moore_def]); 982 983val TotalMooreTrans = 984 store_thm 985 ("TotalMooreTrans", 986 ``Total(MooreTrans nextfn)``, 987 RW_TAC std_ss [Total_def] 988 THEN Cases_on `s` 989 THEN Q.EXISTS_TAC `(q',nextfn(q,r))` 990 THEN RW_TAC std_ss [MooreTrans_def]); 991 992val ReachableMooreTrans = 993 save_thm 994 ("ReachableMooreTrans", 995 SPECL 996 [``\(input:'a,state:'b). (input = inputs 0) /\ (state = states 0)``, 997 ``(input:'a, state:'b)``] 998 (MATCH_MP ReachablePath TotalMooreTrans)); 999 1000(*****************************************************************************) 1001(* val ReachableMooreTrans = *) 1002(* |- !B s. *) 1003(* Reachable (MooreTrans nextfn) B s = *) 1004(* ?f s0. B s0 /\ Path (MooreTrans nextfn,s0) f /\ ?n. s = f n *) 1005(*****************************************************************************) 1006 1007val ReachableMooreTrans = 1008 save_thm 1009 ("ReachableMooreTrans", 1010 MATCH_MP ReachablePath TotalMooreTrans); 1011 1012(* Problem with Q.SPECL? Too many type annotations needed. *) 1013 1014val MooreReachable1 = 1015 Q.store_thm 1016 ("MooreReachable1", 1017 `(!inputs states. 1018 B(inputs 0, states 0) /\ Moore nextfn (inputs,states) 1019 ==> !t. P(inputs t, states t)) 1020 ==> 1021 (!s. Reachable (MooreTrans nextfn) B s ==> P s)`, 1022 RW_TAC std_ss [ReachableMooreTrans,MoorePath] 1023 THEN Q.PAT_X_ASSUM `$! M` 1024 (MP_TAC o REWRITE_RULE [PAIR] o BETA_RULE o Q.SPECL 1025 [`\t. if t=0 then FST (s0:'a#'b) else FST(f t:'a#'b)`, 1026 `\t. if t=0 then SND (s0:'a#'b) else SND(f t:'a#'b)`]) 1027 THEN RW_TAC std_ss [COND_RAND,COND_RATOR] 1028 THEN `f:num->'a#'b = \t. if t=0 then s0 else f t` 1029 by (RW_TAC std_ss [FUN_EQ_THM] THEN PROVE_TAC [Path_def]) 1030 THEN Q.PAT_X_ASSUM `Path x y` MP_TAC THEN ONCE_ASM_REWRITE_TAC[] 1031 THEN BETA_TAC THEN PROVE_TAC []); 1032 1033val MooreReachable2 = 1034 store_thm 1035 ("MooreReachable2", 1036 ``(!s. Reachable (MooreTrans nextfn) B s ==> P s) 1037 ==> 1038 (!inputs states. 1039 B(inputs 0, states 0) /\ Moore nextfn (inputs,states) 1040 ==> !t. P(inputs t, states t))``, 1041 RW_TAC std_ss [ReachableMooreTrans,MoorePath] 1042 THEN Q.PAT_X_ASSUM `$! M` 1043 (MP_TAC o BETA_RULE 1044 o Q.SPECL [`\t. (inputs t,states t)`, `(inputs 0,states 0)`] 1045 o Ho_Rewrite.REWRITE_RULE [GSYM LEFT_FORALL_IMP_THM] 1046 o Q.SPEC `(inputs (t:num), states t)`) 1047 THEN RW_TAC std_ss [] 1048 THEN PROVE_TAC []); 1049 1050val MooreReachable = 1051 store_thm 1052 ("MooreReachable", 1053 ``!B nextfn P. 1054 (!inputs states. 1055 B(inputs 0, states 0) /\ Moore nextfn (inputs,states) 1056 ==> !t. P(inputs t, states t)) 1057 = 1058 (!s. Reachable (MooreTrans nextfn) B s ==> P s)``, 1059 REPEAT GEN_TAC 1060 THEN EQ_TAC 1061 THEN REWRITE_TAC[MooreReachable1,MooreReachable2]); 1062 1063 1064(*****************************************************************************) 1065(* val MooreReachableExists = *) 1066(* |- (?inputs states. *) 1067(* (B (inputs 0,states 0) /\ Moore nextfn (inputs,states)) /\ *) 1068(* ?t. P (inputs t,states t)) = *) 1069(* ?s. Reachable (MooreTrans nextfn) B s /\ P s *) 1070(*****************************************************************************) 1071 1072val MooreReachableExists = 1073 save_thm 1074 ("MooreReachableExists", 1075 (REWRITE_RULE[] o 1076 CONV_RULE(REDEPTH_CONV NOT_FORALL_CONV) o 1077 REWRITE_RULE[TAUT_PROVE ``~(a ==> b) = (a /\ ~b)``] o 1078 CONV_RULE(REDEPTH_CONV NOT_FORALL_CONV) o 1079 ONCE_REWRITE_RULE[TAUT_PROVE ``(a=b) = (~a=~b)``] o 1080 BETA_RULE o 1081 SPECL[``B :'a # 'b -> bool``, 1082 ``nextfn :'a # 'b -> 'b``, 1083 ``\p. ~(P :'a # 'b -> bool)p``]) 1084 MooreReachable); 1085 1086val MooreReachableCor1 = 1087 store_thm 1088 ("MooreReachableCor1", 1089 ``!B nextfn. 1090 (!inputs states. 1091 B(inputs 0, states 0) /\ 1092 (!t. states (t + 1) = nextfn (inputs t,states t)) 1093 ==> !t. P(inputs t, states t)) 1094 = 1095 (!s. Reachable (\((i,s),(i',s')). s' = nextfn(i,s)) B s ==> P s)``, 1096 RW_TAC std_ss [GSYM MooreReachable,GSYM Moore_def,GSYM MooreTransEq]); 1097 1098val _ = export_theory(); 1099