1.1 --- a/doc-src/HOL/HOL.tex Mon Aug 28 13:50:24 2000 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Mon Aug 28 13:52:38 2000 +0200
1.3 @@ -5,41 +5,34 @@
1.4
1.5 The theory~\thydx{HOL} implements higher-order logic. It is based on
1.6 Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
1.7 -Church's original paper~\cite{church40}. Andrews's
1.8 -book~\cite{andrews86} is a full description of the original
1.9 -Church-style higher-order logic. Experience with the {\sc hol} system
1.10 -has demonstrated that higher-order logic is widely applicable in many
1.11 -areas of mathematics and computer science, not just hardware
1.12 -verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It is
1.13 -weaker than {\ZF} set theory but for most applications this does not
1.14 -matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
1.15 -to~{\ZF}.
1.16 -
1.17 -The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
1.18 -different syntax. Ancient releases of Isabelle included still another version
1.19 -of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
1.20 -version no longer exists, but \thydx{ZF} supports a similar style of
1.21 -reasoning.} follows $\lambda$-calculus and functional programming. Function
1.22 -application is curried. To apply the function~$f$ of type
1.23 -$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply
1.24 -write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that
1.25 -$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered
1.26 -pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.
1.27 -
1.28 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
1.29 -identifies object-level types with meta-level types, taking advantage of
1.30 -Isabelle's built-in type-checker. It identifies object-level functions
1.31 -with meta-level functions, so it uses Isabelle's operations for abstraction
1.32 -and application.
1.33 -
1.34 -These identifications allow Isabelle to support \HOL\ particularly
1.35 -nicely, but they also mean that \HOL\ requires more sophistication
1.36 -from the user --- in particular, an understanding of Isabelle's type
1.37 -system. Beginners should work with \texttt{show_types} (or even
1.38 -\texttt{show_sorts}) set to \texttt{true}.
1.39 -% Gain experience by
1.40 -%working in first-order logic before attempting to use higher-order logic.
1.41 -%This chapter assumes familiarity with~{\FOL{}}.
1.42 +Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a
1.43 +full description of the original Church-style higher-order logic. Experience
1.44 +with the {\sc hol} system has demonstrated that higher-order logic is widely
1.45 +applicable in many areas of mathematics and computer science, not just
1.46 +hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It
1.47 +is weaker than ZF set theory but for most applications this does not matter.
1.48 +If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
1.49 +
1.50 +The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different
1.51 + syntax. Ancient releases of Isabelle included still another version of~HOL,
1.52 + with explicit type inference rules~\cite{paulson-COLOG}. This version no
1.53 + longer exists, but \thydx{ZF} supports a similar style of reasoning.}
1.54 +follows $\lambda$-calculus and functional programming. Function application
1.55 +is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to
1.56 +the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no
1.57 +`apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means ``$f$ applied to
1.58 +the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle
1.59 +a,b\rangle$ as in ZF.
1.60 +
1.61 +HOL has a distinct feel, compared with ZF and CTT. It identifies object-level
1.62 +types with meta-level types, taking advantage of Isabelle's built-in
1.63 +type-checker. It identifies object-level functions with meta-level functions,
1.64 +so it uses Isabelle's operations for abstraction and application.
1.65 +
1.66 +These identifications allow Isabelle to support HOL particularly nicely, but
1.67 +they also mean that HOL requires more sophistication from the user --- in
1.68 +particular, an understanding of Isabelle's type system. Beginners should work
1.69 +with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.
1.70
1.71
1.72 \begin{figure}
1.73 @@ -123,7 +116,7 @@
1.74 & | & "?!~~" id~id^* " . " formula \\
1.75 \end{array}
1.76 \]
1.77 -\caption{Full grammar for \HOL} \label{hol-grammar}
1.78 +\caption{Full grammar for HOL} \label{hol-grammar}
1.79 \end{figure}
1.80
1.81
1.82 @@ -135,12 +128,11 @@
1.83 $\lnot(a=b)$.
1.84
1.85 \begin{warn}
1.86 - \HOL\ has no if-and-only-if connective; logical equivalence is expressed
1.87 - using equality. But equality has a high priority, as befitting a
1.88 - relation, while if-and-only-if typically has the lowest priority. Thus,
1.89 - $\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.
1.90 - When using $=$ to mean logical equivalence, enclose both operands in
1.91 - parentheses.
1.92 + HOL has no if-and-only-if connective; logical equivalence is expressed using
1.93 + equality. But equality has a high priority, as befitting a relation, while
1.94 + if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$
1.95 + abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$
1.96 + to mean logical equivalence, enclose both operands in parentheses.
1.97 \end{warn}
1.98
1.99 \subsection{Types and overloading}
1.100 @@ -156,7 +148,7 @@
1.101 term} if $\sigma$ and~$\tau$ do, allowing quantification over
1.102 functions.
1.103
1.104 -\HOL\ allows new types to be declared as subsets of existing types;
1.105 +HOL allows new types to be declared as subsets of existing types;
1.106 see~{\S}\ref{sec:HOL:Types}. ML-like datatypes can also be declared; see
1.107 ~{\S}\ref{sec:HOL:datatype}.
1.108
1.109 @@ -218,12 +210,11 @@
1.110
1.111 \subsection{Binders}
1.112
1.113 -Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for
1.114 -some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
1.115 -denote something, a description is always meaningful, but we do not
1.116 -know its value unless $P$ defines it uniquely. We may write
1.117 -descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax
1.118 -\hbox{\tt SOME~$x$.~$P[x]$}.
1.119 +Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$
1.120 +satisfying~$P$, if such exists. Since all terms in HOL denote something, a
1.121 +description is always meaningful, but we do not know its value unless $P$
1.122 +defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x.
1.123 +P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.
1.124
1.125 Existential quantification is defined by
1.126 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]
1.127 @@ -272,7 +263,7 @@
1.128 the constant~\cdx{Let}. It can be expanded by rewriting with its
1.129 definition, \tdx{Let_def}.
1.130
1.131 -\HOL\ also defines the basic syntax
1.132 +HOL also defines the basic syntax
1.133 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
1.134 as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}
1.135 and \sdx{of} are reserved words. Initially, this is mere syntax and has no
1.136 @@ -305,9 +296,8 @@
1.137 \caption{The \texttt{HOL} rules} \label{hol-rules}
1.138 \end{figure}
1.139
1.140 -Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
1.141 -with their~{\ML} names. Some of the rules deserve additional
1.142 -comments:
1.143 +Figure~\ref{hol-rules} shows the primitive inference rules of~HOL, with
1.144 +their~{\ML} names. Some of the rules deserve additional comments:
1.145 \begin{ttdescription}
1.146 \item[\tdx{ext}] expresses extensionality of functions.
1.147 \item[\tdx{iff}] asserts that logically equivalent formulae are
1.148 @@ -342,14 +332,14 @@
1.149 \end{figure}
1.150
1.151
1.152 -\HOL{} follows standard practice in higher-order logic: only a few
1.153 -connectives are taken as primitive, with the remainder defined obscurely
1.154 +HOL follows standard practice in higher-order logic: only a few connectives
1.155 +are taken as primitive, with the remainder defined obscurely
1.156 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
1.157 corresponding definitions \cite[page~270]{mgordon-hol} using
1.158 -object-equality~({\tt=}), which is possible because equality in
1.159 -higher-order logic may equate formulae and even functions over formulae.
1.160 -But theory~\HOL{}, like all other Isabelle theories, uses
1.161 -meta-equality~({\tt==}) for definitions.
1.162 +object-equality~({\tt=}), which is possible because equality in higher-order
1.163 +logic may equate formulae and even functions over formulae. But theory~HOL,
1.164 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
1.165 +definitions.
1.166 \begin{warn}
1.167 The definitions above should never be expanded and are shown for completeness
1.168 only. Instead users should reason in terms of the derived rules shown below
1.169 @@ -401,7 +391,7 @@
1.170 \subcaption{Logical equivalence}
1.171
1.172 \end{ttbox}
1.173 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
1.174 +\caption{Derived rules for HOL} \label{hol-lemmas1}
1.175 \end{figure}
1.176
1.177
1.178 @@ -584,8 +574,8 @@
1.179 \section{A formulation of set theory}
1.180 Historically, higher-order logic gives a foundation for Russell and
1.181 Whitehead's theory of classes. Let us use modern terminology and call them
1.182 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
1.183 -theory, and behave more like {\ZF} classes.
1.184 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
1.185 +and behave more like ZF classes.
1.186 \begin{itemize}
1.187 \item
1.188 Sets are given by predicates over some type~$\sigma$. Types serve to
1.189 @@ -597,17 +587,17 @@
1.190 Although sets may contain other sets as elements, the containing set must
1.191 have a more complex type.
1.192 \end{itemize}
1.193 -Finite unions and intersections have the same behaviour in \HOL\ as they
1.194 -do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
1.195 -denoting the universal set for the given type.
1.196 +Finite unions and intersections have the same behaviour in HOL as they do
1.197 +in~ZF. In HOL the intersection of the empty set is well-defined, denoting the
1.198 +universal set for the given type.
1.199
1.200 \subsection{Syntax of set theory}\index{*set type}
1.201 -\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
1.202 -essentially the same as $\alpha\To bool$. The new type is defined for
1.203 -clarity and to avoid complications involving function types in unification.
1.204 -The isomorphisms between the two types are declared explicitly. They are
1.205 -very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while
1.206 -\hbox{\tt op :} maps in the other direction (ignoring argument order).
1.207 +HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially
1.208 +the same as $\alpha\To bool$. The new type is defined for clarity and to
1.209 +avoid complications involving function types in unification. The isomorphisms
1.210 +between the two types are declared explicitly. They are very natural:
1.211 +\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
1.212 +maps in the other direction (ignoring argument order).
1.213
1.214 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
1.215 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
1.216 @@ -623,11 +613,11 @@
1.217 \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
1.218 \end{eqnarray*}
1.219
1.220 -The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
1.221 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
1.222 -occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
1.223 -x. P[x])$. It defines sets by absolute comprehension, which is impossible
1.224 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
1.225 +The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of
1.226 +suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain
1.227 +free occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.
1.228 +P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF;
1.229 +the type of~$x$ implicitly restricts the comprehension.
1.230
1.231 The set theory defines two {\bf bounded quantifiers}:
1.232 \begin{eqnarray*}
1.233 @@ -867,14 +857,13 @@
1.234
1.235
1.236 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
1.237 -obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
1.238 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
1.239 -are designed for classical reasoning; the rules \tdx{subsetD},
1.240 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
1.241 -strictly necessary but yield more natural proofs. Similarly,
1.242 -\tdx{equalityCE} supports classical reasoning about extensionality,
1.243 -after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for
1.244 -proofs pertaining to set theory.
1.245 +obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such
1.246 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
1.247 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
1.248 +not strictly necessary but yield more natural proofs. Similarly,
1.249 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
1.250 +fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for proofs
1.251 +pertaining to set theory.
1.252
1.253 Figure~\ref{hol-subset} presents lattice properties of the subset relation.
1.254 Unions form least upper bounds; non-empty intersections form greatest lower
1.255 @@ -927,7 +916,7 @@
1.256 \section{Generic packages}
1.257 \label{sec:HOL:generic-packages}
1.258
1.259 -\HOL\ instantiates most of Isabelle's generic packages, making available the
1.260 +HOL instantiates most of Isabelle's generic packages, making available the
1.261 simplifier and the classical reasoner.
1.262
1.263 \subsection{Simplification and substitution}
1.264 @@ -972,17 +961,17 @@
1.265 additional (first) subgoal.
1.266 \end{ttdescription}
1.267
1.268 - \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
1.269 - for an equality throughout a subgoal and its hypotheses. This tactic uses
1.270 - \HOL's general substitution rule.
1.271 +HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
1.272 +equality throughout a subgoal and its hypotheses. This tactic uses HOL's
1.273 +general substitution rule.
1.274
1.275 \subsubsection{Case splitting}
1.276 \label{subsec:HOL:case:splitting}
1.277
1.278 -\HOL{} also provides convenient means for case splitting during
1.279 -rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt
1.280 -then\dots else\dots} often require a case distinction on $b$. This is
1.281 -expressed by the theorem \tdx{split_if}:
1.282 +HOL also provides convenient means for case splitting during rewriting. Goals
1.283 +containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
1.284 +often require a case distinction on $b$. This is expressed by the theorem
1.285 +\tdx{split_if}:
1.286 $$
1.287 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~
1.288 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))
1.289 @@ -1035,9 +1024,9 @@
1.290
1.291 \subsection{Classical reasoning}
1.292
1.293 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
1.294 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.295 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
1.296 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
1.297 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
1.298 +Fig.\ts\ref{hol-lemmas2} above.
1.299
1.300 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and
1.301 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
1.302 @@ -1143,11 +1132,10 @@
1.303
1.304
1.305 \section{Types}\label{sec:HOL:Types}
1.306 -This section describes \HOL's basic predefined types ($\alpha \times
1.307 -\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
1.308 -introducing new types in general. The most important type
1.309 -construction, the \texttt{datatype}, is treated separately in
1.310 -{\S}\ref{sec:HOL:datatype}.
1.311 +This section describes HOL's basic predefined types ($\alpha \times \beta$,
1.312 +$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new
1.313 +types in general. The most important type construction, the
1.314 +\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.
1.315
1.316
1.317 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
1.318 @@ -1407,7 +1395,7 @@
1.319
1.320 \subsection{Numerical types and numerical reasoning}
1.321
1.322 -The integers (type \tdx{int}) are also available in \HOL, and the reals (type
1.323 +The integers (type \tdx{int}) are also available in HOL, and the reals (type
1.324 \tdx{real}) are available in the logic image \texttt{HOL-Real}. They support
1.325 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and
1.326 multiplication (\texttt{*}), and much else. Type \tdx{int} provides the
1.327 @@ -1608,14 +1596,14 @@
1.328
1.329 \subsection{Introducing new types} \label{sec:typedef}
1.330
1.331 -The \HOL-methodology dictates that all extensions to a theory should
1.332 -be \textbf{definitional}. The type definition mechanism that
1.333 -meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},
1.334 -which are inherited from {\Pure} and described elsewhere, are just
1.335 -syntactic abbreviations that have no logical meaning.
1.336 +The HOL-methodology dictates that all extensions to a theory should be
1.337 +\textbf{definitional}. The type definition mechanism that meets this
1.338 +criterion is \ttindex{typedef}. Note that \emph{type synonyms}, which are
1.339 +inherited from Pure and described elsewhere, are just syntactic abbreviations
1.340 +that have no logical meaning.
1.341
1.342 \begin{warn}
1.343 - Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
1.344 + Types in HOL must be non-empty; otherwise the quantifier rules would be
1.345 unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
1.346 \end{warn}
1.347 A \bfindex{type definition} identifies the new type with a subset of
1.348 @@ -1679,8 +1667,8 @@
1.349 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
1.350 and its inverse $Abs_T$.
1.351 \end{itemize}
1.352 -Below are two simple examples of \HOL\ type definitions. Non-emptiness
1.353 -is proved automatically here.
1.354 +Below are two simple examples of HOL type definitions. Non-emptiness is
1.355 +proved automatically here.
1.356 \begin{ttbox}
1.357 typedef unit = "{\ttlbrace}True{\ttrbrace}"
1.358
1.359 @@ -1709,7 +1697,7 @@
1.360 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
1.361 \end{ttbox}
1.362 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
1.363 -class of all \HOL\ types.
1.364 +class of all HOL types.
1.365 \end{warn}
1.366
1.367
1.368 @@ -2746,7 +2734,7 @@
1.369 \item \textit{function} is the name of the function, either as an \textit{id}
1.370 or a \textit{string}.
1.371
1.372 -\item \textit{rel} is a {\HOL} expression for the well-founded termination
1.373 +\item \textit{rel} is a HOL expression for the well-founded termination
1.374 relation.
1.375
1.376 \item \textit{congruence rules} are required only in highly exceptional
1.377 @@ -2852,14 +2840,14 @@
1.378 proves some theorems. Each definition creates an \ML\ structure, which is a
1.379 substructure of the main theory structure.
1.380
1.381 -This package is related to the \ZF\ one, described in a separate
1.382 +This package is related to the ZF one, described in a separate
1.383 paper,%
1.384 \footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is
1.385 distributed with Isabelle.} %
1.386 which you should refer to in case of difficulties. The package is simpler
1.387 -than \ZF's thanks to \HOL's extra-logical automatic type-checking. The types
1.388 -of the (co)inductive sets determine the domain of the fixedpoint definition,
1.389 -and the package does not have to use inference rules for type-checking.
1.390 +than ZF's thanks to HOL's extra-logical automatic type-checking. The types of
1.391 +the (co)inductive sets determine the domain of the fixedpoint definition, and
1.392 +the package does not have to use inference rules for type-checking.
1.393
1.394
1.395 \subsection{The result structure}
1.396 @@ -2990,10 +2978,9 @@
1.397 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction
1.398 rule is \texttt{Fin.induct}.
1.399
1.400 -For another example, here is a theory file defining the accessible
1.401 -part of a relation. The paper
1.402 -\cite{paulson-CADE} discusses a \ZF\ version of this example in more
1.403 -detail.
1.404 +For another example, here is a theory file defining the accessible part of a
1.405 +relation. The paper \cite{paulson-CADE} discusses a ZF version of this
1.406 +example in more detail.
1.407 \begin{ttbox}
1.408 Acc = WF + Inductive +
1.409
1.410 @@ -3041,9 +3028,9 @@
1.411 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
1.412 and $\eta$ reduction~\cite{Nipkow-CR}.
1.413
1.414 -Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of
1.415 -substitutions and unifiers. It is based on Paulson's previous
1.416 -mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
1.417 +Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory
1.418 +of substitutions and unifiers. It is based on Paulson's previous
1.419 +mechanisation in LCF~\cite{paulson85} of Manna and Waldinger's
1.420 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef},
1.421 with nested recursion.
1.422
1.423 @@ -3053,8 +3040,8 @@
1.424 \item Theory \texttt{PropLog} proves the soundness and completeness of
1.425 classical propositional logic, given a truth table semantics. The only
1.426 connective is $\imp$. A Hilbert-style axiom system is specified, and its
1.427 - set of theorems defined inductively. A similar proof in \ZF{} is
1.428 - described elsewhere~\cite{paulson-set-II}.
1.429 + set of theorems defined inductively. A similar proof in ZF is described
1.430 + elsewhere~\cite{paulson-set-II}.
1.431
1.432 \item Theory \texttt{Term} defines the datatype \texttt{term}.
1.433
1.434 @@ -3083,7 +3070,7 @@
1.435 \end{itemize}
1.436
1.437 Directory \texttt{HOL/ex} contains other examples and experimental proofs in
1.438 -{\HOL}.
1.439 +HOL.
1.440 \begin{itemize}
1.441 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef}
1.442 to define recursive functions. Another example is \texttt{Fib}, which
1.443 @@ -3135,7 +3122,7 @@
1.444 of~$\alpha$. This version states that for every function from $\alpha$ to
1.445 its powerset, some subset is outside its range.
1.446
1.447 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
1.448 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and
1.449 the operator \cdx{range}.
1.450 \begin{ttbox}
1.451 context Set.thy;
1.452 @@ -3205,12 +3192,11 @@
1.453 {\out No subgoals!}
1.454 \end{ttbox}
1.455 How much creativity is required? As it happens, Isabelle can prove this
1.456 -theorem automatically. The default classical set \texttt{claset()} contains rules
1.457 -for most of the constructs of \HOL's set theory. We must augment it with
1.458 -\tdx{equalityCE} to break up set equalities, and then apply best-first
1.459 -search. Depth-first search would diverge, but best-first search
1.460 -successfully navigates through the large search space.
1.461 -\index{search!best-first}
1.462 +theorem automatically. The default classical set \texttt{claset()} contains
1.463 +rules for most of the constructs of HOL's set theory. We must augment it with
1.464 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
1.465 +Depth-first search would diverge, but best-first search successfully navigates
1.466 +through the large search space. \index{search!best-first}
1.467 \begin{ttbox}
1.468 choplev 0;
1.469 {\out Level 0}
2.1 --- a/doc-src/HOL/Makefile Mon Aug 28 13:50:24 2000 +0200
2.2 +++ b/doc-src/HOL/Makefile Mon Aug 28 13:52:38 2000 +0200
2.3 @@ -13,7 +13,7 @@
2.4
2.5 NAME = logics-HOL
2.6 FILES = logics-HOL.tex ../Logics/syntax.tex HOL.tex \
2.7 - ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
2.8 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
2.9
2.10 dvi: $(NAME).dvi
2.11
3.1 --- a/doc-src/HOL/logics-HOL.tex Mon Aug 28 13:50:24 2000 +0200
3.2 +++ b/doc-src/HOL/logics-HOL.tex Mon Aug 28 13:52:38 2000 +0200
3.3 @@ -1,6 +1,6 @@
3.4 %% $Id$
3.5 \documentclass[12pt,a4paper]{report}
3.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
3.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
3.8
3.9 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
3.10 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
4.1 --- a/doc-src/Inductive/Makefile Mon Aug 28 13:50:24 2000 +0200
4.2 +++ b/doc-src/Inductive/Makefile Mon Aug 28 13:52:38 2000 +0200
4.3 @@ -12,7 +12,7 @@
4.4 include ../Makefile.in
4.5
4.6 NAME = ind-defs
4.7 -FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty ../manual.bib
4.8 +FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
4.9
4.10 dvi: $(NAME).dvi
4.11
5.1 --- a/doc-src/Inductive/ind-defs.tex Mon Aug 28 13:50:24 2000 +0200
5.2 +++ b/doc-src/Inductive/ind-defs.tex Mon Aug 28 13:52:38 2000 +0200
5.3 @@ -1,6 +1,6 @@
5.4 %% $Id$
5.5 \documentclass[12pt,a4paper]{article}
5.6 -\usepackage{latexsym,../iman,../extra,../proof,../pdfsetup}
5.7 +\usepackage{latexsym,../iman,../extra,../ttbox,../proof,../pdfsetup}
5.8
5.9 \newif\ifshort%''Short'' means a published version, not the documentation
5.10 \shortfalse%%%%%\shorttrue
6.1 --- a/doc-src/Intro/Makefile Mon Aug 28 13:50:24 2000 +0200
6.2 +++ b/doc-src/Intro/Makefile Mon Aug 28 13:52:38 2000 +0200
6.3 @@ -13,7 +13,7 @@
6.4
6.5 NAME = intro
6.6 FILES = intro.tex foundations.tex getting.tex advanced.tex \
6.7 - ../proof.sty ../iman.sty ../extra.sty ../manual.bib
6.8 + ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
6.9
6.10 dvi: $(NAME).dvi
6.11
7.1 --- a/doc-src/Intro/advanced.tex Mon Aug 28 13:50:24 2000 +0200
7.2 +++ b/doc-src/Intro/advanced.tex Mon Aug 28 13:52:38 2000 +0200
7.3 @@ -293,7 +293,7 @@
7.4 \iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
7.5 Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that
7.6 object-logics may add further theory sections, for example
7.7 -\texttt{typedef}, \texttt{datatype} in \HOL.
7.8 +\texttt{typedef}, \texttt{datatype} in HOL.
7.9
7.10 All the declaration parts can be omitted or repeated and may appear in
7.11 any order, except that the {\ML} section must be last (after the {\tt
7.12 @@ -302,7 +302,7 @@
7.13 theories, inheriting their types, constants, syntax, etc. The theory
7.14 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
7.15 \thydx{CPure} offers the more usual higher-order function application
7.16 -syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure.
7.17 +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
7.18
7.19 Each theory definition must reside in a separate file, whose name is
7.20 the theory's with {\tt.thy} appended. Calling
7.21 @@ -964,12 +964,11 @@
7.22
7.23 \index{simplification}\index{examples!of simplification}
7.24
7.25 -Isabelle's simplification tactics repeatedly apply equations to a
7.26 -subgoal, perhaps proving it. For efficiency, the rewrite rules must
7.27 -be packaged into a {\bf simplification set},\index{simplification
7.28 - sets} or {\bf simpset}. We augment the implicit simpset of {\FOL}
7.29 -with the equations proved in the previous section, namely $0+n=n$ and
7.30 -$\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
7.31 +Isabelle's simplification tactics repeatedly apply equations to a subgoal,
7.32 +perhaps proving it. For efficiency, the rewrite rules must be packaged into a
7.33 +{\bf simplification set},\index{simplification sets} or {\bf simpset}. We
7.34 +augment the implicit simpset of FOL with the equations proved in the previous
7.35 +section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
7.36 \begin{ttbox}
7.37 Addsimps [add_0, add_Suc];
7.38 \end{ttbox}
8.1 --- a/doc-src/Intro/foundations.tex Mon Aug 28 13:50:24 2000 +0200
8.2 +++ b/doc-src/Intro/foundations.tex Mon Aug 28 13:52:38 2000 +0200
8.3 @@ -441,20 +441,18 @@
8.4 Under similar conditions, a signature can be extended. Signatures are
8.5 managed internally by Isabelle; users seldom encounter them.
8.6
8.7 -\index{theories|bold} A {\bf theory} consists of a signature plus a
8.8 -collection of axioms. The {\Pure} theory contains only the
8.9 -meta-logic. Theories can be combined provided their signatures are
8.10 -compatible. A theory definition extends an existing theory with
8.11 -further signature specifications --- classes, types, constants and
8.12 -mixfix declarations --- plus lists of axioms and definitions etc.,
8.13 -expressed as strings to be parsed. A theory can formalize a small
8.14 -piece of mathematics, such as lists and their operations, or an entire
8.15 -logic. A mathematical development typically involves many theories in
8.16 -a hierarchy. For example, the {\Pure} theory could be extended to
8.17 -form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two
8.18 -separate ways to form a theory for natural numbers and a theory for
8.19 -lists; the union of these two could be extended into a theory defining
8.20 -the length of a list:
8.21 +\index{theories|bold} A {\bf theory} consists of a signature plus a collection
8.22 +of axioms. The Pure theory contains only the meta-logic. Theories can be
8.23 +combined provided their signatures are compatible. A theory definition
8.24 +extends an existing theory with further signature specifications --- classes,
8.25 +types, constants and mixfix declarations --- plus lists of axioms and
8.26 +definitions etc., expressed as strings to be parsed. A theory can formalize a
8.27 +small piece of mathematics, such as lists and their operations, or an entire
8.28 +logic. A mathematical development typically involves many theories in a
8.29 +hierarchy. For example, the Pure theory could be extended to form a theory
8.30 +for Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form
8.31 +a theory for natural numbers and a theory for lists; the union of these two
8.32 +could be extended into a theory defining the length of a list:
8.33 \begin{tt}
8.34 \[
8.35 \begin{array}{c@{}c@{}c@{}c@{}c}
9.1 --- a/doc-src/Intro/getting.tex Mon Aug 28 13:50:24 2000 +0200
9.2 +++ b/doc-src/Intro/getting.tex Mon Aug 28 13:52:38 2000 +0200
9.3 @@ -26,7 +26,7 @@
9.4 isabelle FOL
9.5 \end{ttbox}
9.6 Note that just typing \texttt{isabelle} usually brings up higher-order logic
9.7 -(\HOL) by default.
9.8 +(HOL) by default.
9.9
9.10
9.11 \subsection{Lexical matters}
9.12 @@ -110,8 +110,8 @@
9.13 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
9.14 \end{array}
9.15 \]
9.16 -Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
9.17 -which differs from that used in \FOL\@.
9.18 +Note that HOL uses its traditional ``higher-order'' syntax for application,
9.19 +which differs from that used in FOL.
9.20
9.21 The theorems and rules of an object-logic are represented by theorems in
9.22 the meta-logic, which are expressed using meta-formulae. Since the
9.23 @@ -228,10 +228,10 @@
9.24 to have subscript zero, improving readability and reducing subscript
9.25 growth.
9.26 \end{ttdescription}
9.27 -The rules of a theory are normally bound to \ML\ identifiers. Suppose we
9.28 -are running an Isabelle session containing theory~\FOL, natural deduction
9.29 -first-order logic.\footnote{For a listing of the \FOL{} rules and their
9.30 - \ML{} names, turn to
9.31 +The rules of a theory are normally bound to \ML\ identifiers. Suppose we are
9.32 +running an Isabelle session containing theory~FOL, natural deduction
9.33 +first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
9.34 + names, turn to
9.35 \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
9.36 {page~\pageref{fol-rules}}.}
9.37 Let us try an example given in~\S\ref{joining}. We
10.1 --- a/doc-src/Intro/intro.tex Mon Aug 28 13:50:24 2000 +0200
10.2 +++ b/doc-src/Intro/intro.tex Mon Aug 28 13:52:38 2000 +0200
10.3 @@ -1,5 +1,5 @@
10.4 \documentclass[12pt,a4paper]{article}
10.5 -\usepackage{graphicx,../iman,../extra,../proof,../pdfsetup}
10.6 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}
10.7
10.8 %% $Id$
10.9 %% run bibtex intro to prepare bibliography
11.1 --- a/doc-src/IsarRef/Makefile Mon Aug 28 13:50:24 2000 +0200
11.2 +++ b/doc-src/IsarRef/Makefile Mon Aug 28 13:52:38 2000 +0200
11.3 @@ -15,7 +15,8 @@
11.4
11.5 FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \
11.6 generic.tex hol.tex refcard.tex conversion.tex ../isar.sty \
11.7 - ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
11.8 + ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty \
11.9 + ../extra.sty ../ttbox.sty ../manual.bib
11.10
11.11 dvi: $(NAME).dvi
11.12
12.1 --- a/doc-src/IsarRef/hol.tex Mon Aug 28 13:50:24 2000 +0200
12.2 +++ b/doc-src/IsarRef/hol.tex Mon Aug 28 13:52:38 2000 +0200
12.3 @@ -231,11 +231,11 @@
12.4 The rule is determined as follows, according to the facts and arguments
12.5 passed to the $cases$ method:
12.6 \begin{matharray}{llll}
12.7 - \text{facts} & & \text{arguments} & \text{rule} \\\hline
12.8 - & cases & & \text{classical case split} \\
12.9 - & cases & t & \text{datatype exhaustion (type of $t$)} \\
12.10 - \edrv a \in A & cases & \dots & \text{inductive set elimination (of $A$)} \\
12.11 - \dots & cases & \dots ~ R & \text{explicit rule $R$} \\
12.12 + \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
12.13 + & cases & & \Text{classical case split} \\
12.14 + & cases & t & \Text{datatype exhaustion (type of $t$)} \\
12.15 + \edrv a \in A & cases & \dots & \Text{inductive set elimination (of $A$)} \\
12.16 + \dots & cases & \dots ~ R & \Text{explicit rule $R$} \\
12.17 \end{matharray}
12.18
12.19 Several instantiations may be given, referring to the \emph{suffix} of
12.20 @@ -257,10 +257,10 @@
12.21 \item [$induct~insts~R$] is analogous to the $cases$ method, but refers to
12.22 induction rules, which are determined as follows:
12.23 \begin{matharray}{llll}
12.24 - \text{facts} & & \text{arguments} & \text{rule} \\\hline
12.25 - & induct & P ~ x ~ \dots & \text{datatype induction (type of $x$)} \\
12.26 - \edrv x \in A & induct & \dots & \text{set induction (of $A$)} \\
12.27 - \dots & induct & \dots ~ R & \text{explicit rule $R$} \\
12.28 + \Text{facts} & & \Text{arguments} & \Text{rule} \\\hline
12.29 + & induct & P ~ x ~ \dots & \Text{datatype induction (type of $x$)} \\
12.30 + \edrv x \in A & induct & \dots & \Text{set induction (of $A$)} \\
12.31 + \dots & induct & \dots ~ R & \Text{explicit rule $R$} \\
12.32 \end{matharray}
12.33
12.34 Several instantiations may be given, each referring to some part of a mutual
13.1 --- a/doc-src/IsarRef/isar-ref.tex Mon Aug 28 13:50:24 2000 +0200
13.2 +++ b/doc-src/IsarRef/isar-ref.tex Mon Aug 28 13:52:38 2000 +0200
13.3 @@ -9,7 +9,7 @@
13.4
13.5
13.6 \documentclass[12pt,a4paper,fleqn]{report}
13.7 -\usepackage{latexsym,graphicx,../iman,../extra,../proof,../rail,../railsetup,../isar,../pdfsetup}
13.8 +\usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
13.9
13.10 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
13.11 \author{\emph{Markus Wenzel} \\ TU M\"unchen}
14.1 --- a/doc-src/IsarRef/pure.tex Mon Aug 28 13:50:24 2000 +0200
14.2 +++ b/doc-src/IsarRef/pure.tex Mon Aug 28 13:52:38 2000 +0200
14.3 @@ -687,7 +687,7 @@
14.4 Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
14.5 multiple facts to be given in their proper order, corresponding to a prefix of
14.6 the premises of the rule involved. Note that positions may be easily skipped
14.7 -using something like $\FROM{\text{\texttt{_}}~a~b}$, for example. This
14.8 +using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This
14.9 involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
14.10 bound in Isabelle/Pure as ``\texttt{_}''
14.11 (underscore).\indexisarthm{_@\texttt{_}}
15.1 --- a/doc-src/IsarRef/refcard.tex Mon Aug 28 13:50:24 2000 +0200
15.2 +++ b/doc-src/IsarRef/refcard.tex Mon Aug 28 13:52:38 2000 +0200
15.3 @@ -15,7 +15,7 @@
15.4 $\BG~\dots~\EN$ & declare explicit blocks \\
15.5 $\NEXT$ & switch implicit blocks \\
15.6 $\NOTE{a}{\vec b}$ & reconsider facts \\
15.7 - $\LET{p = t}$ & \text{abbreviate terms by higher-order matching} \\
15.8 + $\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
15.9 \end{tabular}
15.10
15.11 \begin{matharray}{rcl}
15.12 @@ -61,13 +61,13 @@
15.13 \MOREOVER & \approx & \NOTE{calculation}{calculation~this} \\
15.14 \ULTIMATELY & \approx & \MOREOVER~\FROM{calculation} \\[0.5ex]
15.15 \PRESUME{a}{\vec\phi} & \approx & \ASSUME{a}{\vec\phi} \\
15.16 -% & & \text{(permissive assumption)} \\
15.17 +% & & \Text{(permissive assumption)} \\
15.18 \DEF{a}{x \equiv t} & \approx & \FIX{x}~\ASSUME{a}{x \equiv t} \\
15.19 -% & & \text{(definitional assumption)} \\
15.20 +% & & \Text{(definitional assumption)} \\
15.21 \OBTAIN{\vec x}{a}{\vec\phi} & \approx & \dots~\FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
15.22 -% & & \text{(generalized existence)} \\
15.23 +% & & \Text{(generalized existence)} \\
15.24 \CASE{c} & \approx & \FIX{\vec x}~\ASSUME{c}{\vec\phi} \\
15.25 -% & & \text{(named context)} \\[0.5ex]
15.26 +% & & \Text{(named context)} \\[0.5ex]
15.27 \SORRY & \approx & \BY{cheating} \\
15.28 \end{matharray}
15.29
15.30 @@ -75,11 +75,11 @@
15.31 \subsection{Diagnostic commands}
15.32
15.33 \begin{matharray}{ll}
15.34 - \isarkeyword{pr} & \text{print current state} \\
15.35 - \isarkeyword{thm}~\vec a & \text{print theorems} \\
15.36 - \isarkeyword{term}~t & \text{print term} \\
15.37 - \isarkeyword{prop}~\phi & \text{print meta-level proposition} \\
15.38 - \isarkeyword{typ}~\tau & \text{print meta-level type} \\
15.39 + \isarkeyword{pr} & \Text{print current state} \\
15.40 + \isarkeyword{thm}~\vec a & \Text{print theorems} \\
15.41 + \isarkeyword{term}~t & \Text{print term} \\
15.42 + \isarkeyword{prop}~\phi & \Text{print meta-level proposition} \\
15.43 + \isarkeyword{typ}~\tau & \Text{print meta-level type} \\
15.44 \end{matharray}
15.45
15.46
15.47 @@ -96,11 +96,11 @@
15.48 $induct~\vec x$ & proof by induction (provides cases) \\[2ex]
15.49
15.50 \multicolumn{2}{l}{\textbf{Repeated steps (inserting facts)}} \\[0.5ex]
15.51 - $-$ & \text{no rules} \\
15.52 - $intro~\vec a$ & \text{introduction rules} \\
15.53 - $intro_classes$ & \text{class introduction rules} \\
15.54 - $elim~\vec a$ & \text{elimination rules} \\
15.55 - $unfold~\vec a$ & \text{definitions} \\[2ex]
15.56 + $-$ & \Text{no rules} \\
15.57 + $intro~\vec a$ & \Text{introduction rules} \\
15.58 + $intro_classes$ & \Text{class introduction rules} \\
15.59 + $elim~\vec a$ & \Text{elimination rules} \\
15.60 + $unfold~\vec a$ & \Text{definitions} \\[2ex]
15.61
15.62 \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
15.63 $simp$, $simp_all$ & Simplifier (+ Splitter) \\
16.1 --- a/doc-src/Logics/CTT.tex Mon Aug 28 13:50:24 2000 +0200
16.2 +++ b/doc-src/Logics/CTT.tex Mon Aug 28 13:52:38 2000 +0200
16.3 @@ -40,16 +40,16 @@
16.4 Assumptions can use all the judgement forms, for instance to express that
16.5 $B$ is a family of types over~$A$:
16.6 \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
16.7 -To justify the {\CTT} formulation it is probably best to appeal directly
16.8 -to the semantic explanations of the rules~\cite{martinlof84}, rather than
16.9 -to the rules themselves. The order of assumptions no longer matters,
16.10 -unlike in standard Type Theory. Contexts, which are typical of many modern
16.11 -type theories, are difficult to represent in Isabelle. In particular, it
16.12 -is difficult to enforce that all the variables in a context are distinct.
16.13 -\index{assumptions!in {\CTT}}
16.14 +To justify the CTT formulation it is probably best to appeal directly to the
16.15 +semantic explanations of the rules~\cite{martinlof84}, rather than to the
16.16 +rules themselves. The order of assumptions no longer matters, unlike in
16.17 +standard Type Theory. Contexts, which are typical of many modern type
16.18 +theories, are difficult to represent in Isabelle. In particular, it is
16.19 +difficult to enforce that all the variables in a context are distinct.
16.20 +\index{assumptions!in CTT}
16.21
16.22 -The theory does not use polymorphism. Terms in {\CTT} have type~\tydx{i}, the
16.23 -type of individuals. Types in {\CTT} have type~\tydx{t}.
16.24 +The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the
16.25 +type of individuals. Types in CTT have type~\tydx{t}.
16.26
16.27 \begin{figure} \tabcolsep=1em %wider spacing in tables
16.28 \begin{center}
16.29 @@ -81,29 +81,29 @@
16.30 \cdx{tt} & $i$ & constructor
16.31 \end{tabular}
16.32 \end{center}
16.33 -\caption{The constants of {\CTT}} \label{ctt-constants}
16.34 +\caption{The constants of CTT} \label{ctt-constants}
16.35 \end{figure}
16.36
16.37
16.38 -{\CTT} supports all of Type Theory apart from list types, well-ordering
16.39 -types, and universes. Universes could be introduced {\em\`a la Tarski},
16.40 -adding new constants as names for types. The formulation {\em\`a la
16.41 - Russell}, where types denote themselves, is only possible if we identify
16.42 -the meta-types~{\tt i} and~{\tt t}. Most published formulations of
16.43 -well-ordering types have difficulties involving extensionality of
16.44 -functions; I suggest that you use some other method for defining recursive
16.45 -types. List types are easy to introduce by declaring new rules.
16.46 +CTT supports all of Type Theory apart from list types, well-ordering types,
16.47 +and universes. Universes could be introduced {\em\`a la Tarski}, adding new
16.48 +constants as names for types. The formulation {\em\`a la Russell}, where
16.49 +types denote themselves, is only possible if we identify the meta-types~{\tt
16.50 + i} and~{\tt t}. Most published formulations of well-ordering types have
16.51 +difficulties involving extensionality of functions; I suggest that you use
16.52 +some other method for defining recursive types. List types are easy to
16.53 +introduce by declaring new rules.
16.54
16.55 -{\CTT} uses the 1982 version of Type Theory, with extensional equality.
16.56 -The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are
16.57 -interchangeable. Its rewriting tactics prove theorems of the form $a=b\in
16.58 -A$. It could be modified to have intensional equality, but rewriting
16.59 -tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the
16.60 -computation rules might require a separate simplifier.
16.61 +CTT uses the 1982 version of Type Theory, with extensional equality. The
16.62 +computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
16.63 +Its rewriting tactics prove theorems of the form $a=b\in A$. It could be
16.64 +modified to have intensional equality, but rewriting tactics would have to
16.65 +prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
16.66 +require a separate simplifier.
16.67
16.68
16.69 \begin{figure} \tabcolsep=1em %wider spacing in tables
16.70 -\index{lambda abs@$\lambda$-abstractions!in \CTT}
16.71 +\index{lambda abs@$\lambda$-abstractions!in CTT}
16.72 \begin{center}
16.73 \begin{tabular}{llrrr}
16.74 \it symbol &\it name &\it meta-type & \it priority & \it description \\
16.75 @@ -113,7 +113,7 @@
16.76 \subcaption{Binders}
16.77
16.78 \begin{center}
16.79 -\index{*"` symbol}\index{function applications!in \CTT}
16.80 +\index{*"` symbol}\index{function applications!in CTT}
16.81 \index{*"+ symbol}
16.82 \begin{tabular}{rrrr}
16.83 \it symbol & \it meta-type & \it priority & \it description \\
16.84 @@ -160,7 +160,7 @@
16.85 \]
16.86 \end{center}
16.87 \subcaption{Grammar}
16.88 -\caption{Syntax of {\CTT}} \label{ctt-syntax}
16.89 +\caption{Syntax of CTT} \label{ctt-syntax}
16.90 \end{figure}
16.91
16.92 %%%%\section{Generic Packages} typedsimp.ML????????????????
16.93 @@ -168,16 +168,16 @@
16.94
16.95 \section{Syntax}
16.96 The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include
16.97 -the function application operator (sometimes called `apply'), and the
16.98 -2-place type operators. Note that meta-level abstraction and application,
16.99 -$\lambda x.b$ and $f(a)$, differ from object-level abstraction and
16.100 -application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT}
16.101 -function~$f$ is simply an individual as far as Isabelle is concerned: its
16.102 -Isabelle type is~$i$, not say $i\To i$.
16.103 +the function application operator (sometimes called `apply'), and the 2-place
16.104 +type operators. Note that meta-level abstraction and application, $\lambda
16.105 +x.b$ and $f(a)$, differ from object-level abstraction and application,
16.106 +\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
16.107 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
16.108 +$i\To i$.
16.109
16.110 -The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of
16.111 -Nordstr\"om et al.~\cite{nordstrom90}. The empty type is called $F$ and
16.112 -the one-element type is $T$; other finite types are built as $T+T+T$, etc.
16.113 +The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
16.114 +et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
16.115 +type is $T$; other finite types are built as $T+T+T$, etc.
16.116
16.117 \index{*SUM symbol}\index{*PROD symbol}
16.118 Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
16.119 @@ -387,7 +387,7 @@
16.120 |] ==> snd(p) : B(fst(p))
16.121 \end{ttbox}
16.122
16.123 -\caption{Derived rules for {\CTT}} \label{ctt-derived}
16.124 +\caption{Derived rules for CTT} \label{ctt-derived}
16.125 \end{figure}
16.126
16.127
16.128 @@ -470,7 +470,7 @@
16.129 \section{Rule lists}
16.130 The Type Theory tactics provide rewriting, type inference, and logical
16.131 reasoning. Many proof procedures work by repeatedly resolving certain Type
16.132 -Theory rules against a proof state. {\CTT} defines lists --- each with
16.133 +Theory rules against a proof state. CTT defines lists --- each with
16.134 type
16.135 \hbox{\tt thm list} --- of related rules.
16.136 \begin{ttdescription}
16.137 @@ -514,14 +514,14 @@
16.138 equal_tac : thm list -> tactic
16.139 intr_tac : thm list -> tactic
16.140 \end{ttbox}
16.141 -Blind application of {\CTT} rules seldom leads to a proof. The elimination
16.142 +Blind application of CTT rules seldom leads to a proof. The elimination
16.143 rules, especially, create subgoals containing new unknowns. These subgoals
16.144 unify with anything, creating a huge search space. The standard tactic
16.145 -\ttindex{filt_resolve_tac}
16.146 +\ttindex{filt_resolve_tac}
16.147 (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
16.148 {\S\ref{filt_resolve_tac}})
16.149 %
16.150 -fails for goals that are too flexible; so does the {\CTT} tactic {\tt
16.151 +fails for goals that are too flexible; so does the CTT tactic {\tt
16.152 test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
16.153 achieve a simple kind of subgoal reordering: the less flexible subgoals are
16.154 attempted first. Do some single step proofs, or study the examples below,
16.155 @@ -563,8 +563,8 @@
16.156 CTT} equality rules and the built-in rewriting functor
16.157 {\tt TSimpFun}.%
16.158 \footnote{This should not be confused with Isabelle's main simplifier; {\tt
16.159 - TSimpFun} is only useful for {\CTT} and similar logics with type
16.160 - inference rules. At present it is undocumented.}
16.161 + TSimpFun} is only useful for CTT and similar logics with type inference
16.162 + rules. At present it is undocumented.}
16.163 %
16.164 The rewrites include the computation rules and other equations. The long
16.165 versions of the other rules permit rewriting of subterms and subtypes.
16.166 @@ -583,11 +583,11 @@
16.167
16.168
16.169 \section{Tactics for logical reasoning}
16.170 -Interpreting propositions as types lets {\CTT} express statements of
16.171 -intuitionistic logic. However, Constructive Type Theory is not just
16.172 -another syntax for first-order logic. There are fundamental differences.
16.173 +Interpreting propositions as types lets CTT express statements of
16.174 +intuitionistic logic. However, Constructive Type Theory is not just another
16.175 +syntax for first-order logic. There are fundamental differences.
16.176
16.177 -\index{assumptions!in {\CTT}}
16.178 +\index{assumptions!in CTT}
16.179 Can assumptions be deleted after use? Not every occurrence of a type
16.180 represents a proposition, and Type Theory assumptions declare variables.
16.181 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
16.182 @@ -598,7 +598,7 @@
16.183 refer to $z$ may render the subgoal unprovable: arguably,
16.184 meaningless.
16.185
16.186 -Isabelle provides several tactics for predicate calculus reasoning in \CTT:
16.187 +Isabelle provides several tactics for predicate calculus reasoning in CTT:
16.188 \begin{ttbox}
16.189 mp_tac : int -> tactic
16.190 add_mp_tac : int -> tactic
16.191 @@ -728,7 +728,7 @@
16.192
16.193
16.194 \section{The examples directory}
16.195 -This directory contains examples and experimental proofs in {\CTT}.
16.196 +This directory contains examples and experimental proofs in CTT.
16.197 \begin{ttdescription}
16.198 \item[CTT/ex/typechk.ML]
16.199 contains simple examples of type-checking and type deduction.
17.1 --- a/doc-src/Logics/LK.tex Mon Aug 28 13:50:24 2000 +0200
17.2 +++ b/doc-src/Logics/LK.tex Mon Aug 28 13:52:38 2000 +0200
17.3 @@ -18,8 +18,8 @@
17.4 are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
17.5 belongs to class {\tt logic}.
17.6
17.7 -\LK{} implements a classical logic theorem prover that is nearly as powerful
17.8 -as the generic classical reasoner. The simplifier is now available too.
17.9 +LK implements a classical logic theorem prover that is nearly as powerful as
17.10 +the generic classical reasoner. The simplifier is now available too.
17.11
17.12 To work in LK, start up Isabelle specifying \texttt{Sequents} as the
17.13 object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:
17.14 @@ -179,17 +179,17 @@
17.15 of formulae.
17.16
17.17 The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
17.18 -satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{}
17.19 -denote something, a description is always meaningful, but we do not know
17.20 -its value unless $P[x]$ defines it uniquely. The Isabelle notation is
17.21 -\hbox{\tt THE $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules})
17.22 -does not entail the Axiom of Choice because it requires uniqueness.
17.23 +satisfying~$P[a]$, if one exists and is unique. Since all terms in LK denote
17.24 +something, a description is always meaningful, but we do not know its value
17.25 +unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE
17.26 + $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not
17.27 +entail the Axiom of Choice because it requires uniqueness.
17.28
17.29 Conditional expressions are available with the notation
17.30 \[ \dquotes
17.31 "if"~formula~"then"~term~"else"~term. \]
17.32
17.33 -Figure~\ref{lk-grammar} presents the grammar of \LK. Traditionally,
17.34 +Figure~\ref{lk-grammar} presents the grammar of LK. Traditionally,
17.35 \(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's
17.36 notation, the prefix~\verb|$| on a term makes it range over sequences.
17.37 In a sequent, anything not prefixed by \verb|$| is taken as a formula.
17.38 @@ -272,13 +272,13 @@
17.39
17.40 \section{Automatic Proof}
17.41
17.42 -\LK{} instantiates Isabelle's simplifier. Both equality ($=$) and the
17.43 +LK instantiates Isabelle's simplifier. Both equality ($=$) and the
17.44 biconditional ($\bimp$) may be used for rewriting. The tactic
17.45 \texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With
17.46 sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
17.47 -required; all the formulae{} in the sequent will be simplified. The
17.48 -left-hand formulae{} are taken as rewrite rules. (Thus, the behaviour is what
17.49 -you would normally expect from calling \texttt{Asm_full_simp_tac}.)
17.50 +required; all the formulae{} in the sequent will be simplified. The left-hand
17.51 +formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would
17.52 +normally expect from calling \texttt{Asm_full_simp_tac}.)
17.53
17.54 For classical reasoning, several tactics are available:
17.55 \begin{ttbox}
17.56 @@ -325,15 +325,13 @@
17.57 These tactics refine a subgoal into two by applying the cut rule. The cut
17.58 formula is given as a string, and replaces some other formula in the sequent.
17.59 \begin{ttdescription}
17.60 -\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}]
17.61 -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It
17.62 -then deletes some formula from the right side of subgoal~$i$, replacing
17.63 -that formula by~$P$.
17.64 -
17.65 -\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}]
17.66 -reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It
17.67 -then deletes some formula from the left side of the new subgoal $i+1$,
17.68 -replacing that formula by~$P$.
17.69 +\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
17.70 + applies the cut rule to subgoal~$i$. It then deletes some formula from the
17.71 + right side of subgoal~$i$, replacing that formula by~$P$.
17.72 +
17.73 +\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
17.74 + applies the cut rule to subgoal~$i$. It then deletes some formula from the
17.75 + left side of the new subgoal $i+1$, replacing that formula by~$P$.
17.76 \end{ttdescription}
17.77 All the structural rules --- cut, contraction, and thinning --- can be
17.78 applied to particular formulae using {\tt res_inst_tac}.
17.79 @@ -378,11 +376,11 @@
17.80
17.81 \section{A simple example of classical reasoning}
17.82 The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
17.83 -classical treatment of the existential quantifier. Classical reasoning
17.84 -is easy using~{\LK}, as you can see by comparing this proof with the one
17.85 -given in the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the
17.86 -proofs are essentially the same; the key step here is to use \tdx{exR}
17.87 -rather than the weaker~\tdx{exR_thin}.
17.88 +classical treatment of the existential quantifier. Classical reasoning is
17.89 +easy using~LK, as you can see by comparing this proof with the one given in
17.90 +the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs
17.91 +are essentially the same; the key step here is to use \tdx{exR} rather than
17.92 +the weaker~\tdx{exR_thin}.
17.93 \begin{ttbox}
17.94 Goal "|- EX y. ALL x. P(y)-->P(x)";
17.95 {\out Level 0}
17.96 @@ -405,10 +403,10 @@
17.97 {\out |- EX y. ALL x. P(y) --> P(x)}
17.98 {\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
17.99 \end{ttbox}
17.100 -Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
17.101 -become an assumption; instead, it moves to the left side. The
17.102 -resulting subgoal cannot be instantiated to a basic sequent: the bound
17.103 -variable~$x$ is not unifiable with the unknown~$\Var{x}$.
17.104 +Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
17.105 +assumption; instead, it moves to the left side. The resulting subgoal cannot
17.106 +be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
17.107 +with the unknown~$\Var{x}$.
17.108 \begin{ttbox}
17.109 by (resolve_tac [basic] 1);
17.110 {\out by: tactic failed}
17.111 @@ -548,10 +546,10 @@
17.112 Multiple unifiers occur whenever this is resolved against a goal containing
17.113 more than one conjunction on the left.
17.114
17.115 -\LK{} exploits this representation of lists. As an alternative, the
17.116 -sequent calculus can be formalized using an ordinary representation of
17.117 -lists, with a logic program for removing a formula from a list. Amy Felty
17.118 -has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
17.119 +LK exploits this representation of lists. As an alternative, the sequent
17.120 +calculus can be formalized using an ordinary representation of lists, with a
17.121 +logic program for removing a formula from a list. Amy Felty has applied this
17.122 +technique using the language $\lambda$Prolog~\cite{felty91a}.
17.123
17.124 Explicit formalization of sequents can be tiresome. But it gives precise
17.125 control over contraction and weakening, and is essential to handle relevant
17.126 @@ -575,10 +573,10 @@
17.127 rules require a search strategy, such as backtracking.
17.128
17.129 A \textbf{pack} is a pair whose first component is a list of safe rules and
17.130 -whose second is a list of unsafe rules. Packs can be extended in an
17.131 -obvious way to allow reasoning with various collections of rules. For
17.132 -clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is
17.133 -essentially a type synonym:
17.134 +whose second is a list of unsafe rules. Packs can be extended in an obvious
17.135 +way to allow reasoning with various collections of rules. For clarity, LK
17.136 +declares \mltydx{pack} as an \ML{} datatype, although is essentially a type
17.137 +synonym:
17.138 \begin{ttbox}
17.139 datatype pack = Pack of thm list * thm list;
17.140 \end{ttbox}
17.141 @@ -628,8 +626,7 @@
17.142
17.143 \section{*Proof procedures}\label{sec:sequent-provers}
17.144
17.145 -The \LK{} proof procedure is similar to the classical reasoner
17.146 -described in
17.147 +The LK proof procedure is similar to the classical reasoner described in
17.148 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
17.149 {Chap.\ts\ref{chap:classical}}.
17.150 %
18.1 --- a/doc-src/Logics/Makefile Mon Aug 28 13:50:24 2000 +0200
18.2 +++ b/doc-src/Logics/Makefile Mon Aug 28 13:52:38 2000 +0200
18.3 @@ -13,7 +13,7 @@
18.4
18.5 NAME = logics
18.6 FILES = logics.tex preface.tex syntax.tex LK.tex Sequents.tex CTT.tex \
18.7 - ../proof.sty ../iman.sty ../extra.sty ../manual.bib
18.8 + ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
18.9
18.10 dvi: $(NAME).dvi
18.11
19.1 --- a/doc-src/Logics/Old_HOL.tex Mon Aug 28 13:50:24 2000 +0200
19.2 +++ b/doc-src/Logics/Old_HOL.tex Mon Aug 28 13:52:38 2000 +0200
19.3 @@ -3,33 +3,32 @@
19.4 \index{higher-order logic|(}
19.5 \index{HOL system@{\sc hol} system}
19.6
19.7 -The theory~\thydx{HOL} implements higher-order logic.
19.8 -It is based on Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is
19.9 -based on Church's original paper~\cite{church40}. Andrews's
19.10 -book~\cite{andrews86} is a full description of higher-order logic.
19.11 -Experience with the {\sc hol} system has demonstrated that higher-order
19.12 -logic is useful for hardware verification; beyond this, it is widely
19.13 -applicable in many areas of mathematics. It is weaker than {\ZF} set
19.14 -theory but for most applications this does not matter. If you prefer {\ML}
19.15 -to Lisp, you will probably prefer \HOL\ to~{\ZF}.
19.16 +The theory~\thydx{HOL} implements higher-order logic. It is based on
19.17 +Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
19.18 +Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a
19.19 +full description of higher-order logic. Experience with the {\sc hol} system
19.20 +has demonstrated that higher-order logic is useful for hardware verification;
19.21 +beyond this, it is widely applicable in many areas of mathematics. It is
19.22 +weaker than ZF set theory but for most applications this does not matter. If
19.23 +you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.
19.24
19.25 -Previous releases of Isabelle included a different version of~\HOL, with
19.26 +Previous releases of Isabelle included a different version of~HOL, with
19.27 explicit type inference rules~\cite{paulson-COLOG}. This version no longer
19.28 exists, but \thydx{ZF} supports a similar style of reasoning.
19.29
19.30 -\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
19.31 -identifies object-level types with meta-level types, taking advantage of
19.32 -Isabelle's built-in type checker. It identifies object-level functions
19.33 -with meta-level functions, so it uses Isabelle's operations for abstraction
19.34 -and application. There is no `apply' operator: function applications are
19.35 -written as simply~$f(a)$ rather than $f{\tt`}a$.
19.36 +HOL has a distinct feel, compared with ZF and CTT. It identifies object-level
19.37 +types with meta-level types, taking advantage of Isabelle's built-in type
19.38 +checker. It identifies object-level functions with meta-level functions, so
19.39 +it uses Isabelle's operations for abstraction and application. There is no
19.40 +`apply' operator: function applications are written as simply~$f(a)$ rather
19.41 +than $f{\tt`}a$.
19.42
19.43 -These identifications allow Isabelle to support \HOL\ particularly nicely,
19.44 -but they also mean that \HOL\ requires more sophistication from the user
19.45 ---- in particular, an understanding of Isabelle's type system. Beginners
19.46 -should work with {\tt show_types} set to {\tt true}. Gain experience by
19.47 -working in first-order logic before attempting to use higher-order logic.
19.48 -This chapter assumes familiarity with~{\FOL{}}.
19.49 +These identifications allow Isabelle to support HOL particularly nicely, but
19.50 +they also mean that HOL requires more sophistication from the user --- in
19.51 +particular, an understanding of Isabelle's type system. Beginners should work
19.52 +with {\tt show_types} set to {\tt true}. Gain experience by working in
19.53 +first-order logic before attempting to use higher-order logic. This chapter
19.54 +assumes familiarity with~FOL.
19.55
19.56
19.57 \begin{figure}
19.58 @@ -115,7 +114,7 @@
19.59 & | & "EX!~" id~id^* " . " formula
19.60 \end{array}
19.61 \]
19.62 -\caption{Full grammar for \HOL} \label{hol-grammar}
19.63 +\caption{Full grammar for HOL} \label{hol-grammar}
19.64 \end{figure}
19.65
19.66
19.67 @@ -140,7 +139,7 @@
19.68 $\neg(a=b)$.
19.69
19.70 \begin{warn}
19.71 - \HOL\ has no if-and-only-if connective; logical equivalence is expressed
19.72 + HOL has no if-and-only-if connective; logical equivalence is expressed
19.73 using equality. But equality has a high priority, as befitting a
19.74 relation, while if-and-only-if typically has the lowest priority. Thus,
19.75 $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
19.76 @@ -155,7 +154,7 @@
19.77 belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
19.78 over functions.
19.79
19.80 -Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
19.81 +Types in HOL must be non-empty; otherwise the quantifier rules would be
19.82 unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
19.83
19.84 \index{type definitions}
19.85 @@ -178,11 +177,10 @@
19.86
19.87 \subsection{Binders}
19.88 Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
19.89 -satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
19.90 -something, a description is always meaningful, but we do not know its value
19.91 -unless $P[x]$ defines it uniquely. We may write descriptions as
19.92 -\cdx{Eps}($P$) or use the syntax
19.93 -\hbox{\tt \at $x$.$P[x]$}.
19.94 +satisfying~$P[a]$, if such exists. Since all terms in HOL denote something, a
19.95 +description is always meaningful, but we do not know its value unless $P[x]$
19.96 +defines it uniquely. We may write descriptions as \cdx{Eps}($P$) or use the
19.97 +syntax \hbox{\tt \at $x$.$P[x]$}.
19.98
19.99 Existential quantification is defined by
19.100 \[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]
19.101 @@ -193,14 +191,14 @@
19.102 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
19.103
19.104 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
19.105 -Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
19.106 +Quantifiers have two notations. As in Gordon's {\sc hol} system, HOL
19.107 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
19.108 existential quantifier must be followed by a space; thus {\tt?x} is an
19.109 unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
19.110 -notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
19.111 -available. Both notations are accepted for input. The {\ML} reference
19.112 +notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available. Both
19.113 +notations are accepted for input. The {\ML} reference
19.114 \ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
19.115 -true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
19.116 + true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
19.117 to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
19.118
19.119 All these binders have priority 10.
19.120 @@ -212,7 +210,7 @@
19.121 the constant~\cdx{Let}. It can be expanded by rewriting with its
19.122 definition, \tdx{Let_def}.
19.123
19.124 -\HOL\ also defines the basic syntax
19.125 +HOL also defines the basic syntax
19.126 \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
19.127 as a uniform means of expressing {\tt case} constructs. Therefore {\tt
19.128 case} and \sdx{of} are reserved words. However, so far this is mere
19.129 @@ -259,8 +257,8 @@
19.130
19.131
19.132 \section{Rules of inference}
19.133 -Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
19.134 -their~{\ML} names. Some of the rules deserve additional comments:
19.135 +Figure~\ref{hol-rules} shows the inference rules of~HOL, with their~{\ML}
19.136 +names. Some of the rules deserve additional comments:
19.137 \begin{ttdescription}
19.138 \item[\tdx{ext}] expresses extensionality of functions.
19.139 \item[\tdx{iff}] asserts that logically equivalent formulae are
19.140 @@ -273,14 +271,14 @@
19.141 shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
19.142 \end{ttdescription}
19.143
19.144 -\HOL{} follows standard practice in higher-order logic: only a few
19.145 -connectives are taken as primitive, with the remainder defined obscurely
19.146 +HOL follows standard practice in higher-order logic: only a few connectives
19.147 +are taken as primitive, with the remainder defined obscurely
19.148 (Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
19.149 corresponding definitions \cite[page~270]{mgordon-hol} using
19.150 -object-equality~({\tt=}), which is possible because equality in
19.151 -higher-order logic may equate formulae and even functions over formulae.
19.152 -But theory~\HOL{}, like all other Isabelle theories, uses
19.153 -meta-equality~({\tt==}) for definitions.
19.154 +object-equality~({\tt=}), which is possible because equality in higher-order
19.155 +logic may equate formulae and even functions over formulae. But theory~HOL,
19.156 +like all other Isabelle theories, uses meta-equality~({\tt==}) for
19.157 +definitions.
19.158
19.159 Some of the rules mention type variables; for
19.160 example, {\tt refl} mentions the type variable~{\tt'a}. This allows you to
19.161 @@ -344,7 +342,7 @@
19.162 \subcaption{Logical equivalence}
19.163
19.164 \end{ttbox}
19.165 -\caption{Derived rules for \HOL} \label{hol-lemmas1}
19.166 +\caption{Derived rules for HOL} \label{hol-lemmas1}
19.167 \end{figure}
19.168
19.169
19.170 @@ -521,8 +519,8 @@
19.171 \section{A formulation of set theory}
19.172 Historically, higher-order logic gives a foundation for Russell and
19.173 Whitehead's theory of classes. Let us use modern terminology and call them
19.174 -{\bf sets}, but note that these sets are distinct from those of {\ZF} set
19.175 -theory, and behave more like {\ZF} classes.
19.176 +{\bf sets}, but note that these sets are distinct from those of ZF set theory,
19.177 +and behave more like ZF classes.
19.178 \begin{itemize}
19.179 \item
19.180 Sets are given by predicates over some type~$\sigma$. Types serve to
19.181 @@ -534,20 +532,19 @@
19.182 Although sets may contain other sets as elements, the containing set must
19.183 have a more complex type.
19.184 \end{itemize}
19.185 -Finite unions and intersections have the same behaviour in \HOL\ as they
19.186 -do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
19.187 -denoting the universal set for the given type.
19.188 +Finite unions and intersections have the same behaviour in HOL as they do
19.189 +in~ZF. In HOL the intersection of the empty set is well-defined, denoting the
19.190 +universal set for the given type.
19.191
19.192
19.193 \subsection{Syntax of set theory}\index{*set type}
19.194 -\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
19.195 -essentially the same as $\alpha\To bool$. The new type is defined for
19.196 -clarity and to avoid complications involving function types in unification.
19.197 -Since Isabelle does not support type definitions (as mentioned in
19.198 -\S\ref{HOL-types}), the isomorphisms between the two types are declared
19.199 -explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
19.200 -$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
19.201 -argument order).
19.202 +HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially
19.203 +the same as $\alpha\To bool$. The new type is defined for clarity and to
19.204 +avoid complications involving function types in unification. Since Isabelle
19.205 +does not support type definitions (as mentioned in \S\ref{HOL-types}), the
19.206 +isomorphisms between the two types are declared explicitly. Here they are
19.207 +natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt
19.208 + op :} maps in the other direction (ignoring argument order).
19.209
19.210 Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
19.211 translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
19.212 @@ -563,11 +560,11 @@
19.213 {\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))
19.214 \end{eqnarray*}
19.215
19.216 -The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
19.217 -that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
19.218 -occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
19.219 -x.P[x])$. It defines sets by absolute comprehension, which is impossible
19.220 -in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
19.221 +The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that
19.222 +satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences
19.223 +of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.P[x])$. It defines
19.224 +sets by absolute comprehension, which is impossible in~ZF; the type of~$x$
19.225 +implicitly restricts the comprehension.
19.226
19.227 The set theory defines two {\bf bounded quantifiers}:
19.228 \begin{eqnarray*}
19.229 @@ -811,14 +808,13 @@
19.230
19.231
19.232 Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
19.233 -obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
19.234 -such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
19.235 -are designed for classical reasoning; the rules \tdx{subsetD},
19.236 -\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
19.237 -strictly necessary but yield more natural proofs. Similarly,
19.238 -\tdx{equalityCE} supports classical reasoning about extensionality,
19.239 -after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for
19.240 -proofs pertaining to set theory.
19.241 +obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such
19.242 +as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical
19.243 +reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are
19.244 +not strictly necessary but yield more natural proofs. Similarly,
19.245 +\tdx{equalityCE} supports classical reasoning about extensionality, after the
19.246 +fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining
19.247 +to set theory.
19.248
19.249 Figure~\ref{hol-fun} presents derived inference rules involving functions.
19.250 They also include rules for \cdx{Inv}, which is defined in theory~{\tt
19.251 @@ -905,13 +901,12 @@
19.252
19.253
19.254 \section{Generic packages and classical reasoning}
19.255 -\HOL\ instantiates most of Isabelle's generic packages;
19.256 -see {\tt HOL/ROOT.ML} for details.
19.257 +HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML}
19.258 +for details.
19.259 \begin{itemize}
19.260 -\item
19.261 -Because it includes a general substitution rule, \HOL\ instantiates the
19.262 -tactic {\tt hyp_subst_tac}, which substitutes for an equality
19.263 -throughout a subgoal and its hypotheses.
19.264 +\item Because it includes a general substitution rule, HOL instantiates the
19.265 + tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
19.266 + subgoal and its hypotheses.
19.267 \item
19.268 It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
19.269 simplification set for higher-order logic. Equality~($=$), which also
19.270 @@ -921,14 +916,14 @@
19.271 \item
19.272 It instantiates the classical reasoner, as described below.
19.273 \end{itemize}
19.274 -\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
19.275 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
19.276 -rule; recall Fig.\ts\ref{hol-lemmas2} above.
19.277 +HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
19.278 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
19.279 +Fig.\ts\ref{hol-lemmas2} above.
19.280
19.281 -The classical reasoner is set up as the structure
19.282 -{\tt Classical}. This structure is open, so {\ML} identifiers such
19.283 -as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
19.284 -\HOL\ defines the following classical rule sets:
19.285 +The classical reasoner is set up as the structure {\tt Classical}. This
19.286 +structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt
19.287 + fast_tac}, {\tt best_tac}, etc., refer to it. HOL defines the following
19.288 +classical rule sets:
19.289 \begin{ttbox}
19.290 prop_cs : claset
19.291 HOL_cs : claset
19.292 @@ -1075,13 +1070,12 @@
19.293 called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
19.294 similar constructions in the context of set theory~\cite{paulson-set-II}.
19.295
19.296 -Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
19.297 -overloads $<$ and $\leq$ on the natural numbers. As of this writing,
19.298 -Isabelle provides no means of verifying that such overloading is sensible;
19.299 -there is no means of specifying the operators' properties and verifying
19.300 -that instances of the operators satisfy those properties. To be safe, the
19.301 -\HOL\ theory includes no polymorphic axioms asserting general properties of
19.302 -$<$ and~$\leq$.
19.303 +Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads
19.304 +$<$ and $\leq$ on the natural numbers. As of this writing, Isabelle provides
19.305 +no means of verifying that such overloading is sensible; there is no means of
19.306 +specifying the operators' properties and verifying that instances of the
19.307 +operators satisfy those properties. To be safe, the HOL theory includes no
19.308 +polymorphic axioms asserting general properties of $<$ and~$\leq$.
19.309
19.310 Theory \thydx{Arith} develops arithmetic on the natural numbers. It
19.311 defines addition, multiplication, subtraction, division, and remainder.
19.312 @@ -1190,9 +1184,9 @@
19.313 \subsection{The type constructor for lists, {\tt list}}
19.314 \index{*list type}
19.315
19.316 -\HOL's definition of lists is an example of an experimental method for
19.317 -handling recursive data types. Figure~\ref{hol-list} presents the theory
19.318 -\thydx{List}: the basic list operations with their types and properties.
19.319 +HOL's definition of lists is an example of an experimental method for handling
19.320 +recursive data types. Figure~\ref{hol-list} presents the theory \thydx{List}:
19.321 +the basic list operations with their types and properties.
19.322
19.323 The \sdx{case} construct is defined by the following translation:
19.324 {\dquotes
19.325 @@ -1740,8 +1734,8 @@
19.326 proves the two equivalent. It contains several datatype and inductive
19.327 definitions, and demonstrates their use.
19.328
19.329 -Directory {\tt HOL/ex} contains other examples and experimental proofs in
19.330 -{\HOL}. Here is an overview of the more interesting files.
19.331 +Directory {\tt HOL/ex} contains other examples and experimental proofs in HOL.
19.332 +Here is an overview of the more interesting files.
19.333 \begin{itemize}
19.334 \item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
19.335 predicate calculus theorems, ranging from simple tautologies to
19.336 @@ -1770,12 +1764,12 @@
19.337 as filter, which can compute indefinitely before yielding the next
19.338 element (if any!) of the lazy list. A coinduction principle is defined
19.339 for proving equations on lazy lists.
19.340 -
19.341 -\item Theory {\tt PropLog} proves the soundness and completeness of
19.342 - classical propositional logic, given a truth table semantics. The only
19.343 - connective is $\imp$. A Hilbert-style axiom system is specified, and its
19.344 - set of theorems defined inductively. A similar proof in \ZF{} is
19.345 - described elsewhere~\cite{paulson-set-II}.
19.346 +
19.347 +\item Theory {\tt PropLog} proves the soundness and completeness of classical
19.348 + propositional logic, given a truth table semantics. The only connective is
19.349 + $\imp$. A Hilbert-style axiom system is specified, and its set of theorems
19.350 + defined inductively. A similar proof in ZF is described
19.351 + elsewhere~\cite{paulson-set-II}.
19.352
19.353 \item Theory {\tt Term} develops an experimental recursive type definition;
19.354 the recursion goes through the type constructor~\tydx{list}.
19.355 @@ -1804,8 +1798,8 @@
19.356 of~$\alpha$. This version states that for every function from $\alpha$ to
19.357 its powerset, some subset is outside its range.
19.358
19.359 -The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
19.360 -the operator \cdx{range}. The set~$S$ is given as an unknown instead of a
19.361 +The Isabelle proof uses HOL's set theory, with the type $\alpha\,set$ and the
19.362 +operator \cdx{range}. The set~$S$ is given as an unknown instead of a
19.363 quantified variable so that we may inspect the subset found by the proof.
19.364 \begin{ttbox}
19.365 goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
19.366 @@ -1870,12 +1864,11 @@
19.367 {\out No subgoals!}
19.368 \end{ttbox}
19.369 How much creativity is required? As it happens, Isabelle can prove this
19.370 -theorem automatically. The classical set \ttindex{set_cs} contains rules
19.371 -for most of the constructs of \HOL's set theory. We must augment it with
19.372 -\tdx{equalityCE} to break up set equalities, and then apply best-first
19.373 -search. Depth-first search would diverge, but best-first search
19.374 -successfully navigates through the large search space.
19.375 -\index{search!best-first}
19.376 +theorem automatically. The classical set \ttindex{set_cs} contains rules for
19.377 +most of the constructs of HOL's set theory. We must augment it with
19.378 +\tdx{equalityCE} to break up set equalities, and then apply best-first search.
19.379 +Depth-first search would diverge, but best-first search successfully navigates
19.380 +through the large search space. \index{search!best-first}
19.381 \begin{ttbox}
19.382 choplev 0;
19.383 {\out Level 0}
20.1 --- a/doc-src/Logics/logics.tex Mon Aug 28 13:50:24 2000 +0200
20.2 +++ b/doc-src/Logics/logics.tex Mon Aug 28 13:52:38 2000 +0200
20.3 @@ -1,6 +1,6 @@
20.4 %% $Id$
20.5 \documentclass[12pt,a4paper]{report}
20.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
20.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
20.8
20.9 %%%STILL NEEDS MODAL, LCF
20.10 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
20.11 @@ -16,8 +16,8 @@
20.12 With Contributions by Tobias Nipkow and Markus Wenzel%
20.13 \thanks{Markus Wenzel made numerous improvements. Sara Kalvala
20.14 contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote
20.15 - wrote the first version of the logic~\LK{}. Tobias Nipkow developed
20.16 - \LCF{} and~\Cube{}. Martin Coen developed~\Modal{} with assistance
20.17 + wrote the first version of the logic~LK. Tobias Nipkow developed
20.18 + LCF and~Cube. Martin Coen developed~Modal with assistance
20.19 from Rajeev Gor\'e. The research has been funded by the EPSRC
20.20 (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
20.21 (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
21.1 --- a/doc-src/Logics/preface.tex Mon Aug 28 13:50:24 2000 +0200
21.2 +++ b/doc-src/Logics/preface.tex Mon Aug 28 13:52:38 2000 +0200
21.3 @@ -23,11 +23,11 @@
21.4 \begin{ttdescription}
21.5 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
21.6 which is the basis of a preliminary method for deriving programs from
21.7 - proofs~\cite{coen92}. It is built upon classical~\FOL{}.
21.8 + proofs~\cite{coen92}. It is built upon classical~FOL.
21.9
21.10 \item[\thydx{LCF}] is a version of Scott's Logic for Computable
21.11 Functions, which is also implemented by the~{\sc lcf}
21.12 - system~\cite{paulson87}. It is built upon classical~\FOL{}.
21.13 + system~\cite{paulson87}. It is built upon classical~FOL.
21.14
21.15 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
21.16 \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
22.1 --- a/doc-src/Logics/syntax.tex Mon Aug 28 13:50:24 2000 +0200
22.2 +++ b/doc-src/Logics/syntax.tex Mon Aug 28 13:52:38 2000 +0200
22.3 @@ -31,16 +31,15 @@
22.4 becomes syntactically invalid if the brackets are removed.
22.5
22.6 A {\bf binder} is a symbol associated with a constant of type
22.7 -$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as
22.8 -a binder for the constant~$All$, which has type $(\alpha\To o)\To o$.
22.9 -This defines the syntax $\forall x.t$ to mean $All(\lambda x.t)$. We
22.10 -can also write $\forall x@1\ldots x@m.t$ to abbreviate $\forall x@1.
22.11 -\ldots \forall x@m.t$; this is possible for any constant provided that
22.12 -$\tau$ and $\tau'$ are the same type. \HOL's description operator
22.13 -$\varepsilon x.P\,x$ has type $(\alpha\To bool)\To\alpha$ and can bind
22.14 -only one variable, except when $\alpha$ is $bool$. \ZF's bounded
22.15 -quantifier $\forall x\in A.P(x)$ cannot be declared as a binder
22.16 -because it has type $[i, i\To o]\To o$. The syntax for binders allows
22.17 +$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder
22.18 +for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the
22.19 +syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall
22.20 +x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is
22.21 +possible for any constant provided that $\tau$ and $\tau'$ are the same type.
22.22 +HOL's description operator $\varepsilon x.P\,x$ has type $(\alpha\To
22.23 +bool)\To\alpha$ and can bind only one variable, except when $\alpha$ is
22.24 +$bool$. ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
22.25 +binder because it has type $[i, i\To o]\To o$. The syntax for binders allows
22.26 type constraints on bound variables, as in
22.27 \[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
22.28
23.1 --- a/doc-src/Ref/Makefile Mon Aug 28 13:50:24 2000 +0200
23.2 +++ b/doc-src/Ref/Makefile Mon Aug 28 13:52:38 2000 +0200
23.3 @@ -15,7 +15,7 @@
23.4 FILES = ref.tex introduction.tex goals.tex tactic.tex tctical.tex \
23.5 thm.tex theories.tex defining.tex syntax.tex substitution.tex \
23.6 simplifier.tex classical.tex theory-syntax.tex \
23.7 - ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
23.8 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
23.9
23.10 dvi: $(NAME).dvi
23.11
24.1 --- a/doc-src/Ref/classical.tex Mon Aug 28 13:50:24 2000 +0200
24.2 +++ b/doc-src/Ref/classical.tex Mon Aug 28 13:52:38 2000 +0200
24.3 @@ -3,12 +3,11 @@
24.4 \index{classical reasoner|(}
24.5 \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
24.6
24.7 -Although Isabelle is generic, many users will be working in some
24.8 -extension of classical first-order logic.
24.9 -Isabelle's set theory~{\tt ZF} is built upon theory~\texttt{FOL},
24.10 -while {\HOL} conceptually contains first-order logic as a fragment.
24.11 -Theorem-proving in predicate logic is undecidable, but many
24.12 -researchers have developed strategies to assist in this task.
24.13 +Although Isabelle is generic, many users will be working in some extension of
24.14 +classical first-order logic. Isabelle's set theory~ZF is built upon
24.15 +theory~FOL, while HOL conceptually contains first-order logic as a fragment.
24.16 +Theorem-proving in predicate logic is undecidable, but many researchers have
24.17 +developed strategies to assist in this task.
24.18
24.19 Isabelle's classical reasoner is an \ML{} functor that accepts certain
24.20 information about a logic and delivers a suite of automatic tactics. Each
24.21 @@ -52,9 +51,9 @@
24.22 effectively. There are many tactics to choose from, including
24.23 {\tt Fast_tac} and \texttt{Best_tac}.
24.24
24.25 -We shall first discuss the underlying principles, then present the
24.26 -classical reasoner. Finally, we shall see how to instantiate it for new logics.
24.27 -The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed.
24.28 +We shall first discuss the underlying principles, then present the classical
24.29 +reasoner. Finally, we shall see how to instantiate it for new logics. The
24.30 +logics FOL, ZF, HOL and HOLCF have it already installed.
24.31
24.32
24.33 \section{The sequent calculus}
24.34 @@ -445,12 +444,11 @@
24.35 \begin{itemize}
24.36 \item It does not use the wrapper tacticals described above, such as
24.37 \ttindex{addss}.
24.38 -\item It ignores types, which can cause problems in \HOL. If it applies a rule
24.39 +\item It ignores types, which can cause problems in HOL. If it applies a rule
24.40 whose types are inappropriate, then proof reconstruction will fail.
24.41 \item It does not perform higher-order unification, as needed by the rule {\tt
24.42 - rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}. There are often
24.43 - alternatives to such rules, for example {\tt
24.44 - range_eqI} and \texttt{RepFun_eqI}.
24.45 + rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives
24.46 + to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
24.47 \item Function variables may only be applied to parameters of the subgoal.
24.48 (This restriction arises because the prover does not use higher-order
24.49 unification.) If other function variables are present then the prover will
25.1 --- a/doc-src/Ref/introduction.tex Mon Aug 28 13:50:24 2000 +0200
25.2 +++ b/doc-src/Ref/introduction.tex Mon Aug 28 13:52:38 2000 +0200
25.3 @@ -34,7 +34,7 @@
25.4 \({\langle}isabellehome{\rangle}\)/bin/isabelle
25.5 \end{ttbox}
25.6 This should start an interactive \ML{} session with the default object-logic
25.7 -(usually {\HOL}) already pre-loaded.
25.8 +(usually HOL) already pre-loaded.
25.9
25.10 Subsequently, we assume that the \texttt{isabelle} executable is determined
25.11 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
25.12 @@ -52,7 +52,7 @@
25.13 isabelle FOL
25.14 \end{ttbox}
25.15 This should put you into the world of polymorphic first-order logic (assuming
25.16 -that an image of {\FOL} has been pre-built).
25.17 +that an image of FOL has been pre-built).
25.18
25.19 \index{saving your session|bold} Isabelle provides no means of storing
25.20 theorems or internal proof objects on files. Theorems are simply part of the
25.21 @@ -62,7 +62,7 @@
25.22 \emph{writable} in the first place. The standard object-logic images are
25.23 usually read-only, so you have to create a private working copy first. For
25.24 example, the following shell command puts you into a writable Isabelle session
25.25 -of name \texttt{Foo} that initially contains just plain \HOL:
25.26 +of name \texttt{Foo} that initially contains just plain HOL:
25.27 \begin{ttbox}
25.28 isabelle HOL Foo
25.29 \end{ttbox}
25.30 @@ -202,7 +202,7 @@
25.31
25.32 \end{ttdescription}
25.33
25.34 -Note that theories of pre-built logic images (e.g.\ {\HOL}) are marked as
25.35 +Note that theories of pre-built logic images (e.g.\ HOL) are marked as
25.36 \emph{finished} and cannot be updated any more. See \S\ref{sec:more-theories}
25.37 for further information on Isabelle's theory loader.
25.38
26.1 --- a/doc-src/Ref/ref.tex Mon Aug 28 13:50:24 2000 +0200
26.2 +++ b/doc-src/Ref/ref.tex Mon Aug 28 13:52:38 2000 +0200
26.3 @@ -1,5 +1,5 @@
26.4 \documentclass[12pt,a4paper]{report}
26.5 -\usepackage{graphicx,../iman,../extra,../proof,../rail,../pdfsetup}
26.6 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup}
26.7
26.8 %% $Id$
26.9 %%\includeonly{}
27.1 --- a/doc-src/Ref/simp.tex Mon Aug 28 13:50:24 2000 +0200
27.2 +++ b/doc-src/Ref/simp.tex Mon Aug 28 13:52:38 2000 +0200
27.3 @@ -489,8 +489,8 @@
27.4
27.5
27.6 \section{A sample instantiation}
27.7 -Here is the instantiation of {\tt SIMP_DATA} for {\FOL}. The code for {\tt
27.8 -mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
27.9 +Here is the instantiation of {\tt SIMP_DATA} for FOL. The code for {\tt
27.10 + mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
27.11 \begin{ttbox}
27.12 structure FOL_SimpData : SIMP_DATA =
27.13 struct
28.1 --- a/doc-src/Ref/simplifier.tex Mon Aug 28 13:50:24 2000 +0200
28.2 +++ b/doc-src/Ref/simplifier.tex Mon Aug 28 13:52:38 2000 +0200
28.3 @@ -3,12 +3,11 @@
28.4 \label{chap:simplification}
28.5 \index{simplification|(}
28.6
28.7 -This chapter describes Isabelle's generic simplification package. It
28.8 -performs conditional and unconditional rewriting and uses contextual
28.9 -information (`local assumptions'). It provides several general hooks,
28.10 -which can provide automatic case splits during rewriting, for example.
28.11 -The simplifier is already set up for many of Isabelle's logics: \FOL,
28.12 -\ZF, \HOL, \HOLCF.
28.13 +This chapter describes Isabelle's generic simplification package. It performs
28.14 +conditional and unconditional rewriting and uses contextual information
28.15 +(`local assumptions'). It provides several general hooks, which can provide
28.16 +automatic case splits during rewriting, for example. The simplifier is
28.17 +already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.
28.18
28.19 The first section is a quick introduction to the simplifier that
28.20 should be sufficient to get started. The later sections explain more
28.21 @@ -71,9 +70,9 @@
28.22
28.23 \medskip
28.24
28.25 -As an example, consider the theory of arithmetic in \HOL. The (rather
28.26 -trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call
28.27 -of \texttt{Simp_tac} as follows:
28.28 +As an example, consider the theory of arithmetic in HOL. The (rather trivial)
28.29 +goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call of
28.30 +\texttt{Simp_tac} as follows:
28.31 \begin{ttbox}
28.32 context Arith.thy;
28.33 Goal "0 + (x + 0) = x + 0 + 0";
28.34 @@ -181,11 +180,11 @@
28.35
28.36 \end{ttdescription}
28.37
28.38 -When a new theory is built, its implicit simpset is initialized by the
28.39 -union of the respective simpsets of its parent theories. In addition,
28.40 -certain theory definition constructs (e.g.\ \ttindex{datatype} and
28.41 -\ttindex{primrec} in \HOL) implicitly augment the current simpset.
28.42 -Ordinary definitions are not added automatically!
28.43 +When a new theory is built, its implicit simpset is initialized by the union
28.44 +of the respective simpsets of its parent theories. In addition, certain
28.45 +theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec}
28.46 +in HOL) implicitly augment the current simpset. Ordinary definitions are not
28.47 +added automatically!
28.48
28.49 It is up the user to manipulate the current simpset further by
28.50 explicitly adding or deleting theorems and simplification procedures.
28.51 @@ -253,12 +252,11 @@
28.52 \end{ttbox}
28.53 \begin{ttdescription}
28.54
28.55 -\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very
28.56 - useful under normal circumstances because it doesn't contain
28.57 - suitable tactics (subgoaler etc.). When setting up the simplifier
28.58 - for a particular object-logic, one will typically define a more
28.59 - appropriate ``almost empty'' simpset. For example, in \HOL\ this is
28.60 - called \ttindexbold{HOL_basic_ss}.
28.61 +\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very useful
28.62 + under normal circumstances because it doesn't contain suitable tactics
28.63 + (subgoaler etc.). When setting up the simplifier for a particular
28.64 + object-logic, one will typically define a more appropriate ``almost empty''
28.65 + simpset. For example, in HOL this is called \ttindexbold{HOL_basic_ss}.
28.66
28.67 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$
28.68 and $ss@2$ by building the union of their respective rewrite rules,
28.69 @@ -1077,12 +1075,11 @@
28.70
28.71 \subsection{Example: sums of natural numbers}
28.72
28.73 -This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}).
28.74 -Theory \thydx{Arith} contains natural numbers arithmetic. Its
28.75 -associated simpset contains many arithmetic laws including
28.76 -distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list
28.77 -consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let
28.78 -us prove the theorem
28.79 +This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory
28.80 +\thydx{Arith} contains natural numbers arithmetic. Its associated simpset
28.81 +contains many arithmetic laws including distributivity of~$\times$ over~$+$,
28.82 +while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
28.83 +type \texttt{nat}. Let us prove the theorem
28.84 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
28.85 %
28.86 A functional~\texttt{sum} represents the summation operator under the
28.87 @@ -1216,12 +1213,11 @@
28.88 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
28.89 model checker syntax).
28.90
28.91 -The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an
28.92 -operator \texttt{split} together with some concrete syntax supporting
28.93 -$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a
28.94 -tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of
28.95 -some pair type) to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule
28.96 -is:
28.97 +The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
28.98 +\texttt{split} together with some concrete syntax supporting
28.99 +$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic
28.100 +that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
28.101 +to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is:
28.102 \begin{ttbox}
28.103 pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y))
28.104 \end{ttbox}
28.105 @@ -1298,7 +1294,7 @@
28.106 We first prove lots of standard rewrite rules about the logical
28.107 connectives. These include cancellation and associative laws. We
28.108 define a function that echoes the desired law and then supplies it the
28.109 -prover for intuitionistic \FOL:
28.110 +prover for intuitionistic FOL:
28.111 \begin{ttbox}
28.112 fun int_prove_fun s =
28.113 (writeln s;
28.114 @@ -1437,12 +1433,11 @@
28.115 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
28.116 \end{ttbox}
28.117 %
28.118 -The basic simpset for intuitionistic \FOL{} is
28.119 -\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt
28.120 - gen_all}, \texttt{atomize} and \texttt{mk_eq}. It solves simplified
28.121 -subgoals using \texttt{triv_rls} and assumptions, and by detecting
28.122 -contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of
28.123 -conditional rewrites.
28.124 +The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It
28.125 +preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
28.126 +It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
28.127 +detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals
28.128 +of conditional rewrites.
28.129
28.130 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
28.131 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
29.1 --- a/doc-src/Ref/substitution.tex Mon Aug 28 13:50:24 2000 +0200
29.2 +++ b/doc-src/Ref/substitution.tex Mon Aug 28 13:52:38 2000 +0200
29.3 @@ -61,7 +61,7 @@
29.4 eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.}
29.5 \end{ttbox}
29.6
29.7 -Logics \HOL, {\FOL} and {\ZF} define the tactic \ttindexbold{stac} by
29.8 +Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
29.9 \begin{ttbox}
29.10 fun stac eqth = CHANGED o rtac (eqth RS ssubst);
29.11 \end{ttbox}
30.1 --- a/doc-src/Ref/syntax.tex Mon Aug 28 13:50:24 2000 +0200
30.2 +++ b/doc-src/Ref/syntax.tex Mon Aug 28 13:52:38 2000 +0200
30.3 @@ -688,11 +688,11 @@
30.4 \section{Translation functions} \label{sec:tr_funs}
30.5 \index{translations|(}
30.6 %
30.7 -This section describes the translation function mechanism. By writing
30.8 -\ML{} functions, you can do almost everything to terms or \AST{}s
30.9 -during parsing and printing. The logic \LK\ is a good example of
30.10 -sophisticated transformations between internal and external
30.11 -representations of sequents; here, macros would be useless.
30.12 +This section describes the translation function mechanism. By writing \ML{}
30.13 +functions, you can do almost everything to terms or \AST{}s during parsing and
30.14 +printing. The logic LK is a good example of sophisticated transformations
30.15 +between internal and external representations of sequents; here, macros would
30.16 +be useless.
30.17
30.18 A full understanding of translations requires some familiarity
30.19 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
31.1 --- a/doc-src/Ref/tactic.tex Mon Aug 28 13:50:24 2000 +0200
31.2 +++ b/doc-src/Ref/tactic.tex Mon Aug 28 13:52:38 2000 +0200
31.3 @@ -422,9 +422,9 @@
31.4 flexflex_tac : tactic
31.5 \end{ttbox}
31.6 \begin{ttdescription}
31.7 -\item[\ttindexbold{distinct_subgoals_tac}]
31.8 - removes duplicate subgoals from a proof state. (These arise especially
31.9 - in \ZF{}, where the subgoals are essentially type constraints.)
31.10 +\item[\ttindexbold{distinct_subgoals_tac}] removes duplicate subgoals from a
31.11 + proof state. (These arise especially in ZF, where the subgoals are
31.12 + essentially type constraints.)
31.13
31.14 \item[\ttindexbold{prune_params_tac}]
31.15 removes unused parameters from all subgoals of the proof state. It works
32.1 --- a/doc-src/Ref/theories.tex Mon Aug 28 13:50:24 2000 +0200
32.2 +++ b/doc-src/Ref/theories.tex Mon Aug 28 13:52:38 2000 +0200
32.3 @@ -3,12 +3,12 @@
32.4
32.5 \chapter{Theories, Terms and Types} \label{theories}
32.6 \index{theories|(}\index{signatures|bold}
32.7 -\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the
32.8 -syntax, declarations and axioms of a mathematical development. They
32.9 -are built, starting from the {\Pure} or {\CPure} theory, by extending
32.10 -and merging existing theories. They have the \ML\ type
32.11 -\mltydx{theory}. Theory operations signal errors by raising exception
32.12 -\xdx{THEORY}, returning a message and a list of theories.
32.13 +\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax,
32.14 +declarations and axioms of a mathematical development. They are built,
32.15 +starting from the Pure or CPure theory, by extending and merging existing
32.16 +theories. They have the \ML\ type \mltydx{theory}. Theory operations signal
32.17 +errors by raising exception \xdx{THEORY}, returning a message and a list of
32.18 +theories.
32.19
32.20 Signatures, which contain information about sorts, types, constants and
32.21 syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
32.22 @@ -715,9 +715,9 @@
32.23 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
32.24 is the \textbf{application} of~$t$ to~$u$.
32.25 \end{ttdescription}
32.26 -Application is written as an infix operator to aid readability.
32.27 -Here is an \ML\ pattern to recognize \FOL{} formulae of
32.28 -the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
32.29 +Application is written as an infix operator to aid readability. Here is an
32.30 +\ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the
32.31 +subformulae to~$A$ and~$B$:
32.32 \begin{ttbox}
32.33 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
32.34 \end{ttbox}
33.1 --- a/doc-src/Ref/theory-syntax.tex Mon Aug 28 13:50:24 2000 +0200
33.2 +++ b/doc-src/Ref/theory-syntax.tex Mon Aug 28 13:52:38 2000 +0200
33.3 @@ -5,10 +5,10 @@
33.4
33.5 \chapter{Syntax of Isabelle Theories}\label{app:TheorySyntax}
33.6
33.7 -Below we present the full syntax of theory definition files as
33.8 -provided by {\Pure} Isabelle --- object-logics may add their own
33.9 -sections. \S\ref{sec:ref-defining-theories} explains the meanings of
33.10 -these constructs. The syntax obeys the following conventions:
33.11 +Below we present the full syntax of theory definition files as provided by
33.12 +Pure Isabelle --- object-logics may add their own sections.
33.13 +\S\ref{sec:ref-defining-theories} explains the meanings of these constructs.
33.14 +The syntax obeys the following conventions:
33.15 \begin{itemize}
33.16 \item {\tt Typewriter font} denotes terminal symbols.
33.17
34.1 --- a/doc-src/System/Makefile Mon Aug 28 13:50:24 2000 +0200
34.2 +++ b/doc-src/System/Makefile Mon Aug 28 13:52:38 2000 +0200
34.3 @@ -13,7 +13,7 @@
34.4
34.5 NAME = system
34.6 FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
34.7 - ../iman.sty ../extra.sty ../manual.bib
34.8 + ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
34.9
34.10 dvi: $(NAME).dvi
34.11
35.1 --- a/doc-src/System/fonts.tex Mon Aug 28 13:50:24 2000 +0200
35.2 +++ b/doc-src/System/fonts.tex Mon Aug 28 13:52:38 2000 +0200
35.3 @@ -4,8 +4,8 @@
35.4 \chapter{Fonts and character encodings}
35.5
35.6 Using the print mode mechanism of Isabelle, variant forms of output become
35.7 -very easy. As the canonical application of this feature, {\Pure} and major
35.8 -object-logics (\FOL, \ZF, \HOL, \HOLCF) support optional input and output of
35.9 +very easy. As the canonical application of this feature, Pure and major
35.10 +object-logics (FOL, ZF, HOL, HOLCF) support optional input and output of
35.11 proper mathematical symbols as built-in option.
35.12
35.13 Symbolic output is enabled by activating the ``\ttindex{symbols}'' print mode.
36.1 --- a/doc-src/System/present.tex Mon Aug 28 13:50:24 2000 +0200
36.2 +++ b/doc-src/System/present.tex Mon Aug 28 13:52:38 2000 +0200
36.3 @@ -38,7 +38,7 @@
36.4
36.5 In order to let Isabelle generate theory browsing information, simply append
36.6 ``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
36.7 -making a logic. For example, in order to do this for {\FOL}, add this to your
36.8 +making a logic. For example, in order to do this for FOL, add this to your
36.9 Isabelle settings file
36.10 \begin{ttbox}
36.11 ISABELLE_USEDIR_OPTIONS="-i true"
36.12 @@ -87,8 +87,8 @@
36.13 isatool usedir -i true HOL Foo
36.14 \end{ttbox}
36.15 This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
36.16 -to load all your theories, and {\HOL} is your parent logic image. Ideally,
36.17 -theory browser information would have been generated for {\HOL} already.
36.18 +to load all your theories, and HOL is your parent logic image. Ideally,
36.19 +theory browser information would have been generated for HOL already.
36.20
36.21 Alternatively, one may specify an external link to an existing body of HTML
36.22 data by giving \texttt{usedir} a \texttt{-P} option like this:
36.23 @@ -499,7 +499,7 @@
36.24 \medskip Any \texttt{usedir} session is named by some \emph{session
36.25 identifier}. These accumulate, documenting the way sessions depend on
36.26 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
36.27 -examples of {\FOL}, which in turn is built upon {\Pure}.
36.28 +examples of FOL, which in turn is built upon Pure.
36.29
36.30 The current session's identifier is by default just the base name of the
36.31 \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in
37.1 --- a/doc-src/System/system.tex Mon Aug 28 13:50:24 2000 +0200
37.2 +++ b/doc-src/System/system.tex Mon Aug 28 13:52:38 2000 +0200
37.3 @@ -2,7 +2,7 @@
37.4 %% $Id$
37.5
37.6 \documentclass[12pt,a4paper]{report}
37.7 -\usepackage{graphicx,../iman,../extra,../pdfsetup}
37.8 +\usepackage{graphicx,../iman,../extra,../ttbox,../pdfsetup}
37.9
37.10
37.11 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
38.1 --- a/doc-src/Tutorial/Makefile Mon Aug 28 13:50:24 2000 +0200
38.2 +++ b/doc-src/Tutorial/Makefile Mon Aug 28 13:52:38 2000 +0200
38.3 @@ -13,7 +13,7 @@
38.4
38.5 NAME = tutorial
38.6 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
38.7 - ../iman.sty ttbox.sty extra.sty
38.8 + ../iman.sty ../ttbox.sty ../extra.sty
38.9
38.10 dvi: $(NAME).dvi
38.11
39.1 --- a/doc-src/Tutorial/extra.sty Mon Aug 28 13:50:24 2000 +0200
39.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
39.3 @@ -1,29 +0,0 @@
39.4 -% extra.sty : Isabelle Manual extra macros for non-Springer version
39.5 -%
39.6 -\typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
39.7 -
39.8 -\usepackage{ttbox}
39.9 -{\obeylines\gdef\ttbreak
39.10 -{\allowbreak}}
39.11 -
39.12 -%%Euro-style date: 20 September 1955
39.13 -\def\today{\number\day\space\ifcase\month\or
39.14 -January\or February\or March\or April\or May\or June\or
39.15 -July\or August\or September\or October\or November\or December\fi
39.16 -\space\number\year}
39.17 -
39.18 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
39.19 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
39.20 - \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
39.21 - \pagenumbering{arabic}}
39.22 -
39.23 -%%%Ruled chapter headings
39.24 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf
39.25 - #1 \vskip 14pt\hrule height1pt}
39.26 -\def\@makechapterhead#1{ { \parindent 0pt
39.27 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par
39.28 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
39.29 -
39.30 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright
39.31 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
39.32 -
40.1 --- a/doc-src/Tutorial/ttbox.sty Mon Aug 28 13:50:24 2000 +0200
40.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
40.3 @@ -1,20 +0,0 @@
40.4 -\ProvidesPackage{ttbox}[1997/06/25]
40.5 -\RequirePackage{alltt}
40.6 -
40.7 -%%%Boxed terminal sessions
40.8 -
40.9 -%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH
40.10 -\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\}
40.11 -
40.12 -%Restores % as the comment character (especially, to suppress line breaks)
40.13 -\newcommand\comments{\catcode`\%=14\relax}
40.14 -
40.15 -%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox
40.16 -\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}}
40.17 -
40.18 -%Indented alltt* environment with small point size
40.19 -%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line
40.20 -\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}%
40.21 - {\end{alltt*}\end{quote}}
40.22 -
40.23 -\endinput
41.1 --- a/doc-src/Tutorial/tutorial.tex Mon Aug 28 13:50:24 2000 +0200
41.2 +++ b/doc-src/Tutorial/tutorial.tex Mon Aug 28 13:52:38 2000 +0200
41.3 @@ -1,5 +1,5 @@
41.4 \documentclass[11pt,a4paper]{report}
41.5 -\usepackage{latexsym,verbatim,graphicx,../iman,extra,../pdfsetup}
41.6 +\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,../pdfsetup}
41.7
41.8 \newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
41.9
42.1 --- a/doc-src/TutorialI/Makefile Mon Aug 28 13:50:24 2000 +0200
42.2 +++ b/doc-src/TutorialI/Makefile Mon Aug 28 13:52:38 2000 +0200
42.3 @@ -13,7 +13,7 @@
42.4
42.5 NAME = tutorial
42.6 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
42.7 - ../iman.sty ttbox.sty extra.sty \
42.8 + ../iman.sty ../ttbox.sty ../extra.sty \
42.9 isabelle.sty isabellesym.sty ../pdfsetup.sty
42.10
42.11 dvi: $(NAME).dvi
43.1 --- a/doc-src/TutorialI/extra.sty Mon Aug 28 13:50:24 2000 +0200
43.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
43.3 @@ -1,29 +0,0 @@
43.4 -% extra.sty : Isabelle Manual extra macros for non-Springer version
43.5 -%
43.6 -\typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
43.7 -
43.8 -\usepackage{ttbox}
43.9 -{\obeylines\gdef\ttbreak
43.10 -{\allowbreak}}
43.11 -
43.12 -%%Euro-style date: 20 September 1955
43.13 -\def\today{\number\day\space\ifcase\month\or
43.14 -January\or February\or March\or April\or May\or June\or
43.15 -July\or August\or September\or October\or November\or December\fi
43.16 -\space\number\year}
43.17 -
43.18 -%%%Put first chapter on odd page, with arabic numbering; like \cleardoublepage
43.19 -\newcommand\clearfirst{\clearpage\ifodd\c@page\else
43.20 - \hbox{}\newpage\if@twocolumn\hbox{}\newpage\fi\fi
43.21 - \pagenumbering{arabic}}
43.22 -
43.23 -%%%Ruled chapter headings
43.24 -\def\@rulehead#1{\hrule height1pt \vskip 14pt \Huge \bf
43.25 - #1 \vskip 14pt\hrule height1pt}
43.26 -\def\@makechapterhead#1{ { \parindent 0pt
43.27 - \ifnum\c@secnumdepth >\m@ne \raggedleft\large\bf\@chapapp{} \thechapter \par
43.28 - \vskip 20pt \fi \raggedright \@rulehead{#1} \par \nobreak \vskip 40pt } }
43.29 -
43.30 -\def\@makeschapterhead#1{ { \parindent 0pt \raggedright
43.31 - \@rulehead{#1} \par \nobreak \vskip 40pt } }
43.32 -
44.1 --- a/doc-src/TutorialI/ttbox.sty Mon Aug 28 13:50:24 2000 +0200
44.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
44.3 @@ -1,20 +0,0 @@
44.4 -\ProvidesPackage{ttbox}[1997/06/25]
44.5 -\RequirePackage{alltt}
44.6 -
44.7 -%%%Boxed terminal sessions
44.8 -
44.9 -%Redefines \{ and \} to be in \tt font and \| to make a BACKSLASH
44.10 -\def\ttbraces{\chardef\{=`\{\chardef\}=`\}\chardef\|=`\\}
44.11 -
44.12 -%Restores % as the comment character (especially, to suppress line breaks)
44.13 -\newcommand\comments{\catcode`\%=14\relax}
44.14 -
44.15 -%alltt* environment: like alltt but smaller, and with \{ \} and \| as in ttbox
44.16 -\newenvironment{alltt*}{\begin{alltt}\footnotesize\ttbraces}{\end{alltt}}
44.17 -
44.18 -%Indented alltt* environment with small point size
44.19 -%NO LINE BREAKS are allowed unless \pagebreak appears at START of a line
44.20 -\newenvironment{ttbox}{\begin{quote}\samepage\begin{alltt*}}%
44.21 - {\end{alltt*}\end{quote}}
44.22 -
44.23 -\endinput
45.1 --- a/doc-src/TutorialI/tutorial.tex Mon Aug 28 13:50:24 2000 +0200
45.2 +++ b/doc-src/TutorialI/tutorial.tex Mon Aug 28 13:52:38 2000 +0200
45.3 @@ -1,7 +1,7 @@
45.4 % pr(latex xsymbols symbols)
45.5 \documentclass[11pt,a4paper]{report}
45.6 \usepackage{isabelle,isabellesym}
45.7 -\usepackage{latexsym,verbatim,graphicx,../iman,extra,comment}
45.8 +\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
45.9 \usepackage{../pdfsetup} %last package!
45.10
45.11 \newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions
46.1 --- a/doc-src/ZF/FOL.tex Mon Aug 28 13:50:24 2000 +0200
46.2 +++ b/doc-src/ZF/FOL.tex Mon Aug 28 13:52:38 2000 +0200
46.3 @@ -192,7 +192,7 @@
46.4
46.5
46.6 \section{Generic packages}
46.7 -\FOL{} instantiates most of Isabelle's generic packages.
46.8 +FOL instantiates most of Isabelle's generic packages.
46.9 \begin{itemize}
46.10 \item
46.11 It instantiates the simplifier. Both equality ($=$) and the biconditional
46.12 @@ -210,9 +210,9 @@
46.13 It instantiates the classical reasoner. See~\S\ref{fol-cla-prover}
46.14 for details.
46.15
46.16 -\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
46.17 - for an equality throughout a subgoal and its hypotheses. This tactic uses
46.18 - \FOL's general substitution rule.
46.19 +\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
46.20 + an equality throughout a subgoal and its hypotheses. This tactic uses FOL's
46.21 + general substitution rule.
46.22 \end{itemize}
46.23
46.24 \begin{warn}\index{simplification!of conjunctions}%
46.25 @@ -331,10 +331,10 @@
46.26 the rule
46.27 $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
46.28 \noindent
46.29 -Natural deduction in classical logic is not really all that natural.
46.30 -{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
46.31 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
46.32 -rule (see Fig.\ts\ref{fol-cla-derived}).
46.33 +Natural deduction in classical logic is not really all that natural. FOL
46.34 +derives classical introduction rules for $\disj$ and~$\exists$, as well as
46.35 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
46.36 +Fig.\ts\ref{fol-cla-derived}).
46.37
46.38 The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
46.39 Best_tac} refer to the default claset (\texttt{claset()}), which works for most
46.40 @@ -897,8 +897,8 @@
46.41 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to
46.42 $true\bimp false$, which is of course invalid.
46.43
46.44 -We can repeat this analysis by expanding definitions, using just
46.45 -the rules of {\FOL}:
46.46 +We can repeat this analysis by expanding definitions, using just the rules of
46.47 +FOL:
46.48 \begin{ttbox}
46.49 choplev 0;
46.50 {\out Level 0}
47.1 --- a/doc-src/ZF/Makefile Mon Aug 28 13:50:24 2000 +0200
47.2 +++ b/doc-src/ZF/Makefile Mon Aug 28 13:52:38 2000 +0200
47.3 @@ -13,7 +13,7 @@
47.4
47.5 NAME = logics-ZF
47.6 FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex \
47.7 - ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../manual.bib
47.8 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
47.9
47.10 dvi: $(NAME).dvi
47.11
48.1 --- a/doc-src/ZF/ZF.tex Mon Aug 28 13:50:24 2000 +0200
48.2 +++ b/doc-src/ZF/ZF.tex Mon Aug 28 13:52:38 2000 +0200
48.3 @@ -23,10 +23,9 @@
48.4 provides a streamlined syntax for defining primitive recursive functions over
48.5 datatypes.
48.6
48.7 -Because {\ZF} is an extension of {\FOL}, it provides the same
48.8 -packages, namely \texttt{hyp_subst_tac}, the simplifier, and the
48.9 -classical reasoner. The default simpset and claset are usually
48.10 -satisfactory.
48.11 +Because ZF is an extension of FOL, it provides the same packages, namely
48.12 +\texttt{hyp_subst_tac}, the simplifier, and the classical reasoner. The
48.13 +default simpset and claset are usually satisfactory.
48.14
48.15 Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
48.16 less formally than this chapter. Isabelle employs a novel treatment of
48.17 @@ -94,7 +93,7 @@
48.18 \begin{center}
48.19 \index{*"`"` symbol}
48.20 \index{*"-"`"` symbol}
48.21 -\index{*"` symbol}\index{function applications!in \ZF}
48.22 +\index{*"` symbol}\index{function applications!in ZF}
48.23 \index{*"- symbol}
48.24 \index{*": symbol}
48.25 \index{*"<"= symbol}
48.26 @@ -111,7 +110,7 @@
48.27 \end{tabular}
48.28 \end{center}
48.29 \subcaption{Infixes}
48.30 -\caption{Constants of {\ZF}} \label{zf-constants}
48.31 +\caption{Constants of ZF} \label{zf-constants}
48.32 \end{figure}
48.33
48.34
48.35 @@ -125,10 +124,10 @@
48.36 bounded quantifiers. In most other respects, Isabelle implements precisely
48.37 Zermelo-Fraenkel set theory.
48.38
48.39 -Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
48.40 +Figure~\ref{zf-constants} lists the constants and infixes of~ZF, while
48.41 Figure~\ref{zf-trans} presents the syntax translations. Finally,
48.42 -Figure~\ref{zf-syntax} presents the full grammar for set theory, including
48.43 -the constructs of \FOL.
48.44 +Figure~\ref{zf-syntax} presents the full grammar for set theory, including the
48.45 +constructs of FOL.
48.46
48.47 Local abbreviations can be introduced by a \texttt{let} construct whose
48.48 syntax appears in Fig.\ts\ref{zf-syntax}. Internally it is translated into
48.49 @@ -136,7 +135,7 @@
48.50 definition, \tdx{Let_def}.
48.51
48.52 Apart from \texttt{let}, set theory does not use polymorphism. All terms in
48.53 -{\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
48.54 +ZF have type~\tydx{i}, which is the type of individuals and has class~{\tt
48.55 term}. The type of first-order formulae, remember, is~\textit{o}.
48.56
48.57 Infix operators include binary union and intersection ($A\un B$ and
48.58 @@ -167,15 +166,15 @@
48.59 abbreviates the nest of pairs\par\nobreak
48.60 \centerline{\texttt{Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots).}}
48.61
48.62 -In {\ZF}, a function is a set of pairs. A {\ZF} function~$f$ is simply an
48.63 -individual as far as Isabelle is concerned: its Isabelle type is~$i$, not
48.64 -say $i\To i$. The infix operator~{\tt`} denotes the application of a
48.65 -function set to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The
48.66 -syntax for image is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
48.67 +In ZF, a function is a set of pairs. A ZF function~$f$ is simply an
48.68 +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
48.69 +$i\To i$. The infix operator~{\tt`} denotes the application of a function set
48.70 +to its argument; we must write~$f{\tt`}x$, not~$f(x)$. The syntax for image
48.71 +is~$f{\tt``}A$ and that for inverse image is~$f{\tt-``}A$.
48.72
48.73
48.74 \begin{figure}
48.75 -\index{lambda abs@$\lambda$-abstractions!in \ZF}
48.76 +\index{lambda abs@$\lambda$-abstractions!in ZF}
48.77 \index{*"-"> symbol}
48.78 \index{*"* symbol}
48.79 \begin{center} \footnotesize\tt\frenchspacing
48.80 @@ -215,7 +214,7 @@
48.81 \rm bounded $\exists$
48.82 \end{tabular}
48.83 \end{center}
48.84 -\caption{Translations for {\ZF}} \label{zf-trans}
48.85 +\caption{Translations for ZF} \label{zf-trans}
48.86 \end{figure}
48.87
48.88
48.89 @@ -264,7 +263,7 @@
48.90 & | & "EX!~" id~id^* " . " formula
48.91 \end{array}
48.92 \]
48.93 -\caption{Full grammar for {\ZF}} \label{zf-syntax}
48.94 +\caption{Full grammar for ZF} \label{zf-syntax}
48.95 \end{figure}
48.96
48.97
48.98 @@ -321,14 +320,13 @@
48.99 no constants~\texttt{op~*} and~\hbox{\tt op~->}.} Isabelle accepts these
48.100 abbreviations in parsing and uses them whenever possible for printing.
48.101
48.102 -\index{*THE symbol}
48.103 -As mentioned above, whenever the axioms assert the existence and uniqueness
48.104 -of a set, Isabelle's set theory declares a constant for that set. These
48.105 -constants can express the {\bf definite description} operator~$\iota
48.106 -x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$, if such exists.
48.107 -Since all terms in {\ZF} denote something, a description is always
48.108 -meaningful, but we do not know its value unless $P[x]$ defines it uniquely.
48.109 -Using the constant~\cdx{The}, we may write descriptions as {\tt
48.110 +\index{*THE symbol} As mentioned above, whenever the axioms assert the
48.111 +existence and uniqueness of a set, Isabelle's set theory declares a constant
48.112 +for that set. These constants can express the {\bf definite description}
48.113 +operator~$\iota x. P[x]$, which stands for the unique~$a$ satisfying~$P[a]$,
48.114 +if such exists. Since all terms in ZF denote something, a description is
48.115 +always meaningful, but we do not know its value unless $P[x]$ defines it
48.116 +uniquely. Using the constant~\cdx{The}, we may write descriptions as {\tt
48.117 The($\lambda x. P[x]$)} or use the syntax \hbox{\tt THE $x$.\ $P[x]$}.
48.118
48.119 \index{*lam symbol}
48.120 @@ -385,7 +383,7 @@
48.121 \tdx{Diff_def} A - B == {\ttlbrace}x:A . x~:B{\ttrbrace}
48.122 \subcaption{Union, intersection, difference}
48.123 \end{ttbox}
48.124 -\caption{Rules and axioms of {\ZF}} \label{zf-rules}
48.125 +\caption{Rules and axioms of ZF} \label{zf-rules}
48.126 \end{figure}
48.127
48.128
48.129 @@ -417,7 +415,7 @@
48.130 \tdx{restrict_def} restrict(f,A) == lam x:A. f`x
48.131 \subcaption{Functions and general product}
48.132 \end{ttbox}
48.133 -\caption{Further definitions of {\ZF}} \label{zf-defs}
48.134 +\caption{Further definitions of ZF} \label{zf-defs}
48.135 \end{figure}
48.136
48.137
48.138 @@ -515,7 +513,7 @@
48.139 \tdx{PowD} A : Pow(B) ==> A<=B
48.140 \subcaption{The empty set; power sets}
48.141 \end{ttbox}
48.142 -\caption{Basic derived rules for {\ZF}} \label{zf-lemmas1}
48.143 +\caption{Basic derived rules for ZF} \label{zf-lemmas1}
48.144 \end{figure}
48.145
48.146
48.147 @@ -555,7 +553,7 @@
48.148 Figure~\ref{zf-lemmas3} presents rules for general union and intersection.
48.149 The empty intersection should be undefined. We cannot have
48.150 $\bigcap(\emptyset)=V$ because $V$, the universal class, is not a set. All
48.151 -expressions denote something in {\ZF} set theory; the definition of
48.152 +expressions denote something in ZF set theory; the definition of
48.153 intersection implies $\bigcap(\emptyset)=\emptyset$, but this value is
48.154 arbitrary. The rule \tdx{InterI} must have a premise to exclude
48.155 the empty intersection. Some of the laws governing intersections require
48.156 @@ -1051,7 +1049,7 @@
48.157 See file \texttt{ZF/equalities.ML}.
48.158
48.159 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual
48.160 -operators including a conditional (Fig.\ts\ref{zf-bool}). Although {\ZF} is a
48.161 +operators including a conditional (Fig.\ts\ref{zf-bool}). Although ZF is a
48.162 first-order theory, you can obtain the effect of higher-order logic using
48.163 \texttt{bool}-valued functions, for example. The constant~\texttt{1} is
48.164 translated to \texttt{succ(0)}.
48.165 @@ -1343,13 +1341,13 @@
48.166
48.167 \section{Automatic Tools}
48.168
48.169 -{\ZF} provides the simplifier and the classical reasoner. Moreover it
48.170 -supplies a specialized tool to infer `types' of terms.
48.171 +ZF provides the simplifier and the classical reasoner. Moreover it supplies a
48.172 +specialized tool to infer `types' of terms.
48.173
48.174 \subsection{Simplification}
48.175
48.176 -{\ZF} inherits simplification from {\FOL} but adopts it for set theory. The
48.177 -extraction of rewrite rules takes the {\ZF} primitives into account. It can
48.178 +ZF inherits simplification from FOL but adopts it for set theory. The
48.179 +extraction of rewrite rules takes the ZF primitives into account. It can
48.180 strip bounded universal quantifiers from a formula; for example, ${\forall
48.181 x\in A. f(x)=g(x)}$ yields the conditional rewrite rule $x\in A \Imp
48.182 f(x)=g(x)$. Given $a\in\{x\in A. P(x)\}$ it extracts rewrite rules from $a\in
48.183 @@ -1360,10 +1358,9 @@
48.184 works for most purposes. A small simplification set for set theory is
48.185 called~\ttindexbold{ZF_ss}, and you can even use \ttindex{FOL_ss} as a minimal
48.186 starting point. \texttt{ZF_ss} contains congruence rules for all the binding
48.187 -operators of {\ZF}\@. It contains all the conversion rules, such as
48.188 -\texttt{fst} and \texttt{snd}, as well as the rewrites shown in
48.189 -Fig.\ts\ref{zf-simpdata}. See the file \texttt{ZF/simpdata.ML} for a fuller
48.190 -list.
48.191 +operators of ZF. It contains all the conversion rules, such as \texttt{fst}
48.192 +and \texttt{snd}, as well as the rewrites shown in Fig.\ts\ref{zf-simpdata}.
48.193 +See the file \texttt{ZF/simpdata.ML} for a fuller list.
48.194
48.195
48.196 \subsection{Classical Reasoning}
48.197 @@ -1396,7 +1393,7 @@
48.198 \subsection{Type-Checking Tactics}
48.199 \index{type-checking tactics}
48.200
48.201 -Isabelle/{\ZF} provides simple tactics to help automate those proofs that are
48.202 +Isabelle/ZF provides simple tactics to help automate those proofs that are
48.203 essentially type-checking. Such proofs are built by applying rules such as
48.204 these:
48.205 \begin{ttbox}
48.206 @@ -1614,13 +1611,13 @@
48.207 \label{sec:ZF:datatype}
48.208 \index{*datatype|(}
48.209
48.210 -The \ttindex{datatype} definition package of \ZF\ constructs inductive
48.211 -datatypes similar to those of \ML. It can also construct coinductive
48.212 -datatypes (codatatypes), which are non-well-founded structures such as
48.213 -streams. It defines the set using a fixed-point construction and proves
48.214 -induction rules, as well as theorems for recursion and case combinators. It
48.215 -supplies mechanisms for reasoning about freeness. The datatype package can
48.216 -handle both mutual and indirect recursion.
48.217 +The \ttindex{datatype} definition package of ZF constructs inductive datatypes
48.218 +similar to those of \ML. It can also construct coinductive datatypes
48.219 +(codatatypes), which are non-well-founded structures such as streams. It
48.220 +defines the set using a fixed-point construction and proves induction rules,
48.221 +as well as theorems for recursion and case combinators. It supplies
48.222 +mechanisms for reasoning about freeness. The datatype package can handle both
48.223 +mutual and indirect recursion.
48.224
48.225
48.226 \subsection{Basics}
48.227 @@ -2440,10 +2437,10 @@
48.228 proves the two equivalent. It contains several datatype and inductive
48.229 definitions, and demonstrates their use.
48.230
48.231 -The directory \texttt{ZF/ex} contains further developments in {\ZF} set
48.232 -theory. Here is an overview; see the files themselves for more details. I
48.233 -describe much of this material in other
48.234 -publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
48.235 +The directory \texttt{ZF/ex} contains further developments in ZF set theory.
48.236 +Here is an overview; see the files themselves for more details. I describe
48.237 +much of this material in other
48.238 +publications~\cite{paulson-set-I,paulson-set-II,paulson-CADE}.
48.239 \begin{itemize}
48.240 \item File \texttt{misc.ML} contains miscellaneous examples such as
48.241 Cantor's Theorem, the Schr\"oder-Bernstein Theorem and the `Composition
49.1 --- a/doc-src/ZF/logics-ZF.tex Mon Aug 28 13:50:24 2000 +0200
49.2 +++ b/doc-src/ZF/logics-ZF.tex Mon Aug 28 13:52:38 2000 +0200
49.3 @@ -1,6 +1,6 @@
49.4 %% $Id$
49.5 \documentclass[11pt,a4paper]{report}
49.6 -\usepackage{graphicx,../iman,../extra,../proof,../rail,latexsym,../pdfsetup}
49.7 +\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,latexsym,../pdfsetup}
49.8
49.9 %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
49.10 %%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
49.11 @@ -15,8 +15,8 @@
49.12 \texttt{lcp@cl.cam.ac.uk}\\[3ex]
49.13 With Contributions by Tobias Nipkow and Markus Wenzel%
49.14 \thanks{Markus Wenzel made numerous improvements.
49.15 - Philippe de Groote contributed to~\ZF{}. Philippe No\"el and
49.16 - Martin Coen made many contributions to~\ZF{}. The research has
49.17 + Philippe de Groote contributed to~ZF. Philippe No\"el and
49.18 + Martin Coen made many contributions to~ZF. The research has
49.19 been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381,
49.20 GR/K77051, GR/M75440) and by ESPRIT (projects 3245:
49.21 Logical Frameworks, and 6453: Types) and by the DFG Schwerpunktprogramm