		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-thms

Generate all the theorems.

Signature
(defmapping-gen-thms doma$ domb$ alpha$ beta$ a1...an b1...bm beta-of-alpha-thm$ alpha-of-beta-thm$ unconditional$ thm-names$ thm-enable$ appconds appcond-thm-names wrld) → (mv local-events exported-events)
Arguments: doma$ — Guard (pseudo-termfnp doma$).; 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).; beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).; alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).; unconditional$ — Guard (booleanp unconditional$).; thm-names$ — Guard (symbol-symbol-alistp thm-names$).; thm-enable$ — Guard (keyword-listp thm-enable$).; appconds — Guard (evmac-appcond-listp appconds).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; wrld — Guard (plist-worldp wrld).
Returns: local-events — A pseudo-event-form-listp.; exported-events — A pseudo-event-form-listp.

Definitions and Theorems

Function: defmapping-gen-thms

(defun defmapping-gen-thms
       (doma$ domb$ alpha$ beta$ a1...an b1...bm
              beta-of-alpha-thm$ alpha-of-beta-thm$
              unconditional$ thm-names$ thm-enable$
              appconds appcond-thm-names wrld)
  (declare
       (xargs :guard (and (pseudo-termfnp doma$)
                          (pseudo-termfnp domb$)
                          (pseudo-termfnp alpha$)
                          (pseudo-termfnp beta$)
                          (symbol-listp a1...an)
                          (symbol-listp b1...bm)
                          (booleanp beta-of-alpha-thm$)
                          (booleanp alpha-of-beta-thm$)
                          (booleanp unconditional$)
                          (symbol-symbol-alistp thm-names$)
                          (keyword-listp thm-enable$)
                          (evmac-appcond-listp appconds)
                          (symbol-symbol-alistp appcond-thm-names)
                          (plist-worldp wrld))))
  (let ((__function__ 'defmapping-gen-thms))
    (declare (ignorable __function__))
    (b* (((mv appcond-local-events
              appcond-exported-events)
          (defmapping-gen-appcond-thms appconds appcond-thm-names
                                       thm-names$ thm-enable$ wrld))
         ((mv nonappcond-local-events
              nonappcond-exporte-events)
          (defmapping-gen-nonappcond-thms
               doma$ domb$ alpha$ beta$ a1...an b1...bm
               beta-of-alpha-thm$ alpha-of-beta-thm$
               unconditional$ thm-names$
               thm-enable$ appcond-thm-names wrld)))
      (mv (append appcond-local-events
                  nonappcond-local-events)
          (append appcond-exported-events
                  nonappcond-exporte-events)))))