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