author | wenzelm |
Wed, 31 Dec 1997 15:17:49 +0100 | |
changeset 4504 | 2f39aa4bebf3 |
parent 4395 | a2b726277050 |
child 4557 | 03003b966e91 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
3950 | 2 |
\chapter{Simplification} |
3 |
\label{chap:simplification} |
|
104 | 4 |
\index{simplification|(} |
5 |
||
4395 | 6 |
This chapter describes Isabelle's generic simplification package. It |
7 |
performs conditional and unconditional rewriting and uses contextual |
|
8 |
information (`local assumptions'). It provides several general hooks, |
|
9 |
which can provide automatic case splits during rewriting, for example. |
|
10 |
The simplifier is already set up for many of Isabelle's logics: \FOL, |
|
11 |
\ZF, \HOL, \HOLCF. |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
12 |
|
4395 | 13 |
The first section is a quick introduction to the simplifier that |
14 |
should be sufficient to get started. The later sections explain more |
|
15 |
advanced features. |
|
16 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
17 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
18 |
\section{Simplification for dummies} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
19 |
\label{sec:simp-for-dummies} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
20 |
|
4395 | 21 |
Basic use of the simplifier is particularly easy because each theory |
22 |
is equipped with an implicit {\em current |
|
23 |
simpset}\index{simpset!current}. This provides sensible default |
|
24 |
information in many cases. A suite of commands refer to the implicit |
|
25 |
simpset of the current theory context. |
|
26 |
||
27 |
\begin{warn} |
|
28 |
Make sure that you are working within the correct theory context. |
|
29 |
Executing proofs interactively, or loading them from ML files |
|
30 |
without associated theories may require setting the current theory |
|
31 |
manually via the \ttindex{context} command. |
|
32 |
\end{warn} |
|
33 |
||
34 |
\subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs} |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
35 |
\begin{ttbox} |
4395 | 36 |
Simp_tac : int -> tactic |
37 |
Asm_simp_tac : int -> tactic |
|
38 |
Full_simp_tac : int -> tactic |
|
39 |
Asm_full_simp_tac : int -> tactic |
|
40 |
trace_simp : bool ref \hfill{\bf initially false} |
|
41 |
\end{ttbox} |
|
42 |
||
43 |
\begin{ttdescription} |
|
44 |
\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the |
|
45 |
current simpset. It may solve the subgoal completely if it has |
|
46 |
become trivial, using the simpset's solver tactic. |
|
47 |
||
48 |
\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification} |
|
49 |
is like \verb$Simp_tac$, but extracts additional rewrite rules from |
|
50 |
the local assumptions. |
|
51 |
||
52 |
\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also |
|
53 |
simplifies the assumptions (without using the assumptions to |
|
54 |
simplify each other or the actual goal). |
|
55 |
||
56 |
\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, |
|
57 |
but also simplifies the assumptions one by one. Working from |
|
58 |
\emph{left to right}, it uses each assumption in the simplification |
|
59 |
of those following. |
|
60 |
||
61 |
\item[set \ttindexbold{trace_simp};] makes the simplifier output |
|
62 |
internal operations. This includes rewrite steps, but also |
|
63 |
bookkeeping like modifications of the simpset. |
|
64 |
\end{ttdescription} |
|
65 |
||
66 |
\medskip |
|
67 |
||
68 |
As an example, consider the theory of arithmetic in \HOL. The (rather |
|
69 |
trivial) goal $0 + (x + 0) = x + 0 + 0$ can be solved by a single call |
|
70 |
of \texttt{Simp_tac} as follows: |
|
71 |
\begin{ttbox} |
|
72 |
context Arith.thy; |
|
73 |
goal Arith.thy "0 + (x + 0) = x + 0 + 0"; |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
74 |
{\out 1. 0 + (x + 0) = x + 0 + 0} |
4395 | 75 |
by (Simp_tac 1); |
76 |
{\out Level 1} |
|
77 |
{\out 0 + (x + 0) = x + 0 + 0} |
|
78 |
{\out No subgoals!} |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
79 |
\end{ttbox} |
4395 | 80 |
|
81 |
The simplifier uses the current simpset of \texttt{Arith.thy}, which |
|
82 |
contains suitable theorems like $\Var{n}+0 = \Var{n}$ and $0+\Var{n} = |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
83 |
\Var{n}$. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
84 |
|
4395 | 85 |
\medskip In many cases, assumptions of a subgoal are also needed in |
86 |
the simplification process. For example, \texttt{x = 0 ==> x + x = 0} |
|
87 |
is solved by \texttt{Asm_simp_tac} as follows: |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
88 |
\begin{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
89 |
{\out 1. x = 0 ==> x + x = 0} |
2479 | 90 |
by (Asm_simp_tac 1); |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
91 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
92 |
|
4395 | 93 |
\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet |
94 |
of tactics but may also loop where some of the others terminate. For |
|
95 |
example, |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
96 |
\begin{ttbox} |
4395 | 97 |
{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
98 |
\end{ttbox} |
4395 | 99 |
is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt |
100 |
Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} = |
|
101 |
g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not |
|
102 |
terminate. Isabelle notices certain simple forms of nontermination, |
|
103 |
but not this one. |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
104 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
105 |
\begin{warn} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
106 |
Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
107 |
misses opportunities for simplification: given the subgoal |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
108 |
\begin{ttbox} |
4395 | 109 |
{\out [| P (f a); f a = t |] ==> \dots} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
110 |
\end{ttbox} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
111 |
\verb$Asm_full_simp_tac$ will not simplify the first assumption using the |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset
|
112 |
second but will leave the assumptions unchanged. See |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
113 |
\S\ref{sec:reordering-asms} for ways around this problem. |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
114 |
\end{warn} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
115 |
|
4395 | 116 |
\medskip |
117 |
||
3108 | 118 |
Using the simplifier effectively may take a bit of experimentation. |
4395 | 119 |
Set the \verb$trace_simp$\index{tracing!of simplification} flag to get |
120 |
a better idea of what is going on. The resulting output can be |
|
121 |
enormous, especially since invocations of the simplifier are often |
|
122 |
nested (e.g.\ when solving conditions of rewrite rules). |
|
123 |
||
124 |
||
125 |
\subsection{Modifying the current simpset} |
|
126 |
\begin{ttbox} |
|
127 |
Addsimps : thm list -> unit |
|
128 |
Delsimps : thm list -> unit |
|
129 |
Addsimprocs : simproc list -> unit |
|
130 |
Delsimprocs : simproc list -> unit |
|
131 |
Addcongs : thm list -> unit |
|
132 |
Delcongs : thm list -> unit |
|
133 |
\end{ttbox} |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
134 |
|
4395 | 135 |
Depending on the theory context, the \texttt{Add} and \texttt{Del} |
136 |
functions manipulate basic components of the associated current |
|
137 |
simpset. Internally, all rewrite rules have to be expressed as |
|
138 |
(conditional) meta-equalities. This form is derived automatically |
|
139 |
from object-level equations that are supplied by the user. Another |
|
140 |
source of rewrite rules are \emph{simplification procedures}, that is |
|
141 |
\ML\ functions that produce suitable theorems on demand, depending on |
|
142 |
the current redex. Congruences are a more advanced feature; see |
|
143 |
\S\ref{sec:simp-congs}. |
|
144 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
145 |
\begin{ttdescription} |
4395 | 146 |
|
147 |
\item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from |
|
148 |
$thms$ to the current simpset. |
|
149 |
||
150 |
\item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived |
|
151 |
from $thms$ from the current simpset. |
|
152 |
||
153 |
\item[\ttindexbold{Addsimprocs} $procs$;] adds simplification |
|
154 |
procedures $procs$ to the current simpset. |
|
155 |
||
156 |
\item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification |
|
157 |
procedures $procs$ from the current simpset. |
|
158 |
||
159 |
\item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the |
|
160 |
current simpset. |
|
161 |
||
162 |
\item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules to the |
|
163 |
current simpset. |
|
164 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
165 |
\end{ttdescription} |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
166 |
|
4395 | 167 |
When a new theory is built, its implicit simpset is initialized by the |
168 |
union of the respective simpsets of its parent theories. In addition, |
|
169 |
certain theory definition constructs (e.g.\ \ttindex{datatype} and |
|
170 |
\ttindex{primrec} in \HOL) implicitly augment the current simpset. |
|
171 |
Ordinary definitions are not added automatically! |
|
172 |
||
173 |
It is up the user to manipulate the current simpset further by |
|
174 |
explicitly adding or deleting theorems and simplification procedures. |
|
175 |
||
176 |
\medskip |
|
177 |
||
178 |
Good simpsets are hard to design. As a rule of thump, generally |
|
179 |
useful ``simplification rules'' like $\Var{n}+0 = \Var{n}$ should be |
|
180 |
added to the current simpset right after they have been proved. Those |
|
181 |
of a more specific nature (e.g.\ the laws of de~Morgan, which alter |
|
182 |
the structure of a formula) should only be added for specific proofs |
|
183 |
and deleted again afterwards. Conversely, it may also happen that a |
|
184 |
generally useful rule needs to be removed for a certain proof and is |
|
185 |
added again afterwards. The need of frequent temporary additions or |
|
186 |
deletions may indicate a badly designed simpset. |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
187 |
|
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
188 |
\begin{warn} |
4395 | 189 |
The union of the parent simpsets (as described above) is not always |
190 |
a good starting point for the new theory. If some ancestors have |
|
191 |
deleted simplification rules because they are no longer wanted, |
|
192 |
while others have left those rules in, then the union will contain |
|
193 |
the unwanted rules. |
|
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
194 |
\end{warn} |
104 | 195 |
|
196 |
||
286 | 197 |
\section{Simplification sets}\index{simplification sets} |
4395 | 198 |
|
199 |
The simplifier is controlled by information contained in {\bf |
|
200 |
simpsets}. These consist of several components, including rewrite |
|
201 |
rules, simplification procedures, congruence rules, and the subgoaler, |
|
202 |
solver and looper tactics. The simplifier should be set up with |
|
203 |
sensible defaults so that most simplifier calls specify only rewrite |
|
204 |
rules or simplification procedures. Experienced users can exploit the |
|
205 |
other components to streamline proofs in more sophisticated manners. |
|
206 |
||
207 |
\subsection{Inspecting simpsets} |
|
208 |
\begin{ttbox} |
|
209 |
print_ss : simpset -> unit |
|
210 |
\end{ttbox} |
|
211 |
\begin{ttdescription} |
|
212 |
||
213 |
\item[\ttindexbold{print_ss} $ss$;] displays the printable contents of |
|
214 |
simpset $ss$. This includes the rewrite rules and congruences in |
|
215 |
their internal form expressed as meta-equalities. The names of the |
|
216 |
simplification procedures and the patterns they are invoked on are |
|
217 |
also shown. The other parts, functions and tactics, are |
|
218 |
non-printable. |
|
219 |
||
220 |
\end{ttdescription} |
|
221 |
||
323 | 222 |
|
4395 | 223 |
\subsection{Building simpsets} |
224 |
\begin{ttbox} |
|
225 |
empty_ss : simpset |
|
226 |
merge_ss : simpset * simpset -> simpset |
|
227 |
\end{ttbox} |
|
228 |
\begin{ttdescription} |
|
229 |
||
230 |
\item[\ttindexbold{empty_ss}] is the empty simpset. This is not very |
|
231 |
useful under normal circumstances because it doesn't contain |
|
232 |
suitable tactics (subgoaler etc.). When setting up the simplifier |
|
233 |
for a particular object-logic, one will typically define a more |
|
234 |
appropriate ``almost empty'' simpset. For example, in \HOL\ this is |
|
235 |
called \ttindexbold{HOL_basic_ss}. |
|
236 |
||
237 |
\item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ |
|
238 |
and $ss@2$ by building the union of their respective rewrite rules, |
|
239 |
simplification procedures and congruences. The other components |
|
240 |
(tactics etc.) cannot be merged, though; they are simply inherited |
|
241 |
from either simpset. |
|
242 |
||
243 |
\end{ttdescription} |
|
244 |
||
245 |
||
246 |
\subsection{Accessing the current simpset} |
|
247 |
||
248 |
\begin{ttbox} |
|
249 |
simpset : unit -> simpset |
|
250 |
simpset_ref : unit -> simpset ref |
|
251 |
simpset_of : theory -> simpset |
|
252 |
simpset_ref_of : theory -> simpset ref |
|
253 |
print_simpset : theory -> unit |
|
254 |
\end{ttbox} |
|
255 |
||
256 |
Each theory contains a current simpset\index{simpset!current} stored |
|
257 |
within a private ML reference variable. This can be retrieved and |
|
258 |
modified as follows. |
|
259 |
||
260 |
\begin{ttdescription} |
|
261 |
||
262 |
\item[\ttindexbold{simpset}();] retrieves the simpset value from the |
|
263 |
current theory context. |
|
264 |
||
265 |
\item[\ttindexbold{simpset_ref}();] retrieves the simpset reference |
|
266 |
variable from the current theory context. This can be assigned to |
|
267 |
by using \texttt{:=} in ML. |
|
268 |
||
269 |
\item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value |
|
270 |
from theory $thy$. |
|
271 |
||
272 |
\item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset |
|
273 |
reference variable from theory $thy$. |
|
274 |
||
275 |
\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset |
|
276 |
of theory $thy$ in the same way as \texttt{print_ss}. |
|
277 |
||
278 |
\end{ttdescription} |
|
279 |
||
104 | 280 |
|
332 | 281 |
\subsection{Rewrite rules} |
4395 | 282 |
\begin{ttbox} |
283 |
addsimps : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
284 |
delsimps : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
285 |
\end{ttbox} |
|
286 |
||
287 |
\index{rewrite rules|(} Rewrite rules are theorems expressing some |
|
288 |
form of equality, for example: |
|
323 | 289 |
\begin{eqnarray*} |
290 |
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\ |
|
291 |
\Var{P}\conj\Var{P} &\bimp& \Var{P} \\ |
|
714 | 292 |
\Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\} |
323 | 293 |
\end{eqnarray*} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
294 |
Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = |
4395 | 295 |
0$ are also permitted; the conditions can be arbitrary formulas. |
104 | 296 |
|
4395 | 297 |
Internally, all rewrite rules are translated into meta-equalities, |
298 |
theorems with conclusion $lhs \equiv rhs$. Each simpset contains a |
|
299 |
function for extracting equalities from arbitrary theorems. For |
|
300 |
example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} |
|
301 |
\equiv False$. This function can be installed using |
|
302 |
\ttindex{setmksimps} but only the definer of a logic should need to do |
|
303 |
this; see \S\ref{sec:setmksimps}. The function processes theorems |
|
304 |
added by \texttt{addsimps} as well as local assumptions. |
|
104 | 305 |
|
4395 | 306 |
\begin{ttdescription} |
307 |
||
308 |
\item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived |
|
309 |
from $thms$ to the simpset $ss$. |
|
310 |
||
311 |
\item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules |
|
312 |
derived from $thms$ from the simpset $ss$. |
|
313 |
||
314 |
\end{ttdescription} |
|
104 | 315 |
|
332 | 316 |
\begin{warn} |
4395 | 317 |
The simplifier will accept all standard rewrite rules: those where |
318 |
all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} = |
|
319 |
{(\Var{i}+\Var{j})+\Var{k}}$ is OK. |
|
320 |
||
321 |
It will also deal gracefully with all rules whose left-hand sides |
|
322 |
are so-called {\em higher-order patterns}~\cite{nipkow-patterns}. |
|
323 |
\indexbold{higher-order pattern}\indexbold{pattern, higher-order} |
|
324 |
These are terms in $\beta$-normal form (this will always be the case |
|
325 |
unless you have done something strange) where each occurrence of an |
|
326 |
unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are |
|
327 |
distinct bound variables. Hence $(\forall x.\Var{P}(x) \land |
|
328 |
\Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall |
|
329 |
x.\Var{Q}(x))$ is also OK, in both directions. |
|
330 |
||
331 |
In some rare cases the rewriter will even deal with quite general |
|
332 |
rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ |
|
333 |
rewrites $g(a) \in range(g)$ to $True$, but will fail to match |
|
334 |
$g(h(b)) \in range(\lambda x.g(h(x)))$. However, you can replace |
|
335 |
the offending subterms (in our case $\Var{f}(\Var{x})$, which is not |
|
336 |
a pattern) by adding new variables and conditions: $\Var{y} = |
|
337 |
\Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is |
|
338 |
acceptable as a conditional rewrite rule since conditions can be |
|
339 |
arbitrary terms. |
|
340 |
||
341 |
There is basically no restriction on the form of the right-hand |
|
342 |
sides. They may not contain extraneous term or type variables, |
|
343 |
though. |
|
104 | 344 |
\end{warn} |
332 | 345 |
\index{rewrite rules|)} |
346 |
||
4395 | 347 |
|
348 |
\subsection{Simplification procedures} |
|
349 |
\begin{ttbox} |
|
350 |
addsimprocs : simpset * simproc list -> simpset |
|
351 |
delsimprocs : simpset * simproc list -> simpset |
|
352 |
\end{ttbox} |
|
353 |
||
354 |
Simplification procedures are {\ML} functions that may produce |
|
355 |
\emph{proven} rewrite rules on demand. They are associated with |
|
356 |
certain patterns that conceptually represent left-hand sides of |
|
357 |
equations; these are shown by \texttt{print_ss}. During its |
|
358 |
operation, the simplifier may offer a simplification procedure the |
|
359 |
current redex and ask for a suitable rewrite rule. Thus rules may be |
|
360 |
specifically fashioned for particular situations, resulting in a more |
|
361 |
powerful mechanism than term rewriting by a fixed set of rules. |
|
362 |
||
363 |
||
364 |
\begin{ttdescription} |
|
365 |
||
366 |
\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification |
|
367 |
procedures $procs$ to the current simpset. |
|
368 |
||
369 |
\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification |
|
370 |
procedures $procs$ from the current simpset. |
|
371 |
||
372 |
\end{ttdescription} |
|
373 |
||
374 |
||
375 |
\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} |
|
376 |
\begin{ttbox} |
|
377 |
addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
378 |
delcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
379 |
addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
380 |
deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
381 |
\end{ttbox} |
|
382 |
||
104 | 383 |
Congruence rules are meta-equalities of the form |
3108 | 384 |
\[ \dots \Imp |
104 | 385 |
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). |
386 |
\] |
|
323 | 387 |
This governs the simplification of the arguments of~$f$. For |
104 | 388 |
example, some arguments can be simplified under additional assumptions: |
389 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |
|
390 |
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2}) |
|
391 |
\] |
|
4395 | 392 |
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite |
393 |
rules from it when simplifying~$P@2$. Such local assumptions are |
|
394 |
effective for rewriting formulae such as $x=0\imp y+x=y$. The local |
|
395 |
assumptions are also provided as theorems to the solver; see |
|
396 |
\S~\ref{sec:simp-solver} below. |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
397 |
|
4395 | 398 |
\begin{ttdescription} |
399 |
||
400 |
\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the |
|
401 |
simpset $ss$. These are derived from $thms$ in an appropriate way, |
|
402 |
depending on the underlying object-logic. |
|
403 |
||
404 |
\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules |
|
405 |
derived from $thms$. |
|
406 |
||
407 |
\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in |
|
408 |
their internal form (conclusions using meta-equality) to simpset |
|
409 |
$ss$. This is the basic mechanism that \texttt{addcongs} is built |
|
410 |
on. It should be rarely used directly. |
|
411 |
||
412 |
\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules |
|
413 |
in internal form from simpset $ss$. |
|
414 |
||
415 |
\end{ttdescription} |
|
416 |
||
417 |
\medskip |
|
418 |
||
419 |
Here are some more examples. The congruence rule for bounded |
|
420 |
quantifiers also supplies contextual information, this time about the |
|
421 |
bound variable: |
|
286 | 422 |
\begin{eqnarray*} |
423 |
&&\List{\Var{A}=\Var{B};\; |
|
424 |
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ |
|
425 |
&&\qquad\qquad |
|
426 |
(\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x)) |
|
427 |
\end{eqnarray*} |
|
323 | 428 |
The congruence rule for conditional expressions can supply contextual |
429 |
information for simplifying the arms: |
|
104 | 430 |
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~ |
431 |
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp |
|
432 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d}) |
|
433 |
\] |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
434 |
A congruence rule can also {\em prevent\/} simplification of some arguments. |
104 | 435 |
Here is an alternative congruence rule for conditional expressions: |
436 |
\[ \Var{p}=\Var{q} \Imp |
|
437 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b}) |
|
438 |
\] |
|
439 |
Only the first argument is simplified; the others remain unchanged. |
|
440 |
This can make simplification much faster, but may require an extra case split |
|
441 |
to prove the goal. |
|
442 |
||
443 |
||
4395 | 444 |
\subsection{*The subgoaler}\label{sec:simp-subgoaler} |
445 |
\begin{ttbox} |
|
446 |
setsubgoaler : simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
447 |
prems_of_ss : simpset -> thm list |
|
448 |
\end{ttbox} |
|
449 |
||
104 | 450 |
The subgoaler is the tactic used to solve subgoals arising out of |
451 |
conditional rewrite rules or congruence rules. The default should be |
|
4395 | 452 |
simplification itself. Occasionally this strategy needs to be |
453 |
changed. For example, if the premise of a conditional rule is an |
|
454 |
instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} |
|
455 |
< \Var{n}$, the default strategy could loop. |
|
104 | 456 |
|
4395 | 457 |
\begin{ttdescription} |
458 |
||
459 |
\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of |
|
460 |
$ss$ to $tacf$. The function $tacf$ will be applied to the current |
|
461 |
simplifier context expressed as a simpset. |
|
462 |
||
463 |
\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of |
|
464 |
premises from simplifier context $ss$. This may be non-empty only |
|
465 |
if the simplifier has been told to utilize local assumptions in the |
|
466 |
first place, e.g.\ if invoked via \texttt{asm_simp_tac}. |
|
467 |
||
468 |
\end{ttdescription} |
|
469 |
||
470 |
As an example, consider the following subgoaler: |
|
104 | 471 |
\begin{ttbox} |
4395 | 472 |
fun subgoaler ss = |
473 |
assume_tac ORELSE' |
|
474 |
resolve_tac (prems_of_ss ss) ORELSE' |
|
475 |
asm_simp_tac ss; |
|
104 | 476 |
\end{ttbox} |
4395 | 477 |
This tactic first tries to solve the subgoal by assumption or by |
478 |
resolving with with one of the premises, calling simplification only |
|
479 |
if that fails. |
|
480 |
||
104 | 481 |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
482 |
\subsection{*The solver}\label{sec:simp-solver} |
4395 | 483 |
\begin{ttbox} |
484 |
setSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
485 |
addSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
486 |
setSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
487 |
addSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
488 |
\end{ttbox} |
|
489 |
||
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
490 |
The solver is a pair of tactics that attempt to solve a subgoal after |
4395 | 491 |
simplification. Typically it just proves trivial subgoals such as |
492 |
{\tt True} and $t=t$. It could use sophisticated means such as {\tt |
|
493 |
blast_tac}, though that could make simplification expensive. |
|
286 | 494 |
|
3108 | 495 |
Rewriting does not instantiate unknowns. For example, rewriting |
496 |
cannot prove $a\in \Var{A}$ since this requires |
|
497 |
instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic |
|
498 |
and may instantiate unknowns as it pleases. This is the only way the |
|
499 |
simplifier can handle a conditional rewrite rule whose condition |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset
|
500 |
contains extra variables. When a simplification tactic is to be |
3108 | 501 |
combined with other provers, especially with the classical reasoner, |
4395 | 502 |
it is important whether it can be considered safe or not. For this |
503 |
reason the solver is split into a safe and an unsafe part. |
|
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
504 |
|
3108 | 505 |
The standard simplification strategy solely uses the unsafe solver, |
4395 | 506 |
which is appropriate in most cases. For special applications where |
3108 | 507 |
the simplification process is not allowed to instantiate unknowns |
4395 | 508 |
within the goal, simplification starts with the safe solver, but may |
509 |
still apply the ordinary unsafe one in nested simplifications for |
|
510 |
conditional rules or congruences. |
|
511 |
||
512 |
\begin{ttdescription} |
|
513 |
||
514 |
\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the |
|
515 |
\emph{safe} solver of $ss$. |
|
516 |
||
517 |
\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an |
|
518 |
additional \emph{safe} solver; it will be tried after the solvers |
|
519 |
which had already been present in $ss$. |
|
520 |
||
521 |
\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the |
|
522 |
unsafe solver of $ss$. |
|
523 |
||
524 |
\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an |
|
525 |
additional unsafe solver; it will be tried after the solvers which |
|
526 |
had already been present in $ss$. |
|
323 | 527 |
|
4395 | 528 |
\end{ttdescription} |
529 |
||
530 |
\medskip |
|
104 | 531 |
|
4395 | 532 |
\index{assumptions!in simplification} The solver tactic is invoked |
533 |
with a list of theorems, namely assumptions that hold in the local |
|
534 |
context. This may be non-empty only if the simplifier has been told |
|
535 |
to utilize local assumptions in the first place, e.g.\ if invoked via |
|
536 |
\texttt{asm_simp_tac}. The solver is also presented the full goal |
|
537 |
including its assumptions in any case. Thus it can use these (e.g.\ |
|
538 |
by calling \texttt{assume_tac}), even if the list of premises is not |
|
539 |
passed. |
|
540 |
||
541 |
\medskip |
|
542 |
||
543 |
As explained in \S\ref{sec:simp-subgoaler}, the subgoaler is also used |
|
544 |
to solve the premises of congruence rules. These are usually of the |
|
545 |
form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$ |
|
546 |
needs to be instantiated with the result. Typically, the subgoaler |
|
547 |
will invoke the simplifier at some point, which will eventually call |
|
548 |
the solver. For this reason, solver tactics must be prepared to solve |
|
549 |
goals of the form $t = \Var{x}$, usually by reflexivity. In |
|
550 |
particular, reflexivity should be tried before any of the fancy |
|
551 |
tactics like {\tt blast_tac}. |
|
323 | 552 |
|
3108 | 553 |
It may even happen that due to simplification the subgoal is no longer |
554 |
an equality. For example $False \bimp \Var{Q}$ could be rewritten to |
|
555 |
$\neg\Var{Q}$. To cover this case, the solver could try resolving |
|
556 |
with the theorem $\neg False$. |
|
104 | 557 |
|
4395 | 558 |
\medskip |
559 |
||
104 | 560 |
\begin{warn} |
4395 | 561 |
If the simplifier aborts with the message \texttt{Failed congruence |
3108 | 562 |
proof!}, then the subgoaler or solver has failed to prove a |
563 |
premise of a congruence rule. This should never occur under normal |
|
564 |
circumstances; it indicates that some congruence rule, or possibly |
|
565 |
the subgoaler or solver, is faulty. |
|
104 | 566 |
\end{warn} |
567 |
||
323 | 568 |
|
4395 | 569 |
\subsection{*The looper}\label{sec:simp-looper} |
570 |
\begin{ttbox} |
|
571 |
setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4} |
|
572 |
addloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4} |
|
573 |
addsplits : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
574 |
\end{ttbox} |
|
575 |
||
576 |
The looper is a tactic that is applied after simplification, in case |
|
577 |
the solver failed to solve the simplified goal. If the looper |
|
578 |
succeeds, the simplification process is started all over again. Each |
|
579 |
of the subgoals generated by the looper is attacked in turn, in |
|
580 |
reverse order. |
|
581 |
||
582 |
A typical looper is case splitting: the expansion of a conditional. |
|
583 |
Another possibility is to apply an elimination rule on the |
|
584 |
assumptions. More adventurous loopers could start an induction. |
|
585 |
||
586 |
\begin{ttdescription} |
|
587 |
||
588 |
\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the looper |
|
589 |
of $ss$. |
|
590 |
||
591 |
\item[$ss$ \ttindexbold{addloop} $tacf$] adds $tacf$ as an additional |
|
592 |
looper; it will be tried after the loopers which had already been |
|
593 |
present in $ss$. |
|
594 |
||
595 |
\item[$ss$ \ttindexbold{addsplits} $thms$] adds |
|
596 |
\texttt{(split_tac~$thms$)} as an additional looper. |
|
597 |
||
598 |
\end{ttdescription} |
|
599 |
||
104 | 600 |
|
601 |
||
4395 | 602 |
\section{The simplification tactics}\label{simp-tactics} |
603 |
\index{simplification!tactics}\index{tactics!simplification} |
|
604 |
\begin{ttbox} |
|
605 |
simp_tac : simpset -> int -> tactic |
|
606 |
asm_simp_tac : simpset -> int -> tactic |
|
607 |
full_simp_tac : simpset -> int -> tactic |
|
608 |
asm_full_simp_tac : simpset -> int -> tactic |
|
609 |
safe_asm_full_simp_tac : simpset -> int -> tactic |
|
610 |
SIMPSET : (simpset -> tactic) -> tactic |
|
611 |
SIMPSET' : (simpset -> 'a -> tactic) -> 'a -> tactic |
|
612 |
\end{ttbox} |
|
2567 | 613 |
|
4395 | 614 |
These are the basic tactics that are underlying any actual |
615 |
simplification work. The rewriting strategy is always strictly bottom |
|
616 |
up, except for congruence rules, which are applied while descending |
|
617 |
into a term. Conditions in conditional rewrite rules are solved |
|
618 |
recursively before the rewrite rule is applied. |
|
104 | 619 |
|
4395 | 620 |
\begin{ttdescription} |
621 |
||
622 |
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, |
|
623 |
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are |
|
624 |
the basic simplification tactics that work exactly like their |
|
625 |
namesakes in \S\ref{sec:simp-for-dummies}, except that they are |
|
626 |
explicitly supplied with a simpset. |
|
627 |
||
628 |
\item[\ttindexbold{safe_asm_full_simp_tac}] is like |
|
629 |
\texttt{asm_full_simp_tac}, but uses the safe solver as explained in |
|
630 |
\S\ref{sec:simp-solver}. This tactic is mainly intended for |
|
631 |
building special tools, e.g.\ for combining the simplifier with the |
|
632 |
classical reasoner. It is rarely used directly. |
|
633 |
||
634 |
\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$] |
|
635 |
are tacticals that make a tactic depend on the implicit current |
|
636 |
simpset of the theory associated with the proof state they are |
|
637 |
applied on. |
|
104 | 638 |
|
4395 | 639 |
\end{ttdescription} |
104 | 640 |
|
4395 | 641 |
\medskip |
104 | 642 |
|
4395 | 643 |
Local modifications of simpsets within a proof are often much cleaner |
644 |
by using above tactics in conjunction with explicit simpsets, rather |
|
645 |
than their capitalized counterparts. For example |
|
1213 | 646 |
\begin{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
647 |
Addsimps \(thms\); |
2479 | 648 |
by (Simp_tac \(i\)); |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
649 |
Delsimps \(thms\); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
650 |
\end{ttbox} |
4395 | 651 |
can be expressed more appropriately as |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
652 |
\begin{ttbox} |
4395 | 653 |
by (simp_tac (simpset() addsimps \(thms\)) \(i\)); |
1213 | 654 |
\end{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
655 |
|
4395 | 656 |
\medskip |
657 |
||
658 |
Also note that functions depending implicitly on the current theory |
|
659 |
context (like capital \texttt{Simp_tac} and the other commands of |
|
660 |
\S\ref{sec:simp-for-dummies}) should be considered harmful outside of |
|
661 |
actual proof scripts. In particular, ML programs like theory |
|
662 |
definition packages or special tactics should refer to simpsets only |
|
663 |
explicitly, via the above tactics used in conjunction with |
|
664 |
\texttt{simpset_of} or the \texttt{SIMPSET} tacticals. |
|
665 |
||
666 |
\begin{warn} |
|
667 |
There is a subtle difference between \texttt{(SIMPSET'~$tacf$)} and |
|
668 |
\texttt{($tacf$~(simpset()))}. For example \texttt{(SIMPSET' |
|
669 |
simp_tac)} would depend on the theory of the proof state it is |
|
670 |
applied to, while \texttt{(simp_tac (simpset()))} implicitly refers |
|
671 |
to the current theory context. Both are usually the same in proof |
|
672 |
scripts, provided that goals are only stated within the current |
|
673 |
theory. Robust programs would not count on that, of course. |
|
674 |
\end{warn} |
|
675 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
676 |
|
4395 | 677 |
\section{Forward simplification rules} |
678 |
\index{simplification!forward rules} |
|
679 |
\begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify} |
|
680 |
simplify : simpset -> thm -> thm |
|
681 |
asm_simplify : simpset -> thm -> thm |
|
682 |
full_simplify : simpset -> thm -> thm |
|
683 |
asm_full_simplify : simpset -> thm -> thm |
|
684 |
\end{ttbox} |
|
685 |
||
686 |
These are forward rules, simplifying theorems in a similar way as the |
|
687 |
corresponding simplification tactics do. The forward rules affect the whole |
|
104 | 688 |
|
4395 | 689 |
subgoals of a proof state. The |
690 |
looper~/ solver process as described in \S\ref{sec:simp-looper} and |
|
691 |
\S\ref{sec:simp-solver} does not apply here, though. |
|
692 |
||
693 |
\begin{warn} |
|
694 |
Forward simplification should be used rarely in ordinary proof |
|
695 |
scripts. It as mainly intended to provide an internal interface to |
|
696 |
the simplifier for ML coded special utilities. |
|
697 |
\end{warn} |
|
698 |
||
699 |
||
700 |
\section{Examples of using the simplifier} |
|
3112 | 701 |
\index{examples!of simplification} Assume we are working within {\tt |
702 |
FOL} (cf.\ \texttt{FOL/ex/Nat}) and that |
|
323 | 703 |
\begin{ttdescription} |
704 |
\item[Nat.thy] |
|
705 |
is a theory including the constants $0$, $Suc$ and $+$, |
|
706 |
\item[add_0] |
|
707 |
is the rewrite rule $0+\Var{n} = \Var{n}$, |
|
708 |
\item[add_Suc] |
|
709 |
is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$, |
|
710 |
\item[induct] |
|
711 |
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp |
|
712 |
\Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. |
|
713 |
\end{ttdescription} |
|
4395 | 714 |
We augment the implicit simpset inherited from \texttt{Nat} with the |
715 |
basic rewrite rules for natural numbers: |
|
104 | 716 |
\begin{ttbox} |
3112 | 717 |
Addsimps [add_0, add_Suc]; |
104 | 718 |
\end{ttbox} |
323 | 719 |
|
720 |
\subsection{A trivial example} |
|
286 | 721 |
Proofs by induction typically involve simplification. Here is a proof |
722 |
that~0 is a right identity: |
|
104 | 723 |
\begin{ttbox} |
724 |
goal Nat.thy "m+0 = m"; |
|
725 |
{\out Level 0} |
|
726 |
{\out m + 0 = m} |
|
727 |
{\out 1. m + 0 = m} |
|
286 | 728 |
\end{ttbox} |
729 |
The first step is to perform induction on the variable~$m$. This returns a |
|
730 |
base case and inductive step as two subgoals: |
|
731 |
\begin{ttbox} |
|
104 | 732 |
by (res_inst_tac [("n","m")] induct 1); |
733 |
{\out Level 1} |
|
734 |
{\out m + 0 = m} |
|
735 |
{\out 1. 0 + 0 = 0} |
|
736 |
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} |
|
737 |
\end{ttbox} |
|
286 | 738 |
Simplification solves the first subgoal trivially: |
104 | 739 |
\begin{ttbox} |
3112 | 740 |
by (Simp_tac 1); |
104 | 741 |
{\out Level 2} |
742 |
{\out m + 0 = m} |
|
743 |
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)} |
|
744 |
\end{ttbox} |
|
3112 | 745 |
The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the |
104 | 746 |
induction hypothesis as a rewrite rule: |
747 |
\begin{ttbox} |
|
3112 | 748 |
by (Asm_simp_tac 1); |
104 | 749 |
{\out Level 3} |
750 |
{\out m + 0 = m} |
|
751 |
{\out No subgoals!} |
|
752 |
\end{ttbox} |
|
753 |
||
323 | 754 |
\subsection{An example of tracing} |
3108 | 755 |
\index{tracing!of simplification|(}\index{*trace_simp} |
323 | 756 |
Let us prove a similar result involving more complex terms. The two |
757 |
equations together can be used to prove that addition is commutative. |
|
104 | 758 |
\begin{ttbox} |
759 |
goal Nat.thy "m+Suc(n) = Suc(m+n)"; |
|
760 |
{\out Level 0} |
|
761 |
{\out m + Suc(n) = Suc(m + n)} |
|
762 |
{\out 1. m + Suc(n) = Suc(m + n)} |
|
286 | 763 |
\end{ttbox} |
764 |
We again perform induction on~$m$ and get two subgoals: |
|
765 |
\begin{ttbox} |
|
104 | 766 |
by (res_inst_tac [("n","m")] induct 1); |
767 |
{\out Level 1} |
|
768 |
{\out m + Suc(n) = Suc(m + n)} |
|
769 |
{\out 1. 0 + Suc(n) = Suc(0 + n)} |
|
286 | 770 |
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>} |
771 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} |
|
772 |
\end{ttbox} |
|
773 |
Simplification solves the first subgoal, this time rewriting two |
|
774 |
occurrences of~0: |
|
775 |
\begin{ttbox} |
|
3112 | 776 |
by (Simp_tac 1); |
104 | 777 |
{\out Level 2} |
778 |
{\out m + Suc(n) = Suc(m + n)} |
|
286 | 779 |
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>} |
780 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)} |
|
104 | 781 |
\end{ttbox} |
782 |
Switching tracing on illustrates how the simplifier solves the remaining |
|
783 |
subgoal: |
|
784 |
\begin{ttbox} |
|
4395 | 785 |
set trace_simp; |
3112 | 786 |
by (Asm_simp_tac 1); |
323 | 787 |
\ttbreak |
3112 | 788 |
{\out Adding rewrite rule:} |
789 |
{\out .x + Suc(n) == Suc(.x + n)} |
|
323 | 790 |
\ttbreak |
104 | 791 |
{\out Rewriting:} |
3112 | 792 |
{\out Suc(.x) + Suc(n) == Suc(.x + Suc(n))} |
323 | 793 |
\ttbreak |
104 | 794 |
{\out Rewriting:} |
3112 | 795 |
{\out .x + Suc(n) == Suc(.x + n)} |
323 | 796 |
\ttbreak |
104 | 797 |
{\out Rewriting:} |
3112 | 798 |
{\out Suc(.x) + n == Suc(.x + n)} |
799 |
\ttbreak |
|
800 |
{\out Rewriting:} |
|
801 |
{\out Suc(Suc(.x + n)) = Suc(Suc(.x + n)) == True} |
|
323 | 802 |
\ttbreak |
104 | 803 |
{\out Level 3} |
804 |
{\out m + Suc(n) = Suc(m + n)} |
|
805 |
{\out No subgoals!} |
|
806 |
\end{ttbox} |
|
286 | 807 |
Many variations are possible. At Level~1 (in either example) we could have |
808 |
solved both subgoals at once using the tactical \ttindex{ALLGOALS}: |
|
104 | 809 |
\begin{ttbox} |
3112 | 810 |
by (ALLGOALS Asm_simp_tac); |
104 | 811 |
{\out Level 2} |
812 |
{\out m + Suc(n) = Suc(m + n)} |
|
813 |
{\out No subgoals!} |
|
814 |
\end{ttbox} |
|
3108 | 815 |
\index{tracing!of simplification|)} |
104 | 816 |
|
323 | 817 |
\subsection{Free variables and simplification} |
104 | 818 |
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying |
323 | 819 |
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: |
104 | 820 |
\begin{ttbox} |
821 |
val [prem] = goal Nat.thy |
|
822 |
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
|
823 |
{\out Level 0} |
|
824 |
{\out f(i + j) = i + f(j)} |
|
825 |
{\out 1. f(i + j) = i + f(j)} |
|
323 | 826 |
\ttbreak |
286 | 827 |
{\out val prem = "f(Suc(?n)) = Suc(f(?n))} |
828 |
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm} |
|
323 | 829 |
\end{ttbox} |
830 |
In the theorem~{\tt prem}, note that $f$ is a free variable while |
|
831 |
$\Var{n}$ is a schematic variable. |
|
832 |
\begin{ttbox} |
|
104 | 833 |
by (res_inst_tac [("n","i")] induct 1); |
834 |
{\out Level 1} |
|
835 |
{\out f(i + j) = i + f(j)} |
|
836 |
{\out 1. f(0 + j) = 0 + f(j)} |
|
837 |
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} |
|
838 |
\end{ttbox} |
|
839 |
We simplify each subgoal in turn. The first one is trivial: |
|
840 |
\begin{ttbox} |
|
3112 | 841 |
by (Simp_tac 1); |
104 | 842 |
{\out Level 2} |
843 |
{\out f(i + j) = i + f(j)} |
|
844 |
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)} |
|
845 |
\end{ttbox} |
|
3112 | 846 |
The remaining subgoal requires rewriting by the premise, so we add it |
4395 | 847 |
to the current simpset: |
104 | 848 |
\begin{ttbox} |
4395 | 849 |
by (asm_simp_tac (simpset() addsimps [prem]) 1); |
104 | 850 |
{\out Level 3} |
851 |
{\out f(i + j) = i + f(j)} |
|
852 |
{\out No subgoals!} |
|
853 |
\end{ttbox} |
|
854 |
||
1213 | 855 |
\subsection{Reordering assumptions} |
856 |
\label{sec:reordering-asms} |
|
857 |
\index{assumptions!reordering} |
|
858 |
||
4395 | 859 |
As mentioned in \S\ref{sec:simp-for-dummies-tacs}, |
860 |
\ttindex{asm_full_simp_tac} may require the assumptions to be permuted |
|
861 |
to be more effective. Given the subgoal |
|
1213 | 862 |
\begin{ttbox} |
863 |
{\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S} |
|
864 |
\end{ttbox} |
|
865 |
we can rotate the assumptions two positions to the right |
|
866 |
\begin{ttbox} |
|
867 |
by (rotate_tac ~2 1); |
|
868 |
\end{ttbox} |
|
869 |
to obtain |
|
870 |
\begin{ttbox} |
|
871 |
{\out 1. [| f(a) = t; R; P(f(a)); Q |] ==> S} |
|
872 |
\end{ttbox} |
|
873 |
which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to |
|
874 |
\verb$P(t)$. |
|
875 |
||
876 |
Since rotation alone cannot produce arbitrary permutations, you can also pick |
|
877 |
out a particular assumption which needs to be rewritten and move it the the |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3134
diff
changeset
|
878 |
right end of the assumptions. In the above case rotation can be replaced by |
1213 | 879 |
\begin{ttbox} |
880 |
by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1); |
|
881 |
\end{ttbox} |
|
882 |
which is more directed and leads to |
|
883 |
\begin{ttbox} |
|
884 |
{\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S} |
|
885 |
\end{ttbox} |
|
886 |
||
4395 | 887 |
\begin{warn} |
888 |
Reordering assumptions usually leads to brittle proofs and should be |
|
889 |
avoided. Future versions of \verb$asm_full_simp_tac$ may remove the |
|
890 |
need for such manipulations. |
|
891 |
\end{warn} |
|
892 |
||
286 | 893 |
|
332 | 894 |
\section{Permutative rewrite rules} |
323 | 895 |
\index{rewrite rules!permutative|(} |
4395 | 896 |
\begin{ttbox} |
897 |
settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} |
|
898 |
\end{ttbox} |
|
323 | 899 |
|
900 |
A rewrite rule is {\bf permutative} if the left-hand side and right-hand |
|
901 |
side are the same up to renaming of variables. The most common permutative |
|
902 |
rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = |
|
903 |
(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ |
|
904 |
for sets. Such rules are common enough to merit special attention. |
|
905 |
||
4395 | 906 |
Because ordinary rewriting loops given such rules, the simplifier |
907 |
employs a special strategy, called {\bf ordered |
|
908 |
rewriting}\index{rewriting!ordered}. There is a standard |
|
909 |
lexicographic ordering on terms. This should be perfectly OK in most |
|
910 |
cases, but can be changed for special applications. |
|
911 |
||
912 |
\begin{ttdescription} |
|
913 |
||
914 |
\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as |
|
915 |
term order in simpset $ss$. |
|
916 |
||
917 |
\end{ttdescription} |
|
918 |
||
919 |
\medskip |
|
323 | 920 |
|
4395 | 921 |
A permutative rewrite rule is applied only if it decreases the given |
922 |
term with respect to this ordering. For example, commutativity |
|
923 |
rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less |
|
924 |
than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also |
|
925 |
employs ordered rewriting. |
|
926 |
||
927 |
Permutative rewrite rules are added to simpsets just like other |
|
928 |
rewrite rules; the simplifier recognizes their special status |
|
929 |
automatically. They are most effective in the case of |
|
930 |
associative-commutative operators. (Associativity by itself is not |
|
931 |
permutative.) When dealing with an AC-operator~$f$, keep the |
|
932 |
following points in mind: |
|
323 | 933 |
\begin{itemize}\index{associative-commutative operators} |
4395 | 934 |
|
935 |
\item The associative law must always be oriented from left to right, |
|
936 |
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
|
937 |
used with commutativity, leads to looping in conjunction with the |
|
938 |
standard term order. |
|
323 | 939 |
|
940 |
\item To complete your set of rewrite rules, you must add not just |
|
941 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf |
|
942 |
left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
|
943 |
\end{itemize} |
|
944 |
Ordered rewriting with the combination of A, C, and~LC sorts a term |
|
945 |
lexicographically: |
|
946 |
\[\def\maps#1{\stackrel{#1}{\longmapsto}} |
|
947 |
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] |
|
948 |
Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many |
|
949 |
examples; other algebraic structures are amenable to ordered rewriting, |
|
950 |
such as boolean rings. |
|
951 |
||
3108 | 952 |
\subsection{Example: sums of natural numbers} |
4395 | 953 |
|
954 |
This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}). |
|
955 |
Theory \thydx{Arith} contains natural numbers arithmetic. Its |
|
956 |
associated simpset contains many arithmetic laws including |
|
957 |
distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list |
|
958 |
consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let |
|
959 |
us prove the theorem |
|
323 | 960 |
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] |
961 |
% |
|
962 |
A functional~{\tt sum} represents the summation operator under the |
|
3108 | 963 |
interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We |
4395 | 964 |
extend {\tt Arith} as follows: |
323 | 965 |
\begin{ttbox} |
966 |
NatSum = Arith + |
|
1387 | 967 |
consts sum :: [nat=>nat, nat] => nat |
4245 | 968 |
primrec "sum" nat |
969 |
"sum f 0 = 0" |
|
970 |
"sum f (Suc n) = f(n) + sum f n" |
|
323 | 971 |
end |
972 |
\end{ttbox} |
|
4245 | 973 |
The \texttt{primrec} declaration automatically adds rewrite rules for |
974 |
\texttt{sum} to the default simpset. We now insert the AC-rules for~$+$: |
|
323 | 975 |
\begin{ttbox} |
4245 | 976 |
Addsimps add_ac; |
323 | 977 |
\end{ttbox} |
3108 | 978 |
Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = |
323 | 979 |
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: |
980 |
\begin{ttbox} |
|
3108 | 981 |
goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; |
323 | 982 |
{\out Level 0} |
3108 | 983 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
984 |
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} |
|
323 | 985 |
\end{ttbox} |
3108 | 986 |
Induction should not be applied until the goal is in the simplest |
987 |
form: |
|
323 | 988 |
\begin{ttbox} |
4245 | 989 |
by (Simp_tac 1); |
323 | 990 |
{\out Level 1} |
3108 | 991 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
992 |
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} |
|
323 | 993 |
\end{ttbox} |
3108 | 994 |
Ordered rewriting has sorted the terms in the left-hand side. The |
995 |
subgoal is now ready for induction: |
|
323 | 996 |
\begin{ttbox} |
4245 | 997 |
by (induct_tac "n" 1); |
323 | 998 |
{\out Level 2} |
3108 | 999 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
1000 |
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} |
|
323 | 1001 |
\ttbreak |
4245 | 1002 |
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} |
1003 |
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =} |
|
1004 |
{\out Suc n * Suc n} |
|
323 | 1005 |
\end{ttbox} |
1006 |
Simplification proves both subgoals immediately:\index{*ALLGOALS} |
|
1007 |
\begin{ttbox} |
|
4245 | 1008 |
by (ALLGOALS Asm_simp_tac); |
323 | 1009 |
{\out Level 3} |
3108 | 1010 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
323 | 1011 |
{\out No subgoals!} |
1012 |
\end{ttbox} |
|
4245 | 1013 |
Simplification cannot prove the induction step if we omit {\tt add_ac} from |
1014 |
the simpset. Observe that like terms have not been collected: |
|
323 | 1015 |
\begin{ttbox} |
4245 | 1016 |
{\out Level 3} |
1017 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
|
1018 |
{\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n} |
|
1019 |
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i. i) n)) =} |
|
1020 |
{\out n + (n + (n + n * n))} |
|
323 | 1021 |
\end{ttbox} |
1022 |
Ordered rewriting proves this by sorting the left-hand side. Proving |
|
1023 |
arithmetic theorems without ordered rewriting requires explicit use of |
|
1024 |
commutativity. This is tedious; try it and see! |
|
1025 |
||
1026 |
Ordered rewriting is equally successful in proving |
|
1027 |
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. |
|
1028 |
||
1029 |
||
1030 |
\subsection{Re-orienting equalities} |
|
1031 |
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality |
|
1032 |
signs: |
|
1033 |
\begin{ttbox} |
|
1034 |
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" |
|
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset
|
1035 |
(fn _ => [Blast_tac 1]); |
323 | 1036 |
\end{ttbox} |
1037 |
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs |
|
1038 |
in the conclusion but not~$s$, can often be brought into the right form. |
|
1039 |
For example, ordered rewriting with {\tt symmetry} can prove the goal |
|
1040 |
\[ f(a)=b \conj f(a)=c \imp b=c. \] |
|
1041 |
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$ |
|
1042 |
because $f(a)$ is lexicographically greater than $b$ and~$c$. These |
|
1043 |
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the |
|
1044 |
conclusion by~$f(a)$. |
|
1045 |
||
1046 |
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. |
|
1047 |
The differing orientations make this appear difficult to prove. Ordered |
|
1048 |
rewriting with {\tt symmetry} makes the equalities agree. (Without |
|
1049 |
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ |
|
1050 |
or~$u=t$.) Then the simplifier can prove the goal outright. |
|
1051 |
||
1052 |
\index{rewrite rules!permutative|)} |
|
1053 |
||
1054 |
||
4395 | 1055 |
\section{*Coding simplification procedures} |
1056 |
\begin{ttbox} |
|
1057 |
mk_simproc: string -> cterm list -> |
|
1058 |
(Sign.sg -> thm list -> term -> thm option) -> simproc |
|
1059 |
\end{ttbox} |
|
1060 |
||
1061 |
\begin{ttdescription} |
|
1062 |
\item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes $proc$ a |
|
1063 |
simplification procedure for left-hand side patterns $lhss$. The |
|
1064 |
name just serves as a comment. The function $proc$ may be invoked |
|
1065 |
by the simplifier for redex positions matched by one of $lhss$ as |
|
1066 |
described below. |
|
1067 |
\end{ttdescription} |
|
1068 |
||
1069 |
Simplification procedures are applied in a two-stage process as |
|
1070 |
follows: The simplifier tries to match the current redex position |
|
1071 |
against any one of the $lhs$ patterns of any simplification procedure. |
|
1072 |
If this succeeds, it invokes the corresponding {\ML} function, passing |
|
1073 |
with the current signature, local assumptions and the (potential) |
|
1074 |
redex. The result may be either \texttt{None} (indicating failure) or |
|
1075 |
\texttt{Some~$thm$}. |
|
1076 |
||
1077 |
Any successful result is supposed to be a (possibly conditional) |
|
1078 |
rewrite rule $t \equiv u$ that is applicable to the current redex. |
|
1079 |
The rule will be applied just as any ordinary rewrite rule. It is |
|
1080 |
expected to be already in \emph{internal form}, though, bypassing the |
|
1081 |
automatic preprocessing of object-level equivalences. |
|
1082 |
||
1083 |
\medskip |
|
1084 |
||
1085 |
As an example of how to write your own simplification procedures, |
|
1086 |
consider eta-expansion of pair abstraction (see also |
|
1087 |
\texttt{HOL/Modelcheck/MCSyn} where this is used to provide external |
|
1088 |
model checker syntax). |
|
1089 |
||
1090 |
The {\HOL} theory of tuples (see \texttt{HOL/Prod}) provides an |
|
1091 |
operator \texttt{split} together with some concrete syntax supporting |
|
1092 |
$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a |
|
1093 |
tactic that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of |
|
1094 |
some pair type) to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule |
|
1095 |
is: |
|
1096 |
\begin{ttbox} |
|
1097 |
pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) |
|
1098 |
\end{ttbox} |
|
1099 |
Unfortunately, term rewriting using this rule directly would not |
|
1100 |
terminate! We now use the simplification procedure mechanism in order |
|
1101 |
to stop the simplifier from applying this rule over and over again, |
|
1102 |
making it rewrite only actual abstractions. The simplification |
|
1103 |
procedure \texttt{pair_eta_expand_proc} is defined as follows: |
|
1104 |
\begin{ttbox} |
|
1105 |
local |
|
1106 |
val lhss = |
|
1107 |
[read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
|
1108 |
val rew = mk_meta_eq pair_eta_expand; \medskip |
|
1109 |
fun proc _ _ (Abs _) = Some rew |
|
1110 |
| proc _ _ _ = None; |
|
1111 |
in |
|
1112 |
val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
|
1113 |
end; |
|
1114 |
\end{ttbox} |
|
1115 |
This is an example of using \texttt{pair_eta_expand_proc}: |
|
1116 |
\begin{ttbox} |
|
1117 |
{\out 1. P (\%p::'a * 'a. fst p + snd p + z)} |
|
1118 |
by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1); |
|
1119 |
{\out 1. P (\%(x::'a,y::'a). x + y + z)} |
|
1120 |
\end{ttbox} |
|
1121 |
||
1122 |
\medskip |
|
1123 |
||
1124 |
In the above example the simplification procedure just did fine |
|
1125 |
grained control over rule application, beyond higher-order pattern |
|
1126 |
matching. Usually, procedures would do some more work, in particular |
|
1127 |
prove particular theorems depending on the current redex. |
|
1128 |
||
1129 |
For example, simplification procedures \ttindexbold{nat_cancel} of |
|
1130 |
\texttt{HOL/Arith} cancel common summands and constant factors out of |
|
1131 |
several relations of sums over natural numbers. |
|
1132 |
||
1133 |
Consider the following goal, which after cancelling $a$ on both sides |
|
1134 |
contains a factor of $2$. Simplifying with the simpset of |
|
1135 |
\texttt{Arith.thy} will do the cancellation automatically: |
|
1136 |
\begin{ttbox} |
|
1137 |
{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} |
|
1138 |
by (Simp_tac 1); |
|
1139 |
{\out 1. x < Suc (a + (a + y))} |
|
1140 |
\end{ttbox} |
|
1141 |
||
1142 |
\medskip |
|
1143 |
||
1144 |
The {\ML} sources for these simplification procedures consist of a |
|
1145 |
generic part (files \texttt{cancel_sums.ML} and |
|
1146 |
\texttt{cancel_factor.ML} in \texttt{Provers/Arith}), and a |
|
1147 |
\texttt{HOL} specific part in \texttt{HOL/arith_data.ML}. |
|
1148 |
||
1149 |
||
323 | 1150 |
\section{*Setting up the simplifier}\label{sec:setting-up-simp} |
1151 |
\index{simplification!setting up} |
|
286 | 1152 |
|
1153 |
Setting up the simplifier for new logics is complicated. This section |
|
4395 | 1154 |
describes how the simplifier is installed for intuitionistic |
1155 |
first-order logic; the code is largely taken from {\tt |
|
1156 |
FOL/simpdata.ML} of the Isabelle sources. |
|
286 | 1157 |
|
323 | 1158 |
The simplifier and the case splitting tactic, which reside on separate |
4395 | 1159 |
files, are not part of Pure Isabelle. They must be loaded explicitly |
1160 |
by the object-logic as follows: |
|
286 | 1161 |
\begin{ttbox} |
4395 | 1162 |
use "$ISABELLE_HOME/src/Provers/simplifier.ML"; |
1163 |
use "$ISABELLE_HOME/src/Provers/splitter.ML"; |
|
286 | 1164 |
\end{ttbox} |
1165 |
||
1166 |
Simplification works by reducing various object-equalities to |
|
323 | 1167 |
meta-equality. It requires rules stating that equal terms and equivalent |
1168 |
formulae are also equal at the meta-level. The rule declaration part of |
|
3108 | 1169 |
the file {\tt FOL/IFOL.thy} contains the two lines |
323 | 1170 |
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} |
286 | 1171 |
eq_reflection "(x=y) ==> (x==y)" |
1172 |
iff_reflection "(P<->Q) ==> (P==Q)" |
|
1173 |
\end{ttbox} |
|
323 | 1174 |
Of course, you should only assert such rules if they are true for your |
286 | 1175 |
particular logic. In Constructive Type Theory, equality is a ternary |
4395 | 1176 |
relation of the form $a=b\in A$; the type~$A$ determines the meaning |
1177 |
of the equality essentially as a partial equivalence relation. The |
|
1178 |
present simplifier cannot be used. Rewriting in {\tt CTT} uses |
|
1179 |
another simplifier, which resides in the file {\tt |
|
1180 |
Provers/typedsimp.ML} and is not documented. Even this does not |
|
1181 |
work for later variants of Constructive Type Theory that use |
|
323 | 1182 |
intensional equality~\cite{nordstrom90}. |
286 | 1183 |
|
1184 |
||
1185 |
\subsection{A collection of standard rewrite rules} |
|
1186 |
The file begins by proving lots of standard rewrite rules about the logical |
|
323 | 1187 |
connectives. These include cancellation and associative laws. To prove |
1188 |
them easily, it defines a function that echoes the desired law and then |
|
286 | 1189 |
supplies it the theorem prover for intuitionistic \FOL: |
1190 |
\begin{ttbox} |
|
1191 |
fun int_prove_fun s = |
|
1192 |
(writeln s; |
|
1193 |
prove_goal IFOL.thy s |
|
1194 |
(fn prems => [ (cut_facts_tac prems 1), |
|
4395 | 1195 |
(IntPr.fast_tac 1) ])); |
286 | 1196 |
\end{ttbox} |
1197 |
The following rewrite rules about conjunction are a selection of those |
|
1198 |
proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the |
|
1199 |
standard simpset. |
|
1200 |
\begin{ttbox} |
|
4395 | 1201 |
val conj_simps = map int_prove_fun |
286 | 1202 |
["P & True <-> P", "True & P <-> P", |
1203 |
"P & False <-> False", "False & P <-> False", |
|
1204 |
"P & P <-> P", |
|
1205 |
"P & ~P <-> False", "~P & P <-> False", |
|
1206 |
"(P & Q) & R <-> P & (Q & R)"]; |
|
1207 |
\end{ttbox} |
|
1208 |
The file also proves some distributive laws. As they can cause exponential |
|
1209 |
blowup, they will not be included in the standard simpset. Instead they |
|
323 | 1210 |
are merely bound to an \ML{} identifier, for user reference. |
286 | 1211 |
\begin{ttbox} |
4395 | 1212 |
val distrib_simps = map int_prove_fun |
286 | 1213 |
["P & (Q | R) <-> P&Q | P&R", |
1214 |
"(Q | R) & P <-> Q&P | R&P", |
|
1215 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
|
1216 |
\end{ttbox} |
|
1217 |
||
1218 |
||
1219 |
\subsection{Functions for preprocessing the rewrite rules} |
|
323 | 1220 |
\label{sec:setmksimps} |
4395 | 1221 |
\begin{ttbox}\indexbold{*setmksimps} |
1222 |
setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4} |
|
1223 |
\end{ttbox} |
|
286 | 1224 |
The next step is to define the function for preprocessing rewrite rules. |
1225 |
This will be installed by calling {\tt setmksimps} below. Preprocessing |
|
1226 |
occurs whenever rewrite rules are added, whether by user command or |
|
1227 |
automatically. Preprocessing involves extracting atomic rewrites at the |
|
1228 |
object-level, then reflecting them to the meta-level. |
|
1229 |
||
1230 |
To start, the function {\tt gen_all} strips any meta-level |
|
1231 |
quantifiers from the front of the given theorem. Usually there are none |
|
1232 |
anyway. |
|
1233 |
\begin{ttbox} |
|
1234 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
|
1235 |
\end{ttbox} |
|
1236 |
The function {\tt atomize} analyses a theorem in order to extract |
|
1237 |
atomic rewrite rules. The head of all the patterns, matched by the |
|
1238 |
wildcard~{\tt _}, is the coercion function {\tt Trueprop}. |
|
1239 |
\begin{ttbox} |
|
1240 |
fun atomize th = case concl_of th of |
|
1241 |
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at |
|
1242 |
atomize(th RS conjunct2) |
|
1243 |
| _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp) |
|
1244 |
| _ $ (Const("All",_) $ _) => atomize(th RS spec) |
|
1245 |
| _ $ (Const("True",_)) => [] |
|
1246 |
| _ $ (Const("False",_)) => [] |
|
1247 |
| _ => [th]; |
|
1248 |
\end{ttbox} |
|
1249 |
There are several cases, depending upon the form of the conclusion: |
|
1250 |
\begin{itemize} |
|
1251 |
\item Conjunction: extract rewrites from both conjuncts. |
|
1252 |
||
1253 |
\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and |
|
1254 |
extract rewrites from~$Q$; these will be conditional rewrites with the |
|
1255 |
condition~$P$. |
|
1256 |
||
1257 |
\item Universal quantification: remove the quantifier, replacing the bound |
|
1258 |
variable by a schematic variable, and extract rewrites from the body. |
|
1259 |
||
1260 |
\item {\tt True} and {\tt False} contain no useful rewrites. |
|
1261 |
||
1262 |
\item Anything else: return the theorem in a singleton list. |
|
1263 |
\end{itemize} |
|
1264 |
The resulting theorems are not literally atomic --- they could be |
|
323 | 1265 |
disjunctive, for example --- but are broken down as much as possible. See |
286 | 1266 |
the file {\tt ZF/simpdata.ML} for a sophisticated translation of |
1267 |
set-theoretic formulae into rewrite rules. |
|
104 | 1268 |
|
286 | 1269 |
The simplified rewrites must now be converted into meta-equalities. The |
323 | 1270 |
rule {\tt eq_reflection} converts equality rewrites, while {\tt |
286 | 1271 |
iff_reflection} converts if-and-only-if rewrites. The latter possibility |
1272 |
can arise in two other ways: the negative theorem~$\neg P$ is converted to |
|
323 | 1273 |
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to |
286 | 1274 |
$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt |
1275 |
iff_reflection_T} accomplish this conversion. |
|
1276 |
\begin{ttbox} |
|
1277 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
|
1278 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
1279 |
\ttbreak |
|
1280 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
1281 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
1282 |
\end{ttbox} |
|
1283 |
The function {\tt mk_meta_eq} converts a theorem to a meta-equality |
|
1284 |
using the case analysis described above. |
|
1285 |
\begin{ttbox} |
|
1286 |
fun mk_meta_eq th = case concl_of th of |
|
1287 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection |
|
1288 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
|
1289 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
|
1290 |
| _ => th RS iff_reflection_T; |
|
1291 |
\end{ttbox} |
|
1292 |
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will |
|
1293 |
be composed together and supplied below to {\tt setmksimps}. |
|
1294 |
||
1295 |
||
1296 |
\subsection{Making the initial simpset} |
|
4395 | 1297 |
|
1298 |
It is time to assemble these items. We open module {\tt Simplifier} |
|
1299 |
to gain direct access to its components. We define the infix operator |
|
1300 |
\ttindex{addcongs} to insert congruence rules; given a list of |
|
1301 |
theorems, it converts their conclusions into meta-equalities and |
|
1302 |
passes them to \ttindex{addeqcongs}. |
|
286 | 1303 |
\begin{ttbox} |
1304 |
open Simplifier; |
|
1305 |
\ttbreak |
|
4395 | 1306 |
infix 4 addcongs; |
286 | 1307 |
fun ss addcongs congs = |
1308 |
ss addeqcongs (congs RL [eq_reflection,iff_reflection]); |
|
1309 |
\end{ttbox} |
|
4395 | 1310 |
Furthermore, we define the infix operator \ttindex{addsplits} |
1311 |
providing a convenient interface for adding split tactics. |
|
286 | 1312 |
\begin{ttbox} |
4395 | 1313 |
infix 4 addsplits; |
1314 |
fun ss addsplits splits = ss addloop (split_tac splits); |
|
1315 |
\end{ttbox} |
|
1316 |
||
1317 |
The list {\tt IFOL_simps} contains the default rewrite rules for |
|
1318 |
first-order logic. The first of these is the reflexive law expressed |
|
1319 |
as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is |
|
1320 |
clearly useless. |
|
1321 |
\begin{ttbox} |
|
1322 |
val IFOL_simps = |
|
1323 |
[refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at |
|
1324 |
imp_simps \at iff_simps \at quant_simps; |
|
286 | 1325 |
\end{ttbox} |
1326 |
The list {\tt triv_rls} contains trivial theorems for the solver. Any |
|
1327 |
subgoal that is simplified to one of these will be removed. |
|
1328 |
\begin{ttbox} |
|
1329 |
val notFalseI = int_prove_fun "~False"; |
|
1330 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
|
1331 |
\end{ttbox} |
|
323 | 1332 |
% |
4395 | 1333 |
The basic simpset for intuitionistic \FOL{} is |
1334 |
\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt |
|
1335 |
gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified |
|
1336 |
subgoals using {\tt triv_rls} and assumptions, and by detecting |
|
1337 |
contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of |
|
1338 |
conditional rewrites. |
|
1339 |
||
1340 |
Other simpsets built from {\tt FOL_basic_ss} will inherit these items. |
|
1341 |
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt |
|
1342 |
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later |
|
1343 |
extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg |
|
1344 |
P\bimp P$. |
|
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
1345 |
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} |
286 | 1346 |
\index{*addsimps}\index{*addcongs} |
1347 |
\begin{ttbox} |
|
4395 | 1348 |
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems), |
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
1349 |
atac, etac FalseE]; |
4395 | 1350 |
|
1351 |
fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems), |
|
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
1352 |
eq_assume_tac, ematch_tac [FalseE]]; |
4395 | 1353 |
|
1354 |
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
|
1355 |
addsimprocs [defALL_regroup,defEX_regroup] |
|
1356 |
setSSolver safe_solver |
|
1357 |
setSolver unsafe_solver |
|
1358 |
setmksimps (map mk_meta_eq o atomize o gen_all); |
|
1359 |
||
1360 |
val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps) |
|
1361 |
addcongs [imp_cong]; |
|
286 | 1362 |
\end{ttbox} |
1363 |
This simpset takes {\tt imp_cong} as a congruence rule in order to use |
|
1364 |
contextual information to simplify the conclusions of implications: |
|
1365 |
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp |
|
1366 |
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) |
|
1367 |
\] |
|
1368 |
By adding the congruence rule {\tt conj_cong}, we could obtain a similar |
|
1369 |
effect for conjunctions. |
|
1370 |
||
1371 |
||
1372 |
\subsection{Case splitting} |
|
323 | 1373 |
To set up case splitting, we must prove the theorem below and pass it to |
1374 |
\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses |
|
1375 |
{\tt mk_meta_eq}, defined above, to convert the splitting rules to |
|
1376 |
meta-equalities. |
|
286 | 1377 |
\begin{ttbox} |
1378 |
val meta_iffD = |
|
1379 |
prove_goal FOL.thy "[| P==Q; Q |] ==> P" |
|
1380 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) |
|
1381 |
\ttbreak |
|
1382 |
fun split_tac splits = |
|
1383 |
mk_case_split_tac meta_iffD (map mk_meta_eq splits); |
|
1384 |
\end{ttbox} |
|
1385 |
% |
|
323 | 1386 |
The splitter replaces applications of a given function; the right-hand side |
1387 |
of the replacement can be anything. For example, here is a splitting rule |
|
1388 |
for conditional expressions: |
|
286 | 1389 |
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x})) |
1390 |
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) |
|
1391 |
\] |
|
323 | 1392 |
Another example is the elimination operator (which happens to be |
1393 |
called~$split$) for Cartesian products: |
|
286 | 1394 |
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = |
1395 |
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) |
|
1396 |
\] |
|
1397 |
Case splits should be allowed only when necessary; they are expensive |
|
4395 | 1398 |
and hard to control. Here is an example of use, where {\tt expand_if} |
1399 |
is the first rule above: |
|
286 | 1400 |
\begin{ttbox} |
4395 | 1401 |
by (simp_tac (simpset() addloop (split_tac [expand_if])) 1); |
1402 |
\end{ttbox} |
|
1403 |
Users would usually prefer the following shortcut using |
|
1404 |
\ttindex{addsplits}: |
|
1405 |
\begin{ttbox} |
|
1406 |
by (simp_tac (simpset() addsplits [expand_if]) 1); |
|
286 | 1407 |
\end{ttbox} |
1408 |
||
104 | 1409 |
|
4395 | 1410 |
\subsection{Theory data for implicit simpsets} |
1411 |
\begin{ttbox}\indexbold{*simpset_thy_data} |
|
1412 |
simpset_thy_data: string * (object * (object -> object) * |
|
1413 |
(object * object -> object) * (Sign.sg -> object -> unit)) |
|
1414 |
\end{ttbox} |
|
1415 |
||
1416 |
Theory data for implicit simpsets has to be set up explicitly. The |
|
1417 |
simplifier already provides an appropriate data kind definition |
|
1418 |
record. This has to be installed into the base theory of any new |
|
1419 |
object-logic as \ttindexbold{thy_data} within the \texttt{ML} section. |
|
1420 |
||
1421 |
This is done at the end of \texttt{IFOL.thy} as follows: |
|
1422 |
\begin{ttbox} |
|
1423 |
ML val thy_data = [Simplifier.simpset_thy_data]; |
|
1424 |
\end{ttbox} |
|
1425 |
||
104 | 1426 |
|
1427 |
\index{simplification|)} |