1(in-package "ACL2") 2 3#| 4 5 circuits.lisp 6 ~~~~~~~~~~~~~ 7 8In this book, we discuss a procedure to construct Kripke Structures from 9"circuit descriptions. A circuit in our world is a collection of variables, a 10collection of equations, and a collection of equations. An equation is a 11boolean evaluator of the current circuit valuaes producing the next state 12function. We show that under certain "well-formed-ness constraints", our 13procedure produces a valid model, in terms of the circuit-modelp predicate 14defined earlier. 15 16|# 17 18 19(include-book "circuit-bisim") 20 21 22;; A circuit is a collection of variables, equations and initial states. We 23;; will add equations to the macros, and tell you what is a good circuit. 24 25(defmacro equations (c) `(<- ,c :equations)) 26 27;; Now we define what it means for the equations to be consistent with the 28;; variables of the circuit. 29 30(defun find-variables (equation) 31 (cond ((and (atom equation) (not (booleanp equation))) 32 (list equation)) 33 ((and (equal (len equation) 3) (memberp (second equation) '(& +))) 34 (set-union (find-variables (first equation)) 35 (find-variables (third equation)))) 36 ((and (equal (len equation) 2) (equal (first equation) '~)) 37 (find-variables (second equation))) 38 (t nil))) 39 40(defun-sk consistent-equation-record-p (vars equations) 41 (forall (v equation) 42 (implies (and (uniquep vars) 43 (memberp v vars) 44 (memberp equation (<- equations v))) 45 (subset (find-variables equation) vars)))) 46 47(defun cons-list-p (vars equations) 48 (if (endp vars) T 49 (and (consp (<- equations (first vars))) 50 (cons-list-p (rest vars) equations)))) 51 52;; OK, now let us define the function circuitp. 53 54(defun circuitp (C) 55 (and (only-evaluations-p (initial-states C) (variables C)) 56 (strict-evaluation-list-p (variables C) (initial-states C)) 57 (uniquep (variables C)) 58 (cons-list-p (variables C) (equations C)) 59 (consistent-equation-record-p (variables C) (equations C)))) 60 61;; Now let us try to create a Kripke Structure from the circuit. We need to 62;; show that under (circuitp C), the kripke structure we produce is a 63;; circuit-model-p. 64 65(defun assign-T (v states) 66 (if (endp states) nil 67 (cons (-> (first states) v T) 68 (assign-T v (rest states))))) 69 70(defun assign-nil (v states) 71 (if (endp states) nil 72 (cons (-> (first states) v nil) 73 (assign-nil v (rest states))))) 74 75;; Now we create all the states of the model. 76 77(defun create-all-evaluations (vars states) 78 (if (endp vars) states 79 (let ((rec-states (create-all-evaluations (cdr vars) states))) 80 (append (assign-t (car vars) rec-states) 81 (assign-nil (car vars) rec-states))))) 82 83;; Now let us create the label function. 84 85(defun label-fn-of-st (st vars) 86 (if (endp vars) nil 87 (if (equal (<- st (first vars)) T) 88 (cons (first vars) 89 (label-fn-of-st st (rest vars))) 90 (label-fn-of-st st (rest vars))))) 91 92(defun create-label-fn (states vars label) 93 (if (endp states) label 94 (create-label-fn (rest states) vars 95 (-> label (first states) 96 (label-fn-of-st (first states) vars))))) 97 98;; And finally the transitions. 99 100(defun apply-equation (equation st) 101 (cond ((atom equation) (if (booleanp equation) 102 equation 103 (<- st equation))) 104 ((equal (len equation) 2) 105 (case (first equation) 106 (~ (not (apply-equation (second equation) st))) 107 (t nil))) 108 ((equal (len equation) 3) 109 (case (second equation) 110 (& (and (apply-equation (first equation) st) 111 (apply-equation (third equation) st))) 112 (+ (or (apply-equation (first equation) st) 113 (apply-equation (third equation) st))) 114 (t nil))) 115 (t nil))) 116 117(defun produce-next-state (vars st equations) 118 (if (endp vars) st 119 (-> (produce-next-state (rest vars) st equations) 120 (first vars) 121 (apply-equation (<- equations (first vars)) st)))) 122 123(defun consistent-p-equations (vars eqn equations) 124 (if (endp vars) T 125 (and (memberp (<- eqn (first vars)) (<- equations (first vars))) 126 (consistent-p-equations (rest vars) eqn equations)))) 127 128(defun-sk next-state-is-ok (p q vars equations) 129 (exists eqn (and (consistent-p-equations vars eqn equations) 130 (evaluation-eq q (produce-next-state vars p eqn) vars)))) 131 132(defun create-next-states-of-p (p states vars equations) 133 (if (endp states) nil 134 (if (next-state-is-ok p (first states) vars equations) 135 (cons (first states) (create-next-states-of-p 136 p (rest states) vars equations)) 137 (create-next-states-of-p p (rest states) vars equations)))) 138 139(defun create-next-states (states states-prime vars equations) 140 (if (endp states) () 141 (-> 142 (create-next-states (rest states) states-prime vars equations) 143 (first states) 144 (create-next-states-of-p (first states) states-prime vars equations)))) 145 146(defun create-kripke (C) 147 (let ((vars (variables C)) 148 (equations (equations C)) 149 (initial-states (initial-states C))) 150 (let* ((states (create-all-evaluations vars (list ()))) 151 (label-fn (create-label-fn (set-union initial-states states) vars ())) 152 (transition (create-next-states (set-union initial-states states) 153 (set-union initial-states states) 154 vars equations))) 155 (>_ :states (set-union initial-states states) 156 :initial-states initial-states 157 :label-fn label-fn 158 :transition transition 159 :variables vars)))) 160 161 162;; Since I have defined the Kripke model for a circuit, let us prove that it is 163;; a circuit-model-p. 164 165;; We start with the initial states. 166 167;; The theorem that initial-states are subsets of states is trivial by 168;; union. So there is nothing to prove. 169 170(local 171(defthm initial-states-are-subset-of-states 172 (subset (initial-states (create-kripke C)) (states (create-kripke C)))) 173) 174 175;; END of proofs on initial-states. 176 177;; OK, let us prove that create-label-fn is a valid label function. 178 179(local 180(defthm label-fn-is-subset 181 (subset (label-fn-of-st st vars) vars)) 182) 183 184(local 185(defthm label-fn-of-st-is-truth-p-label 186 (truthp-label (label-fn-of-st st vars) st)) 187) 188 189(local 190(defthm label-fn-of-st-is-all-truths-p-label 191 (all-truthsp-label (label-fn-of-st st vars) st vars)) 192) 193 194(local 195(defun abs-only-all-truths-p (states label vars) 196 (if (endp states) T 197 (and (all-truthsp-label (<- label (first states)) (first states) vars) 198 (abs-only-all-truths-p (rest states) label vars)))) 199) 200 201(local 202(defthm abs-concrete-only-all-truthsp-reduction 203 (equal (only-all-truths-p states m vars) 204 (abs-only-all-truths-p states (label-fn m) vars)) 205 :hints (("Goal" 206 :in-theory (enable label-of)))) 207) 208 209;; And now let us just prove abs-all-truthsp-label for the label-fn 210 211 212(local 213(defthm create-label-fn-does-not-mess-with-non-members 214 (implies (not (memberp s states)) 215 (equal (<- (create-label-fn states vars label) s) 216 (<- label s)))) 217) 218 219(local 220(defthm create-label-fn-creates-an-all-truthsp-label 221 (implies (memberp s states) 222 (equal (<- (create-label-fn states vars label) s) 223 (label-fn-of-st s vars)))) 224) 225 226(local 227(defthm label-fn-is-abs-only--all-truthsp 228 (abs-only-all-truths-p states (create-label-fn states vars label) vars) 229 :hints (("Subgoal *1/3" 230 :cases ((memberp (car states) (cdr states))) 231 :do-not-induct t))) 232) 233 234(local 235(defthm label-fn-is-only-all-truthsp 236 (only-all-truths-p (states (create-kripke C)) (create-kripke C) 237 (variables C))) 238) 239 240(local 241(in-theory (disable abs-concrete-only-all-truthsp-reduction)) 242) 243 244(local 245(defun abs-label-subset-vars (states label vars) 246 (if (endp states) T 247 (and (subset (<- label (first states)) vars) 248 (abs-label-subset-vars (rest states) label vars)))) 249) 250 251(local 252(defthm abs-label-subset-vars-is-same-as-concrete 253 (equal (label-subset-vars states m vars) 254 (abs-label-subset-vars states (label-fn m) vars)) 255 :hints (("Goal" 256 :in-theory (enable label-of)))) 257) 258 259(local 260(defthm create-label-fn-is-abs-label-subset-vars 261 (abs-label-subset-vars states (create-label-fn states vars label) vars) 262 :hints (("Subgoal *1/3" 263 :cases ((memberp (car states) (cdr states))) 264 :do-not-induct t))) 265) 266 267(local 268(defthm label-fn-is-label-subset-vars 269 (label-subset-vars (states (create-kripke C)) (create-kripke C) (variables 270 C))) 271) 272 273(local 274(in-theory (disable abs-label-subset-vars-is-same-as-concrete)) 275) 276 277(local 278(defun abs-only-truth-p (states label) 279 (if (endp states) T 280 (and (truthp-label (<- label (first states)) (first states)) 281 (abs-only-truth-p (rest states) label)))) 282) 283 284(local 285(defthm only-truth-p-abs-reduction 286 (equal (only-truth-p states m) 287 (abs-only-truth-p states (label-fn m))) 288 :hints (("Goal" 289 :in-theory (enable label-of)))) 290) 291 292(local 293(defthm label-fn-is-abs-only-truth-p 294 (abs-only-truth-p states (create-label-fn states vars label)) 295 :hints (("Subgoal *1/3" 296 :cases ((memberp (car states) (cdr states)))))) 297) 298 299(local 300(defthm label-fn-is-only-truth-p 301 (only-truth-p (states (create-kripke C)) (create-kripke C))) 302) 303 304(local 305(in-theory (disable only-truth-p-abs-reduction)) 306) 307 308;; END of proofs for label function. 309 310;; Let us now work with the transition function. 311 312(local 313(defthm create-next-states-is-subset-of-states-aux 314 (implies (memberp q (create-next-states-of-p p states vars equations)) 315 (memberp q states))) 316) 317 318(local 319(defthm create-next-states-of-p-subset-helper 320 (implies (subset states-prime (create-next-states-of-p p states vars 321 equations)) 322 (subset states-prime states))) 323) 324 325 326(local 327(defthm create-next-states-is-subset-of-states 328 (subset (create-next-states-of-p p states vars equations) 329 states) 330 :hints (("Goal" 331 :use ((:instance create-next-states-of-p-subset-helper 332 (states-prime (create-next-states-of-p p states 333 vars equations))))))) 334) 335 336(local 337(defthm not-memberp-next-states-reduction 338 (implies (not (memberp s states)) 339 (equal (<- (create-next-states states states-prime vars equations) 340 s) 341 nil))) 342) 343 344(local 345(defthm memberp-next-state-reduction 346 (implies (memberp s states) 347 (equal (<- (create-next-states states states-prime vars equations) 348 s) 349 (create-next-states-of-p s states-prime vars equations))) 350 :hints (("Subgoal *1/3" 351 :cases ((equal s (car states)))))) 352) 353 354(local 355(defthm transition-subset-p-for-next-state 356 (transition-subset-p states states-prime 357 (create-next-states states states-prime vars 358 equations)) 359 :otf-flg t 360 :hints (("Subgoal *1/2" 361 :cases ((memberp (car states) (cdr states))))))) 362 363(local 364(defthm transition-subset-p-holds-for-kripke 365 (transition-subset-p (states (create-kripke C)) 366 (states (create-kripke C)) 367 (transition (create-kripke C)))) 368) 369 370(local 371(defthm next-states-in-states-concretized 372 (equal (next-states-in-states m states) 373 (transition-subset-p states (states m) (transition m))) 374 :hints (("Goal" 375 :in-theory (enable next-states-in-states)))) 376) 377 378(local 379(defthm next-states-in-states-holds-for-create-kripke 380 (next-states-in-states (create-kripke C) (states (create-kripke C)))) 381) 382 383 384;; END of proofs for transition function. 385 386;; BEGIN proofs for states 387 388;; first states is a consp 389 390(local 391(defthm consp-states-for-consp-vars 392 (implies (consp states) 393 (consp (create-all-evaluations vars states)))) 394) 395 396;; The following theorem is a hack. This theorem is known as a 397;; type-prescription rule for append. Unfortunately, we need it as a rewrite 398;; rule. 399 400(local 401(in-theory (enable set-union)) 402) 403 404(local 405(defthm consp-union-reduction 406 (implies (consp y) 407 (consp (set-union x y)))) 408) 409 410(local 411(defthm create-kripke-is-consp-states 412 (consp (states (create-kripke C)))) 413) 414 415;; OK let us prove that everything is boolean with create-all-evaluations 416 417(local 418(defthm only-evaluations-p-union-reduction 419 (implies (and (only-evaluations-p init vars) 420 (only-evaluations-p states vars)) 421 (only-evaluations-p (set-union init states) vars))) 422) 423 424;; OK that takes care of the set-union part. Now we only need to show the 425;; create-all-evaluations produces only-evaluations-p 426 427(local 428(defun boolean-p-states (v states) 429 (if (endp states) T 430 (and (booleanp (<- (first states) v)) 431 (boolean-p-states v (rest states))))) 432) 433 434(local 435(defun boolean-list-p-states (vars states) 436 (if (endp vars) T 437 (and (boolean-p-states (first vars) states) 438 (boolean-list-p-states (rest vars) states)))) 439) 440 441;; Now can we prove that boolean-p-states holds for create-all-evaluations? 442 443(local 444(defthm assign-t-produces-boolean-p 445 (boolean-p-states v (assign-T v states))) 446) 447 448(local 449(defthm assign-nil-produces-boolean-p 450 (boolean-p-states v (assign-nil v states))) 451) 452 453(local 454(defthm assign-T-remains-same-for-not-v 455 (implies (not (equal v v-prime)) 456 (equal (boolean-p-states v (assign-T v-prime states)) 457 (boolean-p-states v states)))) 458) 459 460(local 461(defthm assign-nil-remains-same-for-not-v 462 (implies (not (equal v v-prime)) 463 (equal (boolean-p-states v (assign-nil v-prime states)) 464 (boolean-p-states v states)))) 465) 466 467(local 468(defthm boolean-p-append-reduction 469 (equal (boolean-p-states v (append states states-prime)) 470 (and (boolean-p-states v states) 471 (boolean-p-states v states-prime)))) 472) 473 474(local 475(defthm boolean-p-create-non-member-reduction 476 (implies (not (memberp v vars)) 477 (equal (boolean-p-states v (create-all-evaluations vars states)) 478 (boolean-p-states v states))) 479 :hints (("Goal" 480 :induct (create-all-evaluations vars states) 481 :do-not-induct t))) 482) 483 484(local 485(defthm create-all-evaluations-for-member-is-boolean 486 (implies (memberp v vars) 487 (boolean-p-states v (create-all-evaluations vars states))) 488 :hints (("Goal" 489 :induct (create-all-evaluations vars states) 490 :do-not-induct t) 491 ("Subgoal *1/2" 492 :cases ((equal v (car vars)))))) 493) 494 495(local 496(defthm create-all-evaluations-is-boolean-list-p-aux 497 (implies (subset vars vars-prime) 498 (boolean-list-p-states vars 499 (create-all-evaluations vars-prime states)))) 500) 501 502(local 503(defthm create-all-evaluations-is-boolean-list-p 504 (boolean-list-p-states vars (create-all-evaluations vars states))) 505) 506 507;; Can we prove that if we produce a boolean list then it is an evaluation? 508 509(local 510(defun evaluation-witness-variable (vars st) 511 (if (endp vars) nil 512 (if (not (booleanp (<- st (first vars)))) 513 (first vars) 514 (evaluation-witness-variable (rest vars) st)))) 515) 516 517(local 518(defthm evaluation-p-from-witness 519 (implies (booleanp (<- st (evaluation-witness-variable vars st))) 520 (evaluation-p st vars))) 521) 522 523(local 524(defthm boolean-list-p-to-boolean-vars 525 (implies (and (boolean-list-p-states vars states) 526 (memberp v vars)) 527 (boolean-p-states v states))) 528) 529 530(local 531(defthm boolean-p-states-implies-boolean-v 532 (implies (and (boolean-p-states v states) 533 (memberp st states)) 534 (booleanp (<- st v)))) 535) 536 537(local 538(defthm boolean-p-states-to-evaluation-p 539 (implies (and (boolean-list-p-states vars states) 540 (memberp st states)) 541 (evaluation-p st vars))) 542) 543 544(local 545(defthm boolean-p-states-to-only-evaluation-p-aux 546 (implies (and (boolean-list-p-states vars states) 547 (subset states-prime states)) 548 (only-evaluations-p states-prime vars))) 549) 550 551(local 552(defthm boolean-p-states-to-only-evaluations-p 553 (implies (boolean-list-p-states vars states) 554 (only-evaluations-p states vars))) 555) 556 557(local 558(defthm create-all-evaluations-is-only-evaluations-p 559 (only-evaluations-p (create-all-evaluations vars states) vars)) 560) 561 562(local 563(defthm create-kripke-is-only-evaluations-p 564 (implies (circuitp C) 565 (only-evaluations-p (states (create-kripke C)) (variables C)))) 566) 567 568;; The final predicate is all-evaluations-p. This is tricky, since it is 569;; defined using defun-sk. We try to create a witness for all-evaluations-p. 570 571(local 572(defun find-matching-states (st vars states) 573 (cond ((endp vars) states) 574 ((equal (<- st (first vars)) T) 575 (assign-t (first vars) 576 (find-matching-states st (rest vars) states))) 577 (t (assign-nil (first vars) 578 (find-matching-states st (rest vars) states))))) 579) 580 581;; Let us first prove find-matching-states is a consp 582 583(local 584(defthm find-matching-states-is-consp 585 (implies (consp states) 586 (consp (find-matching-states st vars states)))) 587) 588 589;; Now let us prove that for every member of find-matching-states it is 590;; evaluation-eq to st. 591 592(local 593(defthm nth-member-reduction 594 (implies (and (< i (len x)) 595 (consp x)) 596 (memberp (nth i x) x))) 597) 598 599(local 600(defthm nth-member-reduction-2 601 (implies (and (>= i (len x)) 602 (integerp i)) 603 (equal (nth i x) nil)) 604 :hints (("Goal" 605 :in-theory (enable zp)))) 606) 607 608(local 609(defthm assign-nil-produces-nil-member 610 (implies (memberp q (assign-nil v states)) 611 (equal (<- q v) nil))) 612) 613 614(local 615(defthm assign-t-produces-t-member 616 (implies (memberp q (assign-t v states)) 617 (equal (<- q v) t))) 618) 619 620(local 621(defthm assign-nil-produces-nil 622 (implies (and (consp states) 623 (integerp i)) 624 (not (<- (nth i (assign-nil v states)) v))) 625 :otf-flg t 626 :hints (("Goal" 627 :cases ((>= i (len (assign-nil v states)))) 628 :do-not-induct t) 629 ("Subgoal 2" 630 :in-theory (disable nth-member-reduction) 631 :use ((:instance nth-member-reduction 632 (x (assign-nil v states))))))) 633) 634 635(local 636(defthm assign-t-has-same-len 637 (equal (len (assign-t v states)) 638 (len states))) 639) 640 641(local 642(defthm assign-nil-has-same-len 643 (equal (len (assign-nil v states)) 644 (len states))) 645) 646 647(local 648(defthm len-consp-reduction 649 (implies (and (equal (len x) (len y)) 650 (consp x)) 651 (consp y))) 652) 653 654(local 655(defthm assign-t-produces-t 656 (implies (and (consp states) 657 (< i (len states)) 658 (integerp i)) 659 (equal (<- (nth i (assign-t v states)) v) t)) 660 :otf-flg t 661 :hints (("Goal" 662 :in-theory (disable nth-member-reduction) 663 :use ((:instance nth-member-reduction 664 (x (assign-t v states))))))) 665) 666 667(local 668(defthm assign-t-does-not-fuss 669 (implies (and (consp states) 670 (< i (len states)) 671 (integerp i) 672 (not (equal v v-prime))) 673 (equal (<- (nth i (assign-t v states)) v-prime) 674 (<- (nth i states) v-prime)))) 675) 676 677(local 678(defthm assign-nil-does-not-fuss 679 (implies (and (consp states) 680 (< i (len states)) 681 (integerp i) 682 (not (equal v v-prime))) 683 (equal (<- (nth i (assign-nil v states)) v-prime) 684 (<- (nth i states) v-prime)))) 685) 686 687(local 688(defthm len-of-find-matching-states-is-same 689 (equal (len (find-matching-states st vars states)) 690 (len states))) 691) 692 693(local 694(defthm find-matching-state-produces-equivalent-assignment 695 (implies (and (memberp v vars) 696 (consp states) 697 (integerp i) 698 (< i (len states)) 699 (evaluation-p st vars)) 700 (equal (<- (nth i (find-matching-states st vars states)) v) 701 (<- st v))) 702 :otf-flg t 703 :hints (("Goal" 704 :induct (find-matching-states st vars states) 705 :do-not '(eliminate-destructors generalize) 706 :do-not-induct t) 707 ("Subgoal *1/3.1" 708 :cases ((equal v (car vars)))) 709 ("Subgoal *1/2.1" 710 :cases ((equal v (car vars)))))) 711) 712 713(local 714(defun falsifier-evaluation-eq (p q vars) 715 (if (endp vars) nil 716 (if (not (equal (<- p (first vars)) 717 (<- q (first vars)))) 718 (first vars) 719 (falsifier-evaluation-eq p q (rest vars))))) 720) 721 722(local 723(defthm falsifier-means-evaluation-eq 724 (implies (equal (<- p (falsifier-evaluation-eq p q vars)) 725 (<- q (falsifier-evaluation-eq p q vars))) 726 (evaluation-eq p q vars))) 727) 728 729(local 730(defthm falsifier-not-member-to-evaluation-eq 731 (implies (not (memberp (falsifier-evaluation-eq p q vars) vars)) 732 (evaluation-eq p q vars))) 733) 734 735(local 736(defthm find-matching-states-evaluation-eq 737 (implies (and (consp states) 738 (integerp i) 739 (< i (len states)) 740 (evaluation-p st vars)) 741 (evaluation-eq (nth i (find-matching-states st vars states)) 742 st vars)) 743 :hints (("Goal" 744 :cases ((not (memberp 745 (falsifier-evaluation-eq 746 (nth i (find-matching-states st vars states)) 747 st vars) 748 vars)))))) 749) 750 751(local 752 (defthm len-not-consp 753 (implies (equal (len x) 0) 754 (not (consp x))) 755 :rule-classes :forward-chaining)) 756 757(local 758(defthm find-matching-is-evaluation-eq-concretized 759 (implies (and (consp states) 760 (evaluation-p st vars)) 761 (evaluation-eq (car (find-matching-states st vars states)) 762 st vars)) 763 :hints (("Goal" 764 :in-theory (disable find-matching-states-evaluation-eq) 765 :use ((:instance find-matching-states-evaluation-eq 766 (i 0)))))) 767) 768 769(local 770(defthm memberp-append-reduction 771 (equal (memberp a (append x y)) 772 (or (memberp a x) 773 (memberp a y)))) 774) 775 776(local 777(defthm member-assign-t-reduction 778 (implies (memberp e x) 779 (memberp (-> e v t) 780 (assign-t v x)))) 781) 782 783(local 784(defthm assign-t-subset-reduction 785 (implies (subset x y) 786 (subset (assign-t v x) 787 (assign-t v y)))) 788) 789 790(local 791(defthm member-assign-nil-reduction 792 (implies (memberp e x) 793 (memberp (-> e v nil) 794 (assign-nil v x)))) 795) 796 797(local 798(defthm assign-nil-subset-reduction 799 (implies (subset x y) 800 (subset (assign-nil v x) 801 (assign-nil v y)))) 802) 803 804(local 805(defthm append-subset-reduction-1 806 (implies (subset x y) 807 (subset x (append y z)))) 808) 809 810(local 811(defthm append-subset-reduction-2 812 (implies (subset x y) 813 (subset x (append z y)))) 814) 815 816(local 817(defthm find-matching-subset-reduction 818 (subset (find-matching-states st vars states) 819 (create-all-evaluations vars states))) 820) 821 822(local 823(defthm car-of-find-matching-is-member-of-all-evaluations 824 (implies (consp states) 825 (memberp (car (find-matching-states st vars states)) 826 (create-all-evaluations vars states)))) 827) 828 829(local 830(defthm evaluation-eq-memberp-from-memberp 831 (implies (and (evaluation-eq p q vars) 832 (memberp q states)) 833 (evaluation-eq-member-p p states vars))) 834) 835 836(local 837(defthm evalaution-eq-symmetry-hack 838 (implies (and (evaluation-eq p q vars) 839 (memberp p states)) 840 (evaluation-eq-member-p q states vars)) 841 :hints (("Goal" 842 :in-theory (disable evaluation-eq evaluation-eq-member-p 843 evaluation-eq-memberp-from-memberp) 844 :use ((:instance evaluation-eq-memberp-from-memberp 845 (p q) 846 (q p)) 847 (:instance evaluation-eq-is-symmetric))))) 848) 849 850(local 851(in-theory (disable evaluation-eq-memberp-from-memberp)) 852) 853 854(local 855(defthm create-all-evaluations-is-evaluation-eq-memberp 856 (implies (and (evaluation-p st vars) 857 (consp states)) 858 (evaluation-eq-member-p st (create-all-evaluations vars states) 859 vars)) 860 :hints (("Goal" 861 :do-not '(eliminate-destructors generalize) 862 :do-not-induct t 863 :in-theory (disable evalaution-eq-symmetry-hack) 864 :use ((:instance evalaution-eq-symmetry-hack 865 (q st) 866 (states (create-all-evaluations vars states)) 867 (p (car (find-matching-states st vars 868 states)))))))) 869) 870 871(local 872(defthm consp-states-to-all-evaluations-p 873 (implies (consp states) 874 (all-evaluations-p (create-all-evaluations vars states) vars)) 875 :hints (("Goal" 876 :use ((:instance (:definition all-evaluations-p) 877 (states (create-all-evaluations vars states))))))) 878) 879 880(local 881(defthm append-evaluation-eq-member-reduction 882 (implies (evaluation-eq-member-p st states vars) 883 (evaluation-eq-member-p st (set-union init states) vars))) 884) 885 886(local 887(defthm all-evaluations-p-union-reduction 888 (implies (all-evaluations-p states vars) 889 (all-evaluations-p (set-union init states) vars)) 890 :hints (("Goal" 891 :use ((:instance all-evaluations-p-necc) 892 (:instance (:definition all-evaluations-p) 893 (states (set-union init states))))))) 894) 895 896(local 897(defthm create-kripke-is-all-evaluations-p 898 (all-evaluations-p (states (create-kripke C)) 899 (variables c))) 900) 901 902(local 903(defthm variables-of-create-kripke-are-original-vars 904 (equal (variables (create-kripke C)) 905 (variables C))) 906) 907 908(local 909(defthm strict-evaluations-list-to-evaluation 910 (implies (and (strict-evaluation-list-p vars states) 911 (memberp st states)) 912 (strict-evaluation-p st vars))) 913) 914 915(local 916(defthm strict-evaluations-append-reduction 917 (implies (and (strict-evaluation-list-p vars states) 918 (strict-evaluation-list-p vars states-prime)) 919 (strict-evaluation-list-p vars (append states states-prime)))) 920) 921 922(local 923(defthm strict-evaluation-list-p-nth-reduction 924 (implies (and (strict-evaluation-list-p vars states) 925 (integerp i) 926 (< i (len states)) 927 (consp states)) 928 (strict-evaluation-p (nth i states) vars))) 929) 930 931(local 932(defthm assign-t-strict-evaluations-reduction 933 (implies (and (strict-evaluation-list-p vars states) 934 (memberp v vars) 935 (consp states) 936 (integerp i) 937 (< i (len states)) 938 (not (memberp v-prime vars))) 939 (not (<- (nth i (assign-t v states)) v-prime))) 940 :hints (("Goal" 941 :do-not-induct t 942 :in-theory (disable assign-t-does-not-fuss) 943 :use ((:instance assign-t-does-not-fuss) 944 (:instance strict-evaluation-p-necc 945 (v v-prime) 946 (st (nth i states))))))) 947) 948 949(local 950(defthm assign-nil-strict-evaluations-reduction 951 (implies (and (strict-evaluation-list-p vars states) 952 (memberp v vars) 953 (consp states) 954 (integerp i) 955 (< i (len states)) 956 (not (memberp v-prime vars))) 957 (not (<- (nth i (assign-nil v states)) v-prime))) 958 :hints (("Goal" 959 :do-not-induct t 960 :in-theory (disable assign-nil-does-not-fuss) 961 :use ((:instance assign-nil-does-not-fuss) 962 (:instance strict-evaluation-p-necc 963 (v v-prime) 964 (st (nth i states))))))) 965) 966 967(local 968(defthm strict-evaluations-assign-t-reduction 969 (implies (and (integerp i) 970 (consp states) 971 (strict-evaluation-list-p vars states) 972 (memberp v vars) 973 (< i (len states))) 974 (strict-evaluation-p (nth i (assign-t v states)) vars))) 975) 976 977(local 978(defthm strict-evaluations-assign-nil-reduction 979 (implies (and (integerp i) 980 (consp states) 981 (strict-evaluation-list-p vars states) 982 (memberp v vars) 983 (< i (len states))) 984 (strict-evaluation-p (nth i (assign-nil v states)) vars))) 985) 986 987(local 988(defun find-index (st states) 989 (if (endp states) 0 990 (if (equal st (first states)) 0 991 (1+ (find-index st (rest states)))))) 992) 993 994(local 995(defthm find-index-is-memberp 996 (implies (memberp st states) 997 (equal (nth (find-index st states) states) 998 st))) 999) 1000 1001(local 1002(defthm find-index-returns-<-len 1003 (implies (memberp st states) 1004 (< (find-index st states) (len states))) 1005 :rule-classes :linear) 1006) 1007 1008(local 1009(defthm strict-evaluation-for-memberp-assign-t 1010 (implies (and (consp states) 1011 (strict-evaluation-list-p vars states) 1012 (memberp v vars) 1013 (memberp st (assign-t v states))) 1014 (strict-evaluation-p st vars)) 1015 :hints (("Goal" 1016 :do-not-induct t 1017 :in-theory (disable assign-t-strict-evaluations-reduction 1018 strict-evaluation-p) 1019 :use ((:instance strict-evaluations-assign-t-reduction 1020 (i (find-index st (assign-t v states)))))))) 1021) 1022 1023(local 1024(defthm strict-evaluation-for-memberp-assign-nil 1025 (implies (and (consp states) 1026 (strict-evaluation-list-p vars states) 1027 (memberp v vars) 1028 (memberp st (assign-nil v states))) 1029 (strict-evaluation-p st vars)) 1030 :hints (("Goal" 1031 :do-not-induct t 1032 :in-theory (disable assign-nil-strict-evaluations-reduction 1033 strict-evaluation-p) 1034 :use ((:instance strict-evaluations-assign-nil-reduction 1035 (i (find-index st (assign-nil v states)))))))) 1036) 1037 1038(local 1039(in-theory (disable strict-evaluation-p)) 1040) 1041 1042(local 1043(defthm strict-evaluations-for-assign-t 1044 (implies (and (consp states) 1045 (strict-evaluation-list-p vars states) 1046 (memberp v vars)) 1047 (strict-evaluation-list-p vars (assign-t v states)))) 1048) 1049 1050(local 1051(defthm strict-evaluations-for-assign-nil 1052 (implies (and (consp states) 1053 (strict-evaluation-list-p vars states) 1054 (memberp v vars)) 1055 (strict-evaluation-list-p vars (assign-nil v states)))) 1056) 1057 1058(local 1059(defun null-list-p (states) 1060 (if (endp states) T 1061 (and (null (first states)) 1062 (null-list-p (rest states))))) 1063) 1064 1065(local 1066(defthm strict-evaluation-p-cons-reduction 1067 (implies (strict-evaluation-p st vars) 1068 (strict-evaluation-p (-> st v t) (cons v vars))) 1069 :hints (("Goal" 1070 :expand (strict-evaluation-p (-> st v t) (cons v vars))))) 1071) 1072 1073(local 1074(defthm strict-evaluation-p-cons-reduction-2 1075 (implies (strict-evaluation-p st vars) 1076 (strict-evaluation-p (-> st v nil) (cons v vars))) 1077 :hints (("Goal" 1078 :expand (strict-evaluation-p (-> st v nil) (cons v vars))))) 1079) 1080 1081(local 1082(defthm strict-evaluation-p-assign-reduction-t 1083 (implies (strict-evaluation-list-p vars states) 1084 (strict-evaluation-list-p (cons v vars) (assign-t v states)))) 1085) 1086 1087(local 1088(defthm strict-evaluation-p-assign-reduction-nil 1089 (implies (strict-evaluation-list-p vars states) 1090 (strict-evaluation-list-p (cons v vars) (assign-nil v states)))) 1091) 1092 1093(local 1094(defthm nil-is-strict-evaluation-p 1095 (strict-evaluation-p nil vars) 1096 :hints (("Goal" 1097 :in-theory (enable strict-evaluation-p)))) 1098) 1099 1100(local 1101(defthm null-list-p-is-strict-evaluation-p 1102 (implies (null-list-p states) 1103 (strict-evaluation-list-p vars states))) 1104) 1105 1106(local 1107(defthm create-evaluations-is-strict-evaluation-list-p 1108 (implies (and (consp states) 1109 (null-list-p states) 1110 (uniquep vars)) 1111 (strict-evaluation-list-p 1112 vars (create-all-evaluations vars states))) 1113 :otf-flg t 1114 :hints (("Goal" 1115 :induct (create-all-evaluations vars states) 1116 :do-not '(eliminate-destructors generalize) 1117 :do-not-induct t) 1118 ("Subgoal *1/2" 1119 :in-theory (disable strict-evaluation-p-assign-reduction-t 1120 strict-evaluation-p-assign-reduction-nil) 1121 :use ((:instance strict-evaluation-p-assign-reduction-t 1122 (states (create-all-evaluations (cdr vars) states)) 1123 (vars (cdr vars)) 1124 (v (car vars))) 1125 (:instance strict-evaluation-p-assign-reduction-nil 1126 (states (create-all-evaluations (cdr vars) states)) 1127 (vars (cdr vars)) 1128 (v (car vars))))))) 1129) 1130 1131(local 1132(defthm strict-evaluation-set-union-reduction 1133 (implies (and (strict-evaluation-list-p vars init) 1134 (strict-evaluation-list-p vars states)) 1135 (strict-evaluation-list-p vars (set-union init states))) 1136 :hints (("Goal" 1137 :in-theory (enable set-union)))) 1138) 1139 1140(local 1141(defthm strict-evaluation-list-p-holds 1142 (implies (circuitp C) 1143 (strict-evaluation-list-p (variables C) (states (create-kripke C))))) 1144) 1145 1146(local 1147(in-theory (disable create-kripke)) 1148) 1149 1150(DEFTHM create-kripke-produces-circuit-model 1151 (implies (circuitp C) 1152 (circuit-modelp (create-kripke C)))) 1153 1154