		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-old-to-new

Generate the theorem that relates the old and new functions.

Signature
(restrict-gen-old-to-new old restriction new new-body old-to-new old-to-new-enable appcond-thm-names stub? old-unnorm new-unnorm wrld) → (mv local-event exported-event)
Arguments: old — Guard (symbolp old).; restriction — Guard (pseudo-termp restriction).; new — Guard (symbolp new).; new-body — Guard (pseudo-termp new-body).; old-to-new — Guard (symbolp old-to-new).; old-to-new-enable — Guard (booleanp old-to-new-enable).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; stub? — Guard (symbolp stub?).; old-unnorm — Guard (symbolp old-unnorm).; new-unnorm — Guard (symbolp new-unnorm).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

The macro used to introduce the theorem is determined by whether the theorem must be enabled or not.

The formula of the theorem equates old and new functions under the restricting predicate, as described in the documentation.

If the old and new functions are not recursive, then, following the design notes, the theorem is proved in the theory consisting of the non-normalized definitions of the functions.

If the old and new functions are recursive, then, following the design notes, the theorem is proved by induction on the old function, utilizing the non-normalized definitions of the functions and the applicability condition. We have seen at least one case in which a definition was not expanded, presumably due to some ACL2 heuristics. Using :expand hints does not work when the restricting predicate equates a formal with a quoted constant, because in that case ACL2 may replace the formal with the constant, preventing the :expand from applying. So we generate proof builder instructions to apply the induction rule, claims the non-normalized definitions (which are thus added as hypothesis to the induction step), and prove the induction step(s) and base case(s). Since there may be multiple induction step(s) and/or base case(s), we repeat the same proof builder instructions until there are no more goals. If the old and new functions are reflexive, we functionally instantiate the stub in that applicability condition, in the induction step.

Definitions and Theorems

Function: restrict-gen-old-to-new

(defun restrict-gen-old-to-new
       (old restriction new new-body old-to-new
            old-to-new-enable appcond-thm-names
            stub? old-unnorm new-unnorm wrld)
 (declare
      (xargs :guard (and (symbolp old)
                         (pseudo-termp restriction)
                         (symbolp new)
                         (pseudo-termp new-body)
                         (symbolp old-to-new)
                         (booleanp old-to-new-enable)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp stub?)
                         (symbolp old-unnorm)
                         (symbolp new-unnorm)
                         (plist-worldp wrld))))
 (let ((__function__ 'restrict-gen-old-to-new))
  (declare (ignorable __function__))
  (b*
    ((formals (formals old wrld))
     (formula
          (implicate restriction
                     (cons 'equal
                           (cons (cons old formals)
                                 (cons (cons new formals) 'nil)))))
     (formula (untranslate formula t wrld))
     (recursive (recursivep old nil wrld)))
   (if recursive
    (b*
     ((lemma-name
       (cdr (assoc-eq :restriction-of-rec-calls appcond-thm-names)))
      (lemma-instance
           (if stub? (cons ':functional-instance
                           (cons lemma-name
                                 (cons (cons stub? (cons new 'nil))
                                       'nil)))
             lemma-name))
      (instructions
       (cons
        (cons 'in-theory
              (cons (cons 'enable
                          (cons (cons ':induction (cons old 'nil))
                                'nil))
                    'nil))
        (cons
         (cons
          'then
          (cons
           (cons 'induct
                 (cons (cons old formals) 'nil))
           (cons
            (cons
             'do-all
             (cons
              (cons
               'claim
               (cons
                (cons 'equal
                      (cons (cons old formals)
                            (cons (ubody old wrld) 'nil)))
                (cons
                 ':hints
                 (cons
                  (cons
                   (cons
                    '"Goal"
                    (cons
                     ':in-theory
                     (cons
                          (cons 'quote
                                (cons (cons old-unnorm 'nil) 'nil))
                          (cons ':expand
                                (cons (cons (cons old formals) 'nil)
                                      'nil)))))
                   'nil)
                  'nil))))
              (cons
               (cons
                'claim
                (cons
                 (cons 'equal
                       (cons (cons new formals)
                             (cons new-body 'nil)))
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                          (cons 'quote
                                (cons (cons new-unnorm 'nil) 'nil))
                          (cons ':expand
                                (cons (cons (cons new formals) 'nil)
                                      'nil)))))
                    'nil)
                   'nil))))
               (cons
                (cons
                 'prove
                 (cons
                  ':hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                            (cons old-unnorm (cons new-unnorm 'nil))
                            'nil))
                       (cons ':use
                             (cons lemma-instance 'nil)))))
                    'nil)
                   'nil)))
                'nil))))
            'nil)))
         'nil))))
     (evmac-generate-defthm old-to-new
                            :formula formula
                            :instructions instructions
                            :enable old-to-new-enable))
    (b*
     ((hints
       (cons
        (cons
         '"Goal"
         (cons
          ':in-theory
          (cons (cons 'quote
                      (cons (cons old-unnorm (cons new-unnorm 'nil))
                            'nil))
                'nil)))
        'nil)))
     (evmac-generate-defthm old-to-new
                            :formula formula
                            :hints hints
                            :enable old-to-new-enable))))))