Prim_rec.new_recursive

STRUCTURE

SYNOPSIS

Defines a primitive recursive function over a concrete recursive type.

DESCRIPTION

new_recursive_definition provides a facility for defining primitive recursive functions on arbitrary concrete recursive types. name is a name under which the resulting definition will be saved in the current theory segment. def is a term giving the desired primitive recursive function definition. rec_axiom is the primitive recursion theorem for the concrete type in question; this must be a theorem obtained from define_type. 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 ith 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

where the variables v1, ..., vm, vs are distinct in each clause, and where in the ith clause fn appears (free) in bodyi only as part of an application of the form:

   fn t1 ... v ... tm

in which the variable v of type ty also occurs among the variables vsi.

If tm is a conjunction of clauses, as described above, then evaluating:

   new_recursive_definition{name=name, rec_axiom=th,def=tm}

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.

new_recursive_definition also allows the supplied definition to omit clauses for any number of constructors. If a defining equation for the ith constructor is omitted, then the value of fn at that constructor:

   fn v1 ... (Ci vsi) ... vn

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)

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:

   - val Leaves = new_recursive_definition
           {name = "Leaves",
            rec_axiom = th,
            def= --`(Leaves (LEAF (x:'a)) = 1) /\
                    (Leaves (NODE t1 t2) = (Leaves t1) + (Leaves t2))`--};
    > val Leaves =
        |- (!x. Leaves (LEAF x) = 1) /\
           !t1 t2. Leaves (NODE t1 t2) = Leaves t1 + Leaves t2 : thm

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:

   - val IsLeaf = new_recursive_definition
           {name = "IsLeaf",
            rec_axiom = th,
            def = --`(IsLeaf (NODE t1 t2) = F) /\
                     (IsLeaf (LEAF (x:'a)) = T)`--};
> val IsLeaf = |- (!t1 t2. IsLeaf (NODE t1 t2) = F) /\ 
                  !x. IsLeaf (LEAF x) = T : thm

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:

   - val Label = new_recursive_definition
                   {name = "Label",
                    rec_axiom = th,
                     def = --`Label (LEAF (x:'a)) = x`--};
   > val Label = |- !x. Label (LEAF x) = x : thm

Curried functions can also be defined, and the recursion can be on any argument. The next definition defines an infix function << which expresses the idea that one tree is a proper subtree of another.

   - val _ = set_fixity ("<<", Infixl 231);

   - val Subtree = new_recursive_definition
           {name = "Subtree",
            rec_axiom = th,
            def = --`($<< (t:'a bintree) (LEAF (x:'a)) = F) /\
                     ($<< t (NODE t1 t2) = (t = t1) \/
                                           (t = t2) \/
                                           ($<< t t1) \/
                                           ($<< t t2))`--};
   > val Subtree =
       |- (!t x. t << LEAF x = F) /\
          !t t1 t2.
            t << NODE t1 t2 = (t = t1) \/ (t = t2) \/ 
                              (t << t1) \/ (t << t2) : thm

Note that the fixity of the identifier << is set independently of the definition.

SEEALSO

Hol_datatype, prove_rec_fn_exists, Define, set_fixity