author nipkow Mon Jul 15 12:36:56 1996 +0200 (1996-07-15) changeset 1860 71bfeecfa96c parent 1859 2ea3f7ebeccb child 1861 505b104f675a
Documented simplification tactics which make use of the implicit simpset.
     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}
`