author paulson Tue, 07 Jan 1997 10:17:07 +0100 changeset 2479 57109c1a653d parent 2478 adbd622bb375 child 2480 f9be937df511
Updated account of implicit simpsets and clasets
 doc-src/Ref/classical.tex file | annotate | diff | comparison | revisions doc-src/Ref/simplifier.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/classical.tex	Tue Jan 07 09:06:01 1997 +0100
+++ b/doc-src/Ref/classical.tex	Tue Jan 07 10:17:07 1997 +0100
@@ -28,10 +28,18 @@
be traced, and their components can be called directly; in this manner,
any proof can be viewed interactively.

-We shall first discuss the underlying principles, then consider how to use
-the classical reasoner.  Finally, we shall see how to instantiate it for
-new logics.  The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already
-installed.
+The simplest way to apply the classical reasoner (to subgoal~$i$) is as
+follows:
+\begin{ttbox}
+by (Fast_tac $$i$$);
+\end{ttbox}
+If the subgoal is a simple formula of the predicate calculus or set theory,
+then it should be proved quickly.  However, to use the classical reasoner
+effectively, you need to know how it works.
+
+We shall first discuss the underlying principles, then present the classical
+reasoner.  Finally, we shall see how to instantiate it for new logics.  The
+logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already installed.

\section{The sequent calculus}
@@ -397,12 +405,12 @@
\end{ttdescription}

\subsection{The current claset}
-Some logics (e.g.\ \HOL) support the concept of a {\em current set of
-classical rules}\index{claset!current}.
-The underlying idea is quite similar to that of a current simpset described
-in \S\ref{sec:simp-for-dummies}.
-Just like simpsets, clasets can be associated with theories.
-The tactics
+Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
+claset\index{claset!current}.  This is a default set of classical rules.  The
+underlying idea is quite similar to that of a current simpset described in
+\S\ref{sec:simp-for-dummies}; please read that section, including its
+warnings.  Just like simpsets, clasets can be associated with theories.  The
+tactics
\begin{ttbox}
Step_tac     : int -> tactic
Fast_tac     : int -> tactic
--- a/doc-src/Ref/simplifier.tex	Tue Jan 07 09:06:01 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Tue Jan 07 10:17:07 1997 +0100
@@ -15,17 +15,17 @@
\section{Simplification for dummies}
\label{sec:simp-for-dummies}

-In some logics (e.g.\ \HOL), the simplifier is particularly easy to
-use because it supports the concept of a {\em current set of simplification
-  rules}, also called the {\em current simpset}\index{simpset!current}. All
-commands are interpreted relative to the current simpset. For example, in the
-theory of arithmetic the goal
+In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to
+use because it supports the concept of a {\em current
+  simpset}\index{simpset!current}.  This is a default set of simplification
+rules.  All commands are interpreted relative to the current simpset.  For
+example, in the theory of arithmetic the goal
\begin{ttbox}
{\out  1. 0 + (x + 0) = x + 0 + 0}
\end{ttbox}
can be solved by a single
\begin{ttbox}
-by(Simp_tac 1);
+by (Simp_tac 1);
\end{ttbox}
The simplifier uses the current simpset, which in the case of arithmetic
contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = @@ -38,7 +38,7 @@ \end{ttbox} then there is the more powerful \begin{ttbox} -by(Asm_simp_tac 1); +by (Asm_simp_tac 1); \end{ttbox} which solves the above goal. @@ -117,6 +117,18 @@ designed simpsets need few temporary additions or deletions. \begin{warn} + The union of the ancestor simpsets (as described above) is not always a good + simpset for the new theory. If some ancestors have deleted simplification + rules because they are no longer wanted, while others have left those rules + in, then the union will contain the unwanted rules. If the ancestor + simpsets differ in other components (the subgoaler, solver, looper or rule + preprocessor: see below), then you cannot be sure which version of that + component will be inherited. You may have to set the component explicitly + for the new theory's simpset by an assignment of the form + {\tt simpset := \dots}. +\end{warn} + +\begin{warn} If you execute proofs interactively, or load them from an ML file without associated {\tt .thy} file, you must set the current simpset by calling \ttindex{set_current_thy}~{\tt"}$T${\tt"}, where$T\$ is the name of the
@@ -378,12 +390,12 @@
example
\begin{ttbox}
Addsimps $$thms$$;
-by(Simp_tac $$i$$);
+by (Simp_tac $$i$$);
Delsimps $$thms$$;
\end{ttbox}
can be compressed into
\begin{ttbox}
-by(simp_tac (!simpset addsimps $$thms$$) $$i$$);
+by (simp_tac (!simpset addsimps $$thms$$) $$i$$);
\end{ttbox}

The simpset associated with a particular theory can be retrieved via the name