• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
      • Simplify-defun
      • Isodata
      • Tailrec
      • Schemalg
      • Restrict
      • Expdata
      • Casesplit
        • Casesplit-implementation
          • Casesplit-event-generation
            • Casesplit-gen-everything
            • Casesplit-gen-new-fn
            • Casesplit-gen-old-to-new-thm
            • Casesplit-gen-appconds-new-guard
            • Casesplit-gen-appconds
            • Casesplit-gen-appconds-thm-hyp
            • Casesplit-gen-appcond-new-guard
            • Casesplit-gen-appcond-name-from-parts
            • Casesplit-gen-appconds-cond-guard
            • Casesplit-gen-appcond-thm-hyp
            • Casesplit-gen-appcond-cond-guard
            • Casesplit-gen-appconds-new-guard-aux
            • Casesplit-gen-appcond-cond-guard-name
            • Casesplit-gen-appcond-thm-hyp-name
            • Casesplit-gen-appcond-new-guard-name
          • Casesplit-fn
          • Casesplit-input-processing
          • Casesplit-macro-definition
          • Casesplit-library-extensions
      • Simplify-term
      • Simplify-defun-sk
      • Parteval
      • Solve
      • Wrap-output
      • Propagate-iso
      • Simplify
      • Finite-difference
      • Drop-irrelevant-params
      • Copy-function
      • Lift-iso
      • Rename-params
      • Utilities
      • Simplify-term-programmatic
      • Simplify-defun-sk-programmatic
      • Simplify-defun-programmatic
      • Simplify-defun+
      • Common-options
      • Common-concepts
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Casesplit-event-generation

Casesplit-gen-appconds

Generate the applicability conditions that are present for the current call of the transformation, in the order given in the reference documentation.

Signature

(casesplit-gen-appconds old$ conditions$ 
                        hyps news verify-guards$ state) 
 
  → 
appconds

Arguments

old$ — Guard (symbolp old$).

conditions$ — Guard (pseudo-term-listp conditions$).

hyps — Guard (pseudo-term-listp hyps).

news — Guard (pseudo-term-listp news).

verify-guards$ — Guard (booleanp verify-guards$).

Returns

appconds — An evmac-appcond-listp.

Definitions and Theorems

Function: casesplit-gen-appconds

(defun casesplit-gen-appconds (old$ conditions$
                                    hyps news verify-guards$ state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-term-listp conditions$)
                             (pseudo-term-listp hyps)
                             (pseudo-term-listp news)
                             (booleanp verify-guards$))))
 (declare
      (xargs :guard (and (= (len hyps) (1+ (len conditions$)))
                         (= (len news) (1+ (len conditions$))))))
 (let ((__function__ 'casesplit-gen-appconds))
  (declare (ignorable __function__))
  (if verify-guards$
   (append
     (casesplit-gen-appconds-thm-hyp conditions$ hyps (w state))
     (casesplit-gen-appconds-cond-guard old$ conditions$ state)
     (casesplit-gen-appconds-new-guard old$ conditions$ news state))
   (casesplit-gen-appconds-thm-hyp conditions$ hyps (w state)))))