summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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