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