• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
      • Defprojection
      • Deflist
      • Defaggregate
      • Define
      • Defmapping
        • Defsurj
        • Defiso
        • Defmapping-implementation
          • Defmapping-event-generation
          • Defmapping-check-redundancy
          • Defmapping-table
          • Defmapping-fn
          • Defmapping-input-processing
            • Defmapping-process-thm-names
            • Defmapping-process-inputs
            • Defmapping-process-function
            • Defmapping-process-functions
            • Defmapping-process-thm-enable
            • Defmapping-thm-keywords
            • Defmapping-process-name
          • Defmapping-macro-definition
        • Definj
      • Defenum
      • Add-io-pairs
      • Defalist
      • Defmapappend
      • Returns-specifiers
      • Defarbrec
      • Defines
      • Define-sk
      • Error-value-tuples
      • Defmax-nat
      • Defmin-int
      • Deftutorial
      • Extended-formals
      • Defrule
      • Defval
      • Defsurj
      • Defiso
      • Defconstrained-recognizer
      • Deffixer
      • Defmvtypes
      • Defconsts
      • Defthm-unsigned-byte-p
      • Support
      • Defthm-signed-byte-p
      • Defthm-natp
      • Defund-sk
      • Defmacro+
      • Defsum
      • Defthm-commutative
      • Definj
      • Defirrelevant
      • Defredundant
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defmapping-input-processing

Defmapping-process-thm-enable

Process the :thm-enable input.

Signature

(defmapping-process-thm-enable thm-enable 
                               beta-of-alpha-thm$ alpha-of-beta-thm$ 
                               guard-thms$ ctx state) 
 
  → 
(mv erp thm-enable$ state)

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-enable$ — Type (keyword-listp thm-enable$).

If the processing is successful, we return a normalized version of this input, namely a list of keywords that specifies which theorems must be enabled, among the ones that are generated.

Definitions and Theorems

Function: defmapping-process-thm-enable

(defun defmapping-process-thm-enable
       (thm-enable beta-of-alpha-thm$ alpha-of-beta-thm$
                   guard-thms$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp beta-of-alpha-thm$)
                             (booleanp alpha-of-beta-thm$)
                             (booleanp guard-thms$))))
 (let ((__function__ 'defmapping-process-thm-enable))
  (declare (ignorable __function__))
  (b*
   (((when (eq thm-enable :all))
     (value
          (defmapping-thm-keywords beta-of-alpha-thm$
                                   alpha-of-beta-thm$ guard-thms$)))
    ((when (eq thm-enable :all-nonguard))
     (value
       (set-difference-eq
            (defmapping-thm-keywords beta-of-alpha-thm$
                                     alpha-of-beta-thm$ guard-thms$)
            '(:doma-guard :domb-guard
                          :alpha-guard :beta-guard))))
    ((unless (keyword-listp thm-enable))
     (er-soft+
      ctx t nil
      "The :THM-ENABLE input, ~x0, is not ~
                   :ALL, :ALL-NOGUARD, or a list of keywords."
      thm-enable))
    ((er &)
     (ensure-list-has-no-duplicates$
          thm-enable
          (msg "The :THM-ENABLE list, ~x0," thm-enable)
          t nil))
    (thms (defmapping-thm-keywords beta-of-alpha-thm$
                                   alpha-of-beta-thm$ guard-thms$))
    ((unless (subsetp-eq thm-enable thms))
     (er-soft+
      ctx t nil
      "The :THM-ENABLE input, ~x0, is not a subset of ~
                   the keywords ~x1 for the generated theorems."
      thm-enable thms)))
   (value thm-enable))))

Theorem: keyword-listp-of-defmapping-process-thm-enable.thm-enable$

(defthm keyword-listp-of-defmapping-process-thm-enable.thm-enable$
  (b* (((mv ?erp ?thm-enable$ ?state)
        (defmapping-process-thm-enable
             thm-enable
             beta-of-alpha-thm$ alpha-of-beta-thm$
             guard-thms$ ctx state)))
    (keyword-listp thm-enable$))
  :rule-classes :rewrite)