104
|
1 |
%%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!!
|
|
2 |
\chapter{Simplification} \label{simp-chap}
|
|
3 |
\index{simplification|(}
|
|
4 |
Object-level rewriting is not primitive in Isabelle. For efficiency,
|
|
5 |
perhaps it ought to be. On the other hand, it is difficult to conceive of
|
|
6 |
a general mechanism that could accommodate the diversity of rewriting found
|
|
7 |
in different logics. Hence rewriting in Isabelle works via resolution,
|
|
8 |
using unknowns as place-holders for simplified terms. This chapter
|
|
9 |
describes a generic simplification package, the functor~\ttindex{SimpFun},
|
|
10 |
which expects the basic laws of equational logic and returns a suite of
|
|
11 |
simplification tactics. The code lives in
|
|
12 |
\verb$Provers/simp.ML$.
|
|
13 |
|
|
14 |
This rewriting package is not as general as one might hope (using it for {\tt
|
|
15 |
HOL} is not quite as convenient as it could be; rewriting modulo equations is
|
|
16 |
not supported~\ldots) but works well for many logics. It performs
|
|
17 |
conditional and unconditional rewriting and handles multiple reduction
|
|
18 |
relations and local assumptions. It also has a facility for automatic case
|
|
19 |
splits by expanding conditionals like {\it if-then-else\/} during rewriting.
|
|
20 |
|
|
21 |
For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})
|
|
22 |
the simplifier has been set up already. Hence we start by describing the
|
|
23 |
functions provided by the simplifier --- those functions exported by
|
|
24 |
\ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in
|
286
|
25 |
Fig.\ts\ref{SIMP}.
|
104
|
26 |
|
|
27 |
|
|
28 |
\section{Simplification sets}
|
|
29 |
\index{simplification sets}
|
|
30 |
The simplification tactics are controlled by {\bf simpsets}, which consist of
|
|
31 |
three things:
|
|
32 |
\begin{enumerate}
|
|
33 |
\item {\bf Rewrite rules}, which are theorems like
|
|
34 |
$\Var{m} + succ(\Var{n}) = succ(\Var{m} + \Var{n})$. {\bf Conditional}
|
|
35 |
rewrites such as $m<n \Imp m/n = 0$ are permitted.
|
|
36 |
\index{rewrite rules}
|
|
37 |
|
|
38 |
\item {\bf Congruence rules}, which typically have the form
|
|
39 |
\index{congruence rules}
|
|
40 |
\[ \List{\Var{x@1} = \Var{y@1}; \ldots; \Var{x@n} = \Var{y@n}} \Imp
|
|
41 |
f(\Var{x@1},\ldots,\Var{x@n}) = f(\Var{y@1},\ldots,\Var{y@n}).
|
|
42 |
\]
|
|
43 |
|
|
44 |
\item The {\bf auto-tactic}, which attempts to solve the simplified
|
|
45 |
subgoal, say by recognizing it as a tautology.
|
|
46 |
\end{enumerate}
|
|
47 |
|
|
48 |
\subsection{Congruence rules}
|
|
49 |
Congruence rules enable the rewriter to simplify subterms. Without a
|
|
50 |
congruence rule for the function~$g$, no argument of~$g$ can be rewritten.
|
|
51 |
Congruence rules can be generalized in the following ways:
|
|
52 |
|
|
53 |
{\bf Additional assumptions} are allowed:
|
|
54 |
\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
|
|
55 |
\Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2})
|
|
56 |
\]
|
|
57 |
This rule assumes $Q@1$, and any rewrite rules it contains, while
|
1100
|
58 |
simplifying~$P@2$. Such `local' assumptions are effective for rewriting
|
104
|
59 |
formulae such as $x=0\imp y+x=y$.
|
|
60 |
|
|
61 |
{\bf Additional quantifiers} are allowed, typically for binding operators:
|
|
62 |
\[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp
|
|
63 |
\forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x)
|
|
64 |
\]
|
|
65 |
|
|
66 |
{\bf Different equalities} can be mixed. The following example
|
|
67 |
enables the transition from formula rewriting to term rewriting:
|
|
68 |
\[ \List{\Var{x@1}=\Var{y@1};\Var{x@2}=\Var{y@2}} \Imp
|
|
69 |
(\Var{x@1}=\Var{x@2}) \bimp (\Var{y@1}=\Var{y@2})
|
|
70 |
\]
|
|
71 |
\begin{warn}
|
|
72 |
It is not necessary to assert a separate congruence rule for each constant,
|
|
73 |
provided your logic contains suitable substitution rules. The function {\tt
|
|
74 |
mk_congs} derives congruence rules from substitution
|
|
75 |
rules~\S\ref{simp-tactics}.
|
|
76 |
\end{warn}
|
|
77 |
|
|
78 |
|
|
79 |
\begin{figure}
|
|
80 |
\indexbold{*SIMP}
|
|
81 |
\begin{ttbox}
|
|
82 |
infix 4 addrews addcongs delrews delcongs setauto;
|
|
83 |
signature SIMP =
|
|
84 |
sig
|
|
85 |
type simpset
|
|
86 |
val empty_ss : simpset
|
|
87 |
val addcongs : simpset * thm list -> simpset
|
|
88 |
val addrews : simpset * thm list -> simpset
|
|
89 |
val delcongs : simpset * thm list -> simpset
|
|
90 |
val delrews : simpset * thm list -> simpset
|
|
91 |
val print_ss : simpset -> unit
|
|
92 |
val setauto : simpset * (int -> tactic) -> simpset
|
|
93 |
val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
|
|
94 |
val ASM_SIMP_TAC : simpset -> int -> tactic
|
|
95 |
val CASE_TAC : simpset -> int -> tactic
|
|
96 |
val SIMP_CASE2_TAC : simpset -> int -> tactic
|
|
97 |
val SIMP_THM : simpset -> thm -> thm
|
|
98 |
val SIMP_TAC : simpset -> int -> tactic
|
|
99 |
val SIMP_CASE_TAC : simpset -> int -> tactic
|
|
100 |
val mk_congs : theory -> string list -> thm list
|
|
101 |
val mk_typed_congs : theory -> (string*string) list -> thm list
|
|
102 |
val tracing : bool ref
|
|
103 |
end;
|
|
104 |
\end{ttbox}
|
|
105 |
\caption{The signature {\tt SIMP}} \label{SIMP}
|
|
106 |
\end{figure}
|
|
107 |
|
|
108 |
|
|
109 |
\subsection{The abstract type {\tt simpset}}\label{simp-simpsets}
|
|
110 |
Simpsets are values of the abstract type \ttindexbold{simpset}. They are
|
|
111 |
manipulated by the following functions:
|
|
112 |
\index{simplification sets|bold}
|
323
|
113 |
\begin{ttdescription}
|
104
|
114 |
\item[\ttindexbold{empty_ss}]
|
|
115 |
is the empty simpset. It has no congruence or rewrite rules and its
|
|
116 |
auto-tactic always fails.
|
|
117 |
|
323
|
118 |
\item[$ss$ \ttindexbold{addcongs} $thms$]
|
104
|
119 |
is the simpset~$ss$ plus the congruence rules~$thms$.
|
|
120 |
|
323
|
121 |
\item[$ss$ \ttindexbold{delcongs} $thms$]
|
104
|
122 |
is the simpset~$ss$ minus the congruence rules~$thms$.
|
|
123 |
|
323
|
124 |
\item[$ss$ \ttindexbold{addrews} $thms$]
|
104
|
125 |
is the simpset~$ss$ plus the rewrite rules~$thms$.
|
|
126 |
|
323
|
127 |
\item[$ss$ \ttindexbold{delrews} $thms$]
|
104
|
128 |
is the simpset~$ss$ minus the rewrite rules~$thms$.
|
|
129 |
|
323
|
130 |
\item[$ss$ \ttindexbold{setauto} $tacf$]
|
104
|
131 |
is the simpset~$ss$ with $tacf$ for its auto-tactic.
|
|
132 |
|
|
133 |
\item[\ttindexbold{print_ss} $ss$]
|
|
134 |
prints all the congruence and rewrite rules in the simpset~$ss$.
|
323
|
135 |
\end{ttdescription}
|
104
|
136 |
Adding a rule to a simpset already containing it, or deleting one
|
|
137 |
from a simpset not containing it, generates a warning message.
|
|
138 |
|
|
139 |
In principle, any theorem can be used as a rewrite rule. Before adding a
|
|
140 |
theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the
|
|
141 |
maximum amount of rewriting from it. Thus it need not have the form $s=t$.
|
|
142 |
In {\tt FOL} for example, an atomic formula $P$ is transformed into the
|
|
143 |
rewrite rule $P \bimp True$. This preprocessing is not fixed but logic
|
|
144 |
dependent. The existing logics like {\tt FOL} are fairly clever in this
|
|
145 |
respect. For a more precise description see {\tt mk_rew_rules} in
|
|
146 |
\S\ref{SimpFun-input}.
|
|
147 |
|
|
148 |
The auto-tactic is applied after simplification to solve a goal. This may
|
|
149 |
be the overall goal or some subgoal that arose during conditional
|
|
150 |
rewriting. Calling ${\tt auto_tac}~i$ must either solve exactly
|
|
151 |
subgoal~$i$ or fail. If it succeeds without reducing the number of
|
|
152 |
subgoals by one, havoc and strange exceptions may result.
|
|
153 |
A typical auto-tactic is {\tt ares_tac [TrueI]}, which attempts proof by
|
|
154 |
assumption and resolution with the theorem $True$. In explicitly typed
|
|
155 |
logics, the auto-tactic can be used to solve simple type checking
|
|
156 |
obligations. Some applications demand a sophisticated auto-tactic such as
|
|
157 |
{\tt fast_tac}, but this could make simplification slow.
|
|
158 |
|
|
159 |
\begin{warn}
|
|
160 |
Rewriting never instantiates unknowns in subgoals. (It uses
|
|
161 |
\ttindex{match_tac} rather than \ttindex{resolve_tac}.) However, the
|
|
162 |
auto-tactic is permitted to instantiate unknowns.
|
|
163 |
\end{warn}
|
|
164 |
|
|
165 |
|
|
166 |
\section{The simplification tactics} \label{simp-tactics}
|
|
167 |
\index{simplification!tactics|bold}
|
|
168 |
\index{tactics!simplification|bold}
|
|
169 |
The actual simplification work is performed by the following tactics. The
|
|
170 |
rewriting strategy is strictly bottom up. Conditions in conditional rewrite
|
|
171 |
rules are solved recursively before the rewrite rule is applied.
|
|
172 |
|
|
173 |
There are two basic simplification tactics:
|
323
|
174 |
\begin{ttdescription}
|
104
|
175 |
\item[\ttindexbold{SIMP_TAC} $ss$ $i$]
|
|
176 |
simplifies subgoal~$i$ using the rules in~$ss$. It may solve the
|
|
177 |
subgoal completely if it has become trivial, using the auto-tactic
|
|
178 |
(\S\ref{simp-simpsets}).
|
|
179 |
|
|
180 |
\item[\ttindexbold{ASM_SIMP_TAC}]
|
|
181 |
is like \verb$SIMP_TAC$, but also uses assumptions as additional
|
|
182 |
rewrite rules.
|
323
|
183 |
\end{ttdescription}
|
104
|
184 |
Many logics have conditional operators like {\it if-then-else}. If the
|
|
185 |
simplifier has been set up with such case splits (see~\ttindex{case_splits}
|
|
186 |
in \S\ref{SimpFun-input}), there are tactics which automatically alternate
|
|
187 |
between simplification and case splitting:
|
323
|
188 |
\begin{ttdescription}
|
104
|
189 |
\item[\ttindexbold{SIMP_CASE_TAC}]
|
|
190 |
is like {\tt SIMP_TAC} but also performs automatic case splits.
|
|
191 |
More precisely, after each simplification phase the tactic tries to apply a
|
|
192 |
theorem in \ttindex{case_splits}. If this succeeds, the tactic calls
|
|
193 |
itself recursively on the result.
|
|
194 |
|
|
195 |
\item[\ttindexbold{ASM_SIMP_CASE_TAC}]
|
|
196 |
is like {\tt SIMP_CASE_TAC}, but also uses assumptions for
|
|
197 |
rewriting.
|
|
198 |
|
|
199 |
\item[\ttindexbold{SIMP_CASE2_TAC}]
|
|
200 |
is like {\tt SIMP_CASE_TAC}, but also tries to solve the
|
|
201 |
pre-conditions of conditional simplification rules by repeated case splits.
|
|
202 |
|
|
203 |
\item[\ttindexbold{CASE_TAC}]
|
|
204 |
tries to break up a goal using a rule in
|
|
205 |
\ttindex{case_splits}.
|
|
206 |
|
|
207 |
\item[\ttindexbold{SIMP_THM}]
|
|
208 |
simplifies a theorem using assumptions and case splitting.
|
323
|
209 |
\end{ttdescription}
|
104
|
210 |
Finally there are two useful functions for generating congruence
|
|
211 |
rules for constants and free variables:
|
323
|
212 |
\begin{ttdescription}
|
104
|
213 |
\item[\ttindexbold{mk_congs} $thy$ $cs$]
|
|
214 |
computes a list of congruence rules, one for each constant in $cs$.
|
|
215 |
Remember that the name of an infix constant
|
|
216 |
\verb$+$ is \verb$op +$.
|
|
217 |
|
|
218 |
\item[\ttindexbold{mk_typed_congs}]
|
|
219 |
computes congruence rules for explicitly typed free variables and
|
|
220 |
constants. Its second argument is a list of name and type pairs. Names
|
|
221 |
can be either free variables like {\tt P}, or constants like \verb$op =$.
|
|
222 |
For example in {\tt FOL}, the pair
|
|
223 |
\verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$.
|
|
224 |
Such congruence rules are necessary for goals with free variables whose
|
|
225 |
arguments need to be rewritten.
|
323
|
226 |
\end{ttdescription}
|
104
|
227 |
Both functions work correctly only if {\tt SimpFun} has been supplied with the
|
|
228 |
necessary substitution rules. The details are discussed in
|
|
229 |
\S\ref{SimpFun-input} under {\tt subst_thms}.
|
|
230 |
\begin{warn}
|
|
231 |
Using the simplifier effectively may take a bit of experimentation. In
|
|
232 |
particular it may often happen that simplification stops short of what you
|
|
233 |
expected or runs forever. To diagnose these problems, the simplifier can be
|
|
234 |
traced. The reference variable \ttindexbold{tracing} controls the output of
|
|
235 |
tracing information.
|
|
236 |
\index{tracing!of simplification}
|
|
237 |
\end{warn}
|
|
238 |
|
|
239 |
|
|
240 |
\section{Example: using the simplifier}
|
|
241 |
\index{simplification!example}
|
|
242 |
Assume we are working within {\tt FOL} and that
|
323
|
243 |
\begin{ttdescription}
|
|
244 |
\item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
|
|
245 |
\item[add_0] is the rewrite rule $0+n = n$,
|
|
246 |
\item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
|
|
247 |
\item[induct] is the induction rule
|
104
|
248 |
$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
|
323
|
249 |
\item[FOL_ss] is a basic simpset for {\tt FOL}.
|
|
250 |
\end{ttdescription}
|
104
|
251 |
We generate congruence rules for $Suc$ and for the infix operator~$+$:
|
|
252 |
\begin{ttbox}
|
|
253 |
val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
|
|
254 |
prths nat_congs;
|
|
255 |
{\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)}
|
|
256 |
{\out [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb}
|
|
257 |
\end{ttbox}
|
|
258 |
We create a simpset for natural numbers by extending~{\tt FOL_ss}:
|
|
259 |
\begin{ttbox}
|
|
260 |
val add_ss = FOL_ss addcongs nat_congs
|
|
261 |
addrews [add_0, add_Suc];
|
|
262 |
\end{ttbox}
|
|
263 |
Proofs by induction typically involve simplification:\footnote
|
|
264 |
{These examples reside on the file {\tt FOL/ex/nat.ML}.}
|
|
265 |
\begin{ttbox}
|
|
266 |
goal Nat.thy "m+0 = m";
|
|
267 |
{\out Level 0}
|
|
268 |
{\out m + 0 = m}
|
|
269 |
{\out 1. m + 0 = m}
|
|
270 |
\ttbreak
|
|
271 |
by (res_inst_tac [("n","m")] induct 1);
|
|
272 |
{\out Level 1}
|
|
273 |
{\out m + 0 = m}
|
|
274 |
{\out 1. 0 + 0 = 0}
|
|
275 |
{\out 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
|
|
276 |
\end{ttbox}
|
|
277 |
Simplification solves the first subgoal:
|
|
278 |
\begin{ttbox}
|
|
279 |
by (SIMP_TAC add_ss 1);
|
|
280 |
{\out Level 2}
|
|
281 |
{\out m + 0 = m}
|
|
282 |
{\out 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
|
|
283 |
\end{ttbox}
|
|
284 |
The remaining subgoal requires \ttindex{ASM_SIMP_TAC} in order to use the
|
|
285 |
induction hypothesis as a rewrite rule:
|
|
286 |
\begin{ttbox}
|
|
287 |
by (ASM_SIMP_TAC add_ss 1);
|
|
288 |
{\out Level 3}
|
|
289 |
{\out m + 0 = m}
|
|
290 |
{\out No subgoals!}
|
|
291 |
\end{ttbox}
|
|
292 |
The next proof is similar.
|
|
293 |
\begin{ttbox}
|
|
294 |
goal Nat.thy "m+Suc(n) = Suc(m+n)";
|
|
295 |
{\out Level 0}
|
|
296 |
{\out m + Suc(n) = Suc(m + n)}
|
|
297 |
{\out 1. m + Suc(n) = Suc(m + n)}
|
|
298 |
\ttbreak
|
|
299 |
by (res_inst_tac [("n","m")] induct 1);
|
|
300 |
{\out Level 1}
|
|
301 |
{\out m + Suc(n) = Suc(m + n)}
|
|
302 |
{\out 1. 0 + Suc(n) = Suc(0 + n)}
|
|
303 |
{\out 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
|
|
304 |
\end{ttbox}
|
|
305 |
Using the tactical \ttindex{ALLGOALS}, a single command simplifies all the
|
|
306 |
subgoals:
|
|
307 |
\begin{ttbox}
|
|
308 |
by (ALLGOALS (ASM_SIMP_TAC add_ss));
|
|
309 |
{\out Level 2}
|
|
310 |
{\out m + Suc(n) = Suc(m + n)}
|
|
311 |
{\out No subgoals!}
|
|
312 |
\end{ttbox}
|
|
313 |
Some goals contain free function variables. The simplifier must have
|
|
314 |
congruence rules for those function variables, or it will be unable to
|
|
315 |
simplify their arguments:
|
|
316 |
\begin{ttbox}
|
|
317 |
val f_congs = mk_typed_congs Nat.thy [("f","nat => nat")];
|
|
318 |
val f_ss = add_ss addcongs f_congs;
|
|
319 |
prths f_congs;
|
|
320 |
{\out ?Xa = ?Ya ==> f(?Xa) = f(?Ya)}
|
|
321 |
\end{ttbox}
|
|
322 |
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
|
|
323 |
the law $f(Suc(n)) = Suc(f(n))$:
|
|
324 |
\begin{ttbox}
|
|
325 |
val [prem] = goal Nat.thy
|
|
326 |
"(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
|
|
327 |
{\out Level 0}
|
|
328 |
{\out f(i + j) = i + f(j)}
|
|
329 |
{\out 1. f(i + j) = i + f(j)}
|
|
330 |
\ttbreak
|
|
331 |
by (res_inst_tac [("n","i")] induct 1);
|
|
332 |
{\out Level 1}
|
|
333 |
{\out f(i + j) = i + f(j)}
|
|
334 |
{\out 1. f(0 + j) = 0 + f(j)}
|
|
335 |
{\out 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
|
|
336 |
\end{ttbox}
|
|
337 |
We simplify each subgoal in turn. The first one is trivial:
|
|
338 |
\begin{ttbox}
|
|
339 |
by (SIMP_TAC f_ss 1);
|
|
340 |
{\out Level 2}
|
|
341 |
{\out f(i + j) = i + f(j)}
|
|
342 |
{\out 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
|
|
343 |
\end{ttbox}
|
|
344 |
The remaining subgoal requires rewriting by the premise, shown
|
|
345 |
below, so we add it to {\tt f_ss}:
|
|
346 |
\begin{ttbox}
|
|
347 |
prth prem;
|
|
348 |
{\out f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]}
|
|
349 |
by (ASM_SIMP_TAC (f_ss addrews [prem]) 1);
|
|
350 |
{\out Level 3}
|
|
351 |
{\out f(i + j) = i + f(j)}
|
|
352 |
{\out No subgoals!}
|
|
353 |
\end{ttbox}
|
|
354 |
|
|
355 |
|
|
356 |
\section{Setting up the simplifier} \label{SimpFun-input}
|
|
357 |
\index{simplification!setting up|bold}
|
|
358 |
To set up a simplifier for a new logic, the \ML\ functor
|
|
359 |
\ttindex{SimpFun} needs to be supplied with theorems to justify
|
|
360 |
rewriting. A rewrite relation must be reflexive and transitive; symmetry
|
|
361 |
is not necessary. Hence the package is also applicable to non-symmetric
|
|
362 |
relations such as occur in operational semantics. In the sequel, $\gg$
|
|
363 |
denotes some {\bf reduction relation}: a binary relation to be used for
|
|
364 |
rewriting. Several reduction relations can be used at once. In {\tt FOL},
|
|
365 |
both $=$ (on terms) and $\bimp$ (on formulae) can be used for rewriting.
|
|
366 |
|
|
367 |
The argument to {\tt SimpFun} is a structure with signature
|
|
368 |
\ttindexbold{SIMP_DATA}:
|
|
369 |
\begin{ttbox}
|
|
370 |
signature SIMP_DATA =
|
|
371 |
sig
|
|
372 |
val case_splits : (thm * string) list
|
|
373 |
val dest_red : term -> term * term * term
|
|
374 |
val mk_rew_rules : thm -> thm list
|
|
375 |
val norm_thms : (thm*thm) list
|
|
376 |
val red1 : thm
|
|
377 |
val red2 : thm
|
|
378 |
val refl_thms : thm list
|
|
379 |
val subst_thms : thm list
|
|
380 |
val trans_thms : thm list
|
|
381 |
end;
|
|
382 |
\end{ttbox}
|
|
383 |
The components of {\tt SIMP_DATA} need to be instantiated as follows. Many
|
|
384 |
of these components are lists, and can be empty.
|
323
|
385 |
\begin{ttdescription}
|
104
|
386 |
\item[\ttindexbold{refl_thms}]
|
|
387 |
supplies reflexivity theorems of the form $\Var{x} \gg
|
|
388 |
\Var{x}$. They must not have additional premises as, for example,
|
|
389 |
$\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory.
|
|
390 |
|
|
391 |
\item[\ttindexbold{trans_thms}]
|
|
392 |
supplies transitivity theorems of the form
|
|
393 |
$\List{\Var{x}\gg\Var{y}; \Var{y}\gg\Var{z}} \Imp {\Var{x}\gg\Var{z}}$.
|
|
394 |
|
|
395 |
\item[\ttindexbold{red1}]
|
|
396 |
is a theorem of the form $\List{\Var{P}\gg\Var{Q};
|
|
397 |
\Var{P}} \Imp \Var{Q}$, where $\gg$ is a relation between formulae, such as
|
|
398 |
$\bimp$ in {\tt FOL}.
|
|
399 |
|
|
400 |
\item[\ttindexbold{red2}]
|
|
401 |
is a theorem of the form $\List{\Var{P}\gg\Var{Q};
|
|
402 |
\Var{Q}} \Imp \Var{P}$, where $\gg$ is a relation between formulae, such as
|
|
403 |
$\bimp$ in {\tt FOL}.
|
|
404 |
|
|
405 |
\item[\ttindexbold{mk_rew_rules}]
|
|
406 |
is a function that extracts rewrite rules from theorems. A rewrite rule is
|
|
407 |
a theorem of the form $\List{\ldots}\Imp s \gg t$. In its simplest form,
|
|
408 |
{\tt mk_rew_rules} maps a theorem $t$ to the singleton list $[t]$. More
|
|
409 |
sophisticated versions may do things like
|
|
410 |
\[
|
|
411 |
\begin{array}{l@{}r@{\quad\mapsto\quad}l}
|
|
412 |
\mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]
|
|
413 |
\mbox{remove negations:}& \lnot P & [P \bimp False] \\[.5ex]
|
|
414 |
\mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]
|
|
415 |
\mbox{break up conjunctions:}&
|
|
416 |
(s@1 \gg@1 t@1) \conj (s@2 \gg@2 t@2) & [s@1 \gg@1 t@1, s@2 \gg@2 t@2]
|
|
417 |
\end{array}
|
|
418 |
\]
|
|
419 |
The more theorems are turned into rewrite rules, the better. The function
|
|
420 |
is used in two places:
|
|
421 |
\begin{itemize}
|
|
422 |
\item
|
|
423 |
$ss$~\ttindex{addrews}~$thms$ applies {\tt mk_rew_rules} to each element of
|
|
424 |
$thms$ before adding it to $ss$.
|
|
425 |
\item
|
|
426 |
simplification with assumptions (as in \ttindex{ASM_SIMP_TAC}) uses
|
|
427 |
{\tt mk_rew_rules} to turn assumptions into rewrite rules.
|
|
428 |
\end{itemize}
|
|
429 |
|
|
430 |
\item[\ttindexbold{case_splits}]
|
|
431 |
supplies expansion rules for case splits. The simplifier is designed
|
|
432 |
for rules roughly of the kind
|
|
433 |
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
|
|
434 |
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))
|
|
435 |
\]
|
|
436 |
but is insensitive to the form of the right-hand side. Other examples
|
|
437 |
include product types, where $split ::
|
|
438 |
(\alpha\To\beta\To\gamma)\To\alpha*\beta\To\gamma$:
|
|
439 |
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
|
|
440 |
{<}a,b{>} \imp \Var{P}(\Var{f}(a,b)))
|
|
441 |
\]
|
|
442 |
Each theorem in the list is paired with the name of the constant being
|
|
443 |
eliminated, {\tt"if"} and {\tt"split"} in the examples above.
|
|
444 |
|
|
445 |
\item[\ttindexbold{norm_thms}]
|
|
446 |
supports an optimization. It should be a list of pairs of rules of the
|
|
447 |
form $\Var{x} \gg norm(\Var{x})$ and $norm(\Var{x}) \gg \Var{x}$. These
|
|
448 |
introduce and eliminate {\tt norm}, an arbitrary function that should be
|
|
449 |
used nowhere else. This function serves to tag subterms that are in normal
|
|
450 |
form. Such rules can speed up rewriting significantly!
|
|
451 |
|
|
452 |
\item[\ttindexbold{subst_thms}]
|
|
453 |
supplies substitution rules of the form
|
|
454 |
\[ \List{\Var{x} \gg \Var{y}; \Var{P}(\Var{x})} \Imp \Var{P}(\Var{y}) \]
|
|
455 |
They are used to derive congruence rules via \ttindex{mk_congs} and
|
|
456 |
\ttindex{mk_typed_congs}. If $f :: [\tau@1,\cdots,\tau@n]\To\tau$ is a
|
|
457 |
constant or free variable, the computation of a congruence rule
|
|
458 |
\[\List{\Var{x@1} \gg@1 \Var{y@1}; \ldots; \Var{x@n} \gg@n \Var{y@n}}
|
|
459 |
\Imp f(\Var{x@1},\ldots,\Var{x@n}) \gg f(\Var{y@1},\ldots,\Var{y@n}) \]
|
|
460 |
requires a reflexivity theorem for some reduction ${\gg} ::
|
|
461 |
\alpha\To\alpha\To\sigma$ such that $\tau$ is an instance of $\alpha$. If a
|
|
462 |
suitable reflexivity law is missing, no congruence rule for $f$ can be
|
|
463 |
generated. Otherwise an $n$-ary congruence rule of the form shown above is
|
|
464 |
derived, subject to the availability of suitable substitution laws for each
|
|
465 |
argument position.
|
|
466 |
|
|
467 |
A substitution law is suitable for argument $i$ if it
|
|
468 |
uses a reduction ${\gg@i} :: \alpha@i\To\alpha@i\To\sigma@i$ such that
|
|
469 |
$\tau@i$ is an instance of $\alpha@i$. If a suitable substitution law for
|
|
470 |
argument $i$ is missing, the $i^{th}$ premise of the above congruence rule
|
|
471 |
cannot be generated and hence argument $i$ cannot be rewritten. In the
|
|
472 |
worst case, if there are no suitable substitution laws at all, the derived
|
|
473 |
congruence simply degenerates into a reflexivity law.
|
|
474 |
|
|
475 |
\item[\ttindexbold{dest_red}]
|
|
476 |
takes reductions apart. Given a term $t$ representing the judgement
|
|
477 |
\mbox{$a \gg b$}, \verb$dest_red$~$t$ should return a triple $(c,ta,tb)$
|
|
478 |
where $ta$ and $tb$ represent $a$ and $b$, and $c$ is a term of the form
|
|
479 |
\verb$Const(_,_)$, the reduction constant $\gg$.
|
|
480 |
|
|
481 |
Suppose the logic has a coercion function like $Trueprop::o\To prop$, as do
|
|
482 |
{\tt FOL} and~{\tt HOL}\@. If $\gg$ is a binary operator (not necessarily
|
|
483 |
infix), the following definition does the job:
|
|
484 |
\begin{verbatim}
|
|
485 |
fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb);
|
|
486 |
\end{verbatim}
|
|
487 |
The wildcard pattern {\tt_} matches the coercion function.
|
323
|
488 |
\end{ttdescription}
|
104
|
489 |
|
|
490 |
|
|
491 |
\section{A sample instantiation}
|
|
492 |
Here is the instantiation of {\tt SIMP_DATA} for {\FOL}. The code for {\tt
|
|
493 |
mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
|
|
494 |
\begin{ttbox}
|
|
495 |
structure FOL_SimpData : SIMP_DATA =
|
|
496 |
struct
|
|
497 |
val refl_thms = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]
|
|
498 |
val trans_thms = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),
|
|
499 |
\(\List{\Var{P}\bimp\Var{Q};\Var{Q}\bimp\Var{R}}\Imp\Var{P}\bimp\Var{R}\) ]
|
|
500 |
val red1 = \(\List{\Var{P}\bimp\Var{Q}; \Var{P}} \Imp \Var{Q}\)
|
|
501 |
val red2 = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)
|
|
502 |
val mk_rew_rules = ...
|
|
503 |
val case_splits = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)
|
|
504 |
\((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))\) ]
|
|
505 |
val norm_thms = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),
|
|
506 |
(\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]
|
|
507 |
val subst_thms = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]
|
|
508 |
val dest_red = fn (_ $ (opn $ lhs $ rhs)) => (opn,lhs,rhs)
|
|
509 |
end;
|
|
510 |
\end{ttbox}
|
|
511 |
|
|
512 |
\index{simplification|)}
|