1(*****************************************************************************) 2(* Properties of models. *) 3(*****************************************************************************) 4 5(*****************************************************************************) 6(* START BOILERPLATE *) 7(*****************************************************************************) 8 9(****************************************************************************** 10* Load theories 11* (commented out for compilation) 12******************************************************************************) 13(* 14quietdec := true; 15loadPath 16 := 17 "../official-semantics" :: "../../path" :: !loadPath; 18map load 19 ["pred_setLib","res_quanTools", "rich_listTheory", "pairLib","intLib", 20 "FinitePSLPathTheory", "PSLPathTheory", "UnclockedSemanticsTheory", 21 "SyntacticSugarTheory", "ClockedSemanticsTheory", "RewritesTheory", 22 "RewritesPropertiesTheory","ProjectionTheory", 23 "rich_listTheory", "res_quanLib", "res_quanTheory", "metisLib"]; 24open SyntaxTheory SyntacticSugarTheory 25 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 26 RewritesPropertiesTheory ProjectionTheory pred_setLib res_quanTools 27 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 28 ClockedSemanticsTheory pairLib pred_setTheory ModelTheory metisLib 29 FinitePSLPathTheory PSLPathTheory pairTheory; (* Open after list theory for CONS_def *) 30val _ = intLib.deprecate_int(); 31quietdec := false; 32*) 33 34(****************************************************************************** 35* Boilerplate needed for compilation 36******************************************************************************) 37open HolKernel Parse boolLib bossLib; 38 39(****************************************************************************** 40* Open theories 41******************************************************************************) 42open SyntaxTheory SyntacticSugarTheory 43 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 44 pred_setLib pred_setTheory arithmeticTheory listTheory rich_listTheory 45 res_quanLib pairLib res_quanTheory ModelTheory ClockedSemanticsTheory 46 res_quanTools RewritesPropertiesTheory ProjectionTheory ModelTheory 47 metisLib FinitePSLPathTheory pairTheory 48 PSLPathTheory; (* Open after list theory for CONS_def *) 49 50(****************************************************************************** 51* Set default parsing to natural numbers rather than integers 52******************************************************************************) 53val _ = intLib.deprecate_int(); 54 55(*****************************************************************************) 56(* END BOILERPLATE *) 57(*****************************************************************************) 58 59(****************************************************************************** 60* Start a new theory called Lemmas 61******************************************************************************) 62val _ = new_theory "ModelLemmas"; 63val _ = ParseExtras.temp_loose_equality() 64 65val Know = Q_TAC KNOW_TAC; 66val Suff = Q_TAC SUFF_TAC; 67 68(*****************************************************************************) 69(* A simpset fragment to rewrite away quantifiers restricted with :: LESS *) 70(*****************************************************************************) 71val resq_SS = 72 simpLib.merge_ss 73 [res_quanTools.resq_SS, 74 rewrites 75 [LESS_def,LENGTH_def,IN_LESS,IN_LESSX]]; 76 77val PATH_CASES = 78 store_thm 79 ("PATH_CASES", 80 ``(PATH M s (FINITE l) = 81 (LENGTH l > 0) /\ (s = HD l) /\ s IN M.S /\ 82 (!n :: (LESS(LENGTH l - 1)). 83 EL n l IN M.S /\ EL (SUC n) l IN M.S /\ (EL n l, EL (SUC n) l) IN M.R) /\ 84 !s. s IN M.S ==> ~((EL (LENGTH l - 1) l, s) IN M.R)) 85 /\ 86 (PATH M s (INFINITE f) = 87 (s = f 0) /\ !n. f n IN M.S /\ (f n, f(SUC n)) IN M.R)``, 88 RW_TAC (list_ss++resq_SS) [PATH_def,LS,GT,ELEM_INFINITE,ELEM_FINITE,SUB] 89 THEN EQ_TAC 90 THEN RW_TAC list_ss []); 91 92(*****************************************************************************) 93(* A useful special case (possibly the only one we'll need) is to identify *) 94(* propositions with predicates on states, then we just need to specify the *) 95(* set of initial states B:'state->bool and *) 96(* transition relation R:'state#'state->bool, then: *) 97(* SIMPLE_MODEL B R : :('a, 'a -> bool) model *) 98(*****************************************************************************) 99val SIMPLE_MODEL_def = 100 Define 101 `SIMPLE_MODEL (B:'state -> bool) (R:'state#'state->bool) = 102 <| S := {s | T}; 103 S0 := B; 104 R := R; 105 P := {p | T}; 106 L := (\(s:'state). {p:'state -> bool | s IN p}) |>`; 107 108val MODEL_SIMPLE_MODEL = 109 store_thm 110 ("MODEL_SIMPLE_MODEL", 111 ``MODEL(SIMPLE_MODEL B R)``, 112 RW_TAC list_ss [MODEL_def,SIMPLE_MODEL_def] 113 THEN RW_TAC (srw_ss()) [SUBSET_UNIV]); 114 115(*****************************************************************************) 116(* Product of two models *) 117(* *) 118(* (S1,S01,R1,P1,L1) || (S2,S02,R2,P2,L2) *) 119(* = *) 120(* (S1 x S2, -- Cartesian product *) 121(* S01 x S02, -- Cartesian product *) 122(* {((s1,s2),(s1,s2)) | R1(s1,s1') and R2(s2,s2')}, *) 123(* P1 U P2, -- disjoint union *) 124(* lambda (s1,s2) *) 125(* {p in (P1 U P2) | if (p in P1) then (p in L1 s1) else (p in L2 s2)} *) 126(* ) *) 127(*****************************************************************************) 128val MODEL_PROD_def = 129 Define 130 `MODEL_PROD (M1:('state1, 'prop1) model) (M2:('state2, 'prop2) model) = 131 <| S := {(s1,s2) | s1 IN M1.S /\ s2 IN M2.S}; 132 S0 := {(s1,s2) | s1 IN M1.S0 /\ s2 IN M2.S0}; 133 R := {((s1,s2),(s1',s2')) | (s1,s1') IN M1.R /\ (s2,s2') IN M2.R}; 134 P := {p | if ISL p then OUTL p IN M1.P else OUTR p IN M2.P}; 135 L := \(s1,s2). 136 {p | if ISL p then OUTL p IN M1.L s1 else OUTR p IN M2.L s2} |>`; 137 138val _ = set_fixity "||" (Infixl 650); 139val _ = overload_on ("||", ``MODEL_PROD``); 140 141val MODEL_MODEL_PROD = 142 store_thm 143 ("MODEL_MODEL_PROD", 144 ``!M1 M2. MODEL M1 /\ MODEL M2 ==> MODEL(M1 || M2)``, 145 RW_TAC list_ss [MODEL_def,MODEL_PROD_def] 146 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] 147 THEN RW_TAC list_ss [] 148 THEN RES_TAC 149 THEN FULL_SIMP_TAC list_ss [] 150 THEN ASSUM_LIST(fn thl => ASSUME_TAC(GEN_BETA_RULE(el 4 thl))) 151 THEN FULL_SIMP_TAC (srw_ss()) [] 152 THEN PROVE_TAC[]); 153 154(*****************************************************************************) 155(* ``L_SEM l p`` means proposition p is true with respect to letter l *) 156(*****************************************************************************) 157val L_SEM_def = 158 Define 159 `(L_SEM TOP (p:'prop) = T) 160 /\ 161 (L_SEM BOTTOM p = F) 162 /\ 163 (L_SEM(STATE s) p = p IN s)`; 164 165(*****************************************************************************) 166(* LETTER_IN p v iff p occurs in an element of finite or infinite path v *) 167(*****************************************************************************) 168val LETTER_IN_def = 169 Define 170 `LETTER_IN p v = 171 ?i. i < LENGTH v /\ ?s. (ELEM v i = STATE s) /\ p IN s` ; 172 173(*****************************************************************************) 174(* FINITE_LETTER_IN p l iff p occurs in an element of l *) 175(*****************************************************************************) 176val FINITE_LETTER_IN_def = 177 Define 178 `FINITE_LETTER_IN p l = 179 ?i. i < LENGTH l /\ ?s. (EL i l = STATE s) /\ p IN s` ; 180 181(*****************************************************************************) 182(* INFINITE_LETTER_IN p f iff p occurs in an element of f *) 183(*****************************************************************************) 184val INFINITE_LETTER_IN_def = 185 Define 186 `INFINITE_LETTER_IN p f = 187 ?i s. (f i = STATE s) /\ p IN s` ; 188 189val LETTER_IN_CASES = 190 store_thm 191 ("LETTER_IN_CASES", 192 ``(LETTER_IN p (FINITE l) = FINITE_LETTER_IN p l) 193 /\ 194 (LETTER_IN p (INFINITE f) = INFINITE_LETTER_IN p f)``, 195 RW_TAC list_ss 196 [LETTER_IN_def,FINITE_LETTER_IN_def,INFINITE_LETTER_IN_def, 197 LENGTH_def,LS,ELEM_FINITE,ELEM_INFINITE]); 198 199(*****************************************************************************) 200(* Conversion of a path to a model (Kripke structure) *) 201(*****************************************************************************) 202val PATH_TO_MODEL_def = 203 Define 204 `(PATH_TO_MODEL v = 205 <| S := {n | n < LENGTH v}; 206 S0 := {0}; 207 R := {(n,n') | n < LENGTH v /\ n' < LENGTH v /\ (n' = n+1)}; 208 P := {p:'prop | LETTER_IN p v}; 209 L := \n. {p | n < LENGTH v /\ LETTER_IN p v /\ L_SEM (ELEM v n) p} |>)`; 210 211val PATH_TO_MODEL_CASES = 212 store_thm 213 ("PATH_TO_MODEL_CASES", 214 ``(PATH_TO_MODEL(FINITE l) = 215 <| S := {n | n < LENGTH l}; 216 S0 := {0}; 217 R := {(n,n') | n < LENGTH l /\ n' < LENGTH l /\ (n' = n+1)}; 218 P := {p:'prop | FINITE_LETTER_IN p l}; 219 L := \n. {p | n < LENGTH l /\ FINITE_LETTER_IN p l /\ L_SEM (EL n l) p} |>) 220 /\ 221 (PATH_TO_MODEL(INFINITE f) = 222 <| S := {n | T}; 223 S0 := {0}; 224 R := {(n,n') | n' = n+1}; 225 P := {p:'prop | INFINITE_LETTER_IN p f}; 226 L := \n. {p | INFINITE_LETTER_IN p f /\ L_SEM (f n) p} |>)``, 227 RW_TAC list_ss 228 [PATH_TO_MODEL_def,LENGTH_def,LS,ELEM_FINITE,ELEM_INFINITE, 229 LETTER_IN_CASES]); 230 231val MODEL_PATH_TO_MODEL = 232 store_thm 233 ("MODEL_PATH_TO_MODEL", 234 ``!p. 0 < LENGTH p ==> MODEL(PATH_TO_MODEL p)``, 235 GEN_TAC 236 THEN Cases_on `p` 237 THEN RW_TAC list_ss [SUBSET_DEF,MODEL_def,PATH_TO_MODEL_CASES] 238 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_UNIV,LENGTH_def,LS]); 239 240(*****************************************************************************) 241(* Definition of an automaton: ``: ('label,'state)automaton`` *) 242(* (e.g. Clarke/Grumberg/Peled "Model Checking" Chapter 9) *) 243(*****************************************************************************) 244val automaton_def = 245 Hol_datatype 246 `automaton = 247 <| Sigma: 'label -> bool; 248 Q: 'state -> bool; 249 Delta: 'state # 'label # 'state -> bool; 250 Q0: 'state -> bool; 251 F: 'state -> bool |>`; 252 253(*****************************************************************************) 254(* AUTOMATON_PATH A w <=> w is a (finite or infinite) trace of A *) 255(*****************************************************************************) 256(* 257val AUTOMATON_PATH_def = 258 Define 259 `AUTOMATON_PATH A w = 260 LENGTH w > 0 /\ ELEM w 0 IN A.Q0 /\ 261 (!n::LESS (LENGTH w - 1). 262 ELEM w n IN A.Q /\ ELEM w (SUC n) IN A.Q /\ 263 ?lab. lab IN A.Sigma /\ (ELEM w n, lab, ELEM w (SUC n)) IN A.Delta) /\ 264 !l. (w = FINITE l) 265 ==> 266 !s lab. s IN A.Q /\ lab IN A.Sigma 267 ==> ~((ELEM w (LENGTH l - 1), lab, s) IN A.Delta)`; 268 269*) 270 271(*****************************************************************************) 272(* The open model over a set P of propositions P : 'prop -> bool *) 273(*****************************************************************************) 274(* 275val OLD_OPEN_MODEL_def = 276 Define 277 `OLD_OPEN_MODEL(P:'prop -> bool) = 278 <| S := {s | s SUBSET P}; 279 S0 := {s | s SUBSET P}; 280 R := {(s,t) | s SUBSET P /\ t SUBSET P}; 281 P := P; 282 L := \s. {p | p IN s} |>`; 283*) 284 285(****************************************************************************** 286* Formalise Eisner/Fisman {s | s SUBSET P} UNION {sink} 287******************************************************************************) 288val SINK_def = 289 Define `SINK P = {@p. ~(p IN P)}`; 290 291val OPEN_MODEL_def = 292 Define 293 `OPEN_MODEL(P:'prop -> bool) = 294 <| S := {s | s SUBSET P} UNION {SINK P}; 295 S0 := {s | s SUBSET P}; 296 R := {(s,t) | s SUBSET P /\ (t SUBSET P \/ (t = SINK P))}; 297 P := P; 298 L := \s. if s = SINK P then {} else {p | p IN s} |>`; 299 300val MODEL_OPEN_MODEL = 301 store_thm 302 ("MODEL_OPEN_MODEL", 303 ``MODEL(OPEN_MODEL P)``, 304 RW_TAC list_ss [MODEL_def,OPEN_MODEL_def] 305 THEN FULL_SIMP_TAC (srw_ss()) [] 306 THEN PROVE_TAC[EMPTY_SUBSET]); 307 308val AUTOMATON_def = 309 Define 310 `AUTOMATON A = 311 A.Q0 SUBSET A.Q /\ 312 (!s a s'. (s,a,s') IN A.Delta ==> s IN A.Q /\ a IN A.Sigma /\ s' IN A.Q) /\ 313 A.F SUBSET A.Q`; 314 315(*****************************************************************************) 316(* Use of totality suggested by Cindy Eisner *) 317(*****************************************************************************) 318val TOTAL_AUTOMATON_def = 319 Define 320 `TOTAL_AUTOMATON A = 321 AUTOMATON A /\ !s a. ?s'. s' IN A.Q /\ (s,a,s') IN A.Delta`; 322 323(*****************************************************************************) 324(* Convert a model to an automaton *) 325(* (Clarke/Grumberg/Peled "Model Checking" 9.2) *) 326(*****************************************************************************) 327val MODEL_TO_AUTOMATON_def = 328 Define 329 `MODEL_TO_AUTOMATON (M:('prop,'state)model) = 330 <| Sigma := {a | a SUBSET M.P}; 331 Q := {SOME s : ('state)option | s IN M.S} UNION {NONE}; 332 Delta := {(SOME s, a, SOME s') | (s,s') IN M.R /\ (a = M.L s')} 333 UNION 334 {(NONE, a, SOME s) | s IN M.S0 /\ (a = M.L s)}; 335 Q0 := {NONE : ('state)option}; 336 F := {SOME s : ('state)option | s IN M.S} UNION {NONE} |>`; 337 338val AUTOMATON_MODEL_TO_AUTOMATON = 339 store_thm 340 ("AUTOMATON_MODEL_TO_AUTOMATON", 341 ``!M. MODEL M ==> AUTOMATON(MODEL_TO_AUTOMATON M)``, 342 RW_TAC list_ss [MODEL_def,AUTOMATON_def,MODEL_TO_AUTOMATON_def] 343 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] 344 THEN RW_TAC list_ss [] 345 THEN PROVE_TAC[]); 346 347(*****************************************************************************) 348(* Product of a model with an automaton *) 349(* *) 350(* S is the cross product of the states of M with the states of A. That *) 351(* is, the set of states (s,t) such that s is a state in M and t a state *) 352(* in A. So is the set of states (s,t) such that s is in the initial *) 353(* states of M and t is in the initial states of A. R((s,t),(s',t')) iff *) 354(* (s,s') is in the relation of M, and (t,a,t') is in the relation of A, *) 355(* where a is the labeling of s. P are the propositions of M and *) 356(* L(s,t) = L(s). *) 357(*****************************************************************************) 358val MODEL_AUTOMATON_PROD_def = 359 Define 360 `MODEL_AUTOMATON_PROD 361 (M:('prop,'state2) model) (A:('prop -> bool, 'state1) automaton) = 362 <| S := {(s,t) | s IN M.S /\ t IN A.Q}; 363 S0 := {(s,t) | s IN M.S0 /\ t IN A.Q0}; 364 R := {((s,t),(s',t')) | 365 ?a. (a = M.L s) /\ (s,s') IN M.R /\ (t,a,t') IN A.Delta}; 366 P := M.P; 367 L := \(s,t). M.L s |>`; 368 369val _ = overload_on ("||", ``MODEL_AUTOMATON_PROD``); 370 371val MODEL_MODEL_AUTOMATON_PROD = 372 store_thm 373 ("MODEL_MODEL_AUTOMATON_PROD", 374 ``!M A. MODEL M /\ AUTOMATON A ==> MODEL(M || A)``, 375 RW_TAC list_ss [MODEL_def,AUTOMATON_def,MODEL_AUTOMATON_PROD_def] 376 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] 377 THEN RW_TAC list_ss [] 378 THEN RES_TAC 379 THEN FULL_SIMP_TAC list_ss []); 380 381(*****************************************************************************) 382(* Product of automata *) 383(*****************************************************************************) 384val AUTOMATON_PROD_def = 385 Define 386 `AUTOMATON_PROD 387 (A1:('label1,'state1)automaton) (A2:('label2,'state2)automaton) = 388 <| Sigma := {(a1,a2) | a1 IN A1.Sigma /\ a2 IN A2.Sigma }; 389 Q := {(q1,q2) | q1 IN A1.Q /\ q2 IN A2.Q}; 390 Delta := {((q1,q2),(a1,a2),(q1',q2')) | 391 (q1,a1,q1') IN A1.Delta /\ (q2,a2,q2') IN A2.Delta}; 392 Q0 := {(q1,q2) | q1 IN A1.Q0 /\ q2 IN A2.Q0}; 393 F := {(q1,q2) | q1 IN A1.F /\ q2 IN A2.F} |>`; 394 395val _ = overload_on ("||", ``AUTOMATON_PROD``); 396 397val AUTOMATON_AUTOMATON_PROD = 398 store_thm 399 ("AUTOMATON_AUTOMATON_PROD", 400 ``!A1 A2. AUTOMATON A1 /\ AUTOMATON A2 ==> AUTOMATON(A1 || A2)``, 401 RW_TAC list_ss [AUTOMATON_def,AUTOMATON_PROD_def] 402 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] 403 THEN RW_TAC list_ss [] 404 THEN PROVE_TAC[]); 405 406val IN_LESS_LENGTH = 407 store_thm 408 ("IN_LESS_LENGTH", 409 ``!n v. n IN LESS(LENGTH v) = n < LENGTH v``, 410 Cases_on `v` 411 THEN RW_TAC list_ss [IN_LESS,IN_LESSX,LENGTH_def,LS]); 412 413val IN_LESS_LENGTH_SUB1 = 414 store_thm 415 ("IN_LESS_LENGTH_SUB1", 416 ``!n v. n IN LESS(LENGTH v - 1) = n < LENGTH v - 1``, 417 Cases_on `v` 418 THEN RW_TAC list_ss [IN_LESS,IN_LESSX,LENGTH_def,LS,SUB]); 419 420val IN_PATH = 421 store_thm 422 ("IN_PATH", 423 ``w IN PATH M s = PATH M s w``, 424 RW_TAC list_ss [IN_DEF]); 425 426val IN_COMPUTATION = 427 store_thm 428 ("IN_COMPUTATION", 429 ``w IN COMPUTATION M = ?s. s IN M.S0 /\ PATH M s w``, 430 RW_TAC list_ss [IN_DEF,COMPUTATION_def]); 431 432val SUBSET_SINK = 433 store_thm 434 ("SUBSET_SINK", 435 ``!A P. (?p. ~(p IN P)) /\ A SUBSET P ==> ~(A = SINK P)``, 436 RW_TAC list_ss [SUBSET_DEF,SINK_def] 437 THEN Cases_on `A = {@p. ~(p IN P)}` 438 THEN FULL_SIMP_TAC list_ss [IN_SING] 439 THEN FULL_SIMP_TAC list_ss [IN_DEF] 440 THEN `~(P @p. ~P p)` by METIS_TAC[SELECT_THM]); 441 442val EQ_PAIR = 443 store_thm 444 ("EQ_PAIR", 445 ``!p x y. (p = (x,y)) = (x = FST p) /\ (y = SND p)``, 446 Cases_on `p` 447 THEN ZAP_TAC std_ss []); 448 449val LENGTH_LAST = 450 store_thm 451 ("LENGTH_LAST", 452 ``!l. LENGTH l > 0 453 ==> 454 (LAST l = EL (LENGTH l - 1) l)``, 455 RW_TAC arith_ss [EL_PRE_LENGTH]); 456 457val COMPUTATION_OPEN_MODEL = 458 store_thm 459 ("COMPUTATION_OPEN_MODEL", 460 ``(?p. ~(p IN P)) 461 ==> 462 (v IN COMPUTATION(OPEN_MODEL P) = 463 LENGTH v > 0 /\ ELEM v 0 SUBSET P 464 /\ 465 (!n::LESS(LENGTH v - 1). 466 ELEM v n SUBSET P /\ 467 (ELEM v (SUC n) SUBSET P \/ (ELEM v (SUC n) = SINK P))) 468 /\ 469 !l. (v = FINITE l) ==> ~(LAST l SUBSET P))``, 470 RW_TAC (srw_ss()++resq_SS) 471 [OPEN_MODEL_def,IN_COMPUTATION, 472 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK] 473 THEN EQ_TAC 474 THEN RW_TAC list_ss [] 475 THEN FULL_SIMP_TAC std_ss [EQ_PAIR,ELEM_FINITE,LENGTH_def,SUB,LS,GT] 476 THEN PROVE_TAC[LENGTH_LAST]); 477 478val UF_VALID_OPEN_MODEL = 479 store_thm 480 ("UF_VALID_OPEN_MODEL", 481 ``(?p. ~(p IN P)) /\ AUTOMATON A 482 ==> 483 (UF_VALID (OPEN_MODEL P) f = 484 !v. LENGTH v > 0 /\ ELEM v 0 SUBSET P 485 /\ 486 (!n::LESS(LENGTH v - 1). 487 ELEM v n SUBSET P /\ 488 (ELEM v (SUC n) SUBSET P \/ (ELEM v (SUC n) = SINK P))) 489 /\ 490 (!l. (v = FINITE l) ==> ~(LAST l SUBSET P)) 491 ==> 492 UF_SEM (MAP_PATH (\s. STATE (if s = SINK P then {} else s)) v) f)``, 493 RW_TAC (srw_ss()++resq_SS) [UF_VALID_def,COMPUTATION_OPEN_MODEL] 494 THEN EQ_TAC 495 THEN RW_TAC list_ss [] 496 THENL 497 [`UF_SEM (MAP_PATH (\s. STATE ((OPEN_MODEL P).L s)) v) f` by METIS_TAC[] 498 THEN FULL_SIMP_TAC (srw_ss()++resq_SS) [OPEN_MODEL_def], 499 `UF_SEM (MAP_PATH (\s. STATE (if s = SINK P then {} else s)) v) f` 500 by METIS_TAC[] 501 THEN RW_TAC (srw_ss()++resq_SS) [OPEN_MODEL_def]]); 502 503val LENGTH1_LAST = 504 store_thm 505 ("LENGTH1_LAST", 506 ``!l. (LENGTH l = 1) ==> (LAST l = EL 0 l)``, 507 RW_TAC list_ss [LENGTH1] 508 THEN RW_TAC list_ss [LENGTH1,LAST_CONS,EL]); 509 510val LEMMA1 = (* Surprisingly tricky proof needed *) 511 prove 512 (``(?p. ~(p IN P)) 513 ==> 514 ((A /\ B) /\ (s SUBSET P /\ C) /\ Q(s = SINK P) = 515 (A /\ B) /\ (s SUBSET P /\ C) /\ Q F)``, 516 RW_TAC list_ss [] 517 THEN EQ_TAC 518 THEN RW_TAC list_ss [] 519 THEN IMP_RES_TAC SUBSET_SINK 520 THEN RW_TAC list_ss [] 521 THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th])); 522 523val COMPUTATION_OPEN_MODEL_AUTOMATON = 524 store_thm 525 ("COMPUTATION_OPEN_MODEL_AUTOMATON", 526 ``(?p. ~(p IN P)) /\ AUTOMATON A 527 ==> 528 (v IN COMPUTATION(OPEN_MODEL P || A) = 529 LENGTH v > 0 /\ FST(ELEM v 0) SUBSET P /\ SND(ELEM v 0) IN A.Q0 530 /\ 531 (!n::LESS(LENGTH v - 1). 532 FST(ELEM v n) SUBSET P /\ 533 (FST(ELEM v (SUC n)) SUBSET P \/ (FST (ELEM v (SUC n)) = SINK P)) /\ 534 (SND(ELEM v n), FST(ELEM v n), SND(ELEM v (SUC n))) IN A.Delta) 535 /\ 536 !l. (v = FINITE l) /\ FST(LAST l) SUBSET P 537 ==> 538 !s. s IN A.Q ==> ~((SND(LAST l), FST(LAST l), s) IN A.Delta))``, 539 RW_TAC (srw_ss()++resq_SS) 540 [MODEL_AUTOMATON_PROD_def,OPEN_MODEL_def,IN_COMPUTATION, 541 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK, 542 DECIDE ``~A \/ (~B \/ ~C /\ ~D) \/ E = A ==> B ==> (C \/ D) ==> E``, 543 LEMMA1] 544 THEN FULL_SIMP_TAC (srw_ss()++resq_SS) [AUTOMATON_def] 545 THEN EQ_TAC 546 THEN RW_TAC list_ss [] 547 THEN FULL_SIMP_TAC std_ss [EQ_PAIR,ELEM_FINITE,LENGTH_def,SUB,LS,GT] 548 THEN RW_TAC list_ss [] 549 THEN ZAP_TAC std_ss [SUBSET_DEF] 550 THEN ASM_REWRITE_TAC[GSYM EL] 551 THEN Cases_on `LENGTH l = 1` 552 THEN ASSUM_LIST 553 (fn thl => 554 if is_eq(concl(el 1 thl)) 555 then FULL_SIMP_TAC list_ss [GSYM(MATCH_MP LENGTH1_LAST (el 1 thl))] 556 else ALL_TAC) 557 THEN TRY(ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `(P,s)` (el 2 thl)))) 558 THEN METIS_TAC[SUBSET_REFL,FST,SND,LENGTH_LAST,LENGTH1_LAST,EL]); 559 560val UF_VALID_OPEN_MODEL_AUTOMATON = 561 store_thm 562 ("UF_VALID_OPEN_MODEL_AUTOMATON", 563 ``(?p. ~(p IN P)) /\ AUTOMATON A 564 ==> 565 (UF_VALID (MODEL_AUTOMATON_PROD (OPEN_MODEL P) A) f = 566 !v. LENGTH v > 0 /\ FST(ELEM v 0) SUBSET P /\ SND(ELEM v 0) IN A.Q0 567 /\ 568 (!n::LESS(LENGTH v - 1). 569 FST(ELEM v n) SUBSET P /\ 570 (FST(ELEM v (SUC n)) SUBSET P \/ (FST (ELEM v (SUC n)) = SINK P)) /\ 571 (SND(ELEM v n), FST(ELEM v n), SND(ELEM v (SUC n))) IN A.Delta) 572 /\ 573 (!l. (v = FINITE l) /\ FST(LAST l) SUBSET P 574 ==> 575 !s. s IN A.Q ==> ~((SND(LAST l), FST(LAST l), s) IN A.Delta)) 576 ==> 577 UF_SEM (MAP_PATH (\s. STATE (if FST s = SINK P then {} else FST s)) v) f)``, 578 RW_TAC (srw_ss()++resq_SS) [UF_VALID_def,COMPUTATION_OPEN_MODEL_AUTOMATON] 579 THEN EQ_TAC 580 THEN RW_TAC list_ss [] 581 THENL 582 [`UF_SEM (MAP_PATH (\s. STATE ((OPEN_MODEL P || A).L s)) v) f` by METIS_TAC[] 583 THEN FULL_SIMP_TAC (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def,OPEN_MODEL_def] 584 THEN POP_ASSUM(ASSUME_TAC o GEN_BETA_RULE) 585 THEN RW_TAC std_ss [], 586 `UF_SEM (MAP_PATH (\s. STATE (if FST s = SINK P then {} else FST s)) v) f` 587 by METIS_TAC[] 588 THEN RW_TAC (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def,OPEN_MODEL_def] 589 THEN GEN_BETA_TAC 590 THEN RW_TAC std_ss []]); 591 592(*****************************************************************************) 593(* Conversion of a computation to a model (Kripke structure) *) 594(*****************************************************************************) 595val COMPUTATION_TO_MODEL_def = 596 Define 597 `COMPUTATION_TO_MODEL w = 598 <| S := {n | n < LENGTH w}; 599 S0 := {0}; 600 R := {(n,n') | n < LENGTH w /\ n' < LENGTH w /\ (n' = n+1)}; 601 P := {p:'prop | ?i. i < LENGTH w /\ p IN ELEM w i}; 602 L := \n. {p | n < LENGTH w /\ p IN (ELEM w n)} |>`; 603 604val COMPUTATION_TO_MODEL_CASES = 605 store_thm 606 ("COMPUTATION_TO_MODEL_CASES", 607 ``(COMPUTATION_TO_MODEL(FINITE l) = 608 <| S := {n | n < LENGTH l}; 609 S0 := {0}; 610 R := {(n,n') | n < LENGTH l /\ n' < LENGTH l /\ (n' = n+1)}; 611 P := {p:'prop | ?i. i < LENGTH l /\ p IN EL i l}; 612 L := \n. {p | n < LENGTH l /\ p IN (EL n l)} |>) 613 /\ 614 (COMPUTATION_TO_MODEL(INFINITE f) = 615 <| S := {n | T}; 616 S0 := {0}; 617 R := {(n,n') | n' = n+1}; 618 P := {p:'prop | ?i. p IN f i}; 619 L := \n. {p | p IN (f n)} |>)``, 620 RW_TAC list_ss 621 [COMPUTATION_TO_MODEL_def,LENGTH_def,LS,ELEM_INFINITE,ELEM_FINITE]); 622 623val MODEL_COMPUTATION_TO_MODEL = 624 store_thm 625 ("MODEL_COMPUTATION_TO_MODEL", 626 ``!p. 0 < LENGTH p ==> MODEL(COMPUTATION_TO_MODEL p)``, 627 GEN_TAC 628 THEN Cases_on `p` 629 THEN RW_TAC list_ss [SUBSET_DEF,MODEL_def,COMPUTATION_TO_MODEL_def] 630 THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_UNIV,LENGTH_def,LS] 631 THEN PROVE_TAC[]); 632 633val LS_GT_IMP = 634 store_thm 635 ("LS_GT_IMP", 636 ``!(n:num) (w:'a path). n < LENGTH w ==> LENGTH w > 0``, 637 Cases_on `w` 638 THEN RW_TAC list_ss [LENGTH_def,LS,GT]); 639 640val GT_LS_IMP = 641 store_thm 642 ("GT_LS_IMP", 643 ``!(n:num) (w:'a path). LENGTH w > n ==> 0 < LENGTH w``, 644 Cases_on `w` 645 THEN RW_TAC list_ss [LENGTH_def,LS,GT]); 646 647val LEMMA2 = 648 prove 649 (``1 <= LENGTH w 650 /\ 651 (!n. n < LENGTH v - 1 ==> 652 SUC(FST(ELEM v n)) < LENGTH w 653 /\ 654 FST(ELEM v (SUC n)) < LENGTH w 655 /\ 656 (FST(ELEM v (SUC n)) = SUC(FST(ELEM v n)))) 657 ==> 658 LENGTH v <= LENGTH w``, 659 Cases_on `v` THEN Cases_on `w` 660 THEN RW_TAC arith_ss 661 [LENGTH_def,ELEM_FINITE,ELEM_INFINITE,LE,LS,SUB,GSYM EL, 662 DECIDE ``~A \/ ~B \/ C = A /\ B ==> C``] 663 THENL 664 [ Know `!m. m < LENGTH l ==> (FST(EL m l) = FST(EL 0 l) + m)` 665 >- ( Induct >> fs [] ) >> DISCH_TAC 666 THEN RW_TAC arith_ss [] 667 THEN Cases_on `LENGTH l <= 1` 668 THEN RW_TAC arith_ss [] 669 THEN `LENGTH l - 1 < LENGTH l /\ LENGTH l - 2 < LENGTH l - 1` by DECIDE_TAC 670 THEN RES_TAC 671 THEN `SUC (LENGTH l - 2) = LENGTH l - 1` 672 by PROVE_TAC[DECIDE``m - 1 < m /\ m - 2 < m - 1 ==> (SUC(m - 2) = m - 1)``] 673 THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th]) 674 THEN `FST (EL 0 l) + (LENGTH l - 1) < LENGTH l'` by PROVE_TAC[] 675 THEN DECIDE_TAC, 676 RW_TAC std_ss [DECIDE``~A \/ B = A ==> B``] 677 THEN CCONTR_TAC 678 THEN FULL_SIMP_TAC std_ss [] 679 THEN Know `!m. FST(f m) = FST(f 0) + m` >- (Induct >> fs []) >> DISCH_TAC 680 THEN RW_TAC arith_ss [] 681 THEN POP_ASSUM(ASSUME_TAC o AP_TERM ``SUC`` o Q.SPEC `LENGTH l`) 682 THEN `SUC (FST (f (LENGTH l))) < LENGTH l` by PROVE_TAC[] 683 THEN DECIDE_TAC]); 684 685val LEMMA3 = 686 prove 687 (``1 <= LENGTH w 688 /\ 689 (FST (ELEM v 0) = 0) 690 /\ 691 (!n. n < LENGTH v - 1 ==> 692 SUC(FST(ELEM v n)) < LENGTH w 693 /\ 694 FST(ELEM v (SUC n)) < LENGTH w 695 /\ 696 (FST(ELEM v (SUC n)) = SUC(FST(ELEM v n)))) 697 ==> 698 !m. m < LENGTH v - 1 ==> (FST (ELEM v m) = m)``, 699 Cases_on `v` THEN Cases_on `w` 700 THEN RW_TAC arith_ss 701 [LENGTH_def,ELEM_FINITE,ELEM_INFINITE,LE,LS,SUB,GSYM EL, 702 DECIDE ``~A \/ ~B \/ C = A /\ B ==> C``] 703 THEN Induct_on `m` 704 THEN RW_TAC arith_ss []); 705 706val COMPUTATION_COMPUTATION_MODEL_AUTOMATON_LEMMA = 707 store_thm 708 ("COMPUTATION_COMPUTATION_MODEL_AUTOMATON_LEMMA", 709 ``AUTOMATON A 710 ==> 711 (v IN COMPUTATION(COMPUTATION_TO_MODEL w || A) = 712 LENGTH v > 0 /\ LENGTH w > 0 /\ (FST(ELEM v 0) = 0) /\ SND(ELEM v 0) IN A.Q0 713 /\ 714 (!n::LESS(LENGTH v - 1). 715 SUC(FST(ELEM v n)) < LENGTH w /\ FST(ELEM v (SUC n)) < LENGTH w /\ 716 SND(ELEM v n) IN A.Q /\ (FST(ELEM v (SUC n)) = SUC(FST(ELEM v n))) /\ 717 (SND(ELEM v n), ELEM w (FST(ELEM v n)), SND(ELEM v (SUC n))) IN A.Delta) 718 /\ 719 !l. (v = FINITE l) 720 ==> 721 !s. s IN A.Q /\ SUC(FST(LAST l)) < LENGTH w 722 ==> ~((SND(LAST l), ELEM w (FST(LAST l)), s) IN A.Delta))``, 723 RW_TAC (srw_ss()++resq_SS) 724 [MODEL_AUTOMATON_PROD_def,COMPUTATION_TO_MODEL_def,IN_COMPUTATION, 725 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK, 726 DECIDE ``(~A \/ ~B) \/ ~C \/ ~D \/ E = A ==> B ==> C ==> D ==> E``] 727 THEN FULL_SIMP_TAC (srw_ss()++resq_SS) [AUTOMATON_def] 728 THEN EQ_TAC 729 THEN RW_TAC list_ss [] 730 THEN FULL_SIMP_TAC std_ss [EQ_PAIR,ELEM_FINITE,LENGTH_def,SUB,LS,GT] 731 THEN RW_TAC list_ss [] 732 THEN ZAP_TAC std_ss [SUBSET_DEF] 733 THEN TRY(METIS_TAC[ADD1]) 734 THEN TRY(`EL (LENGTH l - 1) l = LAST l` by PROVE_TAC[LENGTH_LAST] 735 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th])) 736 THENL 737 [METIS_TAC[LS_GT_IMP], 738 `(SND (ELEM v n), 739 {p | FST (ELEM v n) < LENGTH w /\ p IN ELEM w (FST (ELEM v n))}, 740 SND (ELEM v (SUC n))) IN A.Delta` by METIS_TAC[] 741 THEN `FST (ELEM v n) < LENGTH w` by METIS_TAC[] 742 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th,GSPEC_ID]), 743 POP_ASSUM(ASSUME_TAC o Q.SPEC `(SUC(FST (LAST(l :(num # 'b) list))),s)`) 744 THEN FULL_SIMP_TAC list_ss [] 745 THEN METIS_TAC[DECIDE``(m:num) < SUC m``,LS_TRANS_X], 746 METIS_TAC[GT_LS_IMP], 747 METIS_TAC[LS_TRANS_X,DECIDE``n < SUC n``,ADD1], 748 METIS_TAC[LS_TRANS_X,DECIDE``n < SUC n``,ADD1], 749 `FST (ELEM v n) < LENGTH w` by METIS_TAC[LS_TRANS_X,DECIDE``n < SUC n``] 750 THEN RW_TAC list_ss [GSPEC_ID], 751 METIS_TAC[ADD1]]); 752 753val COMPUTATION_COMPUTATION_MODEL_AUTOMATON = 754 store_thm 755 ("COMPUTATION_COMPUTATION_MODEL_AUTOMATON", 756 ``AUTOMATON A 757 ==> 758 (v IN COMPUTATION(COMPUTATION_TO_MODEL w || A) = 759 LENGTH v > 0 /\ LENGTH w > 0 /\ (FST(ELEM v 0) = 0) 760 /\ 761 SND(ELEM v 0) IN A.Q0 /\ LENGTH v <= LENGTH w 762 /\ 763 (!n::LESS(LENGTH v - 1). 764 (FST(ELEM v (SUC n)) = SUC n) /\ SND(ELEM v n) IN A.Q /\ 765 (SND(ELEM v n), ELEM w n, SND(ELEM v (SUC n))) IN A.Delta) 766 /\ 767 !l. (v = FINITE l) /\ SUC(FST(LAST l)) < LENGTH w 768 ==> 769 !s. s IN A.Q ==> ~((SND(LAST l), ELEM w (FST(LAST l)), s) IN A.Delta))``, 770 RW_TAC (srw_ss()++resq_SS) 771 [COMPUTATION_COMPUTATION_MODEL_AUTOMATON_LEMMA, 772 IN_LESS_LENGTH_SUB1] 773 THEN EQ_TAC 774 THEN RW_TAC list_ss [] 775 THEN `1 <= LENGTH w` 776 by (Cases_on `w` 777 THEN RW_TAC list_ss [LENGTH_def,LE] 778 THEN FULL_SIMP_TAC arith_ss [LENGTH_def,GT]) 779 THENL 780 [METIS_TAC[LEMMA2], 781 METIS_TAC[LEMMA3], 782 METIS_TAC[LEMMA3], 783 Cases_on `v` THEN Cases_on `w` 784 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,SUB,GT,LE,ELEM_FINITE,ELEM_INFINITE] 785 THEN FULL_SIMP_TAC std_ss [GSYM EL] 786 THEN Cases_on `n=0` 787 THEN RW_TAC list_ss [] 788 THEN `n - 1 < LENGTH l - 1` by DECIDE_TAC 789 THEN `SUC(n-1) = n` by DECIDE_TAC 790 THEN `FST (EL n l) = n` by PROVE_TAC[] 791 THEN DECIDE_TAC, 792 Cases_on `v` THEN Cases_on `w` 793 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,SUB,GT,LE,ELEM_FINITE,ELEM_INFINITE], 794 Cases_on `n=0` 795 THEN RW_TAC list_ss [] 796 THEN Cases_on `v` 797 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,SUB,GT,LE,ELEM_FINITE,ELEM_INFINITE] 798 THEN FULL_SIMP_TAC std_ss [GSYM EL] 799 THENL 800 [`n - 1 < LENGTH l - 1` by DECIDE_TAC 801 THEN `SUC(n-1) = n` by DECIDE_TAC 802 THEN `FST (EL n l) = n` by PROVE_TAC[] 803 THEN DECIDE_TAC, 804 `SUC(n-1) = n` by DECIDE_TAC 805 THEN `FST (f n) = n` by PROVE_TAC[] 806 THEN RW_TAC list_ss []], 807 Cases_on `n=0` 808 THEN RW_TAC list_ss [] 809 THEN TRY(PROVE_TAC [ONE]) 810 THEN `n - 1 < LENGTH v - 1` 811 by (Cases_on `v` 812 THEN RW_TAC list_ss [LENGTH_def,LS,SUB] 813 THEN FULL_SIMP_TAC arith_ss [LENGTH_def,GT,LS,SUB]) 814 THEN `SUC(n-1) = n` by DECIDE_TAC 815 THEN METIS_TAC[]]); 816 817val SUC_SUB1_LS = 818 store_thm 819 ("SUC_SUB1_LS", 820 ``SUC n < (x:xnum) = n < x - 1``, 821 Cases_on `x` 822 THEN RW_TAC arith_ss [LS,SUB]); 823 824val GT_LE_TRANS = 825 store_thm 826 ("GT_LE_TRANS", 827 ``(x:xnum) > 0 /\ x <= (y:xnum) ==> y > 0``, 828 Cases_on `x` THEN Cases_on `y` 829 THEN RW_TAC arith_ss [LS,GT,LE]); 830 831val COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR1 = 832 store_thm 833 ("COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR1", 834 ``AUTOMATON A 835 ==> 836 (v IN COMPUTATION(COMPUTATION_TO_MODEL w || A) = 837 LENGTH v > 0 /\ (FST(ELEM v 0) = 0) 838 /\ 839 SND(ELEM v 0) IN A.Q0 /\ LENGTH v <= LENGTH w 840 /\ 841 (!n. n < LENGTH v ==> (FST(ELEM v n) = n)) 842 /\ 843 (!n. n < (LENGTH v - 1) ==> 844 SND(ELEM v n) IN A.Q /\ 845 (SND(ELEM v n), ELEM w n, SND(ELEM v (SUC n))) IN A.Delta) 846 /\ 847 !l. (v = FINITE l) /\ SUC(FST(LAST l)) < LENGTH w 848 ==> 849 !s. s IN A.Q ==> ~((SND(LAST l), ELEM w (FST(LAST l)), s) IN A.Delta))``, 850 RW_TAC (srw_ss()++resq_SS) [COMPUTATION_COMPUTATION_MODEL_AUTOMATON,IN_LESS_LENGTH_SUB1] 851 THEN EQ_TAC 852 THEN ZAP_TAC list_ss [SUC_SUB1_LS,GT_LE_TRANS] 853 THEN Induct_on `n` 854 THEN RW_TAC list_ss [] 855 THEN PROVE_TAC[SUC_SUB1_LS]); 856 857val XNUM_LS = 858 store_thm 859 ("XNUM_LS", 860 ``XNUM m < n = m < n``, 861 Cases_on `n` 862 THEN RW_TAC std_ss [LS]); 863 864val COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR2 = 865 store_thm 866 ("COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR2", 867 ``AUTOMATON A 868 ==> 869 (v IN COMPUTATION(COMPUTATION_TO_MODEL w || A) = 870 LENGTH v > 0 /\ (FST(ELEM v 0) = 0) 871 /\ 872 SND(ELEM v 0) IN A.Q0 /\ LENGTH v <= LENGTH w 873 /\ 874 (!n. n < LENGTH v ==> (FST(ELEM v n) = n)) 875 /\ 876 (!n. n < (LENGTH v - 1) ==> 877 SND(ELEM v n) IN A.Q /\ 878 (SND(ELEM v n), ELEM w n, SND(ELEM v (SUC n))) IN A.Delta) 879 /\ 880 !l. (v = FINITE l) /\ LENGTH v < LENGTH w 881 ==> 882 !s. s IN A.Q ==> ~((SND(LAST l), ELEM w (FST(LAST l)), s) IN A.Delta))``, 883 RW_TAC (srw_ss()++resq_SS) [COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR1,IN_LESS_LENGTH_SUB1] 884 THEN EQ_TAC 885 THEN ZAP_TAC list_ss [SUC_SUB1_LS,GT_LE_TRANS] 886 THEN FULL_SIMP_TAC list_ss [LENGTH_def,ELEM_FINITE,GT,LS,SUB,LE] 887 THEN `LENGTH l - 1 < LENGTH l` by DECIDE_TAC 888 THEN `FST(LAST l) = LENGTH l - 1` by PROVE_TAC[LENGTH_LAST] 889 THEN `SUC(FST(LAST l)) = LENGTH l` by DECIDE_TAC 890 THEN FULL_SIMP_TAC list_ss [XNUM_LS]); 891 892val COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR3 = 893 store_thm 894 ("COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR3", 895 ``TOTAL_AUTOMATON A 896 ==> 897 (v IN COMPUTATION(COMPUTATION_TO_MODEL w || A) = 898 LENGTH v > 0 /\ (FST(ELEM v 0) = 0) 899 /\ 900 SND(ELEM v 0) IN A.Q0 /\ (LENGTH v = LENGTH w) 901 /\ 902 (!n. n < LENGTH v ==> (FST(ELEM v n) = n)) 903 /\ 904 (!n. n < (LENGTH v - 1) ==> 905 SND(ELEM v n) IN A.Q /\ 906 (SND(ELEM v n), ELEM w n, SND(ELEM v (SUC n))) IN A.Delta))``, 907 RW_TAC (srw_ss()++resq_SS) 908 [TOTAL_AUTOMATON_def,COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR2,IN_LESS_LENGTH_SUB1] 909 THEN EQ_TAC 910 THEN RW_TAC list_ss [SUC_SUB1_LS,GT_LE_TRANS] 911 THEN TRY(Cases_on `v`) THEN TRY(Cases_on `w`) 912 THEN FULL_SIMP_TAC list_ss 913 [LENGTH_def,ELEM_FINITE,GT,LS,SUB,LE,xnum_11,xnum_distinct,path_11] 914 THENL 915 [Cases_on `LENGTH l < LENGTH l'` 916 THEN TRY DECIDE_TAC 917 THEN `?s'. s' IN A.Q /\ (SND (LAST l),EL (FST (LAST l)) l',s) IN A.Delta` 918 by PROVE_TAC[] 919 THEN PROVE_TAC[], 920 `?s'. s' IN A.Q /\ (SND (LAST l),EL (FST (LAST l)) l',s) IN A.Delta` 921 by PROVE_TAC[] 922 THEN PROVE_TAC[]]); 923 924val LANGUAGE_def = 925 Define 926 `(LANGUAGE A (FINITE l) = 927 (LENGTH l > 0) /\ 928 EL 0 l IN A.Q0 /\ 929 (!n :: (LESS(LENGTH l - 1)). ?a. (EL n l, a, EL (SUC n) l) IN A.Delta) /\ 930 !a s. ~((EL (LENGTH l - 1) l, a, s) IN A.Delta)) 931 /\ 932 (LANGUAGE A (INFINITE f) = 933 f 0 IN A.Q0 /\ !n. ?a. (f n, a, f(SUC n)) IN A.Delta)`; 934 935(*****************************************************************************) 936(* MODEL_TO_AUTOMATON adds a value -- "iota" in Clarke/Grumberg/Peled -- to *) 937(* the states of M. STRIP_IOTA removes iotas. *) 938(* Not sure if this is needed. *) 939(*****************************************************************************) 940val STRIP_IOTA_def = 941 Define `STRIP_IOTA(SOME x) = x`; 942 943val PATH_STRIP_IOTA_def = 944 Define 945 `(PATH_STRIP_IOTA(FINITE l) = FINITE(MAP STRIP_IOTA l)) 946 /\ 947 (PATH_STRIP_IOTA(INFINITE f) = INFINITE(STRIP_IOTA o f))`; 948 949(*****************************************************************************) 950(* Add iotas to a path *) 951(*****************************************************************************) 952val PATH_ADD_IOTA_def = 953 Define 954 `(PATH_ADD_IOTA(FINITE l) = FINITE(MAP SOME l)) 955 /\ 956 (PATH_ADD_IOTA(INFINITE f) = INFINITE(SOME o f))`; 957 958(*****************************************************************************) 959(* Should have proved FINITE_PATH_LANGUAGE directly, but now too lazy to *) 960(* tweak the rather tedious proof. *) 961(*****************************************************************************) 962val FINITE_PATH_LANGUAGE_LEMMA = 963 store_thm 964 ("FINITE_PATH_LANGUAGE_LEMMA", 965 ``!M s l. 966 MODEL M /\ s IN M.S0 /\ (s = HD l) 967 ==> 968 (PATH M s (FINITE l) = 969 LANGUAGE 970 (MODEL_TO_AUTOMATON M) 971 (CONS(NONE, (PATH_ADD_IOTA (FINITE l)))))``, 972 REPEAT GEN_TAC 973 THEN SIMP_TAC (list_ss++resq_SS) 974 [MODEL_def,PATH_CASES,LANGUAGE_def,MODEL_TO_AUTOMATON_def, 975 PATH_ADD_IOTA_def,CONS_def] 976 THEN RW_TAC (srw_ss()) [] 977 THEN EQ_TAC 978 THEN RW_TAC list_ss [] (* 9 subgoals *) 979 THENL 980 [Cases_on `n` 981 THEN RW_TAC list_ss [] 982 THENL 983 [Q.EXISTS_TAC `HD l` 984 THEN RW_TAC list_ss [] 985 THEN Cases_on `l` 986 THEN RW_TAC list_ss [] 987 THEN FULL_SIMP_TAC list_ss [], 988 Q.EXISTS_TAC `M.L(EL (SUC n') l)` 989 THEN DISJ1_TAC 990 THEN Q.EXISTS_TAC `EL n' l` 991 THEN Q.EXISTS_TAC `EL (SUC n') l` 992 THEN `n' < LENGTH l` by DECIDE_TAC 993 THEN RW_TAC list_ss [EL_MAP] 994 THEN Cases_on `l` 995 THEN RW_TAC list_ss [] 996 THEN FULL_SIMP_TAC list_ss [] 997 THEN `n' < LENGTH t` by DECIDE_TAC 998 THEN RW_TAC list_ss [EL_MAP]], 999 Cases_on `(~(EL (LENGTH l) (NONE::MAP SOME l) = SOME s') \/ ~(a = M.L s'') \/ 1000 ~(s = SOME s'')) \/ ~((s',s'') IN M.R)` 1001 THEN FULL_SIMP_TAC list_ss [] 1002 THEN RW_TAC list_ss [] 1003 THEN `LENGTH l = SUC(LENGTH l - 1)` by DECIDE_TAC 1004 THEN `EL (LENGTH l - 1) (MAP SOME l) = SOME s'` by PROVE_TAC[TL,EL] 1005 THEN `LENGTH l - 1 < LENGTH l` by DECIDE_TAC 1006 THEN `SOME(EL (LENGTH l - 1) l) = SOME s'` by PROVE_TAC[EL_MAP] 1007 THEN FULL_SIMP_TAC list_ss [] 1008 THEN PROVE_TAC[], 1009 Cases_on `(~(EL (LENGTH l) (NONE::MAP SOME l) = NONE) \/ ~(a = M.L s') \/ 1010 ~(s = SOME s')) \/ ~(s' IN M.S0)` 1011 THEN FULL_SIMP_TAC list_ss [] 1012 THEN RW_TAC list_ss [] 1013 THEN `LENGTH l = SUC(LENGTH l - 1)` by DECIDE_TAC 1014 THEN `EL (LENGTH l - 1) (MAP SOME l) = NONE` by PROVE_TAC[TL,EL] 1015 THEN `LENGTH l - 1 < LENGTH l` by DECIDE_TAC 1016 THEN `SOME(EL (LENGTH l - 1) l) = NONE` by PROVE_TAC[EL_MAP] 1017 THEN FULL_SIMP_TAC list_ss [], 1018 Cases_on `LENGTH l = 0` 1019 THEN RW_TAC list_ss [] 1020 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th]), 1021 FULL_SIMP_TAC list_ss [SUBSET_DEF], 1022 `SUC n < LENGTH l` by DECIDE_TAC 1023 THEN RES_TAC 1024 THEN `n < LENGTH l` by DECIDE_TAC 1025 THEN FULL_SIMP_TAC list_ss [EL_MAP] 1026 THEN PROVE_TAC[], 1027 `SUC n < LENGTH l` by DECIDE_TAC 1028 THEN RES_TAC 1029 THEN `n < LENGTH l` by DECIDE_TAC 1030 THEN FULL_SIMP_TAC list_ss [EL_MAP] 1031 THEN Cases_on `l` 1032 THEN RW_TAC list_ss [] 1033 THEN FULL_SIMP_TAC list_ss [] 1034 THEN `EL n (MAP SOME t) = SOME (EL n t)` by PROVE_TAC[EL_MAP] 1035 (* Above needed, I think, for mysterious type variable reasons *) 1036 THEN `SOME(EL n t) = SOME s''` by PROVE_TAC[] 1037 THEN FULL_SIMP_TAC list_ss [] 1038 THEN PROVE_TAC[], 1039 `SUC n < LENGTH l` by DECIDE_TAC 1040 THEN RES_TAC 1041 THEN FULL_SIMP_TAC list_ss [EL_MAP] 1042 THEN `n < LENGTH l` by DECIDE_TAC 1043 THEN `EL n (MAP SOME l) = SOME (EL n l)` by PROVE_TAC[EL_MAP] 1044 THENL 1045 [`SOME(EL n l) = SOME s'` by PROVE_TAC[] 1046 THEN FULL_SIMP_TAC list_ss [] 1047 THEN Cases_on `l` 1048 THEN RW_TAC list_ss [] 1049 THEN FULL_SIMP_TAC list_ss [] 1050 THEN `EL n (MAP SOME t) = SOME (EL n t)` by PROVE_TAC[EL_MAP] 1051 (* Above needed, I think, for mysterious type variable reasons *) 1052 THEN `SOME(EL n t) = SOME s''` by PROVE_TAC[] 1053 THEN FULL_SIMP_TAC list_ss [], 1054 `SOME(EL n l) = NONE` by PROVE_TAC[] 1055 THEN FULL_SIMP_TAC list_ss []], 1056 Cases_on `LENGTH l = 0` 1057 THEN RW_TAC list_ss [] 1058 THEN FULL_SIMP_TAC list_ss [] 1059 THEN Know `LENGTH l - 1 < LENGTH l` 1060 >- (Suff `LENGTH l <> 0` >- DECIDE_TAC \\ 1061 METIS_TAC [LENGTH_EQ_NUM]) >> DISCH_TAC 1062 THEN RES_TAC 1063 THENL 1064 [`!a s. 1065 (!s' s''. 1066 (~(EL (LENGTH l) (NONE::MAP SOME l) = SOME s') \/ 1067 ~(a = M.L s'') \/ ~(s = SOME s'')) \/ ~((s',s'') IN M.R))` 1068 by PROVE_TAC[] 1069 THEN POP_ASSUM 1070 (fn th => 1071 ASSUME_TAC(Q.SPECL[`M.L s`,`SOME s`,`EL (LENGTH l - 1) l`,`s`]th)) 1072 THEN FULL_SIMP_TAC list_ss [] 1073 THEN `LENGTH l = SUC(LENGTH l - 1)` by DECIDE_TAC 1074 THEN `LENGTH l - 1 < LENGTH l` by DECIDE_TAC 1075 THEN PROVE_TAC[EL,TL,EL_MAP], 1076 `!a s. 1077 (!s' s''. 1078 (~(EL (LENGTH l) (NONE::MAP SOME l) = SOME s') \/ 1079 ~(a = M.L s'') \/ ~(s = SOME s'')) \/ ~((s',s'') IN M.R))` 1080 by PROVE_TAC[] 1081 THEN POP_ASSUM 1082 (fn th => 1083 ASSUME_TAC(Q.SPECL[`M.L s`,`SOME s`,`EL (LENGTH l - 1) l`,`s`]th)) 1084 THEN FULL_SIMP_TAC list_ss [] 1085 THEN `LENGTH l = SUC(LENGTH l - 1)` by DECIDE_TAC 1086 THEN `LENGTH l - 1 < LENGTH l` by DECIDE_TAC 1087 THEN PROVE_TAC[EL,TL,EL_MAP]]]); 1088 1089(*****************************************************************************) 1090(* |- !M l. *) 1091(* MODEL M /\ HD l IN M.S0 ==> *) 1092(* (PATH M (HD l) (FINITE l) = *) 1093(* LANGUAGE (MODEL_TO_AUTOMATON M) *) 1094(* (CONS (NONE,PATH_ADD_IOTA (FINITE l)))) *) 1095(*****************************************************************************) 1096val FINITE_PATH_LANGUAGE = 1097 save_thm 1098 ("FINITE_PATH_LANGUAGE", 1099 ((Q.GEN `M` o Q.GEN `l`) 1100 (SIMP_RULE list_ss [] 1101 (Q.SPECL[`M`,`HD l`,`l`]FINITE_PATH_LANGUAGE_LEMMA)))); 1102 1103val INFINITE_PATH_LANGUAGE = 1104 store_thm 1105 ("INFINITE_PATH_LANGUAGE", 1106 ``!M f. 1107 MODEL M /\ f 0 IN M.S0 1108 ==> 1109 (PATH M (f 0) (INFINITE f) = 1110 LANGUAGE 1111 (MODEL_TO_AUTOMATON M) 1112 (CONS(NONE, (PATH_ADD_IOTA (INFINITE f)))))``, 1113 REPEAT GEN_TAC 1114 THEN SIMP_TAC (list_ss++resq_SS) 1115 [MODEL_def,PATH_CASES,LANGUAGE_def,MODEL_TO_AUTOMATON_def, 1116 PATH_ADD_IOTA_def,CONS_def] 1117 THEN RW_TAC (srw_ss()) [] 1118 THEN EQ_TAC 1119 THEN RW_TAC list_ss [] 1120 THENL 1121 [Cases_on `n` 1122 THEN RW_TAC list_ss [], 1123 Cases_on `n` 1124 THEN ZAP_TAC list_ss [SUBSET_DEF], 1125 POP_ASSUM(STRIP_ASSUME_TAC o Q.SPEC `SUC n`) 1126 THEN FULL_SIMP_TAC list_ss []]); 1127 1128val PATH_LANGUAGE = 1129 store_thm 1130 ("PATH_LANGUAGE", 1131 ``!M w. 1132 MODEL M /\ (ELEM w 0) IN M.S0 1133 ==> 1134 (PATH M (ELEM w 0) w = 1135 LANGUAGE (MODEL_TO_AUTOMATON M) (CONS(NONE, (PATH_ADD_IOTA w))))``, 1136 REPEAT GEN_TAC 1137 THEN Cases_on `w` 1138 THEN SIMP_TAC (list_ss++resq_SS) 1139 [ELEM_def,HEAD_def,REST_def,RESTN_def, 1140 FINITE_PATH_LANGUAGE,INFINITE_PATH_LANGUAGE]); 1141 1142(*****************************************************************************) 1143(* Not sure if the next four theorems are needed *) 1144(* (as they are subsumed by the following two). *) 1145(*****************************************************************************) 1146 1147val UF_SEM_FINITE_TOP_FREE_F_ALWAYS = 1148 store_thm 1149 ("UF_SEM_FINITE_TOP_FREE_F_ALWAYS", 1150 ``TOP_FREE l 1151 ==> 1152 (UF_SEM (FINITE l) (F_ALWAYS(F_WEAK_BOOL b)) = 1153 !i. i < LENGTH l ==> B_SEM (EL i l) b)``, 1154 RW_TAC 1155 (list_ss++resq_SS) 1156 [UF_SEM,B_SEM_def,UF_SEM_F_G,F_ALWAYS_def,FinitePSLPathTheory.LENGTH_RESTN,LESSX_def,LS, 1157 ELEM_RESTN,ELEM_def,HEAD_def,REST_def,RESTN_FINITE,HD_RESTN,xnum_11,TOP_FREE_EL] 1158 THEN EQ_TAC 1159 THEN RW_TAC list_ss [] 1160 THEN RES_TAC 1161 THEN `j < LENGTH l` by DECIDE_TAC 1162 THEN RES_TAC); 1163 1164val UF_SEM_FINITE_F_ALWAYS = 1165 store_thm 1166 ("UF_SEM_FINITE_F_ALWAYS", 1167 ``UF_SEM (FINITE l) (F_ALWAYS(F_WEAK_BOOL b)) = 1168 !i. i < LENGTH l ==> B_SEM (EL i l) b \/ 1169 ?j. j < i /\ (EL j l = TOP) /\ ~(LENGTH l = j)``, 1170 RW_TAC 1171 (list_ss++resq_SS) 1172 [UF_SEM,B_SEM_def,UF_SEM_F_G,F_ALWAYS_def,FinitePSLPathTheory.LENGTH_RESTN,LESSX_def,LS, 1173 ELEM_RESTN,ELEM_def,HEAD_def,REST_def,RESTN_FINITE,HD_RESTN,xnum_11,TOP_FREE_EL] 1174 THEN EQ_TAC 1175 THEN RW_TAC list_ss []); 1176 1177val UF_SEM_INFINITE_TOP_FREE_F_ALWAYS = 1178 store_thm 1179 ("UF_SEM_INFINITE_TOP_FREE_F_ALWAYS", 1180 ``(!i:num. ~(f i = TOP)) 1181 ==> 1182 (UF_SEM (INFINITE f) (F_ALWAYS(F_WEAK_BOOL b)) = !i. B_SEM (f i) b)``, 1183 RW_TAC 1184 (list_ss++resq_SS) 1185 [UF_SEM,B_SEM_def,UF_SEM_F_G,F_ALWAYS_def,LENGTH_RESTN,LESSX_def,LS, 1186 ELEM_RESTN,ELEM_def,HEAD_def,REST_def,RESTN_INFINITE,HD_RESTN,TOP_FREE_EL]); 1187 1188val UF_SEM_INFINITE_F_ALWAYS = 1189 store_thm 1190 ("UF_SEM_INFINITE_F_ALWAYS", 1191 ``UF_SEM (INFINITE f) (F_ALWAYS(F_WEAK_BOOL b)) = 1192 !i. B_SEM (f i) b \/ ?j. j < i /\ (f j = TOP)``, 1193 RW_TAC 1194 (list_ss++resq_SS) 1195 [UF_SEM,B_SEM_def,UF_SEM_F_G,F_ALWAYS_def,LENGTH_RESTN,LESSX_def,LS, 1196 ELEM_RESTN,ELEM_def,HEAD_def,REST_def,RESTN_INFINITE,HD_RESTN]); 1197 1198val UF_SEM_F_ALWAYS = 1199 store_thm 1200 ("UF_SEM_F_ALWAYS", 1201 ``UF_SEM w (F_ALWAYS(F_WEAK_BOOL b)) = 1202 !i::LESS(LENGTH w). B_SEM (ELEM w i) b \/ ?j::LESS i. ELEM w j = TOP``, 1203 Cases_on `w` 1204 THEN RW_TAC (list_ss++resq_SS) 1205 [UF_SEM_FINITE_F_ALWAYS,UF_SEM_INFINITE_F_ALWAYS,LENGTH_def,ELEM_def, 1206 LENGTH_RESTN,LESSX_def,LS,ELEM_RESTN,ELEM_def,HEAD_def,REST_def, 1207 RESTN_INFINITE,RESTN_FINITE,HD_RESTN] 1208 THEN EQ_TAC 1209 THEN RW_TAC list_ss [] 1210 THEN RES_TAC 1211 THEN ZAP_TAC list_ss [] 1212 THEN `~(LENGTH l = j)` by DECIDE_TAC 1213 THEN PROVE_TAC[]); 1214 1215val UF_SEM_TOP_FREE_F_ALWAYS = 1216 store_thm 1217 ("UF_SEM_TOP_FREE_F_ALWAYS", 1218 ``PATH_TOP_FREE w 1219 ==> 1220 (UF_SEM w (F_ALWAYS(F_WEAK_BOOL b)) = !i::LESS(LENGTH w). B_SEM (ELEM w i) b)``, 1221 Cases_on `w` 1222 THEN RW_TAC (list_ss++resq_SS) 1223 [UF_SEM_FINITE_F_ALWAYS,UF_SEM_INFINITE_F_ALWAYS,LENGTH_def,ELEM_def, 1224 LENGTH_RESTN,LESSX_def,LS,ELEM_RESTN,ELEM_def,HEAD_def,REST_def, 1225 RESTN_INFINITE,RESTN_FINITE,HD_RESTN,PATH_TOP_FREE_def] 1226 THEN EQ_TAC 1227 THEN RW_TAC list_ss [] 1228 THEN RES_TAC 1229 THEN FULL_SIMP_TAC list_ss[TOP_FREE_EL] 1230 THEN `j < LENGTH l` by DECIDE_TAC 1231 THEN RES_TAC); 1232 1233val O_TRUE_def = 1234 Define `O_TRUE = O_BOOL B_TRUE`; 1235 1236val O_SEM_O_TRUE = 1237 store_thm 1238 ("O_SEM_O_TRUE", 1239 ``O_SEM M O_TRUE s``, 1240 RW_TAC std_ss [O_TRUE_def,O_SEM_def,B_SEM_def]); 1241 1242val O_EF_def = 1243 Define `O_EF f = O_EU(O_TRUE, f)`; 1244 1245val PATH_ELEM_0 = 1246 store_thm 1247 ("PATH_ELEM_0", 1248 ``PATH M s p ==> (ELEM p 0 = s)``, 1249 Cases_on `p` 1250 THEN RW_TAC (std_ss++resq_SS) [PATH_CASES,ELEM_FINITE,ELEM_INFINITE,EL]); 1251 1252val O_SEM_O_EF = 1253 store_thm 1254 ("O_SEM_O_EF", 1255 ``O_SEM M (O_EF f) s = 1256 ?p :: PATH M s. ?i :: (LESS(LENGTH p)). O_SEM M f (ELEM p i)``, 1257 RW_TAC (std_ss++resq_SS) [IN_DEF,O_EF_def,O_SEM_def,LESSX_def,O_SEM_O_TRUE] 1258 THEN EQ_TAC 1259 THEN ZAP_TAC std_ss [PATH_ELEM_0]); 1260 1261val O_AG_def = 1262 Define `O_AG f = O_NOT(O_EF(O_NOT f))`; 1263 1264val O_SEM_O_AG = 1265 store_thm 1266 ("O_SEM_O_AG", 1267 ``O_SEM M (O_AG f) s = 1268 !p :: PATH M s. !i :: (LESS(LENGTH p)). O_SEM M f (ELEM p i)``, 1269 RW_TAC (std_ss++resq_SS) [IN_DEF,O_SEM_O_EF,O_AG_def,O_SEM_def,LESSX_def] 1270 THEN EQ_TAC 1271 THEN ZAP_TAC std_ss [PATH_ELEM_0]); 1272 1273(*****************************************************************************) 1274(* Lemmas about MAP_PATH *) 1275(*****************************************************************************) 1276 1277val LENGTH_MAP_PATH = 1278 store_thm 1279 ("LENGTH_MAP_PATH", 1280 ``!g p. LENGTH(MAP_PATH g p) = LENGTH p``, 1281 Cases_on `p` 1282 THEN RW_TAC list_ss [MAP_PATH_def,LENGTH_def]); 1283 1284val ELEM_MAP_PATH = 1285 store_thm 1286 ("ELEM_MAP_PATH", 1287 ``n < LENGTH p ==> (ELEM (MAP_PATH g p) n = g(ELEM p n))``, 1288 Cases_on `p` 1289 THEN RW_TAC list_ss 1290 [MAP_PATH_def,ELEM_INFINITE,ELEM_FINITE,LENGTH_def,LS,EL_MAP]); 1291 1292val RESTN_MAP_PATH = 1293 store_thm 1294 ("RESTN_MAP_PATH", 1295 ``n < LENGTH p ==> (RESTN (MAP_PATH g p) n = MAP_PATH g (RESTN p n))``, 1296 Cases_on `p` 1297 THEN RW_TAC list_ss 1298 [MAP_PATH_def,ELEM_INFINITE,ELEM_FINITE,LENGTH_def,LS,EL_MAP, 1299 RESTN_FINITE,RESTN_INFINITE] 1300 THEN Q.UNDISCH_TAC `n < LENGTH l` 1301 THEN Q.SPEC_TAC(`l`,`l`) 1302 THEN Induct_on `n` 1303 THEN RW_TAC list_ss [FinitePSLPathTheory.RESTN_def,FinitePSLPathTheory.REST_def] 1304 THEN `~(LENGTH l = 0)` by DECIDE_TAC 1305 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 1306 THEN RW_TAC list_ss [TL_MAP] 1307 THEN `LENGTH (TL l) = LENGTH l - 1` by RW_TAC arith_ss [LENGTH_TL] 1308 THEN `n < LENGTH(TL l)` by DECIDE_TAC 1309 THEN PROVE_TAC[]); 1310 1311(*****************************************************************************) 1312(* M |=ltl G b! <=> M |=ctl AG b! *) 1313(*****************************************************************************) 1314val SHARED_ALWAYS_STRONG_BOOL = 1315 store_thm 1316 ("SHARED_ALWAYS_STRONG_BOOL", 1317 ``UF_VALID M (F_G(F_STRONG_BOOL b)) = O_VALID M (O_AG(O_BOOL b))``, 1318 RW_TAC (arith_ss++resq_SS) 1319 [IN_DEF,LESSX_def,UF_VALID_def,O_VALID_def,UF_SEM_F_G, 1320 O_SEM_O_AG,COMPUTATION_def,UF_SEM,O_SEM_def,ELEM_RESTN, 1321 ELEM_MAP_PATH,LENGTH_MAP_PATH] 1322 THEN EQ_TAC 1323 THEN RW_TAC std_ss [] 1324 THENL 1325 [`LENGTH (RESTN (MAP_PATH (\s. STATE (M.L s)) p) i) > 0 /\ 1326 B_SEM (STATE (M.L (ELEM p i))) b \/ 1327 ?j. j < i /\ (ELEM (MAP_PATH (\s. STATE (M.L s)) p) j = TOP) /\ 1328 ~(LENGTH p = XNUM j)` 1329 by PROVE_TAC[] 1330 THEN `j < LENGTH p` by PROVE_TAC[LS_TRANS_X] 1331 THEN FULL_SIMP_TAC std_ss [ELEM_MAP_PATH,letter_distinct], 1332 RW_TAC list_ss [RESTN_MAP_PATH,LENGTH_MAP_PATH] 1333 THEN Cases_on `v` 1334 THEN RW_TAC list_ss [RESTN_FINITE,RESTN_INFINITE,LENGTH_def,GT] 1335 THEN IMP_RES_TAC LENGTH_RESTN_COR 1336 THEN FULL_SIMP_TAC list_ss [RESTN_FINITE,LENGTH_def,xnum_11,SUB,LS]]); 1337 1338(*****************************************************************************) 1339(* M |=ltl G b <=> M |=ctl AG b *) 1340(*****************************************************************************) 1341val SHARED_ALWAYS_WEAK_BOOL = 1342 store_thm 1343 ("SHARED_ALWAYS_WEAK_BOOL", 1344 ``UF_VALID M (F_G(F_WEAK_BOOL b)) = O_VALID M (O_AG(O_BOOL b))``, 1345 RW_TAC (arith_ss++resq_SS) 1346 [IN_DEF,LESSX_def,UF_VALID_def,O_VALID_def,UF_SEM_F_G, 1347 O_SEM_O_AG,COMPUTATION_def,UF_SEM,O_SEM_def,ELEM_RESTN, 1348 ELEM_MAP_PATH,LENGTH_MAP_PATH] 1349 THEN EQ_TAC 1350 THEN RW_TAC std_ss [] 1351 THEN `((LENGTH (RESTN (MAP_PATH (\s. STATE (M.L s)) p) i) = 1352 XNUM 0) \/ B_SEM (STATE (M.L (ELEM p i))) b) \/ 1353 ?j. j < i /\ (ELEM (MAP_PATH (\s. STATE (M.L s)) p) j = TOP) /\ 1354 ~(LENGTH p = XNUM j)` 1355 by PROVE_TAC[] 1356 THEN TRY(`j < LENGTH p` by PROVE_TAC[LS_TRANS_X]) 1357 THEN FULL_SIMP_TAC std_ss [ELEM_MAP_PATH,letter_distinct] 1358 THEN `i < LENGTH(MAP_PATH (\s. STATE (M.L s)) p)` by PROVE_TAC[LENGTH_MAP_PATH] 1359 THEN FULL_SIMP_TAC list_ss 1360 [RESTN_MAP_PATH,LENGTH_MAP_PATH,PATH_FINITE_LENGTH_RESTN_0_COR] 1361 THEN `LENGTH(MAP_PATH (\s. STATE (M.L s)) p) = LENGTH(FINITE l)` by PROVE_TAC[] 1362 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LENGTH_MAP_PATH,LS]); 1363 1364val O_OR_def = 1365 Define 1366 `O_OR(f1,f2) = O_NOT(O_AND(O_NOT f1, O_NOT f2))`; 1367 1368val O_SEM_O_OR = 1369 store_thm 1370 ("O_SEM_O_OR", 1371 ``O_SEM M (O_OR (f1,f2)) s = O_SEM M f1 s \/ O_SEM M f2 s``, 1372 RW_TAC list_ss [O_SEM_def,O_OR_def]); 1373 1374val O_IMP_def = 1375 Define 1376 `O_IMP(f1,f2) = O_OR(O_NOT f1, f2)`; 1377 1378val O_SEM_O_IMP = 1379 store_thm 1380 ("O_SEM_O_IMP", 1381 ``O_SEM M (O_IMP (f1,f2)) s = O_SEM M f1 s ==> O_SEM M f2 s``, 1382 RW_TAC list_ss [O_SEM_def,O_SEM_O_OR,O_IMP_def] 1383 THEN PROVE_TAC[]); 1384 1385val O_IFF_def = 1386 Define 1387 `O_IFF(f1,f2) = O_AND(O_IMP(f1, f2), O_IMP(f2, f1))`; 1388 1389val O_SEM_O_IFF = 1390 store_thm 1391 ("O_SEM_O_IFF", 1392 ``O_SEM M (O_IFF (f1,f2)) s = (O_SEM M f1 s = O_SEM M f2 s)``, 1393 RW_TAC list_ss [O_SEM_def,O_SEM_O_IMP,O_IFF_def] 1394 THEN PROVE_TAC[]); 1395 1396(*****************************************************************************) 1397(* M |=ctl AG(b1 <-> b2) ==> M |=ctl AG b1 <-> AG b2 *) 1398(*****************************************************************************) 1399val O_SEM_AG_B_IFF_IMP = 1400 store_thm 1401 ("O_SEM_AG_B_IFF_IMP", 1402 ``O_VALID M (O_AG(O_BOOL(B_IFF(b1, b2)))) ==> 1403 O_VALID M (O_IFF(O_AG(O_BOOL b1), O_AG(O_BOOL b2)))``, 1404 RW_TAC (list_ss++resq_SS) 1405 [O_VALID_def,B_OR_def,B_IFF_def,B_IMP_def,B_SEM_def,B_SEM_def, 1406 O_SEM_O_AG,O_SEM_def,O_SEM_O_IFF] 1407 THEN PROVE_TAC[]); 1408 1409(* 1410Ultimately want: 1411 1412 M0 || A |= G b ==> !pi. pi in COMPUTATION M0 ==> pi || A |= G b 1413 1414try to prove 1415 1416 M0 || A |= f ==> !pi. pi in COMPUTATION M0 ==> pi || A |= f 1417*) 1418 1419val UF_INFINITE_VALID_def = 1420 Define 1421 `UF_INFINITE_VALID M f = 1422 !pi. COMPUTATION M (INFINITE pi) 1423 ==> 1424 UF_SEM (MAP_PATH (\s. STATE (M.L s)) (INFINITE pi)) f`; 1425 1426val UF_FINITE_VALID_def = 1427 Define 1428 `UF_FINITE_VALID M f = 1429 !pi. COMPUTATION M (FINITE pi) 1430 ==> 1431 UF_SEM (MAP_PATH (\s. STATE (M.L s)) (FINITE pi)) f`; 1432 1433 1434(*****************************************************************************) 1435(* mike, *) 1436(* *) 1437(* >If M (I assume I meant "M0") is the open model, would you expect: *) 1438(* > *) 1439(* > (M0 || A |=ltl f) and pi a computation of M0 implies (pi || A |=ltl f) *) 1440(* > *) 1441(* >to hold. *) 1442(* *) 1443(* yes. *) 1444(* *) 1445(* cindy. *) 1446(*****************************************************************************) 1447 1448val FST_LEMMA = 1449 prove 1450 (``!Q x. (\(s,t). Q s) x = Q(FST x)``, 1451 Cases_on `x` 1452 THEN RW_TAC std_ss []); 1453 1454(* Probably won't need this *) 1455val OPEN_MODEL_PROD_INFINITE = 1456 store_thm 1457 ("OPEN_MODEL_PROD_INFINITE", 1458 ``(?p. ~(p IN P)) /\ AUTOMATON A /\ UF_VALID (MODEL_AUTOMATON_PROD (OPEN_MODEL P) A) f 1459 ==> 1460 !pi. COMPUTATION (OPEN_MODEL P) (INFINITE pi) 1461 ==> 1462 UF_INFINITE_VALID 1463 (MODEL_AUTOMATON_PROD (COMPUTATION_TO_MODEL(INFINITE pi)) A) 1464 f``, 1465 RW_TAC (srw_ss()++resq_SS) 1466 [AUTOMATON_def,UF_VALID_def,UF_INFINITE_VALID_def,MODEL_AUTOMATON_PROD_def, 1467 OPEN_MODEL_def,COMPUTATION_def,IN_COMPUTATION,COMPUTATION_TO_MODEL_CASES,PATH_CASES] 1468 THEN FULL_SIMP_TAC list_ss 1469 [FST_LEMMA,PROVE[]``(!v. (?s. P s v) ==> Q v) = !v s. P s v ==> Q v``, 1470 MAP_PATH_def] 1471 THEN `(!n. (?s t. (pi' n = (s,t)) /\ t IN A.Q)) /\ 1472 (!n. ?s t t'. 1473 ((pi' n = (s,t)) /\ (pi' (SUC n) = (s + 1,t'))) /\ 1474 (t,pi s,t') IN A.Delta)` 1475 by PROVE_TAC[] 1476 THEN POP_ASSUM(fn th => STRIP_ASSUME_TAC(CONV_RULE SKOLEM_CONV th)) 1477 THEN POP_ASSUM(fn th => STRIP_ASSUME_TAC(CONV_RULE SKOLEM_CONV th)) 1478 THEN POP_ASSUM(fn th => STRIP_ASSUME_TAC(CONV_RULE SKOLEM_CONV th)) 1479 THEN ASSUM_LIST(fn thl => STRIP_ASSUME_TAC(CONV_RULE SKOLEM_CONV (el 2 thl))) 1480 THEN POP_ASSUM(fn th => STRIP_ASSUME_TAC(CONV_RULE SKOLEM_CONV th)) 1481 THEN ASSUM_LIST 1482 (fn thl => ASSUME_TAC 1483 (SPECL 1484 [``INFINITE(\n. (pi(FST((pi' :num -> num # 'b) n)), t''' n)):(('a -> bool) # 'b) path``, 1485 ``(pi:num -> 'a -> bool 0,t):('a -> bool) # 'b``] 1486 (el 9 thl))) 1487 THEN `PATH 1488 <|S := {(s,t) | (s SUBSET P \/ (s = SINK P)) /\ t IN A.Q}; 1489 S0 := {(s,t) | s SUBSET P /\ t IN A.Q0}; 1490 R := 1491 {((s,t),s',t') | 1492 (s SUBSET P /\ (s' SUBSET P \/ (s' = SINK P))) /\ 1493 (t,(if s = SINK P then {} else s),t') IN A.Delta}; P := P; 1494 L := (\(s,t). (if s = SINK P then {} else s))|> (pi 0,t) 1495 (INFINITE (\n. (pi:num -> 'a -> bool (FST (pi':num -> num # 'b n)),t''' n))) 1496 ==> 1497 UF_SEM 1498 (MAP_PATH (\s'. STATE (if FST s' = SINK P then {} else FST s')) 1499 (INFINITE (\n. (pi (FST (pi' n)),t''' n)))) f` 1500 by PROVE_TAC[] 1501 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE (srw_ss()++resq_SS) [PATH_CASES,MAP_PATH_def]) 1502 THEN POP_ASSUM(fn th => ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss thl th))) 1503 THEN ASM_REWRITE_TAC [] 1504 THEN ASSUM_LIST(fn thl => POP_ASSUM(fn th => ASSUME_TAC(SIMP_RULE list_ss [SIMP_RULE list_ss [el 8 thl] (Q.SPEC `0` (el 3 thl))] th))) 1505 THEN ASSUM_LIST(fn thl => POP_ASSUM(fn th => ASSUME_TAC(SIMP_RULE list_ss [SIMP_RULE list_ss [el 3 thl] (Q.SPEC `n` (el 4 thl))] th))) 1506 THEN ASSUM_LIST(fn thl => REWRITE_TAC[SIMP_RULE list_ss [el 3 thl] (Q.SPEC `n` (el 4 thl))]) 1507 THEN `!n. (pi:num -> 'a -> bool) n SUBSET P` by METIS_TAC[] 1508 THEN `!n. ~((pi:num -> 'a -> bool) n = SINK P)` by PROVE_TAC[SUBSET_SINK] 1509 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th])); 1510 1511(*****************************************************************************) 1512(* |- (COMPUTATION_TO_MODEL w || A).L = *) 1513(* (\(s,t). {p | s < LENGTH w /\ p IN ELEM w s}) : thm *) 1514(*****************************************************************************) 1515val LEMMA4 = 1516 SIMP_CONV (srw_ss()++resq_SS) 1517 [MODEL_AUTOMATON_PROD_def,OPEN_MODEL_def,IN_COMPUTATION,COMPUTATION_TO_MODEL_def, 1518 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK, 1519 DECIDE ``~A \/ (~B \/ ~C /\ ~D) \/ E = A ==> B ==> (C \/ D) ==> E``, 1520 LEMMA1] 1521 ``(COMPUTATION_TO_MODEL w || A).L``; 1522 1523val FST_SND_LEMMA = 1524 prove 1525 (``!p x y. (p = (x,y)) = (x = FST p) /\ (y = SND p)``, 1526 Cases_on `p` 1527 THEN ZAP_TAC std_ss []); 1528 1529val SET_COND = 1530 store_thm 1531 ("SET_COND", 1532 ``{p | P /\ (p IN Q)} = if ~P then {} else Q``, 1533 RW_TAC (srw_ss()++resq_SS) [EXTENSION] 1534 THEN RW_TAC std_ss[]); 1535 1536val SINGLETON_SUBSET_IN = 1537 store_thm 1538 ("SINGLETON_SUBSET_IN", 1539 ``(\x. x=a) SUBSET X = a IN X``, 1540 RW_TAC std_ss [SUBSET_DEF,IN_DEF]); 1541 1542val PAIR_EQ_SPLIT = 1543 store_thm 1544 ("PAIR_EQ_SPLIT", 1545 ``((a,b) = p) = (a = FST p) /\ (b = SND p)``, 1546 Cases_on `p` 1547 THEN RW_TAC list_ss []); 1548 1549val LS_SUB1 = 1550 store_thm 1551 ("LS_SUB1", 1552 ``m:num < (n:xnum) - 1 ==> m < n``, 1553 Cases_on `n` 1554 THEN RW_TAC arith_ss [LS,LE,SUB]); 1555 1556val LS_SUB1_SUC = 1557 store_thm 1558 ("LS_SUB1_SUC", 1559 ``m:num < (n:xnum) - 1 ==> SUC m < n``, 1560 Cases_on `n` 1561 THEN RW_TAC arith_ss [LS,LE,SUB]); 1562 1563val MAP_PATH_FST_EXISTS = 1564 store_thm 1565 ("MAP_PATH_FST_EXISTS", 1566 ``(MAP_PATH FST p = FINITE l1) ==> ?l. p = FINITE l``, 1567 Cases_on `p` 1568 THEN RW_TAC list_ss [MAP_PATH_def]); 1569 1570val PROD_FST = 1571 store_thm 1572 ("PROD_FST", 1573 ``TOTAL_AUTOMATON A /\ p IN PATH (M || A) (s,t) ==> (MAP_PATH FST p) IN PATH M s ``, 1574 RW_TAC (srw_ss()++resq_SS) 1575 [PATH_def,IN_LESS_LENGTH_SUB1,LENGTH_MAP_PATH,GT_LS,ELEM_MAP_PATH, 1576 PAIR_EQ_SPLIT,ELEM_FINITE,TOTAL_AUTOMATON_def,IN_PATH, 1577 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).S``, 1578 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).R``] 1579 THEN IMP_RES_TAC LS_SUB1 1580 THEN IMP_RES_TAC LS_SUB1_SUC 1581 THEN IMP_RES_TAC MAP_PATH_FST_EXISTS 1582 THEN RW_TAC list_ss [ELEM_MAP_PATH] 1583 THEN `?s'. (SND (EL (LENGTH l' - 1) l'), 1584 M.L (FST (EL (LENGTH l' - 1) l')), 1585 s') IN A.Delta` 1586 by PROVE_TAC[] 1587 THEN ASSUM_LIST 1588 (fn thl => 1589 ASSUME_TAC 1590 (SIMP_RULE std_ss [el 1 thl] (Q.SPEC `(s',s'')` (el 2 thl)))) 1591 THEN FULL_SIMP_TAC list_ss [MAP_PATH_def,path_11,LENGTH_def,ELEM_FINITE,LS,SUB] 1592 THEN RW_TAC arith_ss [LENGTH_MAP,EL_MAP] 1593 THEN METIS_TAC[AUTOMATON_def]); 1594 1595val MAP_PATH_MAP_PATH = 1596 store_thm 1597 ("MAP_PATH_MAP_PATH", 1598 ``MAP_PATH f (MAP_PATH g p) = MAP_PATH (\x. f(g x)) p``, 1599 Cases_on `p` 1600 THEN RW_TAC list_ss [MAP_PATH_def,MAP_MAP_o,combinTheory.o_DEF]); 1601 1602val MK_FINITE_PROD_PATH_def = 1603 Define 1604 `(MK_FINITE_PROD_PATH [] n = []) /\ 1605 (MK_FINITE_PROD_PATH (x::l) n = (n,SND x)::MK_FINITE_PROD_PATH l (n+1))`; 1606 1607val MK_INFINITE_PROD_PATH_def = 1608 Define 1609 `MK_INFINITE_PROD_PATH f = \n. (n,SND(f n))`; 1610 1611val MK_PROD_PATH_def = 1612 Define 1613 `(MK_PROD_PATH(FINITE l) = FINITE(MK_FINITE_PROD_PATH l 0)) /\ 1614 (MK_PROD_PATH(INFINITE f) = INFINITE(MK_INFINITE_PROD_PATH f))`; 1615 1616val LENGTH_MK_FINITE_PROD_PATH = 1617 store_thm 1618 ("LENGTH_MK_FINITE_PROD_PATH", 1619 ``!l n. LENGTH(MK_FINITE_PROD_PATH l n) = LENGTH l``, 1620 Induct 1621 THEN RW_TAC list_ss [LENGTH_def,MK_FINITE_PROD_PATH_def]); 1622 1623val LENGTH_MK_PROD_PATH = 1624 store_thm 1625 ("LENGTH_MK_PROD_PATH", 1626 ``LENGTH(MK_PROD_PATH p) = LENGTH p``, 1627 Cases_on `p` 1628 THEN RW_TAC list_ss 1629 [LENGTH_def,MK_PROD_PATH_def,LENGTH_MK_FINITE_PROD_PATH]); 1630 1631val ELEM_MK_FINITE_PROD_PATH = 1632 store_thm 1633 ("ELEM_MK_FINITE_PROD_PATH", 1634 ``!l m n. 1635 m < LENGTH l 1636 ==> 1637 (EL m (MK_FINITE_PROD_PATH l n) = (m+n, SND(EL m l)))``, 1638 Induct 1639 THEN RW_TAC list_ss [ELEM_def,MK_FINITE_PROD_PATH_def] 1640 THEN Cases_on `m` 1641 THEN RW_TAC list_ss []); 1642 1643val ELEM_MK_PROD_PATH = 1644 store_thm 1645 ("ELEM_MK_PROD_PATH", 1646 ``!l m. 1647 m < LENGTH p ==> (ELEM (MK_PROD_PATH p) m = (m,SND(ELEM p m)))``, 1648 Cases_on `p` 1649 THEN RW_TAC list_ss 1650 [MK_PROD_PATH_def, 1651 ELEM_FINITE,ELEM_INFINITE,LENGTH_def, 1652 MK_INFINITE_PROD_PATH_def,MK_FINITE_PROD_PATH_def] 1653 THEN FULL_SIMP_TAC list_ss [LS,ELEM_MK_FINITE_PROD_PATH]); 1654 1655val AUTOMATON_Q0_Q = 1656 store_thm 1657 ("AUTOMATON_Q0_Q", 1658 ``!A t. AUTOMATON A /\ t IN A.Q0 ==> t IN A.Q``, 1659 RW_TAC list_ss [SUBSET_DEF,AUTOMATON_def]); 1660 1661(* Hoped this would work with higher-order matching, but it didn't 1662val EXISTS_EL_MAP_LEMMA = 1663 prove 1664 (``!P l f. 1665 (?i. i < LENGTH l /\ ?s. P s (EL i (MAP f l))) = 1666 (?i. i < LENGTH l /\ ?s. P s (f(EL i l)))``, 1667 REPEAT GEN_TAC 1668 THEN EQ_TAC 1669 THEN ZAP_TAC list_ss [EL_MAP]); 1670*) 1671 1672val EXISTS_EL_MAP_LEMMA1 = 1673 prove 1674 (``((?i. 1675 i < LENGTH l /\ 1676 ?s. 1677 (EL i (MAP (\s. STATE (M.L (FST s))) l) = STATE s) /\ 1678 p IN s) /\ L_SEM (EL n (MAP (\s. STATE (M.L (FST s))) l)) p) = 1679 ((?i. 1680 i < LENGTH l /\ 1681 ?s. 1682 (s = M.L (FST(EL i l))) /\ 1683 p IN s) /\ L_SEM (EL n (MAP (\s. STATE (M.L (FST s))) l)) p)``, 1684 EQ_TAC 1685 THEN RW_TAC list_ss [] 1686 THENL 1687 [IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1688 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L (FST s)))`) 1689 THEN PROVE_TAC[letter_11], 1690 IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1691 THEN Q.EXISTS_TAC `i` 1692 THEN RW_TAC list_ss []]); 1693 1694val EXISTS_EL_MAP_LEMMA2 = 1695 prove 1696 (``n < LENGTH l 1697 ==> 1698 (((?i. 1699 i < LENGTH l /\ 1700 ?s. 1701 (EL i (MAP (\s. STATE (M.L (FST s))) l) = STATE s) /\ 1702 p IN s) /\ L_SEM (EL n (MAP (\s. STATE (M.L (FST s))) l)) p) = 1703 p IN M.L (FST (EL n l)))``, 1704 RW_TAC list_ss [] 1705 THEN EQ_TAC 1706 THEN RW_TAC list_ss [] 1707 THENL 1708 [IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1709 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L (FST s)))`) 1710 THEN PROVE_TAC[letter_11,L_SEM_def], 1711 IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1712 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L (FST s)))`) 1713 THEN PROVE_TAC[letter_11,L_SEM_def], 1714 IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1715 THEN RW_TAC list_ss [L_SEM_def]]); 1716 1717val EXISTS_ELEM_MAP_PATH_LEMMA1 = 1718 prove 1719 (``((?i'. i' < LENGTH p /\ 1720 ?s. (ELEM (MAP_PATH (\s. STATE (M.L (FST s))) p) i' = STATE s) /\ p' IN s) 1721 /\ p' IN M.L (FST (ELEM p i))) = 1722 ((?i'. i' < LENGTH p /\ ?s. (s = M.L (FST(ELEM p i'))) /\ p' IN s) 1723 /\ p' IN M.L (FST (ELEM p i)))``, 1724 EQ_TAC 1725 THEN RW_TAC list_ss [] 1726 THENL 1727 [IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]ELEM_MAP_PATH) 1728 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L (FST s)))`) 1729 THEN PROVE_TAC[letter_11], 1730 IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]ELEM_MAP_PATH) 1731 THEN Q.EXISTS_TAC `i'` 1732 THEN RW_TAC list_ss []]); 1733 1734val EXISTS_ELEM_MAP_PATH_LEMMA2 = 1735 prove 1736 (``(s < LENGTH v /\ 1737 (?i'. 1738 i' < LENGTH v /\ 1739 ?s. 1740 (ELEM (MAP_PATH (\s. STATE (M.L s)) v) i' = STATE s) /\ 1741 p IN s) /\ 1742 L_SEM (ELEM (MAP_PATH (\s. STATE (M.L s)) v) s) p) = 1743 s < LENGTH v /\ 1744 (?i'. i' < LENGTH v /\ ?s. (s = M.L (ELEM v i')) /\ p IN s) /\ 1745 p IN M.L (ELEM v s)``, 1746 EQ_TAC 1747 THEN RW_TAC list_ss [] 1748 THEN IMP_RES_TAC(INST_TYPE[``:'b``|->``:'b letter``]ELEM_MAP_PATH) 1749 THENL 1750 [ASSUM_LIST 1751 (fn thl=> 1752 ASSUME_TAC(SIMP_RULE std_ss [](Q.SPEC `(\s. STATE (M.L s))` (el 2 thl)))) 1753 THEN PROVE_TAC[letter_11], 1754 POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L s))`) 1755 THEN PROVE_TAC[L_SEM_def], 1756 Q.EXISTS_TAC `i'` 1757 THEN RW_TAC list_ss [], 1758 RW_TAC list_ss [L_SEM_def]]); 1759 1760val EL_MAP_LEMMA = 1761 prove 1762 (``(s' < LENGTH l /\ (?i. i < LENGTH l /\ p IN M.L (FST (EL i l))) /\ 1763 L_SEM (EL s' (MAP (\s. STATE (M.L (FST s))) l)) p) = 1764 (s' < LENGTH l /\ p IN M.L (FST (EL s' l)))``, 1765 EQ_TAC 1766 THEN RW_TAC list_ss [] 1767 THENL 1768 [IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1769 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `(\s. STATE (M.L (FST s)))`) 1770 THEN PROVE_TAC[L_SEM_def], 1771 PROVE_TAC[], 1772 IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a # 'b``,``:'b``|->``:'c letter``]EL_MAP) 1773 THEN RW_TAC list_ss [L_SEM_def]]); 1774 1775val EXISTS_IN_LEMMA1 = 1776 prove 1777 (``((?i. p IN M.L (FST (f i))) /\ p IN M.L (FST (f s))) = 1778 p IN M.L (FST (f s))``, 1779 PROVE_TAC[]); 1780 1781val EXISTS_IN_LEMMA2 = 1782 prove 1783 (``n < LENGTH l 1784 ==> 1785 (((?i. i < LENGTH l /\ p IN M.L (FST (EL i l))) /\ 1786 p IN M.L (FST (EL n l))) = 1787 p IN M.L (FST (EL n l)))``, 1788 PROVE_TAC[]); 1789 1790val EXISTS_IN_LEMMA3 = 1791 prove 1792 (``i < LENGTH p 1793 ==> 1794 (((?i'. i' < LENGTH p /\ p' IN M.L (FST (ELEM p i'))) /\ 1795 p' IN M.L (FST (ELEM p i))) = 1796 p' IN M.L (FST (ELEM p i)))``, 1797 PROVE_TAC[]); 1798 1799val EXISTS_IN_LEMMA4 = 1800 prove 1801 (``(s < LENGTH v /\ 1802 (?i'. i' < LENGTH v /\ p IN M.L (ELEM v i')) /\ 1803 p IN M.L (ELEM v s)) = 1804 s < LENGTH v /\ p IN M.L (ELEM v s)``, 1805 PROVE_TAC[]); 1806 1807val LENGTH_GT_0 = 1808 store_thm 1809 ("LENGTH_GT_0", 1810 ``LENGTH l > 0 = ?x l'. l = x::l'``, 1811 Cases_on `l` 1812 THEN RW_TAC list_ss []); 1813 1814val MK_PATH_PROD_LEMMA = 1815 store_thm 1816 ("MK_PATH_PROD_LEMMA", 1817 ``PATH (M || A) (s,t) p /\ AUTOMATON A 1818 ==> 1819 PATH 1820 (PATH_TO_MODEL (MAP_PATH (\s. STATE (M.L (FST s))) p) || A) 1821 (0,t) 1822 (MK_PROD_PATH p)``, 1823 Cases_on `p` 1824 THEN RW_TAC list_ss 1825 [MK_PROD_PATH_def,PATH_TO_MODEL_def,ELEM_FINITE,ELEM_INFINITE, 1826 PATH_def,LENGTH_def,GT,LENGTH_MK_FINITE_PROD_PATH,LS] 1827 THEN RW_TAC (srw_ss()++resq_SS) 1828 [MODEL_AUTOMATON_PROD_def,LENGTH_MAP_PATH,LENGTH_def,LS,SUB] 1829 THEN RW_TAC list_ss 1830 [ELEM_MK_FINITE_PROD_PATH,AUTOMATON_Q0_Q,MAP_PATH_def, 1831 LETTER_IN_def,L_SEM_def,LENGTH_def,ELEM_FINITE,ELEM_INFINITE, 1832 LS,EXISTS_EL_MAP_LEMMA1] 1833 THEN TRY(`n < LENGTH l` by DECIDE_TAC) 1834 THEN RW_TAC list_ss 1835 [EL_MAP,L_SEM_def,EL_MAP_LEMMA,GSPEC_ID,EXISTS_EL_MAP_LEMMA2, 1836 EXISTS_IN_LEMMA1,EXISTS_IN_LEMMA2, 1837 PROVE[]``((~A \/ ~B) \/ ~C) \/ ~D \/ ~E \/ G = A ==> B ==> C ==> D ==> E ==> G``] 1838 THEN FULL_SIMP_TAC (srw_ss()++resq_SS) [IN_LESS,LS,SUB,LENGTH_GT_0] 1839 THEN RW_TAC list_ss [] 1840 THEN FULL_SIMP_TAC (list_ss ++ PRED_SET_ss) 1841 [MK_FINITE_PROD_PATH_def,PAIR_EQ_SPLIT, 1842 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).S``] 1843 THEN RW_TAC list_ss [ELEM_MK_FINITE_PROD_PATH,MK_INFINITE_PROD_PATH_def] 1844 THEN FULL_SIMP_TAC (list_ss ++ PRED_SET_ss) 1845 [SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).R``] 1846 THEN METIS_TAC[PAIR_EQ_SPLIT]); 1847 1848(*****************************************************************************) 1849(* |- forall v: (v |=ltl f) <=> (v || A |=ctl always b) *) 1850(* ------------------------------------------------------ *) 1851(* |- forall M: (M |=ltl f) <=> (M || A |=ctl always b) *) 1852(*****************************************************************************) 1853 1854val MODEL_INTRO_IMP1 = 1855 store_thm 1856 ("MODEL_INTRO_IMP1", 1857 ``TOTAL_AUTOMATON A 1858 ==> 1859 (!v. UF_SEM v f = O_VALID (PATH_TO_MODEL v || A) (O_AG(O_BOOL b))) 1860 ==> 1861 (UF_VALID M f ==> O_VALID (M || A) (O_AG(O_BOOL b)))``, 1862 SIMP_TAC (srw_ss()++resq_SS) 1863 [O_VALID_def,UF_VALID_def,O_SEM_O_AG] 1864 THEN RW_TAC (srw_ss()++resq_SS) 1865 [O_SEM_def,IN_LESS_LENGTH,LENGTH_MAP_PATH,IN_COMPUTATION, 1866 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).L``, 1867 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).S0``, 1868 SIMP_CONV (srw_ss()++resq_SS) [PATH_TO_MODEL_def] ``(PATH_TO_MODEL v).S0``, 1869 SIMP_CONV (srw_ss()++resq_SS) [PATH_TO_MODEL_def] ``(PATH_TO_MODEL v).L``] 1870 THEN RW_TAC std_ss [] 1871 THEN `(MAP_PATH FST p) IN PATH M s'` by PROVE_TAC[PROD_FST] 1872 THEN FULL_SIMP_TAC std_ss [IN_PATH] 1873 THEN ASSUM_LIST 1874 (fn thl => 1875 (ASSUME_TAC o GEN_ALL) 1876 (SIMP_RULE list_ss 1877 [el 1 thl,el 3 thl,el 4 thl,el 5 thl, 1878 MAP_PATH_MAP_PATH] 1879 ((SPEC_ALL o Q.SPECL [`s'`,`t`]) 1880 (SIMP_RULE list_ss 1881 [PROVE [] ``((?x. P x) ==> Q) = !x. P x ==> Q``, 1882 PROVE [] ``(!x. P x ==> !y. Q x y) = !x y. P x ==> Q x y``] 1883 (Q.SPEC `MAP_PATH FST (p :('c # 'b) path)` (el 6 thl)))))) 1884 THEN POP_ASSUM 1885 (ASSUME_TAC o 1886 SIMP_RULE list_ss 1887 [LENGTH_MAP_PATH,LENGTH_MK_PROD_PATH, 1888 ELEM_MK_PROD_PATH] o 1889 Q.SPEC `MK_PROD_PATH (p :('c # 'b) path)`) 1890 THEN FULL_SIMP_TAC std_ss [TOTAL_AUTOMATON_def] 1891 THEN ASSUM_LIST 1892 (fn thl => ASSUME_TAC(MATCH_MP MK_PATH_PROD_LEMMA (CONJ (el 4 thl) (el 10 thl)))) 1893 THEN ASSUM_LIST 1894 (fn thl => ASSUME_TAC(MATCH_MP (el 2 thl) (el 1 thl))) 1895 THEN ASSUM_LIST 1896 (fn thl => ASSUME_TAC(MATCH_MP (el 1 thl) (el 5 thl))) 1897 THEN ASSUM_LIST 1898 (fn thl => 1899 ASSUME_TAC 1900 (SIMP_RULE list_ss 1901 [el 6 thl,ELEM_MAP_PATH,L_SEM_def,LETTER_IN_def,GSPEC_ID, 1902 LENGTH_MAP_PATH,EXISTS_ELEM_MAP_PATH_LEMMA1,EXISTS_IN_LEMMA3] 1903 (el 1 thl))) 1904 THEN CONV_TAC(DEPTH_CONV GEN_BETA_CONV) 1905 THEN RW_TAC std_ss []); 1906 1907val EXISTS_ELEM_MAP_PATH_LEMMA3 = 1908 prove 1909 (``(?i. i < LENGTH v /\ 1910 ?s. (ELEM (MAP_PATH STATE v) i = STATE s) /\ p IN s) = 1911 ?i. i < LENGTH v /\ p IN (ELEM v i)``, 1912 EQ_TAC 1913 THEN RW_TAC list_ss [] 1914 THEN IMP_RES_TAC(INST_TYPE [``:'a``|->``:'a->bool``,``:'b``|->``:'a letter``]ELEM_MAP_PATH) 1915 THENL 1916 [POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `STATE`) 1917 THEN PROVE_TAC[letter_11], 1918 Q.EXISTS_TAC `i` 1919 THEN RW_TAC list_ss []]); 1920 1921val EXISTS_ELEM_MAP_PATH_LEMMA4 = 1922 prove 1923 (``(n < LENGTH v /\ 1924 (?i. i < LENGTH v /\ p IN (ELEM v i)) /\ 1925 L_SEM (ELEM (MAP_PATH STATE v) n) p) = 1926 n < LENGTH v /\ p IN (ELEM v n)``, 1927 EQ_TAC 1928 THEN RW_TAC list_ss [] 1929 THEN IMP_RES_TAC(INST_TYPE [``:'a``|->``:'a->bool``,``:'b``|->``:'a letter``]ELEM_MAP_PATH) 1930 THEN RW_TAC list_ss [L_SEM_def] 1931 THENL 1932 [POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPEC `STATE`) 1933 THEN PROVE_TAC[letter_11,L_SEM_def], 1934 PROVE_TAC[]]); 1935 1936val PATH_TO_MODEL_COMPUTATION_TO_MODEL = 1937 store_thm 1938 ("PATH_TO_MODEL_COMPUTATION_TO_MODEL", 1939 ``PATH_TO_MODEL (MAP_PATH STATE v) = COMPUTATION_TO_MODEL v``, 1940 RW_TAC list_ss 1941 [PATH_TO_MODEL_def,COMPUTATION_TO_MODEL_def,LENGTH_MAP_PATH,LETTER_IN_def, 1942 EXISTS_ELEM_MAP_PATH_LEMMA2, 1943 EXISTS_ELEM_MAP_PATH_LEMMA3,EXISTS_ELEM_MAP_PATH_LEMMA4]); 1944 1945val PATH_TO_MODEL_COMPUTATION_TO_MODEL_COR = 1946 store_thm 1947 ("PATH_TO_MODEL_COMPUTATION_TO_MODEL_COR", 1948 ``PATH_TO_MODEL (MAP_PATH (\s. STATE (M.L s)) v) = 1949 COMPUTATION_TO_MODEL(MAP_PATH M.L v)``, 1950 RW_TAC list_ss 1951 [GSYM PATH_TO_MODEL_COMPUTATION_TO_MODEL,MAP_PATH_MAP_PATH]); 1952 1953val PATH_TO_MODEL_PROD_S0 = 1954 store_thm 1955 ("PATH_TO_MODEL_PROD_S0", 1956 ``(s,q) IN (PATH_TO_MODEL v || A).S0 = (s = 0) /\ q IN A.Q0``, 1957 ACCEPT_TAC 1958 (SIMP_CONV (srw_ss()++resq_SS) 1959 [MODEL_AUTOMATON_PROD_def, 1960 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK,PATH_TO_MODEL_def] 1961 ``(s,q) IN (PATH_TO_MODEL v || A).S0``)); 1962 1963val COMPUTATION_TO_MODEL_PROD_S0 = 1964 store_thm 1965 ("COMPUTATION_TO_MODEL_PROD_S0", 1966 ``(s,q) IN (COMPUTATION_TO_MODEL v || A).S0 = (s = 0) /\ q IN A.Q0``, 1967 RW_TAC list_ss 1968 [GSYM PATH_TO_MODEL_COMPUTATION_TO_MODEL,PATH_TO_MODEL_PROD_S0]); 1969 1970val LE_LS_SUB1_MONO = 1971 store_thm 1972 ("LE_LS_SUB1_MONO", 1973 ``(x:xnum) <= (y:xnum) ==> (n:num) < x - 1 ==> n < y - 1``, 1974 Cases_on `x` THEN Cases_on `y` 1975 THEN RW_TAC arith_ss [LS,LE,SUB]); 1976 1977val PATH_COMPUTATION_PROD = 1978 store_thm 1979 ("PATH_COMPUTATION_PROD", 1980 ``s IN M.S0 /\ t IN A.Q0 /\ PATH M s v /\ MODEL M /\ AUTOMATON A /\ 1981 PATH (COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A) (0,t) p /\ 1982 (IS_FINITE p ==> LENGTH p < LENGTH v) 1983 ==> 1984 PATH (M || A) (s,t) (MAP_PATH (\(n,q). (ELEM v n,q)) p)``, 1985 RW_TAC list_ss [] 1986 THEN `p IN COMPUTATION(COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A)` 1987 by PROVE_TAC[COMPUTATION_def,COMPUTATION_TO_MODEL_PROD_S0,IN_COMPUTATION] 1988 THEN ASSUM_LIST 1989 (fn thl => 1990 ASSUME_TAC(SIMP_RULE list_ss [el 4 thl,COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR2] (el 1 thl))) 1991 THEN RW_TAC (srw_ss()++resq_SS) 1992 [MODEL_AUTOMATON_PROD_def, 1993 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK,PATH_TO_MODEL_def,LENGTH_MAP_PATH] 1994 THEN TRY(`0 < LENGTH p` by PROVE_TAC[GT_LS]) 1995 THEN RW_TAC list_ss [ELEM_MAP_PATH] 1996 THEN GEN_BETA_TAC 1997 THEN RW_TAC list_ss [] 1998 THENL 1999 [METIS_TAC[PATH_def], 2000 METIS_TAC[PATH_def,SND], 2001 METIS_TAC[MODEL_def,SUBSET_DEF], 2002 METIS_TAC[AUTOMATON_def,SUBSET_DEF], 2003 IMP_RES_TAC LS_SUB1 2004 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2005 THEN GEN_BETA_TAC 2006 THEN RW_TAC list_ss [PAIR_EQ] 2007 THEN METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2008 IMP_RES_TAC LS_SUB1_SUC 2009 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2010 THEN GEN_BETA_TAC 2011 THEN RW_TAC list_ss [PAIR_EQ] 2012 THENL 2013 [METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2014 METIS_TAC[AUTOMATON_def]], 2015 IMP_RES_TAC LS_SUB1 2016 THEN IMP_RES_TAC LS_SUB1_SUC 2017 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2018 THEN GEN_BETA_TAC 2019 THEN RW_TAC list_ss [PAIR_EQ] 2020 THENL 2021 [METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2022 METIS_TAC[AUTOMATON_def,ELEM_MAP_PATH,LS_LE_TRANS_X]], 2023 REWRITE_TAC[PROVE[]``(~A \/ ~B \/ ~C) \/ ~D \/ E = A ==> B ==> C ==> D ==> E``,EQ_PAIR] 2024 THEN RW_TAC list_ss [] 2025 THEN `EL (LENGTH l - 1) l = LAST l` by METIS_TAC[LENGTH_LAST,GT,LENGTH_MAP_PATH,LENGTH_def] 2026 THEN RW_TAC list_ss [] 2027 THEN Cases_on`p` 2028 THEN FULL_SIMP_TAC list_ss 2029 [path_11,path_distinct,MAP_PATH_def,LENGTH_def,LS,LE,GT,ELEM_FINITE,SUB,IS_FINITE_def] 2030 THEN `LENGTH l' = LENGTH l` by PROVE_TAC[LENGTH_MAP] 2031 THEN `LENGTH l' - 1 < LENGTH l'` by DECIDE_TAC 2032 THEN `FST(LAST l') = LENGTH l' - 1` by PROVE_TAC[LENGTH_LAST,DECIDE``m:num < n:num = n > m``] 2033 THEN `SUC(FST(LAST l')) = LENGTH l'` by DECIDE_TAC 2034 THEN `XNUM(SUC(FST(LAST l'))) < LENGTH v` by METIS_TAC[] 2035 THEN FULL_SIMP_TAC list_ss [XNUM_LS] 2036 THEN RES_TAC 2037 THEN `FST(LAST l') < LENGTH v` by METIS_TAC[DECIDE``n < SUC n``,LS_TRANS_X] 2038 THEN `ELEM (MAP_PATH M.L v) (FST (LAST l')) = M.L(ELEM v (FST (LAST l')))` 2039 by PROVE_TAC[ELEM_MAP_PATH] 2040 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th]) 2041 THEN `LENGTH l' - 1 < LENGTH l'` by DECIDE_TAC 2042 THEN `LAST l = (\(n,q). (ELEM v n,q)) (EL (LENGTH l' - 1) l')` 2043 by PROVE_TAC[EL_MAP] 2044 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE list_ss [PAIR_EQ_SPLIT] o GEN_BETA_RULE) 2045 THEN `LENGTH l' > 0` by DECIDE_TAC 2046 THEN `EL (LENGTH l' - 1) l' = LAST l'` by PROVE_TAC[LENGTH_LAST] 2047 THEN PROVE_TAC[]]); 2048 2049val PATH_COMPUTATION_PROD_TOTAL = 2050 store_thm 2051 ("PATH_COMPUTATION_PROD_TOTAL", 2052 ``s IN M.S0 /\ t IN A.Q0 /\ PATH M s v /\ MODEL M /\ TOTAL_AUTOMATON A /\ 2053 PATH (COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A) (0,t) p 2054 ==> 2055 PATH (M || A) (s,t) (MAP_PATH (\(n,q). (ELEM v n,q)) p)``, 2056 RW_TAC list_ss [] 2057 THEN `p IN COMPUTATION(COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A)` 2058 by PROVE_TAC[COMPUTATION_def,COMPUTATION_TO_MODEL_PROD_S0,IN_COMPUTATION] 2059 THEN ASSUM_LIST 2060 (fn thl => 2061 ASSUME_TAC(SIMP_RULE list_ss [el 3 thl,COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR3] (el 1 thl))) 2062 THEN RW_TAC (srw_ss()++resq_SS) 2063 [MODEL_AUTOMATON_PROD_def, 2064 PATH_def,IN_LESS_LENGTH_SUB1,ELEM_FINITE,SUBSET_SINK,PATH_TO_MODEL_def,LENGTH_MAP_PATH] 2065 THEN TRY(`0 < LENGTH p` by PROVE_TAC[GT_LS]) 2066 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2067 THEN GEN_BETA_TAC 2068 THEN RW_TAC list_ss [] 2069 THENL 2070 [METIS_TAC[PATH_def], 2071 METIS_TAC[PATH_def], 2072 METIS_TAC[PATH_def,SND], 2073 METIS_TAC[MODEL_def,SUBSET_DEF], 2074 METIS_TAC[TOTAL_AUTOMATON_def,AUTOMATON_def,SUBSET_DEF], 2075 IMP_RES_TAC LS_SUB1 2076 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2077 THEN GEN_BETA_TAC 2078 THEN RW_TAC list_ss [PAIR_EQ] 2079 THEN METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2080 IMP_RES_TAC LS_SUB1_SUC 2081 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2082 THEN GEN_BETA_TAC 2083 THEN RW_TAC list_ss [PAIR_EQ] 2084 THENL 2085 [METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2086 METIS_TAC[TOTAL_AUTOMATON_def,AUTOMATON_def]], 2087 IMP_RES_TAC LS_SUB1 2088 THEN IMP_RES_TAC LS_SUB1_SUC 2089 THEN RW_TAC list_ss [ELEM_MAP_PATH] 2090 THEN GEN_BETA_TAC 2091 THEN RW_TAC list_ss [PAIR_EQ] 2092 THENL 2093 [METIS_TAC[LE_LS_SUB1_MONO,SIMP_RULE (srw_ss()++resq_SS) [IN_LESS_LENGTH_SUB1] PATH_def], 2094 METIS_TAC[TOTAL_AUTOMATON_def,AUTOMATON_def,ELEM_MAP_PATH,LS_LE_TRANS_X]], 2095 REWRITE_TAC[PROVE[]``(~A \/ ~B \/ ~C) \/ ~D \/ E = A ==> B ==> C ==> D ==> E``,EQ_PAIR] 2096 THEN RW_TAC list_ss [] 2097 THEN `EL (LENGTH l - 1) l = LAST l` by METIS_TAC[LENGTH_LAST,GT,LENGTH_MAP_PATH,LENGTH_def] 2098 THEN RW_TAC list_ss [] 2099 2100 THEN Cases_on`v` 2101 THEN FULL_SIMP_TAC list_ss [path_11,path_distinct,MAP_PATH_def,LENGTH_def,LS,LE,GT,ELEM_FINITE,SUB] 2102 THENL 2103 [ASSUM_LIST 2104 (fn thl => 2105 ASSUME_TAC(SIMP_RULE list_ss [PATH_def,path_11,ELEM_FINITE](el 17 thl))) 2106 THEN `~((EL (LENGTH l' - 1) l',s'') IN M.R)` by PROVE_TAC[] 2107 THEN Cases_on`p` 2108 THEN FULL_SIMP_TAC list_ss [path_11,path_distinct,MAP_PATH_def,LENGTH_def,LS,LE,GT,ELEM_FINITE,SUB,xnum_11] 2109 THEN `LENGTH l'' - 1 < LENGTH l''` by DECIDE_TAC 2110 THEN `EL (LENGTH l'' - 1) (MAP (\(n,q). (EL n l',q)) l'') = 2111 (\(n,q). (EL n l',q))(EL (LENGTH l'' - 1) l'')` 2112 by METIS_TAC[EL_MAP] 2113 THEN `LENGTH l'' = LENGTH l` by PROVE_TAC[LENGTH_MAP] 2114 THEN ASSUM_LIST 2115 (fn thl => 2116 ASSUME_TAC(SIMP_RULE list_ss [el 1 thl, el 10 thl, el 21 thl](GEN_BETA_RULE(el 2 thl)))) 2117 THEN `FST(LAST l) = EL (FST (EL (LENGTH l - 1) l'')) l'` by PROVE_TAC[FST] 2118 THEN `LENGTH l - 1 < LENGTH l''` by DECIDE_TAC 2119 THEN METIS_TAC[LENGTH_LAST], 2120 Cases_on`p` 2121 THEN FULL_SIMP_TAC list_ss [ELEM_INFINITE,MAP_PATH_def,path_distinct,LENGTH_def,xnum_distinct]]]); 2122 2123val MODEL_INTRO_IMP2 = 2124 store_thm 2125 ("MODEL_INTRO_IMP2", 2126 ``TOTAL_AUTOMATON A /\ MODEL M 2127 ==> 2128 (!v. UF_SEM v f = O_VALID (PATH_TO_MODEL v || A) (O_AG(O_BOOL b))) 2129 ==> 2130 (O_VALID (M || A) (O_AG(O_BOOL b)) ==> UF_VALID M f)``, 2131 SIMP_TAC (srw_ss()++resq_SS) 2132 [O_VALID_def,UF_VALID_def,O_SEM_O_AG] 2133 THEN RW_TAC (srw_ss()++resq_SS) 2134 [O_SEM_def,IN_LESS_LENGTH,LENGTH_MAP_PATH,IN_COMPUTATION,LETTER_IN_def, 2135 EXISTS_ELEM_MAP_PATH_LEMMA2,EXISTS_IN_LEMMA4, 2136 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).L``, 2137 SIMP_CONV (srw_ss()++resq_SS) [MODEL_AUTOMATON_PROD_def] ``(M || A).S0``, 2138 SIMP_CONV (srw_ss()++resq_SS) [PATH_TO_MODEL_def] ``(PATH_TO_MODEL v).S0``, 2139 SIMP_CONV (srw_ss()++resq_SS) [PATH_TO_MODEL_def] ``(PATH_TO_MODEL v).L``] 2140 THEN GEN_BETA_TAC 2141 THEN ASSUM_LIST 2142 (fn thl => 2143 ASSUME_TAC 2144 (GEN_BETA_RULE 2145 (SIMP_RULE std_ss 2146 [el 3 thl,el 5 thl, 2147 PROVE[]``(!p. P p ==> !i. Q i p) = !p i. P p ==> Q i p``] 2148 (Q.SPEC `(s,t)` (el 6 thl))))) 2149 THEN ASSUM_LIST 2150 (fn thl => 2151 ASSUME_TAC 2152 (SIMP_RULE list_ss [LENGTH_MAP_PATH,el 2 thl] 2153 (Q.SPECL 2154 [`MAP_PATH (\(n,q). (ELEM v n, q)) p`,`i`] 2155 (el 1 thl)))) 2156 THEN FULL_SIMP_TAC list_ss [IN_PATH] 2157 THEN `p IN COMPUTATION(PATH_TO_MODEL (MAP_PATH (\s. STATE (M.L s)) v) || A)` 2158 by PROVE_TAC[PATH_TO_MODEL_PROD_S0,COMPUTATION_def,IN_COMPUTATION] 2159 THEN FULL_SIMP_TAC list_ss [PATH_TO_MODEL_COMPUTATION_TO_MODEL_COR] 2160 THEN `(FST (ELEM p i) = i) /\ i < LENGTH v` 2161 by METIS_TAC 2162 [COMPUTATION_COMPUTATION_MODEL_AUTOMATON_COR3, 2163 TOTAL_AUTOMATON_def,LENGTH_MAP_PATH,LS_LE_TRANS_X] 2164 THEN RW_TAC list_ss [GSPEC_ID] 2165 THEN IMP_RES_TAC(ISPECL 2166 [``p:(num # 'b) path``,``i:num``, 2167 ``\((n :num),(q :'b)). (ELEM (v :'c path) n,q)``] 2168 (GEN_ALL ELEM_MAP_PATH)) 2169 THEN ASSUM_LIST 2170 (fn thl => 2171 ASSUME_TAC 2172 (SIMP_RULE list_ss [el 3 thl] 2173 (GEN_BETA_RULE(SIMP_RULE list_ss [el 1 thl] (el 5 thl))))) 2174 THEN METIS_TAC[PATH_COMPUTATION_PROD_TOTAL]); 2175 2176 2177val MODEL_INTRO = 2178 store_thm 2179 ("MODEL_INTRO", 2180 ``MODEL M /\ TOTAL_AUTOMATON A 2181 ==> 2182 (!v. UF_SEM v f = O_VALID (PATH_TO_MODEL v || A) (O_AG(O_BOOL b))) 2183 ==> 2184 (UF_VALID M f = O_VALID (M || A) (O_AG(O_BOOL b)))``, 2185 PROVE_TAC[MODEL_INTRO_IMP1,MODEL_INTRO_IMP2]); 2186 2187val _ = export_theory(); 2188