Logics_ZF/document/ZF.tex

80   \cdx{restrict}& $[i, i] \To i$        & restriction of a function\\
91 \index{*"` symbol}\index{function applications}
164 In ZF, a function is a set of pairs.  A ZF function~$f$ is simply an
166 $i\To i$.  The infix operator~{\tt`} denotes the application of a function set
199         \rm function space \\
281 single-valued binary predicate is also called a {\bf class function}.
286 function~$\lambda x. b[x]$.  The resulting set consists of all $b[x]$
288 since it applies a function to every element of a set.  The syntax is
329 this to be a set, the function's domain~$A$ must be given.  Using the
330 constant~\cdx{Lambda}, we may express function sets as \isa{Lambda($A$,$\lambda x. b[x]$)} or use the syntax \isa{lam $x$:$A$.\ $b[x]$}.
466 function \cdx{restrict}$(f,A)$ has the same values as~$f$, but only
514 \section{From basic lemmas to function spaces}
657 \caption{The successor function} \label{zf-succ}
689 function, which is defined in terms of~\isa{cons}.  The proof that
852 $\pair{y,x}$ such that $\pair{x,y}\in r$; if $r$ is a function, then
934 the generalized function space.  For example, if $f$ is a function and
939 By \tdx{Pi_type}, a function typing of the form $f\in A\to C$ can be
942 any dependent typing can be flattened to yield a function type of the form
946 describe the graph of the generated function, while \tdx{beta} and
1159 The Knaster-Tarski Theorem states that every monotone function over a
1258   \cdx{id}      & $i\To i$      &       & identity function \\
1259   \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
1260   \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
1261   \cdx{bij}     & $[i,i]\To i$  &       & bijective function space
1307 relation, and three specialized function spaces: injective, surjective and
1420 %\item[\ttindexbold{tcset}] is a function to return the default tcset; use the
1509 operators coerce their arguments to be natural numbers.  The function
1568 applying the function \cdx{intify}.  This function is the identity on integers
1632 A datatype can occur recursively as the argument of some function~$F$.  This
1636 recursive function definitions.
1752 \isa{f_Cons} is a function that computes the value to return if the
1753 argument has the form $\isa{Cons}(a,l)$.  The function can be expressed as
1969 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
1981 recursive function over binary trees:
2017 immaterial.  For missing constructors, the function is defined to return zero.
2040 $\lambda$-abstraction and function application.  For example, let us
2051 Now \isa{n\_nodes\_aux(t)\ `\ k} is our function in two arguments. We
2355 operators for handling recursive function definitions.  I have described
2427   and the finite function space operator.
2457   proof that Ackermann's function is not primitive recursive.
2653 ordered pairs.  The second subgoal is to verify that \isa{f\ \isasymunion \ g} is a function, since
2654 \isa{Pi(?A,?B)} denotes a dependent function space.
2681 function space, and observe that~{\tt?A2} gets instantiated to~\isa{A}.