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:
`