find-matching - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "unify-subst")

find-matchmutual-recursion

(mutual-recursion (defun find-match
    (pat x initial-alist)
    (declare (xargs :guard (and (pseudo-termp pat)
          (pseudo-termp x)
          (alistp initial-alist))))
    (b* (((mv match ?alist) (simple-one-way-unify pat x initial-alist)) ((when match) (mv t x))
        ((when (or (variablep x) (fquotep x))) (mv nil nil)))
      (find-match-list pat (cdr x) initial-alist)))
  (defun find-match-list
    (pat x initial-alist)
    (declare (xargs :guard (and (pseudo-termp pat)
          (pseudo-term-listp x)
          (alistp initial-alist))))
    (b* (((when (atom x)) (mv nil nil)) ((mv ok subterm) (find-match pat (car x) initial-alist))
        ((when ok) (mv ok subterm)))
      (find-match-list pat (cdr x) initial-alist))))

find-matching-literal-in-clausefunction

(defun find-matching-literal-in-clause
  (pat clause initial-alist)
  (declare (xargs :guard (and (pseudo-termp pat)
        (pseudo-term-listp clause)
        (alistp initial-alist))))
  (b* (((when (atom clause)) (mv nil nil)) ((mv match ?alist) (simple-one-way-unify pat (car clause) initial-alist))
      ((when match) (mv t (car clause))))
    (find-matching-literal-in-clause pat
      (cdr clause)
      initial-alist)))

find-matchesmutual-recursion

(mutual-recursion (defun find-matches
    (pat x initial-alist)
    (declare (xargs :guard (and (pseudo-termp pat)
          (pseudo-termp x)
          (alistp initial-alist))))
    (b* (((mv match ?alist) (simple-one-way-unify pat x initial-alist)) ((when (or (variablep x) (fquotep x))) (and match (list x)))
        (rest (find-matches-list pat (cdr x) initial-alist)))
      (if match
        (cons x rest)
        rest)))
  (defun find-matches-list
    (pat x initial-alist)
    (declare (xargs :guard (and (pseudo-termp pat)
          (pseudo-term-listp x)
          (alistp initial-alist))))
    (if (atom x)
      nil
      (append (find-matches pat (car x) initial-alist)
        (find-matches-list pat (cdr x) initial-alist)))))

other

(make-flag find-matches-flg find-matches)

other

(defthm-find-matches-flg (defthm pseudo-termp-find-match
    (implies (pseudo-termp x)
      (pseudo-termp (mv-nth 1 (find-match pat x initial-alist))))
    :flag find-matches)
  (defthm pseudo-termp-find-match-list
    (implies (pseudo-term-listp x)
      (pseudo-termp (mv-nth 1 (find-match-list pat x initial-alist))))
    :flag find-matches-list))

other

(defthm-find-matches-flg (defthm pseudo-term-listp-find-matches
    (implies (pseudo-termp x)
      (pseudo-term-listp (find-matches pat x initial-alist)))
    :flag find-matches)
  (defthm pseudo-term-listp-find-matches-list
    (implies (pseudo-term-listp x)
      (pseudo-term-listp (find-matches-list pat x initial-alist)))
    :flag find-matches-list))