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 |
|
25 Fig.\ts\ref{SIMP}. |
|
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 |
|
58 simplifying~$P@2$. Such `local' assumptions are effective for rewriting |
|
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} |
|
113 \begin{ttdescription} |
|
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 |
|
118 \item[$ss$ \ttindexbold{addcongs} $thms$] |
|
119 is the simpset~$ss$ plus the congruence rules~$thms$. |
|
120 |
|
121 \item[$ss$ \ttindexbold{delcongs} $thms$] |
|
122 is the simpset~$ss$ minus the congruence rules~$thms$. |
|
123 |
|
124 \item[$ss$ \ttindexbold{addrews} $thms$] |
|
125 is the simpset~$ss$ plus the rewrite rules~$thms$. |
|
126 |
|
127 \item[$ss$ \ttindexbold{delrews} $thms$] |
|
128 is the simpset~$ss$ minus the rewrite rules~$thms$. |
|
129 |
|
130 \item[$ss$ \ttindexbold{setauto} $tacf$] |
|
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$. |
|
135 \end{ttdescription} |
|
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: |
|
174 \begin{ttdescription} |
|
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. |
|
183 \end{ttdescription} |
|
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: |
|
188 \begin{ttdescription} |
|
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. |
|
209 \end{ttdescription} |
|
210 Finally there are two useful functions for generating congruence |
|
211 rules for constants and free variables: |
|
212 \begin{ttdescription} |
|
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. |
|
226 \end{ttdescription} |
|
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 |
|
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 |
|
248 $\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$. |
|
249 \item[FOL_ss] is a basic simpset for {\tt FOL}. |
|
250 \end{ttdescription} |
|
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. |
|
385 \begin{ttdescription} |
|
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:}& \neg 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 (\neg\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. |
|
488 \end{ttdescription} |
|
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 (\neg\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|)} |
|