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{Accessing the current simpset}
273 \label{sec:access-current-simpset}
276 simpset : unit -> simpset
277 simpset_ref : unit -> simpset ref
278 simpset_of : theory -> simpset
279 simpset_ref_of : theory -> simpset ref
280 print_simpset : theory -> unit
281 SIMPSET :(simpset -> tactic) -> tactic
282 SIMPSET' :(simpset -> 'a -> tactic) -> 'a -> tactic
285 Each theory contains a current simpset\index{simpset!current} stored
286 within a private ML reference variable. This can be retrieved and
289 \begin{ttdescription}
291 \item[\ttindexbold{simpset}();] retrieves the simpset value from the
292 current theory context.
294 \item[\ttindexbold{simpset_ref}();] retrieves the simpset reference
295 variable from the current theory context. This can be assigned to
296 by using \texttt{:=} in ML.
298 \item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value
301 \item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
302 reference variable from theory $thy$.
304 \item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
305 of theory $thy$ in the same way as \texttt{print_ss}.
307 \item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
308 are tacticals that make a tactic depend on the implicit current
309 simpset of the theory associated with the proof state they are
315 There is a small difference between \texttt{(SIMPSET'~$tacf$)} and
316 \texttt{($tacf\,$(simpset()))}. For example \texttt{(SIMPSET'
317 simp_tac)} would depend on the theory of the proof state it is
318 applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
319 to the current theory context. Both are usually the same in proof
320 scripts, provided that goals are only stated within the current
321 theory. Robust programs would not count on that, of course.
325 \subsection{Rewrite rules}
327 addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
328 delsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
331 \index{rewrite rules|(} Rewrite rules are theorems expressing some
332 form of equality, for example:
334 Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\
335 \Var{P}\conj\Var{P} &\bimp& \Var{P} \\
336 \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
338 Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
339 0$ are also permitted; the conditions can be arbitrary formulas.
341 Internally, all rewrite rules are translated into meta-equalities,
342 theorems with conclusion $lhs \equiv rhs$. Each simpset contains a
343 function for extracting equalities from arbitrary theorems. For
344 example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
345 \equiv False$. This function can be installed using
346 \ttindex{setmksimps} but only the definer of a logic should need to do
347 this; see {\S}\ref{sec:setmksimps}. The function processes theorems
348 added by \texttt{addsimps} as well as local assumptions.
350 \begin{ttdescription}
352 \item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived
353 from $thms$ to the simpset $ss$.
355 \item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules
356 derived from $thms$ from the simpset $ss$.
361 The simplifier will accept all standard rewrite rules: those where
362 all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} =
363 {(\Var{i}+\Var{j})+\Var{k}}$ is OK.
365 It will also deal gracefully with all rules whose left-hand sides
366 are so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
367 \indexbold{higher-order pattern}\indexbold{pattern, higher-order}
368 These are terms in $\beta$-normal form (this will always be the case
369 unless you have done something strange) where each occurrence of an
370 unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are
371 distinct bound variables. Hence $(\forall x.\Var{P}(x) \land
372 \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall
373 x.\Var{Q}(x))$ is also OK, in both directions.
375 In some rare cases the rewriter will even deal with quite general
376 rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$
377 rewrites $g(a) \in range(g)$ to $True$, but will fail to match
378 $g(h(b)) \in range(\lambda x.g(h(x)))$. However, you can replace
379 the offending subterms (in our case $\Var{f}(\Var{x})$, which is not
380 a pattern) by adding new variables and conditions: $\Var{y} =
381 \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is
382 acceptable as a conditional rewrite rule since conditions can be
385 There is basically no restriction on the form of the right-hand
386 sides. They may not contain extraneous term or type variables,
389 \index{rewrite rules|)}
392 \subsection{*Simplification procedures}
394 addsimprocs : simpset * simproc list -> simpset
395 delsimprocs : simpset * simproc list -> simpset
398 Simplification procedures are {\ML} objects of abstract type
399 \texttt{simproc}. Basically they are just functions that may produce
400 \emph{proven} rewrite rules on demand. They are associated with
401 certain patterns that conceptually represent left-hand sides of
402 equations; these are shown by \texttt{print_ss}. During its
403 operation, the simplifier may offer a simplification procedure the
404 current redex and ask for a suitable rewrite rule. Thus rules may be
405 specifically fashioned for particular situations, resulting in a more
406 powerful mechanism than term rewriting by a fixed set of rules.
409 \begin{ttdescription}
411 \item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification
412 procedures $procs$ to the current simpset.
414 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification
415 procedures $procs$ from the current simpset.
419 For example, simplification procedures \ttindexbold{nat_cancel} of
420 \texttt{HOL/Arith} cancel common summands and constant factors out of
421 several relations of sums over natural numbers.
423 Consider the following goal, which after cancelling $a$ on both sides
424 contains a factor of $2$. Simplifying with the simpset of
425 \texttt{Arith.thy} will do the cancellation automatically:
427 {\out 1. x + a + x < y + y + 2 + a + a + a + a + a}
429 {\out 1. x < Suc (a + (a + y))}
433 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
435 addcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
436 delcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
437 addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
438 deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
441 Congruence rules are meta-equalities of the form
443 f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
445 This governs the simplification of the arguments of~$f$. For
446 example, some arguments can be simplified under additional assumptions:
447 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
448 \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
450 Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
451 rules from it when simplifying~$P@2$. Such local assumptions are
452 effective for rewriting formulae such as $x=0\imp y+x=y$. The local
453 assumptions are also provided as theorems to the solver; see
454 {\S}~\ref{sec:simp-solver} below.
456 \begin{ttdescription}
458 \item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
459 simpset $ss$. These are derived from $thms$ in an appropriate way,
460 depending on the underlying object-logic.
462 \item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
465 \item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
466 their internal form (conclusions using meta-equality) to simpset
467 $ss$. This is the basic mechanism that \texttt{addcongs} is built
468 on. It should be rarely used directly.
470 \item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
471 in internal form from simpset $ss$.
477 Here are some more examples. The congruence rule for bounded
478 quantifiers also supplies contextual information, this time about the
481 &&\List{\Var{A}=\Var{B};\;
482 \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
484 (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
486 The congruence rule for conditional expressions can supply contextual
487 information for simplifying the arms:
488 \[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
489 \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
490 if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
492 A congruence rule can also {\em prevent\/} simplification of some arguments.
493 Here is an alternative congruence rule for conditional expressions:
494 \[ \Var{p}=\Var{q} \Imp
495 if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
497 Only the first argument is simplified; the others remain unchanged.
498 This can make simplification much faster, but may require an extra case split
502 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
505 simpset * (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
506 prems_of_ss : simpset -> thm list
509 The subgoaler is the tactic used to solve subgoals arising out of
510 conditional rewrite rules or congruence rules. The default should be
511 simplification itself. Occasionally this strategy needs to be
512 changed. For example, if the premise of a conditional rule is an
513 instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m}
514 < \Var{n}$, the default strategy could loop.
516 \begin{ttdescription}
518 \item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of
519 $ss$ to $tacf$. The function $tacf$ will be applied to the current
520 simplifier context expressed as a simpset.
522 \item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of
523 premises from simplifier context $ss$. This may be non-empty only
524 if the simplifier has been told to utilize local assumptions in the
525 first place, e.g.\ if invoked via \texttt{asm_simp_tac}.
529 As an example, consider the following subgoaler:
533 resolve_tac (prems_of_ss ss) ORELSE'
536 This tactic first tries to solve the subgoal by assumption or by
537 resolving with with one of the premises, calling simplification only
541 \subsection{*The solver}\label{sec:simp-solver}
543 mk_solver : string -> (thm list -> int -> tactic) -> solver
544 setSolver : simpset * solver -> simpset \hfill{\bf infix 4}
545 addSolver : simpset * solver -> simpset \hfill{\bf infix 4}
546 setSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
547 addSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
550 A solver is a tactic that attempts to solve a subgoal after
551 simplification. Typically it just proves trivial subgoals such as
552 \texttt{True} and $t=t$. It could use sophisticated means such as {\tt
553 blast_tac}, though that could make simplification expensive.
554 To keep things more abstract, solvers are packaged up in type
555 \texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.
557 Rewriting does not instantiate unknowns. For example, rewriting
558 cannot prove $a\in \Var{A}$ since this requires
559 instantiating~$\Var{A}$. The solver, however, is an arbitrary tactic
560 and may instantiate unknowns as it pleases. This is the only way the
561 simplifier can handle a conditional rewrite rule whose condition
562 contains extra variables. When a simplification tactic is to be
563 combined with other provers, especially with the classical reasoner,
564 it is important whether it can be considered safe or not. For this
565 reason a simpset contains two solvers, a safe and an unsafe one.
567 The standard simplification strategy solely uses the unsafe solver,
568 which is appropriate in most cases. For special applications where
569 the simplification process is not allowed to instantiate unknowns
570 within the goal, simplification starts with the safe solver, but may
571 still apply the ordinary unsafe one in nested simplifications for
572 conditional rules or congruences. Note that in this way the overall
573 tactic is not totally safe: it may instantiate unknowns that appear also
576 \begin{ttdescription}
577 \item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
578 the string $s$ is only attached as a comment and has no other significance.
580 \item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the
581 \emph{safe} solver of $ss$.
583 \item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an
584 additional \emph{safe} solver; it will be tried after the solvers
585 which had already been present in $ss$.
587 \item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the
588 unsafe solver of $ss$.
590 \item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an
591 additional unsafe solver; it will be tried after the solvers which
592 had already been present in $ss$.
598 \index{assumptions!in simplification} The solver tactic is invoked
599 with a list of theorems, namely assumptions that hold in the local
600 context. This may be non-empty only if the simplifier has been told
601 to utilize local assumptions in the first place, e.g.\ if invoked via
602 \texttt{asm_simp_tac}. The solver is also presented the full goal
603 including its assumptions in any case. Thus it can use these (e.g.\
604 by calling \texttt{assume_tac}), even if the list of premises is not
609 As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
610 to solve the premises of congruence rules. These are usually of the
611 form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
612 needs to be instantiated with the result. Typically, the subgoaler
613 will invoke the simplifier at some point, which will eventually call
614 the solver. For this reason, solver tactics must be prepared to solve
615 goals of the form $t = \Var{x}$, usually by reflexivity. In
616 particular, reflexivity should be tried before any of the fancy
617 tactics like \texttt{blast_tac}.
619 It may even happen that due to simplification the subgoal is no longer
620 an equality. For example $False \bimp \Var{Q}$ could be rewritten to
621 $\neg\Var{Q}$. To cover this case, the solver could try resolving
622 with the theorem $\neg False$.
627 If a premise of a congruence rule cannot be proved, then the
628 congruence is ignored. This should only happen if the rule is
629 \emph{conditional} --- that is, contains premises not of the form $t
630 = \Var{x}$; otherwise it indicates that some congruence rule, or
631 possibly the subgoaler or solver, is faulty.
635 \subsection{*The looper}\label{sec:simp-looper}
637 setloop : simpset * (int -> tactic) -> simpset \hfill{\bf infix 4}
638 addloop : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
639 delloop : simpset * string -> simpset \hfill{\bf infix 4}
640 addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
641 delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
644 The looper is a list of tactics that are applied after simplification, in case
645 the solver failed to solve the simplified goal. If the looper
646 succeeds, the simplification process is started all over again. Each
647 of the subgoals generated by the looper is attacked in turn, in
650 A typical looper is \index{case splitting}: the expansion of a conditional.
651 Another possibility is to apply an elimination rule on the
652 assumptions. More adventurous loopers could start an induction.
654 \begin{ttdescription}
656 \item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
659 \item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
660 looper tactic with name $name$; it will be tried after the looper tactics
661 that had already been present in $ss$.
663 \item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
666 \item[$ss$ \ttindexbold{addsplits} $thms$] adds
667 split tactics for $thms$ as additional looper tactics of $ss$.
669 \item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
670 split tactics for $thms$ from the looper tactics of $ss$.
674 The splitter replaces applications of a given function; the right-hand side
675 of the replacement can be anything. For example, here is a splitting rule
676 for conditional expressions:
677 \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
678 \conj (\neg\Var{Q} \imp \Var{P}(\Var{y}))
680 Another example is the elimination operator for Cartesian products (which
681 happens to be called~$split$):
682 \[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
683 \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
686 For technical reasons, there is a distinction between case splitting in the
687 conclusion and in the premises of a subgoal. The former is done by
688 \texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split},
689 which do not split the subgoal, while the latter is done by
690 \texttt{split_asm_tac} with rules like \texttt{split_if_asm} or
691 \texttt{option.split_asm}, which split the subgoal.
692 The operator \texttt{addsplits} automatically takes care of which tactic to
693 call, analyzing the form of the rules given as argument.
695 Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
698 Case splits should be allowed only when necessary; they are expensive
699 and hard to control. Here is an example of use, where \texttt{split_if}
700 is the first rule above:
702 by (simp_tac (simpset()
703 addloop ("split if", split_tac [split_if])) 1);
705 Users would usually prefer the following shortcut using \texttt{addsplits}:
707 by (simp_tac (simpset() addsplits [split_if]) 1);
709 Case-splitting on conditional expressions is usually beneficial, so it is
710 enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.
713 \section{The simplification tactics}\label{simp-tactics}
714 \index{simplification!tactics}\index{tactics!simplification}
716 generic_simp_tac : bool -> bool * bool * bool ->
717 simpset -> int -> tactic
718 simp_tac : simpset -> int -> tactic
719 asm_simp_tac : simpset -> int -> tactic
720 full_simp_tac : simpset -> int -> tactic
721 asm_full_simp_tac : simpset -> int -> tactic
722 safe_asm_full_simp_tac : simpset -> int -> tactic
725 \texttt{generic_simp_tac} is the basic tactic that is underlying any actual
726 simplification work. The others are just instantiations of it. The rewriting
727 strategy is always strictly bottom up, except for congruence rules,
728 which are applied while descending into a term. Conditions in conditional
729 rewrite rules are solved recursively before the rewrite rule is applied.
731 \begin{ttdescription}
733 \item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)]
734 gives direct access to the various simplification modes:
736 \item if $safe$ is {\tt true}, the safe solver is used as explained in
737 {\S}\ref{sec:simp-solver},
738 \item $simp\_asm$ determines whether the local assumptions are simplified,
739 \item $use\_asm$ determines whether the assumptions are used as local rewrite
741 \item $mutual$ determines whether assumptions can simplify each other rather
742 than being processed from left to right.
744 This generic interface is intended
745 for building special tools, e.g.\ for combining the simplifier with the
746 classical reasoner. It is rarely used directly.
748 \item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
749 \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
750 the basic simplification tactics that work exactly like their
751 namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
752 explicitly supplied with a simpset.
758 Local modifications of simpsets within a proof are often much cleaner
759 by using above tactics in conjunction with explicit simpsets, rather
760 than their capitalized counterparts. For example
766 can be expressed more appropriately as
768 by (simp_tac (simpset() addsimps \(thms\)) \(i\));
773 Also note that functions depending implicitly on the current theory
774 context (like capital \texttt{Simp_tac} and the other commands of
775 {\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
776 actual proof scripts. In particular, ML programs like theory
777 definition packages or special tactics should refer to simpsets only
778 explicitly, via the above tactics used in conjunction with
779 \texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
782 \section{Forward rules and conversions}
783 \index{simplification!forward rules}\index{simplification!conversions}
784 \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}
785 simplify : simpset -> thm -> thm
786 asm_simplify : simpset -> thm -> thm
787 full_simplify : simpset -> thm -> thm
788 asm_full_simplify : simpset -> thm -> thm\medskip
789 Simplifier.rewrite : simpset -> cterm -> thm
790 Simplifier.asm_rewrite : simpset -> cterm -> thm
791 Simplifier.full_rewrite : simpset -> cterm -> thm
792 Simplifier.asm_full_rewrite : simpset -> cterm -> thm
795 The first four of these functions provide \emph{forward} rules for
796 simplification. Their effect is analogous to the corresponding
797 tactics described in {\S}\ref{simp-tactics}, but affect the whole
798 theorem instead of just a certain subgoal. Also note that the
799 looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
800 {\S}\ref{sec:simp-solver} is omitted in forward simplification.
802 The latter four are \emph{conversions}, establishing proven equations
803 of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
807 Forward simplification rules and conversions should be used rarely
808 in ordinary proof scripts. The main intention is to provide an
809 internal interface to the simplifier for special utilities.
813 \section{Permutative rewrite rules}
814 \index{rewrite rules!permutative|(}
816 A rewrite rule is {\bf permutative} if the left-hand side and right-hand
817 side are the same up to renaming of variables. The most common permutative
818 rule is commutativity: $x+y = y+x$. Other examples include $(x-y)-z =
819 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
820 for sets. Such rules are common enough to merit special attention.
822 Because ordinary rewriting loops given such rules, the simplifier
823 employs a special strategy, called {\bf ordered
824 rewriting}\index{rewriting!ordered}. There is a standard
825 lexicographic ordering on terms. This should be perfectly OK in most
826 cases, but can be changed for special applications.
829 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
831 \begin{ttdescription}
833 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as
834 term order in simpset $ss$.
840 A permutative rewrite rule is applied only if it decreases the given
841 term with respect to this ordering. For example, commutativity
842 rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less
843 than $b+a$. The Boyer-Moore theorem prover~\cite{bm88book} also
844 employs ordered rewriting.
846 Permutative rewrite rules are added to simpsets just like other
847 rewrite rules; the simplifier recognizes their special status
848 automatically. They are most effective in the case of
849 associative-commutative operators. (Associativity by itself is not
850 permutative.) When dealing with an AC-operator~$f$, keep the
851 following points in mind:
852 \begin{itemize}\index{associative-commutative operators}
854 \item The associative law must always be oriented from left to right,
855 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
856 used with commutativity, leads to looping in conjunction with the
859 \item To complete your set of rewrite rules, you must add not just
860 associativity~(A) and commutativity~(C) but also a derived rule, {\bf
861 left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
863 Ordered rewriting with the combination of A, C, and~LC sorts a term
865 \[\def\maps#1{\stackrel{#1}{\longmapsto}}
866 (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \]
867 Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
868 examples; other algebraic structures are amenable to ordered rewriting,
869 such as boolean rings.
871 \subsection{Example: sums of natural numbers}
873 This example is again set in HOL (see \texttt{HOL/ex/NatSum}). Theory
874 \thydx{Arith} contains natural numbers arithmetic. Its associated simpset
875 contains many arithmetic laws including distributivity of~$\times$ over~$+$,
876 while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
877 type \texttt{nat}. Let us prove the theorem
878 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
880 A functional~\texttt{sum} represents the summation operator under the
881 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We
882 extend \texttt{Arith} as follows:
885 consts sum :: [nat=>nat, nat] => nat
888 "sum f (Suc n) = f(n) + sum f n"
891 The \texttt{primrec} declaration automatically adds rewrite rules for
892 \texttt{sum} to the default simpset. We now remove the
893 \texttt{nat_cancel} simplification procedures (in order not to spoil
894 the example) and insert the AC-rules for~$+$:
896 Delsimprocs nat_cancel;
899 Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
900 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:
902 Goal "2 * sum (\%i.i) (Suc n) = n * Suc n";
904 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
905 {\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
907 Induction should not be applied until the goal is in the simplest
912 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
913 {\out 1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
915 Ordered rewriting has sorted the terms in the left-hand side. The
916 subgoal is now ready for induction:
918 by (induct_tac "n" 1);
920 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
921 {\out 1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
923 {\out 2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
924 {\out ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =}
927 Simplification proves both subgoals immediately:\index{*ALLGOALS}
929 by (ALLGOALS Asm_simp_tac);
931 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
934 Simplification cannot prove the induction step if we omit \texttt{add_ac} from
935 the simpset. Observe that like terms have not been collected:
938 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
939 {\out 1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n}
940 {\out ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =}
941 {\out n + (n + (n + n * n))}
943 Ordered rewriting proves this by sorting the left-hand side. Proving
944 arithmetic theorems without ordered rewriting requires explicit use of
945 commutativity. This is tedious; try it and see!
947 Ordered rewriting is equally successful in proving
948 $\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
951 \subsection{Re-orienting equalities}
952 Ordered rewriting with the derived rule \texttt{symmetry} can reverse
955 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
956 (fn _ => [Blast_tac 1]);
958 This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs
959 in the conclusion but not~$s$, can often be brought into the right form.
960 For example, ordered rewriting with \texttt{symmetry} can prove the goal
961 \[ f(a)=b \conj f(a)=c \imp b=c. \]
962 Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
963 because $f(a)$ is lexicographically greater than $b$ and~$c$. These
964 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
965 conclusion by~$f(a)$.
967 Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
968 The differing orientations make this appear difficult to prove. Ordered
969 rewriting with \texttt{symmetry} makes the equalities agree. (Without
970 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
971 or~$u=t$.) Then the simplifier can prove the goal outright.
973 \index{rewrite rules!permutative|)}
976 \section{*Coding simplification procedures}
978 val Simplifier.simproc: Sign.sg -> string -> string list
979 -> (Sign.sg -> simpset -> term -> thm option) -> simproc
980 val Simplifier.simproc_i: Sign.sg -> string -> term list
981 -> (Sign.sg -> simpset -> term -> thm option) -> simproc
984 \begin{ttdescription}
985 \item[\ttindexbold{Simplifier.simproc}~$sign$~$name$~$lhss$~$proc$] makes
986 $proc$ a simplification procedure for left-hand side patterns $lhss$. The
987 name just serves as a comment. The function $proc$ may be invoked by the
988 simplifier for redex positions matched by one of $lhss$ as described below
989 (which are be specified as strings to be read as terms).
991 \item[\ttindexbold{Simplifier.simproc_i}] is similar to
992 \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument.
995 Simplification procedures are applied in a two-stage process as
996 follows: The simplifier tries to match the current redex position
997 against any one of the $lhs$ patterns of any simplification procedure.
998 If this succeeds, it invokes the corresponding {\ML} function, passing
999 with the current signature, local assumptions and the (potential)
1000 redex. The result may be either \texttt{None} (indicating failure) or
1001 \texttt{Some~$thm$}.
1003 Any successful result is supposed to be a (possibly conditional)
1004 rewrite rule $t \equiv u$ that is applicable to the current redex.
1005 The rule will be applied just as any ordinary rewrite rule. It is
1006 expected to be already in \emph{internal form}, though, bypassing the
1007 automatic preprocessing of object-level equivalences.
1011 As an example of how to write your own simplification procedures,
1012 consider eta-expansion of pair abstraction (see also
1013 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
1014 model checker syntax).
1016 The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
1017 \texttt{split} together with some concrete syntax supporting
1018 $\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic
1019 that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
1020 to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is:
1022 pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y))
1024 Unfortunately, term rewriting using this rule directly would not
1025 terminate! We now use the simplification procedure mechanism in order
1026 to stop the simplifier from applying this rule over and over again,
1027 making it rewrite only actual abstractions. The simplification
1028 procedure \texttt{pair_eta_expand_proc} is defined as follows:
1030 val pair_eta_expand_proc =
1031 Simplifier.simproc (Theory.sign_of (the_context ()))
1032 "pair_eta_expand" ["f::'a*'b=>'c"]
1033 (fn _ => fn _ => fn t =>
1034 case t of Abs _ => Some (mk_meta_eq pair_eta_expand)
1037 This is an example of using \texttt{pair_eta_expand_proc}:
1039 {\out 1. P (\%p::'a * 'a. fst p + snd p + z)}
1040 by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1);
1041 {\out 1. P (\%(x::'a,y::'a). x + y + z)}
1046 In the above example the simplification procedure just did fine
1047 grained control over rule application, beyond higher-order pattern
1048 matching. Usually, procedures would do some more work, in particular
1049 prove particular theorems depending on the current redex.
1052 \section{*Setting up the Simplifier}\label{sec:setting-up-simp}
1053 \index{simplification!setting up}
1055 Setting up the simplifier for new logics is complicated in the general case.
1056 This section describes how the simplifier is installed for intuitionistic
1057 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
1060 The case splitting tactic, which resides on a separate files, is not part of
1061 Pure Isabelle. It needs to be loaded explicitly by the object-logic as
1062 follows (below \texttt{\~\relax\~\relax} refers to \texttt{\$ISABELLE_HOME}):
1064 use "\~\relax\~\relax/src/Provers/splitter.ML";
1067 Simplification requires converting object-equalities to meta-level rewrite
1068 rules. This demands rules stating that equal terms and equivalent formulae
1069 are also equal at the meta-level. The rule declaration part of the file
1070 \texttt{FOL/IFOL.thy} contains the two lines
1071 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
1072 eq_reflection "(x=y) ==> (x==y)"
1073 iff_reflection "(P<->Q) ==> (P==Q)"
1075 Of course, you should only assert such rules if they are true for your
1076 particular logic. In Constructive Type Theory, equality is a ternary
1077 relation of the form $a=b\in A$; the type~$A$ determines the meaning
1078 of the equality essentially as a partial equivalence relation. The
1079 present simplifier cannot be used. Rewriting in \texttt{CTT} uses
1080 another simplifier, which resides in the file {\tt
1081 Provers/typedsimp.ML} and is not documented. Even this does not
1082 work for later variants of Constructive Type Theory that use
1083 intensional equality~\cite{nordstrom90}.
1086 \subsection{A collection of standard rewrite rules}
1088 We first prove lots of standard rewrite rules about the logical
1089 connectives. These include cancellation and associative laws. We
1090 define a function that echoes the desired law and then supplies it the
1091 prover for intuitionistic FOL:
1093 fun int_prove_fun s =
1095 prove_goal IFOL.thy s
1096 (fn prems => [ (cut_facts_tac prems 1),
1097 (IntPr.fast_tac 1) ]));
1099 The following rewrite rules about conjunction are a selection of those
1100 proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the
1103 val conj_simps = map int_prove_fun
1104 ["P & True <-> P", "True & P <-> P",
1105 "P & False <-> False", "False & P <-> False",
1107 "P & ~P <-> False", "~P & P <-> False",
1108 "(P & Q) & R <-> P & (Q & R)"];
1110 The file also proves some distributive laws. As they can cause exponential
1111 blowup, they will not be included in the standard simpset. Instead they
1112 are merely bound to an \ML{} identifier, for user reference.
1114 val distrib_simps = map int_prove_fun
1115 ["P & (Q | R) <-> P&Q | P&R",
1116 "(Q | R) & P <-> Q&P | R&P",
1117 "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
1121 \subsection{Functions for preprocessing the rewrite rules}
1122 \label{sec:setmksimps}
1123 \begin{ttbox}\indexbold{*setmksimps}
1124 setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
1126 The next step is to define the function for preprocessing rewrite rules.
1127 This will be installed by calling \texttt{setmksimps} below. Preprocessing
1128 occurs whenever rewrite rules are added, whether by user command or
1129 automatically. Preprocessing involves extracting atomic rewrites at the
1130 object-level, then reflecting them to the meta-level.
1132 To start, the function \texttt{gen_all} strips any meta-level
1133 quantifiers from the front of the given theorem.
1135 The function \texttt{atomize} analyses a theorem in order to extract
1136 atomic rewrite rules. The head of all the patterns, matched by the
1137 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
1139 fun atomize th = case concl_of th of
1140 _ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at
1141 atomize(th RS conjunct2)
1142 | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
1143 | _ $ (Const("All",_) $ _) => atomize(th RS spec)
1144 | _ $ (Const("True",_)) => []
1145 | _ $ (Const("False",_)) => []
1148 There are several cases, depending upon the form of the conclusion:
1150 \item Conjunction: extract rewrites from both conjuncts.
1151 \item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
1152 extract rewrites from~$Q$; these will be conditional rewrites with the
1154 \item Universal quantification: remove the quantifier, replacing the bound
1155 variable by a schematic variable, and extract rewrites from the body.
1156 \item \texttt{True} and \texttt{False} contain no useful rewrites.
1157 \item Anything else: return the theorem in a singleton list.
1159 The resulting theorems are not literally atomic --- they could be
1160 disjunctive, for example --- but are broken down as much as possible.
1161 See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
1162 set-theoretic formulae into rewrite rules.
1164 For standard situations like the above,
1165 there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a
1166 list of pairs $(name, thms)$, where $name$ is an operator name and
1167 $thms$ is a list of theorems to resolve with in case the pattern matches,
1168 and returns a suitable \texttt{atomize} function.
1171 The simplified rewrites must now be converted into meta-equalities. The
1172 rule \texttt{eq_reflection} converts equality rewrites, while {\tt
1173 iff_reflection} converts if-and-only-if rewrites. The latter possibility
1174 can arise in two other ways: the negative theorem~$\neg P$ is converted to
1175 $P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
1176 $P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
1177 iff_reflection_T} accomplish this conversion.
1179 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
1180 val iff_reflection_F = P_iff_F RS iff_reflection;
1182 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
1183 val iff_reflection_T = P_iff_T RS iff_reflection;
1185 The function \texttt{mk_eq} converts a theorem to a meta-equality
1186 using the case analysis described above.
1188 fun mk_eq th = case concl_of th of
1189 _ $ (Const("op =",_)$_$_) => th RS eq_reflection
1190 | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
1191 | _ $ (Const("Not",_)$_) => th RS iff_reflection_F
1192 | _ => th RS iff_reflection_T;
1195 three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}
1196 will be composed together and supplied below to \texttt{setmksimps}.
1199 \subsection{Making the initial simpset}
1201 It is time to assemble these items. The list \texttt{IFOL_simps} contains the
1202 default rewrite rules for intuitionistic first-order logic. The first of
1203 these is the reflexive law expressed as the equivalence
1204 $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless.
1207 [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at
1208 imp_simps \at iff_simps \at quant_simps;
1210 The list \texttt{triv_rls} contains trivial theorems for the solver. Any
1211 subgoal that is simplified to one of these will be removed.
1213 val notFalseI = int_prove_fun "~False";
1214 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
1216 We also define the function \ttindex{mk_meta_cong} to convert the conclusion
1217 of congruence rules into meta-equalities.
1219 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));
1222 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It
1223 preprocess rewrites using
1224 {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
1225 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
1226 detecting contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals
1227 of conditional rewrites.
1229 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
1230 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
1231 IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
1232 extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
1234 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
1235 \index{*addsimps}\index{*addcongs}
1237 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems),
1240 fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
1241 eq_assume_tac, ematch_tac [FalseE]];
1244 empty_ss setsubgoaler asm_simp_tac
1245 addsimprocs [defALL_regroup, defEX_regroup]
1246 setSSolver safe_solver
1247 setSolver unsafe_solver
1248 setmksimps (map mk_eq o atomize o gen_all)
1249 setmkcong mk_meta_cong;
1252 FOL_basic_ss addsimps (IFOL_simps {\at}
1253 int_ex_simps {\at} int_all_simps)
1254 addcongs [imp_cong];
1256 This simpset takes \texttt{imp_cong} as a congruence rule in order to use
1257 contextual information to simplify the conclusions of implications:
1258 \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
1259 (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
1261 By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
1262 effect for conjunctions.
1265 \subsection{Splitter setup}\index{simplification!setting up the splitter}
1267 To set up case splitting, we have to call the \ML{} functor \ttindex{
1268 SplitterFun}, which takes the argument signature \texttt{SPLITTER_DATA}.
1269 So we prove the theorem \texttt{meta_eq_to_iff} below and store it, together
1270 with the \texttt{mk_eq} function described above and several standard
1271 theorems, in the structure \texttt{SplitterData}. Calling the functor with
1272 this data yields a new instantiation of the splitter for our logic.
1274 val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
1275 (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
1277 structure SplitterData =
1279 structure Simplifier = Simplifier
1281 val meta_eq_to_iff = meta_eq_to_iff
1286 val contrapos = contrapos
1287 val contrapos2 = contrapos2
1288 val notnotD = notnotD
1291 structure Splitter = SplitterFun(SplitterData);
1295 \index{simplification|)}
1298 %%% Local Variables:
1300 %%% TeX-master: "ref"