# HG changeset patch # User oheimb # Date 964194119 -7200 # Node ID 0ee9b281915564c947ed24e249a49deffc7b5947 # Parent 358e6741025324edf408152cf64900d70d67fc42 removed safe_asm_full_simp_tac, added generic_simp_tac diff -r 358e67410253 -r 0ee9b2819155 doc-src/Ref/simplifier.tex --- 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}