--- a/doc-src/Ref/simplifier.tex Fri Jul 21 16:35:12 2000 +0200
+++ b/doc-src/Ref/simplifier.tex Fri Jul 21 17:41:59 2000 +0200
@@ -342,7 +342,7 @@
Internally, all rewrite rules are translated into meta-equalities,
theorems with conclusion $lhs \equiv rhs$. Each simpset contains a
function for extracting equalities from arbitrary theorems. For
-example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
+example, $\lnot(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
\equiv False$. This function can be installed using
\ttindex{setmksimps} but only the definer of a logic should need to do
this; see \S\ref{sec:setmksimps}. The function processes theorems
@@ -487,7 +487,7 @@
The congruence rule for conditional expressions can supply contextual
information for simplifying the arms:
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
- \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
+ \lnot\Var{q} \Imp \Var{b}=\Var{d}} \Imp
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
\]
A congruence rule can also {\em prevent\/} simplification of some arguments.
@@ -570,7 +570,9 @@
the simplification process is not allowed to instantiate unknowns
within the goal, simplification starts with the safe solver, but may
still apply the ordinary unsafe one in nested simplifications for
-conditional rules or congruences.
+conditional rules or congruences. Note that in this way the overall
+tactic is not totally safe: it may instantiate unknowns that appear also
+in other subgoals.
\begin{ttdescription}
\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
@@ -617,8 +619,8 @@
It may even happen that due to simplification the subgoal is no longer
an equality. For example $False \bimp \Var{Q}$ could be rewritten to
-$\neg\Var{Q}$. To cover this case, the solver could try resolving
-with the theorem $\neg False$.
+$\lnot\Var{Q}$. To cover this case, the solver could try resolving
+with the theorem $\lnot False$.
\medskip
@@ -646,7 +648,7 @@
of the subgoals generated by the looper is attacked in turn, in
reverse order.
-A typical looper is case splitting: the expansion of a conditional.
+A typical looper is \index{case splitting}: the expansion of a conditional.
Another possibility is to apply an elimination rule on the
assumptions. More adventurous loopers could start an induction.
@@ -684,10 +686,10 @@
For technical reasons, there is a distinction between case splitting in the
conclusion and in the premises of a subgoal. The former is done by
-\texttt{split_tac} with rules like \texttt{split_if},
-which does not split the subgoal, while the latter is done by
-\texttt{split_asm_tac} with rules like \texttt{split_if_asm},
-which splits the subgoal.
+\texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split},
+which do not split the subgoal, while the latter is done by
+\texttt{split_asm_tac} with rules like \texttt{split_if_asm} or
+\texttt{option.split_asm}, which split the subgoal.
The operator \texttt{addsplits} automatically takes care of which tactic to
call, analyzing the form of the rules given as argument.
\begin{warn}
@@ -712,6 +714,8 @@
\section{The simplification tactics}\label{simp-tactics}
\index{simplification!tactics}\index{tactics!simplification}
\begin{ttbox}
+generic_simp_tac : bool -> bool * bool * bool ->
+ simpset -> int -> tactic
simp_tac : simpset -> int -> tactic
asm_simp_tac : simpset -> int -> tactic
full_simp_tac : simpset -> int -> tactic
@@ -719,26 +723,35 @@
safe_asm_full_simp_tac : simpset -> int -> tactic
\end{ttbox}
-These are the basic tactics that are underlying any actual
-simplification work. The rewriting strategy is always strictly bottom
-up, except for congruence rules, which are applied while descending
-into a term. Conditions in conditional rewrite rules are solved
-recursively before the rewrite rule is applied.
+\texttt{generic_simp_tac} is the basic tactic that is underlying any actual
+simplification work. The others are just instantiations of it. The rewriting
+strategy is always strictly bottom up, except for congruence rules,
+which are applied while descending into a term. Conditions in conditional
+rewrite rules are solved recursively before the rewrite rule is applied.
\begin{ttdescription}
+\item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)]
+ gives direct access to the various simplification modes:
+ \begin{itemize}
+ \item if $safe$ is {\tt true}, the safe solver is used as explained in
+ \S\ref{sec:simp-solver},
+ \item $simp\_asm$ determines whether the local assumptions are simplified,
+ \item $use\_asm$ determines whether the assumptions are used as local rewrite
+ rules, and
+ \item $mutual$ determines whether assumptions can simplify each other rather
+ than being processed from left to right.
+ \end{itemize}
+ This generic interface is intended
+ for building special tools, e.g.\ for combining the simplifier with the
+ classical reasoner. It is rarely used directly.
+
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
the basic simplification tactics that work exactly like their
namesakes in \S\ref{sec:simp-for-dummies}, except that they are
explicitly supplied with a simpset.
-\item[\ttindexbold{safe_asm_full_simp_tac}] is like
- \texttt{asm_full_simp_tac}, but uses the safe solver as explained in
- \S\ref{sec:simp-solver}. This tactic is mainly intended for
- building special tools, e.g.\ for combining the simplifier with the
- classical reasoner. It is rarely used directly.
-
\end{ttdescription}
\medskip
@@ -1159,7 +1172,7 @@
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
conclusion by~$f(a)$.
-Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
+Another example is the goal $\lnot(t=u) \imp \lnot(u=t)$.
The differing orientations make this appear difficult to prove. Ordered
rewriting with \texttt{symmetry} makes the equalities agree. (Without
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
@@ -1372,7 +1385,7 @@
The simplified rewrites must now be converted into meta-equalities. The
rule \texttt{eq_reflection} converts equality rewrites, while {\tt
iff_reflection} converts if-and-only-if rewrites. The latter possibility
-can arise in two other ways: the negative theorem~$\neg P$ is converted to
+can arise in two other ways: the negative theorem~$\lnot P$ is converted to
$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
iff_reflection_T} accomplish this conversion.
@@ -1434,7 +1447,7 @@
Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
-extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
+extend \texttt{IFOL_ss} with classical rewrite rules such as $\lnot\lnot
P\bimp P$.
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
\index{*addsimps}\index{*addcongs}