author oheimb Fri, 21 Jul 2000 17:41:59 +0200 changeset 9398 0ee9b2819155 parent 9397 358e67410253 child 9399 effc8d44c89c
--- a/doc-src/Ref/simplifier.tex	Fri Jul 21 16:35:12 2000 +0200
theorems with conclusion $lhs \equiv rhs$.  Each simpset contains a
-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}$stacf$] 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{*addsimps}\index{*addcongs}