Logics_ZF/document/ZF.tex

22 provides a streamlined syntax for defining primitive recursive functions over
1627 parameter (one of $A@1$, \ldots, $A@h$) or a recursive occurrence of one of
1636 recursive function definitions.
1648 Trees and forests can be modelled by the mutually recursive datatype
1697 \isa{list.induct} in Fig.\ts\ref{zf-list}.  For mutually recursive
1756 For mutually recursive datatypes, there is a single \isa{case} operator.
1802 not recursive, so only \isa{case_tac} is available.)
1969 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
1970 \index{recursive functions|see{recursion}}
1979 In principle, one could introduce primitive recursive functions by asserting
1981 recursive function over binary trees:
1992 recursive functions on datatypes:
2004 \subsubsection{Syntax of recursive definitions}
2006 The general form of a primitive recursive definition is
2014 contains only the free variables on the left-hand side, and all recursive
2031 You can even use the \isa{primrec} form with non-recursive datatypes and
2038 All arguments, other than the recursive one, must be the same in each equation
2039 and in each recursive call.  To get around this restriction, use explict
2041 define the tail-recursive version of \isa{n\_nodes}, using an
2043 recursive calls.
2060 Now, we can use \isa{n\_nodes\_aux} to define a tail-recursive version
2130   {\it string\/}~\isa{\isasymsubseteq }~{\it string}, associating each recursive set with
2139   a recursive set in the introduction rules.  There \textbf{must} be a theorem
2146   this section; one exception is the primitive recursive functions example;
2160 \item The theory must separately declare the recursive sets as
2163 \item The names of the recursive sets must be identifiers, not infix
2355 operators for handling recursive function definitions.  I have described
2364     recursive definitions within set theory.
2456   inductively defines the set of primitive recursive functions and presents a
2457   proof that Ackermann's function is not primitive recursive.
2466 \item Theory \isa{BT} defines the recursive data structure $\isa{bt}(A)$, labelled binary trees.
2468 \item Theory \isa{Term} defines a recursive data structure for terms
2472   recursive equations over sets.  It constructs sets of trees and forests