doc-src/Ref/simplifier.tex
changeset 1860 71bfeecfa96c
parent 1387 9bcad9c22fd4
child 2020 586f3c075b05
     1.1 --- a/doc-src/Ref/simplifier.tex	Mon Jul 15 10:41:30 1996 +0200
     1.2 +++ b/doc-src/Ref/simplifier.tex	Mon Jul 15 12:36:56 1996 +0200
     1.3 @@ -7,8 +7,122 @@
     1.4  unconditional rewriting and uses contextual information (`local
     1.5  assumptions').  It provides a few general hooks, which can provide
     1.6  automatic case splits during rewriting, for example.  The simplifier is set
     1.7 -up for many of Isabelle's logics: {\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt
     1.8 -  HOL}.
     1.9 +up for many of Isabelle's logics: \FOL, \ZF, \HOL\ and \HOLCF.
    1.10 +
    1.11 +The next section is a quick introduction to the simplifier, the later
    1.12 +sections explain advanced features.
    1.13 +
    1.14 +\section{Simplification for dummies}
    1.15 +\label{sec:simp-for-dummies}
    1.16 +
    1.17 +In some logics (e.g.\ \HOL), the simplifier is particularly easy to
    1.18 +use because it supports the concept of a {\em current set of simplification
    1.19 +  rules}, also called the {\em current simpset}\index{simpset!current}. All
    1.20 +commands are interpreted relative to the current simpset. For example, in the
    1.21 +theory of arithmetic the goal
    1.22 +\begin{ttbox}
    1.23 +{\out  1. 0 + (x + 0) = x + 0 + 0}
    1.24 +\end{ttbox}
    1.25 +can be solved by a single
    1.26 +\begin{ttbox}
    1.27 +by(Simp_tac 1);
    1.28 +\end{ttbox}
    1.29 +The simplifier uses the current simpset, which in the case of arithmetic
    1.30 +contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} =
    1.31 +\Var{n}$.
    1.32 +
    1.33 +If assumptions of the subgoal are also needed in the simplification
    1.34 +process, as in
    1.35 +\begin{ttbox}
    1.36 +{\out  1. x = 0 ==> x + x = 0}
    1.37 +\end{ttbox}
    1.38 +then there is the more powerful
    1.39 +\begin{ttbox}
    1.40 +by(Asm_simp_tac 1);
    1.41 +\end{ttbox}
    1.42 +which solves the above goal.
    1.43 +
    1.44 +There are four basic simplification tactics:
    1.45 +\begin{ttdescription}
    1.46 +\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the current
    1.47 +  simpset.  It may solve the subgoal completely if it has become trivial,
    1.48 +  using the solver.
    1.49 +  
    1.50 +\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification}
    1.51 +  is like \verb$Simp_tac$, but extracts additional rewrite rules from the
    1.52 +  assumptions.
    1.53 +
    1.54 +\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also
    1.55 +  simplifies the assumptions (but without using the assumptions to simplify
    1.56 +  each other or the actual goal.)
    1.57 +
    1.58 +\item[\ttindexbold{Asm_full_simp_tac}]
    1.59 +  is like \verb$Asm_simp_tac$, but also simplifies the assumptions one by
    1.60 +  one.  {\em Working from left to right, it uses each assumption in the
    1.61 +  simplification of those following.}
    1.62 +\end{ttdescription}
    1.63 +
    1.64 +{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also
    1.65 +loop where some of the others terminate. For example,
    1.66 +\begin{ttbox}
    1.67 +{\out  1. ALL x. f(x) = g(f(g(x))) ==> f(0) = f(0)+0}
    1.68 +\end{ttbox}
    1.69 +is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt Asm_simp_tac}
    1.70 +loop because the rewrite rule $f(\Var{x}) = f(g(f(\Var{x})))$ extracted from
    1.71 +the assumption does not terminate. Isabelle notices certain simple forms of
    1.72 +nontermination, but not this one.
    1.73 + 
    1.74 +\begin{warn}
    1.75 +  Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes
    1.76 +misses opportunities for simplification: given the subgoal
    1.77 +\begin{ttbox}
    1.78 +{\out [| P(f(a)); f(a) = t |] ==> ...}
    1.79 +\end{ttbox}
    1.80 +\verb$Asm_full_simp_tac$ will not simplify the first assumption using the
    1.81 +second but will leave the assumptions unchanged. See
    1.82 +\S\ref{sec:reordering-asms} for ways around this problem.
    1.83 +\end{warn}
    1.84 +
    1.85 +Using the simplifier effectively may take a bit of experimentation.  The
    1.86 +tactics can be traced with the ML command \verb$trace_simp := true$.
    1.87 +
    1.88 +There is not just one global current simpset, but one associated with each
    1.89 +theory as well. How are these simpset built up?
    1.90 +\begin{enumerate}
    1.91 +\item When loading {\tt T.thy}, the current simpset is initialized with the
    1.92 +  union of the simpsets associated with all the ancestors of {\tt T}. In
    1.93 +  addition, certain constructs in {\tt T} may add new rules to the simpset,
    1.94 +  e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL. Definitions are not
    1.95 +  added automatically!
    1.96 +\item The script in {\tt T.ML} may manipulate the current simpset further by
    1.97 +  explicitly adding/deleting theorems to/from it (see below).
    1.98 +\item After {\tt T.ML} has been read, the current simpset is associated with
    1.99 +  theory {\tt T}.
   1.100 +\end{enumerate}
   1.101 +The current simpset is manipulated by
   1.102 +\begin{ttbox}
   1.103 +Addsimps, Delsimps: thm list -> unit
   1.104 +\end{ttbox}
   1.105 +\begin{ttdescription}
   1.106 +\item[\ttindexbold{Addsimps} $thms$] adds $thms$ to the current simpset
   1.107 +\item[\ttindexbold{Delsimps} $thms$] deletes $thms$ from the current simpset
   1.108 +\end{ttdescription}
   1.109 +
   1.110 +Generally useful simplification rules $\Var{n}+0 = \Var{n}$ should be added
   1.111 +to the current simpset right after they have been proved. Those of a more
   1.112 +specific nature (e.g.\ the laws of de~Morgan, which alter the structure of a
   1.113 +formula) should only be added for specific proofs and deleted again
   1.114 +afterwards. Conversely, it may also happen that a generally useful rule needs
   1.115 +to be removed for a certain proof and is added again afterwards.  Well
   1.116 +designed simpsets need few temporary additions or deletions.
   1.117 +
   1.118 +\begin{warn}
   1.119 +  If you execute proofs interactively, or load them from an ML file without
   1.120 +  associated {\tt .thy} file, you must set the current simpset by calling
   1.121 +  \ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the
   1.122 +  theory you want to work in. If you have just loaded $T$, this is not
   1.123 +  necessary.
   1.124 +\end{warn}
   1.125  
   1.126  
   1.127  \section{Simplification sets}\index{simplification sets} 
   1.128 @@ -18,6 +132,10 @@
   1.129  defaults so that most simplifier calls specify only rewrite rules.
   1.130  Experienced users can exploit the other components to streamline proofs.
   1.131  
   1.132 +Logics like \HOL, which support a current simpset\index{simpset!current},
   1.133 +store its value in an ML reference variable usually called {\tt
   1.134 +  simpset}\index{simpset@{\tt simpset} ML value}. It can be accessed via
   1.135 +{\tt!simpset} and updated via {\tt simpset := \dots}.
   1.136  
   1.137  \subsection{Rewrite rules}
   1.138  \index{rewrite rules|(}
   1.139 @@ -27,10 +145,8 @@
   1.140    \Var{P}\conj\Var{P}    &\bimp&  \Var{P} \\
   1.141    \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
   1.142  \end{eqnarray*}
   1.143 -{\bf Conditional} rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
   1.144 -0$ are permitted; the conditions can be arbitrary terms.  The infix
   1.145 -operation \ttindex{addsimps} adds new rewrite rules, while
   1.146 -\ttindex{delsimps} deletes rewrite rules from a simpset.
   1.147 +Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
   1.148 +0$ are permitted; the conditions can be arbitrary terms.
   1.149  
   1.150  Internally, all rewrite rules are translated into meta-equalities, theorems
   1.151  with conclusion $lhs \equiv rhs$.  Each simpset contains a function for
   1.152 @@ -212,6 +328,7 @@
   1.153    type simpset
   1.154    val simp_tac:          simpset -> int -> tactic
   1.155    val asm_simp_tac:      simpset -> int -> tactic
   1.156 +  val full_simp_tac:     simpset -> int -> tactic
   1.157    val asm_full_simp_tac: simpset -> int -> tactic\smallskip
   1.158    val addeqcongs:   simpset * thm list -> simpset
   1.159    val addsimps:     simpset * thm list -> simpset
   1.160 @@ -230,43 +347,52 @@
   1.161  \end{figure}
   1.162  
   1.163  
   1.164 -\section{The simplification tactics} \label{simp-tactics}
   1.165 +\section{The simplification tactics}
   1.166 +\label{simp-tactics}
   1.167  \index{simplification!tactics}
   1.168  \index{tactics!simplification}
   1.169  
   1.170 -The actual simplification work is performed by the following tactics.  The
   1.171 -rewriting strategy is strictly bottom up, except for congruence rules, which
   1.172 -are applied while descending into a term.  Conditions in conditional rewrite
   1.173 -rules are solved recursively before the rewrite rule is applied.
   1.174 +The actual simplification work is performed by the following basic tactics:
   1.175 +\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
   1.176 +\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}. They work
   1.177 +exactly like their namesakes in \S\ref{sec:simp-for-dummies}, except that
   1.178 +they are explicitly supplied with a simpset. This is because the ones in
   1.179 +\S\ref{sec:simp-for-dummies} are defined in terms of the ones above, e.g.
   1.180 +\begin{ttbox}
   1.181 +fun Simp_tac i = simp_tac (!simpset) i;
   1.182 +\end{ttbox}
   1.183 +where \ttindex{!simpset} is the current simpset\index{simpset!current}.
   1.184  
   1.185 -There are three basic simplification tactics:
   1.186 -\begin{ttdescription}
   1.187 -\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules
   1.188 -  in~$ss$.  It may solve the subgoal completely if it has become trivial,
   1.189 -  using the solver.
   1.190 -  
   1.191 -\item[\ttindexbold{asm_simp_tac}]\index{assumptions!in simplification}
   1.192 -  is like \verb$simp_tac$, but extracts additional rewrite rules from the
   1.193 -  assumptions.
   1.194 +The rewriting strategy of all four tactics is strictly bottom up, except for
   1.195 +congruence rules, which are applied while descending into a term.  Conditions
   1.196 +in conditional rewrite rules are solved recursively before the rewrite rule
   1.197 +is applied.
   1.198  
   1.199 -\item[\ttindexbold{asm_full_simp_tac}] 
   1.200 -  is like \verb$asm_simp_tac$, but also simplifies the assumptions one by
   1.201 -  one.  Working from left to right, it uses each assumption in the
   1.202 -  simplification of those following.
   1.203 -\end{ttdescription}
   1.204 -\begin{warn}
   1.205 -  Since \verb$asm_full_simp_tac$ works from left to right, it sometimes
   1.206 -misses opportunities for simplification: given the subgoal
   1.207 +The infix operations \ttindex{addsimps}/\ttindex{delsimps} add/delete rewrite
   1.208 +rules to/from a simpset. They are used to implement \ttindex{Addsimps} and
   1.209 +\ttindex{Delsimps}, e.g.
   1.210 +\begin{ttbox}
   1.211 +fun Addsimps thms = (simpset := (!simpset addsimps thms));
   1.212 +\end{ttbox}
   1.213 +and can also be used directly, even in the presence of a current simpset. For
   1.214 +example
   1.215  \begin{ttbox}
   1.216 -{\out [| P(f(a)); f(a) = t |] ==> ...}
   1.217 +Addsimps \(thms\);
   1.218 +by(Simp_tac \(i\));
   1.219 +Delsimps \(thms\);
   1.220 +\end{ttbox}
   1.221 +can be compressed into
   1.222 +\begin{ttbox}
   1.223 +by(simp_tac (!simpset addsimps \(thms\)) \(i\));
   1.224  \end{ttbox}
   1.225 -\verb$asm_full_simp_tac$ will not simplify the first assumption using the
   1.226 -second but will leave the assumptions unchanged. See
   1.227 -\S\ref{sec:reordering-asms} for ways around this problem.
   1.228 -\end{warn}
   1.229 -Using the simplifier effectively may take a bit of experimentation.  The
   1.230 -tactics can be traced with the ML command \verb$trace_simp := true$.  To
   1.231 -remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
   1.232 +
   1.233 +The simpset associated with a particular theory can be retrieved via the name
   1.234 +of the theory using the function
   1.235 +\begin{ttbox}
   1.236 +simpset_of: string -> simpset
   1.237 +\end{ttbox}\index{*simpset_of}
   1.238 +
   1.239 +To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
   1.240  return its simplification and congruence rules.
   1.241  
   1.242  \section{Examples using the simplifier}