doc-src/Ref/simplifier.tex
author wenzelm
Sat Jan 12 16:37:58 2002 +0100 (2002-01-12 ago)
changeset 12725 7ede865e1fe5
parent 12717 2d6b5e22e05d
child 13474 f326c5d97d76
permissions -rw-r--r--
renamed forall_elim_vars_safe to gen_all;
     1 %% $Id$
     2 \chapter{Simplification}
     3 \label{chap:simplification}
     4 \index{simplification|(}
     5 
     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.
    11 
    12 The first section is a quick introduction to the simplifier that
    13 should be sufficient to get started.  The later sections explain more
    14 advanced features.
    15 
    16 
    17 \section{Simplification for dummies}
    18 \label{sec:simp-for-dummies}
    19 
    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
    25 context.
    26 
    27 \begin{warn}
    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.
    32 \end{warn}
    33 
    34 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs}
    35 \begin{ttbox}
    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}
    42 \end{ttbox}
    43 
    44 \begin{ttdescription}
    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.
    48   
    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.
    52   
    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).
    56   
    57 \item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$,
    58   but also simplifies the assumptions. In particular, assumptions can
    59   simplify each other.
    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.
    69 \end{ttdescription}
    70 
    71 \medskip
    72 
    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:
    76 \begin{ttbox}
    77 context Arith.thy;
    78 Goal "0 + (x + 0) = x + 0 + 0";
    79 {\out  1. 0 + (x + 0) = x + 0 + 0}
    80 by (Simp_tac 1);
    81 {\out Level 1}
    82 {\out 0 + (x + 0) = x + 0 + 0}
    83 {\out No subgoals!}
    84 \end{ttbox}
    85 
    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} =
    88 \Var{n}$.
    89 
    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:
    93 \begin{ttbox}
    94 {\out  1. x = 0 ==> x + x = 0}
    95 by (Asm_simp_tac 1);
    96 \end{ttbox}
    97 
    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
   100 example,
   101 \begin{ttbox}
   102 {\out  1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}
   103 \end{ttbox}
   104 is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt
   105   Asm_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.
   110  
   111 \begin{warn}
   112   \verb$Asm_full_simp_tac$ may miss opportunities to simplify an assumption
   113   $A@i$ using an assumption $A@j$ in case $A@j$ is to the right of $A@i$.
   114   For example, given the subgoal
   115 \begin{ttbox}
   116 {\out [| \dots f a \dots; P a; ALL x. P x --> f x = g x |] ==> \dots}
   117 \end{ttbox}
   118 \verb$Asm_full_simp_tac$ will not simplify the \texttt{f a} on the left.
   119 This problem can be overcome by reordering assumptions (see
   120 {\S}\ref{sec:reordering-asms}). Future versions of \verb$Asm_full_simp_tac$
   121 will not suffer from this deficiency.
   122 \end{warn}
   123 
   124 \medskip
   125 
   126 Using the simplifier effectively may take a bit of experimentation.
   127 Set the \verb$trace_simp$\index{tracing!of simplification} flag to get
   128 a better idea of what is going on.  The resulting output can be
   129 enormous, especially since invocations of the simplifier are often
   130 nested (e.g.\ when solving conditions of rewrite rules).
   131 
   132 
   133 \subsection{Modifying the current simpset}
   134 \begin{ttbox}
   135 Addsimps    : thm list -> unit
   136 Delsimps    : thm list -> unit
   137 Addsimprocs : simproc list -> unit
   138 Delsimprocs : simproc list -> unit
   139 Addcongs    : thm list -> unit
   140 Delcongs    : thm list -> unit
   141 Addsplits   : thm list -> unit
   142 Delsplits   : thm list -> unit
   143 \end{ttbox}
   144 
   145 Depending on the theory context, the \texttt{Add} and \texttt{Del}
   146 functions manipulate basic components of the associated current
   147 simpset.  Internally, all rewrite rules have to be expressed as
   148 (conditional) meta-equalities.  This form is derived automatically
   149 from object-level equations that are supplied by the user.  Another
   150 source of rewrite rules are \emph{simplification procedures}, that is
   151 \ML\ functions that produce suitable theorems on demand, depending on
   152 the current redex.  Congruences are a more advanced feature; see
   153 {\S}\ref{sec:simp-congs}.
   154 
   155 \begin{ttdescription}
   156 
   157 \item[\ttindexbold{Addsimps} $thms$;] adds rewrite rules derived from
   158   $thms$ to the current simpset.
   159   
   160 \item[\ttindexbold{Delsimps} $thms$;] deletes rewrite rules derived
   161   from $thms$ from the current simpset.
   162   
   163 \item[\ttindexbold{Addsimprocs} $procs$;] adds simplification
   164   procedures $procs$ to the current simpset.
   165   
   166 \item[\ttindexbold{Delsimprocs} $procs$;] deletes simplification
   167   procedures $procs$ from the current simpset.
   168   
   169 \item[\ttindexbold{Addcongs} $thms$;] adds congruence rules to the
   170   current simpset.
   171   
   172 \item[\ttindexbold{Delcongs} $thms$;] deletes congruence rules from the
   173   current simpset.
   174 
   175 \item[\ttindexbold{Addsplits} $thms$;] adds splitting rules to the
   176   current simpset.
   177   
   178 \item[\ttindexbold{Delsplits} $thms$;] deletes splitting rules from the
   179   current simpset.
   180 
   181 \end{ttdescription}
   182 
   183 When a new theory is built, its implicit simpset is initialized by the union
   184 of the respective simpsets of its parent theories.  In addition, certain
   185 theory definition constructs (e.g.\ \ttindex{datatype} and \ttindex{primrec}
   186 in HOL) implicitly augment the current simpset.  Ordinary definitions are not
   187 added automatically!
   188 
   189 It is up the user to manipulate the current simpset further by
   190 explicitly adding or deleting theorems and simplification procedures.
   191 
   192 \medskip
   193 
   194 Good simpsets are hard to design.  Rules that obviously simplify,
   195 like $\Var{n}+0 = \Var{n}$, should be added to the current simpset right after
   196 they have been proved.  More specific ones (such as distributive laws, which
   197 duplicate subterms) should be added only for specific proofs and deleted
   198 afterwards.  Conversely, sometimes a rule needs
   199 to be removed for a certain proof and restored afterwards.  The need of
   200 frequent additions or deletions may indicate a badly designed
   201 simpset.
   202 
   203 \begin{warn}
   204   The union of the parent simpsets (as described above) is not always
   205   a good starting point for the new theory.  If some ancestors have
   206   deleted simplification rules because they are no longer wanted,
   207   while others have left those rules in, then the union will contain
   208   the unwanted rules.  After this union is formed, changes to 
   209   a parent simpset have no effect on the child simpset.
   210 \end{warn}
   211 
   212 
   213 \section{Simplification sets}\index{simplification sets} 
   214 
   215 The simplifier is controlled by information contained in {\bf
   216   simpsets}.  These consist of several components, including rewrite
   217 rules, simplification procedures, congruence rules, and the subgoaler,
   218 solver and looper tactics.  The simplifier should be set up with
   219 sensible defaults so that most simplifier calls specify only rewrite
   220 rules or simplification procedures.  Experienced users can exploit the
   221 other components to streamline proofs in more sophisticated manners.
   222 
   223 \subsection{Inspecting simpsets}
   224 \begin{ttbox}
   225 print_ss : simpset -> unit
   226 rep_ss   : simpset -> \{mss        : meta_simpset, 
   227                        subgoal_tac: simpset  -> int -> tactic,
   228                        loop_tacs  : (string * (int -> tactic))list,
   229                        finish_tac : solver list,
   230                 unsafe_finish_tac : solver list\}
   231 \end{ttbox}
   232 \begin{ttdescription}
   233   
   234 \item[\ttindexbold{print_ss} $ss$;] displays the printable contents of
   235   simpset $ss$.  This includes the rewrite rules and congruences in
   236   their internal form expressed as meta-equalities.  The names of the
   237   simplification procedures and the patterns they are invoked on are
   238   also shown.  The other parts, functions and tactics, are
   239   non-printable.
   240 
   241 \item[\ttindexbold{rep_ss} $ss$;] decomposes $ss$ as a record of its internal 
   242   components, namely the meta_simpset, the subgoaler, the loop, and the safe
   243   and unsafe solvers.
   244 
   245 \end{ttdescription}
   246 
   247 
   248 \subsection{Building simpsets}
   249 \begin{ttbox}
   250 empty_ss : simpset
   251 merge_ss : simpset * simpset -> simpset
   252 \end{ttbox}
   253 \begin{ttdescription}
   254   
   255 \item[\ttindexbold{empty_ss}] is the empty simpset.  This is not very useful
   256   under normal circumstances because it doesn't contain suitable tactics
   257   (subgoaler etc.).  When setting up the simplifier for a particular
   258   object-logic, one will typically define a more appropriate ``almost empty''
   259   simpset.  For example, in HOL this is called \ttindexbold{HOL_basic_ss}.
   260   
   261 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$
   262   and $ss@2$ by building the union of their respective rewrite rules,
   263   simplification procedures and congruences.  The other components
   264   (tactics etc.) cannot be merged, though; they are taken from either
   265   simpset\footnote{Actually from $ss@1$, but it would unwise to count
   266     on that.}.
   267 
   268 \end{ttdescription}
   269 
   270 
   271 \subsection{Accessing the current simpset}
   272 \label{sec:access-current-simpset}
   273 
   274 \begin{ttbox}
   275 simpset        : unit   -> simpset
   276 simpset_ref    : unit   -> simpset ref
   277 simpset_of     : theory -> simpset
   278 simpset_ref_of : theory -> simpset ref
   279 print_simpset  : theory -> unit
   280 SIMPSET        :(simpset ->       tactic) ->       tactic
   281 SIMPSET'       :(simpset -> 'a -> tactic) -> 'a -> tactic
   282 \end{ttbox}
   283 
   284 Each theory contains a current simpset\index{simpset!current} stored
   285 within a private ML reference variable.  This can be retrieved and
   286 modified as follows.
   287 
   288 \begin{ttdescription}
   289   
   290 \item[\ttindexbold{simpset}();] retrieves the simpset value from the
   291   current theory context.
   292   
   293 \item[\ttindexbold{simpset_ref}();] retrieves the simpset reference
   294   variable from the current theory context.  This can be assigned to
   295   by using \texttt{:=} in ML.
   296   
   297 \item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value
   298   from theory $thy$.
   299   
   300 \item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
   301   reference variable from theory $thy$.
   302 
   303 \item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
   304   of theory $thy$ in the same way as \texttt{print_ss}.
   305 
   306 \item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
   307   are tacticals that make a tactic depend on the implicit current
   308   simpset of the theory associated with the proof state they are
   309   applied on.
   310 
   311 \end{ttdescription}
   312 
   313 \begin{warn}
   314   There is a small difference between \texttt{(SIMPSET'~$tacf$)} and
   315   \texttt{($tacf\,$(simpset()))}.  For example \texttt{(SIMPSET'
   316     simp_tac)} would depend on the theory of the proof state it is
   317   applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
   318   to the current theory context.  Both are usually the same in proof
   319   scripts, provided that goals are only stated within the current
   320   theory.  Robust programs would not count on that, of course.
   321 \end{warn}
   322 
   323 
   324 \subsection{Rewrite rules}
   325 \begin{ttbox}
   326 addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
   327 delsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
   328 \end{ttbox}
   329 
   330 \index{rewrite rules|(} Rewrite rules are theorems expressing some
   331 form of equality, for example:
   332 \begin{eqnarray*}
   333   Suc(\Var{m}) + \Var{n} &=&      \Var{m} + Suc(\Var{n}) \\
   334   \Var{P}\conj\Var{P}    &\bimp&  \Var{P} \\
   335   \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
   336 \end{eqnarray*}
   337 Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
   338 0$ are also permitted; the conditions can be arbitrary formulas.
   339 
   340 Internally, all rewrite rules are translated into meta-equalities,
   341 theorems with conclusion $lhs \equiv rhs$.  Each simpset contains a
   342 function for extracting equalities from arbitrary theorems.  For
   343 example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
   344 \equiv False$.  This function can be installed using
   345 \ttindex{setmksimps} but only the definer of a logic should need to do
   346 this; see {\S}\ref{sec:setmksimps}.  The function processes theorems
   347 added by \texttt{addsimps} as well as local assumptions.
   348 
   349 \begin{ttdescription}
   350   
   351 \item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived
   352   from $thms$ to the simpset $ss$.
   353   
   354 \item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules
   355   derived from $thms$ from the simpset $ss$.
   356 
   357 \end{ttdescription}
   358 
   359 \begin{warn}
   360   The simplifier will accept all standard rewrite rules: those where
   361   all unknowns are of base type.  Hence ${\Var{i}+(\Var{j}+\Var{k})} =
   362   {(\Var{i}+\Var{j})+\Var{k}}$ is OK.
   363   
   364   It will also deal gracefully with all rules whose left-hand sides
   365   are so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
   366   \indexbold{higher-order pattern}\indexbold{pattern, higher-order}
   367   These are terms in $\beta$-normal form (this will always be the case
   368   unless you have done something strange) where each occurrence of an
   369   unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are
   370   distinct bound variables. Hence $(\forall x.\Var{P}(x) \land
   371   \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall
   372   x.\Var{Q}(x))$ is also OK, in both directions.
   373   
   374   In some rare cases the rewriter will even deal with quite general
   375   rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$
   376   rewrites $g(a) \in range(g)$ to $True$, but will fail to match
   377   $g(h(b)) \in range(\lambda x.g(h(x)))$.  However, you can replace
   378   the offending subterms (in our case $\Var{f}(\Var{x})$, which is not
   379   a pattern) by adding new variables and conditions: $\Var{y} =
   380   \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is
   381   acceptable as a conditional rewrite rule since conditions can be
   382   arbitrary terms.
   383   
   384   There is basically no restriction on the form of the right-hand
   385   sides.  They may not contain extraneous term or type variables,
   386   though.
   387 \end{warn}
   388 \index{rewrite rules|)}
   389 
   390 
   391 \subsection{*Simplification procedures}
   392 \begin{ttbox}
   393 addsimprocs : simpset * simproc list -> simpset
   394 delsimprocs : simpset * simproc list -> simpset
   395 \end{ttbox}
   396 
   397 Simplification procedures are {\ML} objects of abstract type
   398 \texttt{simproc}.  Basically they are just functions that may produce
   399 \emph{proven} rewrite rules on demand.  They are associated with
   400 certain patterns that conceptually represent left-hand sides of
   401 equations; these are shown by \texttt{print_ss}.  During its
   402 operation, the simplifier may offer a simplification procedure the
   403 current redex and ask for a suitable rewrite rule.  Thus rules may be
   404 specifically fashioned for particular situations, resulting in a more
   405 powerful mechanism than term rewriting by a fixed set of rules.
   406 
   407 
   408 \begin{ttdescription}
   409   
   410 \item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification
   411   procedures $procs$ to the current simpset.
   412   
   413 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification
   414   procedures $procs$ from the current simpset.
   415 
   416 \end{ttdescription}
   417 
   418 For example, simplification procedures \ttindexbold{nat_cancel} of
   419 \texttt{HOL/Arith} cancel common summands and constant factors out of
   420 several relations of sums over natural numbers.
   421 
   422 Consider the following goal, which after cancelling $a$ on both sides
   423 contains a factor of $2$.  Simplifying with the simpset of
   424 \texttt{Arith.thy} will do the cancellation automatically:
   425 \begin{ttbox}
   426 {\out 1. x + a + x < y + y + 2 + a + a + a + a + a}
   427 by (Simp_tac 1);
   428 {\out 1. x < Suc (a + (a + y))}
   429 \end{ttbox}
   430 
   431 
   432 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
   433 \begin{ttbox}
   434 addcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
   435 delcongs   : simpset * thm list -> simpset \hfill{\bf infix 4}
   436 addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
   437 deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
   438 \end{ttbox}
   439 
   440 Congruence rules are meta-equalities of the form
   441 \[ \dots \Imp
   442    f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
   443 \]
   444 This governs the simplification of the arguments of~$f$.  For
   445 example, some arguments can be simplified under additional assumptions:
   446 \[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
   447    \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
   448 \]
   449 Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
   450 rules from it when simplifying~$P@2$.  Such local assumptions are
   451 effective for rewriting formulae such as $x=0\imp y+x=y$.  The local
   452 assumptions are also provided as theorems to the solver; see
   453 {\S}~\ref{sec:simp-solver} below.
   454 
   455 \begin{ttdescription}
   456   
   457 \item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
   458   simpset $ss$.  These are derived from $thms$ in an appropriate way,
   459   depending on the underlying object-logic.
   460   
   461 \item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
   462   derived from $thms$.
   463   
   464 \item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
   465   their internal form (conclusions using meta-equality) to simpset
   466   $ss$.  This is the basic mechanism that \texttt{addcongs} is built
   467   on.  It should be rarely used directly.
   468   
   469 \item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
   470   in internal form from simpset $ss$.
   471   
   472 \end{ttdescription}
   473 
   474 \medskip
   475 
   476 Here are some more examples.  The congruence rule for bounded
   477 quantifiers also supplies contextual information, this time about the
   478 bound variable:
   479 \begin{eqnarray*}
   480   &&\List{\Var{A}=\Var{B};\; 
   481           \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
   482  &&\qquad\qquad
   483     (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
   484 \end{eqnarray*}
   485 The congruence rule for conditional expressions can supply contextual
   486 information for simplifying the arms:
   487 \[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
   488          \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
   489    if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
   490 \]
   491 A congruence rule can also {\em prevent\/} simplification of some arguments.
   492 Here is an alternative congruence rule for conditional expressions:
   493 \[ \Var{p}=\Var{q} \Imp
   494    if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
   495 \]
   496 Only the first argument is simplified; the others remain unchanged.
   497 This can make simplification much faster, but may require an extra case split
   498 to prove the goal.  
   499 
   500 
   501 \subsection{*The subgoaler}\label{sec:simp-subgoaler}
   502 \begin{ttbox}
   503 setsubgoaler :
   504   simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
   505 prems_of_ss  : simpset -> thm list
   506 \end{ttbox}
   507 
   508 The subgoaler is the tactic used to solve subgoals arising out of
   509 conditional rewrite rules or congruence rules.  The default should be
   510 simplification itself.  Occasionally this strategy needs to be
   511 changed.  For example, if the premise of a conditional rule is an
   512 instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m}
   513 < \Var{n}$, the default strategy could loop.
   514 
   515 \begin{ttdescription}
   516   
   517 \item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of
   518   $ss$ to $tacf$.  The function $tacf$ will be applied to the current
   519   simplifier context expressed as a simpset.
   520   
   521 \item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of
   522   premises from simplifier context $ss$.  This may be non-empty only
   523   if the simplifier has been told to utilize local assumptions in the
   524   first place, e.g.\ if invoked via \texttt{asm_simp_tac}.
   525 
   526 \end{ttdescription}
   527 
   528 As an example, consider the following subgoaler:
   529 \begin{ttbox}
   530 fun subgoaler ss =
   531     assume_tac ORELSE'
   532     resolve_tac (prems_of_ss ss) ORELSE'
   533     asm_simp_tac ss;
   534 \end{ttbox}
   535 This tactic first tries to solve the subgoal by assumption or by
   536 resolving with with one of the premises, calling simplification only
   537 if that fails.
   538 
   539 
   540 \subsection{*The solver}\label{sec:simp-solver}
   541 \begin{ttbox}
   542 mk_solver  : string -> (thm list -> int -> tactic) -> solver
   543 setSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
   544 addSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
   545 setSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
   546 addSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
   547 \end{ttbox}
   548 
   549 A solver is a tactic that attempts to solve a subgoal after
   550 simplification.  Typically it just proves trivial subgoals such as
   551 \texttt{True} and $t=t$.  It could use sophisticated means such as {\tt
   552   blast_tac}, though that could make simplification expensive.
   553 To keep things more abstract, solvers are packaged up in type
   554 \texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.
   555 
   556 Rewriting does not instantiate unknowns.  For example, rewriting
   557 cannot prove $a\in \Var{A}$ since this requires
   558 instantiating~$\Var{A}$.  The solver, however, is an arbitrary tactic
   559 and may instantiate unknowns as it pleases.  This is the only way the
   560 simplifier can handle a conditional rewrite rule whose condition
   561 contains extra variables.  When a simplification tactic is to be
   562 combined with other provers, especially with the classical reasoner,
   563 it is important whether it can be considered safe or not.  For this
   564 reason a simpset contains two solvers, a safe and an unsafe one.
   565 
   566 The standard simplification strategy solely uses the unsafe solver,
   567 which is appropriate in most cases.  For special applications where
   568 the simplification process is not allowed to instantiate unknowns
   569 within the goal, simplification starts with the safe solver, but may
   570 still apply the ordinary unsafe one in nested simplifications for
   571 conditional rules or congruences. Note that in this way the overall
   572 tactic is not totally safe:  it may instantiate unknowns that appear also 
   573 in other subgoals.
   574 
   575 \begin{ttdescription}
   576 \item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
   577   the string $s$ is only attached as a comment and has no other significance.
   578 
   579 \item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the
   580   \emph{safe} solver of $ss$.
   581   
   582 \item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an
   583   additional \emph{safe} solver; it will be tried after the solvers
   584   which had already been present in $ss$.
   585   
   586 \item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the
   587   unsafe solver of $ss$.
   588   
   589 \item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an
   590   additional unsafe solver; it will be tried after the solvers which
   591   had already been present in $ss$.
   592 
   593 \end{ttdescription}
   594 
   595 \medskip
   596 
   597 \index{assumptions!in simplification} The solver tactic is invoked
   598 with a list of theorems, namely assumptions that hold in the local
   599 context.  This may be non-empty only if the simplifier has been told
   600 to utilize local assumptions in the first place, e.g.\ if invoked via
   601 \texttt{asm_simp_tac}.  The solver is also presented the full goal
   602 including its assumptions in any case.  Thus it can use these (e.g.\ 
   603 by calling \texttt{assume_tac}), even if the list of premises is not
   604 passed.
   605 
   606 \medskip
   607 
   608 As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
   609 to solve the premises of congruence rules.  These are usually of the
   610 form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
   611 needs to be instantiated with the result.  Typically, the subgoaler
   612 will invoke the simplifier at some point, which will eventually call
   613 the solver.  For this reason, solver tactics must be prepared to solve
   614 goals of the form $t = \Var{x}$, usually by reflexivity.  In
   615 particular, reflexivity should be tried before any of the fancy
   616 tactics like \texttt{blast_tac}.
   617 
   618 It may even happen that due to simplification the subgoal is no longer
   619 an equality.  For example $False \bimp \Var{Q}$ could be rewritten to
   620 $\neg\Var{Q}$.  To cover this case, the solver could try resolving
   621 with the theorem $\neg False$.
   622 
   623 \medskip
   624 
   625 \begin{warn}
   626   If the simplifier aborts with the message \texttt{Failed congruence
   627     proof!}, then the subgoaler or solver has failed to prove a
   628   premise of a congruence rule.  This should never occur under normal
   629   circumstances; it indicates that some congruence rule, or possibly
   630   the subgoaler or solver, is faulty.
   631 \end{warn}
   632 
   633 
   634 \subsection{*The looper}\label{sec:simp-looper}
   635 \begin{ttbox}
   636 setloop   : simpset *           (int -> tactic)  -> simpset \hfill{\bf infix 4}
   637 addloop   : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
   638 delloop   : simpset *  string                    -> simpset \hfill{\bf infix 4}
   639 addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
   640 delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
   641 \end{ttbox}
   642 
   643 The looper is a list of tactics that are applied after simplification, in case
   644 the solver failed to solve the simplified goal.  If the looper
   645 succeeds, the simplification process is started all over again.  Each
   646 of the subgoals generated by the looper is attacked in turn, in
   647 reverse order.
   648 
   649 A typical looper is \index{case splitting}: the expansion of a conditional.
   650 Another possibility is to apply an elimination rule on the
   651 assumptions.  More adventurous loopers could start an induction.
   652 
   653 \begin{ttdescription}
   654   
   655 \item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
   656   tactic of $ss$.
   657   
   658 \item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
   659   looper tactic with name $name$; it will be tried after the looper tactics
   660   that had already been present in $ss$.
   661   
   662 \item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
   663   from $ss$.
   664   
   665 \item[$ss$ \ttindexbold{addsplits} $thms$] adds
   666   split tactics for $thms$ as additional looper tactics of $ss$.
   667 
   668 \item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
   669   split tactics for $thms$ from the looper tactics of $ss$.
   670 
   671 \end{ttdescription}
   672 
   673 The splitter replaces applications of a given function; the right-hand side
   674 of the replacement can be anything.  For example, here is a splitting rule
   675 for conditional expressions:
   676 \[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
   677 \conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) 
   678 \] 
   679 Another example is the elimination operator for Cartesian products (which
   680 happens to be called~$split$):  
   681 \[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
   682 \langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
   683 \] 
   684 
   685 For technical reasons, there is a distinction between case splitting in the 
   686 conclusion and in the premises of a subgoal. The former is done by
   687 \texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split}, 
   688 which do not split the subgoal, while the latter is done by 
   689 \texttt{split_asm_tac} with rules like \texttt{split_if_asm} or 
   690 \texttt{option.split_asm}, which split the subgoal.
   691 The operator \texttt{addsplits} automatically takes care of which tactic to
   692 call, analyzing the form of the rules given as argument.
   693 \begin{warn}
   694 Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
   695 \end{warn}
   696 
   697 Case splits should be allowed only when necessary; they are expensive
   698 and hard to control.  Here is an example of use, where \texttt{split_if}
   699 is the first rule above:
   700 \begin{ttbox}
   701 by (simp_tac (simpset() 
   702                  addloop ("split if", split_tac [split_if])) 1);
   703 \end{ttbox}
   704 Users would usually prefer the following shortcut using \texttt{addsplits}:
   705 \begin{ttbox}
   706 by (simp_tac (simpset() addsplits [split_if]) 1);
   707 \end{ttbox}
   708 Case-splitting on conditional expressions is usually beneficial, so it is
   709 enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.
   710 
   711 
   712 \section{The simplification tactics}\label{simp-tactics}
   713 \index{simplification!tactics}\index{tactics!simplification}
   714 \begin{ttbox}
   715 generic_simp_tac       : bool -> bool * bool * bool -> 
   716                          simpset -> int -> tactic
   717 simp_tac               : simpset -> int -> tactic
   718 asm_simp_tac           : simpset -> int -> tactic
   719 full_simp_tac          : simpset -> int -> tactic
   720 asm_full_simp_tac      : simpset -> int -> tactic
   721 safe_asm_full_simp_tac : simpset -> int -> tactic
   722 \end{ttbox}
   723 
   724 \texttt{generic_simp_tac} is the basic tactic that is underlying any actual
   725 simplification work. The others are just instantiations of it. The rewriting 
   726 strategy is always strictly bottom up, except for congruence rules, 
   727 which are applied while descending into a term.  Conditions in conditional 
   728 rewrite rules are solved recursively before the rewrite rule is applied.
   729 
   730 \begin{ttdescription}
   731   
   732 \item[\ttindexbold{generic_simp_tac} $safe$ ($simp\_asm$, $use\_asm$, $mutual$)] 
   733   gives direct access to the various simplification modes: 
   734   \begin{itemize}
   735   \item if $safe$ is {\tt true}, the safe solver is used as explained in
   736   {\S}\ref{sec:simp-solver},  
   737   \item $simp\_asm$ determines whether the local assumptions are simplified,
   738   \item $use\_asm$ determines whether the assumptions are used as local rewrite 
   739    rules, and
   740   \item $mutual$ determines whether assumptions can simplify each other rather
   741   than being processed from left to right. 
   742   \end{itemize}
   743   This generic interface is intended 
   744   for building special tools, e.g.\ for combining the simplifier with the 
   745   classical reasoner. It is rarely used directly.
   746   
   747 \item[\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
   748   \ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}] are
   749   the basic simplification tactics that work exactly like their
   750   namesakes in {\S}\ref{sec:simp-for-dummies}, except that they are
   751   explicitly supplied with a simpset.
   752   
   753 \end{ttdescription}
   754 
   755 \medskip
   756 
   757 Local modifications of simpsets within a proof are often much cleaner
   758 by using above tactics in conjunction with explicit simpsets, rather
   759 than their capitalized counterparts.  For example
   760 \begin{ttbox}
   761 Addsimps \(thms\);
   762 by (Simp_tac \(i\));
   763 Delsimps \(thms\);
   764 \end{ttbox}
   765 can be expressed more appropriately as
   766 \begin{ttbox}
   767 by (simp_tac (simpset() addsimps \(thms\)) \(i\));
   768 \end{ttbox}
   769 
   770 \medskip
   771 
   772 Also note that functions depending implicitly on the current theory
   773 context (like capital \texttt{Simp_tac} and the other commands of
   774 {\S}\ref{sec:simp-for-dummies}) should be considered harmful outside of
   775 actual proof scripts.  In particular, ML programs like theory
   776 definition packages or special tactics should refer to simpsets only
   777 explicitly, via the above tactics used in conjunction with
   778 \texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
   779 
   780 
   781 \section{Forward rules and conversions}
   782 \index{simplification!forward rules}\index{simplification!conversions}
   783 \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}
   784 simplify          : simpset -> thm -> thm
   785 asm_simplify      : simpset -> thm -> thm
   786 full_simplify     : simpset -> thm -> thm
   787 asm_full_simplify : simpset -> thm -> thm\medskip
   788 Simplifier.rewrite           : simpset -> cterm -> thm
   789 Simplifier.asm_rewrite       : simpset -> cterm -> thm
   790 Simplifier.full_rewrite      : simpset -> cterm -> thm
   791 Simplifier.asm_full_rewrite  : simpset -> cterm -> thm
   792 \end{ttbox}
   793 
   794 The first four of these functions provide \emph{forward} rules for
   795 simplification.  Their effect is analogous to the corresponding
   796 tactics described in {\S}\ref{simp-tactics}, but affect the whole
   797 theorem instead of just a certain subgoal.  Also note that the
   798 looper~/ solver process as described in {\S}\ref{sec:simp-looper} and
   799 {\S}\ref{sec:simp-solver} is omitted in forward simplification.
   800 
   801 The latter four are \emph{conversions}, establishing proven equations
   802 of the form $t \equiv u$ where the l.h.s.\ $t$ has been given as
   803 argument.
   804 
   805 \begin{warn}
   806   Forward simplification rules and conversions should be used rarely
   807   in ordinary proof scripts.  The main intention is to provide an
   808   internal interface to the simplifier for special utilities.
   809 \end{warn}
   810 
   811 
   812 \section{Examples of using the Simplifier}
   813 \index{examples!of simplification} Assume we are working within {\tt
   814   FOL} (see the file \texttt{FOL/ex/Nat}) and that
   815 \begin{ttdescription}
   816 \item[Nat.thy] 
   817   is a theory including the constants $0$, $Suc$ and $+$,
   818 \item[add_0]
   819   is the rewrite rule $0+\Var{n} = \Var{n}$,
   820 \item[add_Suc]
   821   is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$,
   822 \item[induct]
   823   is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp
   824     \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
   825 \end{ttdescription}
   826 We augment the implicit simpset inherited from \texttt{Nat} with the
   827 basic rewrite rules for addition of natural numbers:
   828 \begin{ttbox}
   829 Addsimps [add_0, add_Suc];
   830 \end{ttbox}
   831 
   832 \subsection{A trivial example}
   833 Proofs by induction typically involve simplification.  Here is a proof
   834 that~0 is a right identity:
   835 \begin{ttbox}
   836 Goal "m+0 = m";
   837 {\out Level 0}
   838 {\out m + 0 = m}
   839 {\out  1. m + 0 = m}
   840 \end{ttbox}
   841 The first step is to perform induction on the variable~$m$.  This returns a
   842 base case and inductive step as two subgoals:
   843 \begin{ttbox}
   844 by (res_inst_tac [("n","m")] induct 1);
   845 {\out Level 1}
   846 {\out m + 0 = m}
   847 {\out  1. 0 + 0 = 0}
   848 {\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
   849 \end{ttbox}
   850 Simplification solves the first subgoal trivially:
   851 \begin{ttbox}
   852 by (Simp_tac 1);
   853 {\out Level 2}
   854 {\out m + 0 = m}
   855 {\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
   856 \end{ttbox}
   857 The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the
   858 induction hypothesis as a rewrite rule:
   859 \begin{ttbox}
   860 by (Asm_simp_tac 1);
   861 {\out Level 3}
   862 {\out m + 0 = m}
   863 {\out No subgoals!}
   864 \end{ttbox}
   865 
   866 \subsection{An example of tracing}
   867 \index{tracing!of simplification|(}\index{*trace_simp}
   868 
   869 Let us prove a similar result involving more complex terms.  We prove
   870 that addition is commutative.
   871 \begin{ttbox}
   872 Goal "m+Suc(n) = Suc(m+n)";
   873 {\out Level 0}
   874 {\out m + Suc(n) = Suc(m + n)}
   875 {\out  1. m + Suc(n) = Suc(m + n)}
   876 \end{ttbox}
   877 Performing induction on~$m$ yields two subgoals:
   878 \begin{ttbox}
   879 by (res_inst_tac [("n","m")] induct 1);
   880 {\out Level 1}
   881 {\out m + Suc(n) = Suc(m + n)}
   882 {\out  1. 0 + Suc(n) = Suc(0 + n)}
   883 {\out  2. !!x. x + Suc(n) = Suc(x + n) ==>}
   884 {\out          Suc(x) + Suc(n) = Suc(Suc(x) + n)}
   885 \end{ttbox}
   886 Simplification solves the first subgoal, this time rewriting two
   887 occurrences of~0:
   888 \begin{ttbox}
   889 by (Simp_tac 1);
   890 {\out Level 2}
   891 {\out m + Suc(n) = Suc(m + n)}
   892 {\out  1. !!x. x + Suc(n) = Suc(x + n) ==>}
   893 {\out          Suc(x) + Suc(n) = Suc(Suc(x) + n)}
   894 \end{ttbox}
   895 Switching tracing on illustrates how the simplifier solves the remaining
   896 subgoal: 
   897 \begin{ttbox}
   898 set trace_simp;
   899 by (Asm_simp_tac 1);
   900 \ttbreak
   901 {\out Adding rewrite rule:}
   902 {\out .x + Suc n == Suc (.x + n)}
   903 \ttbreak
   904 {\out Applying instance of rewrite rule:}
   905 {\out ?m + Suc ?n == Suc (?m + ?n)}
   906 {\out Rewriting:}
   907 {\out Suc .x + Suc n == Suc (Suc .x + n)}
   908 \ttbreak
   909 {\out Applying instance of rewrite rule:}
   910 {\out Suc ?m + ?n == Suc (?m + ?n)}
   911 {\out Rewriting:}
   912 {\out Suc .x + n == Suc (.x + n)}
   913 \ttbreak
   914 {\out Applying instance of rewrite rule:}
   915 {\out Suc ?m + ?n == Suc (?m + ?n)}
   916 {\out Rewriting:}
   917 {\out Suc .x + n == Suc (.x + n)}
   918 \ttbreak
   919 {\out Applying instance of rewrite rule:}
   920 {\out ?x = ?x == True}
   921 {\out Rewriting:}
   922 {\out Suc (Suc (.x + n)) = Suc (Suc (.x + n)) == True}
   923 \ttbreak
   924 {\out Level 3}
   925 {\out m + Suc(n) = Suc(m + n)}
   926 {\out No subgoals!}
   927 \end{ttbox}
   928 Many variations are possible.  At Level~1 (in either example) we could have
   929 solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
   930 \begin{ttbox}
   931 by (ALLGOALS Asm_simp_tac);
   932 {\out Level 2}
   933 {\out m + Suc(n) = Suc(m + n)}
   934 {\out No subgoals!}
   935 \end{ttbox}
   936 \index{tracing!of simplification|)}
   937 
   938 
   939 \subsection{Free variables and simplification}
   940 
   941 Here is a conjecture to be proved for an arbitrary function~$f$
   942 satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$:
   943 \begin{ttbox}
   944 val [prem] = Goal
   945                "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
   946 {\out Level 0}
   947 {\out f(i + j) = i + f(j)}
   948 {\out  1. f(i + j) = i + f(j)}
   949 \ttbreak
   950 {\out val prem = "f(Suc(?n)) = Suc(f(?n))}
   951 {\out             [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
   952 \end{ttbox}
   953 In the theorem~\texttt{prem}, note that $f$ is a free variable while
   954 $\Var{n}$ is a schematic variable.
   955 \begin{ttbox}
   956 by (res_inst_tac [("n","i")] induct 1);
   957 {\out Level 1}
   958 {\out f(i + j) = i + f(j)}
   959 {\out  1. f(0 + j) = 0 + f(j)}
   960 {\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
   961 \end{ttbox}
   962 We simplify each subgoal in turn.  The first one is trivial:
   963 \begin{ttbox}
   964 by (Simp_tac 1);
   965 {\out Level 2}
   966 {\out f(i + j) = i + f(j)}
   967 {\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
   968 \end{ttbox}
   969 The remaining subgoal requires rewriting by the premise, so we add it
   970 to the current simpset:
   971 \begin{ttbox}
   972 by (asm_simp_tac (simpset() addsimps [prem]) 1);
   973 {\out Level 3}
   974 {\out f(i + j) = i + f(j)}
   975 {\out No subgoals!}
   976 \end{ttbox}
   977 
   978 \subsection{Reordering assumptions}
   979 \label{sec:reordering-asms}
   980 \index{assumptions!reordering}
   981 
   982 As mentioned in {\S}\ref{sec:simp-for-dummies-tacs},
   983 \ttindex{asm_full_simp_tac} may require the assumptions to be permuted
   984 to be more effective.  Given the subgoal
   985 \begin{ttbox}
   986 {\out 1. [| ALL x. P x --> f x = g x; Q(f a); P a; R |] ==> S}
   987 \end{ttbox}
   988 we can rotate the assumptions two positions to the right
   989 \begin{ttbox}
   990 by (rotate_tac ~2 1);
   991 \end{ttbox}
   992 to obtain
   993 \begin{ttbox}
   994 {\out 1. [| P a; R; ALL x. P x --> f x = g x; Q(f a) |] ==> S}
   995 \end{ttbox}
   996 which enables \verb$asm_full_simp_tac$ to simplify \verb$Q(f a)$ to
   997 \verb$Q(g a)$ because now all required assumptions are to the left of
   998 \verb$Q(f a)$.
   999 
  1000 Since rotation alone cannot produce arbitrary permutations, you can also pick
  1001 out a particular assumption which needs to be rewritten and move it the the
  1002 right end of the assumptions.  In the above case rotation can be replaced by
  1003 \begin{ttbox}
  1004 by (dres_inst_tac [("psi","Q(f a)")] asm_rl 1);
  1005 \end{ttbox}
  1006 which is more directed and leads to
  1007 \begin{ttbox}
  1008 {\out 1. [| ALL x. P x --> f x = g x; P a; R; Q(f a) |] ==> S}
  1009 \end{ttbox}
  1010 
  1011 \begin{warn}
  1012   Reordering assumptions usually leads to brittle proofs and should be
  1013   avoided.  Future versions of \verb$asm_full_simp_tac$ will completely
  1014   remove the need for such manipulations.
  1015 \end{warn}
  1016 
  1017 
  1018 \section{Permutative rewrite rules}
  1019 \index{rewrite rules!permutative|(}
  1020 
  1021 A rewrite rule is {\bf permutative} if the left-hand side and right-hand
  1022 side are the same up to renaming of variables.  The most common permutative
  1023 rule is commutativity: $x+y = y+x$.  Other examples include $(x-y)-z =
  1024 (x-z)-y$ in arithmetic and $insert(x,insert(y,A)) = insert(y,insert(x,A))$
  1025 for sets.  Such rules are common enough to merit special attention.
  1026 
  1027 Because ordinary rewriting loops given such rules, the simplifier
  1028 employs a special strategy, called {\bf ordered
  1029   rewriting}\index{rewriting!ordered}.  There is a standard
  1030 lexicographic ordering on terms.  This should be perfectly OK in most
  1031 cases, but can be changed for special applications.
  1032 
  1033 \begin{ttbox}
  1034 settermless : simpset * (term * term -> bool) -> simpset \hfill{\bf infix 4}
  1035 \end{ttbox}
  1036 \begin{ttdescription}
  1037   
  1038 \item[$ss$ \ttindexbold{settermless} $rel$] installs relation $rel$ as
  1039   term order in simpset $ss$.
  1040 
  1041 \end{ttdescription}
  1042 
  1043 \medskip
  1044 
  1045 A permutative rewrite rule is applied only if it decreases the given
  1046 term with respect to this ordering.  For example, commutativity
  1047 rewrites~$b+a$ to $a+b$, but then stops because $a+b$ is strictly less
  1048 than $b+a$.  The Boyer-Moore theorem prover~\cite{bm88book} also
  1049 employs ordered rewriting.
  1050 
  1051 Permutative rewrite rules are added to simpsets just like other
  1052 rewrite rules; the simplifier recognizes their special status
  1053 automatically.  They are most effective in the case of
  1054 associative-commutative operators.  (Associativity by itself is not
  1055 permutative.)  When dealing with an AC-operator~$f$, keep the
  1056 following points in mind:
  1057 \begin{itemize}\index{associative-commutative operators}
  1058   
  1059 \item The associative law must always be oriented from left to right,
  1060   namely $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if
  1061   used with commutativity, leads to looping in conjunction with the
  1062   standard term order.
  1063 
  1064 \item To complete your set of rewrite rules, you must add not just
  1065   associativity~(A) and commutativity~(C) but also a derived rule, {\bf
  1066     left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
  1067 \end{itemize}
  1068 Ordered rewriting with the combination of A, C, and~LC sorts a term
  1069 lexicographically:
  1070 \[\def\maps#1{\stackrel{#1}{\longmapsto}}
  1071  (b+c)+a \maps{A} b+(c+a) \maps{C} b+(a+c) \maps{LC} a+(b+c) \]
  1072 Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
  1073 examples; other algebraic structures are amenable to ordered rewriting,
  1074 such as boolean rings.
  1075 
  1076 \subsection{Example: sums of natural numbers}
  1077 
  1078 This example is again set in HOL (see \texttt{HOL/ex/NatSum}).  Theory
  1079 \thydx{Arith} contains natural numbers arithmetic.  Its associated simpset
  1080 contains many arithmetic laws including distributivity of~$\times$ over~$+$,
  1081 while \texttt{add_ac} is a list consisting of the A, C and LC laws for~$+$ on
  1082 type \texttt{nat}.  Let us prove the theorem
  1083 \[ \sum@{i=1}^n i = n\times(n+1)/2. \]
  1084 %
  1085 A functional~\texttt{sum} represents the summation operator under the
  1086 interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We
  1087 extend \texttt{Arith} as follows:
  1088 \begin{ttbox}
  1089 NatSum = Arith +
  1090 consts sum     :: [nat=>nat, nat] => nat
  1091 primrec 
  1092   "sum f 0 = 0"
  1093   "sum f (Suc n) = f(n) + sum f n"
  1094 end
  1095 \end{ttbox}
  1096 The \texttt{primrec} declaration automatically adds rewrite rules for
  1097 \texttt{sum} to the default simpset.  We now remove the
  1098 \texttt{nat_cancel} simplification procedures (in order not to spoil
  1099 the example) and insert the AC-rules for~$+$:
  1100 \begin{ttbox}
  1101 Delsimprocs nat_cancel;
  1102 Addsimps add_ac;
  1103 \end{ttbox}
  1104 Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
  1105 n\times(n+1)/2$.  The Isabelle goal has both sides multiplied by~$2$:
  1106 \begin{ttbox}
  1107 Goal "2 * sum (\%i.i) (Suc n) = n * Suc n";
  1108 {\out Level 0}
  1109 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1110 {\out  1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1111 \end{ttbox}
  1112 Induction should not be applied until the goal is in the simplest
  1113 form:
  1114 \begin{ttbox}
  1115 by (Simp_tac 1);
  1116 {\out Level 1}
  1117 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1118 {\out  1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
  1119 \end{ttbox}
  1120 Ordered rewriting has sorted the terms in the left-hand side.  The
  1121 subgoal is now ready for induction:
  1122 \begin{ttbox}
  1123 by (induct_tac "n" 1);
  1124 {\out Level 2}
  1125 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1126 {\out  1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
  1127 \ttbreak
  1128 {\out  2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
  1129 {\out           ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i.\,i) (Suc n)) =}
  1130 {\out               Suc n * Suc n}
  1131 \end{ttbox}
  1132 Simplification proves both subgoals immediately:\index{*ALLGOALS}
  1133 \begin{ttbox}
  1134 by (ALLGOALS Asm_simp_tac);
  1135 {\out Level 3}
  1136 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1137 {\out No subgoals!}
  1138 \end{ttbox}
  1139 Simplification cannot prove the induction step if we omit \texttt{add_ac} from
  1140 the simpset.  Observe that like terms have not been collected:
  1141 \begin{ttbox}
  1142 {\out Level 3}
  1143 {\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
  1144 {\out  1. !!n. n + sum (\%i. i) n + (n + sum (\%i. i) n) = n + n * n}
  1145 {\out           ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i.\,i) n)) =}
  1146 {\out               n + (n + (n + n * n))}
  1147 \end{ttbox}
  1148 Ordered rewriting proves this by sorting the left-hand side.  Proving
  1149 arithmetic theorems without ordered rewriting requires explicit use of
  1150 commutativity.  This is tedious; try it and see!
  1151 
  1152 Ordered rewriting is equally successful in proving
  1153 $\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
  1154 
  1155 
  1156 \subsection{Re-orienting equalities}
  1157 Ordered rewriting with the derived rule \texttt{symmetry} can reverse
  1158 equations:
  1159 \begin{ttbox}
  1160 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
  1161                  (fn _ => [Blast_tac 1]);
  1162 \end{ttbox}
  1163 This is frequently useful.  Assumptions of the form $s=t$, where $t$ occurs
  1164 in the conclusion but not~$s$, can often be brought into the right form.
  1165 For example, ordered rewriting with \texttt{symmetry} can prove the goal
  1166 \[ f(a)=b \conj f(a)=c \imp b=c. \]
  1167 Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
  1168 because $f(a)$ is lexicographically greater than $b$ and~$c$.  These
  1169 re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
  1170 conclusion by~$f(a)$. 
  1171 
  1172 Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
  1173 The differing orientations make this appear difficult to prove.  Ordered
  1174 rewriting with \texttt{symmetry} makes the equalities agree.  (Without
  1175 knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
  1176 or~$u=t$.)  Then the simplifier can prove the goal outright.
  1177 
  1178 \index{rewrite rules!permutative|)}
  1179 
  1180 
  1181 \section{*Coding simplification procedures}
  1182 \begin{ttbox}
  1183 mk_simproc: string -> cterm list ->
  1184               (Sign.sg -> thm list -> term -> thm option) -> simproc
  1185 \end{ttbox}
  1186 
  1187 \begin{ttdescription}
  1188 \item[\ttindexbold{mk_simproc}~$name$~$lhss$~$proc$] makes $proc$ a
  1189   simplification procedure for left-hand side patterns $lhss$.  The
  1190   name just serves as a comment.  The function $proc$ may be invoked
  1191   by the simplifier for redex positions matched by one of $lhss$ as
  1192   described below.
  1193 \end{ttdescription}
  1194 
  1195 Simplification procedures are applied in a two-stage process as
  1196 follows: The simplifier tries to match the current redex position
  1197 against any one of the $lhs$ patterns of any simplification procedure.
  1198 If this succeeds, it invokes the corresponding {\ML} function, passing
  1199 with the current signature, local assumptions and the (potential)
  1200 redex.  The result may be either \texttt{None} (indicating failure) or
  1201 \texttt{Some~$thm$}.
  1202 
  1203 Any successful result is supposed to be a (possibly conditional)
  1204 rewrite rule $t \equiv u$ that is applicable to the current redex.
  1205 The rule will be applied just as any ordinary rewrite rule.  It is
  1206 expected to be already in \emph{internal form}, though, bypassing the
  1207 automatic preprocessing of object-level equivalences.
  1208 
  1209 \medskip
  1210 
  1211 As an example of how to write your own simplification procedures,
  1212 consider eta-expansion of pair abstraction (see also
  1213 \texttt{HOL/Modelcheck/MCSyn} where this is used to provide external
  1214 model checker syntax).
  1215   
  1216 The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator
  1217 \texttt{split} together with some concrete syntax supporting
  1218 $\lambda\,(x,y).b$ abstractions.  Assume that we would like to offer a tactic
  1219 that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type)
  1220 to $\lambda\,(x,y).f\,(x,y)$.  The corresponding rule is:
  1221 \begin{ttbox}
  1222 pair_eta_expand:  (f::'a*'b=>'c) = (\%(x, y). f (x, y))
  1223 \end{ttbox}
  1224 Unfortunately, term rewriting using this rule directly would not
  1225 terminate!  We now use the simplification procedure mechanism in order
  1226 to stop the simplifier from applying this rule over and over again,
  1227 making it rewrite only actual abstractions.  The simplification
  1228 procedure \texttt{pair_eta_expand_proc} is defined as follows:
  1229 \begin{ttbox}
  1230 local
  1231   val lhss =
  1232     [read_cterm (sign_of Prod.thy) 
  1233                 ("f::'a*'b=>'c", TVar (("'z", 0), []))];
  1234   val rew = mk_meta_eq pair_eta_expand; \medskip
  1235   fun proc _ _ (Abs _) = Some rew
  1236     | proc _ _ _ = None;
  1237 in
  1238   val pair_eta_expand_proc = mk_simproc "pair_eta_expand" lhss proc;
  1239 end;
  1240 \end{ttbox}
  1241 This is an example of using \texttt{pair_eta_expand_proc}:
  1242 \begin{ttbox}
  1243 {\out 1. P (\%p::'a * 'a. fst p + snd p + z)}
  1244 by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1);
  1245 {\out 1. P (\%(x::'a,y::'a). x + y + z)}
  1246 \end{ttbox}
  1247 
  1248 \medskip
  1249 
  1250 In the above example the simplification procedure just did fine
  1251 grained control over rule application, beyond higher-order pattern
  1252 matching.  Usually, procedures would do some more work, in particular
  1253 prove particular theorems depending on the current redex.
  1254 
  1255 
  1256 \section{*Setting up the Simplifier}\label{sec:setting-up-simp}
  1257 \index{simplification!setting up}
  1258 
  1259 Setting up the simplifier for new logics is complicated in the general case.
  1260 This section describes how the simplifier is installed for intuitionistic
  1261 first-order logic; the code is largely taken from {\tt FOL/simpdata.ML} of the
  1262 Isabelle sources.
  1263 
  1264 The simplifier and the case splitting tactic, which reside on separate files,
  1265 are not part of Pure Isabelle.  They must be loaded explicitly by the
  1266 object-logic as follows (below \texttt{\~\relax\~\relax} refers to
  1267 \texttt{\$ISABELLE_HOME}):
  1268 \begin{ttbox}
  1269 use "\~\relax\~\relax/src/Provers/simplifier.ML";
  1270 use "\~\relax\~\relax/src/Provers/splitter.ML";
  1271 \end{ttbox}
  1272 
  1273 Simplification requires converting object-equalities to meta-level rewrite
  1274 rules.  This demands rules stating that equal terms and equivalent formulae
  1275 are also equal at the meta-level.  The rule declaration part of the file
  1276 \texttt{FOL/IFOL.thy} contains the two lines
  1277 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
  1278 eq_reflection   "(x=y)   ==> (x==y)"
  1279 iff_reflection  "(P<->Q) ==> (P==Q)"
  1280 \end{ttbox}
  1281 Of course, you should only assert such rules if they are true for your
  1282 particular logic.  In Constructive Type Theory, equality is a ternary
  1283 relation of the form $a=b\in A$; the type~$A$ determines the meaning
  1284 of the equality essentially as a partial equivalence relation.  The
  1285 present simplifier cannot be used.  Rewriting in \texttt{CTT} uses
  1286 another simplifier, which resides in the file {\tt
  1287   Provers/typedsimp.ML} and is not documented.  Even this does not
  1288 work for later variants of Constructive Type Theory that use
  1289 intensional equality~\cite{nordstrom90}.
  1290 
  1291 
  1292 \subsection{A collection of standard rewrite rules}
  1293 
  1294 We first prove lots of standard rewrite rules about the logical
  1295 connectives.  These include cancellation and associative laws.  We
  1296 define a function that echoes the desired law and then supplies it the
  1297 prover for intuitionistic FOL:
  1298 \begin{ttbox}
  1299 fun int_prove_fun s = 
  1300  (writeln s;  
  1301   prove_goal IFOL.thy s
  1302    (fn prems => [ (cut_facts_tac prems 1), 
  1303                   (IntPr.fast_tac 1) ]));
  1304 \end{ttbox}
  1305 The following rewrite rules about conjunction are a selection of those
  1306 proved on \texttt{FOL/simpdata.ML}.  Later, these will be supplied to the
  1307 standard simpset.
  1308 \begin{ttbox}
  1309 val conj_simps = map int_prove_fun
  1310  ["P & True <-> P",      "True & P <-> P",
  1311   "P & False <-> False", "False & P <-> False",
  1312   "P & P <-> P",
  1313   "P & ~P <-> False",    "~P & P <-> False",
  1314   "(P & Q) & R <-> P & (Q & R)"];
  1315 \end{ttbox}
  1316 The file also proves some distributive laws.  As they can cause exponential
  1317 blowup, they will not be included in the standard simpset.  Instead they
  1318 are merely bound to an \ML{} identifier, for user reference.
  1319 \begin{ttbox}
  1320 val distrib_simps  = map int_prove_fun
  1321  ["P & (Q | R) <-> P&Q | P&R", 
  1322   "(Q | R) & P <-> Q&P | R&P",
  1323   "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
  1324 \end{ttbox}
  1325 
  1326 
  1327 \subsection{Functions for preprocessing the rewrite rules}
  1328 \label{sec:setmksimps}
  1329 \begin{ttbox}\indexbold{*setmksimps}
  1330 setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
  1331 \end{ttbox}
  1332 The next step is to define the function for preprocessing rewrite rules.
  1333 This will be installed by calling \texttt{setmksimps} below.  Preprocessing
  1334 occurs whenever rewrite rules are added, whether by user command or
  1335 automatically.  Preprocessing involves extracting atomic rewrites at the
  1336 object-level, then reflecting them to the meta-level.
  1337 
  1338 To start, the function \texttt{gen_all} strips any meta-level
  1339 quantifiers from the front of the given theorem.
  1340 
  1341 The function \texttt{atomize} analyses a theorem in order to extract
  1342 atomic rewrite rules.  The head of all the patterns, matched by the
  1343 wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
  1344 \begin{ttbox}
  1345 fun atomize th = case concl_of th of 
  1346     _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) \at
  1347                                        atomize(th RS conjunct2)
  1348   | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
  1349   | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
  1350   | _ $ (Const("True",_))           => []
  1351   | _ $ (Const("False",_))          => []
  1352   | _                               => [th];
  1353 \end{ttbox}
  1354 There are several cases, depending upon the form of the conclusion:
  1355 \begin{itemize}
  1356 \item Conjunction: extract rewrites from both conjuncts.
  1357 \item Implication: convert $P\imp Q$ to the meta-implication $P\Imp Q$ and
  1358   extract rewrites from~$Q$; these will be conditional rewrites with the
  1359   condition~$P$.
  1360 \item Universal quantification: remove the quantifier, replacing the bound
  1361   variable by a schematic variable, and extract rewrites from the body.
  1362 \item \texttt{True} and \texttt{False} contain no useful rewrites.
  1363 \item Anything else: return the theorem in a singleton list.
  1364 \end{itemize}
  1365 The resulting theorems are not literally atomic --- they could be
  1366 disjunctive, for example --- but are broken down as much as possible. 
  1367 See the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
  1368 set-theoretic formulae into rewrite rules. 
  1369 
  1370 For standard situations like the above,
  1371 there is a generic auxiliary function \ttindexbold{mk_atomize} that takes a 
  1372 list of pairs $(name, thms)$, where $name$ is an operator name and
  1373 $thms$ is a list of theorems to resolve with in case the pattern matches, 
  1374 and returns a suitable \texttt{atomize} function.
  1375 
  1376 
  1377 The simplified rewrites must now be converted into meta-equalities.  The
  1378 rule \texttt{eq_reflection} converts equality rewrites, while {\tt
  1379   iff_reflection} converts if-and-only-if rewrites.  The latter possibility
  1380 can arise in two other ways: the negative theorem~$\neg P$ is converted to
  1381 $P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
  1382 $P\equiv\texttt{True}$.  The rules \texttt{iff_reflection_F} and {\tt
  1383   iff_reflection_T} accomplish this conversion.
  1384 \begin{ttbox}
  1385 val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
  1386 val iff_reflection_F = P_iff_F RS iff_reflection;
  1387 \ttbreak
  1388 val P_iff_T = int_prove_fun "P ==> (P <-> True)";
  1389 val iff_reflection_T = P_iff_T RS iff_reflection;
  1390 \end{ttbox}
  1391 The function \texttt{mk_eq} converts a theorem to a meta-equality
  1392 using the case analysis described above.
  1393 \begin{ttbox}
  1394 fun mk_eq th = case concl_of th of
  1395     _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
  1396   | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
  1397   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
  1398   | _                           => th RS iff_reflection_T;
  1399 \end{ttbox}
  1400 The 
  1401 three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq} 
  1402 will be composed together and supplied below to \texttt{setmksimps}.
  1403 
  1404 
  1405 \subsection{Making the initial simpset}
  1406 
  1407 It is time to assemble these items.  The list \texttt{IFOL_simps} contains the
  1408 default rewrite rules for intuitionistic first-order logic.  The first of
  1409 these is the reflexive law expressed as the equivalence
  1410 $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is clearly useless.
  1411 \begin{ttbox}
  1412 val IFOL_simps =
  1413    [refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at 
  1414     imp_simps \at iff_simps \at quant_simps;
  1415 \end{ttbox}
  1416 The list \texttt{triv_rls} contains trivial theorems for the solver.  Any
  1417 subgoal that is simplified to one of these will be removed.
  1418 \begin{ttbox}
  1419 val notFalseI = int_prove_fun "~False";
  1420 val triv_rls = [TrueI,refl,iff_refl,notFalseI];
  1421 \end{ttbox}
  1422 We also define the function \ttindex{mk_meta_cong} to convert the conclusion
  1423 of congruence rules into meta-equalities.
  1424 \begin{ttbox}
  1425 fun mk_meta_cong rl = standard (mk_meta_eq (mk_meta_prems rl));
  1426 \end{ttbox}
  1427 %
  1428 The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}.  It
  1429 preprocess rewrites using 
  1430 {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
  1431 It solves simplified subgoals using \texttt{triv_rls} and assumptions, and by
  1432 detecting contradictions.  It uses \ttindex{asm_simp_tac} to tackle subgoals
  1433 of conditional rewrites.
  1434 
  1435 Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
  1436 In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
  1437   IFOL_simps} as rewrite rules.  \ttindexbold{FOL_ss} will later
  1438 extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
  1439 P\bimp P$.
  1440 \index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
  1441 \index{*addsimps}\index{*addcongs}
  1442 \begin{ttbox}
  1443 fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls {\at} prems),
  1444                                  atac, etac FalseE];
  1445 
  1446 fun safe_solver prems = FIRST'[match_tac (triv_rls {\at} prems),
  1447                                eq_assume_tac, ematch_tac [FalseE]];
  1448 
  1449 val FOL_basic_ss =
  1450       empty_ss setsubgoaler asm_simp_tac
  1451                addsimprocs [defALL_regroup, defEX_regroup]
  1452                setSSolver   safe_solver
  1453                setSolver  unsafe_solver
  1454                setmksimps (map mk_eq o atomize o gen_all)
  1455                setmkcong mk_meta_cong;
  1456 
  1457 val IFOL_ss = 
  1458       FOL_basic_ss addsimps (IFOL_simps {\at} 
  1459                              int_ex_simps {\at} int_all_simps)
  1460                    addcongs [imp_cong];
  1461 \end{ttbox}
  1462 This simpset takes \texttt{imp_cong} as a congruence rule in order to use
  1463 contextual information to simplify the conclusions of implications:
  1464 \[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
  1465    (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
  1466 \]
  1467 By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
  1468 effect for conjunctions.
  1469 
  1470 
  1471 \subsection{Splitter setup}\index{simplification!setting up the splitter}
  1472 
  1473 To set up case splitting, we have to call the \ML{} functor \ttindex{
  1474 SplitterFun}, which takes the argument signature \texttt{SPLITTER_DATA}. 
  1475 So we prove the theorem \texttt{meta_eq_to_iff} below and store it, together
  1476 with the \texttt{mk_eq} function described above and several standard
  1477 theorems, in the structure \texttt{SplitterData}. Calling the functor with
  1478 this data yields a new instantiation of the splitter for our logic.
  1479 \begin{ttbox}
  1480 val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
  1481   (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
  1482 \ttbreak
  1483 structure SplitterData =
  1484   struct
  1485   structure Simplifier = Simplifier
  1486   val mk_eq          = mk_eq
  1487   val meta_eq_to_iff = meta_eq_to_iff
  1488   val iffD           = iffD2
  1489   val disjE          = disjE
  1490   val conjE          = conjE
  1491   val exE            = exE
  1492   val contrapos      = contrapos
  1493   val contrapos2     = contrapos2
  1494   val notnotD        = notnotD
  1495   end;
  1496 \ttbreak
  1497 structure Splitter = SplitterFun(SplitterData);
  1498 \end{ttbox}
  1499 
  1500 
  1501 \subsection{Theory setup}\index{simplification!setting up the theory}
  1502 \begin{ttbox}\indexbold{*Simplifier.setup}\index{*setup!simplifier}
  1503 Simplifier.setup: (theory -> theory) list
  1504 \end{ttbox}
  1505 
  1506 Advanced theory related features of the simplifier (e.g.\ implicit
  1507 simpset support) have to be set up explicitly.  The simplifier already
  1508 provides a suitable setup function definition.  This has to be
  1509 installed into the base theory of any new object-logic via a
  1510 \texttt{setup} declaration.
  1511 
  1512 For example, this is done in \texttt{FOL/IFOL.thy} as follows:
  1513 \begin{ttbox}
  1514 setup Simplifier.setup
  1515 \end{ttbox}
  1516 
  1517 
  1518 \index{simplification|)}
  1519 
  1520 
  1521 %%% Local Variables: 
  1522 %%% mode: latex
  1523 %%% TeX-master: "ref"
  1524 %%% End: