1(* ===================================================================== *) 2(* FILE : STEScript.sml *) 3(* DESCRIPTION : STE Embedding in HOL *) 4(* AUTHOR : Ashish Darbari *) 5(* ===================================================================== *) 6(* 7(* For interactive running uncomment this part *) 8 val _ = load "stringLib"; 9 val _ = load "mesonLib"; 10 *) 11 12local 13open boolLib Parse bossLib HolKernel; 14open arithmeticTheory stringLib; 15open listTheory mesonLib pairTheory; 16 17in 18 19(* Creating a new theory that will be called STE *) 20 21val _ = new_theory "STE"; 22val _ = ParseExtras.temp_loose_equality() 23infix THEN THENL; 24 25(* Creating abbreviations for FULL_SIMP_TAC and RW_TAC *) 26 27val fs = FULL_SIMP_TAC std_ss; 28val fl = FULL_SIMP_TAC list_ss; 29val ARW_TAC = RW_TAC std_ss; 30 31(* Dual Rail Encoding of Lattice Values *) 32 33val Top_def = Define `Top = (F, F)`; 34val One_def = Define `One = (T, F)`; 35val Zero_def = Define `Zero = (F, T)`; 36val X_def = Define `X = (T, T)`; 37 38(* Definition of least upper bound *) 39val _ = set_fixity "lub" (Infixl 510); 40val lub_def = Define `(a, b) lub (c, d) = (a /\ c, b /\ d)`; 41 42 43(* Definition of lub on states *) 44 45val lub_state_def = Define `lub_state state1 state2 node = 46 (state1 node) lub (state2 node)`; 47 48(* Defintion of ordering *) 49 (* --- 50 | 51 --- 52 --- *) 53 54val _ = set_fixity "leq" (Infixl 510); 55val leq_def = Define `(a leq b = (b = a lub b))`; 56 57(* Ordering lifted over states *) 58 59val _ = set_fixity "leq_state" (Infixl 510); 60val leq_state_def = Define `state1 leq_state state2 61 = !node:string. (state1 node) leq (state2 node)`; 62 63(* Ordering lifted over sequences *) 64 65val _ = set_fixity "leq_seq" (Infixl 510); 66val leq_seq_def = Define `sigma1 leq_seq sigma2 67 = !node:string t:num. (sigma1 t node) leq (sigma2 t node)`; 68 69(* Definition of suffix *) 70 71val Suffix_def = Define 72 `Suffix i (sigma: num->string->(bool # bool)) 73 = \t node.(sigma (t+i) node)`; 74 75 76(* Dropping from Boolean to Lattice Values *) 77 78val drop_def = Define `(drop T = One) /\ (drop F = Zero)`; 79 80(* Drop operation lifted over states *) 81 82val extended_drop_state_def = Define 83 `extended_drop_state (s_b:string->bool) = \node. drop (s_b node)`; 84 85 86(* Drop operation lifted over sequences *) 87 88val extended_drop_seq_def = Define 89 `extended_drop_seq (sigma_b:num->string->bool) = \t. 90 (extended_drop_state (sigma_b t))`; 91 92(* Next state function is monotonic *) 93 94val Monotonic_def = Define `Monotonic Y_ckt = 95 !s s'. 96 s leq_state s' ==> 97 (Y_ckt s) leq_state (Y_ckt s')`; 98 99 100(* Sequence is in the STE language of a circuit *) 101 102val in_STE_lang_def = Define ` 103 in_STE_lang sigma Y_ckt = 104 !t. (Y_ckt (sigma t)) leq_state (sigma (t+1))`; 105 106 107(* Defining the abstract type of Trajectory formulas *) 108 109val _ = Hol_datatype 110 `TF = Is_0 of string 111 | Is_1 of string 112 | AND of TF => TF 113 | WHEN of TF => bool 114 | NEXT of TF`; 115 116(* Defining the operators WHEN and AND to be left infix *) 117 118val _ = set_fixity "WHEN" (Infixl 500); 119val _ = set_fixity "AND" (Infixl 510); 120 121(* Semantics of trajectory formula - defined wrt a sequence *) 122 123val SAT_STE_def = Define `(SAT_STE (Is_0 n) = \sigma. 124 Zero leq (sigma 0 n)) 125 126 /\ (SAT_STE (Is_1 n) = \sigma. 127 One leq (sigma 0 n)) 128 129 /\ (SAT_STE (tf1 AND tf2) = \sigma. 130 ((SAT_STE tf1 sigma) /\ (SAT_STE tf2 sigma))) 131 132 /\ (SAT_STE (tf WHEN (P:bool)) = \sigma. 133 (P ==> (SAT_STE tf sigma))) 134 135 /\ (SAT_STE (NEXT tf) = \sigma. 136 (SAT_STE tf (Suffix 1 sigma)))`; 137 138(* Datatype of Assertions - leadsto operator *) 139 140val _ = Hol_datatype `Assertion = ==>> of TF => TF`; 141 142(* leadsto is infix *) 143 144val _ = set_fixity "==>>" (Infixl 470); 145 146 147(* Defining Sequence of a trajectory formula *) 148 149val DefSeq_def = Define `(DefSeq (Is_0 m) = \t n. 150 (if ((n = m) /\ (t = 0)) then Zero else X)) 151 152 /\ (DefSeq (Is_1 m) = \t n. 153 (if ((n = m) /\ (t = 0)) then One else X)) 154 155 /\ (DefSeq (tf1 AND tf2) = \t n. 156 ((DefSeq tf1 t n) lub (DefSeq tf2 t n))) 157 158 /\ (DefSeq (tf WHEN (P:bool)) = \t n. 159 (P ==> FST(DefSeq tf t n), P ==> SND(DefSeq tf t n))) 160 161 /\ (DefSeq (NEXT tf) = \t n. 162 (if ~(t = 0) then (DefSeq tf (t-1) n) else X))`; 163 164 165(* Collecting the nodes in the trajectory formula *) 166 167val Nodes_def = Define `(Nodes (Is_0 n) Acc = 168 if MEM n Acc then Acc else (n::Acc)) 169 /\ (Nodes (Is_1 n) Acc = if MEM n Acc then Acc else (n::Acc)) 170 /\ (Nodes (tf1 AND tf2) Acc = Nodes tf2 (Nodes tf1 Acc)) 171 /\ (Nodes (tf WHEN P) Acc = Nodes tf Acc) 172 /\ (Nodes (NEXT tf) Acc = Nodes tf Acc)`; 173 174 175(* Useful properties about node membership *) 176 177val MEM_NODES1 = store_thm("MEM_NODES1",``!tf acc node. 178 MEM node (Nodes tf []) \/ MEM node acc = 179 MEM node (Nodes tf acc)``, 180 Induct THEN 181 fl [Nodes_def] 182 THEN REPEAT STRIP_TAC 183 THEN REPEAT COND_CASES_TAC 184 THEN fl [] THEN PROVE_TAC []); 185 186 187 188val MEM_NODES2 = store_thm("MEM_NODES2", ``!tf tf'. 189 ~MEM node (Nodes tf' (Nodes tf [])) = 190 ~MEM node (Nodes tf []) 191 /\ ~MEM node (Nodes tf' [])``, 192 PROVE_TAC [MEM_NODES1]); 193 194 195val MAX_def = Define `MAX t1 t2 = (if t1 >= t2 then t1 else t2)`;; 196 197(* Depth of a trajectory formula *) 198 199val Depth_def = Define `(Depth (Is_0 n) = 0) 200 /\ (Depth (Is_1 n) = 0) 201 /\ (Depth (tf1 AND tf2) = MAX (Depth tf1)(Depth tf2)) 202 /\ (Depth (tf WHEN P) = Depth tf) 203 /\ (Depth (NEXT tf) = SUC (Depth tf))`; 204 205 206(* Defining Trajectory *) 207 208val DefTraj_def = Define `(DefTraj tf Model 0 node = DefSeq tf 0 node) 209 /\ (DefTraj tf Model (SUC t) node 210 = (DefSeq tf (SUC t) node) lub (Model (DefTraj tf Model t) node))`; 211 212(* The STE implementation *) 213 214val STE_Impl_def = Define `STE_Impl (Ant ==>> Cons) Y_ckt = 215 !t. (t <= Depth Cons ==> 216 !n. MEM n 217 (APPEND(Nodes Ant [])(Nodes Cons [])) ==> 218 (DefSeq Cons t n) leq (DefTraj Ant Y_ckt t n))`; 219 220(* Satisfiability of a Trajectory Assertion *) 221 222val SAT_CKT_def = Define `SAT_CKT (Ant ==>> Cons) Y_ckt 223 = !sigma. (in_STE_lang sigma Y_ckt ) 224 ==> (SAT_STE Ant sigma) 225 ==> (SAT_STE Cons sigma)`; 226 227(* Boolean valued world starts here *) 228 229(* Definition of suffix of a Boolean valued sequence *) 230 231val Suffix_b_def = Define 232 `Suffix_b i (sigma_b:num->string->bool) 233 = \t node.(sigma_b (t+i) node)`; 234 235(* Boolean Valued Sequence is in the relational model of a circuit *) 236 237val in_BOOL_lang_def = Define ` 238 in_BOOL_lang (sigma_b:num->string->bool) Yb_ckt 239 = !t. Yb_ckt (sigma_b t) (sigma_b (t+1))`; 240 241(* Boolean sequence satisfies a trajectory formula *) 242 243val SAT_BOOL_def = Define `(SAT_BOOL (Is_0 n) = \sigma_b. 244 ((sigma_b 0 n) = F)) 245 246 /\ (SAT_BOOL (Is_1 n) = \sigma_b. 247 ((sigma_b 0 n) = T)) 248 249 /\ (SAT_BOOL (tf1 AND tf2) = \sigma_b. 250 (SAT_BOOL tf1 sigma_b) /\ (SAT_BOOL tf2 sigma_b)) 251 252 /\ (SAT_BOOL (tf WHEN (P:bool)) = \sigma_b. 253 (P ==> (SAT_BOOL tf sigma_b))) 254 255 /\ (SAT_BOOL (NEXT(tf)) = \sigma_b. 256 (SAT_BOOL tf (Suffix_b 1 sigma_b)))`; 257 258 259 260(* Linking the lattice and the Boolean Models *) 261 262val Okay_def = Define `Okay (Y_ckt, Yb_ckt) = 263 !s_b:string->bool s_b':string->bool. 264 (Yb_ckt s_b s_b') ==> ((Y_ckt (extended_drop_state s_b)) leq_state 265 (extended_drop_state s_b'))`; 266 267 (* Lemmas and Theorems *) 268 269 270(* Here is the Big Picture *) 271(* 272-----------Top Level Picture : BridgeTheorem --------------------------------- 273 274 A ==>> C Y Yb 275 | | | 276 | | | 277 \|/ \|/ \|/ 278 | | | 279 | | | 280 --STE--------------------------- 281 | | 282 | - its Okay to relate Y and Yb | --- BOOLEAN ---- 283 | - Y is Monotonic | ---> | | 284 | | | Theorem in HOL | 285 | - run STE simulator to see if | | | 286 | | ---------------- 287 | - Y satisfies A ==>> C | 288 | | 289 ------------------------------- 290 291BridgeTheorem: 292|- !Ant Cons Y_ckt Yb_ckt. 293 Okay (Y_ckt, Yb_ckt) ==> 294 Monotonic Y_ckt 295 ==> 296 ( 297 298 (!t. 299 t <= Depth Cons ==> 300 !n. 301 MEM n (Nodes Ant APPEND Nodes Cons) ==> 302 leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n)) 303 304 ==> 305 ( 306 !sigma_b. 307 in_BOOL_lang sigma_b Yb_ckt ==> 308 !t. 309 SAT_BOOL Ant (Suffix_b t sigma_b) ==> 310 SAT_BOOL Cons (Suffix_b t sigma_b)) 311 ) : thm 312 313Proof of BridgeTheorem: 314 315 Relies on proving SAT_CKT_IFF_STE_IMPL and Theorem2 316------------------------------------------------------------------------------ 317 318 319---------------SAT_CKT_IFF_STE_IMPL-------------------------------------------- 320 321 322 A ==>> C Y 323 | | 324 | | 325 \|/ \|/ 326 | | 327 | | 328 ----------------------------------- 329 | | 330 | If Y is monotonic then | 331 | the jth suffix of the lattice | 332 | valued sequence satisfies the | 333 | STE assertion if and only if | 334 | the STE implementation (STE_Impl) | 335 | does. | 336 ----------------------------------- 337 338STE_Impl is defined as: 339 340|- !Ant Cons Y_ckt. 341 STE_Impl (Ant ==>> Cons) Y_ckt = 342 !t. 343 t <= Depth Cons ==> 344 !n. 345 MEM n (Nodes Ant APPEND Nodes Cons) ==> 346 leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n) : thm 347 348SAT_CKT_IFF_STE_IMPL: 349 350 |- !Ant Cons Y_ckt. 351 Monotonic Y_ckt ==> 352 ((!sigma. 353 in_STE_lang sigma Y_ckt ==> 354 !j. 355 SAT_STE Ant (Suffix j sigma) ==> 356 SAT_STE Cons (Suffix j sigma)) = 357 !t. 358 t <= Depth Cons ==> 359 !n. 360 MEM n (Nodes Ant APPEND Nodes Cons) ==> 361 leq (DefSeq Cons t n) (DefTraj Ant Y_ckt t n)) : thm 362 363 364Proof of SAT_CKT_IFF_STE_IMPL: 365 Relies on SAT_CKT_IFF_TIME_SHIFT theorem and 366 AuxTheorem1 (relies on Y being monotonic) 367 368------------------------------------------------------------------------------ 369 370-------------------Theorem2--------------------------------------------------- 371 372 373 ---------------------------------- 374 | If its Okay to relate Y and Yb, | 375 | and Y is monotonic | 376 | then if the lattice sequence | 377 | which is in the langauge of Y | 378 | satisfies the STE assertion, | 379 | the Boolean sequence which is | 380 | in the language of Yb also | 381 | satisfies the same STE assertion | 382 --------------------------------- 383 384 385Theorem2: 386 387|- !Ant Cons Y_ckt Yb_ckt. 388 Okay (Y_ckt,Yb_ckt) 389 ==> 390 (!sigma. 391 in_STE_lang sigma Y_ckt ==> 392 !t. 393 SAT_STE Ant (Suffix t sigma) ==> 394 SAT_STE Cons (Suffix t sigma)) ==> 395 !sigma_b. 396 in_BOOL_lang sigma_b Yb_ckt ==> 397 !t. 398 SAT_BOOL Ant (Suffix_b t sigma_b) ==> 399 SAT_BOOL Cons (Suffix_b t sigma_b) : thm 400 401Proof of Theorem2: 402 Relies on Lemma1, Lemma2 and Suffix_Lemma 403 404------------------------------------------------------------------------------ 405 406*) 407 408 409(* If its Okay to relate Y and Yb then for all Boolean valued 410 sequences which are in the language of the Boolean Model Yb, 411 the drop of the Boolean valued sequence is in the language 412 of the lattice model Y. 413 414 Lemma1 is used in the proof of Theorem2 415 416*) 417 418val Lemma1 = 419 store_thm ("Lemma1", 420 ``!Y_ckt Yb_ckt. Okay (Y_ckt, Yb_ckt) 421 ==> !sigma_b. 422 in_BOOL_lang sigma_b Yb_ckt 423 ==> in_STE_lang (extended_drop_seq sigma_b) Y_ckt``, 424 STRIP_TAC THEN fs [Okay_def, in_BOOL_lang_def, 425 in_STE_lang_def, 426 extended_drop_seq_def]); 427 428(* Calculating the Suffix after calculating the 429 drop of the Boolean valued sequence, results 430 in the sequence that one obtains by first calculating 431 the Suffix of the Boolean valued sequence and then 432 dropping it 433 434 Suffix_Lemma is used in the proof of Theorem2 435 436*) 437val Suffix_Lemma = TAC_PROOF(([], ``!t sigma_b. 438 (Suffix t (extended_drop_seq sigma_b)) = 439 (extended_drop_seq (Suffix_b t sigma_b))``), 440 441 (REPEAT STRIP_TAC 442 THEN Induct_on `t` 443 THEN fs [Suffix_def, Suffix_b_def, 444 extended_drop_seq_def, 445 extended_drop_state_def, drop_def]) 446 ); 447 448 449(* Lemma2_1 is used in the proof of Lemma 2 *) 450 451val Lemma2_1 = prove (``!tf sigma_b. SAT_BOOL tf sigma_b 452 ==> SAT_STE tf (extended_drop_seq sigma_b)``, 453 454 STRIP_TAC 455 THEN Induct_on `tf` 456 THEN fs [SAT_BOOL_def, SAT_STE_def] 457 THEN fs [extended_drop_seq_def, 458 extended_drop_state_def, 459 drop_def, leq_def, Zero_def, 460 lub_def] 461 THEN fs [extended_drop_seq_def, 462 extended_drop_state_def, 463 drop_def, leq_def, One_def, lub_def] 464 THEN fs [Suffix_def, Suffix_b_def, 465 extended_drop_seq_def, 466 extended_drop_state_def] 467 468 ); 469 470 471(* Lemma2_2 is used in the proof of Lemma 2 *) 472 473val Lemma2_2 = prove (``!tf sigma_b. SAT_STE tf (extended_drop_seq sigma_b) 474 ==> SAT_BOOL tf sigma_b``, 475 476 STRIP_TAC THEN Induct_on `tf` 477 THEN fs [SAT_STE_def, SAT_BOOL_def, 478 extended_drop_seq_def, 479 extended_drop_state_def, drop_def] 480 THEN REPEAT STRIP_TAC 481 THEN fs [Zero_def, One_def, drop_def, leq_def, lub_def] 482 483 484 THEN fs [SAT_STE_def, SAT_BOOL_def, 485 extended_drop_seq_def, 486 extended_drop_state_def, drop_def] 487 THEN REPEAT STRIP_TAC 488 THEN fs [Zero_def, One_def, drop_def, 489 leq_def, lub_def] 490 THEN Induct_on `sigma_b 0 s = T` 491 THEN fs [drop_def, lub_def, Zero_def, One_def] 492 THEN fs [SAT_STE_def, SAT_BOOL_def, 493 extended_drop_seq_def, extended_drop_state_def, 494 Suffix_def, Suffix_b_def] 495 ); 496 497(* Trajectory formula is satisfiable by a Boolean valued sequence 498 if and only if the trajectory formula is satisfiable by the 499 drop of the Boolean valued sequence 500 501*) 502 503val Lemma2 = prove (``!tf sigma_b. SAT_BOOL tf sigma_b = 504 SAT_STE tf (extended_drop_seq sigma_b)``, 505 506 REPEAT STRIP_TAC THEN EQ_TAC 507 THEN fs [Lemma2_1, Lemma2_2]); 508 509 510(* Properties of drop operation 511 An interesting property though these lemmas are not used anywhere 512*) 513 514 515val Lemma3_1 = prove(``!sigma_b:num->string->bool. 516 (sigma_b 0 node = F) 517 = (Zero leq ((extended_drop_seq sigma_b) 0 node))``, 518 519 STRIP_TAC THEN EQ_TAC 520 THEN fs [extended_drop_seq_def, extended_drop_state_def, 521 drop_def, leq_def, lub_def] 522 THEN fs [lub_def, Zero_def] 523 THEN fs [extended_drop_seq_def, extended_drop_state_def, 524 drop_def, leq_def, lub_def] 525 THEN STRIP_TAC 526 THEN Induct_on `sigma_b 0 node = T` 527 THEN fs [drop_def, lub_def, Zero_def, One_def] 528 THEN fs [drop_def, lub_def, Zero_def, One_def]); 529 530 531val Lemma3_2 = prove(``!sigma_b:num->string->bool. (sigma_b 0 node = T) 532 = (One leq ((extended_drop_seq sigma_b) 0 node))``, 533 534 STRIP_TAC THEN EQ_TAC 535 THEN fs [extended_drop_seq_def, extended_drop_state_def, 536 drop_def, leq_def, lub_def] 537 THEN fs [lub_def, Zero_def] 538 THEN fs [extended_drop_seq_def, extended_drop_state_def, 539 drop_def, leq_def, lub_def] 540 THEN STRIP_TAC 541 THEN Induct_on `sigma_b 0 node = T` 542 THEN fs [drop_def, lub_def, Zero_def, One_def] 543 THEN fs [drop_def, lub_def, Zero_def, One_def]); 544 545(* lattice_X1_lemma and lattice_X2_lemma state the same thing - 546 that the lub of any lattice value and X is that lattice value. 547 We have two versions they get used as and when they are needed 548 in the proofs of other lemmas 549 550 Used in the proof of DEFSEQ_LE_THAN_SAT_STE1 and AuxTheorem1 551 552*) 553 554val lattice_X1_lemma = store_thm ("lattice_X1_lemma", 555 ``!elem. elem = X lub elem``, 556 STRIP_TAC THEN Cases_on `elem` 557 THEN fs [lub_def, X_def]); 558 559val lattice_X2_lemma = TAC_PROOF(([], ``!elem. elem = (T, T) lub elem``), 560 STRIP_TAC THEN Cases_on `elem` 561 THEN fs [lub_def]); 562 563(* If a number is not zero, it must be either equal to 1 or greater than 1 564 565 Used in the proof of DEFSEQ_LE_THAN_SAT_STE1 566*) 567 568 569val NUM_LEMMA = TAC_PROOF(([], ``!t. ~(t = 0) ==> 1 <= t``), 570 Induct THEN DECIDE_TAC 571 ); 572 573(* Transitivity Lemma 574 Used in the proof of SEQ_LESS_THAN_SAT_STE and 575 DEFTRAJ_LESSTHAN_SEQ_IMP_SAT_STE_2 576 577*) 578val TRANS_LEMMA = 579 TAC_PROOF(([], ``!a c. (?b. a leq b /\ b leq c) ==> a leq c``), 580 REPEAT Cases THEN STRIP_TAC THEN Cases_on `b` THEN 581 fs [leq_def, lub_def] THEN PROVE_TAC[]);; 582 583 584 585(* A rather obvious but useful lemma that the 0th suffix of the sequence 586 gives the sequence itself *) 587 588val SUFFIX_0 = store_thm("SUFFIX_0", ``!sigma. Suffix 0 sigma = sigma``, 589 GEN_TAC THEN fs [Suffix_def] 590 THEN CONV_TAC(FUN_EQ_CONV) 591 THEN GEN_TAC 592 THEN Induct_on `n` THEN fs [] 593 THEN (CONV_TAC(FUN_EQ_CONV)) 594 THEN fs [] THEN (FULL_SIMP_TAC arith_ss []) 595 THEN (CONV_TAC(FUN_EQ_CONV)) THEN fs []); 596 597(* Suffix Closure Axiom: If a sequence is in the language of a lattice 598 circuit model then every suffix of that sequence is in the language 599 of the circuit model 600 601 Used in the proof of SEQ_LESS_THAN_SAT_STE 602*) 603 604(* Suffix closed -- Proposition *) 605val Proposition = 606 store_thm("Proposition", 607 ``!Y_ckt sigma. in_STE_lang sigma Y_ckt 608 ==> !t. in_STE_lang (Suffix t sigma) Y_ckt``, 609 STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC 610 THEN Induct THENL [PROVE_TAC [SUFFIX_0], 611 fs [in_STE_lang_def, Suffix_def] 612 THEN fl [leq_state_def, 613 leq_def] 614 THEN REPEAT STRIP_TAC 615 THEN FIRST_ASSUM 616 (STRIP_ASSUME_TAC 617 o SPECL [``t'+1``, 618 ``node:string``]) 619 THEN 620 FULL_SIMP_TAC bool_ss 621 [ONE, ADD_CLAUSES] 622 THEN RW_TAC std_ss [ADD_COMM] 623 THEN PROVE_TAC []]); 624 625 626 627 628(* Following up from Proposition above, clearly the first suffix is 629 in the language of the circuit model - useful to have this in the proofs 630 631 Used in the proof of DEFSEQ_LE_THAN_SAT_STE1, DEFSEQ_LE_THAN_SAT_STE2 632 and DEFSEQ_LE_THAN_SAT_STE 633 634 *) 635 636 637val Proposition1 = store_thm("Proposition1", 638 ``!Y_ckt sigma. in_STE_lang sigma Y_ckt 639 ==> !t. in_STE_lang (Suffix 1 sigma) Y_ckt``, 640 PROVE_TAC [Proposition]); 641 642 643(* If a sequence sigma is less than or equal to another sequence sigma' 644 then the ith suffix of sigma is less than or equal to the ith suffix 645 of sigma' *) 646 647val SUFFIX_SEQ_LESSTHAN = TAC_PROOF(([], ``!sigma sigma' i. 648 (!t n. (sigma t n) leq (sigma' t n)) 649 ==> !t n. ((Suffix i sigma) t n ) 650 leq ((Suffix i sigma') t n)``), 651 REPEAT STRIP_TAC 652 THEN (Induct_on `t`) 653 THEN (Induct_on `i`) 654 THEN fs [Suffix_def, leq_def] 655 THEN PROVE_TAC [] 656 THEN fs [Suffix_def, leq_def] 657 THEN PROVE_TAC [] 658 ); 659 660(* Lemmas about lub operation. Useful in other proofs *) 661 662val LUB_LEMMA1 = TAC_PROOF(([], ``!a. a = a lub a``), 663 REPEAT STRIP_TAC 664 THEN Cases_on `a` 665 THEN fs [lub_def]); 666 667val LUB_LEMMA2 = TAC_PROOF(([], ``!a b. a leq (a lub b)``), 668 (REPEAT Cases 669 THEN fs [leq_def, lub_def] THEN PROVE_TAC []) 670 ); 671 672val LUB_LEMMA3 = TAC_PROOF(([], ``!a b. a leq (b lub a)``), 673 (REPEAT Cases 674 THEN fs [leq_def, lub_def] THEN PROVE_TAC []) 675 ); 676 677val LUB_LEMMA4 = TAC_PROOF(([], ``!a b c. 678 a leq c ==> b leq c ==> (a lub b) leq c``), 679 (REPEAT Cases 680 THEN fs [leq_def, lub_def] 681 THEN PROVE_TAC [])); 682 683val LUB_LEMMA4a = TAC_PROOF(([], ``!a b c. 684 (a leq c /\ b leq c) ==> (a lub b) leq c``), 685 (REPEAT Cases 686 THEN fs [leq_def, lub_def] 687 THEN PROVE_TAC [])); 688 689val LUB_LEMMA5 = TAC_PROOF(([], ``!a b c. b leq c ==> 690 (a lub b) leq (a lub c)``), 691 REPEAT Cases THEN fs [leq_def, lub_def] 692 THEN PROVE_TAC [] 693 ); 694 695val LUB_LEMMA6 = TAC_PROOF (([], ``!a b c. (c = a lub b) 696 = (c = (FST a,SND a) lub b)``), 697 (REPEAT Cases THEN fs [FST, SND, 698 lub_def])); 699 700val LUB_LEMMA7a = TAC_PROOF(([], 701 ``!a b c. (a lub b) leq c ==> a leq c``), 702 REPEAT Cases THEN fs [leq_def, lub_def] 703 THEN PROVE_TAC [] 704 ); 705 706val LUB_LEMMA7b = TAC_PROOF(([], 707 ``!a b c. (a lub b) leq c ==> b leq c``), 708 REPEAT Cases THEN fs [leq_def, lub_def] 709 THEN PROVE_TAC [] 710 ); 711 712val LUB_LEMMA8 = TAC_PROOF(([], ``!a b. a lub b = b lub a``), 713 REPEAT Cases THEN fs [lub_def] THEN PROVE_TAC []); 714 715 716 717 718(* Defining Sequence for a given trajectory formula is less than or equal to 719 the defining trajectory for the formula at time point 0 - used in the proof 720 for any time t later *) 721 722val LEQ_DEFSEQ_DEFTRAJ_BASE = TAC_PROOF(([], ``!tf Y_ckt. 723 (DefSeq tf 0) leq_state 724 (DefTraj tf Y_ckt 0)``), 725 (REPEAT STRIP_TAC 726 THEN fs [leq_state_def, DefTraj_def] 727 THEN STRIP_TAC 728 THEN PROVE_TAC [leq_def, 729 LUB_LEMMA1]) 730 ); 731 732(* Defining Sequence for a given trajectory formula is less than or equal 733 to the defining trajectory for the same formula for a given circuit model 734 735 Used in the proof of SAT_CKT_IFF_STE1 736*) 737 738val LEQ_DEFSEQ_DEFTRAJ = TAC_PROOF(([], ``!tf Y_ckt t. 739 (DefSeq tf t) leq_state 740 (DefTraj tf Y_ckt t)``), 741 REPEAT STRIP_TAC THEN Induct_on `t` 742 THEN fs [LEQ_DEFSEQ_DEFTRAJ_BASE] 743 THEN fs [leq_state_def] THEN STRIP_TAC 744 THEN fs [DefTraj_def] THEN fs [LUB_LEMMA2] 745 ); 746 747 748 749(* If the circuit is monotonic then the defining trajectory for a given 750 trajectory formula wrt a given circuit model is in the langage of that 751 circuit model 752 753 Used in the proof of DEFTRAJ_LESSTHAN_SEQ_IMP_SAT_STE_1, 754 SAT_CKT_IFF_STE1, SAT_CKT_IFF_STE2 *) 755 756(* val DEFTRAJ_IN_STE_LANG = TAC_PROOF(([], ``!tf Y_ckt. Monotonic Y_ckt ==> *) 757(* in_STE_lang (DefTraj tf Y_ckt) Y_ckt``), *) 758 759(* (REPEAT STRIP_TAC THEN fs *) 760(* [in_STE_lang_def]) *) 761(* THEN (GEN_TAC THEN Induct_on `t`) *) 762(* THENL[ *) 763(* ((fs [DefTraj_def, leq_state_def]) *) 764(* THEN (GEN_TAC THEN fs [DefTraj_def]) *) 765(* THEN (fs [DefTraj_def, ONE]) *) 766(* THEN (fs [LUB_LEMMA3])), *) 767(* ((fs [leq_state_def]) *) 768(* THEN (GEN_TAC) *) 769(* THEN (fs [ONE, ADD, DefTraj_def]) *) 770(* THEN (fs [ADD_SYM, ADD]) *) 771(* THEN (fs [LUB_LEMMA3]))] *) 772(* ); *) 773 774val DEFTRAJ_IN_STE_LANG = TAC_PROOF(([], ``!tf Y_ckt. Monotonic Y_ckt 775 ==> 776 in_STE_lang (DefTraj tf Y_ckt) 777 Y_ckt``), 778 (REPEAT STRIP_TAC THEN fs 779 [in_STE_lang_def]) 780 THEN REWRITE_TAC [GSYM ADD1] 781 THEN Induct 782 THENL[ 783 ((fs [DefTraj_def, 784 leq_state_def]) 785 THEN (GEN_TAC THEN fs 786 [DefTraj_def]) 787 THEN (fs [DefTraj_def]) 788 THEN (fs [LUB_LEMMA3])), 789 ((fs [leq_state_def]) 790 THEN (GEN_TAC) 791 THEN (fs [ADD, DefTraj_def]) 792 THEN (fs [ADD_SYM, ADD]) 793 THEN (fs [LUB_LEMMA3]))] 794 ); 795 796 797(* If the circuit is monotonic and if two given sequences sigma and sigma' 798 are in the language of the circuit and if sigma is less than or equal 799 to sigma' then if sigma satisfies a trajectory formula then so does sigma' 800 *) 801 802val SEQ_LESS_THAN_SAT_STE = TAC_PROOF (([], ``!Y_ckt tf. !sigma sigma'. 803 Monotonic Y_ckt ==> 804 (in_STE_lang sigma Y_ckt) ==> 805 (in_STE_lang sigma' Y_ckt) 806 ==> (!t n. 807 (sigma t n) leq (sigma' t n)) 808 ==> (SAT_STE tf sigma ==> 809 SAT_STE tf sigma')``), 810 (GEN_TAC THEN Induct_on `tf` 811 THEN fs [SAT_STE_def] 812 THEN REPEAT STRIP_TAC THENL 813 [PROVE_TAC [TRANS_LEMMA], 814 PROVE_TAC [TRANS_LEMMA], 815 PROVE_TAC [TRANS_LEMMA], 816 PROVE_TAC [TRANS_LEMMA], 817 PROVE_TAC [TRANS_LEMMA], 818 ALL_TAC] 819 THEN 820 (STRIP_ASSUME_TAC Proposition 821 THEN RES_TAC) THEN 822 fs [SUFFIX_SEQ_LESSTHAN] 823 THEN 824 IMP_RES_TAC 825 (SPECL[``sigma:num->string->bool#bool`` 826 , ``sigma':num->string-> 827 bool#bool``, ``1``] 828 SUFFIX_SEQ_LESSTHAN) 829 THEN 830 FIRST_ASSUM (STRIP_ASSUME_TAC o 831 SPECL[``(Suffix 1 832 833 (sigma:num-> 834 string-> 835 bool#bool))``, 836 ``Suffix 1 837 (sigma':num-> 838 string-> 839 bool#bool)``]) 840 THEN fs [])); 841 842 843(* Specialized versions of LUB_LEMMA - useful in different proofs *) 844 845val SPEC_LUB_LEMMA1 = TAC_PROOF(([], ``!tf tf'. 846 (!t n. 847 ((DefSeq tf t n) lub (DefSeq tf' t n)) 848 leq (sigma t n)) ==> 849 !t n. (DefSeq tf t n) leq (sigma t n)``), 850 851 REPEAT STRIP_TAC THEN 852 Induct_on `t` 853 THENL[((FIRST_ASSUM(STRIP_ASSUME_TAC o 854 SPECL [``0:num``, 855 ``n:string``])) 856 THEN 857 (IMP_RES_TAC LUB_LEMMA7a)), 858 ((FIRST_ASSUM(STRIP_ASSUME_TAC o 859 SPECL [``SUC(t:num)``, 860 ``n:string``])) 861 THEN (IMP_RES_TAC LUB_LEMMA7a))] 862 ); 863 864val SPEC_LUB_LEMMA2 = TAC_PROOF(([], ``!tf tf'. 865 (!t n. ((DefSeq tf t n) lub 866 (DefSeq tf' t n)) leq (sigma t n)) ==> 867 !t n. (DefSeq tf' t n) leq (sigma t n)``), 868 869 REPEAT STRIP_TAC THEN 870 Induct_on `t` 871 THENL[((FIRST_ASSUM(STRIP_ASSUME_TAC o 872 SPECL [``0:num``, 873 ``n:string``])) 874 THEN 875 (IMP_RES_TAC LUB_LEMMA7b)), 876 ((FIRST_ASSUM(STRIP_ASSUME_TAC o 877 SPECL [``SUC(t:num)``, 878 ``n:string``])) 879 THEN (IMP_RES_TAC LUB_LEMMA7b))] 880 ); 881 882 883(* For all time points greater than zero, if DefSeq tf (t - 1) n returns a 884 value less than or equal to the lattice value returned by sigma, then the 885 DefSeq tf t n returns a value less than the first suffix of the sequence 886 sigma 887 *) 888 889val SPEC_NEXT_LEMMA = TAC_PROOF(([], ``!tf.(!t n. (if ~(t=0) 890 then 891 DefSeq tf (t -1) n 892 else X) leq (sigma t n)) 893 ==> (!t n. (DefSeq tf t n) leq 894 (Suffix 1 sigma t n))``), 895 Induct THEN 896 REPEAT STRIP_TAC 897 THEN fl [DefSeq_def, Suffix_def] THEN 898 FIRST_ASSUM(STRIP_ASSUME_TAC o 899 SPECL [``SUC t``, ``n:string``]) 900 THEN fl [] 901 THEN RW_TAC std_ss [SYM(SPEC_ALL ADD1)] 902 THEN fl [leq_def, lattice_X1_lemma] 903 THEN fl [lattice_X1_lemma] 904 THEN fl [ADD_CLAUSES, SUC_ONE_ADD] 905 THEN fl [] 906 ); 907 908 909(* If a lattice sequence sigma is in the language of a circuit model then 910 if sigma satisfies a given trajectory formula then the 911 Defining Sequence of the trajectory formula is less than or equal 912 to sigma *) 913 914val DEFSEQ_LE_THAN_SAT_STE1 = 915 TAC_PROOF(([], ``!tf. !sigma. in_STE_lang sigma Y_ckt ==> 916 (SAT_STE tf sigma ==> 917 !t. !n. (DefSeq tf t n) leq 918 (sigma t n)) ``), 919 920 GEN_TAC THEN Induct_on `tf` 921 THEN fs [SAT_STE_def, DefSeq_def] 922 THEN REPEAT STRIP_TAC 923 THENL 924 [(COND_CASES_TAC THEN fs [leq_def, 925 lub_def, 926 Zero_def] 927 THEN PROVE_TAC 928 [lattice_X1_lemma]), 929 (COND_CASES_TAC THEN fs [leq_def, 930 lub_def, 931 One_def] 932 THEN PROVE_TAC 933 [lattice_X1_lemma]), 934 (fs [LUB_LEMMA4]), 935 ((Cases_on `b`) THEN 936 (PROVE_TAC [lattice_X2_lemma, 937 leq_def, LUB_LEMMA6]) 938 THEN (PROVE_TAC [lattice_X2_lemma, 939 leq_def, 940 LUB_LEMMA6])), 941 ((COND_CASES_TAC) THEN (IMP_RES_TAC 942 Proposition1) 943 THEN (RES_TAC) THEN (fs [Suffix_def]) 944 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o 945 (SPECL [ 946 `` 947 (t:num)-1`` 948 , 949 ``n:string 950 ``]))) 951 THEN (IMP_RES_TAC NUM_LEMMA) 952 THEN (fs [SUB_ADD]) 953 THEN (PROVE_TAC [leq_def, 954 lattice_X1_lemma]) 955 ) 956 ] 957 ); 958 959 960 961(* If a lattice sequence sigma is in the language of a circuit model then 962 if the Defining Sequence of a given trajectory formula is is less than 963 or equal to sigma then sigma satisfies the trajectory formula 964 965 We have stated this theorem in two ways. One is defined on states using 966 leq_state and the later one is defined on lattice values using leq 967*) 968 969val DEFSEQ_LE_THAN_SAT_STE = 970 TAC_PROOF (([], ``!tf. !sigma. 971 in_STE_lang sigma Y_ckt ==> 972 ((!t. (DefSeq tf t) leq_state (sigma t)) 973 ==> SAT_STE tf sigma)``), 974 Induct 975 THEN fs [leq_state_def, SAT_STE_def, DefSeq_def] 976 THEN REPEAT STRIP_TAC 977 THENL [FIRST_ASSUM(STRIP_ASSUME_TAC o 978 SPECL [``0``, ``s:string``]) 979 THEN fs [], 980 FIRST_ASSUM(STRIP_ASSUME_TAC o 981 SPECL [``0``, ``s:string``]) 982 THEN fs [], 983 IMP_RES_TAC LUB_LEMMA7a 984 THEN RES_TAC 985 THEN (IMP_RES_TAC 986 (SPEC_ALL 987 (SPEC_LUB_LEMMA1))) 988 THEN RES_TAC, ((IMP_RES_TAC LUB_LEMMA7b) 989 THEN RES_TAC 990 THEN (IMP_RES_TAC 991 (SPEC_ALL 992 (SPEC_LUB_LEMMA2))) 993 THEN RES_TAC), 994 (IMP_RES_TAC Proposition1 995 THEN RES_TAC 996 THEN (FIRST_ASSUM 997 (STRIP_ASSUME_TAC o 998 SPECL[``(SUC(t:num))``, 999 ``n:string``])) 1000 THEN fs [NOT_EQ_SYM 1001 (SPEC_ALL SUC_NOT)] 1002 THEN fs [SUC_SUB1] 1003 THEN (IMP_RES_TAC 1004 SPEC_NEXT_LEMMA) 1005 THEN (FIRST_ASSUM 1006 (STRIP_ASSUME_TAC o 1007 SPEC ``(Suffix 1 1008 (sigma:num-> 1009 string-> 1010 bool#bool))``)) 1011 THEN RES_TAC)] 1012 ); 1013 1014 1015(* If a lattice sequence sigma is in the language of a circuit model then 1016 if the Defining Sequence of a given trajectory formula is is less than 1017 or equal to sigma then sigma satisfies the trajectory formula 1018 1019 This is the one defined on lattice values using leq 1020 *) 1021 1022 1023val DEFSEQ_LE_THAN_SAT_STE2 = 1024 TAC_PROOF(([], ``!tf. !sigma. 1025 in_STE_lang sigma Y_ckt ==> 1026 ((!t. !n. (DefSeq tf t n) leq 1027 (sigma t n)) 1028 ==> SAT_STE tf sigma)``), 1029 Induct 1030 THEN fs [SAT_STE_def, DefSeq_def] 1031 THEN REPEAT STRIP_TAC 1032 THENL [FIRST_ASSUM(STRIP_ASSUME_TAC o 1033 SPECL [``0``, ``s:string``]) 1034 THEN fs [], 1035 FIRST_ASSUM(STRIP_ASSUME_TAC o 1036 SPECL [``0``, ``s:string``]) 1037 THEN fs [], 1038 IMP_RES_TAC LUB_LEMMA7a 1039 THEN RES_TAC 1040 THEN (IMP_RES_TAC 1041 (SPEC_ALL 1042 (SPEC_LUB_LEMMA1))) 1043 THEN RES_TAC, ((IMP_RES_TAC LUB_LEMMA7b) 1044 THEN RES_TAC 1045 THEN (IMP_RES_TAC 1046 (SPEC_ALL 1047 (SPEC_LUB_LEMMA2))) 1048 THEN RES_TAC), 1049 (IMP_RES_TAC Proposition1 1050 THEN RES_TAC 1051 THEN (FIRST_ASSUM 1052 (STRIP_ASSUME_TAC o 1053 SPECL[``(SUC(t:num))``, 1054 ``n:string``])) 1055 THEN fs [NOT_EQ_SYM 1056 (SPEC_ALL SUC_NOT)] 1057 THEN fs [SUC_SUB1] 1058 THEN (IMP_RES_TAC 1059 SPEC_NEXT_LEMMA) 1060 THEN (FIRST_ASSUM 1061 (STRIP_ASSUME_TAC o 1062 SPEC ``(Suffix 1 1063 (sigma:num-> 1064 string-> 1065 bool#bool))``)) 1066 THEN RES_TAC)] 1067 ); 1068 1069 1070(* DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE 1071 1072 Now proving the if and only if version of the above theorem 1073 1074*) 1075 1076val DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE = TAC_PROOF(([], ``!tf. !sigma. 1077 in_STE_lang sigma Y_ckt ==> 1078 (SAT_STE tf sigma 1079 = !t. 1080 (DefSeq tf t) leq_state 1081 (sigma t))``), 1082 REPEAT STRIP_TAC THEN EQ_TAC 1083 THEN fs [leq_state_def] 1084 THEN (POP_ASSUM MP_TAC 1085 THEN SPEC_TAC 1086 (``sigma:num-> 1087 string->bool#bool``, 1088 ``sigma:num->string-> 1089 bool#bool``) 1090 THEN SPEC_TAC 1091 (``tf:TF``, ``tf:TF``)) 1092 THENL 1093 [PROVE_TAC 1094 [DEFSEQ_LE_THAN_SAT_STE1], 1095 PROVE_TAC 1096 [DEFSEQ_LE_THAN_SAT_STE2] 1097 ] 1098 ); 1099 1100(* DefTraj satisfies the trajectory formula *) 1101 1102val DEFTRAJ_SAT_STE= TAC_PROOF(([], ``!tf Y_ckt. 1103 Monotonic Y_ckt 1104 ==> SAT_STE tf (DefTraj tf Y_ckt)``), 1105 REPEAT STRIP_TAC THEN 1106 (IMP_RES_TAC (SPEC_ALL(DEFTRAJ_IN_STE_LANG))) 1107 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o 1108 (SPEC ``tf:TF``)) 1109 THEN (IMP_RES_TAC 1110 (SPEC_ALL 1111 (DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE))) 1112 THEN (PROVE_TAC 1113 [SPEC_ALL(LEQ_DEFSEQ_DEFTRAJ)])); 1114 1115(* For a circuit model that is monotonic, if a sequence sigma is in the 1116 language of that circuit model then if sigma satisfies a trajectory formula 1117 then the defining trajectory of that formula wrt the given circuit model 1118 returns a lattice value that is less than or equal to the value returned 1119 by sigma *) 1120 1121 1122val SAT_STE_IMP_DEFTRAJ_LESSTHAN_SEQ = 1123 TAC_PROOF(([], ``!tf sigma Y_ckt. 1124 Monotonic Y_ckt ==> 1125 in_STE_lang sigma Y_ckt ==> 1126 SAT_STE tf sigma ==> 1127 (!t n. (DefTraj tf Y_ckt t n) leq (sigma t n))``), 1128 1129 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC 1130 THEN STRIP_TAC THEN Induct 1131 THENL[IMP_RES_TAC DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE 1132 THEN fs [DefTraj_def, leq_state_def], 1133 IMP_RES_TAC DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE 1134 THEN REPEAT STRIP_TAC 1135 THEN fl [leq_state_def] THEN RW_TAC std_ss [DefTraj_def] 1136 THEN fl [Monotonic_def, in_STE_lang_def, leq_state_def] 1137 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o 1138 SPECL [``DefTraj (tf:TF) 1139 (Y_ckt:(string->bool#bool)-> 1140 string->bool#bool)(t:num)``, 1141 ``(sigma:num->string->bool#bool) 1142 (t:num)``])) 1143 THEN RES_TAC 1144 THEN POP_ASSUM MP_TAC 1145 THEN POP_ASSUM MP_TAC 1146 THEN POP_ASSUM MP_TAC 1147 THEN POP_ASSUM MP_TAC 1148 THEN POP_ASSUM MP_TAC 1149 THEN 1150 FIRST_ASSUM(STRIP_ASSUME_TAC o 1151 SPECL[``t:num``, ``n:string``]) 1152 THEN REPEAT STRIP_TAC 1153 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o 1154 SPEC ``n:string``) 1155 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o 1156 SPECL [``SUC t:num``,``n:string``]) 1157 THEN POP_ASSUM MP_TAC THEN RW_TAC std_ss [SUC_ONE_ADD] 1158 THEN PROVE_TAC [TRANS_LEMMA, LUB_LEMMA4, ADD_COMM]]); 1159 1160 1161 1162(* SAT_CKT_IFF_TIME_SHIFT1 and SAT_CKT_IFF_TIME_SHIFT2 are used in the 1163 proof of SAT_CKT_IFF_TIME_SHIFT - Time shifting theorem *) 1164 1165val SAT_CKT_IFF_TIME_SHIFT1 = 1166 TAC_PROOF(([], ``!Ant Cons Y_ckt. 1167 (!sigma. (in_STE_lang sigma Y_ckt ) 1168 ==> ((SAT_STE Ant sigma) 1169 ==> (SAT_STE Cons sigma))) 1170 ==> 1171 (!sigma. (in_STE_lang sigma Y_ckt ) 1172 ==> !t. ((SAT_STE Ant (Suffix t sigma)) 1173 ==> (SAT_STE Cons (Suffix t sigma))))``), 1174 REPEAT STRIP_TAC 1175 THEN (IMP_RES_TAC Proposition) 1176 THEN RES_TAC 1177 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC 1178 o SPEC ``t:num``)) 1179 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o 1180 SPEC ``Suffix (t:num) 1181 (sigma:num->string-> 1182 bool#bool)``)) 1183 THEN fs []); 1184 1185 1186val SAT_CKT_IFF_TIME_SHIFT2 = 1187 TAC_PROOF(([], 1188 ``!Ant Cons Y_ckt. 1189 (!sigma. (in_STE_lang sigma Y_ckt ) 1190 ==> !t. ((SAT_STE Ant (Suffix t sigma)) 1191 ==> (SAT_STE Cons (Suffix t sigma)))) 1192 ==> (!sigma. (in_STE_lang sigma Y_ckt ) 1193 ==> ((SAT_STE Ant sigma) 1194 ==> (SAT_STE Cons sigma)))``), 1195 REPEAT STRIP_TAC 1196 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC 1197 o SPEC ``(sigma:num-> 1198 string-> 1199 bool#bool)``)) 1200 THEN RES_TAC 1201 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC 1202 o SPEC ``0:num``)) 1203 THEN fs [SUFFIX_0] 1204 ); 1205 1206 1207(* Time shifting theorem 1208 1209 A given circuit model satisfies an STE assertion if and only if 1210 for all lattice sequences that are in the language of that circuit 1211 if the ith suffix of the sequence satisfies the antecedent of the 1212 STE assertion then the ith suffix of the sequence also satisfies the 1213 consequent of the STE assertion 1214*) 1215 1216val SAT_CKT_IFF_TIME_SHIFT = 1217 store_thm ("SAT_CKT_IFF_TIME_SHIFT", 1218 ``!Ant Cons Y_ckt. 1219 SAT_CKT (Ant ==>> Cons) Y_ckt 1220 = 1221 (!sigma. (in_STE_lang sigma Y_ckt ) 1222 ==> !t. SAT_STE Ant (Suffix t sigma) 1223 ==> SAT_STE Cons (Suffix t sigma))``, 1224 1225 REPEAT STRIP_TAC THEN fs [SAT_CKT_def] 1226 THEN PROVE_TAC [SAT_CKT_IFF_TIME_SHIFT1, 1227 SAT_CKT_IFF_TIME_SHIFT2]); 1228 1229 1230(* SAT_CKT_IFF_STE1 and SAT_CKT_IFF_STE2 are used in 1231 the proof of SAT_CKT_IFF_STE *) 1232 1233 1234val SAT_CKT_IFF_STE1 = 1235 store_thm ("SAT_CKT_IFF_STE1", 1236 ``!Ant Cons Y_ckt. 1237 Monotonic Y_ckt ==> 1238 (SAT_CKT (Ant ==>> Cons) Y_ckt 1239 ==> !t. (DefSeq Cons t) leq_state 1240 (DefTraj Ant Y_ckt t))``, 1241 let 1242 val temp1 = SPECL [``Cons:TF``, ``DefTraj (Ant:TF) 1243 (Y_ckt:(string->bool#bool)-> 1244 string->bool#bool)``] 1245 DEFSEQ_LESSTHAN_SEQ_IFF_SAT_STE; 1246 val temp2 = SPECL [``Ant:TF``, ``Y_ckt: 1247 (string->bool#bool)-> 1248 string->bool#bool``] 1249 DEFTRAJ_SAT_STE; 1250 val temp3 = SPECL [``Ant:TF``, ``Y_ckt: 1251 (string->bool#bool)-> 1252 string->bool#bool``] 1253 DEFTRAJ_IN_STE_LANG; 1254 val temp4 = SPECL [``Ant:TF``, ``Y_ckt: 1255 (string->bool#bool)-> 1256 string->bool#bool``] 1257 LEQ_DEFSEQ_DEFTRAJ;; 1258 in 1259 REPEAT STRIP_TAC THEN fs [SAT_CKT_def] THEN 1260 (FIRST_ASSUM(STRIP_ASSUME_TAC o 1261 SPEC ``DefTraj (Ant:TF) 1262 (Y_ckt:(string->bool#bool)-> 1263 string->bool#bool)``)) 1264 THEN fs [temp1, temp2, temp3, temp4] 1265 end); 1266 1267val SAT_CKT_IFF_STE2 = 1268 store_thm ("SAT_CKT_IFF_STE2", 1269 ``!Ant Cons Y_ckt. 1270 Monotonic Y_ckt ==> 1271 ((!t. (DefSeq Cons t) leq_state 1272 (DefTraj Ant Y_ckt t)) 1273 ==> 1274 SAT_CKT (Ant ==>> Cons) Y_ckt)``, 1275 1276 let 1277 val temp = SPECL [``Ant:TF``, 1278 ``Y_ckt:(string->bool#bool)-> 1279 string->bool#bool``] 1280 DEFTRAJ_IN_STE_LANG; 1281 in 1282 REPEAT STRIP_TAC 1283 THEN fs [SAT_CKT_def, leq_state_def] 1284 THEN REPEAT STRIP_TAC 1285 THEN STRIP_ASSUME_TAC SEQ_LESS_THAN_SAT_STE 1286 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o 1287 SPECL [``Y_ckt:(string->bool#bool)-> 1288 string->bool#bool``, 1289 ``Cons:TF``, 1290 ``DefTraj (Ant:TF) 1291 (Y_ckt:(string->bool#bool)-> 1292 string->bool#bool)``, 1293 ``sigma:num->string-> 1294 bool#bool``])) 1295 THEN (IMP_RES_TAC temp) 1296 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``Ant:TF``)) 1297 THEN 1298 (FIRST_ASSUM(STRIP_ASSUME_TAC o 1299 SPECL [``Y_ckt:(string->bool#bool)-> 1300 string->bool#bool``, 1301 ``Cons:TF``, 1302 ``DefSeq (Cons:TF)``, 1303 ``DefTraj (Ant:TF) 1304 (Y_ckt:(string->bool#bool)-> 1305 string->bool#bool)`` 1306 ])) 1307 1308 THEN (STRIP_ASSUME_TAC 1309 SAT_STE_IMP_DEFTRAJ_LESSTHAN_SEQ) 1310 THEN (FIRST_ASSUM(STRIP_ASSUME_TAC o 1311 SPECL [``Ant:TF``, 1312 ``sigma:num->string-> 1313 bool#bool``, 1314 ``Y_ckt:(string->bool#bool)-> 1315 string->bool#bool``])) 1316 THEN (STRIP_ASSUME_TAC DEFSEQ_LE_THAN_SAT_STE) 1317 THEN fs [leq_state_def] 1318 end); 1319 1320 1321(* If the circuit model is monotonic then the circuit model 1322 satsifies the STE assertion if and only if the Defining Sequence 1323 of the consequent returns a state value less than or equal to 1324 the state value returned by the defining trajectory for the 1325 antecedent wrt the given circuit model *) 1326 1327val SAT_CKT_IFF_STE = 1328 store_thm("SAT_CKT_IFF_STE", 1329 ``!Ant Cons Y_ckt. 1330 Monotonic Y_ckt ==> 1331 (SAT_CKT (Ant ==>> Cons) Y_ckt 1332 = !t. (DefSeq Cons t) leq_state 1333 (DefTraj Ant Y_ckt t))``, 1334 PROVE_TAC [SAT_CKT_IFF_STE1, SAT_CKT_IFF_STE2] 1335 );; 1336 1337 1338(* Defining Sequence beyond the depth of a trajectory formula is X *) 1339 1340val DEFSEQ_X = 1341 store_thm("DEFSEQ_X", 1342 ``!tf i. i > Depth tf ==> !n. DefSeq tf i n = X``, 1343 1344 Induct THEN fs [DefSeq_def, Depth_def] 1345 THENL[ 1346 (REPEAT STRIP_TAC THEN COND_CASES_TAC THEN FULL_SIMP_TAC 1347 arith_ss []), 1348 1349 (REPEAT STRIP_TAC THEN COND_CASES_TAC THEN FULL_SIMP_TAC 1350 arith_ss []), 1351 1352 (GEN_TAC THEN fs [MAX_def] THEN COND_CASES_TAC THEN 1353 REPEAT STRIP_TAC THEN RES_TAC THEN 1354 (FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``n:string``)) 1355 THEN (FULL_SIMP_TAC arith_ss [lub_def, X_def])), 1356 1357 (REPEAT STRIP_TAC THEN RES_TAC THEN 1358 (FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``n:string``)) 1359 THEN (FULL_SIMP_TAC arith_ss [lub_def, X_def]) THEN 1360 Cases_on `b` THEN fs [FST, SND, X_def]), 1361 1362 (REPEAT STRIP_TAC THEN COND_CASES_TAC THEN 1363 (FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``((i:num)-1)``)) 1364 THEN (FULL_SIMP_TAC arith_ss [])) 1365 ] 1366 );; 1367 1368(* If a node doesn't occur in antecedent and it doesn't appear in NEXT Cons 1369 then it doesn't appear in Ant and it doesn't appear in Cons *) 1370val NODE_LEMMA0 = 1371 store_thm ("NODE_LEMMA0", ``!node Ant Cons. 1372 ~MEM node (APPEND(Nodes Ant []) 1373 (Nodes (NEXT Cons) [])) ==> 1374 ~MEM node (APPEND(Nodes Ant []) 1375 (Nodes Cons [])) 1376 ``, 1377 REPEAT STRIP_TAC THEN fs [Nodes_def]); 1378 1379 1380 1381val NODE_LEMMA1 = store_thm ("NODE_LEMMA1", 1382 ``!elem tf. ~MEM elem (Nodes (NEXT tf) []) 1383 = ~MEM elem (Nodes tf [])``, 1384 REPEAT STRIP_TAC THEN Induct_on `tf` 1385 THEN REPEAT STRIP_TAC THEN fs [Nodes_def]); 1386 1387 1388 1389 1390(* If a node doesn't appear in a trajectory formula, it takes on a value X *) 1391val NODE_LEMMA2 = store_thm("NODE_LEMMA2", 1392 ``!tf (node:string). 1393 ~MEM node (Nodes tf []) ==> 1394 !t. DefSeq tf t node = X``, 1395 Induct THENL 1396 [fl [Nodes_def, DefSeq_def], 1397 fl [Nodes_def, DefSeq_def], 1398 fl [DefSeq_def, Nodes_def] 1399 THEN REPEAT STRIP_TAC THEN 1400 fl [MEM_NODES2, lub_def, X_def], 1401 REPEAT STRIP_TAC 1402 THEN fl [Nodes_def, DefSeq_def] 1403 THEN Cases_on `b` THEN fl [X_def], 1404 fl [DefSeq_def, Nodes_def]]); 1405 1406(* All nodes that don't appear in the antecedent or the consequent take on 1407 a value X *) 1408val NODES_X = 1409 store_thm ("NODES_X", 1410 ``!Ant Cons. !(node:string). 1411 ~(MEM node (APPEND(Nodes Ant []) 1412 (Nodes Cons []))) 1413 ==> !t. (DefSeq Cons t node = X)``, 1414 Induct THENL 1415 [STRIP_TAC THEN Induct THEN fl [Nodes_def, DefSeq_def] 1416 THENL [REPEAT STRIP_TAC THEN IMP_RES_TAC MEM_NODES2 1417 THEN RES_TAC 1418 THEN fl [lub_def, X_def], 1419 REPEAT STRIP_TAC THEN fl [X_def]], 1420 STRIP_TAC THEN Induct THEN fl [Nodes_def, DefSeq_def] 1421 THENL [REPEAT STRIP_TAC THEN IMP_RES_TAC MEM_NODES2 1422 THEN RES_TAC 1423 THEN fl [lub_def, X_def], 1424 REPEAT STRIP_TAC THEN fl [X_def]], 1425 fl [Nodes_def] THEN REPEAT STRIP_TAC THEN 1426 IMP_RES_TAC MEM_NODES2 THEN RES_TAC 1427 THEN fl [lub_def, X_def], 1428 REPEAT STRIP_TAC THEN fl [Nodes_def], 1429 REPEAT STRIP_TAC THEN fl [Nodes_def]]); 1430 1431 1432(* AuxTheorem1 and Theorem1 are basically identical 1433 except that in AuxTheorem1 we have rephrased the goal 1434 with the definition of STE_Impl unfolded. We use AuxTheorem1 1435 in the proof of Theorem1. Theorem1 has purely academic value 1436 - succint representation of AuxTheorem1. AuxTheorem1 1437 is used in the proof of SAT_CKT_IFF_STE_IMPL *) 1438 1439(* If the given circuit model Y is monotonic then it 1440 satisfies an STE assertion Ant ==>> Cons if and only if 1441 the STE Implementation STE_Impl guarantees that *) 1442 1443 1444(* How the proof of AuxTheorem1 and in turn Theorem1 depends on other 1445 important lemmas and theorems, specially the fact that Y has got to 1446 be Monotonic 1447 1448 AuxTheorem1 1449 | 1450 | 1451 | 1452 \|/ 1453 | 1454SAT_CKT_IFF_STE 1455 | \ 1456 | \ 1457 | \ 1458 \|/ \ 1459 | \ 1460SAT_CKT_IFF_STE1 \ 1461 \ 1462 \ 1463 SAT_CKT_IFF_STE2 1464 | 1465 | 1466 | 1467 \|/ 1468 | 1469 SAT_STE_IMP_DEFTRAJ_LESSTHAN_SEQ 1470 | 1471 | 1472 | 1473 \|/ 1474 | 1475 Monotonicity of Y 1476 1477 1478 *) 1479 1480 1481 1482 1483val AuxTheorem1 = 1484 store_thm ("AuxTheorem1", ``!Ant Cons Y_ckt. 1485 Monotonic Y_ckt ==> 1486 (SAT_CKT (Ant ==>> Cons) Y_ckt 1487 = 1488 (!t. 1489 t <= Depth Cons ==> 1490 !n. 1491 MEM n (APPEND(Nodes Ant [])(Nodes Cons [])) 1492 ==> 1493 (DefSeq Cons t n) leq 1494 (DefTraj Ant Y_ckt t n)))``, 1495 1496 REPEAT STRIP_TAC THEN fl [SAT_CKT_IFF_STE] 1497 THEN EQ_TAC THEN REPEAT STRIP_TAC THENL 1498 [fl [leq_state_def], 1499 fl [leq_state_def], 1500 fl [leq_state_def] THEN REPEAT STRIP_TAC 1501 THEN STRIP_ASSUME_TAC DEFSEQ_X 1502 THEN Induct_on `t <= Depth Cons` 1503 THENL [REPEAT STRIP_TAC THEN 1504 Induct_on 1505 `MEM node (APPEND(Nodes Ant []) 1506 (Nodes Cons []))` 1507 THENL [REPEAT STRIP_TAC THEN fl [MEM_APPEND], 1508 REPEAT STRIP_TAC THEN 1509 STRIP_ASSUME_TAC NODES_X 1510 THEN fl [leq_def] THEN 1511 PROVE_TAC [lattice_X1_lemma]], 1512 fl [leq_def] 1513 THEN PROVE_TAC [lattice_X1_lemma]]]); 1514 1515(* Theorem1 *) 1516 1517(* If the given circuit model Y is monotonic then it 1518 satisfies an STE assertion Ant ==>> Cons if and only if 1519 the STE Implementation STE_Impl guarantees that *) 1520 1521val Theorem1 = store_thm ("Theorem1", 1522 ``!Ant Cons Y_ckt. 1523 Monotonic Y_ckt ==> 1524 (SAT_CKT (Ant ==>> Cons) Y_ckt 1525 = STE_Impl (Ant ==>> Cons) Y_ckt)``, 1526 fs [STE_Impl_def] THEN 1527 PROVE_TAC [AuxTheorem1] 1528 ); 1529 1530(* Refer to explanation in the Big Picture section *) 1531 1532val SAT_CKT_IFF_STE_IMPL = 1533 store_thm ("SAT_CKT_IFF_STE_IMPL", 1534 ``!Ant Cons Y_ckt. 1535 Monotonic Y_ckt ==> 1536 ( 1537 (!sigma. 1538 in_STE_lang sigma Y_ckt ==> 1539 !t. 1540 SAT_STE Ant (Suffix t sigma) ==> 1541 SAT_STE Cons (Suffix t sigma)) = 1542 (!t. 1543 t <= Depth Cons ==> 1544 !n. 1545 MEM n (APPEND(Nodes Ant [])(Nodes Cons [])) ==> 1546 (DefSeq Cons t n) leq (DefTraj Ant Y_ckt t n)) 1547 )``, 1548 REPEAT GEN_TAC 1549 THEN fs [SYM(SPEC_ALL SAT_CKT_IFF_TIME_SHIFT)] 1550 THEN fs [AuxTheorem1]); 1551 1552 1553 1554(* Refer for explanation to the Big Picture section *) 1555val Theorem2 = 1556 store_thm ("Theorem2", ``!Ant Cons. 1557 !Y_ckt Yb_ckt. Okay (Y_ckt, Yb_ckt) 1558 ==> 1559 ( 1560 !sigma. in_STE_lang sigma Y_ckt 1561 ==> !t. ((SAT_STE Ant (Suffix t sigma)) 1562 ==> (SAT_STE Cons (Suffix t sigma))) 1563 ) 1564 ==> 1565 ( 1566 !sigma_b. in_BOOL_lang sigma_b Yb_ckt 1567 ==> !t. ((SAT_BOOL Ant (Suffix_b t sigma_b)) 1568 ==> (SAT_BOOL Cons (Suffix_b t sigma_b))) 1569 )``, 1570 REPEAT GEN_TAC THEN 1571 (STRIP_ASSUME_TAC (SPECL 1572 [``Y_ckt:(string->(bool#bool)) 1573 ->(string->(bool#bool))``, 1574 ``Yb_ckt:(string->bool) 1575 ->(string->bool)->bool``] 1576 Lemma1)) 1577 THEN (REPEAT STRIP_TAC) 1578 THEN (fs [Lemma2]) 1579 1580 THEN (FIRST_ASSUM (STRIP_ASSUME_TAC o 1581 SPEC ``extended_drop_seq 1582 (sigma_b:num->string->bool)``)) 1583 THEN (fs [Suffix_Lemma]) 1584 THEN (FIRST_ASSUM (STRIP_ASSUME_TAC o 1585 SPEC 1586 ``sigma_b:num->string->bool``)) 1587 THEN (fs [])); 1588 1589 1590(* Same as Theorem2 except that the definition of SAT_CKT is 1591 uunfolded in Theorem2. This theorem has pure academic value. 1592 - succint representation. This is known as Theorem 2 in the Tech Report 1593 and also in the TPHOLS paper *) 1594val AuxTheorem2 = 1595 store_thm ("AuxTheorem2", ``!Ant Cons. 1596 !Y_ckt Yb_ckt. Okay (Y_ckt, Yb_ckt) 1597 ==> 1598 (SAT_CKT (Ant ==>> Cons) Y_ckt) 1599 ==> 1600 ( 1601 !sigma_b. in_BOOL_lang sigma_b Yb_ckt 1602 ==> !t. ((SAT_BOOL Ant (Suffix_b t sigma_b)) 1603 ==> (SAT_BOOL Cons (Suffix_b t sigma_b))) 1604 )``, PROVE_TAC [SAT_CKT_IFF_TIME_SHIFT, Theorem2]); 1605 1606(* Refer to explanation in the Big Picture section *) 1607 1608val BridgeTheorem = 1609 store_thm ("BridgeTheorem", 1610 ``!Ant Cons Y_ckt Yb_ckt. 1611 Okay (Y_ckt, Yb_ckt) ==> 1612 Monotonic Y_ckt 1613 ==> 1614 ( 1615 1616 (!t. 1617 t <= Depth Cons ==> 1618 !n. 1619 MEM n (APPEND(Nodes Ant [])(Nodes Cons [])) ==> 1620 (DefSeq Cons t n) leq (DefTraj Ant Y_ckt t n)) 1621 1622 ==> 1623 ( 1624 !sigma_b. 1625 in_BOOL_lang sigma_b Yb_ckt ==> 1626 !t. 1627 SAT_BOOL Ant (Suffix_b t sigma_b) ==> 1628 SAT_BOOL Cons (Suffix_b t sigma_b)) 1629 )``, 1630 1631 REPEAT STRIP_TAC 1632 THEN IMP_RES_TAC (SPEC_ALL SAT_CKT_IFF_STE_IMPL) 1633 THEN IMP_RES_TAC (SPEC_ALL Theorem2) 1634 ); 1635 1636 1637val BRIDGETHEOREM2 = store_thm ("BRIDGETHEOREM2", 1638 ``!Ant Cons Y_ckt Yb_ckt. 1639 Okay (Y_ckt,Yb_ckt) ==> 1640 Monotonic Y_ckt ==> 1641 STE_Impl (Ant ==>> Cons) Y_ckt ==> 1642 !sigma_b. 1643 in_BOOL_lang sigma_b Yb_ckt ==> 1644 !t. 1645 SAT_BOOL Ant 1646 (Suffix_b t sigma_b) ==> 1647 SAT_BOOL Cons 1648 (Suffix_b t sigma_b)``, 1649 MATCH_ACCEPT_TAC (CONV_RULE 1650 (SIMP_CONV std_ss 1651 [(SYM o SPEC_ALL) 1652 STE_Impl_def]) 1653 BridgeTheorem)); 1654 1655 1656val _ = export_theory(); 1657end; 1658