prove_rec_fn_existsPrim_rec.prove_rec_fn_exists : thm -> term -> thmProves 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.
As for new_recursive_definition.
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) : thmprove_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 : thmThe result should be compared with the example given under
new_recursive_definition.