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