• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
        • Evmac-prepare-proofs
      • 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-proof-preparation

Evmac-prepare-proofs

Events to prepare proof generation.

We disable the default hints and override hints; these are implicitly local events.

We add an explicitly local event to prevent mv-nth from being expanded, which is accomplished via a system attachment.

We add an implicitly local event to set the induction depth limit to 1. This lets generated proofs by inductions work in case :induct hints are not generated. It also prevents nested inductions from working, which arguably should not be used in generated proofs (or even in manual proofs).

We add an implicitly local event to suppress various warnings. This is useful when the generated events are printed in full.

Macro: evmac-prepare-proofs

(defmacro
 evmac-prepare-proofs nil
 '(progn (set-default-hints nil)
         (set-override-hints nil)
         (local (defattach-system simplifiable-mv-nth-p
                                  constant-nil-function-arity-0))
         (set-induction-depth-limit 1)
         (set-inhibit-warnings "disable" "double-rewrite" "free"
                               "non-rec" "subsume" "theory" "use")))