multi-env-trick - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "misc/untranslate-patterns" :dir :system)

local

(local (include-book "join-thms"))

other

(defevaluator multi-env-ev
  multi-env-ev-lst
  ((if a
     b
     c)))

other

(defchoose multi-env-ev-bad-guy
  (a)
  (x)
  (not (multi-env-ev x a)))

clause-apply-alists-multi-env-evfunction

(defun clause-apply-alists-multi-env-ev
  (clause alists)
  (or (atom alists)
    (and (multi-env-ev (disjoin clause) (car alists))
      (clause-apply-alists-multi-env-ev clause (cdr alists)))))

clauses-apply-alists-multi-env-evfunction

(defun clauses-apply-alists-multi-env-ev
  (clauses alist-lists)
  (or (atom clauses)
    (and (clause-apply-alists-multi-env-ev (car clauses)
        (car alist-lists))
      (clauses-apply-alists-multi-env-ev (cdr clauses)
        (cdr alist-lists)))))

multi-env-ev-theorempmacro

(defmacro multi-env-ev-theoremp
  (x)
  `(multi-env-ev ,X (multi-env-ev-bad-guy ,X)))

other

(add-untranslate-pattern (multi-env-ev ?x (multi-env-ev-bad-guy ?x))
  (multi-env-ev-theoremp ?x))

local

(local (def-join-thms multi-env-ev))

multi-env-ev-theoremp-implies-clause-apply-aliststheorem

(defthm multi-env-ev-theoremp-implies-clause-apply-alists
  (implies (multi-env-ev-theoremp (disjoin x))
    (clause-apply-alists-multi-env-ev x alists))
  :hints (("Subgoal *1/3" :use ((:instance multi-env-ev-bad-guy
        (x (disjoin x))
        (a (car alists)))))))

multi-env-ev-theoremp-conjoin-constheorem

(defthm multi-env-ev-theoremp-conjoin-cons
  (iff (multi-env-ev-theoremp (conjoin (cons a b)))
    (and (multi-env-ev-theoremp a)
      (multi-env-ev-theoremp (conjoin b))))
  :hints (("goal" :use ((:instance multi-env-ev-bad-guy
        (x a)
        (a (multi-env-ev-bad-guy (conjoin (cons a b))))) (:instance multi-env-ev-bad-guy
         (x (conjoin (cons a b)))
         (a (multi-env-ev-bad-guy a)))
       (:instance multi-env-ev-bad-guy
         (x (conjoin b))
         (a (multi-env-ev-bad-guy (conjoin (cons a b)))))
       (:instance multi-env-ev-bad-guy
         (x (conjoin (cons a b)))
         (a (multi-env-ev-bad-guy (conjoin b))))))))

multi-env-theoremp-conjoin-clauses-constheorem

(defthm multi-env-theoremp-conjoin-clauses-cons
  (iff (multi-env-ev-theoremp (conjoin-clauses (cons a b)))
    (and (multi-env-ev-theoremp (disjoin a))
      (multi-env-ev-theoremp (conjoin-clauses b))))
  :hints (("Goal" :in-theory (enable conjoin-clauses))))

multi-env-ev-theoremp-implies-clauses-apply-aliststheorem

(defthm multi-env-ev-theoremp-implies-clauses-apply-alists
  (implies (multi-env-ev-theoremp (conjoin-clauses x))
    (clauses-apply-alists-multi-env-ev x alists))
  :hints (("Goal" :in-theory (enable conjoin-clauses disjoin-lst))))

incatmacro

(defmacro incat
  (sym &rest lst)
  `(intern-in-package-of-symbol (concatenate 'string . ,LST)
    ,SYM))

multi-env-functional-instance-fnfunction

(defun multi-env-functional-instance-fn
  (thm x alists ev evlst bad-guy)
  (let* ((bad-guy (or bad-guy (incat ev (symbol-name ev) "-BAD-GUY"))) (clause-apply (incat ev "CLAUSE-APPLY-ALISTS-" (symbol-name ev)))
      (clauses-apply (incat ev "CLAUSES-APPLY-ALISTS-" (symbol-name ev))))
    `(:use ((:instance (:functional-instance ,THM
           (multi-env-ev ,EV)
           (multi-env-ev-lst ,EVLST)
           (multi-env-ev-bad-guy ,BAD-GUY)
           (clause-apply-alists-multi-env-ev ,CLAUSE-APPLY)
           (clauses-apply-alists-multi-env-ev ,CLAUSES-APPLY))
         (x ,X)
         (alists ,ALISTS))))))

multi-env-functional-instancemacro

(defmacro multi-env-functional-instance
  (thm x alists &key ev evlst bad-guy)
  `(multi-env-functional-instance-fn ',THM
    ',X
    ',ALISTS
    ',EV
    ',EVLST
    ',BAD-GUY))

def-multi-env-fnfunction

(defun def-multi-env-fn
  (ev evlst)
  (declare (xargs :mode :program))
  (let ((bad-guy (incat ev (symbol-name ev) "-BAD-GUY")) (bad-guy-rewrite (incat ev (symbol-name ev) "-BAD-GUY-REWRITE"))
      (theoremp (incat ev (symbol-name ev) "-THEOREMP"))
      (clause-apply (incat ev "CLAUSE-APPLY-ALISTS-" (symbol-name ev)))
      (clauses-apply (incat ev "CLAUSES-APPLY-ALISTS-" (symbol-name ev)))
      (clause-apply-thm (incat ev
          (symbol-name ev)
          "-THEOREMP-IMPLIES-CLAUSE-APPLY-ALISTS"))
      (clauses-apply-thm (incat ev
          (symbol-name ev)
          "-THEOREMP-IMPLIES-CLAUSES-APPLY-ALISTS"))
      (constraint-0 (genvar ev (symbol-name (pack2 ev '-constraint-)) 0 nil)))
    `(progn (defchoose ,BAD-GUY (a) (x) (not (,EV x a)))
      (defthm ,BAD-GUY-REWRITE
        (implies (,EV x (,BAD-GUY x)) (,EV x a))
        :hints (("goal" :use ,BAD-GUY)))
      (defmacro ,THEOREMP (x) `(,',EV ,X (,',BAD-GUY ,X)))
      (add-untranslate-pattern (,EV ?x (,BAD-GUY ?x))
        (,THEOREMP ?x))
      (defun ,CLAUSE-APPLY
        (clause alists)
        (or (atom alists)
          (and (,EV (disjoin clause) (car alists))
            (,CLAUSE-APPLY clause (cdr alists)))))
      (defun ,CLAUSES-APPLY
        (clauses alist-lists)
        (or (atom clauses)
          (and (,CLAUSE-APPLY (car clauses) (car alist-lists))
            (,CLAUSES-APPLY (cdr clauses) (cdr alist-lists)))))
      (defthmd ,CLAUSE-APPLY-THM
        (implies (,THEOREMP (disjoin clause))
          (,CLAUSE-APPLY clause alists))
        :hints ((multi-env-functional-instance multi-env-ev-theoremp-implies-clause-apply-alists
           clause
           alists
           :ev ,EV
           :evlst ,EVLST) (and stable-under-simplificationp
            '(:in-theory (enable ,CONSTRAINT-0)))))
      (defthmd ,CLAUSES-APPLY-THM
        (implies (,THEOREMP (conjoin-clauses clause))
          (,CLAUSES-APPLY clause alists))
        :hints ((multi-env-functional-instance multi-env-ev-theoremp-implies-clauses-apply-alists
           clause
           alists
           :ev ,EV
           :evlst ,EVLST))))))

def-multi-env-fnsmacro

(defmacro def-multi-env-fns
  (ev evlst)
  (def-multi-env-fn ev evlst))

prove-multi-env-clause-proc-fnfunction

(defun prove-multi-env-clause-proc-fn
  (name ev
    evlst
    clauseproc
    alists
    hints
    bad-guy
    alist-name
    world)
  (declare (xargs :mode :program))
  (let* ((bad-guy (or bad-guy (incat ev (symbol-name ev) "-BAD-GUY"))) (clauses-apply-thm (incat ev
          (symbol-name ev)
          "-THEOREMP-IMPLIES-CLAUSES-APPLY-ALISTS"))
      (cp-args (fgetprop clauseproc 'formals nil world))
      (clausename (car cp-args))
      (multivaluesp (< 1 (len (fgetprop clauseproc 'stobjs-out nil world))))
      (cp-call1 `(,CLAUSEPROC . ,CP-ARGS))
      (cp-call (if multivaluesp
          `(clauses-result ,CP-CALL1)
          cp-call1)))
    `(progn (def-multi-env-fns ,EV ,EVLST)
      (defthm ,NAME
        (implies (and (pseudo-term-listp ,CLAUSENAME)
            (alistp ,ALIST-NAME)
            (,EV (conjoin-clauses ,CP-CALL)
              (,BAD-GUY (conjoin-clauses ,CP-CALL))))
          (,EV (disjoin ,CLAUSENAME) ,ALIST-NAME))
        :hints (("Goal" :use ((:instance ,CLAUSES-APPLY-THM
              (clause ,CP-CALL)
              (alists ,ALISTS)))) . ,HINTS)
        :otf-flg t
        :rule-classes :clause-processor))))

prove-multi-env-clause-procmacro

(defmacro prove-multi-env-clause-proc
  (name &key
    ev
    evlst
    clauseproc
    alists
    bad-guy
    (alist-name 'al)
    hints)
  `(make-event (prove-multi-env-clause-proc-fn ',NAME
      ',EV
      ',EVLST
      ',CLAUSEPROC
      ',ALISTS
      ',HINTS
      ',BAD-GUY
      ',ALIST-NAME
      (w state))))