		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-ext-table

Generate the event that extends the defmapping table.

Signature
(defmapping-gen-ext-table name$ doma$ domb$ alpha$ beta$ unconditional$ thm-names$ call$ expansion) → event
Arguments: name$ — Guard (symbolp name$).; doma$ — Guard (pseudo-termfnp doma$).; domb$ — Guard (pseudo-termfnp domb$).; alpha$ — Guard (pseudo-termfnp alpha$).; beta$ — Guard (pseudo-termfnp beta$).; unconditional$ — Guard (booleanp unconditional$).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; call$ — Guard (pseudo-event-formp call$).; expansion — Guard (pseudo-event-formp expansion).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defmapping-gen-ext-table

(defun defmapping-gen-ext-table
       (name$ doma$ domb$ alpha$ beta$ unconditional$
              thm-names$ call$ expansion)
 (declare (xargs :guard (and (symbolp name$)
                             (pseudo-termfnp doma$)
                             (pseudo-termfnp domb$)
                             (pseudo-termfnp alpha$)
                             (pseudo-termfnp beta$)
                             (booleanp unconditional$)
                             (symbol-symbol-alistp thm-names$)
                             (pseudo-event-formp call$)
                             (pseudo-event-formp expansion))))
 (let ((__function__ 'defmapping-gen-ext-table))
   (declare (ignorable __function__))
   (b*
     ((alpha-image (cdr (assoc-eq :alpha-image thm-names$)))
      (beta-image (cdr (assoc-eq :beta-image thm-names$)))
      (beta-of-alpha (cdr (assoc-eq :beta-of-alpha thm-names$)))
      (alpha-of-beta (cdr (assoc-eq :alpha-of-beta thm-names$)))
      (alpha-injective (cdr (assoc-eq :alpha-injective thm-names$)))
      (beta-injective (cdr (assoc-eq :beta-injective thm-names$)))
      (doma-guard (cdr (assoc-eq :doma-guard thm-names$)))
      (domb-guard (cdr (assoc-eq :domb-guard thm-names$)))
      (alpha-guard (cdr (assoc-eq :alpha-guard thm-names$)))
      (beta-guard (cdr (assoc-eq :beta-guard thm-names$)))
      (info (make-defmapping-info :call$ call$
                                  :expansion expansion
                                  :doma doma$
                                  :domb domb$
                                  :alpha alpha$
                                  :beta beta$
                                  :alpha-image alpha-image
                                  :beta-image beta-image
                                  :beta-of-alpha beta-of-alpha
                                  :alpha-of-beta alpha-of-beta
                                  :alpha-injective alpha-injective
                                  :beta-injective beta-injective
                                  :doma-guard doma-guard
                                  :domb-guard domb-guard
                                  :alpha-guard alpha-guard
                                  :beta-guard beta-guard
                                  :unconditional unconditional$)))
     (cons 'table
           (cons *defmapping-table-name*
                 (cons (cons 'quote (cons name$ 'nil))
                       (cons (cons 'quote (cons info 'nil))
                             'nil)))))))

Theorem: pseudo-event-formp-of-defmapping-gen-ext-table

(defthm pseudo-event-formp-of-defmapping-gen-ext-table
  (b* ((event (defmapping-gen-ext-table
                   name$
                   doma$ domb$ alpha$ beta$ unconditional$
                   thm-names$ call$ expansion)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)