--- a/doc-src/Logics/HOL.tex Wed May 07 17:15:57 1997 +0200
+++ b/doc-src/Logics/HOL.tex Wed May 07 17:16:18 1997 +0200
@@ -312,7 +312,7 @@
But theory~\HOL{}, like all other Isabelle theories, uses
meta-equality~({\tt==}) for definitions.
\begin{warn}
-The above definitions should never be expanded and are shown for completeness
+The definitions above should never be expanded and are shown for completeness
only. Instead users should reason in terms of the derived rules shown below
or, better still, using high-level tactics
(see~\S\ref{sec:HOL:generic-packages}).
@@ -846,8 +846,8 @@
HOL/equalities.ML}.
\begin{warn}
-Many set theoretic theorems are proved automatically by {\tt Fast_tac}.
-Hence you rarely need to refer to the above theorems explicitly.
+\texttt{Blast_tac} proves many set-theoretic theorems automatically.
+Hence you seldom need to refer to the theorems above.
\end{warn}
\begin{figure}
@@ -885,15 +885,13 @@
\section{Generic packages}
\label{sec:HOL:generic-packages}
-\HOL\ instantiates most of Isabelle's generic packages.
+\HOL\ instantiates most of Isabelle's generic packages, making available the
+simplifier and the classical reasoner.
\subsection{Substitution and simplification}
-%Because it includes a general substitution rule, \HOL\ instantiates the
-%tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
-%subgoal and its hypotheses.
-
-It instantiates the simplifier. Tactics such as {\tt Asm_simp_tac} and {\tt
+The simplifier is available in \HOL. Tactics such as {\tt Asm_simp_tac} and
+{\tt
Full_simp_tac} use the default simpset ({\tt!simpset}), which works for most
purposes. A minimal simplification set for higher-order logic
is~\ttindexbold{HOL_ss}. Equality~($=$), which also expresses logical
@@ -904,17 +902,16 @@
{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
and simplification.
-\begin{warn}\index{simplification!of conjunctions}
- The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$
- to \verb$a = b & ...b...$: it does not use the left part of a conjunction
- while simplifying the right part. This can be changed by including
- \ttindex{conj_cong} in a simpset: \verb$addcongs [conj_cong]$. It can slow
- down rewriting and is therefore not included by default.
+\begin{warn}\index{simplification!of conjunctions}%
+ Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The
+ left part of a conjunction helps in simplifying the right part. This effect
+ is not available by default: it can be slow. It can be obtained by
+ including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
\end{warn}
-In case a rewrite rule cannot be dealt with by the simplifier (either because
-of nontermination or because its left-hand side is too flexible), HOL
-provides {\tt stac}:
+If the simplifier cannot use a certain rewrite rule---either because of
+nontermination or because its left-hand side is too flexible---then you might
+try {\tt stac}:
\begin{ttdescription}
\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
@@ -925,9 +922,9 @@
additional (first) subgoal.
\end{ttdescription}
-Because \HOL\ includes a general substitution rule, the tactic {\tt
-hyp_subst_tac}, which substitutes for an equality throughout a subgoal and
-its hypotheses, is also available.
+ \HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
+ for an equality throughout a subgoal and its hypotheses. This tactic uses
+ \HOL's general substitution rule.
\subsection{Classical reasoning}
@@ -936,7 +933,7 @@
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule; recall Fig.\ts\ref{hol-lemmas2} above.
-The classical reasoner is installed. Tactics such as {\tt Fast_tac} and {\tt
+The classical reasoner is installed. Tactics such as {\tt Blast_tac} and {\tt
Best_tac} use the default claset ({\tt!claset}), which works for most
purposes. Named clasets include \ttindexbold{prop_cs}, which includes the
propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier
@@ -984,8 +981,8 @@
\tdx{split} split c (a,b) = c a b
\tdx{expand_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
-\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
-\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
+\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
+\tdx{SigmaE} [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
\end{ttbox}
\caption{Type $\alpha\times\beta$}\label{hol-prod}
\end{figure}
@@ -1309,9 +1306,6 @@
hd (x#xs) = x
tl (x#xs) = xs
-%
-%ttl [] = []
-%ttl (x#xs) = xs
[] @ ys = ys
(x#xs) @ ys = x # xs @ ys
@@ -1322,9 +1316,6 @@
filter P [] = []
filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
-list_all P [] = True
-list_all P (x#xs) = (P x & list_all P xs)
-
set_of_list [] = \{\}
set_of_list (x#xs) = insert x (set_of_list xs)
@@ -1466,8 +1457,7 @@
abstract axiomatic description $P$ of a type, this involves two steps:
\begin{enumerate}
\item Find an appropriate type $\tau$ and subset $A$ which has the desired
- properties $P$, and make the above type definition based on this
- representation.
+ properties $P$, and make a type definition based on this representation.
\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
\end{enumerate}
You can now forget about the representation and work solely in terms of the
@@ -2008,10 +1998,11 @@
monos "[Pow_mono]"
end
\end{ttbox}
-The HOL distribution contains many other inductive definitions, such as the
-theory {\tt HOL/ex/PropLog.thy} and the subdirectories {\tt IMP}, {\tt Lambda}
-and {\tt Auth}. The theory {\tt HOL/ex/LList.thy} contains coinductive
-definitions.
+The HOL distribution contains many other inductive definitions. Simple
+examples are collected on subdirectory \texttt{Induct}. The theory {\tt
+ HOL/Induct/LList.thy} contains coinductive definitions. Larger examples may
+be found on other subdirectories, such as {\tt IMP}, {\tt Lambda} and {\tt
+ Auth}.
\index{*coinductive|)} \index{*inductive|)}
@@ -2027,7 +2018,8 @@
Directory {\tt HOL/IMP} contains a formalization of various denotational,
operational and axiomatic semantics of a simple while-language, the necessary
-equivalence proofs, soundness and completeness of the Hoare rules w.r.t.\ the
+equivalence proofs, soundness and completeness of the Hoare rules with respect
+to the
denotational semantics, and soundness and completeness of a verification
condition generator. Much of development is taken from
Winskel~\cite{winskel93}. For details see~\cite{nipkow-IMP}.
@@ -2048,8 +2040,44 @@
mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
theory~\cite{mw81}.
+Directory {\tt HOL/Induct} presents simple examples of (co)inductive
+definitions.
+\begin{itemize}
+\item Theory {\tt PropLog} proves the soundness and completeness of
+ classical propositional logic, given a truth table semantics. The only
+ connective is $\imp$. A Hilbert-style axiom system is specified, and its
+ set of theorems defined inductively. A similar proof in \ZF{} is
+ described elsewhere~\cite{paulson-set-II}.
+
+\item Theory {\tt Term} develops an experimental recursive type definition;
+ the recursion goes through the type constructor~\tydx{list}.
+
+\item Theory {\tt Simult} constructs mutually recursive sets of trees and
+ forests, including induction and recursion rules.
+
+\item The definition of lazy lists demonstrates methods for handling
+ infinite data structures and coinduction in higher-order
+ logic~\cite{paulson-coind}.%
+\footnote{To be precise, these lists are \emph{potentially infinite} rather
+ than lazy. Lazy implies a particular operational semantics.}
+ Theory \thydx{LList} defines an operator for
+ corecursion on lazy lists, which is used to define a few simple functions
+ such as map and append. A coinduction principle is defined
+ for proving equations on lazy lists.
+
+\item Theory \thydx{LFilter} defines the filter functional for lazy lists.
+ This functional is notoriously difficult to define because finding the next
+ element meeting the predicate requires possibly unlimited search. It is not
+ computable, but can be expressed using a combination of induction and
+ corecursion.
+
+\item Theory \thydx{Exp} illustrates the use of iterated inductive definitions
+ to express a programming language semantics that appears to require mutual
+ induction. Iterated induction allows greater modularity.
+\end{itemize}
+
Directory {\tt HOL/ex} contains other examples and experimental proofs in
-{\HOL}. Here is an overview of the more interesting files.
+{\HOL}.
\begin{itemize}
\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
predicate calculus theorems, ranging from simple tautologies to
@@ -2067,27 +2095,6 @@
\item File {\tt set.ML} proves Cantor's Theorem, which is presented in
\S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
-\item The definition of lazy lists demonstrates methods for handling
- infinite data structures and coinduction in higher-order
- logic~\cite{paulson-coind}. Theory \thydx{LList} defines an operator for
- corecursion on lazy lists, which is used to define a few simple functions
- such as map and append. Corecursion cannot easily define operations such
- as filter, which can compute indefinitely before yielding the next
- element (if any!) of the lazy list. A coinduction principle is defined
- for proving equations on lazy lists.
-
-\item Theory {\tt PropLog} proves the soundness and completeness of
- classical propositional logic, given a truth table semantics. The only
- connective is $\imp$. A Hilbert-style axiom system is specified, and its
- set of theorems defined inductively. A similar proof in \ZF{} is
- described elsewhere~\cite{paulson-set-II}.
-
-\item Theory {\tt Term} develops an experimental recursive type definition;
- the recursion goes through the type constructor~\tydx{list}.
-
-\item Theory {\tt Simult} constructs mutually recursive sets of trees and
- forests, including induction and recursion rules.
-
\item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
Milner and Tofte's coinduction example~\cite{milner-coind}. This
substantial proof concerns the soundness of a type system for a simple