		Search-engine friendly clone of the ACL2 documentation.

Schemalg-event-generation

Schemalg-gen-old-if-new

Generate the theorem old-if-new.

Signature
(schemalg-gen-old-if-new old-if-new old-if-new-enable old ?f x-x1...xn x-z1...zm x-a1...am x equal-algo new algo algo-correct) → (mv local-event exported-event)
Arguments: old-if-new — Guard (symbolp old-if-new).; old-if-new-enable — Guard (booleanp old-if-new-enable).; old — Guard (symbolp old).; ?f — Guard (symbolp ?f).; x-x1...xn — Guard (symbol-listp x-x1...xn).; x-z1...zm — Guard (symbol-listp x-z1...zm).; x-a1...am — Guard (symbol-listp x-a1...am).; x — Guard (symbolp x).; equal-algo — Guard (symbolp equal-algo).; new — Guard (symbolp new).; algo — Guard (symbolp algo).; algo-correct — Guard (symbolp algo-correct).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

Definitions and Theorems

Function: schemalg-gen-old-if-new

(defun schemalg-gen-old-if-new
       (old-if-new old-if-new-enable
                   old ?f x-x1...xn x-z1...zm x-a1...am
                   x equal-algo new algo algo-correct)
 (declare (xargs :guard (and (symbolp old-if-new)
                             (booleanp old-if-new-enable)
                             (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x-x1...xn)
                             (symbol-listp x-z1...zm)
                             (symbol-listp x-a1...am)
                             (symbolp x)
                             (symbolp equal-algo)
                             (symbolp new)
                             (symbolp algo)
                             (symbolp algo-correct))))
 (let ((__function__ 'schemalg-gen-old-if-new))
  (declare (ignorable __function__))
  (b*
   ((formula (cons 'implies
                   (cons (cons new 'nil)
                         (cons (cons old 'nil) 'nil))))
    (old-witness (add-suffix-to-fn old "-WITNESS"))
    (equal-algo-l2r (packn-pos (list ?f '-to- algo)
                               equal-algo))
    (x-x1...xn-subst
     (if
      (>= (len x-x1...xn) 2)
      (loop$
           for var in x-x1...xn
           as i from 0 to (1- (len x-x1...xn))
           collect
           (cons var
                 (cons 'mv-nth
                       (cons i
                             (cons (cons old-witness 'nil) 'nil)))))
      (list (cons x (cons old-witness 'nil)))))
    (x-x1...xn-instantiation (alist-to-doublets x-x1...xn-subst))
    (x-z1...zm-instantiation
         (loop$ for
                z in x-z1...zm as a in x-a1...am collect
                (cons z
                      (cons (sublis-var x-x1...xn-subst a)
                            'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons 'quote
               (cons (cons old (cons new 'nil)) 'nil))
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons equal-algo-l2r x-z1...zm-instantiation))
            (cons (cons ':instance
                        (cons algo-correct x-x1...xn-instantiation))
                  'nil))
           'nil)))))
      'nil)))
   (evmac-generate-defthm old-if-new
                          :formula formula
                          :hints hints
                          :enable old-if-new-enable))))

Theorem: pseudo-event-formp-of-schemalg-gen-old-if-new.local-event

(defthm pseudo-event-formp-of-schemalg-gen-old-if-new.local-event
  (b*
    (((mv ?local-event ?exported-event)
      (schemalg-gen-old-if-new old-if-new old-if-new-enable
                               old ?f x-x1...xn x-z1...zm x-a1...am
                               x equal-algo new algo algo-correct)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-schemalg-gen-old-if-new.exported-event

(defthm pseudo-event-formp-of-schemalg-gen-old-if-new.exported-event
  (b*
    (((mv ?local-event ?exported-event)
      (schemalg-gen-old-if-new old-if-new old-if-new-enable
                               old ?f x-x1...xn x-z1...zm x-a1...am
                               x equal-algo new algo algo-correct)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)