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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
\DOC new_recursive_definition
\TYPE {new_recursive_definition : (bool -> thm -> string -> conv)}
\SYNOPSIS
Defines a primitive recursive function over a concrete recursive type.
\DESCRIBE
{new_recursive_definition} provides the facility for defining primitive
recursive functions on arbitrary concrete recursive types. It takes four
arguments. The first is a boolean flag which indicates if the recursive
function to be defined will be an infix or not. The second is the primitive
recursion theorem for the concrete type in question; this must be a theorem
obtained from {define_type}. The third argument is a name under which the
resulting definition will be saved in the current theory segment. And the
fourth argument is a term giving the desired primitive recursive function
definition. The value returned by {new_recursive_definition} is a theorem
which states the primitive recursive definition requested by the user. This
theorem is derived by formal proof from an instance of the general primitive
recursion theorem given as the second argument.
A theorem {th} of the form returned by {define_type} is a primitive recursion
theorem for an automatically-defined concrete type {ty}. Let {C1}, ..., {Cn}
be the constructors of this type, and let `{(Ci vs)}' represent a (curried)
application of the {i}th constructor to a sequence of variables. Then a
curried primitive recursive function {fn} over {ty} can be specified by a
conjunction of (optionally universally-quantified) clauses of the form:
{
fn v1 ... (C1 vs1) ... vm = body1 /\
fn v1 ... (C2 vs2) ... vm = body2 /\
.
.
fn v1 ... (Cn vsn) ... vm = bodyn
}
\noindent where the variables {v1}, ..., {vm}, {vs} are distinct in each
clause, and where in the {i}th clause {fn} appears (free) in {bodyi} only
as part of an application of the form:
{
"fn t1 ... v ... tm"
}
\noindent in which the variable {v} of type {ty} also occurs among the
variables {vsi}.
If {<definition>} is a conjunction of clauses, as described above, then
evaluating:
{
new_recursive_definition flag th `name` tm "<definition>";;
}
\noindent automatically proves the existence of a function {fn} that satisfies
the defining equations supplied as the fourth argument, and then declares a new
constant in the current theory with this definition as its specification. This
constant specification is returned as a theorem and is saved in the current
theory segment under the name {name}. If {flag} is {true}, the constant is
given infix status.
{new_recursive_definition} also allows the supplied definition to omit clauses
for any number of constructors. If a defining equation for the {i}th
constructor is omitted, then the value of {fn} at that constructor:
{
fn v1 ... (Ci vsi) ... vn
}
\noindent is left unspecified ({fn}, however, is still a total function).
\FAILURE
A call to {new_recursive_definition} fails if the supplied theorem is not a
primitive recursion theorem of the form returned by {define_type}; if the term
argument supplied is not a well-formed primitive recursive definition; or if
any other condition for making a constant specification is violated (see the
failure conditions for {new_specification}).
\EXAMPLE
Given the following primitive recursion theorem for labelled binary trees:
{
|- !f0 f1.
?! fn.
(!x. fn(LEAF x) = f0 x) /\
(!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
}
\noindent {new_recursive_definition} can be used to define primitive recursive
functions over binary trees. Suppose the value of {th} is this theorem. Then
a recursive function {Leaves}, which computes the number of leaves in a
binary tree, can be defined recursively as shown below:
{
#let Leaves =
# new_recursive_definition false th `Leaves`
# "(Leaves (LEAF (x:*)) = 1) /\
# (Leaves (NODE t1 t2) = (Leaves t1) + (Leaves t2))";;
Leaves =
|- (!x. Leaves(LEAF x) = 1) /\
(!t1 t2. Leaves(NODE t1 t2) = (Leaves t1) + (Leaves t2))
}
\noindent The result is a theorem which states that the constant {Leaves}
satisfies the primitive-recursive defining equations supplied by the user.
The function defined using {new_recursive_definition} need not, in fact, be
recursive. Here is the definition of a predicate {IsLeaf}, which is true of
binary trees which are leaves, but is false of the internal nodes in a binary
tree:
{
#let IsLeaf =
# new_recursive_definition false th `IsLeaf`
# "(IsLeaf (NODE t1 t2) = F) /\ (IsLeaf (LEAF (x:*)) = T)";;
IsLeaf = |- (!t1 t2. IsLeaf(NODE t1 t2) = F) /\ (!x. IsLeaf(LEAF x) = T)
}
\noindent Note that the equations defining a (recursive or non-recursive)
function on binary trees by cases can be given in either order. Here, the
{NODE} case is given first, and the {LEAF} case second. The reverse order was
used in the above definition of {Leaves}.
{new_recursive_definition} also allows the user to partially specify the value
of a function defined on a concrete type, by allowing defining equations for
some of the constructors to be omitted. Here, for example, is the definition
of a function {Label} which extracts the label from a leaf node. The value of
{Label} applied to an internal node is left unspecified:
{
#let Label =
# new_recursive_definition false th `Label`
# "Label (LEAF (x:*)) = x";;
Label = |- !x. Label(LEAF x) = x
}
\noindent Curried functions can also be defined, and the recursion can be on
any argument. The next definition defines an infix (curried) function {<<}
which expresses the idea that one tree is a proper subtree of another.
{
#let Subtree =
# new_recursive_definition true th `Subtree`
# "(<< (t:(*)btree) (LEAF (x:*)) = F) /\
# (<< t (NODE t1 t2) = ((t=t1)\/(t=t2)\/(<< t t1)\/(<< t t2)))";;
Subtree =
|- (!t x. t << (LEAF x) = F) /\
(!t t1 t2.
t << (NODE t1 t2) = (t = t1) \/ (t = t2) \/ t << t1 \/ t << t2)
}
\noindent Note that the first argument is {true}, to indicate that the function
being defined is to have infix status, and that the constant {<<} is an infix
after the definition has been made. Furthermore, the function {<<} is
recursive on its second argument.
\SEEALSO
define_type, prove_rec_fn_exists.
\ENDDOC
|
