--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/simplifier.tex Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,360 @@
+%% $Id$
+\chapter{Simplification} \label{simp-chap}
+\index{simplification|(}
+
+
+This chapter describes Isabelle's generic simplification package, which
+provides a suite of simplification tactics. This rewriting package is less
+general than its predecessor --- it works only for the equality relation,
+not arbitrary preorders --- but it is fast and flexible. It performs
+conditional and unconditional rewriting and uses contextual information
+(``local assumptions''). It provides a few general hooks, which can
+provide automatic case splits during rewriting, for example. The
+simplifier is set up for many of Isabelle's logics: {\tt FOL}, {\tt ZF},
+{\tt LCF} and {\tt HOL}.
+
+
+\section{Simplification sets}
+\index{simplification sets}
+
+The simplification tactics are controlled by {\bf simpsets}. These consist
+of five components: rewrite rules, congruence rules, the subgoaler, the
+solver and the looper. Normally, the simplifier is set up with sensible
+defaults, so that most simplifier calls specify only rewrite rules.
+Sophisticated usage of the other components can be highly effective, but
+most users should never worry about them.
+
+\subsection{Rewrite rules}\index{rewrite rules}
+
+Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +
+Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \un \Var{B}
+\equiv \{x.x\in A \disj x\in B\}$. {\bf Conditional} rewrites such as
+$\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
+can be arbitrary terms. The infix operation \ttindex{addsimps} adds new
+rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
+simpset.
+
+Theorems added via \ttindex{addsimps} need not be equalities to start with.
+Each simpset contains a (user-definable) function for extracting equalities
+from arbitrary theorems. For example $\neg(x\in \{\})$ could be turned
+into $x\in \{\} \equiv False$. This function can be set with
+\ttindex{setmksimps} but only the definer of a logic should need to do
+this. Exceptionally, one may want to install a selective version of
+\ttindex{mksimps} in order to filter out looping rewrite rules arising from
+local assumptions (see below).
+
+Internally, all rewrite rules are translated into meta-equalities:
+theorems with conclusion $lhs \equiv rhs$. To this end every simpset contains
+a function of type \verb$thm -> thm list$ to extract a list
+of meta-equalities from a given theorem.
+
+\begin{warn}\index{rewrite rules}
+ The left-hand side of a rewrite rule must look like a first-order term:
+ after eta-contraction, none of its unknowns should have arguments. Hence
+ ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall
+ x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas
+ $\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not. However, you can
+ replace the offending subterms by new variables and conditions: $\Var{y} =
+ \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again
+ acceptable.
+\end{warn}
+
+\subsection {Congruence rules}\index{congruence rules}
+Congruence rules are meta-equalities of the form
+\[ \List{\dots} \Imp
+ f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
+\]
+They control the simplification of the arguments of certain constants. For
+example, some arguments can be simplified under additional assumptions:
+\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
+ \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
+\]
+This rule assumes $Q@1$ and any rewrite rules it implies, while
+simplifying~$P@2$. Such ``local'' assumptions are effective for rewriting
+formulae such as $x=0\imp y+x=y$. The next example makes similar use of
+such contextual information in bounded quantifiers:
+\[ \List{\Var{A}=\Var{B};\; \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)}
+ \Imp (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
+\]
+This congruence rule supplies contextual information for simplifying the
+arms of a conditional expressions:
+\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
+ \neg\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 suppress simplification of certain arguments.
+Here is an alternative congruence rule for conditional expressions:
+\[ \Var{p}=\Var{q} \Imp
+ if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
+\]
+Only the first argument is simplified; the others remain unchanged.
+This can make simplification much faster, but may require an extra case split
+to prove the goal.
+
+Congruence rules are added using \ttindex{addeqcongs}. Their conclusion
+must be a meta-equality, as in the examples above. It is more
+natural to derive the rules with object-logic equality, for example
+\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
+ \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}),
+\]
+So each object-logic should provide an alternative combinator
+\ttindex{addcongs} that expects object-equalities and translates them into
+meta-equalities.
+
+\subsection{The subgoaler} \index{subgoaler}
+The subgoaler is the tactic used to solve subgoals arising out of
+conditional rewrite rules or congruence rules. The default should be
+simplification itself. Occasionally this strategy needs to be changed. For
+example, if the premise of a conditional rule is an instance of its
+conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the
+default strategy could loop.
+
+The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For
+example, the subgoaler
+\begin{ttbox}
+fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE'
+ asm_simp_tac ss;
+\end{ttbox}
+tries to solve the subgoal with one of the premises and calls
+simplification only if that fails; here {\tt prems_of_ss} extracts the
+current premises from a simpset.
+
+\subsection{The solver} \index{solver}
+The solver attempts to solve a subgoal after simplification, say by
+recognizing it as a tautology. It can be set with \ttindex{setsolver}.
+Occasionally, simplification on its own is not enough to reduce the subgoal
+to a tautology; additional means, like \verb$fast_tac$, may be necessary.
+
+\begin{warn}
+ Rewriting does not instantiate unknowns. Trying to rewrite $a\in
+ \Var{A}$ with the rule $\Var{x}\in \{\Var{x}\}$ leads nowhere. The
+ solver, however, is an arbitrary tactic and may instantiate unknowns as
+ it pleases. This is the only way the simplifier can handle a conditional
+ rewrite rule whose condition contains extra variables.
+\end{warn}
+
+\begin{warn}
+ If you want to supply your own subgoaler or solver, read on. The subgoaler
+ is also used to solve the premises of congruence rules, which are usually
+ of the form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
+ needs to be instantiated with the result. Hence the subgoaler should call
+ the simplifier at some point. The simplifier will then call the solver,
+ which must therefore be prepared to solve goals of the form $t = \Var{x}$,
+ usually by reflexivity. In particular, reflexivity should be tried before
+ any of the fancy tactics like {\tt fast_tac}. 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}$, in which case the
+ solver must also try resolving with the theorem $\neg False$.
+
+ If the simplifier aborts with the message {\tt Failed congruence proof!},
+ it is due to the subgoaler or solver who failed to prove a premise of a
+ congruence rule.
+\end{warn}
+
+\subsection{The looper} \index{looper}
+The looper is a tactic that is applied after simplification, in case the
+solver failed to solve the simplified goal. If the looper succeeds, the
+simplification process is started all over again. Each 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. Another
+possibility is to apply an elimination rule on the assumptions. More
+adventurous loopers could start an induction. The looper is set with
+\ttindex{setloop}.
+
+
+\begin{figure}
+\indexbold{*SIMPLIFIER}
+\begin{ttbox}
+infix addsimps addeqcongs delsimps
+ setsubgoaler setsolver setloop setmksimps;
+
+signature SIMPLIFIER =
+sig
+ type simpset
+ val simp_tac: simpset -> int -> tactic
+ val asm_simp_tac: simpset -> int -> tactic
+ val asm_full_simp_tac: simpset -> int -> tactic
+ val addeqcongs: simpset * thm list -> simpset
+ val addsimps: simpset * thm list -> simpset
+ val delsimps: simpset * thm list -> simpset
+ val empty_ss: simpset
+ val merge_ss: simpset * simpset -> simpset
+ val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
+ val setsolver: simpset * (thm list -> int -> tactic) -> simpset
+ val setloop: simpset * (int -> tactic) -> simpset
+ val setmksimps: simpset * (thm -> thm list) -> simpset
+ val prems_of_ss: simpset -> thm list
+ val rep_ss: simpset -> \{simps: thm list, congs: thm list\}
+end;
+\end{ttbox}
+\caption{The signature \ttindex{SIMPLIFIER}} \label{SIMPLIFIER}
+\end{figure}
+
+
+\section{The simplification tactics} \label{simp-tactics}
+\index{simplification!tactics|bold}
+\index{tactics!simplification|bold}
+
+The actual simplification work is performed by the following tactics. The
+rewriting strategy is 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.
+
+There are three basic simplification tactics:
+\begin{description}
+\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules
+ in~$ss$. It may solve the subgoal completely if it has become trivial,
+ using the solver.
+
+\item[\ttindexbold{asm_simp_tac}] is like \verb$simp_tac$, but also uses
+ assumptions as additional rewrite rules.
+
+\item[\ttindexbold{asm_full_simp_tac}] is like \verb$asm_simp_tac$, but also
+ simplifies the assumptions one by one, using each assumption in the
+ simplification of the following ones.
+\end{description}
+Using the simplifier effectively may take a bit of experimentation. The
+tactics can be traced with the ML command \verb$trace_simp := true$. To
+remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
+return its simplification and congruence rules.
+
+\section{Example: using the simplifier}
+\index{simplification!example}
+Assume we are working within {\tt FOL} and that
+\begin{description}
+\item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
+\item[\tt add_0] is the rewrite rule $0+n = n$,
+\item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
+\item[\tt induct] is the induction rule
+$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
+\item[\tt FOL_ss] is a basic simpset for {\tt FOL}.\footnote
+{These examples reside on the file {\tt FOL/ex/nat.ML}.}
+\end{description}
+
+We create a simpset for natural numbers by extending~{\tt FOL_ss}:
+\begin{ttbox}
+val add_ss = FOL_ss addsimps [add_0, add_Suc];
+\end{ttbox}
+Proofs by induction typically involve simplification:
+\begin{ttbox}
+goal Nat.thy "m+0 = m";
+{\out Level 0}
+{\out m + 0 = m}
+{\out 1. m + 0 = m}
+\ttbreak
+by (res_inst_tac [("n","m")] induct 1);
+{\out Level 1}
+{\out m + 0 = m}
+{\out 1. 0 + 0 = 0}
+{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
+\end{ttbox}
+Simplification solves the first subgoal:
+\begin{ttbox}
+by (simp_tac add_ss 1);
+{\out Level 2}
+{\out m + 0 = m}
+{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
+\end{ttbox}
+The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the
+induction hypothesis as a rewrite rule:
+\begin{ttbox}
+by (asm_simp_tac add_ss 1);
+{\out Level 3}
+{\out m + 0 = m}
+{\out No subgoals!}
+\end{ttbox}
+
+\medskip
+The next proof is similar.
+\begin{ttbox}
+goal Nat.thy "m+Suc(n) = Suc(m+n)";
+{\out Level 0}
+{\out m + Suc(n) = Suc(m + n)}
+{\out 1. m + Suc(n) = Suc(m + n)}
+\ttbreak
+by (res_inst_tac [("n","m")] induct 1);
+{\out Level 1}
+{\out m + Suc(n) = Suc(m + n)}
+{\out 1. 0 + Suc(n) = Suc(0 + n)}
+{\out 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
+\ttbreak
+by (simp_tac add_ss 1);
+{\out Level 2}
+{\out m + Suc(n) = Suc(m + n)}
+{\out 1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
+\end{ttbox}
+Switching tracing on illustrates how the simplifier solves the remaining
+subgoal:
+\begin{ttbox}
+trace_simp := true;
+by (asm_simp_tac add_ss 1);
+{\out Rewriting:}
+{\out Suc(x) + Suc(n) == Suc(x + Suc(n))}
+{\out Rewriting:}
+{\out x + Suc(n) == Suc(x + n)}
+{\out Rewriting:}
+{\out Suc(x) + n == Suc(x + n)}
+{\out Rewriting:}
+{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True}
+{\out Level 3}
+{\out m + Suc(n) = Suc(m + n)}
+{\out No subgoals!}
+\end{ttbox}
+As usual, many variations are possible. At Level~1 we could have solved
+both subgoals at once using the tactical \ttindex{ALLGOALS}:
+\begin{ttbox}
+by (ALLGOALS (asm_simp_tac add_ss));
+{\out Level 2}
+{\out m + Suc(n) = Suc(m + n)}
+{\out No subgoals!}
+\end{ttbox}
+
+\medskip
+Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
+the law $f(Suc(n)) = Suc(f(n))$:\footnote{The previous
+ simplifier required congruence rules for such function variables in
+ order to simplify their arguments. The present simplifier can be given
+ congruence rules to realize non-standard simplification of a function's
+ arguments, but this is seldom necessary.}
+\begin{ttbox}
+val [prem] = goal Nat.thy
+ "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
+{\out Level 0}
+{\out f(i + j) = i + f(j)}
+{\out 1. f(i + j) = i + f(j)}
+{\out val prem = "f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
+\ttbreak
+by (res_inst_tac [("n","i")] induct 1);
+{\out Level 1}
+{\out f(i + j) = i + f(j)}
+{\out 1. f(0 + j) = 0 + f(j)}
+{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
+\end{ttbox}
+We simplify each subgoal in turn. The first one is trivial:
+\begin{ttbox}
+by (simp_tac add_ss 1);
+{\out Level 2}
+{\out f(i + j) = i + f(j)}
+{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
+\end{ttbox}
+The remaining subgoal requires rewriting by the premise, so we add it to
+{\tt add_ss}:
+\begin{ttbox}
+by (asm_simp_tac (add_ss addsimps [prem]) 1);
+{\out Level 3}
+{\out f(i + j) = i + f(j)}
+{\out No subgoals!}
+\end{ttbox}
+
+No documentation is available on setting up the simplifier for new logics.
+Please consult {\tt FOL/simpdata.ML} to see how this is done, and {\tt
+ FOL/simpdata.ML} for a fairly sophisticated translation of formulae into
+rewrite rules.
+
+%%\section{Setting up the simplifier} \label{SimpFun-input}
+%%Should be written!
+
+
+\index{simplification|)}
+