`define : term -> thm`

SYNOPSIS
Defines a general recursive function.

DESCRIPTION
The function define should be applied to a conjunction of `definitional' clauses `def_1[f] /\ ... /\ def_n[f]` for some variable f, where each clause def_i is a universally quantified equation with an application of f to arguments on the left-hand side. The idea is that these clauses define the action of f on arguments of various kinds, for example on an empty list and nonempty list:
```  (f [] = a) /\ (!h t. CONS h t = k[f,h,t])
```
or on even numbers and odd numbers:
```  (!n. f(2 * n) = a[f,n]) /\ (!n. f(2 * n + 1) = b[f,n])
```
The define function attempts to prove that there is indeed a function satisfying all these properties, and if it succeeds it defines a new function f and returns the input term with the variable f replaced by the newly defined constant.

FAILURE CONDITIONS
Fails if the definition is malformed or if some of the necessary conditions for the definition to be admissible cannot be proved automatically, or if there is already a constant of the given name.

EXAMPLE
This is a `multifactorial' function:
```  # define
`multifactorial m n =
if m = 0 then 1
else if n <= m then n else n * multifactorial m (n - m)`;;
val it : thm =
|- multifactorial m n =
(if m = 0 then 1 else if n <= m then n else n * multifactorial m (n - m))
```
Note that it fails without the m = 0 guard because then there's no reason to suppose that n - m decreases and hence the recursion is apparently illfounded. Perhaps a more surprising example is the Collatz function:
```  # define
`!n. collatz(n) = if n <= 1 then n
else if EVEN(n) then collatz(n DIV 2)
else collatz(3 * n + 1)`;;
```
Note that the definition was made successfully because there provably is a function satisfying these recursion equations, notwithstanding the fact that it is unknown whether the recursion is wellfounded. (Tail-recursive functions are always logically consistent, though they may not have any useful provable properties.)