pure_prove_recursive_function_exists : term -> thm

SYNOPSIS

Proves existence of general recursive function but leaves unproven assumptions.

DESCRIPTION

The function pure_prove_recursive_function_exists 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:

  ?f. (f [] = a) /\ (!h t. CONS h t = k[f,h,t])

or on even numbers and odd numbers:

  ?f. (!n. f(2 * n) = a[f,n]) /\ (!n. f(2 * n + 1) = b[f,n])

The returned value is a theorem whose conclusion matches the input term, with in general one or two assumptions stating what properties must hold so that the existence of such a function to be deduced. Roughly, one assumption states that the clauses are not mutually contradictory, as in

  ?f. (!n. f(n + 1) = 1) /\ (!n. f(n + 2) = 2)

and the other states that there is some wellfounded order making any recursion admissible. This rule attempts to eliminate any hypotheses of the first kind, but does not attempt to guess a wellfounded ordering as prove_general_recursive_function_exists does.

FAILURE CONDITIONS

Fails only if the definition is malformed. However it is possible that for an inadmissible definition the assumptions of the theorem may not hold.

EXAMPLE

In the definition of the Fibonacci numbers, the function successfully eliminates the mutual consistency hypotheses:

  # pure_prove_recursive_function_exists
     `?fib. fib 0 = 1 /\ fib 1 = 1 /\
            !n. fib(n + 2) = fib(n) + fib(n + 1)`;;
  val it : thm =
    ?(<<). WF (<<) /\ (!n. T ==> n << n + 2) /\ (!n. T ==> n + 1 << n + 2)
    |- ?fib. fib 0 = 1 /\ fib 1 = 1 /\ (!n. fib (n + 2) = fib n + fib (n + 1))

but leaves a wellfounded ordering to be given. (By contrast, prove_general_recursive_function_exists will automatically eliminate it.)

USES

Normally, use prove_general_recursive_function_exists for this operation. Use the present function only when the attempt by prove_general_recursive_function_exists to discharge the proof obligations is not successful and merely wastes time.