prove_recursive_functions_exist : thm -> term -> thm
Prove existence of recursive function over inductive type.
This function has essentially the same interface and functionality as
new_recursive_definition, but it merely proves the existence of the function
rather than defining it.
The first argument to prove_recursive_functions_exist is the primitive
recursion theorem for the concrete type in question; this is normally the
second theorem obtained from define_type. The second argument is a term
giving the desired primitive recursive function definition. The value returned
by prove_recursive_functions_exist is a theorem stating the existence of a
function satisfying the `definition' clauses. This theorem is derived by formal
proof from an instance of the general primitive recursion theorem given as the
Let C1, ..., Cn be the constructors of this type, and let `(Ci vs)'
represent a (curried) application of the ith constructor to a sequence of
variables. Then a curried primitive recursive function fn over ty can be
specified by a conjunction of (optionally universally-quantified) clauses of
where the variables v1, ..., vm, vs are distinct in each
clause, and where in the ith clause fn appears (free) in bodyi only
as part of an application of the form:
in which the variable v of type ty also occurs among the
If is a conjunction of clauses, as described above, then
fn v1 ... (C1 vs1) ... vm = body1 /\
fn v1 ... (C2 vs2) ... vm = body2 /\
fn v1 ... (Cn vsn) ... vm = bodyn
automatically proves the existence of a function fn that satisfies
the defining equations supplied, and returns a theorem:
prove_recursive_functions_exist also allows the supplied definition to omit
clauses for any number of constructors. If a defining equation for the ith
constructor is omitted, then the value of fn at that constructor:
prove_recursive_functions_exist th ``;;
is left unspecified (fn, however, is still a total function).
fn v1 ... (Ci vsi) ... vn
- FAILURE CONDITIONS
Fails if the clauses cannot be matched up with the recursion theorem. You may
find that prove_general_recursive_function_exists still works in such cases.
Here we show that there exists a product function:
`(prod f 0 = 1) /\ (!n. prod f (SUC n) = f(SUC n) * prod f n)`;;
val it : thm =
|- ?prod. prod f 0 = 1 /\ (!n. prod f (SUC n) = f (SUC n) * prod f n)
Often prove_general_recursive_function_exists is an easier route to the same
goal. Its interface is simpler (no need to specify the recursion theorem) and
it is more powerful. However, for suitably constrained definitions
prove_recursive_functions_exist works well and is much more efficient.
It is more usual to want to actually make definitions of recursive functions.
However, if a recursive function is needed in the middle of a proof, and seems
to ad-hoc for general use, you may just use prove_recursive_functions_exist,
perhaps adding the ``definition'' as an assumption of the goal with
- SEE ALSO