		Search-engine friendly clone of the ACL2 documentation.

Defmapping-input-processing

Defmapping-thm-keywords

Keywords that identify all the theorems to generate.

Signature
(defmapping-thm-keywords beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$) → thm-keywords
Arguments: beta-of-alpha-thm$ — Guard (booleanp beta-of-alpha-thm$).; alpha-of-beta-thm$ — Guard (booleanp alpha-of-beta-thm$).; guard-thms$ — Guard (booleanp guard-thms$).
Returns: thm-keywords — Type (keyword-listp thm-keywords).

Definitions and Theorems

Function: defmapping-thm-keywords

(defun defmapping-thm-keywords
       (beta-of-alpha-thm$ alpha-of-beta-thm$ guard-thms$)
  (declare (xargs :guard (and (booleanp beta-of-alpha-thm$)
                              (booleanp alpha-of-beta-thm$)
                              (booleanp guard-thms$))))
  (let ((__function__ 'defmapping-thm-keywords))
    (declare (ignorable __function__))
    (append (list :alpha-image :beta-image)
            (and beta-of-alpha-thm$
                 (list :beta-of-alpha :alpha-injective))
            (and alpha-of-beta-thm$
                 (list :alpha-of-beta :beta-injective))
            (and guard-thms$
                 (list :doma-guard :domb-guard
                       :alpha-guard :beta-guard)))))

Theorem: keyword-listp-of-defmapping-thm-keywords

(defthm keyword-listp-of-defmapping-thm-keywords
  (b*
    ((thm-keywords
          (defmapping-thm-keywords beta-of-alpha-thm$
                                   alpha-of-beta-thm$ guard-thms$)))
    (keyword-listp thm-keywords))
  :rule-classes :rewrite)

Theorem: no-duplicatesp-equal-of-defmapping-thm-keywords

(defthm no-duplicatesp-equal-of-defmapping-thm-keywords
  (b*
    ((thm-keywords
          (defmapping-thm-keywords beta-of-alpha-thm$
                                   alpha-of-beta-thm$ guard-thms$)))
    (no-duplicatesp-equal thm-keywords))
  :rule-classes :rewrite)