summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/simplifier.tex

author | clasohm |

Tue, 16 Nov 1993 14:13:11 +0100 | |

changeset 122 | db9043a8e372 |

parent 104 | d8205bb279a7 |

child 133 | 2322fd6d57a1 |

permissions | -rw-r--r-- |

replaced \un by \union in "Simplification sets"

%% $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} \union \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|)}