Introduce a theorem by instantiating a second-order theorem.

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

A symbol, which names the new theorem obtained by

instantiating sothm . It must be a valid theorem name that is not already in use.

Name of the second-order theorem to instantiate.

An

instantiation, which specifies how to generate thm fromsothm .sothm mustdepend on at least the function variables fvar1 , ...,fvarN .

An option to specify the rule classes of

thm .

An option to enable or disable

thm . This ist by default, i.e. enable.

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.

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

`defthm-inst`,
its value is used for

;; 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)))

;; 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)))

- Defthm-inst-implementation
- Implementation of
`defthm-inst`.