Recursion and Induction: The Definitional Principle

Below we give a new definitional principle that subsumes the previously given Principle of Structural Recursion.

The definition

`(defun` *f* `(`*v_1* … *v_n*`)` *β*`)`

is *admissible* if and only if

*f*is a new function symbol,- the
*v_i*are distinct variable symbols, *β*is a term that mentions no variable other than the*v_i*and calls no new function symbol other than (possibly)*f*, and- there is a term
*m*(called the*measure*) such that the following are theorems:*Ordinal Conjecture*`(o-p`*m*`)`*Measure Conjecture(s)*For each recursive call of`(`*f a_1*…*a_n*`)`in*β*and the conjunction*q*of tests ruling it,`(implies`*q*`(o<`*m*/*σ**m*`))`where

*σ*is`{`*v_1*←*a_1*, … ,*v_n*←*a_n*`}`.

If that definition is admissible, then it adds the axiom:

`(`*f* *v_1* … *v_n*`) = `*β*.

In each of the problems below, admit the proposed definition, i.e., identify the measure and prove the required theorems.

(Maybe explore <<`defun`>>? Note in particular how the
user can explicitly specify the measure and well-founded relation alleged to
decrease. When specified, the system will attempt to prove it decreases as
per the Definitional Principle. If no measure is specified by the user, the
system attempts to find an argument whose `ACL2-count` decreases
according to `o<`.)

**Problem 95. **

(defun tree-copy (x) (if (atom x) x (cons (tree-copy (first x)) (tree-copy (rest x)))))

**Problem 96. **

(defun ack (x y) (if (zp x) 1 (if (zp y) (if (equal x 1) 2 (+ x 2)) (ack (ack (- x 1) y) (- y 1)))))

**Problem 97. ** Recursion like that in

**Problem 98. **

(defun f1 (i j) (if (and (natp i) (natp j) (< i j)) (f1 (+ 1 i) j) 1))

**Problem 99. **

(defun f2 (x) (if (equal x nil) 2 (and (f2 (car x)) (f2 (cdr x)))))

**Problem 100. **

(defun f3 (x y) (if (and (endp x) (endp y)) 3 (f3 (cdr x) (cdr y))))

**Problem 101. ** Suppose

Theoremdn-spec (and (o-p (m x)) (implies (p x) (o< (m (dn x)) (m x))))

Then admit

(defun f4 (x y q) (if (p x) (if q (f4 y (dn x) (not q)) (f4 y (up x) (not q))) 4))

Note that `f4` is swapping its arguments. Thus, if `q` starts at
`t`, say, then in successive calls the first argument is `x`,
`y`, `(dn x)`, `(up y)`, `(dn (dn x))`, `(up (up y))`,
etc. I thank Anand Padmanaban for helping me think of
and solve this problem.

Next: