Filtering...

unify-subst

books/clause-processors/unify-subst

Included Books

term-vars def-functional-instance ev-find-rules pseudo-termp-lemmas
other
(in-package "ACL2")
include-book
(include-book "term-vars")
include-book
(include-book "tools/def-functional-instance" :dir :system)
include-book
(include-book "ev-find-rules")
include-book
(include-book "meta/pseudo-termp-lemmas" :dir :system)
other
(defevaluator unify-ev
  unify-ev-lst
  ((cons a b) (binary-+ a b))
  :namedp t)
other
(define unify-ev-alist
  (x al)
  :verify-guards nil
  (if (atom x)
    nil
    (cons (cons (caar x) (unify-ev (cdar x) al))
      (unify-ev-alist (cdr x) al)))
  ///
  (defthm assoc-equal-unify-ev-alist
    (equal (cdr (assoc-equal k (unify-ev-alist x al)))
      (unify-ev (cdr (assoc-equal k x)) al)))
  (defthm assoc-equal-unify-ev-alist-iff
    (implies k
      (iff (assoc-equal k (unify-ev-alist x al))
        (assoc-equal k x))))
  (defthm assoc-equal-unify-ev-alist-when-assoc
    (implies (assoc k x) (assoc k (unify-ev-alist x al))))
  (defthm unify-ev-alist-pairlis$
    (equal (unify-ev-alist (pairlis$ a b) al)
      (pairlis$ a (unify-ev-lst b al))))
  (defthm unify-ev-alist-of-cons
    (equal (unify-ev-alist (cons x y) a)
      (cons (cons (car x) (unify-ev (cdr x) a))
        (unify-ev-alist y a)))))
local
(local (defthm assoc-equal-consp
    (implies (alistp x)
      (or (not (assoc-equal k x)) (consp (assoc-equal k x))))
    :rule-classes (:type-prescription (:rewrite :corollary (implies (and (alistp x) (assoc-equal k x))
          (consp (assoc-equal k x)))))))
other
(define all-keys-bound
  (keys (alist alistp))
  (if (atom keys)
    t
    (and (assoc-equal (car keys) alist)
      (all-keys-bound (cdr keys) alist)))
  ///
  (defthmd all-keys-bound-member
    (implies (and (all-keys-bound keys alist) (member-equal k keys))
      (assoc-equal k alist)))
  (defthm all-keys-bound-of-unify-ev-alist
    (implies (all-keys-bound keys alist)
      (all-keys-bound keys (unify-ev-alist alist a))))
  (defthm all-keys-bound-of-union-eq
    (equal (all-keys-bound (union-eq x y) alist)
      (and (all-keys-bound x alist) (all-keys-bound y alist)))
    :hints (("Goal" :in-theory (enable union-eq) :induct (len x))))
  (defthm all-keys-bound-of-cons
    (equal (all-keys-bound (cons x y) a)
      (and (assoc x a) (all-keys-bound y a))))
  (defthm acons-preserves-all-keys-bound
    (implies (all-keys-bound keys alist)
      (all-keys-bound keys (cons (cons k v) alist))))
  (defthm all-keys-bound-of-nil (all-keys-bound nil x)))
local
(local (in-theory (enable unify-ev-of-nonsymbol-atom)))
other
(defthm-simple-term-vars-flag (defthm unify-ev-of-acons-when-all-vars-bound
    (implies (and (all-keys-bound (simple-term-vars x) a)
        (not (assoc k a)))
      (equal (unify-ev x (cons (cons k v) a)) (unify-ev x a)))
    :hints ('(:expand ((simple-term-vars x))) (and stable-under-simplificationp
        '(:in-theory (enable unify-ev-of-fncall-args))))
    :flag simple-term-vars)
  (defthm unify-ev-lst-of-acons-when-all-vars-bound
    (implies (and (all-keys-bound (simple-term-vars-lst x) a)
        (not (assoc k a)))
      (equal (unify-ev-lst x (cons (cons k v) a))
        (unify-ev-lst x a)))
    :hints ('(:expand ((simple-term-vars-lst x))))
    :flag simple-term-vars-lst))
other
(defines substitute-into-term
  :flag-local nil
  (define substitute-into-term
    ((x pseudo-termp) (al alistp))
    :returns (xx pseudo-termp
      :hyp (and (pseudo-termp x) (pseudo-term-substp al))
      :hints ((and stable-under-simplificationp
         '(:expand ((pseudo-termp x))))))
    (cond ((atom x) (and x (mbt (symbolp x)) (cdr (assoc-equal x al))))
      ((eq (car x) 'quote) x)
      (t (cons (car x) (substitute-into-list (cdr x) al)))))
  (define substitute-into-list
    ((x pseudo-term-listp) (al alistp))
    :returns (xx (and (implies (and (pseudo-term-listp x) (pseudo-term-substp al))
          (pseudo-term-listp xx))
        (equal (len xx) (len x))))
    (if (atom x)
      nil
      (cons (substitute-into-term (car x) al)
        (substitute-into-list (cdr x) al))))
  ///
  (defthm-substitute-into-term-flag substitute-into-term-correct-lemma
    (defthm substitute-into-term-correct
      (equal (unify-ev (substitute-into-term x subst) a)
        (unify-ev x (unify-ev-alist subst a)))
      :hints ((and stable-under-simplificationp
         '(:in-theory (enable unify-ev-of-fncall-args))))
      :flag substitute-into-term)
    (defthm substitute-into-list-correct
      (equal (unify-ev-lst (substitute-into-list x subst) a)
        (unify-ev-lst x (unify-ev-alist subst a)))
      :flag substitute-into-list))
  (defthm substitute-into-list-of-cons
    (equal (substitute-into-list (cons x y) a)
      (cons (substitute-into-term x a) (substitute-into-list y a))))
  (defthm substitute-into-list-of-atom
    (implies (not (consp x))
      (equal (substitute-into-list x a) nil))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))
other
(define unify-const
  ((pat pseudo-termp) const (alist alistp))
  :returns (mv ok
    (al (and (implies (pseudo-termp pat)
          (equal (pseudo-term-substp al) (pseudo-term-substp alist)))
        (equal (alistp al) (alistp alist)))))
  (cond ((atom pat) (if (and pat (mbt (symbolp pat)))
        (let ((pair (assoc pat alist)))
          (if pair
            (let ((term (cdr pair)))
              (if (and (quotep term)
                  (consp (cdr term))
                  (equal (unquote term) const)
                  (null (cddr term)))
                (mv t alist)
                (mv nil alist)))
            (mv t (cons (cons pat (kwote const)) alist))))
        (if (eq const nil)
          (mv t alist)
          (mv nil alist))))
    ((eq (car pat) 'quote) (if (equal (unquote pat) const)
        (mv t alist)
        (mv nil alist)))
    ((and (eq (car pat) 'cons) (int= (len pat) 3)) (if (consp const)
        (b* (((mv car-ok alist) (unify-const (second pat) (car const) alist)) ((unless car-ok) (mv nil alist)))
          (unify-const (third pat) (cdr const) alist))
        (mv nil alist)))
    ((and (eq (car pat) 'binary-+) (int= (len pat) 3)) (cond ((not (acl2-numberp const)) (mv nil alist))
        ((quotep (second pat)) (let ((num (unquote (second pat))))
            (if (acl2-numberp num)
              (unify-const (third pat) (- const num) alist)
              (mv nil alist))))
        ((quotep (third pat)) (let ((num (unquote (third pat))))
            (if (acl2-numberp num)
              (unify-const (second pat) (- const num) alist)
              (mv nil alist))))
        (t (mv nil alist))))
    (t (mv nil alist)))
  ///
  (defthm unify-const-preserves-assoc-exists
    (implies (assoc k alist)
      (assoc k (mv-nth 1 (unify-const pat const alist)))))
  (defthm unify-const-preserves-assoc
    (b* (((mv ok newalist) (unify-const pat const alist)) (look (assoc k alist)))
      (implies (and ok look) (equal (assoc k newalist) look))))
  (defthm unify-const-preserves-all-keys-bound
    (b* (((mv ?ok newalist) (unify-const pat const alist)))
      (implies (all-keys-bound keys alist)
        (all-keys-bound keys newalist))))
  (encapsulate nil
    (local (defthm equal-of-len
        (equal (equal (len x) n)
          (if (zp n)
            (and (equal n 0) (not (consp x)))
            (and (consp x) (equal (len (cdr x)) (1- n)))))))
    (local (in-theory (disable len)))
    (local (defthm simple-term-vars-when-quotep
        (implies (equal (car x) 'quote)
          (equal (simple-term-vars x) nil))
        :hints (("goal" :expand ((simple-term-vars x))))))
    (defthm all-keys-bound-of-unify-const
      (b* (((mv ok newalist) (unify-const pat const alist)))
        (implies ok
          (all-keys-bound (simple-term-vars pat) newalist)))
      :hints (("goal" :induct (unify-const pat const alist)
         :expand ((unify-const pat const alist) (simple-term-vars pat)
           (simple-term-vars-lst (cdr pat)))
         :in-theory (disable (:d unify-const))) (and stable-under-simplificationp
          '(:expand ((simple-term-vars-lst (cddr pat))))))))
  (defthm unify-const-preserves-eval
    (mv-let (ok subst)
      (unify-const pat const alist)
      (implies (and ok (all-keys-bound (simple-term-vars term2) alist))
        (equal (unify-ev term2 (unify-ev-alist subst a))
          (unify-ev term2 (unify-ev-alist alist a))))))
  (defthm unify-const-preserves-eval-lst
    (mv-let (ok subst)
      (unify-const pat const alist)
      (implies (and ok (all-keys-bound (simple-term-vars-lst term2) alist))
        (equal (unify-ev-lst term2 (unify-ev-alist subst a))
          (unify-ev-lst term2 (unify-ev-alist alist a))))))
  (defthm unify-const-correct
    (mv-let (ok subst)
      (unify-const pat const alist)
      (implies (and ok)
        (equal (unify-ev pat (unify-ev-alist subst a)) const)))
    :hints (("goal" :induct t) (and stable-under-simplificationp
        '(:in-theory (enable unify-ev-of-fncall-args)))))
  (defthm unify-const-vars-nonnil
    (implies (not (assoc nil alist))
      (not (assoc nil (mv-nth 1 (unify-const pat const alist)))))))
other
(defines simple-one-way-unify
  :flag-local nil
  :verify-guards nil
  (define simple-one-way-unify
    ((pat pseudo-termp) (term pseudo-termp) (alist alistp))
    :returns (mv ok
      (a pseudo-term-substp
        :hyp (and (pseudo-termp term)
          (pseudo-termp pat)
          (pseudo-term-substp alist))))
    (cond ((atom pat) (if (and pat (mbt (symbolp pat)))
          (let ((pair (assoc-equal pat alist)))
            (if pair
              (if (equal term (cdr pair))
                (mv t alist)
                (mv nil alist))
              (mv t (cons (cons pat term) alist))))
          (if (or (eq term nil) (equal term *nil*))
            (mv t alist)
            (mv nil alist))))
      ((atom term) (mv nil alist))
      ((eq (car pat) 'quote) (if (equal pat term)
          (mv t alist)
          (mv nil alist)))
      ((eq (car term) 'quote) (unify-const pat (unquote term) alist))
      ((equal (car pat) (car term)) (simple-one-way-unify-lst (cdr pat) (cdr term) alist))
      (t (mv nil alist))))
  (define simple-one-way-unify-lst
    ((pat pseudo-term-listp) (term pseudo-term-listp)
      (alist alistp))
    :returns (mv ok
      (a pseudo-term-substp
        :hyp (and (pseudo-term-listp pat)
          (pseudo-term-listp term)
          (pseudo-term-substp alist))))
    (if (atom pat)
      (if (atom term)
        (mv t alist)
        (mv nil alist))
      (if (atom term)
        (mv nil alist)
        (mv-let (ok alist)
          (simple-one-way-unify (car pat) (car term) alist)
          (if ok
            (simple-one-way-unify-lst (cdr pat) (cdr term) alist)
            (mv nil alist))))))
  ///
  (defthm-simple-one-way-unify-flag alistp-simple-one-way-unify-lemma
    (simple-one-way-unify (implies (alistp alist)
        (alistp (mv-nth 1 (simple-one-way-unify pat term alist))))
      :name alistp-simple-one-way-unify)
    (simple-one-way-unify-lst (implies (alistp alist)
        (alistp (mv-nth 1 (simple-one-way-unify-lst pat term alist))))
      :name alistp-simple-one-way-unify-lst)
    :hints (("Goal" :induct (simple-one-way-unify-flag flag pat term alist)
       :expand ((:free (x) (simple-one-way-unify pat x alist)) (:free (x) (simple-one-way-unify-lst pat x alist))
         (:free (x) (simple-one-way-unify x term alist))
         (:free (x) (simple-one-way-unify-lst x term alist))
         (simple-one-way-unify nil nil alist)
         (pseudo-termp term)))))
  (verify-guards simple-one-way-unify)
  (defthm-simple-one-way-unify-flag assoc-one-way-unify-lemma
    (defthm assoc-equal-of-simple-one-way-unify-preserved
      (implies (and (assoc-equal k alist)
          (mv-nth 0 (simple-one-way-unify pat x alist)))
        (equal (assoc-equal k
            (mv-nth 1 (simple-one-way-unify pat x alist)))
          (assoc-equal k alist)))
      :flag simple-one-way-unify)
    (defthm assoc-equal-of-simple-one-way-unify-lst-preserved
      (implies (and (assoc-equal k alist)
          (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
        (equal (assoc-equal k
            (mv-nth 1 (simple-one-way-unify-lst pat x alist)))
          (assoc-equal k alist)))
      :flag simple-one-way-unify-lst)
    :hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
  (defthm-simple-term-vars-flag substitute-into-one-way-unify-reduce-lemma
    (defthm substitute-into-one-way-unify-reduce
      (implies (and (all-keys-bound (simple-term-vars term) alist)
          (mv-nth 0 (simple-one-way-unify pat x alist)))
        (equal (substitute-into-term term
            (mv-nth 1 (simple-one-way-unify pat x alist)))
          (substitute-into-term term alist)))
      :hints ('(:expand ((:free (a) (substitute-into-term term a)) (:free (a) (substitute-into-term nil a))
           (simple-term-vars term))))
      :flag simple-term-vars)
    (defthm substitute-into-one-way-unify-reduce-list
      (implies (and (all-keys-bound (simple-term-vars-lst term) alist)
          (mv-nth 0 (simple-one-way-unify pat x alist)))
        (equal (substitute-into-list term
            (mv-nth 1 (simple-one-way-unify pat x alist)))
          (substitute-into-list term alist)))
      :hints ((and stable-under-simplificationp
         '(:expand ((:free (a) (substitute-into-list term a)) (simple-term-vars-lst term)))))
      :flag simple-term-vars-lst)
    :hints (("goal" :induct (simple-term-vars-flag flag term)
       :in-theory (enable subsetp-equal))))
  (defthm-simple-term-vars-flag substitute-into-one-way-unify-lst-reduce-lemma
    (defthm substitute-into-one-way-unify-lst-reduce
      (implies (and (all-keys-bound (simple-term-vars term) alist)
          (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
        (equal (substitute-into-term term
            (mv-nth 1 (simple-one-way-unify-lst pat x alist)))
          (substitute-into-term term alist)))
      :hints ('(:expand ((:free (a) (substitute-into-term term a)) (:free (a) (substitute-into-term nil a))
           (simple-term-vars term))))
      :flag simple-term-vars)
    (defthm substitute-into-one-way-unify-lst-reduce-list
      (implies (and (all-keys-bound (simple-term-vars-lst term) alist)
          (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
        (equal (substitute-into-list term
            (mv-nth 1 (simple-one-way-unify-lst pat x alist)))
          (substitute-into-list term alist)))
      :hints ((and stable-under-simplificationp
         '(:expand ((:free (a) (substitute-into-list term a)) (simple-term-vars-lst term)))))
      :flag simple-term-vars-lst)
    :hints (("goal" :induct (simple-term-vars-flag flag term)
       :in-theory (enable subsetp-equal))))
  (defthm-simple-one-way-unify-flag one-way-unify-all-keys-bound-lemma
    (defthm one-way-unify-all-keys-bound
      (mv-let (ok subst)
        (simple-one-way-unify pat x alist)
        (declare (ignore ok))
        (implies (all-keys-bound keys alist)
          (all-keys-bound keys subst)))
      :hints ('(:expand ((simple-term-vars pat))))
      :flag simple-one-way-unify)
    (defthm one-way-unify-lst-all-keys-bound
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat x alist)
        (declare (ignore ok))
        (implies (all-keys-bound keys alist)
          (all-keys-bound keys subst)))
      :hints ('(:expand ((simple-term-vars-lst pat))))
      :flag simple-one-way-unify-lst)
    :hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
  (defthm-simple-one-way-unify-flag one-way-unify-all-vars-bound-lemma
    (defthm one-way-unify-all-vars-bound
      (mv-let (ok subst)
        (simple-one-way-unify pat x alist)
        (implies ok (all-keys-bound (simple-term-vars pat) subst)))
      :hints ((and stable-under-simplificationp
         '(:expand ((simple-term-vars pat)))))
      :flag simple-one-way-unify)
    (defthm one-way-unify-lst-all-vars-bound
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat x alist)
        (implies ok
          (all-keys-bound (simple-term-vars-lst pat) subst)))
      :hints ('(:expand ((simple-term-vars-lst pat))))
      :flag simple-one-way-unify-lst)
    :hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
  (local (in-theory (disable simple-one-way-unify simple-one-way-unify-lst)))
  (defthm-simple-one-way-unify-flag (defthm one-way-unify-vars-nonnil
      (implies (not (assoc nil alist))
        (mv-let (ok subst)
          (simple-one-way-unify pat x alist)
          (declare (ignore ok))
          (not (assoc nil subst))))
      :hints ((and stable-under-simplificationp
         '(:expand ((:free (x) (simple-one-way-unify pat x alist)) (:free (x) (simple-one-way-unify nil x alist))))))
      :flag simple-one-way-unify)
    (defthm one-way-unify-lst-vars-nonnil
      (implies (not (assoc nil alist))
        (mv-let (ok subst)
          (simple-one-way-unify-lst pat x alist)
          (declare (ignore ok))
          (not (assoc nil subst))))
      :hints ('(:expand ((simple-one-way-unify-lst pat x alist))))
      :flag simple-one-way-unify-lst)
    :hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
  (defthm-simple-one-way-unify-flag (defthm simple-one-way-unify-preserves-eval
      (mv-let (ok subst)
        (simple-one-way-unify pat term alist)
        (implies (and ok (all-keys-bound (simple-term-vars term2) alist))
          (equal (unify-ev term2 (unify-ev-alist subst a))
            (unify-ev term2 (unify-ev-alist alist a)))))
      :hints ('(:expand ((:free (term) (simple-one-way-unify pat term alist)) (:free (term) (simple-one-way-unify nil term alist)))))
      :flag simple-one-way-unify)
    (defthm simple-one-way-unify-lst-preserves-eval
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat term alist)
        (implies (and ok (all-keys-bound (simple-term-vars term2) alist))
          (equal (unify-ev term2 (unify-ev-alist subst a))
            (unify-ev term2 (unify-ev-alist alist a)))))
      :hints ('(:expand (simple-one-way-unify-lst pat term alist)))
      :flag simple-one-way-unify-lst))
  (defthm-simple-one-way-unify-flag (defthm simple-one-way-unify-preserves-eval-lst
      (mv-let (ok subst)
        (simple-one-way-unify pat term alist)
        (implies (and ok (all-keys-bound (simple-term-vars-lst term2) alist))
          (equal (unify-ev-lst term2 (unify-ev-alist subst a))
            (unify-ev-lst term2 (unify-ev-alist alist a)))))
      :hints ('(:expand ((:free (term) (simple-one-way-unify pat term alist)) (:free (term) (simple-one-way-unify nil term alist)))))
      :flag simple-one-way-unify)
    (defthm simple-one-way-unify-lst-preserves-eval-lst
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat term alist)
        (implies (and ok (all-keys-bound (simple-term-vars-lst term2) alist))
          (equal (unify-ev-lst term2 (unify-ev-alist subst a))
            (unify-ev-lst term2 (unify-ev-alist alist a)))))
      :hints ('(:expand (simple-one-way-unify-lst pat term alist)))
      :flag simple-one-way-unify-lst))
  (defthm-simple-one-way-unify-flag (defthm simple-one-way-unify-correct
      (mv-let (ok subst)
        (simple-one-way-unify pat term alist)
        (implies (and ok)
          (equal (unify-ev pat (unify-ev-alist subst a))
            (unify-ev term a))))
      :hints ('(:expand ((:free (term) (simple-one-way-unify pat term alist)) (:free (term) (simple-one-way-unify nil term alist)))) (and stable-under-simplificationp
          '(:in-theory (enable unify-ev-of-fncall-args))))
      :flag simple-one-way-unify)
    (defthm simple-one-way-unify-lst-correct
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat term alist)
        (implies (and ok)
          (equal (unify-ev-lst pat (unify-ev-alist subst a))
            (unify-ev-lst term a))))
      :hints ('(:expand (simple-one-way-unify-lst pat term alist)))
      :flag simple-one-way-unify-lst)))
find-eval-alists-termmutual-recursion
(mutual-recursion (defun find-eval-alists-term
    (eval-fns x)
    (declare (xargs :guard (and (pseudo-termp x) (symbol-listp eval-fns))
        :verify-guards nil))
    (cond ((variablep x) nil)
      ((fquotep x) nil)
      (t (let ((arg-envs (find-eval-alists-list eval-fns (fargs x))))
          (if (member-eq (ffn-symb x) eval-fns)
            (let ((env (third x)))
              (if (member-equal env arg-envs)
                arg-envs
                (cons env arg-envs)))
            arg-envs)))))
  (defun find-eval-alists-list
    (eval-fns x)
    (declare (xargs :guard (and (pseudo-term-listp x) (symbol-listp eval-fns))))
    (if (atom x)
      nil
      (union-equal (find-eval-alists-term eval-fns (car x))
        (find-eval-alists-list eval-fns (cdr x))))))
list-termfunction
(defun list-term
  (lst)
  (declare (xargs :guard t))
  (if (consp lst)
    (cons 'cons
      (cons (car lst) (cons (list-term (cdr lst)) nil)))
    ''nil))
filter-out-unify-subst-evalsfunction
(defun filter-out-unify-subst-evals
  (env-terms simple-one-way-unify-call
    ev-alist
    full-env-terms)
  (if (atom env-terms)
    nil
    (let* ((env (car env-terms)) (rest (filter-out-unify-subst-evals (cdr env-terms)
            simple-one-way-unify-call
            ev-alist
            full-env-terms)))
      (case-match env
        ((!ev-alist ('mv-nth ''1 !simple-one-way-unify-call) a) (if (member-equal a full-env-terms)
            rest
            (cons a rest)))
        (& (cons env rest))))))
simple-one-way-unify-bind-freefunction
(defun simple-one-way-unify-bind-free
  (rw-term eval-fns mfc state)
  (declare (xargs :mode :program :stobjs state)
    (ignorable state))
  (and (let ((lit (access rewrite-constant
           (access metafunction-context mfc :rcnst)
           :current-literal)))
      (and (consp lit) (eq (car lit) t) (equal (cdr lit) rw-term)))
    (null (mfc-ancestors mfc))
    (let ((terms (find-eval-alists-list eval-fns (mfc-clause mfc))))
      (and terms
        (let ((terms (filter-out-unify-subst-evals terms
               (third rw-term)
               (third eval-fns)
               terms)))
          `((envs . ,(LIST-TERM TERMS))))))))
unify-ev-simple-one-way-unify-equalitiesfunction
(defun unify-ev-simple-one-way-unify-equalities
  (pat term subst envs)
  (if (atom envs)
    t
    (and (equal (unify-ev term (car envs))
        (unify-ev pat (unify-ev-alist subst (car envs))))
      (unify-ev-simple-one-way-unify-equalities pat
        term
        subst
        (cdr envs)))))
other
(defund-nx unify-succeeded
  (pat term alist)
  (mv-nth 0 (simple-one-way-unify pat term alist)))
unify-succeeded-impliestheorem
(defthm unify-succeeded-implies
  (implies (unify-succeeded pat term alist)
    (mv-nth 0 (simple-one-way-unify pat term alist)))
  :hints (("Goal" :in-theory (enable unify-succeeded)))
  :rule-classes (:rewrite :forward-chaining))
other
(defund-nx unify-lst-succeeded
  (pat term alist)
  (mv-nth 0 (simple-one-way-unify-lst pat term alist)))
unify-lst-succeeded-impliestheorem
(defthm unify-lst-succeeded-implies
  (implies (unify-lst-succeeded pat term alist)
    (mv-nth 0 (simple-one-way-unify-lst pat term alist)))
  :hints (("Goal" :in-theory (enable unify-lst-succeeded)))
  :rule-classes (:rewrite :forward-chaining))
simple-one-way-unify-usagetheorem
(defthm simple-one-way-unify-usage
  (mv-let (ok subst)
    (simple-one-way-unify pat term alist)
    (implies (and (bind-free (simple-one-way-unify-bind-free `(mv-nth '0 (simple-one-way-unify ,PAT ,TERM ,ALIST))
            '(unify-ev unify-ev-lst unify-ev-alist)
            mfc
            state)
          (envs)))
      (iff ok
        (and (unify-succeeded pat term alist)
          (unify-ev-simple-one-way-unify-equalities pat
            term
            subst
            envs)))))
  :hints (("goal" :induct (len envs)
     :in-theory (enable unify-succeeded))))
unify-ev-simple-one-way-unify-equalities-of-niltheorem
(defthm unify-ev-simple-one-way-unify-equalities-of-nil
  (equal (unify-ev-simple-one-way-unify-equalities pat
      term
      subst
      nil)
    t))
unify-ev-simple-one-way-unify-equalities-of-constheorem
(defthm unify-ev-simple-one-way-unify-equalities-of-cons
  (equal (unify-ev-simple-one-way-unify-equalities pat
      term
      subst
      (cons a b))
    (and (equal (unify-ev term a)
        (unify-ev pat (unify-ev-alist subst a)))
      (unify-ev-simple-one-way-unify-equalities pat term subst b))))
in-theory
(in-theory (disable unify-ev-simple-one-way-unify-equalities))
unify-ev-lst-simple-one-way-unify-equalitiesfunction
(defun unify-ev-lst-simple-one-way-unify-equalities
  (pat term subst envs)
  (if (atom envs)
    t
    (and (equal (unify-ev-lst term (car envs))
        (unify-ev-lst pat (unify-ev-alist subst (car envs))))
      (unify-ev-lst-simple-one-way-unify-equalities pat
        term
        subst
        (cdr envs)))))
simple-one-way-unify-lst-usagetheorem
(defthm simple-one-way-unify-lst-usage
  (mv-let (ok subst)
    (simple-one-way-unify-lst pat term alist)
    (implies (and (bind-free (simple-one-way-unify-bind-free `(mv-nth '0 (simple-one-way-unify-lst ,PAT ,TERM ,ALIST))
            '(unify-ev unify-ev-lst unify-ev-alist)
            mfc
            state)
          (envs))
        (pseudo-term-listp term)
        (pseudo-term-listp pat))
      (iff ok
        (and (unify-lst-succeeded pat term alist)
          (unify-ev-lst-simple-one-way-unify-equalities pat
            term
            subst
            envs)))))
  :hints (("goal" :induct (len envs)
     :in-theory (enable unify-lst-succeeded))))
unify-ev-lst-simple-one-way-unify-equalities-of-niltheorem
(defthm unify-ev-lst-simple-one-way-unify-equalities-of-nil
  (equal (unify-ev-lst-simple-one-way-unify-equalities pat
      term
      subst
      nil)
    t))
unify-ev-lst-simple-one-way-unify-equalities-of-constheorem
(defthm unify-ev-lst-simple-one-way-unify-equalities-of-cons
  (equal (unify-ev-lst-simple-one-way-unify-equalities pat
      term
      subst
      (cons a b))
    (and (equal (unify-ev-lst term a)
        (unify-ev-lst pat (unify-ev-alist subst a)))
      (unify-ev-lst-simple-one-way-unify-equalities pat
        term
        subst
        b))))
in-theory
(in-theory (disable unify-ev-lst-simple-one-way-unify-equalities))
*def-unify-template*constant
(defconst *def-unify-template*
  '(encapsulate nil
    (local (in-theory (disable pseudo-termp default-car default-cdr)))
    (defun new-ev-alist
      (x al)
      (if (atom x)
        nil
        (cons (cons (caar x) (new-ev (cdar x) al))
          (new-ev-alist (cdr x) al))))
    (def-functional-instance simple-one-way-unify-correct-for-new-ev
      simple-one-way-unify-correct
      ((unify-ev new-ev) (unify-ev-lst new-ev-lst)
        (unify-ev-alist new-ev-alist))
      :hints ((and stable-under-simplificationp
         '(:in-theory (enable new-ev-constraint-0)))))
    (def-functional-instance simple-one-way-unify-lst-correct-for-new-ev
      simple-one-way-unify-lst-correct
      ((unify-ev new-ev) (unify-ev-lst new-ev-lst)
        (unify-ev-alist new-ev-alist)))
    (def-functional-instance substitute-into-term-correct-for-new-ev
      substitute-into-term-correct
      ((unify-ev new-ev) (unify-ev-lst new-ev-lst)
        (unify-ev-alist new-ev-alist)))
    (def-functional-instance substitute-into-list-correct-for-new-ev
      substitute-into-list-correct
      ((unify-ev new-ev) (unify-ev-lst new-ev-lst)
        (unify-ev-alist new-ev-alist)))
    (defun new-ev-simple-one-way-unify-equalities
      (pat term subst envs)
      (if (atom envs)
        t
        (and (equal (new-ev term (car envs))
            (new-ev pat (new-ev-alist subst (car envs))))
          (new-ev-simple-one-way-unify-equalities pat
            term
            subst
            (cdr envs)))))
    (defthm simple-one-way-unify-with-new-ev
      (mv-let (ok subst)
        (simple-one-way-unify pat term alist)
        (implies (and (bind-free (simple-one-way-unify-bind-free `(mv-nth '0 (simple-one-way-unify ,PAT ,TERM ,ALIST))
                '(new-ev new-ev-lst new-ev-alist)
                mfc
                state)
              (envs)))
          (iff ok
            (and (unify-succeeded pat term alist)
              (new-ev-simple-one-way-unify-equalities pat term subst envs)))))
      :hints (("goal" :induct (len envs)
         :in-theory (enable unify-succeeded))))
    (defthm new-ev-simple-one-way-unify-equalities-of-nil
      (equal (new-ev-simple-one-way-unify-equalities pat term subst nil)
        t))
    (defthm new-ev-simple-one-way-unify-equalities-of-cons
      (equal (new-ev-simple-one-way-unify-equalities pat
          term
          subst
          (cons a b))
        (and (equal (new-ev term a) (new-ev pat (new-ev-alist subst a)))
          (new-ev-simple-one-way-unify-equalities pat term subst b))))
    (in-theory (disable new-ev-simple-one-way-unify-equalities))
    (defun new-ev-lst-simple-one-way-unify-equalities
      (pat term subst envs)
      (if (atom envs)
        t
        (and (equal (new-ev-lst term (car envs))
            (new-ev-lst pat (new-ev-alist subst (car envs))))
          (new-ev-lst-simple-one-way-unify-equalities pat
            term
            subst
            (cdr envs)))))
    (defthm simple-one-way-unify-lst-with-new-ev
      (mv-let (ok subst)
        (simple-one-way-unify-lst pat term alist)
        (implies (and (bind-free (simple-one-way-unify-bind-free `(mv-nth '0 (simple-one-way-unify-lst ,PAT ,TERM ,ALIST))
                '(new-ev new-ev-lst new-ev-alist)
                mfc
                state)
              (envs))
            (pseudo-term-listp term)
            (pseudo-term-listp pat))
          (iff ok
            (and (unify-lst-succeeded pat term alist)
              (new-ev-lst-simple-one-way-unify-equalities pat
                term
                subst
                envs)))))
      :hints (("goal" :induct (len envs)
         :in-theory (enable unify-lst-succeeded))))
    (defthm new-ev-lst-simple-one-way-unify-equalities-of-nil
      (equal (new-ev-lst-simple-one-way-unify-equalities pat
          term
          subst
          nil)
        t))
    (defthm new-ev-lst-simple-one-way-unify-equalities-of-cons
      (equal (new-ev-lst-simple-one-way-unify-equalities pat
          term
          subst
          (cons a b))
        (and (equal (new-ev-lst term a)
            (new-ev-lst pat (new-ev-alist subst a)))
          (new-ev-lst-simple-one-way-unify-equalities pat
            term
            subst
            b))))
    (in-theory (disable new-ev-lst-simple-one-way-unify-equalities))
    (in-theory (disable simple-one-way-unify-correct-for-new-ev
        simple-one-way-unify-lst-correct-for-new-ev))))
def-unify-prefix-pairfunction
(defun def-unify-prefix-pair
  (new-ev ev sym)
  (let ((str (symbol-name sym)))
    (cons (intern$ (concatenate 'string (symbol-name new-ev) str)
        "ACL2")
      (intern-in-package-of-symbol (concatenate 'string (symbol-name ev) str)
        ev))))
def-unify-prefix-pairsfunction
(defun def-unify-prefix-pairs
  (new-ev ev syms)
  (if (atom syms)
    nil
    (cons (def-unify-prefix-pair new-ev ev (car syms))
      (def-unify-prefix-pairs new-ev ev (cdr syms)))))
def-unify-suffix-pairfunction
(defun def-unify-suffix-pair
  (new-ev ev sym)
  (let ((str (symbol-name sym)))
    (cons (intern$ (concatenate 'string str (symbol-name new-ev))
        "ACL2")
      (intern-in-package-of-symbol (concatenate 'string str (symbol-name ev))
        ev))))
def-unify-suffix-pairsfunction
(defun def-unify-suffix-pairs
  (new-ev ev syms)
  (if (atom syms)
    nil
    (cons (def-unify-suffix-pair new-ev ev (car syms))
      (def-unify-suffix-pairs new-ev ev (cdr syms)))))
def-unify-fnfunction
(defun def-unify-fn
  (ev ev-alist world)
  (b* ((ev-lst (find-ev-counterpart ev world)) (constr-0 (ev-find-fncall-generic-rule ev world))
      (alist (append `((new-ev . ,EV) (new-ev-lst . ,EV-LST)
            (new-ev-alist . ,EV-ALIST)
            (new-ev-constraint-0 . ,CONSTR-0))
          (def-unify-suffix-pairs 'new-ev
            ev
            '(simple-one-way-unify-correct-for- simple-one-way-unify-lst-correct-for-
              substitute-into-term-correct-for-
              substitute-into-list-correct-for-
              simple-one-way-unify-with-
              simple-one-way-unify-lst-with-))
          (def-unify-prefix-pairs 'new-ev
            ev
            '(-simple-one-way-unify-equalities -simple-one-way-unify-equalities-of-nil
              -simple-one-way-unify-equalities-of-cons))
          (def-unify-prefix-pairs 'new-ev-lst
            ev-lst
            '(-simple-one-way-unify-equalities -simple-one-way-unify-equalities-of-nil
              -simple-one-way-unify-equalities-of-cons)))))
    (sublis alist *def-unify-template*)))
def-unifymacro
(defmacro def-unify
  (ev ev-alist)
  `(make-event (def-unify-fn ',EV ',EV-ALIST (w state))))
other
(with-output :off :all :on (error)
  :gag-mode nil
  (local (progn (defevaluator my-ev
        my-ev-lst
        ((cons p q) (binary-+ f g) (len x)))
      (def-unify my-ev my-ev-alist)
      (defevaluator my-ev2
        my-ev-lst2
        ((if a
           b
           c) (cons g h)
          (binary-+ j l)))
      (def-unify my-ev2 my-ev-alist2))))