prove_rec_fn_exists
Prim_rec.prove_rec_fn_exists : thm -> term -> thm
Proves the existence of a primitive recursive function over a concrete recursive type.
prove_rec_fn_exists is a version of new_recursive_definition which
proves only that the required function exists; it does not make a
constant specification. The first argument is a primitive recursion
theorem of the form generated by Hol_datatype, and the second is a
user-supplied primitive recursive function definition. The theorem which
is returned asserts the existence of the recursively-defined function in
question (if it is primitive recursive over the type characterized by
the theorem given as the first argument). See the entry for
new_recursive_definition for details.
Failure
As for new_recursive_definition.
Example
Given the following primitive recursion theorem for labelled binary trees:
|- !f0 f1.
?fn.
(!a. fn (LEAF a) = f0 a) /\
!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1) : thm
prove_rec_fn_exists can be used to prove the existence of primitive
recursive functions over binary trees. Suppose the value of th is this
theorem. Then the existence of a recursive function Leaves, which
computes the number of leaves in a binary tree, can be proved as shown
below:
- prove_rec_fn_exists th
``(Leaves (LEAF (x:'a)) = 1) /\
(Leaves (NODE t1 t2) = (Leaves t1) + (Leaves t2))``;
> val it =
|- ?Leaves.
(!x. Leaves (LEAF x) = 1) /\
!t1 t2. Leaves (NODE t1 t2) = Leaves t1 + Leaves t2 : thm
The result should be compared with the example given under
new_recursive_definition.