tests/inputs/circuits.lisp

61 ;; Now let us try to create a Kripke Structure from the circuit. We need to
75 ;; Now we create all the states of the model.
77 (defun create-all-evaluations (vars states)
79     (let ((rec-states (create-all-evaluations (cdr vars) states)))
83 ;; Now let us create the label function.
92 (defun create-label-fn (states vars label)
94     (create-label-fn (rest states) vars
132 (defun create-next-states-of-p (p states vars equations)
135         (cons (first states) (create-next-states-of-p
137       (create-next-states-of-p p (rest states) vars equations))))
139 (defun create-next-states (states states-prime vars equations)
142      (create-next-states (rest states) states-prime vars equations)
144      (create-next-states-of-p (first states) states-prime vars equations))))
146 (defun create-kripke (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)
172   (subset (initial-states (create-kripke C)) (states (create-kripke C))))
177 ;; OK, let us prove that create-label-fn is a valid label function.
213 (defthm create-label-fn-does-not-mess-with-non-members
215            (equal (<- (create-label-fn states vars label) s)
220 (defthm create-label-fn-creates-an-all-truthsp-label
222            (equal (<- (create-label-fn states vars label) s)
228   (abs-only-all-truths-p states (create-label-fn states vars label) vars)
236   (only-all-truths-p (states (create-kripke C)) (create-kripke C)
260 (defthm create-label-fn-is-abs-label-subset-vars
261   (abs-label-subset-vars states (create-label-fn states vars label) vars)
269   (label-subset-vars (states (create-kripke C)) (create-kripke C) (variables
294   (abs-only-truth-p states (create-label-fn states vars label))
301   (only-truth-p (states (create-kripke C)) (create-kripke C)))
313 (defthm create-next-states-is-subset-of-states-aux
314   (implies (memberp q (create-next-states-of-p p states vars equations))
319 (defthm create-next-states-of-p-subset-helper
320   (implies (subset states-prime (create-next-states-of-p p states vars
327 (defthm create-next-states-is-subset-of-states
328   (subset (create-next-states-of-p p states vars equations)
331            :use ((:instance create-next-states-of-p-subset-helper
332                             (states-prime (create-next-states-of-p p states
339            (equal (<- (create-next-states states states-prime vars equations)
347            (equal (<- (create-next-states states states-prime vars equations)
349                   (create-next-states-of-p s states-prime vars equations)))
357                        (create-next-states states states-prime vars
365   (transition-subset-p (states (create-kripke C))
366                        (states (create-kripke C))
367                        (transition (create-kripke C))))
379 (defthm next-states-in-states-holds-for-create-kripke
380   (next-states-in-states (create-kripke C) (states (create-kripke C))))
393            (consp (create-all-evaluations vars states))))
411 (defthm create-kripke-is-consp-states
412   (consp (states (create-kripke C))))
415 ;; OK let us prove that everything is boolean with create-all-evaluations
425 ;; create-all-evaluations produces only-evaluations-p
441 ;; Now can we prove that boolean-p-states holds for create-all-evaluations?
475 (defthm boolean-p-create-non-member-reduction
477            (equal (boolean-p-states v (create-all-evaluations vars states))
480            :induct (create-all-evaluations vars states)
485 (defthm create-all-evaluations-for-member-is-boolean
487            (boolean-p-states v (create-all-evaluations vars states)))
489            :induct (create-all-evaluations vars states)
496 (defthm create-all-evaluations-is-boolean-list-p-aux
499                                   (create-all-evaluations vars-prime states))))
503 (defthm create-all-evaluations-is-boolean-list-p
504   (boolean-list-p-states vars (create-all-evaluations vars states)))
558 (defthm create-all-evaluations-is-only-evaluations-p
559   (only-evaluations-p (create-all-evaluations vars states) vars))
563 (defthm create-kripke-is-only-evaluations-p
565            (only-evaluations-p (states (create-kripke C)) (variables C))))
569 ;; defined using defun-sk. We try to create a witness for all-evaluations-p.
819           (create-all-evaluations vars states)))
826                     (create-all-evaluations vars states))))
855 (defthm create-all-evaluations-is-evaluation-eq-memberp
858            (evaluation-eq-member-p st (create-all-evaluations vars states)
866                             (states (create-all-evaluations vars states))
874            (all-evaluations-p (create-all-evaluations vars states) vars))
877                             (states (create-all-evaluations vars states)))))))
897 (defthm create-kripke-is-all-evaluations-p
898   (all-evaluations-p (states (create-kripke C))
903 (defthm variables-of-create-kripke-are-original-vars
904   (equal (variables (create-kripke C))
1107 (defthm create-evaluations-is-strict-evaluation-list-p
1112             vars (create-all-evaluations vars states)))
1115            :induct (create-all-evaluations vars states)
1122                             (states (create-all-evaluations (cdr vars) states))
1126                             (states (create-all-evaluations (cdr vars) states))
1143            (strict-evaluation-list-p (variables C) (states (create-kripke C)))))
1147 (in-theory (disable create-kripke))
1150 (DEFTHM create-kripke-produces-circuit-model
1152            (circuit-modelp (create-kripke C))))