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