104
|
1 |
%% $Id$
|
|
2 |
\chapter{Simplification} \label{simp-chap}
|
|
3 |
\index{simplification|(}
|
|
4 |
|
|
5 |
This chapter describes Isabelle's generic simplification package, which
|
323
|
6 |
provides a suite of simplification tactics. It performs conditional and
|
|
7 |
unconditional rewriting and uses contextual information (`local
|
|
8 |
assumptions'). It provides a few general hooks, which can provide
|
|
9 |
automatic case splits during rewriting, for example. The simplifier is set
|
|
10 |
up for many of Isabelle's logics: {\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt
|
|
11 |
HOL}.
|
104
|
12 |
|
|
13 |
|
286
|
14 |
\section{Simplification sets}\index{simplification sets}
|
104
|
15 |
The simplification tactics are controlled by {\bf simpsets}. These consist
|
|
16 |
of five components: rewrite rules, congruence rules, the subgoaler, the
|
323
|
17 |
solver and the looper. The simplifier should be set up with sensible
|
|
18 |
defaults so that most simplifier calls specify only rewrite rules.
|
|
19 |
Experienced users can exploit the other components to streamline proofs.
|
|
20 |
|
104
|
21 |
|
332
|
22 |
\subsection{Rewrite rules}
|
|
23 |
\index{rewrite rules|(}
|
323
|
24 |
Rewrite rules are theorems expressing some form of equality:
|
|
25 |
\begin{eqnarray*}
|
|
26 |
Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\
|
|
27 |
\Var{P}\conj\Var{P} &\bimp& \Var{P} \\
|
|
28 |
\Var{A} \union \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
|
|
29 |
\end{eqnarray*}
|
|
30 |
{\bf Conditional} rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
|
|
31 |
0$ are permitted; the conditions can be arbitrary terms. The infix
|
|
32 |
operation \ttindex{addsimps} adds new rewrite rules, while
|
|
33 |
\ttindex{delsimps} deletes rewrite rules from a simpset.
|
104
|
34 |
|
323
|
35 |
Internally, all rewrite rules are translated into meta-equalities, theorems
|
|
36 |
with conclusion $lhs \equiv rhs$. Each simpset contains a function for
|
|
37 |
extracting equalities from arbitrary theorems. For example,
|
|
38 |
$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv
|
|
39 |
False$. This function can be installed using \ttindex{setmksimps} but only
|
|
40 |
the definer of a logic should need to do this; see \S\ref{sec:setmksimps}.
|
|
41 |
The function processes theorems added by \ttindex{addsimps} as well as
|
|
42 |
local assumptions.
|
104
|
43 |
|
|
44 |
|
332
|
45 |
\begin{warn}
|
104
|
46 |
The left-hand side of a rewrite rule must look like a first-order term:
|
332
|
47 |
none of its unknowns should have arguments. Hence
|
|
48 |
${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ is
|
|
49 |
acceptable. Even $\neg(\forall x.\Var{P}(x)) \bimp (\exists
|
|
50 |
x.\neg\Var{P}(x))$ is acceptable because its left-hand side is
|
|
51 |
$\neg(All(\Var{P}))$ after $\eta$-contraction. But ${\Var{f}(\Var{x})\in
|
|
52 |
{\tt range}(\Var{f})} = True$ is not acceptable. However, you can
|
|
53 |
replace the offending subterms by adding new variables and conditions:
|
|
54 |
$\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$
|
|
55 |
is acceptable as a conditional rewrite rule.
|
104
|
56 |
\end{warn}
|
|
57 |
|
332
|
58 |
\index{rewrite rules|)}
|
|
59 |
|
|
60 |
\subsection{*Congruence rules}\index{congruence rules}
|
104
|
61 |
Congruence rules are meta-equalities of the form
|
|
62 |
\[ \List{\dots} \Imp
|
|
63 |
f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
|
|
64 |
\]
|
323
|
65 |
This governs the simplification of the arguments of~$f$. For
|
104
|
66 |
example, some arguments can be simplified under additional assumptions:
|
|
67 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
|
|
68 |
\Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
|
|
69 |
\]
|
323
|
70 |
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules
|
|
71 |
from it when simplifying~$P@2$. Such local assumptions are effective for
|
|
72 |
rewriting formulae such as $x=0\imp y+x=y$. The congruence rule for bounded
|
|
73 |
quantifiers can also supply contextual information:
|
286
|
74 |
\begin{eqnarray*}
|
|
75 |
&&\List{\Var{A}=\Var{B};\;
|
|
76 |
\Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
|
|
77 |
&&\qquad\qquad
|
|
78 |
(\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
|
|
79 |
\end{eqnarray*}
|
323
|
80 |
The congruence rule for conditional expressions can supply contextual
|
|
81 |
information for simplifying the arms:
|
104
|
82 |
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
|
|
83 |
\neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
|
|
84 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
|
|
85 |
\]
|
|
86 |
|
|
87 |
A congruence rule can also suppress simplification of certain arguments.
|
|
88 |
Here is an alternative congruence rule for conditional expressions:
|
|
89 |
\[ \Var{p}=\Var{q} \Imp
|
|
90 |
if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
|
|
91 |
\]
|
|
92 |
Only the first argument is simplified; the others remain unchanged.
|
|
93 |
This can make simplification much faster, but may require an extra case split
|
|
94 |
to prove the goal.
|
|
95 |
|
286
|
96 |
Congruence rules are added using \ttindexbold{addeqcongs}. Their conclusion
|
104
|
97 |
must be a meta-equality, as in the examples above. It is more
|
|
98 |
natural to derive the rules with object-logic equality, for example
|
|
99 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
|
|
100 |
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}),
|
|
101 |
\]
|
286
|
102 |
Each object-logic should define an operator called \ttindex{addcongs} that
|
|
103 |
expects object-equalities and translates them into meta-equalities.
|
104
|
104 |
|
323
|
105 |
\subsection{*The subgoaler}
|
104
|
106 |
The subgoaler is the tactic used to solve subgoals arising out of
|
|
107 |
conditional rewrite rules or congruence rules. The default should be
|
|
108 |
simplification itself. Occasionally this strategy needs to be changed. For
|
|
109 |
example, if the premise of a conditional rule is an instance of its
|
|
110 |
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the
|
|
111 |
default strategy could loop.
|
|
112 |
|
|
113 |
The subgoaler can be set explicitly with \ttindex{setsubgoaler}. For
|
|
114 |
example, the subgoaler
|
|
115 |
\begin{ttbox}
|
332
|
116 |
fun subgoal_tac ss = assume_tac ORELSE'
|
|
117 |
resolve_tac (prems_of_ss ss) ORELSE'
|
104
|
118 |
asm_simp_tac ss;
|
|
119 |
\end{ttbox}
|
332
|
120 |
tries to solve the subgoal by assumption or with one of the premises, calling
|
104
|
121 |
simplification only if that fails; here {\tt prems_of_ss} extracts the
|
|
122 |
current premises from a simpset.
|
|
123 |
|
323
|
124 |
\subsection{*The solver}
|
286
|
125 |
The solver is a tactic that attempts to solve a subgoal after
|
|
126 |
simplification. Typically it just proves trivial subgoals such as {\tt
|
323
|
127 |
True} and $t=t$. It could use sophisticated means such as {\tt
|
|
128 |
fast_tac}, though that could make simplification expensive. The solver
|
|
129 |
is set using \ttindex{setsolver}.
|
286
|
130 |
|
323
|
131 |
Rewriting does not instantiate unknowns. For example, rewriting cannot
|
|
132 |
prove $a\in \Var{A}$ since this requires instantiating~$\Var{A}$. The
|
|
133 |
solver, however, is an arbitrary tactic and may instantiate unknowns as it
|
|
134 |
pleases. This is the only way the simplifier can handle a conditional
|
|
135 |
rewrite rule whose condition contains extra variables.
|
|
136 |
|
|
137 |
\index{assumptions!in simplification}
|
286
|
138 |
The tactic is presented with the full goal, including the asssumptions.
|
|
139 |
Hence it can use those assumptions (say by calling {\tt assume_tac}) even
|
|
140 |
inside {\tt simp_tac}, which otherwise does not use assumptions. The
|
|
141 |
solver is also supplied a list of theorems, namely assumptions that hold in
|
|
142 |
the local context.
|
104
|
143 |
|
323
|
144 |
The subgoaler is also used to solve the premises of congruence rules, which
|
|
145 |
are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and
|
|
146 |
$\Var{x}$ needs to be instantiated with the result. Hence the subgoaler
|
|
147 |
should call the simplifier at some point. The simplifier will then call the
|
|
148 |
solver, which must therefore be prepared to solve goals of the form $t =
|
|
149 |
\Var{x}$, usually by reflexivity. In particular, reflexivity should be
|
|
150 |
tried before any of the fancy tactics like {\tt fast_tac}.
|
|
151 |
|
|
152 |
It may even happen that, due to simplification, the subgoal is no longer an
|
|
153 |
equality. For example $False \bimp \Var{Q}$ could be rewritten to
|
|
154 |
$\neg\Var{Q}$. To cover this case, the solver could try resolving with the
|
|
155 |
theorem $\neg False$.
|
104
|
156 |
|
|
157 |
\begin{warn}
|
|
158 |
If the simplifier aborts with the message {\tt Failed congruence proof!},
|
323
|
159 |
then the subgoaler or solver has failed to prove a premise of a
|
|
160 |
congruence rule. This should never occur and indicates that the
|
|
161 |
subgoaler or solver is faulty.
|
104
|
162 |
\end{warn}
|
|
163 |
|
323
|
164 |
|
|
165 |
\subsection{*The looper}
|
104
|
166 |
The looper is a tactic that is applied after simplification, in case the
|
|
167 |
solver failed to solve the simplified goal. If the looper succeeds, the
|
|
168 |
simplification process is started all over again. Each of the subgoals
|
|
169 |
generated by the looper is attacked in turn, in reverse order. A
|
|
170 |
typical looper is case splitting: the expansion of a conditional. Another
|
|
171 |
possibility is to apply an elimination rule on the assumptions. More
|
|
172 |
adventurous loopers could start an induction. The looper is set with
|
|
173 |
\ttindex{setloop}.
|
|
174 |
|
|
175 |
|
|
176 |
\begin{figure}
|
323
|
177 |
\index{*simpset ML type}
|
|
178 |
\index{*simp_tac}
|
|
179 |
\index{*asm_simp_tac}
|
|
180 |
\index{*asm_full_simp_tac}
|
|
181 |
\index{*addeqcongs}
|
|
182 |
\index{*addsimps}
|
|
183 |
\index{*delsimps}
|
|
184 |
\index{*empty_ss}
|
|
185 |
\index{*merge_ss}
|
|
186 |
\index{*setsubgoaler}
|
|
187 |
\index{*setsolver}
|
|
188 |
\index{*setloop}
|
|
189 |
\index{*setmksimps}
|
|
190 |
\index{*prems_of_ss}
|
|
191 |
\index{*rep_ss}
|
104
|
192 |
\begin{ttbox}
|
|
193 |
infix addsimps addeqcongs delsimps
|
|
194 |
setsubgoaler setsolver setloop setmksimps;
|
|
195 |
|
|
196 |
signature SIMPLIFIER =
|
|
197 |
sig
|
|
198 |
type simpset
|
|
199 |
val simp_tac: simpset -> int -> tactic
|
|
200 |
val asm_simp_tac: simpset -> int -> tactic
|
133
|
201 |
val asm_full_simp_tac: simpset -> int -> tactic\smallskip
|
|
202 |
val addeqcongs: simpset * thm list -> simpset
|
|
203 |
val addsimps: simpset * thm list -> simpset
|
|
204 |
val delsimps: simpset * thm list -> simpset
|
104
|
205 |
val empty_ss: simpset
|
|
206 |
val merge_ss: simpset * simpset -> simpset
|
|
207 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
|
|
208 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset
|
|
209 |
val setloop: simpset * (int -> tactic) -> simpset
|
|
210 |
val setmksimps: simpset * (thm -> thm list) -> simpset
|
|
211 |
val prems_of_ss: simpset -> thm list
|
|
212 |
val rep_ss: simpset -> \{simps: thm list, congs: thm list\}
|
|
213 |
end;
|
|
214 |
\end{ttbox}
|
323
|
215 |
\caption{The simplifier primitives} \label{SIMPLIFIER}
|
104
|
216 |
\end{figure}
|
|
217 |
|
|
218 |
|
|
219 |
\section{The simplification tactics} \label{simp-tactics}
|
323
|
220 |
\index{simplification!tactics}
|
|
221 |
\index{tactics!simplification}
|
104
|
222 |
|
|
223 |
The actual simplification work is performed by the following tactics. The
|
|
224 |
rewriting strategy is strictly bottom up, except for congruence rules, which
|
|
225 |
are applied while descending into a term. Conditions in conditional rewrite
|
|
226 |
rules are solved recursively before the rewrite rule is applied.
|
|
227 |
|
|
228 |
There are three basic simplification tactics:
|
323
|
229 |
\begin{ttdescription}
|
104
|
230 |
\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules
|
|
231 |
in~$ss$. It may solve the subgoal completely if it has become trivial,
|
|
232 |
using the solver.
|
|
233 |
|
323
|
234 |
\item[\ttindexbold{asm_simp_tac}]\index{assumptions!in simplification}
|
|
235 |
is like \verb$simp_tac$, but extracts additional rewrite rules from the
|
|
236 |
assumptions.
|
104
|
237 |
|
332
|
238 |
\item[\ttindexbold{asm_full_simp_tac}]
|
|
239 |
is like \verb$asm_simp_tac$, but also simplifies the assumptions one by
|
|
240 |
one. Working from left to right, it uses each assumption in the
|
|
241 |
simplification of those following.
|
323
|
242 |
\end{ttdescription}
|
104
|
243 |
Using the simplifier effectively may take a bit of experimentation. The
|
|
244 |
tactics can be traced with the ML command \verb$trace_simp := true$. To
|
|
245 |
remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
|
|
246 |
return its simplification and congruence rules.
|
|
247 |
|
286
|
248 |
\section{Examples using the simplifier}
|
323
|
249 |
\index{examples!of simplification}
|
104
|
250 |
Assume we are working within {\tt FOL} and that
|
323
|
251 |
\begin{ttdescription}
|
|
252 |
\item[Nat.thy]
|
|
253 |
is a theory including the constants $0$, $Suc$ and $+$,
|
|
254 |
\item[add_0]
|
|
255 |
is the rewrite rule $0+\Var{n} = \Var{n}$,
|
|
256 |
\item[add_Suc]
|
|
257 |
is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$,
|
|
258 |
\item[induct]
|
|
259 |
is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp
|
|
260 |
\Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
|
|
261 |
\item[FOL_ss]
|
|
262 |
is a basic simpset for {\tt FOL}.%
|
332
|
263 |
\footnote{These examples reside on the file {\tt FOL/ex/Nat.ML}.}
|
323
|
264 |
\end{ttdescription}
|
104
|
265 |
|
|
266 |
We create a simpset for natural numbers by extending~{\tt FOL_ss}:
|
|
267 |
\begin{ttbox}
|
|
268 |
val add_ss = FOL_ss addsimps [add_0, add_Suc];
|
|
269 |
\end{ttbox}
|
323
|
270 |
|
|
271 |
\subsection{A trivial example}
|
286
|
272 |
Proofs by induction typically involve simplification. Here is a proof
|
|
273 |
that~0 is a right identity:
|
104
|
274 |
\begin{ttbox}
|
|
275 |
goal Nat.thy "m+0 = m";
|
|
276 |
{\out Level 0}
|
|
277 |
{\out m + 0 = m}
|
|
278 |
{\out 1. m + 0 = m}
|
286
|
279 |
\end{ttbox}
|
|
280 |
The first step is to perform induction on the variable~$m$. This returns a
|
|
281 |
base case and inductive step as two subgoals:
|
|
282 |
\begin{ttbox}
|
104
|
283 |
by (res_inst_tac [("n","m")] induct 1);
|
|
284 |
{\out Level 1}
|
|
285 |
{\out m + 0 = m}
|
|
286 |
{\out 1. 0 + 0 = 0}
|
|
287 |
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
|
|
288 |
\end{ttbox}
|
286
|
289 |
Simplification solves the first subgoal trivially:
|
104
|
290 |
\begin{ttbox}
|
|
291 |
by (simp_tac add_ss 1);
|
|
292 |
{\out Level 2}
|
|
293 |
{\out m + 0 = m}
|
|
294 |
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
|
|
295 |
\end{ttbox}
|
|
296 |
The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the
|
|
297 |
induction hypothesis as a rewrite rule:
|
|
298 |
\begin{ttbox}
|
|
299 |
by (asm_simp_tac add_ss 1);
|
|
300 |
{\out Level 3}
|
|
301 |
{\out m + 0 = m}
|
|
302 |
{\out No subgoals!}
|
|
303 |
\end{ttbox}
|
|
304 |
|
323
|
305 |
\subsection{An example of tracing}
|
|
306 |
Let us prove a similar result involving more complex terms. The two
|
|
307 |
equations together can be used to prove that addition is commutative.
|
104
|
308 |
\begin{ttbox}
|
|
309 |
goal Nat.thy "m+Suc(n) = Suc(m+n)";
|
|
310 |
{\out Level 0}
|
|
311 |
{\out m + Suc(n) = Suc(m + n)}
|
|
312 |
{\out 1. m + Suc(n) = Suc(m + n)}
|
286
|
313 |
\end{ttbox}
|
|
314 |
We again perform induction on~$m$ and get two subgoals:
|
|
315 |
\begin{ttbox}
|
104
|
316 |
by (res_inst_tac [("n","m")] induct 1);
|
|
317 |
{\out Level 1}
|
|
318 |
{\out m + Suc(n) = Suc(m + n)}
|
|
319 |
{\out 1. 0 + Suc(n) = Suc(0 + n)}
|
286
|
320 |
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==>}
|
|
321 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
|
|
322 |
\end{ttbox}
|
|
323 |
Simplification solves the first subgoal, this time rewriting two
|
|
324 |
occurrences of~0:
|
|
325 |
\begin{ttbox}
|
104
|
326 |
by (simp_tac add_ss 1);
|
|
327 |
{\out Level 2}
|
|
328 |
{\out m + Suc(n) = Suc(m + n)}
|
286
|
329 |
{\out 1. !!x. x + Suc(n) = Suc(x + n) ==>}
|
|
330 |
{\out Suc(x) + Suc(n) = Suc(Suc(x) + n)}
|
104
|
331 |
\end{ttbox}
|
|
332 |
Switching tracing on illustrates how the simplifier solves the remaining
|
|
333 |
subgoal:
|
|
334 |
\begin{ttbox}
|
|
335 |
trace_simp := true;
|
|
336 |
by (asm_simp_tac add_ss 1);
|
323
|
337 |
\ttbreak
|
104
|
338 |
{\out Rewriting:}
|
|
339 |
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))}
|
323
|
340 |
\ttbreak
|
104
|
341 |
{\out Rewriting:}
|
|
342 |
{\out x + Suc(n) == Suc(x + n)}
|
323
|
343 |
\ttbreak
|
104
|
344 |
{\out Rewriting:}
|
|
345 |
{\out Suc(x) + n == Suc(x + n)}
|
323
|
346 |
\ttbreak
|
104
|
347 |
{\out Rewriting:}
|
|
348 |
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True}
|
323
|
349 |
\ttbreak
|
104
|
350 |
{\out Level 3}
|
|
351 |
{\out m + Suc(n) = Suc(m + n)}
|
|
352 |
{\out No subgoals!}
|
|
353 |
\end{ttbox}
|
286
|
354 |
Many variations are possible. At Level~1 (in either example) we could have
|
|
355 |
solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
|
104
|
356 |
\begin{ttbox}
|
|
357 |
by (ALLGOALS (asm_simp_tac add_ss));
|
|
358 |
{\out Level 2}
|
|
359 |
{\out m + Suc(n) = Suc(m + n)}
|
|
360 |
{\out No subgoals!}
|
|
361 |
\end{ttbox}
|
|
362 |
|
323
|
363 |
\subsection{Free variables and simplification}
|
104
|
364 |
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
|
323
|
365 |
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$:
|
104
|
366 |
\begin{ttbox}
|
|
367 |
val [prem] = goal Nat.thy
|
|
368 |
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
|
|
369 |
{\out Level 0}
|
|
370 |
{\out f(i + j) = i + f(j)}
|
|
371 |
{\out 1. f(i + j) = i + f(j)}
|
323
|
372 |
\ttbreak
|
286
|
373 |
{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
|
|
374 |
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
|
323
|
375 |
\end{ttbox}
|
|
376 |
In the theorem~{\tt prem}, note that $f$ is a free variable while
|
|
377 |
$\Var{n}$ is a schematic variable.
|
|
378 |
\begin{ttbox}
|
104
|
379 |
by (res_inst_tac [("n","i")] induct 1);
|
|
380 |
{\out Level 1}
|
|
381 |
{\out f(i + j) = i + f(j)}
|
|
382 |
{\out 1. f(0 + j) = 0 + f(j)}
|
|
383 |
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
|
|
384 |
\end{ttbox}
|
|
385 |
We simplify each subgoal in turn. The first one is trivial:
|
|
386 |
\begin{ttbox}
|
|
387 |
by (simp_tac add_ss 1);
|
|
388 |
{\out Level 2}
|
|
389 |
{\out f(i + j) = i + f(j)}
|
|
390 |
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
|
|
391 |
\end{ttbox}
|
|
392 |
The remaining subgoal requires rewriting by the premise, so we add it to
|
323
|
393 |
{\tt add_ss}:%
|
|
394 |
\footnote{The previous simplifier required congruence rules for function
|
|
395 |
variables like~$f$ in order to simplify their arguments. It was more
|
|
396 |
general than the current simplifier, but harder to use and slower. The
|
|
397 |
present simplifier can be given congruence rules to realize non-standard
|
|
398 |
simplification of a function's arguments, but this is seldom necessary.}
|
104
|
399 |
\begin{ttbox}
|
|
400 |
by (asm_simp_tac (add_ss addsimps [prem]) 1);
|
|
401 |
{\out Level 3}
|
|
402 |
{\out f(i + j) = i + f(j)}
|
|
403 |
{\out No subgoals!}
|
|
404 |
\end{ttbox}
|
|
405 |
|
286
|
406 |
|
332
|
407 |
\section{Permutative rewrite rules}
|
323
|
408 |
\index{rewrite rules!permutative|(}
|
|
409 |
|
|
410 |
A rewrite rule is {\bf permutative} if the left-hand side and right-hand
|
|
411 |
side are the same up to renaming of variables. The most common permutative
|
|
412 |
rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z =
|
|
413 |
(x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
|
|
414 |
for sets. Such rules are common enough to merit special attention.
|
|
415 |
|
|
416 |
Because ordinary rewriting loops given such rules, the simplifier employs a
|
|
417 |
special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}.
|
|
418 |
There is a built-in lexicographic ordering on terms. A permutative rewrite
|
|
419 |
rule is applied only if it decreases the given term with respect to this
|
|
420 |
ordering. For example, commutativity rewrites~$b+a$ to $a+b$, but then
|
|
421 |
stops because $a+b$ is strictly less than $b+a$. The Boyer-Moore theorem
|
|
422 |
prover~\cite{bm88book} also employs ordered rewriting.
|
|
423 |
|
|
424 |
Permutative rewrite rules are added to simpsets just like other rewrite
|
|
425 |
rules; the simplifier recognizes their special status automatically. They
|
|
426 |
are most effective in the case of associative-commutative operators.
|
|
427 |
(Associativity by itself is not permutative.) When dealing with an
|
|
428 |
AC-operator~$f$, keep the following points in mind:
|
|
429 |
\begin{itemize}\index{associative-commutative operators}
|
|
430 |
\item The associative law must always be oriented from left to right, namely
|
|
431 |
$f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if used with
|
|
432 |
commutativity, leads to looping! Future versions of Isabelle may remove
|
|
433 |
this restriction.
|
|
434 |
|
|
435 |
\item To complete your set of rewrite rules, you must add not just
|
|
436 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf
|
|
437 |
left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
|
|
438 |
\end{itemize}
|
|
439 |
Ordered rewriting with the combination of A, C, and~LC sorts a term
|
|
440 |
lexicographically:
|
|
441 |
\[\def\maps#1{\stackrel{#1}{\longmapsto}}
|
|
442 |
(b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \]
|
|
443 |
Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
|
|
444 |
examples; other algebraic structures are amenable to ordered rewriting,
|
|
445 |
such as boolean rings.
|
|
446 |
|
|
447 |
\subsection{Example: sums of integers}
|
|
448 |
This example is set in Isabelle's higher-order logic. Theory
|
|
449 |
\thydx{Arith} contains the theory of arithmetic. The simpset {\tt
|
|
450 |
arith_ss} contains many arithmetic laws including distributivity
|
|
451 |
of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the A, C
|
|
452 |
and LC laws for~$+$. Let us prove the theorem
|
|
453 |
\[ \sum@{i=1}^n i = n\times(n+1)/2. \]
|
|
454 |
%
|
|
455 |
A functional~{\tt sum} represents the summation operator under the
|
|
456 |
interpretation ${\tt sum}(f,n+1) = \sum@{i=0}^n f(i)$. We extend {\tt
|
|
457 |
Arith} using a theory file:
|
|
458 |
\begin{ttbox}
|
|
459 |
NatSum = Arith +
|
|
460 |
consts sum :: "[nat=>nat, nat] => nat"
|
|
461 |
rules sum_0 "sum(f,0) = 0"
|
|
462 |
sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
|
|
463 |
end
|
|
464 |
\end{ttbox}
|
332
|
465 |
After declaring {\tt open NatSum}, we make the required simpset by adding
|
323
|
466 |
the AC-rules for~$+$ and the axioms for~{\tt sum}:
|
|
467 |
\begin{ttbox}
|
|
468 |
val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac);
|
|
469 |
{\out val natsum_ss = SS \{\ldots\} : simpset}
|
|
470 |
\end{ttbox}
|
|
471 |
Our desired theorem now reads ${\tt sum}(\lambda i.i,n+1) =
|
|
472 |
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:
|
|
473 |
\begin{ttbox}
|
|
474 |
goal NatSum.thy "Suc(Suc(0))*sum(\%i.i,Suc(n)) = n*Suc(n)";
|
|
475 |
{\out Level 0}
|
|
476 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
|
|
477 |
{\out 1. Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
|
|
478 |
\end{ttbox}
|
|
479 |
Induction should not be applied until the goal is in the simplest form:
|
|
480 |
\begin{ttbox}
|
|
481 |
by (simp_tac natsum_ss 1);
|
|
482 |
{\out Level 1}
|
|
483 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
|
|
484 |
{\out 1. n + (n + (sum(\%i. i, n) + sum(\%i. i, n))) = n + n * n}
|
|
485 |
\end{ttbox}
|
|
486 |
Ordered rewriting has sorted the terms in the left-hand side.
|
|
487 |
The subgoal is now ready for induction:
|
|
488 |
\begin{ttbox}
|
|
489 |
by (nat_ind_tac "n" 1);
|
|
490 |
{\out Level 2}
|
|
491 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
|
|
492 |
{\out 1. 0 + (0 + (sum(\%i. i, 0) + sum(\%i. i, 0))) = 0 + 0 * 0}
|
|
493 |
\ttbreak
|
|
494 |
{\out 2. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =}
|
|
495 |
{\out n1 + n1 * n1 ==>}
|
|
496 |
{\out Suc(n1) +}
|
|
497 |
{\out (Suc(n1) + (sum(\%i. i, Suc(n1)) + sum(\%i. i, Suc(n1)))) =}
|
|
498 |
{\out Suc(n1) + Suc(n1) * Suc(n1)}
|
|
499 |
\end{ttbox}
|
|
500 |
Simplification proves both subgoals immediately:\index{*ALLGOALS}
|
|
501 |
\begin{ttbox}
|
|
502 |
by (ALLGOALS (asm_simp_tac natsum_ss));
|
|
503 |
{\out Level 3}
|
|
504 |
{\out Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)}
|
|
505 |
{\out No subgoals!}
|
|
506 |
\end{ttbox}
|
|
507 |
If we had omitted {\tt add_ac} from the simpset, simplification would have
|
|
508 |
failed to prove the induction step:
|
|
509 |
\begin{ttbox}
|
|
510 |
Suc(Suc(0)) * sum(\%i. i, Suc(n)) = n * Suc(n)
|
|
511 |
1. !!n1. n1 + (n1 + (sum(\%i. i, n1) + sum(\%i. i, n1))) =
|
|
512 |
n1 + n1 * n1 ==>
|
|
513 |
n1 + (n1 + (n1 + sum(\%i. i, n1) + (n1 + sum(\%i. i, n1)))) =
|
|
514 |
n1 + (n1 + (n1 + n1 * n1))
|
|
515 |
\end{ttbox}
|
|
516 |
Ordered rewriting proves this by sorting the left-hand side. Proving
|
|
517 |
arithmetic theorems without ordered rewriting requires explicit use of
|
|
518 |
commutativity. This is tedious; try it and see!
|
|
519 |
|
|
520 |
Ordered rewriting is equally successful in proving
|
|
521 |
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
|
|
522 |
|
|
523 |
|
|
524 |
\subsection{Re-orienting equalities}
|
|
525 |
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality
|
|
526 |
signs:
|
|
527 |
\begin{ttbox}
|
|
528 |
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
|
|
529 |
(fn _ => [fast_tac HOL_cs 1]);
|
|
530 |
\end{ttbox}
|
|
531 |
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs
|
|
532 |
in the conclusion but not~$s$, can often be brought into the right form.
|
|
533 |
For example, ordered rewriting with {\tt symmetry} can prove the goal
|
|
534 |
\[ f(a)=b \conj f(a)=c \imp b=c. \]
|
|
535 |
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$
|
|
536 |
because $f(a)$ is lexicographically greater than $b$ and~$c$. These
|
|
537 |
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
|
|
538 |
conclusion by~$f(a)$.
|
|
539 |
|
|
540 |
Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
|
|
541 |
The differing orientations make this appear difficult to prove. Ordered
|
|
542 |
rewriting with {\tt symmetry} makes the equalities agree. (Without
|
|
543 |
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
|
|
544 |
or~$u=t$.) Then the simplifier can prove the goal outright.
|
|
545 |
|
|
546 |
\index{rewrite rules!permutative|)}
|
|
547 |
|
|
548 |
|
|
549 |
\section{*Setting up the simplifier}\label{sec:setting-up-simp}
|
|
550 |
\index{simplification!setting up}
|
286
|
551 |
|
|
552 |
Setting up the simplifier for new logics is complicated. This section
|
323
|
553 |
describes how the simplifier is installed for intuitionistic first-order
|
|
554 |
logic; the code is largely taken from {\tt FOL/simpdata.ML}.
|
286
|
555 |
|
323
|
556 |
The simplifier and the case splitting tactic, which reside on separate
|
|
557 |
files, are not part of Pure Isabelle. They must be loaded explicitly:
|
286
|
558 |
\begin{ttbox}
|
|
559 |
use "../Provers/simplifier.ML";
|
|
560 |
use "../Provers/splitter.ML";
|
|
561 |
\end{ttbox}
|
|
562 |
|
|
563 |
Simplification works by reducing various object-equalities to
|
323
|
564 |
meta-equality. It requires rules stating that equal terms and equivalent
|
|
565 |
formulae are also equal at the meta-level. The rule declaration part of
|
|
566 |
the file {\tt FOL/ifol.thy} contains the two lines
|
|
567 |
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
|
286
|
568 |
eq_reflection "(x=y) ==> (x==y)"
|
|
569 |
iff_reflection "(P<->Q) ==> (P==Q)"
|
|
570 |
\end{ttbox}
|
323
|
571 |
Of course, you should only assert such rules if they are true for your
|
286
|
572 |
particular logic. In Constructive Type Theory, equality is a ternary
|
|
573 |
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the
|
332
|
574 |
equality essentially as a partial equivalence relation. The present
|
323
|
575 |
simplifier cannot be used. Rewriting in {\tt CTT} uses another simplifier,
|
|
576 |
which resides in the file {\tt typedsimp.ML} and is not documented. Even
|
|
577 |
this does not work for later variants of Constructive Type Theory that use
|
|
578 |
intensional equality~\cite{nordstrom90}.
|
286
|
579 |
|
|
580 |
|
|
581 |
\subsection{A collection of standard rewrite rules}
|
|
582 |
The file begins by proving lots of standard rewrite rules about the logical
|
323
|
583 |
connectives. These include cancellation and associative laws. To prove
|
|
584 |
them easily, it defines a function that echoes the desired law and then
|
286
|
585 |
supplies it the theorem prover for intuitionistic \FOL:
|
|
586 |
\begin{ttbox}
|
|
587 |
fun int_prove_fun s =
|
|
588 |
(writeln s;
|
|
589 |
prove_goal IFOL.thy s
|
|
590 |
(fn prems => [ (cut_facts_tac prems 1),
|
|
591 |
(Int.fast_tac 1) ]));
|
|
592 |
\end{ttbox}
|
|
593 |
The following rewrite rules about conjunction are a selection of those
|
|
594 |
proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the
|
|
595 |
standard simpset.
|
|
596 |
\begin{ttbox}
|
|
597 |
val conj_rews = map int_prove_fun
|
|
598 |
["P & True <-> P", "True & P <-> P",
|
|
599 |
"P & False <-> False", "False & P <-> False",
|
|
600 |
"P & P <-> P",
|
|
601 |
"P & ~P <-> False", "~P & P <-> False",
|
|
602 |
"(P & Q) & R <-> P & (Q & R)"];
|
|
603 |
\end{ttbox}
|
|
604 |
The file also proves some distributive laws. As they can cause exponential
|
|
605 |
blowup, they will not be included in the standard simpset. Instead they
|
323
|
606 |
are merely bound to an \ML{} identifier, for user reference.
|
286
|
607 |
\begin{ttbox}
|
|
608 |
val distrib_rews = map int_prove_fun
|
|
609 |
["P & (Q | R) <-> P&Q | P&R",
|
|
610 |
"(Q | R) & P <-> Q&P | R&P",
|
|
611 |
"(P | Q --> R) <-> (P --> R) & (Q --> R)"];
|
|
612 |
\end{ttbox}
|
|
613 |
|
|
614 |
|
|
615 |
\subsection{Functions for preprocessing the rewrite rules}
|
323
|
616 |
\label{sec:setmksimps}
|
|
617 |
%
|
286
|
618 |
The next step is to define the function for preprocessing rewrite rules.
|
|
619 |
This will be installed by calling {\tt setmksimps} below. Preprocessing
|
|
620 |
occurs whenever rewrite rules are added, whether by user command or
|
|
621 |
automatically. Preprocessing involves extracting atomic rewrites at the
|
|
622 |
object-level, then reflecting them to the meta-level.
|
|
623 |
|
|
624 |
To start, the function {\tt gen_all} strips any meta-level
|
|
625 |
quantifiers from the front of the given theorem. Usually there are none
|
|
626 |
anyway.
|
|
627 |
\begin{ttbox}
|
|
628 |
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
|
|
629 |
\end{ttbox}
|
|
630 |
The function {\tt atomize} analyses a theorem in order to extract
|
|
631 |
atomic rewrite rules. The head of all the patterns, matched by the
|
|
632 |
wildcard~{\tt _}, is the coercion function {\tt Trueprop}.
|
|
633 |
\begin{ttbox}
|
|
634 |
fun atomize th = case concl_of th of
|
|
635 |
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at
|
|
636 |
atomize(th RS conjunct2)
|
|
637 |
| _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
|
|
638 |
| _ $ (Const("All",_) $ _) => atomize(th RS spec)
|
|
639 |
| _ $ (Const("True",_)) => []
|
|
640 |
| _ $ (Const("False",_)) => []
|
|
641 |
| _ => [th];
|
|
642 |
\end{ttbox}
|
|
643 |
There are several cases, depending upon the form of the conclusion:
|
|
644 |
\begin{itemize}
|
|
645 |
\item Conjunction: extract rewrites from both conjuncts.
|
|
646 |
|
|
647 |
\item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
|
|
648 |
extract rewrites from~$Q$; these will be conditional rewrites with the
|
|
649 |
condition~$P$.
|
|
650 |
|
|
651 |
\item Universal quantification: remove the quantifier, replacing the bound
|
|
652 |
variable by a schematic variable, and extract rewrites from the body.
|
|
653 |
|
|
654 |
\item {\tt True} and {\tt False} contain no useful rewrites.
|
|
655 |
|
|
656 |
\item Anything else: return the theorem in a singleton list.
|
|
657 |
\end{itemize}
|
|
658 |
The resulting theorems are not literally atomic --- they could be
|
323
|
659 |
disjunctive, for example --- but are broken down as much as possible. See
|
286
|
660 |
the file {\tt ZF/simpdata.ML} for a sophisticated translation of
|
|
661 |
set-theoretic formulae into rewrite rules.
|
104
|
662 |
|
286
|
663 |
The simplified rewrites must now be converted into meta-equalities. The
|
323
|
664 |
rule {\tt eq_reflection} converts equality rewrites, while {\tt
|
286
|
665 |
iff_reflection} converts if-and-only-if rewrites. The latter possibility
|
|
666 |
can arise in two other ways: the negative theorem~$\neg P$ is converted to
|
323
|
667 |
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to
|
286
|
668 |
$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt
|
|
669 |
iff_reflection_T} accomplish this conversion.
|
|
670 |
\begin{ttbox}
|
|
671 |
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
|
|
672 |
val iff_reflection_F = P_iff_F RS iff_reflection;
|
|
673 |
\ttbreak
|
|
674 |
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
|
|
675 |
val iff_reflection_T = P_iff_T RS iff_reflection;
|
|
676 |
\end{ttbox}
|
|
677 |
The function {\tt mk_meta_eq} converts a theorem to a meta-equality
|
|
678 |
using the case analysis described above.
|
|
679 |
\begin{ttbox}
|
|
680 |
fun mk_meta_eq th = case concl_of th of
|
|
681 |
_ $ (Const("op =",_)$_$_) => th RS eq_reflection
|
|
682 |
| _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
|
|
683 |
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
|
|
684 |
| _ => th RS iff_reflection_T;
|
|
685 |
\end{ttbox}
|
|
686 |
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will
|
|
687 |
be composed together and supplied below to {\tt setmksimps}.
|
|
688 |
|
|
689 |
|
|
690 |
\subsection{Making the initial simpset}
|
|
691 |
It is time to assemble these items. We open module {\tt Simplifier} to
|
323
|
692 |
gain access to its components. We define the infix operator
|
|
693 |
\ttindexbold{addcongs} to insert congruence rules; given a list of theorems,
|
|
694 |
it converts their conclusions into meta-equalities and passes them to
|
|
695 |
\ttindex{addeqcongs}.
|
286
|
696 |
\begin{ttbox}
|
|
697 |
open Simplifier;
|
|
698 |
\ttbreak
|
|
699 |
infix addcongs;
|
|
700 |
fun ss addcongs congs =
|
|
701 |
ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
|
|
702 |
\end{ttbox}
|
|
703 |
The list {\tt IFOL_rews} contains the default rewrite rules for first-order
|
|
704 |
logic. The first of these is the reflexive law expressed as the
|
323
|
705 |
equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless.
|
286
|
706 |
\begin{ttbox}
|
|
707 |
val IFOL_rews =
|
|
708 |
[refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at
|
|
709 |
imp_rews \at iff_rews \at quant_rews;
|
|
710 |
\end{ttbox}
|
|
711 |
The list {\tt triv_rls} contains trivial theorems for the solver. Any
|
|
712 |
subgoal that is simplified to one of these will be removed.
|
|
713 |
\begin{ttbox}
|
|
714 |
val notFalseI = int_prove_fun "~False";
|
|
715 |
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
|
|
716 |
\end{ttbox}
|
323
|
717 |
%
|
286
|
718 |
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}.
|
|
719 |
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt
|
|
720 |
mk_meta_eq}. It solves simplified subgoals using {\tt triv_rls} and
|
|
721 |
assumptions. It uses \ttindex{asm_simp_tac} to tackle subgoals of
|
|
722 |
conditional rewrites. It takes {\tt IFOL_rews} as rewrite rules.
|
|
723 |
Other simpsets built from {\tt IFOL_ss} will inherit these items.
|
323
|
724 |
In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite
|
|
725 |
rules such as $\neg\neg P\bimp P$.
|
286
|
726 |
\index{*setmksimps}\index{*setsolver}\index{*setsubgoaler}
|
|
727 |
\index{*addsimps}\index{*addcongs}
|
|
728 |
\begin{ttbox}
|
|
729 |
val IFOL_ss =
|
|
730 |
empty_ss
|
|
731 |
setmksimps (map mk_meta_eq o atomize o gen_all)
|
|
732 |
setsolver (fn prems => resolve_tac (triv_rls \at prems) ORELSE'
|
|
733 |
assume_tac)
|
|
734 |
setsubgoaler asm_simp_tac
|
|
735 |
addsimps IFOL_rews
|
|
736 |
addcongs [imp_cong];
|
|
737 |
\end{ttbox}
|
|
738 |
This simpset takes {\tt imp_cong} as a congruence rule in order to use
|
|
739 |
contextual information to simplify the conclusions of implications:
|
|
740 |
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
|
|
741 |
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
|
|
742 |
\]
|
|
743 |
By adding the congruence rule {\tt conj_cong}, we could obtain a similar
|
|
744 |
effect for conjunctions.
|
|
745 |
|
|
746 |
|
|
747 |
\subsection{Case splitting}
|
323
|
748 |
To set up case splitting, we must prove the theorem below and pass it to
|
|
749 |
\ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses
|
|
750 |
{\tt mk_meta_eq}, defined above, to convert the splitting rules to
|
|
751 |
meta-equalities.
|
286
|
752 |
\begin{ttbox}
|
|
753 |
val meta_iffD =
|
|
754 |
prove_goal FOL.thy "[| P==Q; Q |] ==> P"
|
|
755 |
(fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
|
|
756 |
\ttbreak
|
|
757 |
fun split_tac splits =
|
|
758 |
mk_case_split_tac meta_iffD (map mk_meta_eq splits);
|
|
759 |
\end{ttbox}
|
|
760 |
%
|
323
|
761 |
The splitter replaces applications of a given function; the right-hand side
|
|
762 |
of the replacement can be anything. For example, here is a splitting rule
|
|
763 |
for conditional expressions:
|
286
|
764 |
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
|
|
765 |
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
|
|
766 |
\]
|
323
|
767 |
Another example is the elimination operator (which happens to be
|
|
768 |
called~$split$) for Cartesian products:
|
286
|
769 |
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
|
|
770 |
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
|
|
771 |
\]
|
|
772 |
Case splits should be allowed only when necessary; they are expensive
|
|
773 |
and hard to control. Here is a typical example of use, where {\tt
|
|
774 |
expand_if} is the first rule above:
|
|
775 |
\begin{ttbox}
|
|
776 |
by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
|
|
777 |
\end{ttbox}
|
|
778 |
|
104
|
779 |
|
|
780 |
|
|
781 |
\index{simplification|)}
|
|
782 |
|
286
|
783 |
|