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