• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Function-definedness
      • Event-macro-input-processing
      • Event-macro-screen-printing
      • Evmac-input-print-p
      • Make-event-terse
      • Event-macro-applicability-conditions
        • Evmac-input-hints-p
        • Event-macro-applicability-condition-utilities
          • Evmac-appcond-theorem
          • Evmac-appcond-theorem-list
          • Evmac-appcondp
          • Evmac-ensure-no-extra-hints
          • Make-evmac-appcond?
          • Evmac-appcond-theorems-no-extra-hints
          • Evmac-appcond-listp
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Event-macro-applicability-condition-utilities

Evmac-appcond-theorems-no-extra-hints

Combine evmac-appcond-theorem-list and evmac-ensure-no-extra-hints.

Signature

(evmac-appcond-theorems-no-extra-hints 
     appconds 
     hints names-to-avoid print ctx state) 
 
  → 
(mv erp val state)

Arguments

appconds — Guard (evmac-appcond-listp appconds).

hints — Guard (evmac-input-hints-p hints).

names-to-avoid — Guard (symbol-listp names-to-avoid).

print — Guard (evmac-input-print-p print).

Returns

val — Type (std::tuple (events pseudo-event-form-listp) (thm-names keyword-symbol-alistp) (updated-names-to-avoid symbol-listp) val) , given (and (evmac-appcond-listp appconds) (symbol-listp names-to-avoid)).

This function automates the coding pattern in which first one calls evmac-appcond-theorem-list and then evmac-ensure-no-extra-hints on the remaining hints. This combining function returns no hints result.

Definitions and Theorems

Function: evmac-appcond-theorems-no-extra-hints

(defun evmac-appcond-theorems-no-extra-hints
       (appconds hints names-to-avoid print ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (evmac-appcond-listp appconds)
                              (evmac-input-hints-p hints)
                              (symbol-listp names-to-avoid)
                              (evmac-input-print-p print))))
  (let ((__function__ 'evmac-appcond-theorems-no-extra-hints))
    (declare (ignorable __function__))
    (b* (((mv events thm-names
              remaining-hints updated-names-to-avoid)
          (evmac-appcond-theorem-list
               appconds
               hints names-to-avoid print ctx state))
         ((er & :iferr (list nil nil nil))
          (evmac-ensure-no-extra-hints remaining-hints ctx state)))
      (value (list events
                   thm-names updated-names-to-avoid)))))

Theorem: return-type-of-evmac-appcond-theorems-no-extra-hints.val

(defthm return-type-of-evmac-appcond-theorems-no-extra-hints.val
  (implies (and (evmac-appcond-listp appconds)
                (symbol-listp names-to-avoid))
           (b* (((mv ?erp ?val ?state)
                 (evmac-appcond-theorems-no-extra-hints
                      appconds
                      hints names-to-avoid print ctx state)))
             (std::tuple (events pseudo-event-form-listp)
                         (thm-names keyword-symbol-alistp)
                         (updated-names-to-avoid symbol-listp)
                         val)))
  :rule-classes :rewrite)