Logics_ZF/document/ZF.tex

18 \texttt{ZF} has a flexible package for handling inductive definitions,
19 such as inference systems, and datatype definitions, such as lists and
20 trees.  Moreover it handles coinductive definitions, such as
21 bisimulation relations, and codatatype definitions, such as streams.  It
411 \caption{Further definitions of ZF} \label{zf-defs}
419 definitions.  In particular, bounded quantifiers and the subset relation
443 The definitions of general intersection, etc., are straightforward.  Note
450 Further definitions appear in Fig.\ts\ref{zf-defs}.  Ordered pairs are
464 Note the simple definitions of $\lambda$-abstraction (using
515 Faced with so many definitions, it is essential to prove lemmas.  Even
517 prove from the definitions alone.  Isabelle's set theory derives many
1076 unions play a role in datatype definitions, particularly when there is
1107 definitions, for example of infinite lists~\cite{paulson-mscs}.
1164 These are essential to many definitions that follow, including the natural
1590 \section{Datatype definitions}
1636 recursive function definitions.
1763 The theory syntax for datatype definitions is shown in the
1825 con_defs        \textrm{definitions of the case operator and constructors}
1840 undocumented features of the datatype package.  Datatype definitions are
1841 reduced to inductive definitions, and the advanced features should be
1969 \subsection{Recursive function definitions}\label{sec:ZF:recursive}
1975   recursion}.  Such definitions rely on the recursion operator defined by the
2004 \subsubsection{Syntax of recursive definitions}
2081 \section{Inductive and coinductive definitions}
2095 definitions.  They may be intermixed with other declarations; in
2099 Each (co)inductive definition adds definitions to the theory and also
2117   con_defs    {\it constructor definitions}
2143 \item[\it constructor definitions] contain definitions of constants
2145   the constructors' definitions here.  Most (co)inductive definitions omit
2193 The chief problem with making (co)inductive definitions involves type-checking
2273 Finally, here are some coinductive definitions.  We begin by defining
2296 The Isabelle distribution contains many other inductive definitions.  Simple
2299 definitions.  Larger examples may be found on other subdirectories of
2312 defs          \textrm{definitions of inductive sets}
2322 inductive definitions as it is for datatypes.  There are many examples
2355 operators for handling recursive function definitions.  I have described
2364     recursive definitions within set theory.
2437 definitions, and demonstrates their use.
2478   definitions, inductive definitions, structural induction and rule
2582 the symbols are replaced by their definitions.