		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-beta-injective

Generate the :beta-injective theorem.

Signature
(defmapping-gen-beta-injective domb$ alpha$ beta$ a1...an b1...bm unconditional$ thm-names$ thm-enable$ appcond-thm-names wrld) → (mv local-event exported-event)
Arguments: domb$ — Guard (pseudo-termfnp domb$).; alpha$ — Guard (pseudo-termfnp alpha$).; beta$ — Guard (pseudo-termfnp beta$).; a1...an — Guard (symbol-listp a1...an).; b1...bm — Guard (symbol-listp b1...bm).; unconditional$ — Guard (booleanp unconditional$).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

This function is called if only if the :alpha-of-beta-thm input is t.

We generate hints based on the proofs in the design notes. The :cases hints correspond, in the proof in the design notes, to the inference step that applies \alpha to both sides of the equality \beta(b)=\beta(b'). The hints for these proofs are the same whether :unconditional is t or nil.

Definitions and Theorems

Function: defmapping-gen-beta-injective

(defun defmapping-gen-beta-injective
       (domb$ alpha$ beta$ a1...an
              b1...bm unconditional$ thm-names$
              thm-enable$ appcond-thm-names wrld)
 (declare
      (xargs :guard (and (pseudo-termfnp domb$)
                         (pseudo-termfnp alpha$)
                         (pseudo-termfnp beta$)
                         (symbol-listp a1...an)
                         (symbol-listp b1...bm)
                         (booleanp unconditional$)
                         (symbol-symbol-alistp thm-names$)
                         (keyword-listp thm-enable$)
                         (symbol-symbol-alistp appcond-thm-names)
                         (plist-worldp wrld))))
 (let ((__function__ 'defmapping-gen-beta-injective))
  (declare (ignorable __function__))
  (b*
   ((bb1...bbm (defmapping-gen-var-aa/bb b1...bm))
    (name (cdr (assoc-eq :beta-injective thm-names$)))
    (formula
     (b*
      ((antecedent (if unconditional$ *t*
                     (conjoin2 (apply-term domb$ b1...bm)
                               (apply-term domb$ bb1...bbm))))
       (consequent
          (cons 'equal
                (cons (cons 'equal
                            (cons (apply-term beta$ b1...bm)
                                  (cons (apply-term beta$ bb1...bbm)
                                        'nil)))
                      (cons (conjoin-equalities b1...bm bb1...bbm)
                            'nil))))
       (formula (implicate antecedent consequent)))
      (untranslate formula t wrld)))
    (hints
     (b*
      ((alpha-of-beta
            (cdr (assoc-eq :alpha-of-beta appcond-thm-names)))
       (alpha-of-beta-instance
        (cons
           ':instance
           (cons alpha-of-beta
                 (alist-to-doublets (pairlis$ b1...bm bb1...bbm)))))
       (n (len a1...an))
       (cases-hints-formula
        (if
         (= n 1)
         (cons
          'equal
          (cons
             (apply-term* alpha$ (apply-term beta$ b1...bm))
             (cons (apply-term* alpha$ (apply-term beta$ bb1...bbm))
                   'nil)))
         (cons
          'equal
          (cons
           (apply-term alpha$
                       (make-mv-nth-calls (apply-term beta$ b1...bm)
                                          n))
           (cons
                (apply-term
                     alpha$
                     (make-mv-nth-calls (apply-term beta$ bb1...bbm)
                                        n))
                'nil))))))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          'nil
          (cons
           ':cases
           (cons
               (cons cases-hints-formula 'nil)
               (cons ':use
                     (cons (cons alpha-of-beta
                                 (cons alpha-of-beta-instance 'nil))
                           'nil)))))))
       'nil)))
    (defthmr/defthmdr (if (member-eq :beta-injective thm-enable$)
                          'defthmr
                        'defthmdr))
    (local-event
     (cons
         'local
         (cons (cons defthmr/defthmdr
                     (cons name
                           (cons formula
                                 (cons ':hints (cons hints 'nil)))))
               'nil)))
    (exported-event (cons defthmr/defthmdr
                          (cons name (cons formula 'nil)))))
   (mv local-event exported-event))))