Introduce a function by instantiating a second-order functions.

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

A symbol, which names the new function obtained by

instantiating sofun . It must be a valid function name that is not already in use.

Name of the second-order function to instantiate.

An

instantiation, which specifies how to generate fun fromsofun . The function variablesfvar1 , ...,fvarN must be function parameters ofsofun .

An option to attempt or omit the guard verification of

fun . This may be present only ifsofun is a plain or quantifier second-order function. If this flag is absent, the guard verification offun is attempted if and only ifsofun 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. Sincedefun-instcurrently does not provide an option to supply guard verification hints forfun ,:verify-guards nil may be used to defer the guard verification offun when it is not accomplished automatically (i.e. without hints). (An option to supply guard verification hints will be added todefun-inst.)

An option to enable or disable

fun , and the associated rewrite rule ifsofun is a quantifier second-order-function. This may be present only ifsofun 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 ifsofun is enabled.

An option to customize the name of the witness function of

fun . This may be present only ifsofun is a quantifier second-order function. If present, this input is passed to thedefun-skgenerated forfun .

An option to customize the name of the rewrite rule of

fun . This may be present only ifsofun is a quantifier second-order function. If present, this input is passed to thedefun-skgenerated forfun .

An option to customize the rewrite rule of

fun . This may be present only ifsofun is a quantifier second-order function and its quantifier is universal. If present, this input is passed to thedefun-skgenerated forfun . If a term is supplied, it mustdepend 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 offun has the same form as insofun ; in particular, the function variables in the rewrite rule ofsofun are instantiated via the instantiation passed todefun-inst.

An option for constraining, instead of defining,

fun . This may be present only ifsofun is a quantifier second-order function. If present, this input is passed to thedefun-skgenerated forfun . If this options is absent, thenfun is constrained ifsofun is constrained, andfun is defined ifsofun is defined.

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.

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 offun are obtained byapplying the instantiation to the body, measure (if recursive), and guard of sofun . Iffun is recursive, its termination proof uses afunctional 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 offun is obtained byapplying the instantiation to the body of sofun . The:strengthen value offun is the same assofun .; 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 offun are obtained byapplying the instantiation to the body and guard of sofun . The guard offun is not verified. The:strengthen value offun is the same assofun . The:quant-ok value offun ist .

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

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

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

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

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

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

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