1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
\DOC pure_prove_recursive_function_exists
\TYPE {pure_prove_recursive_function_exists : term -> thm}
\SYNOPSIS
Proves existence of general recursive function but leaves unproven assumptions.
\DESCRIBE
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])
}
\noindent 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)
}
\noindent 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
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))
}
\noindent 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.
\SEEALSO
define, instantiate_casewise_recursion,
prove_general_recursive_function_exists.
\ENDDOC
|
