author | wenzelm |

Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) | |

changeset 9695 | ec7d7f877712 |

parent 9694 | 13f3aaf12be2 |

child 9696 | 5c8acc0282c8 |

proper setup of iman.sty/extra.sty/ttbox.sty;

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