1(in-package "ACL2") 2 3;; The following two lines are added for portability to v2-7.... 4 5 6#| 7 8 cone-of-influence.lisp 9 ~~~~~~~~~~~~~~~~~~~~~~ 10 11We implement a cone of influence reduction algorithm. Cone of influence is 12(roughly) elimination of redundant variables. Given a collection of V variables, 13we determine the closure V*, V =< V* =< (variables C) and a collection 14E =< (equations C), such that for every variable in V*, the equation in E for 15that variable corresponds to the equation in (equations C). We then claim that 16the Kripke structure created from the cone-of-influence reduced circuit is 17bisimilar with respect to V* to the Kripke Structure created from the original 18circuit. 19 20|# 21 22 23(include-book "circuits") 24 25;; Here are the two culprit rules that I need to disable to get the proof 26;; faster. Just shows how naive a user I was when I did this proof. 27 28(in-theory (disable subset-of-nil-is-nil 29 subset-of-empty-is-empty)) 30 31(defun find-variables* (equation-list) 32 (if (endp equation-list) nil 33 (set-union (find-variables (first equation-list)) 34 (find-variables* (rest equation-list))))) 35 36(defun find-all-variables-1-pass (vars equations) 37 (if (endp vars) nil 38 (set-union (find-variables* (<- equations (first vars))) 39 (find-all-variables-1-pass (rest vars) equations)))) 40 41;; The following function find-all-variables is a difficult function to 42;; admit. It computes the closure of a given set of variables (vars) with 43;; respect to a collection of variables (variables) and a collection of 44;; equations. 45 46(local 47(in-theory (enable set-union)) 48) 49 50(local 51(defthm len-set-union-more-than-y 52 (<= (len y) 53 (len (set-union x y))) 54 :rule-classes :linear) 55) 56 57(local 58(defthm uniquep-member-reduction 59 (equal (memberp e (set-union x y)) 60 (or (memberp e x) 61 (memberp e y)))) 62) 63 64(local 65(defthm uniquep-union-reduction 66 (implies (and (uniquep x) 67 (uniquep y)) 68 (uniquep (set-union x y)))) 69) 70 71(local 72(defthm find-variables-is-unique 73 (uniquep (find-variables equations))) 74) 75 76(local 77(defthm find-variables*-is-unique 78 (uniquep (find-variables* equations))) 79) 80 81(local 82(defthm find-all-variables-1-pass-is-unique 83 (uniquep (find-all-variables-1-pass vars equations))) 84) 85 86(defun del (e x) 87 (if (endp x) x 88 (if (equal e (first x)) 89 (rest x) 90 (cons (first x) (del e (rest x)))))) 91 92(local 93(defthm len-del-reduction-1 94 (implies (memberp e x) 95 (equal (len (del e x)) 96 (1- (len x)))) 97 :hints (("Goal" 98 :in-theory (enable len)))) 99) 100 101(defun induction-hint-for-len-<= (x y) 102 (if (endp x) (list x y) 103 (induction-hint-for-len-<= (cdr x) (del (car x) y)))) 104 105(local 106(defthm del-not-member-reduction 107 (implies (not (memberp e x)) 108 (equal (del e x) x))) 109) 110 111(local 112(defthm member-del-reduction 113 (implies (not (equal v e)) 114 (equal (memberp v (del e y)) 115 (memberp v y)))) 116) 117 118(local 119(defthm subset-del-member 120 (implies (and (not (memberp e x)) 121 (subset x y)) 122 (subset x (del e y)))) 123) 124 125(local 126(defthm uniquep-del-reduction 127 (implies (uniquep x) 128 (uniquep (del e x)))) 129) 130 131(local 132(defthm uniquep-and-subset-implies-len-<= 133 (implies (and (uniquep x) 134 (uniquep y) 135 (subset x y)) 136 (<= (len x) 137 (len y))) 138 :hints (("Goal" 139 :induct (induction-hint-for-len-<= x y) 140 :do-not '(eliminate-destructors generalize) 141 :do-not-induct t))) 142) 143 144(local 145(defthm subset-from-union 146 (implies (and (subset x z) 147 (subset y z)) 148 (subset (set-union x y) z))) 149) 150 151(local 152(defthm subset-from-union-2 153 (implies (and (subset (set-union x y) z) 154 (uniquep x) 155 (uniquep y)) 156 (and (subset x z) 157 (subset y z)))) 158) 159 160(local 161(include-book "arithmetic-2/meta/top" :dir :system) 162) 163 164(local 165(defthm del-e-to-cons-subset 166 (implies (subset (del e y) x) 167 (subset y (cons e x)))) 168) 169 170 171(local 172 (defthm len-not-consp 173 (implies (equal (len x) 0) 174 (not (consp x))) 175 :rule-classes :forward-chaining)) 176 177 178(local 179(defthm len-equal-to-set-equal 180 (implies (and (equal (len x) (len y)) 181 (uniquep x) 182 (uniquep y) 183 (subset x y)) 184 (subset y x)) 185 :hints (("Goal" 186 :induct (induction-hint-for-len-<= x y) 187 :do-not '(eliminate-destructors generalize) 188 :do-not-induct t) 189 ("Subgoal *1/2.1" 190 :in-theory (disable del-e-to-cons-subset) 191 :use ((:instance del-e-to-cons-subset 192 (e (car x)) 193 (x (cdr x))))))) 194) 195 196(defun find-all-variables (vars variables equations) 197 (declare (xargs :measure (nfix (- (len variables) (len vars))) 198 :hints (("Goal" 199 :do-not-induct t 200 :in-theory (enable set-equal) 201 :do-not '(eliminate-destructors generalize))))) 202 (if (or (not (uniquep variables)) 203 (not (uniquep vars)) 204 (not (subset vars variables))) 205 vars 206 (let ((new-vars (set-union (find-all-variables-1-pass vars equations) 207 vars))) 208 (if (not (subset new-vars variables)) nil 209 (if (set-equal vars new-vars) vars 210 (find-all-variables new-vars variables equations)))))) 211 212(defun find-all-equations (vars equations eq-rec) 213 (if (endp vars) eq-rec 214 (find-all-equations (rest vars) equations 215 (-> eq-rec 216 (first vars) 217 (<- equations (first vars)))))) 218 219(defun remove-duplicate-occurrences (x) 220 (cond ((endp x) x) 221 ((memberp (first x) (rest x)) (remove-duplicate-occurrences (rest x))) 222 (t (cons (first x) (remove-duplicate-occurrences (rest x)))))) 223 224(defun corresponding-state (init vars) 225 (if (endp vars) nil 226 (-> (corresponding-state init (rest vars)) 227 (first vars) 228 (<- init (first vars))))) 229 230(defun corresponding-states (inits vars) 231 (if (endp inits) nil 232 (cons (corresponding-state (first inits) vars) 233 (corresponding-states (rest inits) vars)))) 234 235(defun cone-variables (vars C) 236 (find-all-variables 237 (set-intersect (remove-duplicate-occurrences vars) 238 (variables C)) 239 (variables C) 240 (equations C))) 241 242(defun cone-of-influence-reduction (C vars) 243 (let ((variables (cone-variables vars C))) 244 (>_ :variables variables 245 :initial-states (corresponding-states (initial-states C) variables) 246 :equations (find-all-equations variables (equations C) ())))) 247 248;; OK, so we have implemented the cone of influence reduction. Let us prove 249;;that create-kripke of this reduced model is bisim-equiv to create-Kripke of 250;; C. 251 252;; Notice that for the bisimilarity proof to go through, the variables that we 253;; choose are the variables in the cone. So proving that the variables are subset 254;; of the variables of cone is trivial. On the other hand, we need to prove that 255;; the variables are subset of the original collection of variables. 256 257(local 258(defthm find-all-variables-subset-of-variables 259 (implies (and (uniquep vars) 260 (uniquep variables) 261 (subset vars variables)) 262 (subset (find-all-variables vars variables equations) variables)) 263 :hints (("Goal" 264 :in-theory (disable subset-of-nil-is-nil 265 subset-of-empty-is-empty)))) 266) 267 268;; OK, so we know find-all-variables-is-a-subset. We need to prove that vars is 269;; a subset and uniquep, though. Now, vars is really remove-duplicates of 270;; (set-intersect (remove-duplicates vars) (variables C)) 271 272(local 273(defthm member-remove-duplicate-reduction 274 (equal (memberp e (remove-duplicate-occurrences x)) 275 (memberp e x))) 276) 277 278(local 279(defthm unique-duplicate-reduction 280 (uniquep (remove-duplicate-occurrences x))) 281) 282 283(local 284(defthm uniquep-intersect-reduction 285 (implies (and (uniquep x) 286 (uniquep y)) 287 (uniquep (set-intersect x y)))) 288) 289 290(local 291(defthm find-all-variables-is-unique 292 (implies (uniquep vars) 293 (uniquep (find-all-variables vars variables equations))) 294 :hints (("Goal" 295 :in-theory (disable subset-of-empty-is-empty)))) 296) 297 298(local 299(defthm subset-remove-reduction 300 (equal (subset (remove-duplicate-occurrences x) y) 301 (subset x y))) 302) 303 304(local 305(defthm subset-set-intersect-reduction 306 (equal (subset (set-intersect (remove-duplicate-occurrences x) y) z) 307 (subset (set-intersect x y) z)) 308 :hints (("Goal" 309 :in-theory (disable subset-of-empty-is-empty)))) 310) 311 312;; And now check that we have done the trick. 313 314(local 315(defthm variables-are-subset-of-original 316 (implies (circuitp C) 317 (subset (cone-variables vars C) 318 (variables (create-kripke C)))) 319 :hints (("Goal" 320 :in-theory (disable subset-of-nil-is-nil 321 subset-of-empty-is-empty) 322 :do-not-induct t))) 323) 324 325(local 326(defthm variables-are-subset-of-cone 327 (subset (cone-variables vars C) 328 (variables (create-kripke 329 (cone-of-influence-reduction C vars)))) 330 :hints (("Goal" 331 :in-theory (disable cone-variables)))) 332) 333 334;; OK, so we have proved that the vars are subset of variables. Let us now work 335;; on the initial states. 336 337(local 338(defthm evaluation-eq-subset-reduction 339 (implies (and (subset vars-prime vars) 340 (evaluation-eq p q vars)) 341 (evaluation-eq p q vars-prime))) 342) 343 344(local 345(defthm evaluation-eq-member-subset-reduction 346 (implies (and (evaluation-eq-member-p init inits vars) 347 (subset vars-prime vars)) 348 (evaluation-eq-member-p init inits vars-prime))) 349) 350 351(local 352(defthm evaluation-eq-subset-subset-reduction 353 (implies (and (evaluation-eq-subset-p inits states vars) 354 (subset vars-prime vars)) 355 (evaluation-eq-subset-p inits states vars-prime))) 356) 357 358(local 359(defthm corresponding-states-are-evaluation-eq 360 (implies (uniquep vars) 361 (evaluation-eq init (corresponding-state init vars) vars))) 362) 363 364(local 365(defthm corresponding-state-is-member-of-corresponding-states 366 (implies (memberp init inits) 367 (memberp (corresponding-state init vars) 368 (corresponding-states inits vars)))) 369) 370 371(local 372(defthm evaluation-eq-memberp-of-corresponding-states 373 (implies (and (uniquep vars) 374 (memberp init inits)) 375 (evaluation-eq-member-p init (corresponding-states inits vars) 376 vars))) 377) 378 379(local 380(defthm evaluation-eq-subsets-reduction 381 (implies (uniquep vars) 382 (evaluation-eq-subset-p inits (corresponding-states inits vars) 383 vars))) 384) 385 386 387(local 388(defthm initial-states-are-evaluation-eq 389 (implies (circuitp C) 390 (evaluation-eq-subset-p 391 (initial-states (create-kripke C)) 392 (initial-states 393 (create-kripke 394 (cone-of-influence-reduction C vars))) 395 (cone-variables vars C))) 396 :hints (("Goal" 397 :in-theory (disable subset-of-nil-is-nil 398 subset-of-empty-is-empty)))) 399) 400 401(local 402(defthm corresponding-states-are-evaluation-eq-2 403 (implies (uniquep vars) 404 (evaluation-eq (corresponding-state init vars) init vars))) 405) 406 407(local 408(defthm evaluation-eq-memberp-of-corresponding-states-2 409 (implies (and (uniquep vars) 410 (memberp init (corresponding-states inits vars))) 411 (evaluation-eq-member-p init inits 412 vars))) 413) 414 415(local 416(defthm evaluation-eq-subsets-reduction-2 417 (implies (uniquep vars) 418 (evaluation-eq-subset-p (corresponding-states inits vars) inits 419 vars))) 420) 421 422(local 423(defthm initial-states-are-evaluation-eq-2 424 (implies (circuitp C) 425 (evaluation-eq-subset-p 426 (initial-states 427 (create-kripke 428 (cone-of-influence-reduction C vars))) 429 (initial-states (create-kripke C)) 430 (cone-variables vars C)))) 431) 432 433;; END of work on initial states. 434 435;; OK, now let us work on showing that cone-of-influence-reduction produces a 436;; circuit model. This will follow if the cone of influence reduction actually 437;; produces a circuit. We prove that in the lemmas below. 438 439;; We first prove that the initial states are only evaluations of the variables. 440 441(local 442(defthm initial-states-are-evaluations-p 443 (implies (and (evaluation-p p variables) 444 (subset vars variables) 445 (uniquep variables)) 446 (evaluation-p (corresponding-state p vars) vars))) 447) 448 449(local 450(defthm corresponding-states-only-evaluations-p 451 (implies (and (only-evaluations-p init variables) 452 (subset vars variables) 453 (uniquep variables)) 454 (only-evaluations-p (corresponding-states init vars) vars))) 455) 456 457(local 458(defthm initial-states-of-cone-of-influence-are-only-evaluations-p 459 (implies (circuitp C) 460 (only-evaluations-p 461 (initial-states 462 (cone-of-influence-reduction C vars)) 463 (variables 464 (cone-of-influence-reduction C vars))))) 465) 466 467;; Next we work on strict-evaluation-list-p. 468 469(local 470(defthm not-memberp-to-corresponding-state 471 (implies (not (memberp v vars)) 472 (not (<- (corresponding-state init vars) v)))) 473) 474 475(local 476(defthm corresponding-state-strict-evaluation-p 477 (strict-evaluation-p (corresponding-state init vars) vars)) 478) 479 480(local 481(in-theory (disable strict-evaluation-p)) 482) 483 484(local 485(defthm initial-states-strict-evaluation-list-p 486 (strict-evaluation-list-p vars (corresponding-states inits vars))) 487) 488 489(local 490(defthm initial-cone-of-influence-states-are-strict-evaluation-list-p 491 (strict-evaluation-list-p 492 (variables 493 (cone-of-influence-reduction C vars)) 494 (initial-states 495 (cone-of-influence-reduction C vars))) 496 :hints (("Goal" 497 :in-theory (disable cone-variables)))) 498) 499 500(local 501(defthm variables-of-cone-are-unique-p 502 (implies (circuitp C) 503 (uniquep 504 (variables 505 (cone-of-influence-reduction C vars))))) 506) 507 508 509;; We come here to cons-list-p. 510 511 512(local 513(defun equation-equal-p (eqn-orig eqn-cone vars) 514 (if (endp vars) T 515 (and (equal (<- eqn-orig (first vars)) 516 (<- eqn-cone (first vars))) 517 (equation-equal-p eqn-orig eqn-cone (rest vars))))) 518) 519 520(local 521(defthm cons-list-p-equation-equal-reduction 522 (implies (equation-equal-p eqn-orig eqn-cone vars) 523 (equal (cons-list-p vars eqn-cone) 524 (cons-list-p vars eqn-orig)))) 525) 526 527(local 528(defthm find-equations-for-not-member-p 529 (implies (not (memberp v vars)) 530 (equal (<- (find-all-equations vars equations eqn-rec) v) 531 (<- eqn-rec v)))) 532) 533 534(local 535(defthm cons-list-p-subset-reduction 536 (implies (and (cons-list-p vars equations) 537 (subset vars-prime vars)) 538 (cons-list-p vars-prime equations))) 539) 540 541(local 542(defthm equations-of-cone-and-orig-are-equal 543 (implies (uniquep vars) 544 (equation-equal-p equations 545 (find-all-equations 546 vars equations eqn-rec) 547 vars)) 548 :hints (("Goal" 549 :induct (find-all-equations vars equations eqn-rec) 550 :do-not '(eliminate-destructors generalize) 551 :do-not-induct t))) 552) 553 554(local 555(defthm equations-of-cone-are-cons-list-p 556 (implies (circuitp C) 557 (cons-list-p (variables 558 (cone-of-influence-reduction C vars)) 559 (equations 560 (cone-of-influence-reduction C vars)))) 561 :hints (("Goal" 562 :in-theory (disable find-all-equations find-all-variables 563 cons-list-p-equation-equal-reduction) 564 :use ((:instance cons-list-p-equation-equal-reduction 565 (eqn-orig (equations C)) 566 (eqn-cone 567 (equations 568 (cone-of-influence-reduction C vars))) 569 (vars (variables 570 (cone-of-influence-reduction C vars)))))))) 571) 572 573(local 574(defthm find-variables-variables*-reduction 575 (implies (memberp equation equations) 576 (subset (find-variables equation) 577 (find-variables* equations)))) 578) 579 580(local 581(defthm find-variables-1-pass-reduction 582 (implies (and (memberp v vars) 583 (memberp equation (<- equations v))) 584 (subset (find-variables equation) 585 (find-all-variables-1-pass vars equations))) 586 :hints (("Subgoal *1/2" 587 :do-not-induct t 588 :do-not '(eliminate-destructors generalize) 589 :cases ((equal v (car vars)))) 590 ("Subgoal *1/2.1" 591 :in-theory (disable find-variables-variables*-reduction) 592 :use ((:instance find-variables-variables*-reduction 593 (equations (<- equations (first vars))))))) 594 :rule-classes nil) 595) 596 597(local 598(defthm find-all-variables-computes-closure 599 (implies (and (memberp v (find-all-variables vars variables equations)) 600 (uniquep variables) 601 (subset vars variables) 602 (uniquep vars) 603 (memberp equation (<- equations v))) 604 (subset (find-variables equation) 605 (find-all-variables vars variables equations))) 606 :hints (("Goal" 607 :induct (find-all-variables vars variables equations) 608 :do-not '(eliminate-destructors generalize) 609 :do-not-induct t) 610 ("Subgoal *1/2" 611 :in-theory (enable set-equal) 612 :use find-variables-1-pass-reduction))) 613) 614 615(local 616(in-theory (disable find-all-variables)) 617) 618 619(local 620(defthm find-all-variables-is-equation-record-p 621 (implies (and (subset vars variables) 622 (uniquep vars) 623 (uniquep variables)) 624 (consistent-equation-record-p 625 (find-all-variables vars variables equations) 626 equations)) 627 :otf-flg t 628 :hints (("Goal" 629 :do-not-induct t 630 :in-theory (disable find-all-variables-computes-closure) 631 :use ((:instance (:definition consistent-equation-record-p) 632 (vars (find-all-variables vars variables 633 equations))) 634 (:instance find-all-variables-computes-closure 635 (v (mv-nth 0 636 (consistent-equation-record-p-witness 637 (find-all-variables vars variables 638 equations) 639 equations))) 640 (equation 641 (mv-nth 1 642 (consistent-equation-record-p-witness 643 (find-all-variables vars variables 644 equations) 645 equations)))))))) 646) 647 648;; So we have proved that find-all-variables produces a consistent record for 649;; the original equations. Now we have to prove that if two equations are 650;; equation-equal-p, then they are consistent-equation-record-p at the same 651;; time. 652 653(local 654(in-theory (disable consistent-equation-record-p)) 655) 656 657(local 658(defthm equation-equal-p-member-reduction 659 (implies (and (equation-equal-p eqn-orig eqn-cone vars) 660 (memberp v vars)) 661 (equal (<- eqn-cone v) 662 (<- eqn-orig v)))) 663) 664 665(local 666(defthm consistent-eqn-record-p-expanded 667 (implies (and (consistent-equation-record-p vars eqn-orig) 668 (uniquep vars) 669 (memberp v vars) 670 (memberp equation (<- eqn-orig v))) 671 (subset (find-variables equation) 672 vars)) 673 :hints (("Goal" 674 :use ((:instance consistent-equation-record-p-necc 675 (equations eqn-orig)))))) 676) 677 678(local 679(defthm equation-equal-p-to-consistent 680 (implies (and (equation-equal-p eqn-orig eqn-cone vars) 681 (uniquep vars) 682 (consistent-equation-record-p vars eqn-orig)) 683 (consistent-equation-record-p vars eqn-cone)) 684 :hints (("Goal" 685 :do-not-induct t 686 :in-theory (disable consistent-equation-record-p 687 consistent-equation-record-p-necc 688 mv-nth) 689 :expand (consistent-equation-record-p vars eqn-cone) 690 :use ((:instance consistent-equation-record-p-necc 691 (equation eqn-orig)))))) 692) 693 694(local 695(in-theory (disable consistent-equation-record-p 696 consistent-equation-record-p-necc)) 697) 698 699(local 700(defthm cone-of-influence-reduction-is-consistent 701 (implies (circuitp C) 702 (consistent-equation-record-p 703 (variables (cone-of-influence-reduction C vars)) 704 (equations (cone-of-influence-reduction C vars)))) 705 :hints (("Goal" 706 :use ((:instance equation-equal-p-to-consistent 707 (eqn-orig (equations C)) 708 (eqn-cone 709 (equations (cone-of-influence-reduction C vars))) 710 (vars (variables (cone-of-influence-reduction C vars)))))))) 711 712) 713 714(local 715(defthm cone-of-influence-reduction-is-circuit-p 716 (implies (circuitp C) 717 (circuitp (cone-of-influence-reduction C vars))) 718 :hints (("Goal" 719 :in-theory (disable circuitp cone-of-influence-reduction) 720 :expand (circuitp (cone-of-influence-reduction C vars))))) 721) 722 723(local 724(defthm cone-of-influence-reduction-produces-circuit-model 725 (implies (circuitp C) 726 (circuit-modelp (create-kripke (cone-of-influence-reduction C vars)))) 727 :hints (("Goal" 728 :in-theory (disable circuitp circuit-modelp 729 create-kripke 730 cone-of-influence-reduction)))) 731) 732 733;; OK, so the last thing we need to prove is that the transitions of m and n 734;; are well-formed-transition-p. That means that we have to prove that if two 735;; states are evaluation-eq with respect to vars, then the next states are 736;; evaluation-eq with respect to vars. 737 738;; For simplifying the project let us first start with original circuit and get 739;; to the cone of influence reduction. 740 741;; OK, so what do we need? Let us first prove that if r is in next-states of p, 742;; then there exists an equation consistent with equations that takes from p to 743;; r. 744 745;; We start with a couple of theorems about evaluation-eq 746 747(local 748(defthm evaluation-eq-is-reflexive 749 (evaluation-eq x x vars)) 750) 751 752(local 753(defthm evaluation-eq-is-transitive 754 (implies (and (evaluation-eq p q vars) 755 (evaluation-eq q r vars)) 756 (evaluation-eq p r vars))) 757) 758 759;; Now to the argument. If r is in next states of p, then there is an equation 760;; taking p to r. 761 762;; We first prove that r is a valid next state of p. 763 764(local 765(defthm next-state-member-implies-consistent-equation 766 (implies (memberp r (create-next-states-of-p p states vars equations)) 767 (next-state-is-ok p r vars equations))) 768) 769 770;; Now if next-state-is-ok, then we know that there is a consistent equation 771;; that takes p to r. 772 773(local 774(defthm next-state-is-ok-to-consistent-p-equation 775 (implies (next-state-is-ok p r vars equations) 776 (consistent-p-equations 777 vars 778 (next-state-is-ok-witness p r vars equations) 779 equations))) 780) 781 782(local 783(defthm next-state-is-ok-p-to-actual 784 (implies (next-state-is-ok p r vars equations) 785 (evaluation-eq r (produce-next-state vars p 786 (next-state-is-ok-witness 787 p r vars equations)) 788 vars))) 789) 790 791(local 792(defthm thus-r-is-evaluation-eq-to-s 793 (implies (and (next-state-is-ok p r vars-orig equations-orig) 794 (evaluation-eq (produce-next-state vars-orig p 795 (next-state-is-ok-witness p r vars-orig 796 equations-orig)) 797 s 798 vars-cone) 799 (subset vars-cone vars-orig)) 800 (evaluation-eq r s vars-cone)) 801 :hints (("Goal" 802 :in-theory (disable next-state-is-ok-p-to-actual 803 evaluation-eq-subset-reduction 804 next-state-is-ok) 805 :do-not-induct t 806 :use ((:instance next-state-is-ok-p-to-actual 807 (vars vars-orig) 808 (equations equations-orig)) 809 (:instance evaluation-eq-subset-reduction 810 (p r) 811 (q (PRODUCE-NEXT-STATE 812 VARS-ORIG P 813 (NEXT-STATE-IS-OK-WITNESS P R VARS-ORIG 814 EQUATIONS-ORIG))) 815 (vars vars-orig) 816 (vars-prime vars-cone)))))) 817) 818 819;; Thus r is evaluation-eq with respect to s if we can show that 820;; produce-next-state produces something evaluation-eq to s. Now to show that 821;; this implies r is evaluation-eq-member-p of transition of q, we need to show 822;; that s is a member of states-cone and that there is a consistent equation 823;; with respect to cone that takes q to s. Let us see that this analysis is 824;; accurate. 825 826 827(local 828(defthm next-state-is-ok-from-consistent-eqn 829 (implies (and (consistent-p-equations vars eqn equations) 830 (evaluation-eq q (produce-next-state vars p eqn) vars)) 831 (next-state-is-ok p q vars equations))) 832) 833 834(local 835(in-theory (disable next-state-is-ok)) 836) 837 838(local 839(defthm memberp-of-next-state-from-consistent-equation 840 (implies (and (memberp s states-cone) 841 (next-state-is-ok q s vars-cone equations-cone)) 842 (memberp s (create-next-states-of-p q states-cone vars-cone 843 equations-cone)))) 844) 845 846(local 847(defthm memberp-not-using-next-states 848 (implies (and (memberp s states-cone) 849 (consistent-p-equations vars-cone eqn equations-cone) 850 (evaluation-eq s (produce-next-state vars-cone q eqn) vars-cone)) 851 (memberp s (create-next-states-of-p q states-cone vars-cone equations-cone)))) 852) 853 854;; OK, so now, how do we show that s is a member of states? This is because 855;; states are all-evaluations-p, and s is an evaluation-p as we will see. 856 857 858(local 859(defthm member-of-next-states-from-all-evaluations-p 860 (implies (and (all-evaluations-p states-cone vars-cone) 861 (evaluation-p s vars-cone) 862 (consistent-p-equations vars-cone eqn equations-cone) 863 (evaluation-eq s (produce-next-state vars-cone q eqn) vars-cone)) 864 (memberp 865 (evaluation-eq-member s states-cone vars-cone) 866 (create-next-states-of-p q states-cone vars-cone equations-cone))) 867 :hints (("Goal" 868 :do-not-induct t 869 :in-theory (disable memberp-not-using-next-states) 870 :use ((:instance memberp-not-using-next-states 871 (s (evaluation-eq-member s states-cone vars-cone))) 872 (:instance evaluation-eq-is-symmetric 873 (p s) 874 (q (evaluation-eq-member s states-cone vars-cone)) 875 (vars vars-cone)))))) 876) 877 878(local 879(defthm evaluation-eq-and-memberp-to-evaluation-eq-memberp 880 (implies (and (memberp q states) 881 (evaluation-eq p q vars)) 882 (evaluation-eq-member-p p states vars))) 883) 884 885(defthm evaluation-eq-memberp-from-all-evaluations-p 886 (implies (and (all-evaluations-p states-cone vars-cone) 887 (evaluation-p s vars-cone) 888 (consistent-p-equations vars-cone eqn equations-cone) 889 (evaluation-eq s (produce-next-state vars-cone q eqn) 890 vars-cone)) 891 (evaluation-eq-member-p 892 s (create-next-states-of-p q states-cone vars-cone equations-cone) 893 vars-cone)) 894 :hints (("Goal" 895 :do-not-induct t 896 :in-theory (disable 897 evaluation-eq-and-memberp-to-evaluation-eq-memberp) 898 :use ((:instance evaluation-eq-and-memberp-to-evaluation-eq-memberp 899 (q (evaluation-eq-member s states-cone vars-cone)) 900 (p s) 901 (vars vars-cone) 902 (states (create-next-states-of-p 903 q states-cone vars-cone 904 equations-cone))))))) 905 906(local 907(defthm evaluation-eq-and-memberp-to-memberp 908 (implies (and (evaluation-eq p q vars) 909 (evaluation-eq-member-p q states vars)) 910 (evaluation-eq-member-p p states vars))) 911) 912 913(local 914(defthm next-state-of-orig-to-evaluation-eq-member-p 915 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig 916 equations-orig)) 917 (evaluation-eq (produce-next-state vars-orig p 918 (next-state-is-ok-witness p r vars-orig 919 equations-orig)) 920 s 921 vars-cone) 922 (subset vars-cone vars-orig) 923 (all-evaluations-p states-cone vars-cone) 924 (evaluation-p s vars-cone) 925 (consistent-p-equations vars-cone eqn equations-cone) 926 (evaluation-eq s (produce-next-state vars-cone q eqn) 927 vars-cone)) 928 (evaluation-eq-member-p 929 r (create-next-states-of-p q states-cone vars-cone equations-cone) 930 vars-cone)) 931 :hints (("Goal" 932 :do-not-induct t 933 :in-theory (disable thus-r-is-evaluation-eq-to-s) 934 :use thus-r-is-evaluation-eq-to-s))) 935) 936 937;; The theorem above guarantees that if we can get an s and an eqn with the 938;; properties mentioned then we will be done. Our choice of s is 939;; (produce-next-state vars-cone q eqn). Hence the only thing to prove is that 940;; we can get a corresponding equation for s. 941 942(local 943(defun create-corresponding-equation (vars equation-record vars-prime eqn eq-rec) 944 (if (endp vars) eq-rec 945 (-> (create-corresponding-equation (rest vars) equation-record vars-prime 946 eqn eq-rec) 947 (first vars) 948 (if (memberp (first vars) vars-prime) 949 (<- eqn (first vars)) 950 (first (<- equation-record (first vars))))))) 951) 952 953;; OK, so why is this equation consistent with the cone? The argument is that 954;; the cone of influence is well-formed-equation-record-p, and equation-equal-p 955;; with respect to the variables of the cone. 956 957(local 958(defthm equation-equal-to-set-reduction 959 (implies (not (memberp v vars)) 960 (equal (equation-equal-p eqn-orig (-> eqn-cone v a) vars) 961 (equation-equal-p eqn-orig eqn-cone vars)))) 962) 963 964(local 965(defthm create-corresponding-equation-is-equation-equal 966 (implies (and (subset vars-cone vars-orig) 967 (uniquep vars-cone)) 968 (equation-equal-p eqn-orig (create-corresponding-equation 969 vars-cone eqn-cone 970 vars-orig eqn-orig eq-rec) 971 972 vars-cone))) 973) 974 975(local 976(defthm cons-consistent-eqn 977 (implies (and (consistent-p-equations vars eqn equation-record) 978 (memberp equation (<- equation-record v))) 979 (consistent-p-equations (cons v vars) (-> eqn v equation) 980 equation-record)) 981 :hints (("Subgoal *1/4" 982 :cases ((equal v (car vars)))))) 983) 984 985(local 986(defthm consistent-p-equation-memberp-reduction 987 (implies (and (consistent-p-equations vars eqn equations) 988 (memberp v vars)) 989 (memberp (<- eqn v) (<- equations v)))) 990) 991 992(local 993(defthm consistent-set-not-member 994 (implies (not (memberp v vars)) 995 (equal (consistent-p-equations vars (-> eqn v a) equations) 996 (consistent-p-equations vars eqn equations)))) 997) 998 999(local 1000(defthm equation-equal-p-to-consistent-equation 1001 (implies (and (equation-equal-p eqn-orig eqn-cone vars) 1002 (consistent-p-equations vars eqn eqn-orig)) 1003 (consistent-p-equations vars eqn eqn-cone))) 1004) 1005 1006(local 1007(defthm consistent-p-equations-to-consistent-p-equations 1008 (implies (and (consistent-p-equations vars-orig eqn eqn-orig) 1009 (cons-list-p vars-cone eqn-cone) 1010 (equation-equal-p eqn-orig eqn-cone vars-cone) 1011 (uniquep vars-orig) 1012 (uniquep vars-cone)) 1013 (consistent-p-equations 1014 vars-cone 1015 (create-corresponding-equation vars-cone eqn-cone vars-orig eqn 1016 eq-rec) 1017 eqn-cone)) 1018 :otf-flg t 1019 :hints (("Goal" 1020 :induct (create-corresponding-equation vars-cone eqn-cone 1021 vars-orig eqn eq-rec) 1022 :do-not '(eliminate-destructors generalize) 1023 :do-not-induct t))) 1024) 1025 1026;; OK so now we have created an equation eqn that is consistent with respect to 1027;; the cone. So the final proof requirement is that s is evaluation-eq to the 1028;; application of this equation. 1029 1030(local 1031(defun closed-eqn-record-p (eqn vars vars-prime) 1032 (if (endp vars) T 1033 (and (subset (find-variables (<- eqn (first vars))) vars-prime) 1034 (closed-eqn-record-p eqn (rest vars) vars-prime)))) 1035) 1036 1037;; This predicate ensures that the variables of eqn are subsets of 1038;; vars-prime. Now let us show that this notion follows from equation-record-p. 1039 1040(local 1041(defthm closed-eqn-record-p-from-consistent-equation-record-p 1042 (implies (and (consistent-equation-record-p vars-prime equations) 1043 (uniquep vars-prime) 1044 (subset vars vars-prime) 1045 (consistent-p-equations vars eqn equations)) 1046 (closed-eqn-record-p eqn vars vars-prime)) 1047 :hints (("Subgoal *1/5" 1048 :do-not '(eliminate-destructors generalize) 1049 :do-not-induct t))) 1050) 1051 1052;; And thus, by concretizing it, we have the following theorem: 1053 1054(local 1055(defthm closed-eqn-record-p-true-concretized 1056 (implies (and (consistent-equation-record-p vars equations) 1057 (uniquep vars) 1058 (consistent-p-equations vars eqn equations)) 1059 (closed-eqn-record-p eqn vars vars))) 1060) 1061 1062(local 1063(defthm apply-equation-produces-equal 1064 (implies (and (evaluation-p p vars) 1065 (evaluation-p q vars) 1066 (subset (find-variables equation) vars) 1067 (evaluation-eq p q vars)) 1068 (equal (apply-equation equation p) 1069 (apply-equation equation q))) 1070 :hints (("Goal" 1071 :induct (apply-equation equation p)))) 1072) 1073 1074(local 1075(defthm produce-next-state-not-memberp-vars-reduction 1076 (implies (not (memberp v vars)) 1077 (equal (<- (produce-next-state vars p equations) v) 1078 (<- p v)))) 1079) 1080 1081(local 1082(defthm produce-next-state-vars-reduction 1083 (implies (and (memberp v vars) 1084 (uniquep vars)) 1085 (equal (<- (produce-next-state vars p equations) v) 1086 (apply-equation (<- equations v) p)))) 1087) 1088 1089(local 1090(defthm evaluation-eq-set-reduction 1091 (implies (and (evaluation-eq p q vars) 1092 (not (memberp v vars))) 1093 (evaluation-eq (-> p v a) (-> q v b) vars))) 1094) 1095 1096(local 1097(defthm produce-next-state-is-evaluation-eq 1098 (implies (and (evaluation-p p vars-prime) 1099 (uniquep vars-prime) 1100 (evaluation-p q vars-prime) 1101 (uniquep vars-prime) 1102 (uniquep vars) 1103 (subset vars vars-prime) 1104 (evaluation-eq p q vars-prime) 1105 (closed-eqn-record-p eqn-cone vars vars-prime) 1106 (equation-equal-p eqn-orig eqn-cone vars)) 1107 (evaluation-eq 1108 (produce-next-state vars p eqn-orig) 1109 (produce-next-state vars q eqn-cone) 1110 vars)) 1111 :hints (("Goal" 1112 :do-not '(eliminate-destructors generalize) 1113 :in-theory (disable apply-equation-produces-equal)) 1114 ("Subgoal *1/6" 1115 :use ((:instance apply-equation-produces-equal 1116 (vars vars-prime) 1117 (equation (<- eqn-cone (first vars)))))))) 1118) 1119 1120(local 1121(defthm produce-next-state-is-evaluation-eq-concretized 1122 (implies (and (evaluation-p p vars-cone) 1123 (evaluation-p q vars-cone) 1124 (evaluation-eq p q vars-cone) 1125 (uniquep vars-cone) 1126 (consistent-equation-record-p vars-cone equations-cone) 1127 (consistent-p-equations vars-cone eqn-cone equations-cone) 1128 (equation-equal-p eqn-orig eqn-cone vars-cone)) 1129 (evaluation-eq 1130 (produce-next-state vars-cone p eqn-orig) 1131 (produce-next-state vars-cone q eqn-cone) 1132 vars-cone))) 1133) 1134 1135(local 1136(defthm produce-next-state-evaluation-eq-reduction 1137 (implies (and (uniquep vars-orig) 1138 (uniquep vars-cone) 1139 (subset vars-cone vars-orig)) 1140 (evaluation-eq (produce-next-state vars-orig p eqn-orig) 1141 (produce-next-state vars-cone p eqn-orig) 1142 vars-cone))) 1143) 1144 1145(local 1146(defthm produce-next-state-fully-concretized 1147 (implies (and (evaluation-p p vars-cone) 1148 (evaluation-p q vars-cone) 1149 (evaluation-eq p q vars-cone) 1150 (uniquep vars-orig) 1151 (uniquep vars-cone) 1152 (subset vars-cone vars-orig) 1153 (consistent-equation-record-p vars-cone equations-cone) 1154 (consistent-p-equations vars-cone eqn-cone equations-cone) 1155 (equation-equal-p eqn-orig eqn-cone vars-cone)) 1156 (evaluation-eq (produce-next-state vars-orig p eqn-orig) 1157 (produce-next-state vars-cone q eqn-cone) 1158 vars-cone)) 1159 :hints (("Goal" 1160 :do-not '(eliminate-destructors generalize) 1161 :do-not-induct t 1162 :in-theory (disable evaluation-eq-is-transitive 1163 produce-next-state-is-evaluation-eq-concretized) 1164 :use ((:instance produce-next-state-is-evaluation-eq-concretized) 1165 (:instance evaluation-eq-is-transitive 1166 (p (produce-next-state vars-orig p eqn-orig)) 1167 (q (produce-next-state vars-cone p eqn-orig)) 1168 (r (produce-next-state vars-cone q eqn-cone)) 1169 (vars vars-cone)))))) 1170) 1171 1172(local 1173(defthm produce-next-state-for-equation-of-choice 1174 (implies (and (evaluation-p p vars-cone) 1175 (evaluation-p q vars-cone) 1176 (evaluation-eq p q vars-cone) 1177 (cons-list-p vars-cone equations-cone) 1178 (uniquep vars-orig) 1179 (uniquep vars-cone) 1180 (equation-equal-p equations-orig equations-cone vars-cone) 1181 (consistent-p-equations vars-orig eqn-orig equations-orig) 1182 (consistent-equation-record-p vars-cone equations-cone) 1183 (subset vars-cone vars-orig)) 1184 (evaluation-eq 1185 (produce-next-state vars-orig p eqn-orig) 1186 (produce-next-state 1187 vars-cone q 1188 (create-corresponding-equation 1189 vars-cone equations-cone vars-orig eqn-orig eq-rec)) 1190 vars-cone))) 1191) 1192 1193(local 1194(in-theory (disable apply-equation-produces-equal)) 1195) 1196 1197(local 1198(defthm boolean-p-apply-equation 1199 (implies (and (evaluation-p p vars) 1200 (subset (find-variables equation) vars)) 1201 (booleanp (apply-equation equation p))) 1202 :hints (("Goal" 1203 :induct (apply-equation equation p)))) 1204) 1205 1206(local 1207(defthm evaluation-p-set-reduction 1208 (implies (and (booleanp a) 1209 (evaluation-p p vars)) 1210 (evaluation-p (-> p v a) vars)) 1211 :hints (("Subgoal *1/4" 1212 :cases ((equal v (car vars)))))) 1213) 1214 1215(local 1216(defthm produce-next-state-is-evaluation-p 1217 (implies (and (evaluation-p p vars-prime) 1218 (subset vars vars-prime) 1219 (uniquep vars) 1220 (uniquep vars-prime) 1221 (closed-eqn-record-p eqn vars vars-prime)) 1222 (evaluation-p (produce-next-state vars p eqn) vars-prime))) 1223) 1224 1225(local 1226(defthm next-state-is-evaluation-p-concretized 1227 (implies (and (evaluation-p p vars) 1228 (uniquep vars) 1229 (consistent-equation-record-p vars equations) 1230 (consistent-p-equations vars eqn equations)) 1231 (evaluation-p (produce-next-state vars p eqn) vars))) 1232) 1233 1234(local 1235(defthm r-is-evaluation-eq-member-p-with-respect-to-states 1236 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig 1237 equations-orig)) 1238 (evaluation-p p vars-cone) 1239 (evaluation-p q vars-cone) 1240 (evaluation-eq p q vars-cone) 1241 (consistent-equation-record-p vars-orig equations-orig) 1242 (subset vars-cone vars-orig) 1243 (evaluation-p p vars-orig) 1244 (uniquep vars-orig) 1245 (uniquep vars-cone) 1246 (cons-list-p vars-cone equations-cone) 1247 (equation-equal-p equations-orig equations-cone vars-cone) 1248 (consistent-equation-record-p vars-cone equations-cone) 1249 (all-evaluations-p states-cone vars-cone)) 1250 (evaluation-eq-member-p 1251 r (create-next-states-of-p q states-cone vars-cone equations-cone) 1252 vars-cone)) 1253 :otf-flg t 1254 :hints (("Goal" 1255 :do-not-induct t 1256 :in-theory (disable next-state-of-orig-to-evaluation-eq-member-p) 1257 :use ((:instance next-state-of-orig-to-evaluation-eq-member-p 1258 (s (produce-next-state vars-orig p 1259 (next-state-is-ok-witness p r vars-orig 1260 equations-orig))) 1261 (eqn (create-corresponding-equation 1262 vars-cone equations-cone vars-orig 1263 (next-state-is-ok-witness p r vars-orig 1264 equations-orig) 1265 eq-rec))))) 1266 ("Subgoal 2" 1267 :in-theory (disable evaluationp-for-subset 1268 next-state-is-evaluation-p-concretized) 1269 :use ((:instance next-state-is-evaluation-p-concretized 1270 (eqn (next-state-is-ok-witness 1271 p r vars-orig equations-orig)) 1272 (equations equations-orig) 1273 (vars vars-orig)) 1274 (:instance evaluationp-for-subset 1275 (st (PRODUCE-NEXT-STATE 1276 VARS-ORIG P 1277 (NEXT-STATE-IS-OK-WITNESS P R VARS-ORIG 1278 EQUATIONS-ORIG))) 1279 (variables vars-orig) 1280 (vars vars-cone)))) 1281 ("Subgoal 1" 1282 :in-theory (disable 1283 consistent-p-equations-to-consistent-p-equations) 1284 :use ((:instance consistent-p-equations-to-consistent-p-equations 1285 (eqn-orig equations-orig) 1286 (eqn-cone equations-cone) 1287 (eqn (next-state-is-ok-witness p r vars-orig 1288 equations-orig))))))) 1289 1290) 1291 1292(local 1293(defthm evaluation-eq-subset-p-orig->cone 1294 (implies (and (subset l (create-next-states-of-p p states-orig vars-orig 1295 equations-orig)) 1296 (evaluation-p p vars-cone) 1297 (evaluation-p q vars-cone) 1298 (evaluation-eq p q vars-cone) 1299 (consistent-equation-record-p vars-orig equations-orig) 1300 (subset vars-cone vars-orig) 1301 (evaluation-p p vars-orig) 1302 (uniquep vars-orig) 1303 (uniquep vars-cone) 1304 (cons-list-p vars-cone equations-cone) 1305 (equation-equal-p equations-orig equations-cone vars-cone) 1306 (consistent-equation-record-p vars-cone equations-cone) 1307 (all-evaluations-p states-cone vars-cone)) 1308 (evaluation-eq-subset-p 1309 l (create-next-states-of-p q states-cone vars-cone equations-cone) 1310 vars-cone))) 1311) 1312 1313(local 1314(defthm evaluation-eq-subset-orig->cone-concretized 1315 (implies (and (evaluation-p p vars-cone) 1316 (evaluation-p q vars-cone) 1317 (evaluation-eq p q vars-cone) 1318 (consistent-equation-record-p vars-orig equations-orig) 1319 (subset vars-cone vars-orig) 1320 (only-evaluations-p states-orig vars-orig) 1321 (memberp p states-orig) 1322 (uniquep vars-orig) 1323 (uniquep vars-cone) 1324 (cons-list-p vars-cone equations-cone) 1325 (equation-equal-p equations-orig equations-cone vars-cone) 1326 (consistent-equation-record-p vars-cone equations-cone) 1327 (all-evaluations-p states-cone vars-cone)) 1328 (evaluation-eq-subset-p 1329 (create-next-states-of-p p states-orig vars-orig 1330 equations-orig) 1331 (create-next-states-of-p q states-cone vars-cone equations-cone) 1332 vars-cone)) 1333 :hints (("Goal" 1334 :in-theory (disable evaluation-eq-subset-p-orig->cone) 1335 :use ((:instance evaluation-eq-subset-p-orig->cone 1336 (l (create-next-states-of-p p states-orig vars-orig 1337 equations-orig))))))) 1338) 1339 1340(local 1341(defthm equation-equal-is-symmetric 1342 (equal (equation-equal-p eqn-orig eqn-cone vars) 1343 (equation-equal-p eqn-cone eqn-orig vars)) 1344 :rule-classes nil) 1345) 1346 1347(local 1348(defthm equation-equal-to-set-reduction-2 1349 (implies (not (memberp v vars)) 1350 (equal (equation-equal-p (-> eqn-orig v a) eqn-cone vars) 1351 (equation-equal-p eqn-orig eqn-cone vars)))) 1352) 1353 1354(local 1355(defthm memberp-to-create-equation-reduction 1356 (implies (and (memberp v vars-cone) 1357 (memberp v vars-orig)) 1358 (equal (<- (create-corresponding-equation vars-orig eqn-orig 1359 vars-cone eqn-cone 1360 eq-rec) 1361 v) 1362 (<- eqn-cone v))) 1363 :hints (("Subgoal *1/3.2" 1364 :cases ((equal v (car vars-orig)))))) 1365) 1366 1367(local 1368(defthm not-memberp-to-create-equation 1369 (implies (not (memberp v vars-orig)) 1370 (equal (<- (create-corresponding-equation vars-orig eqn-orig 1371 vars-cone eqn-cone eq-rec) 1372 v) 1373 (<- eq-rec v)))) 1374) 1375 1376(local 1377(defthm memberp-equation-reduction-2 1378 (implies (and (not (memberp v vars-cone)) 1379 (memberp v vars-orig)) 1380 (equal (<- (create-corresponding-equation vars-orig eqn-orig 1381 vars-cone eqn-cone eq-rec) 1382 v) 1383 (first (<- eqn-orig v)))) 1384 :hints (("Subgoal *1/3" 1385 :cases ((equal v (car vars-orig)))))) 1386) 1387 1388(local 1389(defthm create-corresponding-equation-is-equation-equal-2 1390 (implies (and (subset vars-cone vars-orig) 1391 (subset vars vars-cone) 1392 (uniquep vars-orig) 1393 (uniquep vars-cone)) 1394 (equation-equal-p (create-corresponding-equation 1395 vars-orig eqn-orig 1396 vars-cone eqn-cone eq-rec) 1397 eqn-cone vars)) 1398 :otf-flg t 1399 :hints (("Goal" 1400 :do-not '(eliminate-destructors generalize)))) 1401) 1402 1403(local 1404(defthm produce-next-state-for-equation-of-choice-2 1405 (implies (and (evaluation-p p vars-cone) 1406 (evaluation-p q vars-cone) 1407 (evaluation-eq p q vars-cone) 1408 (cons-list-p vars-orig equations-orig) 1409 (uniquep vars-orig) 1410 (uniquep vars-cone) 1411 (equation-equal-p equations-orig equations-cone vars-cone) 1412 (consistent-p-equations vars-cone eqn-cone equations-cone) 1413 (consistent-equation-record-p vars-cone equations-cone) 1414 (consistent-equation-record-p vars-orig equations-orig) 1415 (subset vars-cone vars-orig)) 1416 (evaluation-eq 1417 (produce-next-state 1418 vars-orig p 1419 (create-corresponding-equation 1420 vars-orig equations-orig vars-cone eqn-cone eq-rec)) 1421 (produce-next-state vars-cone q eqn-cone) 1422 vars-cone))) 1423) 1424 1425(local 1426(defthm and-thus-for-vars-cone 1427 (implies (and (all-evaluations-p states-orig vars-orig) 1428 (evaluation-p r vars-orig) 1429 (subset vars-cone vars-orig) 1430 (consistent-p-equations vars-orig eqn equations-orig) 1431 (evaluation-eq r (produce-next-state vars-orig p eqn) 1432 vars-orig)) 1433 (evaluation-eq-member-p 1434 r (create-next-states-of-p p states-orig vars-orig equations-orig) 1435 vars-cone)) 1436 :hints (("Goal" 1437 :in-theory (disable evaluation-eq-member-subset-reduction) 1438 :use ((:instance evaluation-eq-member-subset-reduction 1439 (init r) 1440 (vars vars-orig) 1441 (vars-prime vars-cone) 1442 (inits (create-next-states-of-p 1443 p states-orig vars-orig 1444 equations-orig))))))) 1445) 1446 1447(local 1448(defthm thus-r-is-evaluation-eq-to-s-2 1449 (implies (and (next-state-is-ok q s vars-cone equations-cone) 1450 (evaluation-eq (produce-next-state 1451 vars-cone q 1452 (next-state-is-ok-witness q s vars-cone 1453 equations-cone)) 1454 r 1455 1456 vars-cone)) 1457 (evaluation-eq s r vars-cone)) 1458 :rule-classes nil) 1459) 1460 1461;; and then suitably polish it 1462 1463 1464(local 1465(defthm thus-polished-r-is-evaluation-eq-to-s-2 1466 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone 1467 equations-cone)) 1468 (evaluation-eq r (produce-next-state 1469 vars-cone q 1470 (next-state-is-ok-witness 1471 q s vars-cone equations-cone)) 1472 vars-cone)) 1473 (evaluation-eq r s vars-cone)) 1474 :hints (("Goal" 1475 :do-not-induct t 1476 :in-theory (disable next-state-is-ok 1477 next-state-member-implies-consistent-equation) 1478 :use ((:instance next-state-member-implies-consistent-equation 1479 (p q) 1480 (r s) 1481 (vars vars-cone) 1482 (states states-cone) 1483 (equations equations-cone)) 1484 (:instance thus-r-is-evaluation-eq-to-s-2) 1485 (:instance evaluation-eq-is-symmetric 1486 (p r) 1487 (q s) 1488 (vars vars-cone)) 1489 (:instance evaluation-eq-is-symmetric 1490 (p r) 1491 (vars vars-cone) 1492 (q (produce-next-state 1493 vars-cone q 1494 (next-state-is-ok-witness 1495 q s vars-cone equations-cone)))))))) 1496) 1497 1498(local 1499(defthm evaluation-eq-member-p-from-memberp 1500 (implies (and (evaluation-eq s r vars) 1501 (evaluation-eq-member-p r states vars)) 1502 (evaluation-eq-member-p s states vars))) 1503) 1504 1505(local 1506(defthm next-state-of-orig-to-evaluation-eq-member-p-2 1507 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone 1508 equations-cone)) 1509 (evaluation-eq r (produce-next-state 1510 vars-cone q 1511 (next-state-is-ok-witness q s vars-cone 1512 equations-cone)) 1513 vars-cone) 1514 (uniquep vars-orig) 1515 (uniquep vars-cone) 1516 (subset vars-cone vars-orig) 1517 (all-evaluations-p states-orig vars-orig) 1518 (evaluation-p r vars-orig) 1519 (consistent-p-equations vars-orig eqn equations-orig) 1520 (evaluation-eq r (produce-next-state vars-orig p eqn) 1521 vars-orig)) 1522 (evaluation-eq-member-p 1523 s (create-next-states-of-p p states-orig vars-orig equations-orig) 1524 vars-cone)) 1525 :hints (("Goal" 1526 :do-not-induct t 1527 :in-theory (disable ;; produce-next-state-evaluation-eq-reduction 1528 and-thus-for-vars-cone 1529 thus-polished-r-is-evaluation-eq-to-s-2) 1530 :use ((:instance thus-polished-r-is-evaluation-eq-to-s-2) 1531 (:instance and-thus-for-vars-cone) 1532 (:instance evaluation-eq-is-symmetric 1533 (p r) 1534 (q s) 1535 (vars vars-cone)))))) 1536) 1537 1538(local 1539(defthm consistent-p-equations-to-consistent-p-equations-2 1540 (implies (and (consistent-p-equations vars-cone eqn equations-cone) 1541 (cons-list-p vars-orig equations-orig) 1542 (equation-equal-p equations-orig equations-cone vars-cone) 1543 (uniquep vars-orig) 1544 (uniquep vars-cone)) 1545 (consistent-p-equations 1546 vars-orig 1547 (create-corresponding-equation 1548 vars-orig equations-orig vars-cone eqn eqn-rec) 1549 equations-orig)) 1550 :hints (("Goal" 1551 :induct (create-corresponding-equation 1552 vars-orig equations-orig vars-cone eqn eqn-rec) 1553 :do-not-induct t) 1554 ("Subgoal *1/2" 1555 :use ((:instance consistent-p-equation-memberp-reduction 1556 (vars vars-cone) 1557 (v (car vars-orig)) 1558 (equations equations-cone)))))) 1559) 1560 1561(local 1562(defthm next-state-cone->orig-thus-settled 1563 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone 1564 equations-cone)) 1565 (evaluation-p p vars-cone) 1566 (evaluation-p q vars-cone) 1567 (evaluation-eq p q vars-cone) 1568 (consistent-equation-record-p vars-orig equations-orig) 1569 (subset vars-cone vars-orig) 1570 (evaluation-p p vars-orig) 1571 (evaluation-p q vars-cone) 1572 (all-evaluations-p states-orig vars-orig) 1573 (uniquep vars-orig) 1574 (uniquep vars-cone) 1575 (cons-list-p vars-orig equations-orig) 1576 (equation-equal-p equations-orig equations-cone vars-cone) 1577 (consistent-equation-record-p vars-orig equations-orig) 1578 (consistent-equation-record-p vars-cone equations-cone) 1579 (all-evaluations-p states-cone vars-cone)) 1580 (evaluation-eq-member-p 1581 s (create-next-states-of-p p states-orig vars-orig equations-orig) 1582 vars-cone)) 1583 :otf-flg t 1584 :hints (("Goal" 1585 :do-not-induct t 1586 :in-theory (disable 1587 consistent-p-equations-to-consistent-p-equations-2 1588 next-state-of-orig-to-evaluation-eq-member-p-2) 1589 :use ((:instance next-state-of-orig-to-evaluation-eq-member-p-2 1590 (r (produce-next-state 1591 vars-orig p 1592 (create-corresponding-equation 1593 vars-orig equations-orig vars-cone 1594 (next-state-is-ok-witness q s vars-cone 1595 equations-cone) 1596 eq-rec))) 1597 (eqn (create-corresponding-equation 1598 vars-orig equations-orig vars-cone 1599 (next-state-is-ok-witness q s vars-cone 1600 equations-cone) 1601 eq-rec))) 1602 (:instance next-state-is-evaluation-p-concretized 1603 (vars vars-orig) 1604 (equations equations-orig) 1605 (eqn (create-corresponding-equation 1606 vars-orig equations-orig vars-cone 1607 (next-state-is-ok-witness q s vars-cone 1608 equations-cone) 1609 eq-rec))) 1610 (:instance consistent-p-equations-to-consistent-p-equations-2 1611 (eqn-rec eq-rec) 1612 (eqn (next-state-is-ok-witness q s vars-cone 1613 equations-cone))))))) 1614 1615) 1616 1617(local 1618(defthm next-state-cone->orig-concretized 1619 (implies (and (subset l (create-next-states-of-p q states-cone vars-cone 1620 equations-cone)) 1621 (evaluation-p p vars-cone) 1622 (evaluation-p q vars-cone) 1623 (evaluation-eq p q vars-cone) 1624 (consistent-equation-record-p vars-orig equations-orig) 1625 (subset vars-cone vars-orig) 1626 (evaluation-p p vars-orig) 1627 (evaluation-p q vars-cone) 1628 (all-evaluations-p states-orig vars-orig) 1629 (uniquep vars-orig) 1630 (uniquep vars-cone) 1631 (cons-list-p vars-orig equations-orig) 1632 (equation-equal-p equations-orig equations-cone vars-cone) 1633 (consistent-equation-record-p vars-orig equations-orig) 1634 (consistent-equation-record-p vars-cone equations-cone) 1635 (all-evaluations-p states-cone vars-cone)) 1636 (evaluation-eq-subset-p 1637 l (create-next-states-of-p p states-orig vars-orig equations-orig) 1638 vars-cone))) 1639) 1640 1641(local 1642(defthm and-fully-concretized-cone->orig 1643 (implies (and (evaluation-p p vars-cone) 1644 (evaluation-p q vars-cone) 1645 (evaluation-eq p q vars-cone) 1646 (consistent-equation-record-p vars-orig equations-orig) 1647 (subset vars-cone vars-orig) 1648 (only-evaluations-p states-orig vars-orig) 1649 (only-evaluations-p states-cone vars-cone) 1650 (memberp p states-orig) 1651 (memberp q states-cone) 1652 (evaluation-p q vars-cone) 1653 (all-evaluations-p states-orig vars-orig) 1654 (uniquep vars-orig) 1655 (uniquep vars-cone) 1656 (cons-list-p vars-orig equations-orig) 1657 (equation-equal-p equations-orig equations-cone vars-cone) 1658 (consistent-equation-record-p vars-orig equations-orig) 1659 (consistent-equation-record-p vars-cone equations-cone) 1660 (all-evaluations-p states-cone vars-cone)) 1661 (evaluation-eq-subset-p 1662 (create-next-states-of-p q states-cone vars-cone 1663 equations-cone) 1664 (create-next-states-of-p p states-orig vars-orig equations-orig) 1665 vars-cone)) 1666 :hints (("Goal" 1667 :in-theory (disable next-state-cone->orig-concretized) 1668 :use ((:instance next-state-cone->orig-concretized 1669 (l (create-next-states-of-p q states-cone vars-cone 1670 equations-cone))))))) 1671) 1672 1673(local 1674(in-theory (disable create-next-states-of-p)) 1675) 1676 1677(local 1678(defthm not-member-p-to-next-states 1679 (implies (not (memberp p states)) 1680 (equal (<- (create-next-states states states-prime vars equations) 1681 p) 1682 nil))) 1683) 1684 1685(local 1686(defthm create-next-states-to-next-state-of-p 1687 (implies (memberp p states) 1688 (equal (<- (create-next-states states states-prime vars equations) 1689 p) 1690 (create-next-states-of-p p states-prime vars equations))) 1691 :hints (("Subgoal *1/3" 1692 :cases ((equal p (car states)))))) 1693) 1694 1695(local 1696(defthm well-formed-transition-p-aux-orig->cone 1697 (implies (and (evaluation-p p vars-cone) 1698 (evaluation-p q vars-cone) 1699 (evaluation-eq p q vars-cone) 1700 (consistent-equation-record-p vars-orig equations-orig) 1701 (subset vars-cone vars-orig) 1702 (only-evaluations-p states-orig vars-orig) 1703 (memberp p states-orig) 1704 (uniquep vars-orig) 1705 (uniquep vars-cone) 1706 (cons-list-p vars-cone equations-cone) 1707 (memberp q states-cone) 1708 (only-evaluations-p states-cone vars-cone) 1709 (equation-equal-p equations-orig equations-cone vars-cone) 1710 (consistent-equation-record-p vars-cone equations-cone) 1711 (all-evaluations-p states-cone vars-cone)) 1712 (evaluation-eq-subset-p 1713 (<- (create-next-states states-orig states-orig vars-orig 1714 equations-orig) 1715 P) 1716 (<- (create-next-states states-cone states-cone vars-cone 1717 equations-cone) 1718 Q) 1719 vars-cone))) 1720) 1721 1722(local 1723(defthm well-formed-transition-p-aux-cone->orig 1724 (implies (and (evaluation-p p vars-cone) 1725 (evaluation-p q vars-cone) 1726 (evaluation-eq p q vars-cone) 1727 (consistent-equation-record-p vars-orig equations-orig) 1728 (subset vars-cone vars-orig) 1729 (only-evaluations-p states-orig vars-orig) 1730 (only-evaluations-p states-cone vars-cone) 1731 (memberp p states-orig) 1732 (memberp q states-cone) 1733 (evaluation-p q vars-cone) 1734 (all-evaluations-p states-orig vars-orig) 1735 (uniquep vars-orig) 1736 (uniquep vars-cone) 1737 (cons-list-p vars-orig equations-orig) 1738 (equation-equal-p equations-orig equations-cone vars-cone) 1739 (consistent-equation-record-p vars-orig equations-orig) 1740 (consistent-equation-record-p vars-cone equations-cone) 1741 (all-evaluations-p states-cone vars-cone)) 1742 (evaluation-eq-subset-p 1743 (<- (create-next-states states-cone states-cone vars-cone 1744 equations-cone) 1745 q) 1746 (<- (create-next-states states-orig states-orig vars-orig 1747 equations-orig) 1748 p) 1749 vars-cone))) 1750) 1751 1752(local 1753(defthm well-formed-transition-p-aux-cone->orig-concretized 1754 (implies (and (evaluation-p p vars-cone) 1755 (evaluation-p q vars-cone) 1756 (evaluation-eq q p vars-cone) 1757 (consistent-equation-record-p vars-orig equations-orig) 1758 (subset vars-cone vars-orig) 1759 (only-evaluations-p states-orig vars-orig) 1760 (only-evaluations-p states-cone vars-cone) 1761 (memberp p states-orig) 1762 (memberp q states-cone) 1763 (evaluation-p q vars-cone) 1764 (all-evaluations-p states-orig vars-orig) 1765 (uniquep vars-orig) 1766 (uniquep vars-cone) 1767 (cons-list-p vars-orig equations-orig) 1768 (equation-equal-p equations-orig equations-cone vars-cone) 1769 (consistent-equation-record-p vars-orig equations-orig) 1770 (consistent-equation-record-p vars-cone equations-cone) 1771 (all-evaluations-p states-cone vars-cone)) 1772 (evaluation-eq-subset-p 1773 (<- (create-next-states states-cone states-cone vars-cone 1774 equations-cone) 1775 q) 1776 (<- (create-next-states states-orig states-orig vars-orig 1777 equations-orig) 1778 p) 1779 vars-cone)) 1780 :hints (("Goal" 1781 :in-theory (disable and-fully-concretized-cone->orig 1782 evaluation-eq-subset-p 1783 evaluation-eq-member-p 1784 next-state-cone->orig-concretized 1785 well-formed-transition-p-aux-cone->orig) 1786 :use ((:instance well-formed-transition-p-aux-cone->orig) 1787 (:instance evaluation-eq-is-symmetric 1788 (vars vars-cone)))))) 1789) 1790 1791(local 1792(in-theory (disable create-all-evaluations find-all-variables 1793 only-evaluations-p 1794 all-evaluations-p 1795 strict-evaluation-p 1796 only-all-truths-p 1797 label-subset-vars 1798 transition-subset-p 1799 next-states-in-states 1800 cons-list-p 1801 consistent-equation-record-p 1802 uniquep 1803 subset 1804 find-all-equations create-label-fn)) 1805) 1806 1807(local 1808(in-theory (enable well-formed-transition-p)) 1809) 1810 1811(local 1812(defthm orig-cone-cone-is-well-formed-transition-p 1813 (implies (circuitp C) 1814 (well-formed-transition-p 1815 (states (create-kripke C)) 1816 (transition (create-kripke C)) 1817 (states 1818 (create-kripke 1819 (cone-of-influence-reduction C vars))) 1820 (transition 1821 (create-kripke 1822 (cone-of-influence-reduction C vars))) 1823 (cone-variables vars C))) 1824 :hints (("Goal" 1825 :do-not '(eliminate-destructors generalize fertilize) 1826 :do-not-induct t 1827 :in-theory (disable well-formed-transition-p-aux-orig->cone 1828 create-kripke-produces-circuit-model) 1829 :use ((:instance well-formed-transition-p-aux-orig->cone 1830 (states-orig (states (create-kripke C))) 1831 (states-cone (states 1832 (create-kripke 1833 (cone-of-influence-reduction 1834 C vars)))) 1835 (vars-orig (variables C)) 1836 (vars-cone (variables 1837 (cone-of-influence-reduction C vars))) 1838 (equations-orig (equations C)) 1839 (equations-cone (equations 1840 (cone-of-influence-reduction C 1841 vars))) 1842 (p (car (well-formed-transition-p-witness 1843 (states (create-kripke C)) 1844 (transition (create-kripke C)) 1845 (states (create-kripke 1846 (cone-of-influence-reduction C 1847 vars))) 1848 (transition 1849 (create-kripke 1850 (cone-of-influence-reduction C vars))) 1851 (variables (cone-of-influence-reduction C 1852 vars))))) 1853 (q (mv-nth 1 1854 (well-formed-transition-p-witness 1855 (states (create-kripke C)) 1856 (transition (create-kripke C)) 1857 (states (create-kripke 1858 (cone-of-influence-reduction C 1859 vars))) 1860 (transition 1861 (create-kripke 1862 (cone-of-influence-reduction C vars))) 1863 (variables (cone-of-influence-reduction C 1864 vars)))))) 1865 (:instance create-kripke-produces-circuit-model) 1866 (:instance create-kripke-produces-circuit-model 1867 (C (cone-of-influence-reduction C vars))) 1868 (:instance cone-of-influence-reduction-is-circuit-p))))) 1869) 1870 1871(local 1872(defthm cone-orig-is-well-formed-transition-p 1873 (implies (circuitp C) 1874 (well-formed-transition-p 1875 (states 1876 (create-kripke 1877 (cone-of-influence-reduction C vars))) 1878 (transition 1879 (create-kripke 1880 (cone-of-influence-reduction C vars))) 1881 (states (create-kripke C)) 1882 (transition (create-kripke C)) 1883 (cone-variables vars C))) 1884 :hints (("Goal" 1885 :do-not '(eliminate-destructors generalize fertilize) 1886 :do-not-induct t 1887 :in-theory (disable well-formed-transition-p-aux-orig->cone 1888 create-kripke-produces-circuit-model) 1889 :use ((:instance well-formed-transition-p-aux-cone->orig-concretized 1890 (states-orig (states (create-kripke C))) 1891 (states-cone (states 1892 (create-kripke 1893 (cone-of-influence-reduction 1894 C vars)))) 1895 (vars-orig (variables C)) 1896 (vars-cone (variables 1897 (cone-of-influence-reduction C vars))) 1898 (equations-orig (equations C)) 1899 (equations-cone (equations 1900 (cone-of-influence-reduction C 1901 vars))) 1902 (q (car (well-formed-transition-p-witness 1903 (states (create-kripke 1904 (cone-of-influence-reduction C vars))) 1905 (transition (create-kripke 1906 (cone-of-influence-reduction 1907 C vars))) 1908 (states (create-kripke C)) 1909 (transition (create-kripke C)) 1910 1911 (variables (cone-of-influence-reduction C 1912 vars))))) 1913 (p (mv-nth 1 1914 (well-formed-transition-p-witness 1915 (states (create-kripke 1916 (cone-of-influence-reduction C vars))) 1917 (transition (create-kripke 1918 (cone-of-influence-reduction 1919 C vars))) 1920 (states (create-kripke C)) 1921 (transition (create-kripke C)) 1922 (variables (cone-of-influence-reduction C 1923 vars)))))) 1924 1925 (:instance create-kripke-produces-circuit-model) 1926 (:instance create-kripke-produces-circuit-model 1927 (C (cone-of-influence-reduction C vars))) 1928 (:instance cone-of-influence-reduction-is-circuit-p))))) 1929) 1930 1931(local 1932(in-theory (disable well-formed-transition-p create-kripke 1933 cone-of-influence-reduction 1934 cone-variables 1935 circuit-modelp circuitp)) 1936) 1937 1938(local 1939(defthm cone-of-influence-is-c-bisimi-equiv 1940 (implies (circuitp C) 1941 (c-bisim-equiv (create-kripke C) 1942 (create-kripke (cone-of-influence-reduction C vars)) 1943 (cone-variables vars C)))) 1944) 1945 1946(local 1947(in-theory (disable c-bisim-equiv)) 1948) 1949 1950(local 1951(defthm restricted-formula-of-vars-is-also-true-for-subset 1952 (implies (and (restricted-formulap f vars) 1953 (subset vars vars-prime)) 1954 (restricted-formulap f vars-prime))) 1955) 1956 1957;; (DEFTHM cone-of-influence-reduction-is-sound 1958;; (implies (and (restricted-formulap f (cone-variables vars C)) 1959;; (circuitp C)) 1960;; (equal (ltl-semantics f 1961;; (create-kripke (cone-of-influence-reduction C 1962;; vars))) 1963;; (ltl-semantics f (create-kripke C)))) 1964;; :hints (("Goal" 1965;; :in-theory (disable restricted-formulap 1966;; circuit-bisim-implies-same-ltl-semantics) 1967;; :use ((:instance circuit-bisim-implies-same-ltl-semantics 1968;; (n (create-kripke (cone-of-influence-reduction C 1969;; vars))) 1970;; (m (create-kripke C)) 1971;; (vars (cone-variables vars C))))))) 1972 1973;; ;; So we are done. Let us prove a couple of handy theorems. 1974 1975;; (DEFTHM cone-of-influence-reduction-is-sound-generalized 1976;; (implies (and (subset interesting-vars (cone-variables vars C)) 1977;; (circuitp C) 1978;; (restricted-formulap f interesting-vars)) 1979;; (equal (ltl-semantics f (create-kripke 1980;; (cone-of-influence-reduction C vars))) 1981;; (ltl-semantics f (create-kripke C))))) 1982 1983 1984;; The following two theorems were non-locally stated on Sat Nov 8 1985;; 14:25:28 2008 (after commenting out the above). These are the 1986;; theorems about cone of influence reduction that justify the 1987;; bisimulation. 1988 1989(defthm cone-of-influence-reduction-is-circuit-p 1990 (implies (circuitp C) 1991 (circuitp (cone-of-influence-reduction C vars))) 1992 :hints (("Goal" 1993 :in-theory (disable circuitp cone-of-influence-reduction) 1994 :expand (circuitp (cone-of-influence-reduction C vars))))) 1995 1996 1997(defthm cone-of-influence-is-c-bisimi-equiv 1998 (implies (circuitp C) 1999 (c-bisim-equiv (create-kripke C) 2000 (create-kripke (cone-of-influence-reduction C vars)) 2001 (cone-variables vars C)))) 2002 2003 2004 2005 2006