1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
\DOC define
\TYPE {define : term -> thm}
\SYNOPSIS
Defines a general recursive function.
\DESCRIBE
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])
}
\noindent 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
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.)
\COMMENTS
Assuming the definition is well-formed and the constant name is unused, failure
indicates that {define} was unable to prove one or both of the following two
properties: (i) the clauses are not mutually inconsistent (more than one clause
could apply to some arguments, and the results are not obviously the same), or
(ii) the definition is recursive and no ordering justifying the recursion could
be arrived at by the automated heuristic. In order to make progress in such
cases, try applying {prove_general_recursive_function_exists} or
{pure_prove_recursive_function_exists} to the same definition with existential
quantification over {f}, to see the unproven side-conditions. An example is in
the documentation for {prove_general_recursive_function_exists}. On the other
hand, for suitably simple and regular primitive recursive definitions,
the explicit alternative {prove_recursive_functions_exist} is often much faster
than any of these.
\SEEALSO
new_definition, new_recursive_definition, new_specification,
prove_general_recursive_function_exists, prove_recursive_functions_exist,
pure_prove_recursive_function_exists.
\ENDDOC
|
