2 \chapter{Simplification}
3 \label{chap:simplification}
4 \index{simplification|(}
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.
12 The first section is a quick introduction to the simplifier that
13 should be sufficient to get started. The later sections explain more
17 \section{Simplification for dummies}
18 \label{sec:simp-for-dummies}
20 Basic use of the simplifier is particularly easy because each theory
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
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.
34 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs}
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}
41 debug_simp : bool ref \hfill{\bf initially false}
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.
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.
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).
57 \item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$,
58 but also simplifies the assumptions. In particular, assumptions can
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}.}
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.
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:
78 Goal "0 + (x + 0) = x + 0 + 0";
79 {\out 1. 0 + (x + 0) = x + 0 + 0}
82 {\out 0 + (x + 0) = x + 0 + 0}
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} =
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:
94 {\out 1. x = 0 ==> x + x = 0}
98 \medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet
99 of tactics but may also loop where some of the others terminate. For
102 {\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}
104 is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt
105 Asm_full_simp_tac} loop because the rewrite rule $f\,\Var{x} =
106 g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not
107 terminate. Isabelle notices certain simple forms of nontermination,
108 but not this one. Because assumptions may simplify each other, there can be
109 very subtle cases of nontermination. For example, invoking
110 {\tt Asm_full_simp_tac} on
112 {\out 1. [| P (f x); y = x; f x = f y |] ==> Q}
114 gives rise to the infinite reduction sequence
116 P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} P\,(f\,y) \stackrel{y = x}{\longmapsto}
117 P\,(f\,x) \stackrel{f\,x = f\,y}{\longmapsto} \cdots
119 whereas applying the same tactic to
121 {\out 1. [| y = x; f x = f y; P (f x) |] ==> Q}
127 Using the simplifier effectively may take a bit of experimentation.
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).
134 \subsection{Modifying the current simpset}
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
142 Addsplits : thm list -> unit
143 Delsplits : thm list -> unit
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
154 {\S}\ref{sec:simp-congs}.
156 \begin{ttdescription}
158 \item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from
159 $thms$ to the current simpset.
161 \item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived
162 from $thms$ from the current simpset.
164 \item[\ttindexbold{Addsimprocs} $procs$;] adds simplification
165 procedures $procs$ to the current simpset.
167 \item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification
168 procedures $procs$ from the current simpset.
170 \item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the
173 \item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the
176 \item[\ttindexbold{Addsplits} $thms$;] adds splitting rules to the
179 \item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the
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
190 It is up the user to manipulate the current simpset further by
191 explicitly adding or deleting theorems and simplification procedures.
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
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
209 the unwanted rules. After this union is formed, changes to
210 a parent simpset have no effect on the child simpset.
214 \section{Simplification sets}\index{simplification sets}
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.
224 \subsection{Inspecting simpsets}
226 print_ss : simpset -> unit
227 rep_ss : simpset -> \{mss : meta_simpset,
228 subgoal_tac: simpset -> int -> tactic,
229 loop_tacs : (string * (int -> tactic))list,
230 finish_tac : solver list,
231 unsafe_finish_tac : solver list\}
233 \begin{ttdescription}
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
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
249 \subsection{Building simpsets}
252 merge_ss : simpset * simpset -> simpset
254 \begin{ttdescription}
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}.
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
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
272 \subsection{Rewrite rules}
274 addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
275 delsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
278 \index{rewrite rules|(} Rewrite rules are theorems expressing some
279 form of equality, for example:
281 Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\
282 \Var{P}\conj\Var{P} &\bimp& \Var{P} \\
283 \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
285 Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
286 0$ are also permitted; the conditions can be arbitrary formulas.
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
291 example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
292 \equiv False$. This function can be installed using
293 \ttindex{setmksimps} but only the definer of a logic should need to do
294 this; see {\S}\ref{sec:setmksimps}. The function processes theorems
295 added by \texttt{addsimps} as well as local assumptions.
297 \begin{ttdescription}
299 \item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived
300 from $thms$ to the simpset $ss$.
302 \item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules
303 derived from $thms$ from the simpset $ss$.
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.
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.
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
332 There is basically no restriction on the form of the right-hand
333 sides. They may not contain extraneous term or type variables,
336 \index{rewrite rules|)}
339 \subsection{*Simplification procedures}
341 addsimprocs : simpset * simproc list -> simpset
342 delsimprocs : simpset * simproc list -> simpset
345 Simplification procedures are {\ML} objects of abstract type
346 \texttt{simproc}. Basically they are just functions that may produce
347 \emph{proven} rewrite rules on demand. They are associated with
348 certain patterns that conceptually represent left-hand sides of
349 equations; these are shown by \texttt{print_ss}. During its
350 operation, the simplifier may offer a simplification procedure the
351 current redex and ask for a suitable rewrite rule. Thus rules may be
352 specifically fashioned for particular situations, resulting in a more
353 powerful mechanism than term rewriting by a fixed set of rules.
356 \begin{ttdescription}
358 \item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification
359 procedures $procs$ to the current simpset.
361 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification
362 procedures $procs$ from the current simpset.
366 For example, simplification procedures \ttindexbold{nat_cancel} of
367 \texttt{HOL/Arith} cancel common summands and constant factors out of
368 several relations of sums over natural numbers.
370 Consider the following goal, which after cancelling $a$ on both sides
371 contains a factor of $2$. Simplifying with the simpset of
372 \texttt{Arith.thy} will do the cancellation automatically:
374 {\out 1. x + a + x < y + y + 2 + a + a + a + a + a}
376 {\out 1. x < Suc (a + (a + y))}
380 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
382 addcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
383 delcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
384 addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
385 deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
388 Congruence rules are meta-equalities of the form
390 f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
392 This governs the simplification of the arguments of~$f$. For
393 example, some arguments can be simplified under additional assumptions:
394 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
395 \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
397 Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
398 rules from it when simplifying~$P@2$. Such local assumptions are
399 effective for rewriting formulae such as $x=0\imp y+x=y$. The local
400 assumptions are also provided as theorems to the solver; see
401 {\S}~\ref{sec:simp-solver} below.
403 \begin{ttdescription}
405 \item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
406 simpset $ss$. These are derived from $thms$ in an appropriate way,
407 depending on the underlying object-logic.
409 \item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
412 \item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
413 their internal form (conclusions using meta-equality) to simpset
414 $ss$. This is the basic mechanism that \texttt{addcongs} is built
415 on. It should be rarely used directly.
417 \item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
418 in internal form from simpset $ss$.
424 Here are some more examples. The congruence rule for bounded
425 quantifiers also supplies contextual information, this time about the
428 &&\List{\Var{A}=\Var{B};\;
429 \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
431 (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
433 The congruence rule for conditional expressions can supply contextual
434 information for simplifying the arms:
435 \[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
436 \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
437 if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
439 A congruence rule can also {\em prevent\/} simplification of some arguments.
440 Here is an alternative congruence rule for conditional expressions:
441 \[ \Var{p}=\Var{q} \Imp
442 if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
444 Only the first argument is simplified; the others remain unchanged.
445 This can make simplification much faster, but may require an extra case split
449 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
452 simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
453 prems_of_ss : simpset -> thm list
456 The subgoaler is the tactic used to solve subgoals arising out of
457 conditional rewrite rules or congruence rules. The default should be
458 simplification itself. Occasionally this strategy needs to be
459 changed. For example, if the premise of a conditional rule is an
460 instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m}
461 < \Var{n}$, the default strategy could loop.
463 \begin{ttdescription}
465 \item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of
466 $ss$ to $tacf$. The function $tacf$ will be applied to the current
467 simplifier context expressed as a simpset.
469 \item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of
470 premises from simplifier context $ss$. This may be non-empty only
471 if the simplifier has been told to utilize local assumptions in the
472 first place, e.g.\ if invoked via \texttt{asm_simp_tac}.
476 As an example, consider the following subgoaler:
480 resolve_tac (prems_of_ss ss) ORELSE'
483 This tactic first tries to solve the subgoal by assumption or by
484 resolving with with one of the premises, calling simplification only
488 \subsection{*The solver}\label{sec:simp-solver}
490 mk_solver : string -> (thm list -> int -> tactic) -> solver
491 setSolver : simpset * solver -> simpset \hfill{\bf infix 4}
492 addSolver : simpset * solver -> simpset \hfill{\bf infix 4}
493 setSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
494 addSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
497 A solver is a tactic that attempts to solve a subgoal after
498 simplification. Typically it just proves trivial subgoals such as
499 \texttt{True} and $t=t$. It could use sophisticated means such as {\tt
500 blast_tac}, though that could make simplification expensive.
501 To keep things more abstract, solvers are packaged up in type
502 \texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.
504 Rewriting does not instantiate unknowns. For example, rewriting
505 cannot prove $a\in \Var{A}$ since this requires
506 instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic
507 and may instantiate unknowns as it pleases. This is the only way the
508 simplifier can handle a conditional rewrite rule whose condition
509 contains extra variables. When a simplification tactic is to be
510 combined with other provers, especially with the classical reasoner,
511 it is important whether it can be considered safe or not. For this
512 reason a simpset contains two solvers, a safe and an unsafe one.
514 The standard simplification strategy solely uses the unsafe solver,
515 which is appropriate in most cases. For special applications where
516 the simplification process is not allowed to instantiate unknowns
517 within the goal, simplification starts with the safe solver, but may
518 still apply the ordinary unsafe one in nested simplifications for
519 conditional rules or congruences. Note that in this way the overall
520 tactic is not totally safe: it may instantiate unknowns that appear also
523 \begin{ttdescription}
524 \item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
525 the string $s$ is only attached as a comment and has no other significance.
527 \item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the
528 \emph{safe} solver of $ss$.
530 \item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an
531 additional \emph{safe} solver; it will be tried after the solvers
532 which had already been present in $ss$.
534 \item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the
535 unsafe solver of $ss$.
537 \item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an
538 additional unsafe solver; it will be tried after the solvers which
539 had already been present in $ss$.
545 \index{assumptions!in simplification} The solver tactic is invoked
546 with a list of theorems, namely assumptions that hold in the local
547 context. This may be non-empty only if the simplifier has been told
548 to utilize local assumptions in the first place, e.g.\ if invoked via
549 \texttt{asm_simp_tac}. The solver is also presented the full goal
550 including its assumptions in any case. Thus it can use these (e.g.\
551 by calling \texttt{assume_tac}), even if the list of premises is not
556 As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
557 to solve the premises of congruence rules. These are usually of the
558 form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
559 needs to be instantiated with the result. Typically, the subgoaler
560 will invoke the simplifier at some point, which will eventually call
561 the solver. For this reason, solver tactics must be prepared to solve
562 goals of the form $t = \Var{x}$, usually by reflexivity. In
563 particular, reflexivity should be tried before any of the fancy
564 tactics like \texttt{blast_tac}.
566 It may even happen that due to simplification the subgoal is no longer
567 an equality. For example $False \bimp \Var{Q}$ could be rewritten to
568 $\neg\Var{Q}$. To cover this case, the solver could try resolving
569 with the theorem $\neg False$.
574 If a premise of a congruence rule cannot be proved, then the
575 congruence is ignored. This should only happen if the rule is
576 \emph{conditional} --- that is, contains premises not of the form $t
577 = \Var{x}$; otherwise it indicates that some congruence rule, or
578 possibly the subgoaler or solver, is faulty.
582 \subsection{*The looper}\label{sec:simp-looper}
584 setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
585 addloop : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
586 delloop : simpset * string -> simpset \hfill{\bf infix 4}
587 addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
588 delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
591 The looper is a list of tactics that are applied after simplification, in case
592 the solver failed to solve the simplified goal. If the looper
593 succeeds, the simplification process is started all over again. Each
594 of the subgoals generated by the looper is attacked in turn, in
597 A typical looper is \index{case splitting}: the expansion of a conditional.
598 Another possibility is to apply an elimination rule on the
599 assumptions. More adventurous loopers could start an induction.
601 \begin{ttdescription}
603 \item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
606 \item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
607 looper tactic with name $name$; it will be tried after the looper tactics
608 that had already been present in $ss$.
610 \item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
613 \item[$ss$ \ttindexbold{addsplits} $thms$] adds
614 split tactics for $thms$ as additional looper tactics of $ss$.
616 \item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
617 split tactics for $thms$ from the looper tactics of $ss$.
621 The splitter replaces applications of a given function; the right-hand side
622 of the replacement can be anything. For example, here is a splitting rule
623 for conditional expressions:
624 \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
625 \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
627 Another example is the elimination operator for Cartesian products (which
628 happens to be called~$split$):
629 \[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
630 \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
633 For technical reasons, there is a distinction between case splitting in the
634 conclusion and in the premises of a subgoal. The former is done by
635 \texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split},
636 which do not split the subgoal, while the latter is done by
637 \texttt{split_asm_tac} with rules like \texttt{split_if_asm} or
638 \texttt{option.split_asm}, which split the subgoal.
639 The operator \texttt{addsplits} automatically takes care of which tactic to
640 call, analyzing the form of the rules given as argument.
642 Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
645 Case splits should be allowed only when necessary; they are expensive
646 and hard to control. Here is an example of use, where \texttt{split_if}
647 is the first rule above:
649 by (simp_tac (simpset()
650 addloop ("split if", split_tac [split_if])) 1);
652 Users would usually prefer the following shortcut using \texttt{addsplits}:
654 by (simp_tac (simpset() addsplits [split_if]) 1);
656 Case-splitting on conditional expressions is usually beneficial, so it is
657 enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.
660 \section{The simplification tactics}\label{simp-tactics}
661 \index{simplification!tactics}\index{tactics!simplification}
663 generic_simp_tac : bool -> bool * bool * bool ->
664 simpset -> int -> tactic
665 simp_tac : simpset -> int -> tactic
666 asm_simp_tac : simpset -> int -> tactic
667 full_simp_tac : simpset -> int -> tactic
668 asm_full_simp_tac : simpset -> int -> tactic
669 safe_asm_full_simp_tac : simpset -> int -> tactic
672 \texttt{generic_simp_tac} is the basic tactic that is underlying any actual
673 simplification work. The others are just instantiations of it. The rewriting
674 strategy is always strictly bottom up, except for congruence rules,
675 which are applied while descending into a term. Conditions in conditional
676 rewrite rules are solved recursively before the rewrite rule is applied.
678 \begin{ttdescription}
680 \item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)]
681 gives direct access to the various simplification modes:
683 \item if $safe$ is {\tt true}, the safe solver is used as explained in
684 {\S}\ref{sec:simp-solver},
685 \item $simp\_asm$ determines whether the local assumptions are simplified,
686 \item $use\_asm$ determines whether the assumptions are used as local rewrite
688 \item $mutual$ determines whether assumptions can simplify each other rather
689 than being processed from left to right.
691 This generic interface is intended
692 for building special tools, e.g.\ for combining the simplifier with the
693 classical reasoner. It is rarely used directly.
695 \item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
696 \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
697 the basic simplification tactics that work exactly like their
698 namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
699 explicitly supplied with a simpset.
705 Local modifications of simpsets within a proof are often much cleaner
706 by using above tactics in conjunction with explicit simpsets, rather
707 than their capitalized counterparts. For example
713 can be expressed more appropriately as
715 by (simp_tac (simpset() addsimps \(thms\)) \(i\));
720 Also note that functions depending implicitly on the current theory
721 context (like capital \texttt{Simp_tac} and the other commands of
722 {\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
723 actual proof scripts. In particular, ML programs like theory
724 definition packages or special tactics should refer to simpsets only
725 explicitly, via the above tactics used in conjunction with
726 \texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
729 \section{Forward rules and conversions}
730 \index{simplification!forward rules}\index{simplification!conversions}
731 \begin{ttbox}\index{*simplify}\index{*asm_simplify}\index{*full_simplify}\index{*asm_full_simplify}\index{*Simplifier.rewrite}\index{*Simplifier.asm_rewrite}\index{*Simplifier.full_rewrite}\index{*Simplifier.asm_full_rewrite}
732 simplify : simpset -> thm -> thm
733 asm_simplify : simpset -> thm -> thm
734 full_simplify : simpset -> thm -> thm
735 asm_full_simplify : simpset -> thm -> thm\medskip
736 Simplifier.rewrite : simpset -> cterm -> thm
737 Simplifier.asm_rewrite : simpset -> cterm -> thm
738 Simplifier.full_rewrite : simpset -> cterm -> thm
739 Simplifier.asm_full_rewrite : simpset -> cterm -> thm
742 The first four of these functions provide \emph{forward} rules for
743 simplification. Their effect is analogous to the corresponding
744 tactics described in {\S}\ref{simp-tactics}, but affect the whole
745 theorem instead of just a certain subgoal. Also note that the
746 looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
747 {\S}\ref{sec:simp-solver} is omitted in forward simplification.
749 The latter four are \emph{conversions}, establishing proven equations
750 of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
754 Forward simplification rules and conversions should be used rarely
755 in ordinary proof scripts. The main intention is to provide an
756 internal interface to the simplifier for special utilities.
760 \section{Permutative rewrite rules}
761 \index{rewrite rules!permutative|(}
763 A rewrite rule is {\bf permutative} if the left-hand side and right-hand
764 side are the same up to renaming of variables. The most common permutative
765 rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z =
766 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
767 for sets. Such rules are common enough to merit special attention.
769 Because ordinary rewriting loops given such rules, the simplifier
770 employs a special strategy, called {\bf ordered
771 rewriting}\index{rewriting!ordered}. There is a standard
772 lexicographic ordering on terms. This should be perfectly OK in most
773 cases, but can be changed for special applications.
776 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
778 \begin{ttdescription}
780 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as
781 term order in simpset $ss$.
787 A permutative rewrite rule is applied only if it decreases the given
788 term with respect to this ordering. For example, commutativity
789 rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less
790 than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also
791 employs ordered rewriting.
793 Permutative rewrite rules are added to simpsets just like other
794 rewrite rules; the simplifier recognizes their special status
795 automatically. They are most effective in the case of
796 associative-commutative operators. (Associativity by itself is not
797 permutative.) When dealing with an AC-operator~$f$, keep the
798 following points in mind:
799 \begin{itemize}\index{associative-commutative operators}
801 \item The associative law must always be oriented from left to right,
802 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
803 used with commutativity, leads to looping in conjunction with the
806 \item To complete your set of rewrite rules, you must add not just
807 associativity~(A) and commutativity~(C) but also a derived rule, {\bf
808 left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
810 Ordered rewriting with the combination of A, C, and~LC sorts a term
812 \[\def\maps#1{\stackrel{#1}{\longmapsto}}
813 (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \]
814 Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
815 examples; other algebraic structures are amenable to ordered rewriting,
816 such as boolean rings.
818 \subsection{Example: sums of natural numbers}
820 This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory
821 \thydx{Arith} contains natural numbers arithmetic. Its associated simpset
822 contains many arithmetic laws including distributivity of~$\times$ over~$+$,
823 while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
824 type \texttt{nat}. Let us prove the theorem
825 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
827 A functional~\texttt{sum} represents the summation operator under the
828 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We
829 extend \texttt{Arith} as follows:
832 consts sum :: [nat=>nat, nat] => nat
835 "sum f (Suc n) = f(n) + sum f n"
838 The \texttt{primrec} declaration automatically adds rewrite rules for
839 \texttt{sum} to the default simpset. We now remove the
840 \texttt{nat_cancel} simplification procedures (in order not to spoil
841 the example) and insert the AC-rules for~$+$:
843 Delsimprocs nat_cancel;
846 Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
847 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:
849 Goal "2 * sum (\%i.i) (Suc n) = n * Suc n";
851 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
852 {\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
854 Induction should not be applied until the goal is in the simplest
859 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
860 {\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
862 Ordered rewriting has sorted the terms in the left-hand side. The
863 subgoal is now ready for induction:
865 by (induct_tac "n" 1);
867 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
868 {\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
870 {\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
871 {\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =}
874 Simplification proves both subgoals immediately:\index{*ALLGOALS}
876 by (ALLGOALS Asm_simp_tac);
878 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
881 Simplification cannot prove the induction step if we omit \texttt{add_ac} from
882 the simpset. Observe that like terms have not been collected:
885 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
886 {\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n}
887 {\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =}
888 {\out n + (n + (n + n * n))}
890 Ordered rewriting proves this by sorting the left-hand side. Proving
891 arithmetic theorems without ordered rewriting requires explicit use of
892 commutativity. This is tedious; try it and see!
894 Ordered rewriting is equally successful in proving
895 $\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
898 \subsection{Re-orienting equalities}
899 Ordered rewriting with the derived rule \texttt{symmetry} can reverse
902 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
903 (fn _ => [Blast_tac 1]);
905 This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs
906 in the conclusion but not~$s$, can often be brought into the right form.
907 For example, ordered rewriting with \texttt{symmetry} can prove the goal
908 \[ f(a)=b \conj f(a)=c \imp b=c. \]
909 Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
910 because $f(a)$ is lexicographically greater than $b$ and~$c$. These
911 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
912 conclusion by~$f(a)$.
914 Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
915 The differing orientations make this appear difficult to prove. Ordered
916 rewriting with \texttt{symmetry} makes the equalities agree. (Without
917 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
918 or~$u=t$.) Then the simplifier can prove the goal outright.
920 \index{rewrite rules!permutative|)}
923 \section{*Coding simplification procedures}
925 val Simplifier.simproc: Sign.sg -> string -> string list
926 -> (Sign.sg -> simpset -> term -> thm option) -> simproc
927 val Simplifier.simproc_i: Sign.sg -> string -> term list
928 -> (Sign.sg -> simpset -> term -> thm option) -> simproc
931 \begin{ttdescription}
932 \item[\ttindexbold{Simplifier.simproc}~$sign$~$name$~$lhss$~$proc$] makes
933 $proc$ a simplification procedure for left-hand side patterns $lhss$. The
934 name just serves as a comment. The function $proc$ may be invoked by the
935 simplifier for redex positions matched by one of $lhss$ as described below
936 (which are be specified as strings to be read as terms).
938 \item[\ttindexbold{Simplifier.simproc_i}] is similar to
939 \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument.
942 Simplification procedures are applied in a two-stage process as
943 follows: The simplifier tries to match the current redex position
944 against any one of the $lhs$ patterns of any simplification procedure.
945 If this succeeds, it invokes the corresponding {\ML} function, passing
946 with the current signature, local assumptions and the (potential)
947 redex. The result may be either \texttt{None} (indicating failure) or
950 Any successful result is supposed to be a (possibly conditional)
951 rewrite rule $t \equiv u$ that is applicable to the current redex.
952 The rule will be applied just as any ordinary rewrite rule. It is
953 expected to be already in \emph{internal form}, though, bypassing the
954 automatic preprocessing of object-level equivalences.
958 As an example of how to write your own simplification procedures,
959 consider eta-expansion of pair abstraction (see also
960 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
961 model checker syntax).
963 The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
964 \texttt{split} together with some concrete syntax supporting
965 $\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic
966 that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
967 to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is:
969 pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y))
971 Unfortunately, term rewriting using this rule directly would not
972 terminate! We now use the simplification procedure mechanism in order
973 to stop the simplifier from applying this rule over and over again,
974 making it rewrite only actual abstractions. The simplification
975 procedure \texttt{pair_eta_expand_proc} is defined as follows:
977 val pair_eta_expand_proc =
978 Simplifier.simproc (Theory.sign_of (the_context ()))
979 "pair_eta_expand" ["f::'a*'b=>'c"]
980 (fn _ => fn _ => fn t =>
981 case t of Abs _ => Some (mk_meta_eq pair_eta_expand)
984 This is an example of using \texttt{pair_eta_expand_proc}:
986 {\out 1. P (\%p::'a * 'a. fst p + snd p + z)}
987 by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1);
988 {\out 1. P (\%(x::'a,y::'a). x + y + z)}
993 In the above example the simplification procedure just did fine
994 grained control over rule application, beyond higher-order pattern
995 matching. Usually, procedures would do some more work, in particular
996 prove particular theorems depending on the current redex.
999 \section{*Setting up the Simplifier}\label{sec:setting-up-simp}
1000 \index{simplification!setting up}
1002 Setting up the simplifier for new logics is complicated in the general case.
1003 This section describes how the simplifier is installed for intuitionistic
1004 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
1007 The case splitting tactic, which resides on a separate files, is not part of
1008 Pure Isabelle. It needs to be loaded explicitly by the object-logic as
1009 follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}):
1011 use "\~\relax\~\relax/src/Provers/splitter.ML";
1014 Simplification requires converting object-equalities to meta-level rewrite
1015 rules. This demands rules stating that equal terms and equivalent formulae
1016 are also equal at the meta-level. The rule declaration part of the file
1017 \texttt{FOL/IFOL.thy} contains the two lines
1018 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
1019 eq_reflection "(x=y) ==> (x==y)"
1020 iff_reflection "(P<->Q) ==> (P==Q)"
1022 Of course, you should only assert such rules if they are true for your
1023 particular logic. In Constructive Type Theory, equality is a ternary
1024 relation of the form $a=b\in A$; the type~$A$ determines the meaning
1025 of the equality essentially as a partial equivalence relation. The
1026 present simplifier cannot be used. Rewriting in \texttt{CTT} uses
1027 another simplifier, which resides in the file {\tt
1028 Provers/typedsimp.ML} and is not documented. Even this does not
1029 work for later variants of Constructive Type Theory that use
1030 intensional equality~\cite{nordstrom90}.
1033 \subsection{A collection of standard rewrite rules}
1035 We first prove lots of standard rewrite rules about the logical
1036 connectives. These include cancellation and associative laws. We
1037 define a function that echoes the desired law and then supplies it the
1038 prover for intuitionistic FOL:
1040 fun int_prove_fun s =
1042 prove_goal IFOL.thy s
1043 (fn prems => [ (cut_facts_tac prems 1),
1044 (IntPr.fast_tac 1) ]));
1046 The following rewrite rules about conjunction are a selection of those
1047 proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the
1050 val conj_simps = map int_prove_fun
1051 ["P & True <-> P", "True & P <-> P",
1052 "P & False <-> False", "False & P <-> False",
1054 "P & ~P <-> False", "~P & P <-> False",
1055 "(P & Q) & R <-> P & (Q & R)"];
1057 The file also proves some distributive laws. As they can cause exponential
1058 blowup, they will not be included in the standard simpset. Instead they
1059 are merely bound to an \ML{} identifier, for user reference.
1061 val distrib_simps = map int_prove_fun
1062 ["P & (Q | R) <-> P&Q | P&R",
1063 "(Q | R) & P <-> Q&P | R&P",
1064 "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
1068 \subsection{Functions for preprocessing the rewrite rules}
1069 \label{sec:setmksimps}
1070 \begin{ttbox}\indexbold{*setmksimps}
1071 setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
1073 The next step is to define the function for preprocessing rewrite rules.
1074 This will be installed by calling \texttt{setmksimps} below. Preprocessing
1075 occurs whenever rewrite rules are added, whether by user command or
1076 automatically. Preprocessing involves extracting atomic rewrites at the
1077 object-level, then reflecting them to the meta-level.
1079 To start, the function \texttt{gen_all} strips any meta-level
1080 quantifiers from the front of the given theorem.
1082 The function \texttt{atomize} analyses a theorem in order to extract
1083 atomic rewrite rules. The head of all the patterns, matched by the
1084 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
1086 fun atomize th = case concl_of th of
1087 _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at
1088 atomize(th RS conjunct2)
1089 | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
1090 | _ $ (Const("All",_) $ _) => atomize(th RS spec)
1091 | _ $ (Const("True",_)) => []
1092 | _ $ (Const("False",_)) => []
1095 There are several cases, depending upon the form of the conclusion:
1097 \item Conjunction: extract rewrites from both conjuncts.
1098 \item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
1099 extract rewrites from~$Q$; these will be conditional rewrites with the
1101 \item Universal quantification: remove the quantifier, replacing the bound
1102 variable by a schematic variable, and extract rewrites from the body.
1103 \item \texttt{True} and \texttt{False} contain no useful rewrites.
1104 \item Anything else: return the theorem in a singleton list.
1106 The resulting theorems are not literally atomic --- they could be
1107 disjunctive, for example --- but are broken down as much as possible.
1108 See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
1109 set-theoretic formulae into rewrite rules.
1111 For standard situations like the above,
1112 there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a
1113 list of pairs $(name, thms)$, where $name$ is an operator name and
1114 $thms$ is a list of theorems to resolve with in case the pattern matches,
1115 and returns a suitable \texttt{atomize} function.
1118 The simplified rewrites must now be converted into meta-equalities. The
1119 rule \texttt{eq_reflection} converts equality rewrites, while {\tt
1120 iff_reflection} converts if-and-only-if rewrites. The latter possibility
1121 can arise in two other ways: the negative theorem~$\neg P$ is converted to
1122 $P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
1123 $P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
1124 iff_reflection_T} accomplish this conversion.
1126 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
1127 val iff_reflection_F = P_iff_F RS iff_reflection;
1129 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
1130 val iff_reflection_T = P_iff_T RS iff_reflection;
1132 The function \texttt{mk_eq} converts a theorem to a meta-equality
1133 using the case analysis described above.
1135 fun mk_eq th = case concl_of th of
1136 _ $ (Const("op =",_)$_$_) => th RS eq_reflection
1137 | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
1138 | _ $ (Const("Not",_)$_) => th RS iff_reflection_F
1139 | _ => th RS iff_reflection_T;
1142 three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}
1143 will be composed together and supplied below to \texttt{setmksimps}.
1146 \subsection{Making the initial simpset}
1148 It is time to assemble these items. The list \texttt{IFOL_simps} contains the
1149 default rewrite rules for intuitionistic first-order logic. The first of
1150 these is the reflexive law expressed as the equivalence
1151 $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless.
1154 [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at
1155 imp_simps \at iff_simps \at quant_simps;
1157 The list \texttt{triv_rls} contains trivial theorems for the solver. Any
1158 subgoal that is simplified to one of these will be removed.
1160 val notFalseI = int_prove_fun "~False";
1161 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
1163 We also define the function \ttindex{mk_meta_cong} to convert the conclusion
1164 of congruence rules into meta-equalities.
1166 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));
1169 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It
1170 preprocess rewrites using
1171 {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
1172 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
1173 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals
1174 of conditional rewrites.
1176 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
1177 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
1178 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
1179 extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
1181 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
1182 \index{*addsimps}\index{*addcongs}
1184 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems),
1187 fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
1188 eq_assume_tac, ematch_tac [FalseE]];
1191 empty_ss setsubgoaler asm_simp_tac
1192 addsimprocs [defALL_regroup, defEX_regroup]
1193 setSSolver safe_solver
1194 setSolver unsafe_solver
1195 setmksimps (map mk_eq o atomize o gen_all)
1196 setmkcong mk_meta_cong;
1199 FOL_basic_ss addsimps (IFOL_simps {\at}
1200 int_ex_simps {\at} int_all_simps)
1201 addcongs [imp_cong];
1203 This simpset takes \texttt{imp_cong} as a congruence rule in order to use
1204 contextual information to simplify the conclusions of implications:
1205 \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
1206 (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
1208 By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
1209 effect for conjunctions.
1212 \index{simplification|)}
1215 %%% Local Variables:
1217 %%% TeX-master: "ref"