		Search-engine friendly clone of the ACL2 documentation.

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.