Lines Matching defs:create
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))))