author | bulwahn |
Thu, 21 Jul 2011 08:33:57 +0200 | |
changeset 43938 | 78a0a2ad91a3 |
parent 42925 | c6c4f997ad87 |
child 45645 | 4014bc2a09ff |
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 |
|
339 |
\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} |
|
340 |
\begin{ttbox} |
|
341 |
addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
342 |
delcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
343 |
addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
344 |
deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
|
345 |
\end{ttbox} |
|
346 |
||
104 | 347 |
Congruence rules are meta-equalities of the form |
3108 | 348 |
\[ \dots \Imp |
104 | 349 |
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}). |
350 |
\] |
|
323 | 351 |
This governs the simplification of the arguments of~$f$. For |
104 | 352 |
example, some arguments can be simplified under additional assumptions: |
353 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}} |
|
354 |
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2}) |
|
355 |
\] |
|
4395 | 356 |
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite |
357 |
rules from it when simplifying~$P@2$. Such local assumptions are |
|
358 |
effective for rewriting formulae such as $x=0\imp y+x=y$. The local |
|
359 |
assumptions are also provided as theorems to the solver; see |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
360 |
{\S}~\ref{sec:simp-solver} below. |
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
361 |
|
4395 | 362 |
\begin{ttdescription} |
363 |
||
364 |
\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the |
|
365 |
simpset $ss$. These are derived from $thms$ in an appropriate way, |
|
366 |
depending on the underlying object-logic. |
|
367 |
||
368 |
\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules |
|
369 |
derived from $thms$. |
|
370 |
||
371 |
\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in |
|
372 |
their internal form (conclusions using meta-equality) to simpset |
|
373 |
$ss$. This is the basic mechanism that \texttt{addcongs} is built |
|
374 |
on. It should be rarely used directly. |
|
375 |
||
376 |
\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules |
|
377 |
in internal form from simpset $ss$. |
|
378 |
||
379 |
\end{ttdescription} |
|
380 |
||
381 |
\medskip |
|
382 |
||
383 |
Here are some more examples. The congruence rule for bounded |
|
384 |
quantifiers also supplies contextual information, this time about the |
|
385 |
bound variable: |
|
286 | 386 |
\begin{eqnarray*} |
387 |
&&\List{\Var{A}=\Var{B};\; |
|
388 |
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\ |
|
389 |
&&\qquad\qquad |
|
390 |
(\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x)) |
|
391 |
\end{eqnarray*} |
|
323 | 392 |
The congruence rule for conditional expressions can supply contextual |
393 |
information for simplifying the arms: |
|
104 | 394 |
\[ \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
|
395 |
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp |
104 | 396 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d}) |
397 |
\] |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
398 |
A congruence rule can also {\em prevent\/} simplification of some arguments. |
104 | 399 |
Here is an alternative congruence rule for conditional expressions: |
400 |
\[ \Var{p}=\Var{q} \Imp |
|
401 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b}) |
|
402 |
\] |
|
403 |
Only the first argument is simplified; the others remain unchanged. |
|
404 |
This can make simplification much faster, but may require an extra case split |
|
405 |
to prove the goal. |
|
406 |
||
407 |
||
4395 | 408 |
\subsection{*The subgoaler}\label{sec:simp-subgoaler} |
409 |
\begin{ttbox} |
|
7990 | 410 |
setsubgoaler : |
411 |
simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4} |
|
4395 | 412 |
prems_of_ss : simpset -> thm list |
413 |
\end{ttbox} |
|
414 |
||
104 | 415 |
The subgoaler is the tactic used to solve subgoals arising out of |
416 |
conditional rewrite rules or congruence rules. The default should be |
|
4395 | 417 |
simplification itself. Occasionally this strategy needs to be |
418 |
changed. For example, if the premise of a conditional rule is an |
|
419 |
instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} |
|
420 |
< \Var{n}$, the default strategy could loop. |
|
104 | 421 |
|
4395 | 422 |
\begin{ttdescription} |
423 |
||
424 |
\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of |
|
425 |
$ss$ to $tacf$. The function $tacf$ will be applied to the current |
|
426 |
simplifier context expressed as a simpset. |
|
427 |
||
428 |
\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of |
|
429 |
premises from simplifier context $ss$. This may be non-empty only |
|
430 |
if the simplifier has been told to utilize local assumptions in the |
|
431 |
first place, e.g.\ if invoked via \texttt{asm_simp_tac}. |
|
432 |
||
433 |
\end{ttdescription} |
|
434 |
||
435 |
As an example, consider the following subgoaler: |
|
104 | 436 |
\begin{ttbox} |
4395 | 437 |
fun subgoaler ss = |
438 |
assume_tac ORELSE' |
|
439 |
resolve_tac (prems_of_ss ss) ORELSE' |
|
440 |
asm_simp_tac ss; |
|
104 | 441 |
\end{ttbox} |
4395 | 442 |
This tactic first tries to solve the subgoal by assumption or by |
443 |
resolving with with one of the premises, calling simplification only |
|
444 |
if that fails. |
|
445 |
||
104 | 446 |
|
698
23734672dc12
updated discussion of congruence rules in first section
lcp
parents:
332
diff
changeset
|
447 |
\subsection{*The solver}\label{sec:simp-solver} |
4395 | 448 |
\begin{ttbox} |
7620 | 449 |
mk_solver : string -> (thm list -> int -> tactic) -> solver |
450 |
setSolver : simpset * solver -> simpset \hfill{\bf infix 4} |
|
451 |
addSolver : simpset * solver -> simpset \hfill{\bf infix 4} |
|
452 |
setSSolver : simpset * solver -> simpset \hfill{\bf infix 4} |
|
453 |
addSSolver : simpset * solver -> simpset \hfill{\bf infix 4} |
|
4395 | 454 |
\end{ttbox} |
455 |
||
7620 | 456 |
A solver is a tactic that attempts to solve a subgoal after |
4395 | 457 |
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
|
458 |
\texttt{True} and $t=t$. It could use sophisticated means such as {\tt |
4395 | 459 |
blast_tac}, though that could make simplification expensive. |
7620 | 460 |
To keep things more abstract, solvers are packaged up in type |
461 |
\texttt{solver}. The only way to create a solver is via \texttt{mk_solver}. |
|
286 | 462 |
|
3108 | 463 |
Rewriting does not instantiate unknowns. For example, rewriting |
464 |
cannot prove $a\in \Var{A}$ since this requires |
|
465 |
instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic |
|
466 |
and may instantiate unknowns as it pleases. This is the only way the |
|
467 |
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
|
468 |
contains extra variables. When a simplification tactic is to be |
3108 | 469 |
combined with other provers, especially with the classical reasoner, |
4395 | 470 |
it is important whether it can be considered safe or not. For this |
7620 | 471 |
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
|
472 |
|
3108 | 473 |
The standard simplification strategy solely uses the unsafe solver, |
4395 | 474 |
which is appropriate in most cases. For special applications where |
3108 | 475 |
the simplification process is not allowed to instantiate unknowns |
4395 | 476 |
within the goal, simplification starts with the safe solver, but may |
477 |
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
|
478 |
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
|
479 |
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
|
480 |
in other subgoals. |
4395 | 481 |
|
482 |
\begin{ttdescription} |
|
7620 | 483 |
\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver; |
484 |
the string $s$ is only attached as a comment and has no other significance. |
|
485 |
||
4395 | 486 |
\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the |
487 |
\emph{safe} solver of $ss$. |
|
488 |
||
489 |
\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an |
|
490 |
additional \emph{safe} solver; it will be tried after the solvers |
|
491 |
which had already been present in $ss$. |
|
492 |
||
493 |
\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the |
|
494 |
unsafe solver of $ss$. |
|
495 |
||
496 |
\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an |
|
497 |
additional unsafe solver; it will be tried after the solvers which |
|
498 |
had already been present in $ss$. |
|
323 | 499 |
|
4395 | 500 |
\end{ttdescription} |
501 |
||
502 |
\medskip |
|
104 | 503 |
|
4395 | 504 |
\index{assumptions!in simplification} The solver tactic is invoked |
505 |
with a list of theorems, namely assumptions that hold in the local |
|
506 |
context. This may be non-empty only if the simplifier has been told |
|
507 |
to utilize local assumptions in the first place, e.g.\ if invoked via |
|
508 |
\texttt{asm_simp_tac}. The solver is also presented the full goal |
|
509 |
including its assumptions in any case. Thus it can use these (e.g.\ |
|
510 |
by calling \texttt{assume_tac}), even if the list of premises is not |
|
511 |
passed. |
|
512 |
||
513 |
\medskip |
|
514 |
||
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
515 |
As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used |
4395 | 516 |
to solve the premises of congruence rules. These are usually of the |
517 |
form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$ |
|
518 |
needs to be instantiated with the result. Typically, the subgoaler |
|
519 |
will invoke the simplifier at some point, which will eventually call |
|
520 |
the solver. For this reason, solver tactics must be prepared to solve |
|
521 |
goals of the form $t = \Var{x}$, usually by reflexivity. In |
|
522 |
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
|
523 |
tactics like \texttt{blast_tac}. |
323 | 524 |
|
3108 | 525 |
It may even happen that due to simplification the subgoal is no longer |
526 |
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
|
527 |
$\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
|
528 |
with the theorem $\neg False$. |
104 | 529 |
|
4395 | 530 |
\medskip |
531 |
||
104 | 532 |
\begin{warn} |
13938 | 533 |
If a premise of a congruence rule cannot be proved, then the |
534 |
congruence is ignored. This should only happen if the rule is |
|
535 |
\emph{conditional} --- that is, contains premises not of the form $t |
|
536 |
= \Var{x}$; otherwise it indicates that some congruence rule, or |
|
537 |
possibly the subgoaler or solver, is faulty. |
|
104 | 538 |
\end{warn} |
539 |
||
323 | 540 |
|
4395 | 541 |
\subsection{*The looper}\label{sec:simp-looper} |
542 |
\begin{ttbox} |
|
5549 | 543 |
setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4} |
544 |
addloop : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4} |
|
545 |
delloop : simpset * string -> simpset \hfill{\bf infix 4} |
|
4395 | 546 |
addsplits : simpset * thm list -> simpset \hfill{\bf infix 4} |
5549 | 547 |
delsplits : simpset * thm list -> simpset \hfill{\bf infix 4} |
4395 | 548 |
\end{ttbox} |
549 |
||
5549 | 550 |
The looper is a list of tactics that are applied after simplification, in case |
4395 | 551 |
the solver failed to solve the simplified goal. If the looper |
552 |
succeeds, the simplification process is started all over again. Each |
|
553 |
of the subgoals generated by the looper is attacked in turn, in |
|
554 |
reverse order. |
|
555 |
||
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
556 |
A typical looper is \index{case splitting}: the expansion of a conditional. |
4395 | 557 |
Another possibility is to apply an elimination rule on the |
558 |
assumptions. More adventurous loopers could start an induction. |
|
559 |
||
560 |
\begin{ttdescription} |
|
561 |
||
5549 | 562 |
\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper |
563 |
tactic of $ss$. |
|
4395 | 564 |
|
5549 | 565 |
\item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional |
566 |
looper tactic with name $name$; it will be tried after the looper tactics |
|
567 |
that had already been present in $ss$. |
|
568 |
||
569 |
\item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$ |
|
570 |
from $ss$. |
|
4395 | 571 |
|
572 |
\item[$ss$ \ttindexbold{addsplits} $thms$] adds |
|
5549 | 573 |
split tactics for $thms$ as additional looper tactics of $ss$. |
574 |
||
575 |
\item[$ss$ \ttindexbold{addsplits} $thms$] deletes the |
|
576 |
split tactics for $thms$ from the looper tactics of $ss$. |
|
4395 | 577 |
|
578 |
\end{ttdescription} |
|
579 |
||
5549 | 580 |
The splitter replaces applications of a given function; the right-hand side |
581 |
of the replacement can be anything. For example, here is a splitting rule |
|
582 |
for conditional expressions: |
|
583 |
\[ \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
|
584 |
\conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) |
5549 | 585 |
\] |
8136 | 586 |
Another example is the elimination operator for Cartesian products (which |
587 |
happens to be called~$split$): |
|
5549 | 588 |
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} = |
589 |
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) |
|
590 |
\] |
|
591 |
||
592 |
For technical reasons, there is a distinction between case splitting in the |
|
593 |
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
|
594 |
\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
|
595 |
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
|
596 |
\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
|
597 |
\texttt{option.split_asm}, which split the subgoal. |
5549 | 598 |
The operator \texttt{addsplits} automatically takes care of which tactic to |
599 |
call, analyzing the form of the rules given as argument. |
|
600 |
\begin{warn} |
|
601 |
Due to \texttt{split_asm_tac}, the simplifier may split subgoals! |
|
602 |
\end{warn} |
|
603 |
||
604 |
Case splits should be allowed only when necessary; they are expensive |
|
605 |
and hard to control. Here is an example of use, where \texttt{split_if} |
|
606 |
is the first rule above: |
|
607 |
\begin{ttbox} |
|
8136 | 608 |
by (simp_tac (simpset() |
609 |
addloop ("split if", split_tac [split_if])) 1); |
|
5549 | 610 |
\end{ttbox} |
5776 | 611 |
Users would usually prefer the following shortcut using \texttt{addsplits}: |
5549 | 612 |
\begin{ttbox} |
613 |
by (simp_tac (simpset() addsplits [split_if]) 1); |
|
614 |
\end{ttbox} |
|
8136 | 615 |
Case-splitting on conditional expressions is usually beneficial, so it is |
616 |
enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}. |
|
104 | 617 |
|
618 |
||
4395 | 619 |
\section{The simplification tactics}\label{simp-tactics} |
620 |
\index{simplification!tactics}\index{tactics!simplification} |
|
621 |
\begin{ttbox} |
|
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
622 |
generic_simp_tac : bool -> bool * bool * bool -> |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
623 |
simpset -> int -> tactic |
4395 | 624 |
simp_tac : simpset -> int -> tactic |
625 |
asm_simp_tac : simpset -> int -> tactic |
|
626 |
full_simp_tac : simpset -> int -> tactic |
|
627 |
asm_full_simp_tac : simpset -> int -> tactic |
|
628 |
safe_asm_full_simp_tac : simpset -> int -> tactic |
|
629 |
\end{ttbox} |
|
2567 | 630 |
|
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
631 |
\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
|
632 |
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
|
633 |
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
|
634 |
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
|
635 |
rewrite rules are solved recursively before the rewrite rule is applied. |
104 | 636 |
|
4395 | 637 |
\begin{ttdescription} |
638 |
||
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
639 |
\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
|
640 |
gives direct access to the various simplification modes: |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
641 |
\begin{itemize} |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
642 |
\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
|
643 |
{\S}\ref{sec:simp-solver}, |
9398
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
644 |
\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
|
645 |
\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
|
646 |
rules, and |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
647 |
\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
|
648 |
than being processed from left to right. |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
649 |
\end{itemize} |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
650 |
This generic interface is intended |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
651 |
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
|
652 |
classical reasoner. It is rarely used directly. |
0ee9b2819155
removed safe_asm_full_simp_tac, added generic_simp_tac
oheimb
parents:
8136
diff
changeset
|
653 |
|
4395 | 654 |
\item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac}, |
655 |
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are |
|
656 |
the basic simplification tactics that work exactly like their |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
657 |
namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are |
4395 | 658 |
explicitly supplied with a simpset. |
659 |
||
660 |
\end{ttdescription} |
|
104 | 661 |
|
4395 | 662 |
\medskip |
104 | 663 |
|
4395 | 664 |
Local modifications of simpsets within a proof are often much cleaner |
665 |
by using above tactics in conjunction with explicit simpsets, rather |
|
666 |
than their capitalized counterparts. For example |
|
1213 | 667 |
\begin{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
668 |
Addsimps \(thms\); |
2479 | 669 |
by (Simp_tac \(i\)); |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
670 |
Delsimps \(thms\); |
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
671 |
\end{ttbox} |
4395 | 672 |
can be expressed more appropriately as |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
673 |
\begin{ttbox} |
4395 | 674 |
by (simp_tac (simpset() addsimps \(thms\)) \(i\)); |
1213 | 675 |
\end{ttbox} |
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
676 |
|
4395 | 677 |
\medskip |
678 |
||
679 |
Also note that functions depending implicitly on the current theory |
|
680 |
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
|
681 |
{\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of |
4395 | 682 |
actual proof scripts. In particular, ML programs like theory |
683 |
definition packages or special tactics should refer to simpsets only |
|
684 |
explicitly, via the above tactics used in conjunction with |
|
685 |
\texttt{simpset_of} or the \texttt{SIMPSET} tacticals. |
|
686 |
||
1860
71bfeecfa96c
Documented simplification tactics which make use of the implicit simpset.
nipkow
parents:
1387
diff
changeset
|
687 |
|
5370 | 688 |
\section{Forward rules and conversions} |
689 |
\index{simplification!forward rules}\index{simplification!conversions} |
|
690 |
\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 | 691 |
simplify : simpset -> thm -> thm |
692 |
asm_simplify : simpset -> thm -> thm |
|
693 |
full_simplify : simpset -> thm -> thm |
|
5370 | 694 |
asm_full_simplify : simpset -> thm -> thm\medskip |
695 |
Simplifier.rewrite : simpset -> cterm -> thm |
|
696 |
Simplifier.asm_rewrite : simpset -> cterm -> thm |
|
697 |
Simplifier.full_rewrite : simpset -> cterm -> thm |
|
698 |
Simplifier.asm_full_rewrite : simpset -> cterm -> thm |
|
4395 | 699 |
\end{ttbox} |
700 |
||
5370 | 701 |
The first four of these functions provide \emph{forward} rules for |
702 |
simplification. Their effect is analogous to the corresponding |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
703 |
tactics described in {\S}\ref{simp-tactics}, but affect the whole |
5370 | 704 |
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
|
705 |
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
|
706 |
{\S}\ref{sec:simp-solver} is omitted in forward simplification. |
5370 | 707 |
|
708 |
The latter four are \emph{conversions}, establishing proven equations |
|
709 |
of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as |
|
710 |
argument. |
|
4395 | 711 |
|
712 |
\begin{warn} |
|
5370 | 713 |
Forward simplification rules and conversions should be used rarely |
714 |
in ordinary proof scripts. The main intention is to provide an |
|
715 |
internal interface to the simplifier for special utilities. |
|
4395 | 716 |
\end{warn} |
717 |
||
718 |
||
332 | 719 |
\section{Permutative rewrite rules} |
323 | 720 |
\index{rewrite rules!permutative|(} |
721 |
||
722 |
A rewrite rule is {\bf permutative} if the left-hand side and right-hand |
|
723 |
side are the same up to renaming of variables. The most common permutative |
|
724 |
rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z = |
|
725 |
(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$ |
|
726 |
for sets. Such rules are common enough to merit special attention. |
|
727 |
||
4395 | 728 |
Because ordinary rewriting loops given such rules, the simplifier |
729 |
employs a special strategy, called {\bf ordered |
|
730 |
rewriting}\index{rewriting!ordered}. There is a standard |
|
731 |
lexicographic ordering on terms. This should be perfectly OK in most |
|
732 |
cases, but can be changed for special applications. |
|
733 |
||
4947 | 734 |
\begin{ttbox} |
735 |
settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4} |
|
736 |
\end{ttbox} |
|
4395 | 737 |
\begin{ttdescription} |
738 |
||
739 |
\item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as |
|
740 |
term order in simpset $ss$. |
|
741 |
||
742 |
\end{ttdescription} |
|
743 |
||
744 |
\medskip |
|
323 | 745 |
|
4395 | 746 |
A permutative rewrite rule is applied only if it decreases the given |
747 |
term with respect to this ordering. For example, commutativity |
|
748 |
rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less |
|
749 |
than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also |
|
750 |
employs ordered rewriting. |
|
751 |
||
752 |
Permutative rewrite rules are added to simpsets just like other |
|
753 |
rewrite rules; the simplifier recognizes their special status |
|
754 |
automatically. They are most effective in the case of |
|
755 |
associative-commutative operators. (Associativity by itself is not |
|
756 |
permutative.) When dealing with an AC-operator~$f$, keep the |
|
757 |
following points in mind: |
|
323 | 758 |
\begin{itemize}\index{associative-commutative operators} |
4395 | 759 |
|
760 |
\item The associative law must always be oriented from left to right, |
|
761 |
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
|
762 |
used with commutativity, leads to looping in conjunction with the |
|
763 |
standard term order. |
|
323 | 764 |
|
765 |
\item To complete your set of rewrite rules, you must add not just |
|
766 |
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
|
767 |
left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
323 | 768 |
\end{itemize} |
769 |
Ordered rewriting with the combination of A, C, and~LC sorts a term |
|
770 |
lexicographically: |
|
771 |
\[\def\maps#1{\stackrel{#1}{\longmapsto}} |
|
772 |
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \] |
|
773 |
Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many |
|
774 |
examples; other algebraic structures are amenable to ordered rewriting, |
|
775 |
such as boolean rings. |
|
776 |
||
3108 | 777 |
\subsection{Example: sums of natural numbers} |
4395 | 778 |
|
9695 | 779 |
This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory |
780 |
\thydx{Arith} contains natural numbers arithmetic. Its associated simpset |
|
781 |
contains many arithmetic laws including distributivity of~$\times$ over~$+$, |
|
782 |
while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on |
|
783 |
type \texttt{nat}. Let us prove the theorem |
|
323 | 784 |
\[ \sum@{i=1}^n i = n\times(n+1)/2. \] |
785 |
% |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
786 |
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
|
787 |
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
|
788 |
extend \texttt{Arith} as follows: |
323 | 789 |
\begin{ttbox} |
790 |
NatSum = Arith + |
|
1387 | 791 |
consts sum :: [nat=>nat, nat] => nat |
9445
6c93b1eb11f8
Corrected example which still used old primrec syntax.
berghofe
parents:
9398
diff
changeset
|
792 |
primrec |
4245 | 793 |
"sum f 0 = 0" |
794 |
"sum f (Suc n) = f(n) + sum f n" |
|
323 | 795 |
end |
796 |
\end{ttbox} |
|
4245 | 797 |
The \texttt{primrec} declaration automatically adds rewrite rules for |
4557 | 798 |
\texttt{sum} to the default simpset. We now remove the |
799 |
\texttt{nat_cancel} simplification procedures (in order not to spoil |
|
800 |
the example) and insert the AC-rules for~$+$: |
|
323 | 801 |
\begin{ttbox} |
4557 | 802 |
Delsimprocs nat_cancel; |
4245 | 803 |
Addsimps add_ac; |
323 | 804 |
\end{ttbox} |
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
805 |
Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) = |
323 | 806 |
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: |
807 |
\begin{ttbox} |
|
5205 | 808 |
Goal "2 * sum (\%i.i) (Suc n) = n * Suc n"; |
323 | 809 |
{\out Level 0} |
3108 | 810 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
811 |
{\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n} |
|
323 | 812 |
\end{ttbox} |
3108 | 813 |
Induction should not be applied until the goal is in the simplest |
814 |
form: |
|
323 | 815 |
\begin{ttbox} |
4245 | 816 |
by (Simp_tac 1); |
323 | 817 |
{\out Level 1} |
3108 | 818 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
819 |
{\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} |
|
323 | 820 |
\end{ttbox} |
3108 | 821 |
Ordered rewriting has sorted the terms in the left-hand side. The |
822 |
subgoal is now ready for induction: |
|
323 | 823 |
\begin{ttbox} |
4245 | 824 |
by (induct_tac "n" 1); |
323 | 825 |
{\out Level 2} |
3108 | 826 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
827 |
{\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0} |
|
323 | 828 |
\ttbreak |
4245 | 829 |
{\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n} |
8136 | 830 |
{\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =} |
4245 | 831 |
{\out Suc n * Suc n} |
323 | 832 |
\end{ttbox} |
833 |
Simplification proves both subgoals immediately:\index{*ALLGOALS} |
|
834 |
\begin{ttbox} |
|
4245 | 835 |
by (ALLGOALS Asm_simp_tac); |
323 | 836 |
{\out Level 3} |
3108 | 837 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
323 | 838 |
{\out No subgoals!} |
839 |
\end{ttbox} |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
840 |
Simplification cannot prove the induction step if we omit \texttt{add_ac} from |
4245 | 841 |
the simpset. Observe that like terms have not been collected: |
323 | 842 |
\begin{ttbox} |
4245 | 843 |
{\out Level 3} |
844 |
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n} |
|
845 |
{\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n} |
|
8136 | 846 |
{\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =} |
4245 | 847 |
{\out n + (n + (n + n * n))} |
323 | 848 |
\end{ttbox} |
849 |
Ordered rewriting proves this by sorting the left-hand side. Proving |
|
850 |
arithmetic theorems without ordered rewriting requires explicit use of |
|
851 |
commutativity. This is tedious; try it and see! |
|
852 |
||
853 |
Ordered rewriting is equally successful in proving |
|
854 |
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. |
|
855 |
||
856 |
||
857 |
\subsection{Re-orienting equalities} |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
858 |
Ordered rewriting with the derived rule \texttt{symmetry} can reverse |
4557 | 859 |
equations: |
323 | 860 |
\begin{ttbox} |
861 |
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" |
|
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3112
diff
changeset
|
862 |
(fn _ => [Blast_tac 1]); |
323 | 863 |
\end{ttbox} |
864 |
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs |
|
865 |
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
|
866 |
For example, ordered rewriting with \texttt{symmetry} can prove the goal |
323 | 867 |
\[ 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
|
868 |
Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$ |
323 | 869 |
because $f(a)$ is lexicographically greater than $b$ and~$c$. These |
870 |
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the |
|
871 |
conclusion by~$f(a)$. |
|
872 |
||
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
873 |
Another example is the goal $\neg(t=u) \imp \neg(u=t)$. |
323 | 874 |
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
|
875 |
rewriting with \texttt{symmetry} makes the equalities agree. (Without |
323 | 876 |
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$ |
877 |
or~$u=t$.) Then the simplifier can prove the goal outright. |
|
878 |
||
879 |
\index{rewrite rules!permutative|)} |
|
880 |
||
881 |
||
7990 | 882 |
\section{*Setting up the Simplifier}\label{sec:setting-up-simp} |
323 | 883 |
\index{simplification!setting up} |
286 | 884 |
|
9712 | 885 |
Setting up the simplifier for new logics is complicated in the general case. |
886 |
This section describes how the simplifier is installed for intuitionistic |
|
887 |
first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the |
|
888 |
Isabelle sources. |
|
286 | 889 |
|
16019 | 890 |
The case splitting tactic, which resides on a separate files, is not part of |
891 |
Pure Isabelle. It needs to be loaded explicitly by the object-logic as |
|
892 |
follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}): |
|
286 | 893 |
\begin{ttbox} |
6569 | 894 |
use "\~\relax\~\relax/src/Provers/splitter.ML"; |
286 | 895 |
\end{ttbox} |
896 |
||
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
897 |
Simplification requires converting object-equalities to meta-level rewrite |
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
898 |
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
|
899 |
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
|
900 |
\texttt{FOL/IFOL.thy} contains the two lines |
323 | 901 |
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} |
286 | 902 |
eq_reflection "(x=y) ==> (x==y)" |
903 |
iff_reflection "(P<->Q) ==> (P==Q)" |
|
904 |
\end{ttbox} |
|
323 | 905 |
Of course, you should only assert such rules if they are true for your |
286 | 906 |
particular logic. In Constructive Type Theory, equality is a ternary |
4395 | 907 |
relation of the form $a=b\in A$; the type~$A$ determines the meaning |
908 |
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
|
909 |
present simplifier cannot be used. Rewriting in \texttt{CTT} uses |
4395 | 910 |
another simplifier, which resides in the file {\tt |
911 |
Provers/typedsimp.ML} and is not documented. Even this does not |
|
912 |
work for later variants of Constructive Type Theory that use |
|
323 | 913 |
intensional equality~\cite{nordstrom90}. |
286 | 914 |
|
915 |
||
916 |
\subsection{A collection of standard rewrite rules} |
|
4557 | 917 |
|
918 |
We first prove lots of standard rewrite rules about the logical |
|
919 |
connectives. These include cancellation and associative laws. We |
|
920 |
define a function that echoes the desired law and then supplies it the |
|
9695 | 921 |
prover for intuitionistic FOL: |
286 | 922 |
\begin{ttbox} |
923 |
fun int_prove_fun s = |
|
924 |
(writeln s; |
|
925 |
prove_goal IFOL.thy s |
|
926 |
(fn prems => [ (cut_facts_tac prems 1), |
|
4395 | 927 |
(IntPr.fast_tac 1) ])); |
286 | 928 |
\end{ttbox} |
929 |
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
|
930 |
proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the |
286 | 931 |
standard simpset. |
932 |
\begin{ttbox} |
|
4395 | 933 |
val conj_simps = map int_prove_fun |
286 | 934 |
["P & True <-> P", "True & P <-> P", |
935 |
"P & False <-> False", "False & P <-> False", |
|
936 |
"P & P <-> P", |
|
937 |
"P & ~P <-> False", "~P & P <-> False", |
|
938 |
"(P & Q) & R <-> P & (Q & R)"]; |
|
939 |
\end{ttbox} |
|
940 |
The file also proves some distributive laws. As they can cause exponential |
|
941 |
blowup, they will not be included in the standard simpset. Instead they |
|
323 | 942 |
are merely bound to an \ML{} identifier, for user reference. |
286 | 943 |
\begin{ttbox} |
4395 | 944 |
val distrib_simps = map int_prove_fun |
286 | 945 |
["P & (Q | R) <-> P&Q | P&R", |
946 |
"(Q | R) & P <-> Q&P | R&P", |
|
947 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"]; |
|
948 |
\end{ttbox} |
|
949 |
||
950 |
||
951 |
\subsection{Functions for preprocessing the rewrite rules} |
|
323 | 952 |
\label{sec:setmksimps} |
4395 | 953 |
\begin{ttbox}\indexbold{*setmksimps} |
954 |
setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4} |
|
955 |
\end{ttbox} |
|
286 | 956 |
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
|
957 |
This will be installed by calling \texttt{setmksimps} below. Preprocessing |
286 | 958 |
occurs whenever rewrite rules are added, whether by user command or |
959 |
automatically. Preprocessing involves extracting atomic rewrites at the |
|
960 |
object-level, then reflecting them to the meta-level. |
|
961 |
||
12725 | 962 |
To start, the function \texttt{gen_all} strips any meta-level |
12717 | 963 |
quantifiers from the front of the given theorem. |
5549 | 964 |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
965 |
The function \texttt{atomize} analyses a theorem in order to extract |
286 | 966 |
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
|
967 |
wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}. |
286 | 968 |
\begin{ttbox} |
969 |
fun atomize th = case concl_of th of |
|
970 |
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at |
|
971 |
atomize(th RS conjunct2) |
|
972 |
| _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp) |
|
973 |
| _ $ (Const("All",_) $ _) => atomize(th RS spec) |
|
974 |
| _ $ (Const("True",_)) => [] |
|
975 |
| _ $ (Const("False",_)) => [] |
|
976 |
| _ => [th]; |
|
977 |
\end{ttbox} |
|
978 |
There are several cases, depending upon the form of the conclusion: |
|
979 |
\begin{itemize} |
|
980 |
\item Conjunction: extract rewrites from both conjuncts. |
|
981 |
\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and |
|
982 |
extract rewrites from~$Q$; these will be conditional rewrites with the |
|
983 |
condition~$P$. |
|
984 |
\item Universal quantification: remove the quantifier, replacing the bound |
|
985 |
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
|
986 |
\item \texttt{True} and \texttt{False} contain no useful rewrites. |
286 | 987 |
\item Anything else: return the theorem in a singleton list. |
988 |
\end{itemize} |
|
989 |
The resulting theorems are not literally atomic --- they could be |
|
5549 | 990 |
disjunctive, for example --- but are broken down as much as possible. |
991 |
See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of |
|
992 |
set-theoretic formulae into rewrite rules. |
|
993 |
||
994 |
For standard situations like the above, |
|
995 |
there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a |
|
996 |
list of pairs $(name, thms)$, where $name$ is an operator name and |
|
997 |
$thms$ is a list of theorems to resolve with in case the pattern matches, |
|
998 |
and returns a suitable \texttt{atomize} function. |
|
999 |
||
104 | 1000 |
|
286 | 1001 |
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
|
1002 |
rule \texttt{eq_reflection} converts equality rewrites, while {\tt |
286 | 1003 |
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
|
1004 |
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
|
1005 |
$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
|
1006 |
$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt |
286 | 1007 |
iff_reflection_T} accomplish this conversion. |
1008 |
\begin{ttbox} |
|
1009 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)"; |
|
1010 |
val iff_reflection_F = P_iff_F RS iff_reflection; |
|
1011 |
\ttbreak |
|
1012 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)"; |
|
1013 |
val iff_reflection_T = P_iff_T RS iff_reflection; |
|
1014 |
\end{ttbox} |
|
5549 | 1015 |
The function \texttt{mk_eq} converts a theorem to a meta-equality |
286 | 1016 |
using the case analysis described above. |
1017 |
\begin{ttbox} |
|
5549 | 1018 |
fun mk_eq th = case concl_of th of |
286 | 1019 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection |
1020 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection |
|
1021 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F |
|
1022 |
| _ => th RS iff_reflection_T; |
|
1023 |
\end{ttbox} |
|
11162
9e2ec5f02217
debugging: replaced gen_all by forall_elim_vars_safe
oheimb
parents:
9712
diff
changeset
|
1024 |
The |
12725 | 1025 |
three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} |
5549 | 1026 |
will be composed together and supplied below to \texttt{setmksimps}. |
286 | 1027 |
|
1028 |
||
1029 |
\subsection{Making the initial simpset} |
|
4395 | 1030 |
|
9712 | 1031 |
It is time to assemble these items. The list \texttt{IFOL_simps} contains the |
1032 |
default rewrite rules for intuitionistic first-order logic. The first of |
|
1033 |
these is the reflexive law expressed as the equivalence |
|
1034 |
$(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless. |
|
4395 | 1035 |
\begin{ttbox} |
1036 |
val IFOL_simps = |
|
1037 |
[refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at |
|
1038 |
imp_simps \at iff_simps \at quant_simps; |
|
286 | 1039 |
\end{ttbox} |
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
1040 |
The list \texttt{triv_rls} contains trivial theorems for the solver. Any |
286 | 1041 |
subgoal that is simplified to one of these will be removed. |
1042 |
\begin{ttbox} |
|
1043 |
val notFalseI = int_prove_fun "~False"; |
|
1044 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI]; |
|
1045 |
\end{ttbox} |
|
9712 | 1046 |
We also define the function \ttindex{mk_meta_cong} to convert the conclusion |
1047 |
of congruence rules into meta-equalities. |
|
1048 |
\begin{ttbox} |
|
1049 |
fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl)); |
|
1050 |
\end{ttbox} |
|
323 | 1051 |
% |
9695 | 1052 |
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
|
1053 |
preprocess rewrites using |
12725 | 1054 |
{\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}. |
9695 | 1055 |
It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by |
1056 |
detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals |
|
1057 |
of conditional rewrites. |
|
4395 | 1058 |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
1059 |
Other simpsets built from \texttt{FOL_basic_ss} will inherit these items. |
4395 | 1060 |
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt |
1061 |
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11162
diff
changeset
|
1062 |
extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg |
4395 | 1063 |
P\bimp P$. |
2628
1fe7c9f599c2
description of del(eq)congs, safe and unsafe solver
oheimb
parents:
2613
diff
changeset
|
1064 |
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler} |
286 | 1065 |
\index{*addsimps}\index{*addcongs} |
1066 |
\begin{ttbox} |
|
4395 | 1067 |
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
|
1068 |
atac, etac FalseE]; |
4395 | 1069 |
|
8136 | 1070 |
fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems), |
1071 |
eq_assume_tac, ematch_tac [FalseE]]; |
|
4395 | 1072 |
|
9712 | 1073 |
val FOL_basic_ss = |
8136 | 1074 |
empty_ss setsubgoaler asm_simp_tac |
1075 |
addsimprocs [defALL_regroup, defEX_regroup] |
|
1076 |
setSSolver safe_solver |
|
1077 |
setSolver unsafe_solver |
|
12725 | 1078 |
setmksimps (map mk_eq o atomize o gen_all) |
9712 | 1079 |
setmkcong mk_meta_cong; |
4395 | 1080 |
|
8136 | 1081 |
val IFOL_ss = |
1082 |
FOL_basic_ss addsimps (IFOL_simps {\at} |
|
1083 |
int_ex_simps {\at} int_all_simps) |
|
1084 |
addcongs [imp_cong]; |
|
286 | 1085 |
\end{ttbox} |
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
1086 |
This simpset takes \texttt{imp_cong} as a congruence rule in order to use |
286 | 1087 |
contextual information to simplify the conclusions of implications: |
1088 |
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp |
|
1089 |
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'}) |
|
1090 |
\] |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4560
diff
changeset
|
1091 |
By adding the congruence rule \texttt{conj_cong}, we could obtain a similar |
286 | 1092 |
effect for conjunctions. |
1093 |
||
1094 |
||
104 | 1095 |
\index{simplification|)} |
5370 | 1096 |
|
1097 |
||
1098 |
%%% Local Variables: |
|
1099 |
%%% mode: latex |
|
1100 |
%%% TeX-master: "ref" |
|
1101 |
%%% End: |