Instantiate the general scheme for a recursive function existence assertion.
DESCRIPTION
The function instantiate_casewise_recursion should be applied to an
existentially quantified term `?f. def_1[f] /\ ... /\ def_n[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:
The returned value is a theorem whose conclusion matches the input term, with
an assumption sufficient for the existence assertion. This is not normally in a
very convenient form for the user.
FAILURE CONDITIONS
Fails only if the definition is malformed. However it is possible that for an
inadmissible definition the assumption of the theorem may not hold.
USES
This is seldom a convenient function for users. Normally, use
prove_general_recursive_function_exists to prove something like this while
attempting to discharge the side-conditions automatically, or define to
actually make a definition. In situations where the automatic discharge of the
side-conditions fails, one may prefer instead
pure_prove_recursive_function_exists. The even more minimal
instantiate_casewise_recursion is for the rare cases where one wants to force
no processing at all of the side-conditions to be undertaken.