• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
        • Defun-inst
        • Defequal
        • Defsoft
        • Defthm-inst
          • Defthm-inst-implementation
        • Defun2
        • Defunvar
        • Defun-sk2
        • Defchoose2
        • Defthm-2nd-order
        • Define-sk2
        • Defund-sk2
        • Define2
        • Defund2
      • Updates-to-workshop-material
      • Soft-implementation
      • Soft-notions
    • 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

• Soft-macros
• Second-order-theorem-instances

Defthm-inst

Introduce a theorem by instantiating a second-order theorem.

General Form

(defthm-inst thm
  (sothm (fvar1 . fun1) ... (fvarN . funN))
  :rule-classes ...
  :enable ...
  :print ...)

Inputs

thm

A symbol, which names the new theorem obtained by instantiating sothm. It must be a valid theorem name that is not already in use.

sothm

Name of the second-order theorem to instantiate.

((fvar1 . fun1) ... (fvarN . funN))

An instantiation, which specifies how to generate thm from sothm. sothm must depend on at least the function variables fvar1, ..., fvarN.

:rule-classes

An option to specify the rule classes of thm.

:enable

An option to enable or disable thm. This is t by default, i.e. enable.

:print ...

An option to customize the screen output: :all to print all the output; nil to print only any error output; :result (the default) to print only the generated theorem form and any error output.

Generated Events

(defthm thm
  formula
  ... ; proof
  :rule-classes ...)

thm is introduced as a theorem, whose formula formula is obtained by applying the instantiation to the formula of sothm. The proof uses a functional instance of sothm. If :rule-classes is supplied to defthm-inst, its value is used for thm; otherwise, its value is copied from sothm.

Examples

Example 1

;; Homomorphically lift ?F to on true lists of ?P values:
(defun2 map[?f][?p] (l)
  (declare (xargs :guard (all[?p] l)))
  (cond ((endp l) nil)
        (t (cons (?f (car l)) (map[?f][?p] (cdr l))))))

;; Translate lists of octets to lists of characters:
(defun-inst map[code-char][octetp]
  (map[?f][?p] (?f . code-char) (?p . octetp)))

;; The homomorphic lifting of ?F to lists of ?P values
;; preserves the length of the list:
(defthm len-of-map[?f][?p]
  (equal (len (map[?f][?p] l)) (len l)))

;; MAP[CODE-CHAR][OCTETP] preserves the length of the list:
(defthm-inst len-of-map[code-char][octetp]
  (len-of-map[?f][?p] (?f . code-char) (?p . octetp)))

Example 2

;; Apply ?F four times to X:
(defun2 quad[?f] (x)
  (?f (?f (?f (?f x)))))

;; Recognize injective functions:
(defun-sk2 injective[?f] ()
  (forall (x y) (implies (equal (?f x) (?f y)) (equal x y))))

;; Recognize functions whose four-fold application is injective:
(defun-inst injective[quad[?f]] (?f)
  (injective[?f] (?f . quad[?f])))

;; Wrap a value into a singleton list:
(defun wrap (x) (list x))

;; The four-fold application of an injective function is injective:
(defthm injective[quad[?f]]-when-injective[?f]
  (implies (injective[?f]) (injective[quad[?f]]))
  :hints ...)

;; Needed by DEFTHM-INST below to apply its instantiation:
(defun-inst injective[quad[wrap]]
  (injective[quad[?f]] (?f . wrap)))

;; Needed by DEFTHM-INST below to apply its instantiation:
(defun-inst injective[wrap]
  (injective[?f] (?f . wrap)))

;; QUAD[WRAP] is injective if WRAP is:
(defthm-inst injective[quad[wrap]]-when-injective[wrap]
  (injective[quad[?f]]-when-injective[?f] (?f . wrap)))

Subtopics

Defthm-inst-implementation

Implementation of defthm-inst.