		Search-engine friendly clone of the ACL2 documentation.

Defun-inst

Introduce a function by instantiating a second-order functions.

General Form

(defun-inst fun
  (sofun (fvar1 . fun1) ... (fvarN . funN))
  :verify-guards ...
  :enable ...
  :skolem-name ...
  :thm-name ...
  :rewrite ...
  :constrain ...
  :print ...)

Inputs

fun

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

sofun

Name of the second-order function to instantiate.

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

An instantiation, which specifies how to generate fun from sofun. The function variables fvar1, ..., fvarN must be function parameters of sofun.

:verify-guards

An option to attempt or omit the guard verification of fun. This may be present only if sofun is a plain or quantifier second-order function. If this flag is absent, the guard verification of fun is attempted if and only if sofun is guard-verified.
In general it is not possible to verify the guards of an instance of a second-order function from the guard theorem of the second-order function, because function variables have guard t but may be replaced with functions with stricter guards. Since defun-inst currently does not provide an option to supply guard verification hints for fun, :verify-guards nil may be used to defer the guard verification of fun when it is not accomplished automatically (i.e. without hints). (An option to supply guard verification hints will be added to defun-inst.)

:enable

An option to enable or disable fun, and the associated rewrite rule if sofun is a quantifier second-order-function. This may be present only if sofun is a plain or quantifier second-order function. If this flag is absent, fun (and the associated rewrite rule, if applicable) is enabled if and only if sofun is enabled.

:skolem-name

An option to customize the name of the witness function of fun. This may be present only if sofun is a quantifier second-order function. If present, this input is passed to the defun-sk generated for fun.

:thm-name

An option to customize the name of the rewrite rule of fun. This may be present only if sofun is a quantifier second-order function. If present, this input is passed to the defun-sk generated for fun.

:rewrite

An option to customize the rewrite rule of fun. This may be present only if sofun is a quantifier second-order function and its quantifier is universal. If present, this input is passed to the defun-sk generated for fun. If a term is supplied, it must depend on the same function variables that the body of fun depends on; in particular, if fun is first-order, the term supplied as rewrite rule must not depend on any function variables. If this option is absent and the quantifier is universal, then the rewrite rule of fun has the same form as in sofun; in particular, the function variables in the rewrite rule of sofun are instantiated via the instantiation passed to defun-inst.

:constrain

An option for constraining, instead of defining, fun. This may be present only if sofun is a quantifier second-order function. If present, this input is passed to the defun-sk generated for fun. If this options is absent, then fun is constrained if sofun is constrained, and fun is defined if sofun is defined.

: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 function form and any error output. In all cases, the function variables that the new function depends on are printed; if the new function is first-order, its dependence on no function variables is also printed.

Generated Events

One of the following:

```
; if fun is 2nd-order:
(defun2 fun ...)

; if fun is 1st-order:
(defun fun ...)
```
if sofun is a plain second-order function. The body, measure (if recursive), and guard of fun are obtained by applying the instantiation to the body, measure (if recursive), and guard of sofun. If fun is recursive, its termination proof uses a functional instance of the termination theorem of sofun.
```
; if fun is 2nd-order:
(defchoose2 fun ...)

; if fun is 1st-order:
(defchoose fun ...)
```
if sofun is a choice second-order function. The body of fun is obtained by applying the instantiation to the body of sofun. The :strengthen value of fun is the same as sofun.
```
; if fun is 2nd-order:
(defun-sk2 fun ...)

; if fun is 1st-order:
(defun-sk fun ...)
```
if sofun is a plain second-order function. The body and guard of fun are obtained by applying the instantiation to the body and guard of sofun. The guard of fun is not verified. The :strengthen value of fun is the same as sofun. The :quant-ok value of fun is t.

Examples

Example 1

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

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

;; Wrap a value four times:
(defun-inst quad[wrap]
  (quad[?f] (?f . wrap)))

Example 2

;; Recognize true lists of values that satisfy ?P:
(defun2 all[?p] (l)
  (cond ((atom l) (null l))
        (t (and (?p (car l)) (all[?p] (cdr l))))))

;; Recognize octets:
(defun octetp (x) (and (natp x) (< x 256)))

;; Recognize true lists of octets:
(defun-inst all[octetp]
  (all[?p] (?p . octetp)))

Example 3

;; 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 replacement CODE-CHAR of ?F
;; induces the replacement OCTETP of ?P,
;; because the guard of CODE-CHAR is (equivalent to) OCTECTP.
;; The creation of the MAP[CODE-CHAR][OCTETP] instance of MAP[?F][?P]
;; needs the instance ALL[OCTETP) of ALL[?P] (in the guard),
;; created as in the earlier example.

Example 4

;; Folding function on binary trees:
(defun2 fold[?f][?g] (bt)
  (cond ((atom bt) (?f bt))
        (t (?g (fold[?f][?g] (car bt)) (fold[?f][?g] (cdr bt))))))

;; Add up all the natural numbers in a tree, coercing other values to 0:
(defun-inst fold[nfix][binary-+]
  (fold[?f][?g] (?f . nfix) (?g . binary-+)))

Example 5

;; Return a fixed point of ?F, if any exists:
(defchoose2 fixpoint[?f] x ()
  (equal (?f x) x))

;; Double a value:
(defun twice (x) (* 2 (fix x)))

;; Function constrained to return the (only) fixed point 0 of TWICE:
(defun-inst fixpoint[twice]
  (fixpoint[?f] (?f . twice)))

Example 6

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

Subtopics

Defun-inst-implementation: Implementation of defun-inst.