		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-alpha-injective

Generate the :alpha-injective theorem.

Signature
(defmapping-gen-alpha-injective doma$ alpha$ beta$ a1...an b1...bm unconditional$ thm-names$ thm-enable$ appcond-thm-names wrld) → (mv local-event exported-event)
Arguments: doma$ — Guard (pseudo-termfnp doma$).; 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 :beta-of-alpha-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 \beta to both sides of the equality \alpha(a)=\alpha(a'). The hints for these proofs are the same whether :unconditional is t or nil.

Definitions and Theorems

Function: defmapping-gen-alpha-injective

(defun defmapping-gen-alpha-injective
       (doma$ alpha$ beta$ a1...an
              b1...bm unconditional$ thm-names$
              thm-enable$ appcond-thm-names wrld)
 (declare
      (xargs :guard (and (pseudo-termfnp doma$)
                         (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-alpha-injective))
  (declare (ignorable __function__))
  (b*
   ((aa1...aan (defmapping-gen-var-aa/bb a1...an))
    (name (cdr (assoc-eq :alpha-injective thm-names$)))
    (formula
     (b*
      ((antecedent (if unconditional$ *t*
                     (conjoin2 (apply-term doma$ a1...an)
                               (apply-term doma$ aa1...aan))))
       (consequent
         (cons 'equal
               (cons (cons 'equal
                           (cons (apply-term alpha$ a1...an)
                                 (cons (apply-term alpha$ aa1...aan)
                                       'nil)))
                     (cons (conjoin-equalities a1...an aa1...aan)
                           'nil))))
       (formula (implicate antecedent consequent)))
      (untranslate formula t wrld)))
    (hints
     (b*
      ((beta-of-alpha
            (cdr (assoc-eq :beta-of-alpha appcond-thm-names)))
       (beta-of-alpha-instance
        (cons
           ':instance
           (cons beta-of-alpha
                 (alist-to-doublets (pairlis$ a1...an aa1...aan)))))
       (m (len b1...bm))
       (cases-hints-formula
        (if
         (= m 1)
         (cons
          'equal
          (cons
             (apply-term* beta$ (apply-term alpha$ a1...an))
             (cons (apply-term* beta$ (apply-term alpha$ aa1...aan))
                   'nil)))
         (cons
          'equal
          (cons
           (apply-term
                beta$
                (make-mv-nth-calls (apply-term alpha$ a1...an)
                                   m))
           (cons
               (apply-term
                    beta$
                    (make-mv-nth-calls (apply-term alpha$ aa1...aan)
                                       m))
               'nil))))))
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          'nil
          (cons
           ':cases
           (cons
               (cons cases-hints-formula 'nil)
               (cons ':use
                     (cons (cons beta-of-alpha
                                 (cons beta-of-alpha-instance 'nil))
                           'nil)))))))
       'nil)))
    (defthmr/defthmdr (if (member-eq :alpha-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))))