		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-old-if-new

Generate the old-if-new theorem.

Signature
(solve-gen-old-if-new old-if-new old-if-new-enable old ?f x1...xn new f solution-theorem old-instance) → (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).; x1...xn — Guard (symbol-listp x1...xn).; new — Guard (symbolp new).; f — Guard (symbolp f).; solution-theorem — Guard (symbolp solution-theorem).; old-instance — Guard (symbolp old-instance).
Returns: local-event — Type (pseudo-event-formp local-event).; exported-event — Type (pseudo-event-formp exported-event).

The proof follows the design notes, but those use a second-order notation and explicit quantification, so here we need to do things a little differently. We enable the definition of old, which results in its matrix applied to the witness(es). We enable the rewrite rule of new that turns ?f into f, so that it carries out that replacement in the aforementioned matrix. We add the solution theorem via a :use hint; this theorem has the form (old-instance). We use an instance of the rewrite rule of old-instance, where the quantifier variable(s) is/are instantiated with the witness(es): this results exactly in the matrix with f above, and thus the theorem is proved.

Definitions and Theorems

Function: solve-gen-old-if-new-thm-aux

(defun solve-gen-old-if-new-thm-aux (vars index old-witness)
 (declare (xargs :guard (and (symbol-listp vars)
                             (natp index)
                             (symbolp old-witness))))
 (let ((__function__ 'solve-gen-old-if-new-thm-aux))
  (declare (ignorable __function__))
  (cond
   ((endp vars) nil)
   (t
    (cons
       (cons (car vars)
             (cons (cons 'mv-nth
                         (cons index
                               (cons (cons old-witness 'nil) 'nil)))
                   'nil))
       (solve-gen-old-if-new-thm-aux (cdr vars)
                                     (1+ index)
                                     old-witness))))))

Theorem: doublet-listp-of-solve-gen-old-if-new-thm-aux

(defthm doublet-listp-of-solve-gen-old-if-new-thm-aux
  (b* ((instantiation
            (solve-gen-old-if-new-thm-aux vars index old-witness)))
    (doublet-listp instantiation))
  :rule-classes :rewrite)

Function: solve-gen-old-if-new

(defun solve-gen-old-if-new
       (old-if-new old-if-new-enable old ?f x1...xn
                   new f solution-theorem old-instance)
 (declare (xargs :guard (and (symbolp old-if-new)
                             (booleanp old-if-new-enable)
                             (symbolp old)
                             (symbolp ?f)
                             (symbol-listp x1...xn)
                             (symbolp new)
                             (symbolp f)
                             (symbolp solution-theorem)
                             (symbolp old-instance))))
 (let ((__function__ 'solve-gen-old-if-new))
  (declare (ignorable __function__))
  (b*
   ((formula (cons 'implies
                   (cons (cons new 'nil)
                         (cons (cons old 'nil) 'nil))))
    (new-rwrule (packn-pos (list ?f '-to- f) new))
    (old-instance-rwrule (add-suffix-to-fn old-instance "-NECC"))
    (old-witness (add-suffix-to-fn old "-WITNESS"))
    (instantiation
         (if (>= (len x1...xn) 2)
             (solve-gen-old-if-new-thm-aux x1...xn 0 old-witness)
           (cons (cons (car x1...xn)
                       (cons (cons old-witness 'nil) 'nil))
                 'nil)))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons 'quote
               (cons (cons old (cons new-rwrule 'nil))
                     'nil))
         (cons
          ':use
          (cons
           (cons
               solution-theorem
               (cons (cons ':instance
                           (cons old-instance-rwrule instantiation))
                     'nil))
           'nil)))))
      'nil)))
   (evmac-generate-defthm old-if-new
                          :enable old-if-new-enable
                          :formula formula
                          :hints hints))))

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

(defthm pseudo-event-formp-of-solve-gen-old-if-new.local-event
  (b* (((mv ?local-event ?exported-event)
        (solve-gen-old-if-new old-if-new
                              old-if-new-enable old ?f x1...xn
                              new f solution-theorem old-instance)))
    (pseudo-event-formp local-event))
  :rule-classes :rewrite)

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

(defthm pseudo-event-formp-of-solve-gen-old-if-new.exported-event
  (b* (((mv ?local-event ?exported-event)
        (solve-gen-old-if-new old-if-new
                              old-if-new-enable old ?f x1...xn
                              new f solution-theorem old-instance)))
    (pseudo-event-formp exported-event))
  :rule-classes :rewrite)