		Search-engine friendly clone of the ACL2 documentation.

Aignet-extension-p

Aignet-extension-binding

A strategy for making use of aignet-extension-p in rewrite rules.

Rewrite rules using aignet-extension-p are a little odd. For example, suppose we want a rewrite rule just based on the definition, e.g.,

(implies (and (aignet-extension-p new-aignet orig-aignet)
              (aignet-idp id orig-aignet))
         (equal (lookup-id id new-aignet)
                (lookup-id id orig-aignet)))

This isn't a very good rewrite rule because it has to match the free variable orig-aignet. However, we can make it much better with a bind-free strategy. We'll check the syntax of new-aignet to see if it is a call of a aignet-updating function. Then, we'll use the aignet input of that function as the binding for orig-aignet aignet-extension-binding is a macro that implements this binding strategy. In this case, it can be used as follows:

(implies (and (aignet-extension-binding :new new-aignet :orig orig-aignet)
              (aignet-idp id orig-aignet))
         (equal (lookup-id id new-aignet)
                (lookup-id id orig-aignet)))

For a given invocation of aignet-extension-binding, it is assumed that the new argument is a currently bound variable and the orig argument is a variable that needs a binding.

See also aignet-extension-bind-inverse for a similar macro that instead binds a new aignet given an invocation of some function that finds a suffix.

Definitions and Theorems

Function: simple-search-type-alist

(defun simple-search-type-alist (term typ type-alist unify-subst)
  (cond ((endp type-alist) (mv nil unify-subst))
        ((acl2::ts-subsetp (cadr (car type-alist))
                           typ)
         (mv-let (ans unify-subst)
                 (acl2::one-way-unify1 term (car (car type-alist))
                                       unify-subst)
           (if ans (mv t unify-subst)
             (simple-search-type-alist term typ (cdr type-alist)
                                       unify-subst))))
        (t (simple-search-type-alist term typ (cdr type-alist)
                                     unify-subst))))

Theorem: aignet-extension-p-transitive-rw

(defthm aignet-extension-p-transitive-rw
  (implies (and (aignet-extension-binding :new aignet3
                                          :orig aignet2)
                (aignet-extension-p aignet2 aignet1))
           (aignet-extension-p aignet3 aignet1)))

Theorem: aignet-extension-implies-fanin-count-gte

(defthm aignet-extension-implies-fanin-count-gte
  (implies (aignet-extension-binding)
           (<= (fanin-count orig)
               (fanin-count new)))
  :rule-classes ((:linear :trigger-terms ((fanin-count new)))))

Theorem: aignet-extension-implies-stype-count-gte

(defthm aignet-extension-implies-stype-count-gte
 (implies (aignet-extension-binding)
          (<= (stype-count stype orig)
              (stype-count stype new)))
 :rule-classes ((:linear :trigger-terms ((stype-count stype new)))))

Theorem: aignet-extension-p-implies-consp

(defthm aignet-extension-p-implies-consp
  (implies (and (aignet-extension-binding)
                (consp orig))
           (consp new)))