1\DOC new_recursive_definition
2
3\TYPE new_recursive_definition : {name:string, def:term, rec_axiom:thm} -> thm
4
5\SYNOPSIS
6Defines a primitive recursive function over a concrete recursive type.
7
8\DESCRIBE
9{new_recursive_definition} provides a facility for defining primitive
10recursive functions on arbitrary concrete recursive types. {name} is a
11name under which the resulting definition will be saved in the current
12theory segment. {def} is a term giving the desired primitive recursive
13function definition. {rec_axiom} is the primitive recursion theorem for
14the concrete type in question; this must be a theorem obtained from
15{define_type}. The value returned by {new_recursive_definition} is a
16theorem which states the primitive recursive definition requested by the
17user. This theorem is derived by formal proof from an instance of the
18general primitive recursion theorem given as the second argument.
19
20A theorem {th} of the form returned by {define_type} is a primitive recursion
21theorem for an automatically-defined concrete type {ty}.  Let {C1}, ..., {Cn}
22be the constructors of this type, and let `{(Ci vs)}' represent a (curried)
23application of the {i}th constructor to a sequence of variables.  Then a
24curried primitive recursive function {fn} over {ty} can be specified by a
25conjunction of (optionally universally-quantified) clauses of the form:
26{
27   fn v1 ... (C1 vs1) ... vm  =  body1   /\
28   fn v1 ... (C2 vs2) ... vm  =  body2   /\
29                             .
30                             .
31   fn v1 ... (Cn vsn) ... vm  =  bodyn
32}
33where the variables {v1}, ..., {vm}, {vs} are distinct in each
34clause, and where in the {i}th clause {fn} appears (free) in {bodyi} only
35as part of an application of the form:
36{
37   fn t1 ... v ... tm
38}
39in which the variable {v} of type {ty} also occurs among the
40variables {vsi}.
41
42If {tm} is a conjunction of clauses, as described above, then evaluating:
43{
44   new_recursive_definition{name=name, rec_axiom=th, def=tm}
45}
46automatically proves the existence of a function {fn} that satisfies
47the defining equations supplied as the fourth argument, and then declares a new
48constant in the current theory with this definition as its specification. This
49constant specification is returned as a theorem and is saved in the current
50theory segment under the name {name}.
51
52{new_recursive_definition} also allows the supplied definition to omit clauses
53for any number of constructors.  If a defining equation for the {i}th
54constructor is omitted, then the value of {fn} at that constructor:
55{
56   fn v1 ... (Ci vsi) ... vn
57}
58is left unspecified ({fn}, however, is still a total function).
59
60\FAILURE
61A call to {new_recursive_definition} fails if the supplied theorem is not a
62primitive recursion theorem of the form returned by {define_type}; if the term
63argument supplied is not a well-formed primitive recursive definition; or if
64any other condition for making a constant specification is violated (see the
65failure conditions for {new_specification}).
66
67\EXAMPLE
68Given the following primitive recursion theorem for labelled binary trees:
69{
70   |- !f0 f1.
71        ?! fn.
72        (!x. fn(LEAF x) = f0 x) /\
73        (!b1 b2. fn(NODE b1 b2) = f1(fn b1)(fn b2)b1 b2)
74}
75{new_recursive_definition} can be used to define primitive recursive
76functions over binary trees.  Suppose the value of {th} is this theorem.  Then
77a recursive function {Leaves}, which computes the number of leaves in a
78binary tree, can be defined recursively as shown below:
79{
80   - val Leaves = new_recursive_definition
81           {name = "Leaves",
82            rec_axiom = th,
83            def= ���(Leaves (LEAF (x:'a)) = 1) /\
84                    (Leaves (NODE t1 t2) = (Leaves t1) + (Leaves t2))���};
85    > val Leaves =
86        |- (!x. Leaves (LEAF x) = 1) /\
87           !t1 t2. Leaves (NODE t1 t2) = Leaves t1 + Leaves t2 : thm
88}
89The result is a theorem which states that the constant {Leaves}
90satisfies the primitive-recursive defining equations supplied by the user.
91
92The function defined using {new_recursive_definition} need not, in fact, be
93recursive.  Here is the definition of a predicate {IsLeaf}, which is true of
94binary trees which are leaves, but is false of the internal nodes in a binary
95tree:
96{
97   - val IsLeaf = new_recursive_definition
98           {name = "IsLeaf",
99            rec_axiom = th,
100            def = ���(IsLeaf (NODE t1 t2) = F) /\
101                     (IsLeaf (LEAF (x:'a)) = T)���};
102> val IsLeaf = |- (!t1 t2. IsLeaf (NODE t1 t2) = F) /\
103                  !x. IsLeaf (LEAF x) = T : thm
104}
105Note that the equations defining a (recursive or non-recursive)
106function on binary trees by cases can be given in either order.  Here, the
107{NODE} case is given first, and the {LEAF} case second.  The reverse order was
108used in the above definition of {Leaves}.
109
110{new_recursive_definition} also allows the user to partially specify the value
111of a function defined on a concrete type, by allowing defining equations for
112some of the constructors to be omitted.  Here, for example, is the definition
113of a function {Label} which extracts the label from a leaf node.  The value of
114{Label} applied to an internal node is left unspecified:
115{
116   - val Label = new_recursive_definition
117                   {name = "Label",
118                    rec_axiom = th,
119                    def = ���Label (LEAF (x:'a)) = x���};
120   > val Label = |- !x. Label (LEAF x) = x : thm
121}
122Curried functions can also be defined, and the recursion can be on
123any argument.  The next definition defines an infix function {<<} which
124expresses the idea that one tree is a proper subtree of another.
125{
126   - val _ = set_fixity ("<<", Infixl 231);
127
128   - val Subtree = new_recursive_definition
129           {name = "Subtree",
130            rec_axiom = th,
131            def = ���($<< (t:'a bintree) (LEAF (x:'a)) = F) /\
132                     ($<< t (NODE t1 t2) = (t = t1) \/
133                                           (t = t2) \/
134                                           ($<< t t1) \/
135                                           ($<< t t2))���};
136   > val Subtree =
137       |- (!t x. t << LEAF x = F) /\
138          !t t1 t2.
139            t << NODE t1 t2 = (t = t1) \/ (t = t2) \/
140                              (t << t1) \/ (t << t2) : thm
141}
142Note that the fixity of the identifier {<<} is set independently of
143the definition.
144
145\SEEALSO
146bossLib.Hol_datatype, Prim_rec.prove_rec_fn_exists, TotalDefn.Define,
147Parse.set_fixity.
148
149\ENDDOC
150