instantiate_casewise_recursion : term -> thm
Instantiate the general scheme for a recursive function existence assertion.
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:
or on even numbers and odd numbers:
?f. (f  = a) /\ (!h t. CONS h t = k[f,h,t])
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.
?f. (!n. f(2 * n) = a[f,n]) /\ (!n. f(2 * n + 1) = b[f,n])
- 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.
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.
- SEE ALSO