doc-src/Ref/simplifier.tex
author paulson
Thu, 20 Nov 1997 11:54:31 +0100
changeset 4245 b9ce25073cc0
parent 3950 e9d5bcae8351
child 4317 7264fa2ff2ec
permissions -rw-r--r--
Updated the NatSum example
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
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
This chapter describes Isabelle's generic simplification package, which
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
     7
provides a suite of simplification tactics.  It performs conditional and
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
     8
unconditional rewriting and uses contextual information (`local
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
     9
assumptions').  It provides a few general hooks, which can provide
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
    10
automatic case splits during rewriting, for example.  The simplifier is set
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    11
up for many of Isabelle's logics: \FOL, \ZF, \HOL\ and \HOLCF.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    12
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    13
The next section is a quick introduction to the simplifier, the later
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    14
sections explain advanced features.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    15
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    16
\section{Simplification for dummies}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    17
\label{sec:simp-for-dummies}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    18
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    19
In some logics (\FOL, {\HOL} and \ZF), the simplifier is particularly easy to
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    20
use because it supports the concept of a {\em current
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    21
  simpset}\index{simpset!current}.  This is a default set of simplification
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    22
rules.  All commands are interpreted relative to the current simpset.  For
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    23
example, in the theory of arithmetic the goal
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    24
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    25
{\out  1. 0 + (x + 0) = x + 0 + 0}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    26
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    27
can be solved by a single
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    28
\begin{ttbox}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    29
by (Simp_tac 1);
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    30
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    31
The simplifier uses the current simpset, which in the case of arithmetic
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    32
contains the required theorems $\Var{n}+0 = \Var{n}$ and $0+\Var{n} =
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    33
\Var{n}$.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    34
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    35
If assumptions of the subgoal are also needed in the simplification
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    36
process, as in
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    37
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    38
{\out  1. x = 0 ==> x + x = 0}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    39
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    40
then there is the more powerful
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    41
\begin{ttbox}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
    42
by (Asm_simp_tac 1);
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    43
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    44
which solves the above goal.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    45
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    46
There are four basic simplification tactics:
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    47
\begin{ttdescription}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    48
\item[\ttindexbold{Simp_tac} $i$] simplifies subgoal~$i$ using the current
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    49
  simpset.  It may solve the subgoal completely if it has become trivial,
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    50
  using the solver.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    51
  
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    52
\item[\ttindexbold{Asm_simp_tac}]\index{assumptions!in simplification}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    53
  is like \verb$Simp_tac$, but extracts additional rewrite rules from the
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    54
  assumptions.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    55
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    56
\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    57
  simplifies the assumptions (but without using the assumptions to simplify
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    58
  each other or the actual goal.)
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    59
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    60
\item[\ttindexbold{Asm_full_simp_tac}]
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    61
  is like \verb$Asm_simp_tac$, but also simplifies the assumptions one by
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    62
  one.  {\em Working from left to right, it uses each assumption in the
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    63
  simplification of those following.}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    64
\end{ttdescription}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    65
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    66
{\tt Asm_full_simp_tac} is the most powerful of this quartet but may also
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    67
loop where some of the others terminate.  For example,
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    68
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    69
{\out  1. ALL x. f(x) = g(f(g(x))) ==> f(0) = f(0)+0}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    70
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    71
is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt Asm_simp_tac}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    72
loop because the rewrite rule $f(\Var{x}) = f(g(f(\Var{x})))$ extracted from
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    73
the assumption does not terminate.  Isabelle notices certain simple forms of
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    74
nontermination, but not this one.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    75
 
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    76
\begin{warn}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    77
  Since \verb$Asm_full_simp_tac$ works from left to right, it sometimes
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    78
misses opportunities for simplification: given the subgoal
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    79
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    80
{\out [| P(f(a)); f(a) = t |] ==> ...}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    81
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    82
\verb$Asm_full_simp_tac$ will not simplify the first assumption using the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    83
second but will leave the assumptions unchanged.  See
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    84
\S\ref{sec:reordering-asms} for ways around this problem.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    85
\end{warn}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    86
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
    87
Using the simplifier effectively may take a bit of experimentation.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
    88
\index{tracing!of simplification}\index{*trace_simp} The tactics can
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
    89
be traced by setting \verb$trace_simp := true$.
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    90
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    91
There is not just one global current simpset, but one associated with each
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    92
theory as well.  How are these simpset built up?
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    93
\begin{enumerate}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    94
\item When loading {\tt T.thy}, the current simpset is initialized with the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    95
  union of the simpsets associated with all the ancestors of {\tt T}.  In
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    96
  addition, certain constructs in {\tt T} may add new rules to the simpset,
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
    97
  e.g.\ \ttindex{datatype} and \ttindex{primrec} in \HOL.  Definitions are not
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    98
  added automatically!
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
    99
\item The script in {\tt T.ML} may manipulate the current simpset further by
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   100
  explicitly adding/deleting theorems to/from it (see below).
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   101
\item After {\tt T.ML} has been read, the current simpset is associated with
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   102
  theory {\tt T}.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   103
\end{enumerate}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   104
The current simpset is manipulated by
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   105
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   106
Addsimps, Delsimps: thm list -> unit
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   107
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   108
\begin{ttdescription}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   109
\item[\ttindexbold{Addsimps} $thms$] adds $thms$ to the current simpset
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   110
\item[\ttindexbold{Delsimps} $thms$] deletes $thms$ from the current simpset
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   111
\end{ttdescription}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   112
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   113
Generally useful simplification rules $\Var{n}+0 = \Var{n}$ should be added
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   114
to the current simpset right after they have been proved.  Those of a more
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   115
specific nature (e.g.\ the laws of de~Morgan, which alter the structure of a
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   116
formula) should only be added for specific proofs and deleted again
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   117
afterwards.  Conversely, it may also happen that a generally useful rule needs
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   118
to be removed for a certain proof and is added again afterwards.  Well
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   119
designed simpsets need few temporary additions or deletions.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   120
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   121
\begin{warn}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   122
  The union of the ancestor simpsets (as described above) is not always a good
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   123
  simpset for the new theory.  If some ancestors have deleted simplification
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   124
  rules because they are no longer wanted, while others have left those rules
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   125
  in, then the union will contain the unwanted rules.  If the ancestor
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   126
  simpsets differ in other components (the subgoaler, solver, looper or rule
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   127
  preprocessor: see below), then you cannot be sure which version of that
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   128
  component will be inherited.  You may have to set the component explicitly
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   129
  for the new theory's simpset by an assignment of the form
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   130
 {\tt simpset := \dots}.
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   131
\end{warn}
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   132
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   133
\begin{warn}
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   134
  If you execute proofs interactively, or load them from an ML file without
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   135
  associated {\tt .thy} file, you must set the current simpset by calling
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   136
  \ttindex{set_current_thy}~{\tt"}$T${\tt"}, where $T$ is the name of the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   137
  theory you want to work in.  If you have just loaded $T$, this is not
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   138
  necessary.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   139
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   142
\section{Simplification sets}\index{simplification sets} 
3134
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   143
The simplification tactics are controlled by {\bf simpsets}.  These
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   144
consist of several components, including rewrite rules, congruence
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   145
rules, the subgoaler, the solver and the looper.  The simplifier
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   146
should be set up with sensible defaults so that most simplifier calls
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   147
specify only rewrite rules.  Experienced users can exploit the other
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   148
components to streamline proofs.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   149
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   150
Logics like \HOL, which support a current
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   151
simpset\index{simpset!current}, store its value in an ML reference
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   152
variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   154
\subsection{Rewrite rules}
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   155
\index{rewrite rules|(}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   156
Rewrite rules are theorems expressing some form of equality:
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   157
\begin{eqnarray*}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   158
  Suc(\Var{m}) + \Var{n} &=&      \Var{m} + Suc(\Var{n}) \\
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   159
  \Var{P}\conj\Var{P}    &\bimp&  \Var{P} \\
714
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   160
  \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
   161
\end{eqnarray*}
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   162
Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   163
0$ are permitted; the conditions can be arbitrary formulas.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
Internally, all rewrite rules are translated into meta-equalities, theorems
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   166
with conclusion $lhs \equiv rhs$.  Each simpset contains a function for
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   167
extracting equalities from arbitrary theorems.  For example,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   168
$\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\} \equiv
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   169
False$.  This function can be installed using \ttindex{setmksimps} but only
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   170
the definer of a logic should need to do this; see \S\ref{sec:setmksimps}.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   171
The function processes theorems added by \ttindex{addsimps} as well as
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   172
local assumptions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   175
\begin{warn}
1101
b9594fe65d89 trivial rewording
lcp
parents: 714
diff changeset
   176
The simplifier will accept all standard rewrite rules: those
b9594fe65d89 trivial rewording
lcp
parents: 714
diff changeset
   177
where all unknowns are of base type.  Hence ${\Var{i}+(\Var{j}+\Var{k})} =
714
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   178
{(\Var{i}+\Var{j})+\Var{k}}$ is ok.
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   179
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   180
It will also deal gracefully with all rules whose left-hand sides are
3950
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   181
so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   182
\indexbold{higher-order pattern}\indexbold{pattern, higher-order}
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   183
These are terms in $\beta$-normal form (this will always be the case unless
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   184
you have done something strange) where each occurrence of an unknown is of
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   185
the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   186
variables. Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall
e9d5bcae8351 \label{simp-chap} -> chap:simplification
nipkow
parents: 3485
diff changeset
   187
x.\Var{P}(x)) \land (\forall x.\Var{Q}(x))$ is also ok, in both directions.
714
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   188
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   189
In some rare cases the rewriter will even deal with quite general rules: for
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   190
example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   191
range(g)$ to $True$, but will fail to match $g(h(b)) \in range(\lambda
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   192
x.g(h(x)))$.  However, you can replace the offending subterms (in our case
714
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   193
$\Var{f}(\Var{x})$, which is not a pattern) by adding new variables and
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   194
conditions: $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f})
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   195
= True$ is acceptable as a conditional rewrite rule since conditions can
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   196
be arbitrary terms.
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   197
015ec0a9563a Updated description of valid lhss.
nipkow
parents: 698
diff changeset
   198
There is no restriction on the form of the right-hand sides.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   201
\index{rewrite rules|)}
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   202
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   203
\subsection{*Congruence rules}\index{congruence rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
Congruence rules are meta-equalities of the form
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   205
\[ \dots \Imp
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
   f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\]
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   208
This governs the simplification of the arguments of~$f$.  For
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
example, some arguments can be simplified under additional assumptions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
\[ \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
   211
   \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
\]
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   213
Given this rule, the simplifier assumes $Q@1$ and extracts rewrite rules
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   214
from it when simplifying~$P@2$.  Such local assumptions are effective for
698
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   215
rewriting formulae such as $x=0\imp y+x=y$.  The local assumptions are also
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   216
provided as theorems to the solver; see page~\pageref{sec:simp-solver} below.
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   217
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   218
Here are some more examples.  The congruence rule for bounded quantifiers
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   219
also supplies contextual information, this time about the bound variable:
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   220
\begin{eqnarray*}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   221
  &&\List{\Var{A}=\Var{B};\; 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   222
          \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
   223
 &&\qquad\qquad
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   224
    (\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
   225
\end{eqnarray*}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   226
The congruence rule for conditional expressions can supply contextual
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   227
information for simplifying the arms:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
         \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
\]
698
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   232
A congruence rule can also {\em prevent\/} simplification of some arguments.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
Here is an alternative congruence rule for conditional expressions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
\[ \Var{p}=\Var{q} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
Only the first argument is simplified; the others remain unchanged.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
This can make simplification much faster, but may require an extra case split
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
to prove the goal.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   241
Congruence rules are added/deleted using 
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   242
\ttindexbold{addeqcongs}/\ttindex{deleqcongs}.  
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   243
Their conclusion must be a meta-equality, as in the examples above.  It is more
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
natural to derive the rules with object-logic equality, for example
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\[ \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
   246
   \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
\]
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   248
Each object-logic should define operators called \ttindex{addcongs} and 
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   249
\ttindex{delcongs} that expects object-equalities and translates them into 
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   250
meta-equalities.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   252
\subsection{*The subgoaler}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
The subgoaler is the tactic used to solve subgoals arising out of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
conditional rewrite rules or congruence rules.  The default should be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
simplification itself.  Occasionally this strategy needs to be changed.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
example, if the premise of a conditional rule is an instance of its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
default strategy could loop.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
The subgoaler can be set explicitly with \ttindex{setsubgoaler}.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
example, the subgoaler
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   263
fun subgoal_tac ss = assume_tac ORELSE'
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   264
                     resolve_tac (prems_of_ss ss) ORELSE' 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
                     asm_simp_tac ss;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   267
tries to solve the subgoal by assumption or with one of the premises, calling
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
simplification only if that fails; here {\tt prems_of_ss} extracts the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
current premises from a simpset.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
698
23734672dc12 updated discussion of congruence rules in first section
lcp
parents: 332
diff changeset
   271
\subsection{*The solver}\label{sec:simp-solver}
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   272
The solver is a pair of tactics that attempt to solve a subgoal after
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   273
simplification.  Typically it just proves trivial subgoals such as {\tt
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   274
  True} and $t=t$.  It could use sophisticated means such as {\tt
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   275
  blast_tac}, though that could make simplification expensive. 
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   276
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   277
Rewriting does not instantiate unknowns.  For example, rewriting
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   278
cannot prove $a\in \Var{A}$ since this requires
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   279
instantiating~$\Var{A}$.  The solver, however, is an arbitrary tactic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   280
and may instantiate unknowns as it pleases.  This is the only way the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   281
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
   282
contains extra variables.  When a simplification tactic is to be
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   283
combined with other provers, especially with the classical reasoner,
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   284
it is important whether it can be considered safe or not.  Therefore,
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   285
the solver is split into a safe and an unsafe part.  Both parts can be
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   286
set independently, using either \ttindex{setSSolver} with a safe
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   287
tactic as argument, or \ttindex{setSolver} with an unsafe tactic.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   288
Additional solvers, which are tried after the already set solvers, may
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   289
be added using \ttindex{addSSolver} and \ttindex{addSolver}.
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   290
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   291
The standard simplification strategy solely uses the unsafe solver,
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   292
which is appropriate in most cases.  But for special applications where
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   293
the simplification process is not allowed to instantiate unknowns
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   294
within the goal, the tactic \ttindexbold{safe_asm_full_simp_tac} is
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   295
provided.  It uses the \emph{safe} solver for the current subgoal, but
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   296
applies ordinary unsafe {\tt asm_full_simp_tac} for recursive internal
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   297
simplifications (for conditional rules or congruences).
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   298
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   299
\index{assumptions!in simplification}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   300
The tactic is presented with the full goal, including the asssumptions.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   301
Hence it can use those assumptions (say by calling {\tt assume_tac}) even
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   302
inside {\tt simp_tac}, which otherwise does not use assumptions.  The
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   303
solver is also supplied a list of theorems, namely assumptions that hold in
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   304
the local context.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   306
The subgoaler is also used to solve the premises of congruence rules, which
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   307
are usually of the form $s = \Var{x}$, where $s$ needs to be simplified and
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   308
$\Var{x}$ needs to be instantiated with the result.  Hence the subgoaler
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   309
should call the simplifier at some point.  The simplifier will then call the
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   310
solver, which must therefore be prepared to solve goals of the form $t =
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   311
\Var{x}$, usually by reflexivity.  In particular, reflexivity should be
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   312
tried before any of the fancy tactics like {\tt blast_tac}.  
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   313
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   314
It may even happen that due to simplification the subgoal is no longer
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   315
an equality.  For example $False \bimp \Var{Q}$ could be rewritten to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   316
$\neg\Var{Q}$.  To cover this case, the solver could try resolving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   317
with the theorem $\neg False$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
\begin{warn}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   320
  If the simplifier aborts with the message {\tt Failed congruence
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   321
    proof!}, then the subgoaler or solver has failed to prove a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   322
  premise of a congruence rule.  This should never occur under normal
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   323
  circumstances; it indicates that some congruence rule, or possibly
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   324
  the subgoaler or solver, is faulty.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   327
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   328
\subsection{*The looper}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
The looper is a tactic that is applied after simplification, in case the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
solver failed to solve the simplified goal.  If the looper succeeds, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
simplification process is started all over again.  Each of the subgoals
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
generated by the looper is attacked in turn, in reverse order.  A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
typical looper is case splitting: the expansion of a conditional.  Another
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
possibility is to apply an elimination rule on the assumptions.  More
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
adventurous loopers could start an induction.  The looper is set with 
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   336
\ttindex{setloop}.  Additional loopers, which are tried after the already set
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   337
looper, may be added with \ttindex{addloop}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\begin{figure}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   341
\index{*simpset ML type}
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   342
\index{*empty_ss}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   343
\index{*rep_ss}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   344
\index{*prems_of_ss}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   345
\index{*setloop}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   346
\index{*addloop}
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   347
\index{*setSSolver}
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   348
\index{*addSSolver}
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   349
\index{*setSolver}
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   350
\index{*addSolver}
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   351
\index{*setsubgoaler}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   352
\index{*setmksimps}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   353
\index{*addsimps}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   354
\index{*delsimps}
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   355
\index{*addeqcongs}
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   356
\index{*deleqcongs}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   357
\index{*merge_ss}
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   358
\index{*simpset}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   359
\index{*Addsimps}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   360
\index{*Delsimps}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   361
\index{*simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   362
\index{*asm_simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   363
\index{*full_simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   364
\index{*asm_full_simp_tac}
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   365
\index{*safe_asm_full_simp_tac}
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   366
\index{*Simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   367
\index{*Asm_simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   368
\index{*Full_simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   369
\index{*Asm_full_simp_tac}
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   370
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\begin{ttbox}
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   372
infix 4 setsubgoaler setloop addloop 
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   373
        setSSolver addSSolver setSolver addSolver 
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   374
        setmksimps addsimps delsimps addeqcongs deleqcongs;
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
signature SIMPLIFIER =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
  type simpset
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   379
  val empty_ss: simpset
3134
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   380
  val rep_ss: simpset -> {\ttlbrace}simps: thm list, procs: string list, 
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   381
                          congs: thm list,
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   382
                          subgoal_tac:        simpset -> int -> tactic,
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   383
                          loop_tac:                      int -> tactic,
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   384
                                 finish_tac: thm list -> int -> tactic,
3134
cf97438b0232 fixed braces;
wenzelm
parents: 3128
diff changeset
   385
                          unsafe_finish_tac: thm list -> int -> tactic{\ttrbrace}
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   386
  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   387
  val setloop:      simpset *             (int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   388
  val addloop:      simpset *             (int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   389
  val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   390
  val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   391
  val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   392
  val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   393
  val setmksimps:  simpset * (thm -> thm list) -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   394
  val addsimps:    simpset * thm list -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   395
  val delsimps:    simpset * thm list -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   396
  val addeqcongs:  simpset * thm list -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   397
  val deleqcongs:  simpset * thm list -> simpset
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   398
  val merge_ss:    simpset * simpset -> simpset
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   399
  val prems_of_ss: simpset -> thm list
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   400
  val simpset:     simpset ref
2567
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   401
  val Addsimps: thm list -> unit
7a28e02e10b7 added addloop (and also documentation of addsolver
oheimb
parents: 2479
diff changeset
   402
  val Delsimps: thm list -> unit
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   403
  val               simp_tac: simpset -> int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   404
  val           asm_simp_tac: simpset -> int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   405
  val          full_simp_tac: simpset -> int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   406
  val      asm_full_simp_tac: simpset -> int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   407
  val safe_asm_full_simp_tac: simpset -> int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   408
  val               Simp_tac:            int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   409
  val           Asm_simp_tac:            int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   410
  val          Full_simp_tac:            int -> tactic
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   411
  val      Asm_full_simp_tac:            int -> tactic
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   414
\caption{The simplifier primitives} \label{SIMPLIFIER}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   418
\section{The simplification tactics}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   419
\label{simp-tactics}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   420
\index{simplification!tactics}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   421
\index{tactics!simplification}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   423
The actual simplification work is performed by the following basic tactics:
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   424
\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   425
\ttindexbold{full_simp_tac} and \ttindexbold{asm_full_simp_tac}.  They work
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   426
exactly like their namesakes in \S\ref{sec:simp-for-dummies}, except that
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   427
they are explicitly supplied with a simpset.  This is because the ones in
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   428
\S\ref{sec:simp-for-dummies} are defined in terms of the ones above, e.g.
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   429
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   430
fun Simp_tac i = simp_tac (!simpset) i;
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   431
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   432
where \ttindex{!simpset} is the current simpset\index{simpset!current}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   434
The rewriting strategy of all four tactics is strictly bottom up, except for
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   435
congruence rules, which are applied while descending into a term.  Conditions
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   436
in conditional rewrite rules are solved recursively before the rewrite rule
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   437
is applied.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   439
The infix operation \ttindex{addsimps} adds rewrite rules to a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   440
simpset, while \ttindex{delsimps} deletes them.  They are used to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   441
implement \ttindex{Addsimps} and \ttindex{Delsimps}, e.g.
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   442
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   443
fun Addsimps thms = (simpset := (!simpset addsimps thms));
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   444
\end{ttbox}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   445
and can also be used directly, even in the presence of a current simpset.  For
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   446
example
1213
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   447
\begin{ttbox}
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   448
Addsimps \(thms\);
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   449
by (Simp_tac \(i\));
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   450
Delsimps \(thms\);
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   451
\end{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   452
can be compressed into
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   453
\begin{ttbox}
2479
57109c1a653d Updated account of implicit simpsets and clasets
paulson
parents: 2020
diff changeset
   454
by (simp_tac (!simpset addsimps \(thms\)) \(i\));
1213
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   455
\end{ttbox}
1860
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   456
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   457
The simpset associated with a particular theory can be retrieved via the name
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   458
of the theory using the function
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   459
\begin{ttbox}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   460
simpset_of: string -> simpset
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   461
\end{ttbox}\index{*simpset_of}
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   462
71bfeecfa96c Documented simplification tactics which make use of the implicit simpset.
nipkow
parents: 1387
diff changeset
   463
To remind yourself of what is in a simpset, use the function \verb$rep_ss$ to
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
return its simplification and congruence rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   466
\section{Examples using the simplifier}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   467
\index{examples!of simplification} Assume we are working within {\tt
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   468
  FOL} (cf.\ \texttt{FOL/ex/Nat}) and that
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   469
\begin{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   470
\item[Nat.thy] 
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   471
  is a theory including the constants $0$, $Suc$ and $+$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   472
\item[add_0]
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   473
  is the rewrite rule $0+\Var{n} = \Var{n}$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   474
\item[add_Suc]
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   475
  is the rewrite rule $Suc(\Var{m})+\Var{n} = Suc(\Var{m}+\Var{n})$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   476
\item[induct]
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   477
  is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   478
    \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   479
\end{ttdescription}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   480
We augment the implicit simpset of {\FOL} with the basic rewrite rules
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   481
for natural numbers:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   483
Addsimps [add_0, add_Suc];
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   485
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   486
\subsection{A trivial example}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   487
Proofs by induction typically involve simplification.  Here is a proof
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   488
that~0 is a right identity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
goal Nat.thy "m+0 = m";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
{\out  1. m + 0 = m}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   494
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   495
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
   496
base case and inductive step as two subgoals:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   497
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
{\out  1. 0 + 0 = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
{\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   504
Simplification solves the first subgoal trivially:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   506
by (Simp_tac 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
{\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\end{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   511
The remaining subgoal requires \ttindex{Asm_simp_tac} in order to use the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
induction hypothesis as a rewrite rule:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   514
by (Asm_simp_tac 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   520
\subsection{An example of tracing}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   521
\index{tracing!of simplification|(}\index{*trace_simp}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   522
Let us prove a similar result involving more complex terms.  The two
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   523
equations together can be used to prove that addition is commutative.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
goal Nat.thy "m+Suc(n) = Suc(m+n)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
{\out  1. m + Suc(n) = Suc(m + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   529
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   530
We again perform induction on~$m$ and get two subgoals:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   531
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
{\out  1. 0 + Suc(n) = Suc(0 + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   536
{\out  2. !!x. x + Suc(n) = Suc(x + n) ==>}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   537
{\out          Suc(x) + Suc(n) = Suc(Suc(x) + n)}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   538
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   539
Simplification solves the first subgoal, this time rewriting two
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   540
occurrences of~0:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   541
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   542
by (Simp_tac 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
{\out m + Suc(n) = Suc(m + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   545
{\out  1. !!x. x + Suc(n) = Suc(x + n) ==>}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   546
{\out          Suc(x) + Suc(n) = Suc(Suc(x) + n)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
Switching tracing on illustrates how the simplifier solves the remaining
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
subgoal: 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
trace_simp := true;
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   552
by (Asm_simp_tac 1);
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   553
\ttbreak
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   554
{\out Adding rewrite rule:}
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   555
{\out .x + Suc(n) == Suc(.x + n)}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   556
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
{\out Rewriting:}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   558
{\out Suc(.x) + Suc(n) == Suc(.x + Suc(n))}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   559
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
{\out Rewriting:}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   561
{\out .x + Suc(n) == Suc(.x + n)}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   562
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
{\out Rewriting:}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   564
{\out Suc(.x) + n == Suc(.x + n)}
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   565
\ttbreak
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   566
{\out Rewriting:}
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   567
{\out Suc(Suc(.x + n)) = Suc(Suc(.x + n)) == True}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   568
\ttbreak
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   573
Many variations are possible.  At Level~1 (in either example) we could have
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   574
solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   576
by (ALLGOALS Asm_simp_tac);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   581
\index{tracing!of simplification|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   583
\subsection{Free variables and simplification}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   585
the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
val [prem] = goal Nat.thy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
    "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
{\out  1. f(i + j) = i + f(j)}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   592
\ttbreak
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   593
{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   594
{\out             [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   595
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   596
In the theorem~{\tt prem}, note that $f$ is a free variable while
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   597
$\Var{n}$ is a schematic variable.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   598
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
by (res_inst_tac [("n","i")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
{\out  1. f(0 + j) = 0 + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
{\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
We simplify each subgoal in turn.  The first one is trivial:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   607
by (Simp_tac 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
{\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
\end{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   612
The remaining subgoal requires rewriting by the premise, so we add it
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   613
to the current simpset:\footnote{The previous simplifier required
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   614
  congruence rules for function variables like~$f$ in order to
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   615
  simplify their arguments.  It was more general than the current
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   616
  simplifier, but harder to use and slower.  The present simplifier
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   617
  can be given congruence rules to realize non-standard simplification
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   618
  of a function's arguments, but this is seldom necessary.}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
   620
by (asm_simp_tac (!simpset addsimps [prem]) 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
1213
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   626
\subsection{Reordering assumptions}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   627
\label{sec:reordering-asms}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   628
\index{assumptions!reordering}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   629
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   630
As mentioned above, \ttindex{asm_full_simp_tac} may require the assumptions
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   631
to be permuted to be more effective.  Given the subgoal
1213
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   632
\begin{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   633
{\out 1. [| P(f(a)); Q; f(a) = t; R |] ==> S}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   634
\end{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   635
we can rotate the assumptions two positions to the right
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   636
\begin{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   637
by (rotate_tac ~2 1);
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   638
\end{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   639
to obtain
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   640
\begin{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   641
{\out 1. [| f(a) = t; R; P(f(a)); Q |] ==> S}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   642
\end{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   643
which enables \verb$asm_full_simp_tac$ to simplify \verb$P(f(a))$ to
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   644
\verb$P(t)$.
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   645
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   646
Since rotation alone cannot produce arbitrary permutations, you can also pick
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   647
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
   648
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
   649
\begin{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   650
by (dres_inst_tac [("psi","P(f(a))")] asm_rl 1);
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   651
\end{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   652
which is more directed and leads to
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   653
\begin{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   654
{\out 1. [| Q; f(a) = t; R; P(f(a)) |] ==> S}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   655
\end{ttbox}
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   656
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   657
Note that reordering assumptions usually leads to brittle proofs and should
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3134
diff changeset
   658
therefore be avoided.  Future versions of \verb$asm_full_simp_tac$ may remove
1213
a8f6d0fa2a59 added section on "Reordering assumptions".
nipkow
parents: 1101
diff changeset
   659
the need for such manipulations.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   660
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   661
\section{Permutative rewrite rules}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   662
\index{rewrite rules!permutative|(}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   663
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   664
A rewrite rule is {\bf permutative} if the left-hand side and right-hand
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   665
side are the same up to renaming of variables.  The most common permutative
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   666
rule is commutativity: $x+y = y+x$.  Other examples include $(x-y)-z =
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   667
(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
   668
for sets.  Such rules are common enough to merit special attention.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   669
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   670
Because ordinary rewriting loops given such rules, the simplifier employs a
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   671
special strategy, called {\bf ordered rewriting}\index{rewriting!ordered}.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   672
There is a standard lexicographic ordering on terms.  A permutative rewrite
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   673
rule is applied only if it decreases the given term with respect to this
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   674
ordering.  For example, commutativity rewrites~$b+a$ to $a+b$, but then
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   675
stops because $a+b$ is strictly less than $b+a$.  The Boyer-Moore theorem
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   676
prover~\cite{bm88book} also employs ordered rewriting.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   677
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   678
Permutative rewrite rules are added to simpsets just like other rewrite
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   679
rules; the simplifier recognizes their special status automatically.  They
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   680
are most effective in the case of associative-commutative operators.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   681
(Associativity by itself is not permutative.)  When dealing with an
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   682
AC-operator~$f$, keep the following points in mind:
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   683
\begin{itemize}\index{associative-commutative operators}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   684
\item The associative law must always be oriented from left to right, namely
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   685
  $f(f(x,y),z) = f(x,f(y,z))$.  The opposite orientation, if used with
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   686
  commutativity, leads to looping!  Future versions of Isabelle may remove
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   687
  this restriction.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   688
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   689
\item To complete your set of rewrite rules, you must add not just
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   690
  associativity~(A) and commutativity~(C) but also a derived rule, {\bf
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   691
    left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   692
\end{itemize}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   693
Ordered rewriting with the combination of A, C, and~LC sorts a term
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   694
lexicographically:
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   695
\[\def\maps#1{\stackrel{#1}{\longmapsto}}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   696
 (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
   697
Martin and Nipkow~\cite{martin-nipkow} discuss the theory and give many
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   698
examples; other algebraic structures are amenable to ordered rewriting,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   699
such as boolean rings.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   700
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   701
\subsection{Example: sums of natural numbers}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   702
This example is set in \HOL\ (see \texttt{HOL/ex/NatSum}).  Theory
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   703
\thydx{Arith} contains natural numbers arithmetic.  Its associated
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   704
simpset contains many arithmetic laws including distributivity
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   705
of~$\times$ over~$+$, while {\tt add_ac} is a list consisting of the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   706
A, C and LC laws for~$+$ on type \texttt{nat}.  Let us prove the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   707
theorem
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   708
\[ \sum@{i=1}^n i = n\times(n+1)/2. \]
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   709
%
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   710
A functional~{\tt sum} represents the summation operator under the
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   711
interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$.  We
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   712
extend {\tt Arith} using a theory file:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   713
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   714
NatSum = Arith +
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1213
diff changeset
   715
consts sum     :: [nat=>nat, nat] => nat
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   716
primrec "sum" nat 
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   717
  "sum f 0 = 0"
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   718
  "sum f (Suc n) = f(n) + sum f n"
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   719
end
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   720
\end{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   721
The \texttt{primrec} declaration automatically adds rewrite rules for
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   722
\texttt{sum} to the default simpset.  We now insert the AC-rules for~$+$:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   723
\begin{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   724
Addsimps add_ac;
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   725
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   726
Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) =
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   727
n\times(n+1)/2$.  The Isabelle goal has both sides multiplied by~$2$:
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   728
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   729
goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n";
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   730
{\out Level 0}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   731
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   732
{\out  1. 2 * sum (\%i. i) (Suc n) = n * Suc n}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   733
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   734
Induction should not be applied until the goal is in the simplest
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   735
form:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   736
\begin{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   737
by (Simp_tac 1);
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   738
{\out Level 1}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   739
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   740
{\out  1. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   741
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   742
Ordered rewriting has sorted the terms in the left-hand side.  The
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   743
subgoal is now ready for induction:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   744
\begin{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   745
by (induct_tac "n" 1);
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   746
{\out Level 2}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   747
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   748
{\out  1. 0 + (sum (\%i. i) 0 + sum (\%i. i) 0) = 0 * 0}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   749
\ttbreak
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   750
{\out  2. !!n. n + (sum (\%i. i) n + sum (\%i. i) n) = n * n}
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   751
{\out           ==> Suc n + (sum (\%i. i) (Suc n) + sum (\%i. i) (Suc n)) =}
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   752
{\out               Suc n * Suc n}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   753
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   754
Simplification proves both subgoals immediately:\index{*ALLGOALS}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   755
\begin{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   756
by (ALLGOALS Asm_simp_tac);
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   757
{\out Level 3}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   758
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   759
{\out No subgoals!}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   760
\end{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   761
Simplification cannot prove the induction step if we omit {\tt add_ac} from
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   762
the simpset.  Observe that like terms have not been collected:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   763
\begin{ttbox}
4245
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   764
{\out Level 3}
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   765
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   766
{\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
   767
{\out           ==> n + (n + sum (\%i. i) n) + (n + (n + sum (\%i. i) n)) =}
b9ce25073cc0 Updated the NatSum example
paulson
parents: 3950
diff changeset
   768
{\out               n + (n + (n + n * n))}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   769
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   770
Ordered rewriting proves this by sorting the left-hand side.  Proving
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   771
arithmetic theorems without ordered rewriting requires explicit use of
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   772
commutativity.  This is tedious; try it and see!
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   773
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   774
Ordered rewriting is equally successful in proving
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   775
$\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   776
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   777
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   778
\subsection{Re-orienting equalities}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   779
Ordered rewriting with the derived rule {\tt symmetry} can reverse equality
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   780
signs:
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   781
\begin{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   782
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
3128
d01d4c0c4b44 New acknowledgements; fixed overfull lines and tables
paulson
parents: 3112
diff changeset
   783
                 (fn _ => [Blast_tac 1]);
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   784
\end{ttbox}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   785
This is frequently useful.  Assumptions of the form $s=t$, where $t$ occurs
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   786
in the conclusion but not~$s$, can often be brought into the right form.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   787
For example, ordered rewriting with {\tt symmetry} can prove the goal
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   788
\[ f(a)=b \conj f(a)=c \imp b=c. \]
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   789
Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   790
because $f(a)$ is lexicographically greater than $b$ and~$c$.  These
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   791
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   792
conclusion by~$f(a)$. 
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   793
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   794
Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   795
The differing orientations make this appear difficult to prove.  Ordered
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   796
rewriting with {\tt symmetry} makes the equalities agree.  (Without
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   797
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
   798
or~$u=t$.)  Then the simplifier can prove the goal outright.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   799
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   800
\index{rewrite rules!permutative|)}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   801
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   802
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   803
\section{*Setting up the simplifier}\label{sec:setting-up-simp}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   804
\index{simplification!setting up}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   805
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   806
Setting up the simplifier for new logics is complicated.  This section
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   807
describes how the simplifier is installed for intuitionistic first-order
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   808
logic; the code is largely taken from {\tt FOL/simpdata.ML}.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   809
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   810
The simplifier and the case splitting tactic, which reside on separate
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   811
files, are not part of Pure Isabelle.  They must be loaded explicitly:
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   812
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   813
use "../Provers/simplifier.ML";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   814
use "../Provers/splitter.ML";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   815
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   816
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   817
Simplification works by reducing various object-equalities to
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   818
meta-equality.  It requires rules stating that equal terms and equivalent
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   819
formulae are also equal at the meta-level.  The rule declaration part of
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3087
diff changeset
   820
the file {\tt FOL/IFOL.thy} contains the two lines
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   821
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   822
eq_reflection   "(x=y)   ==> (x==y)"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   823
iff_reflection  "(P<->Q) ==> (P==Q)"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   824
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   825
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
   826
particular logic.  In Constructive Type Theory, equality is a ternary
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   827
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the
332
01b87a921967 final Springer copy
lcp
parents: 323
diff changeset
   828
equality essentially as a partial equivalence relation.  The present
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   829
simplifier cannot be used.  Rewriting in {\tt CTT} uses another simplifier,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   830
which resides in the file {\tt typedsimp.ML} and is not documented.  Even
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   831
this does not work for later variants of Constructive Type Theory that use
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   832
intensional equality~\cite{nordstrom90}.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   833
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   834
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   835
\subsection{A collection of standard rewrite rules}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   836
The file begins by proving lots of standard rewrite rules about the logical
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   837
connectives.  These include cancellation and associative laws.  To prove
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   838
them easily, it defines a function that echoes the desired law and then
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   839
supplies it the theorem prover for intuitionistic \FOL:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   840
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   841
fun int_prove_fun s = 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   842
 (writeln s;  
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   843
  prove_goal IFOL.thy s
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   844
   (fn prems => [ (cut_facts_tac prems 1), 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   845
                  (Int.fast_tac 1) ]));
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   846
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   847
The following rewrite rules about conjunction are a selection of those
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   848
proved on {\tt FOL/simpdata.ML}.  Later, these will be supplied to the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   849
standard simpset.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   850
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   851
val conj_rews = map int_prove_fun
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   852
 ["P & True <-> P",      "True & P <-> P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   853
  "P & False <-> False", "False & P <-> False",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   854
  "P & P <-> P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   855
  "P & ~P <-> False",    "~P & P <-> False",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   856
  "(P & Q) & R <-> P & (Q & R)"];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   857
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   858
The file also proves some distributive laws.  As they can cause exponential
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   859
blowup, they will not be included in the standard simpset.  Instead they
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   860
are merely bound to an \ML{} identifier, for user reference.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   861
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   862
val distrib_rews  = map int_prove_fun
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   863
 ["P & (Q | R) <-> P&Q | P&R", 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   864
  "(Q | R) & P <-> Q&P | R&P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   865
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   866
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   867
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   868
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   869
\subsection{Functions for preprocessing the rewrite rules}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   870
\label{sec:setmksimps}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   871
%
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   872
The next step is to define the function for preprocessing rewrite rules.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   873
This will be installed by calling {\tt setmksimps} below.  Preprocessing
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   874
occurs whenever rewrite rules are added, whether by user command or
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   875
automatically.  Preprocessing involves extracting atomic rewrites at the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   876
object-level, then reflecting them to the meta-level.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   877
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   878
To start, the function {\tt gen_all} strips any meta-level
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   879
quantifiers from the front of the given theorem.  Usually there are none
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   880
anyway.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   881
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   882
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   883
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   884
The function {\tt atomize} analyses a theorem in order to extract
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   885
atomic rewrite rules.  The head of all the patterns, matched by the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   886
wildcard~{\tt _}, is the coercion function {\tt Trueprop}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   887
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   888
fun atomize th = case concl_of th of 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   889
    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) \at
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   890
                                       atomize(th RS conjunct2)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   891
  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   892
  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   893
  | _ $ (Const("True",_))           => []
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   894
  | _ $ (Const("False",_))          => []
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   895
  | _                               => [th];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   896
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   897
There are several cases, depending upon the form of the conclusion:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   898
\begin{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   899
\item Conjunction: extract rewrites from both conjuncts.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   900
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   901
\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
   902
  extract rewrites from~$Q$; these will be conditional rewrites with the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   903
  condition~$P$.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   904
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   905
\item Universal quantification: remove the quantifier, replacing the bound
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   906
  variable by a schematic variable, and extract rewrites from the body.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   907
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   908
\item {\tt True} and {\tt False} contain no useful rewrites.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   909
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   910
\item Anything else: return the theorem in a singleton list.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   911
\end{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   912
The resulting theorems are not literally atomic --- they could be
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   913
disjunctive, for example --- but are broken down as much as possible.  See
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   914
the file {\tt ZF/simpdata.ML} for a sophisticated translation of
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   915
set-theoretic formulae into rewrite rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   916
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   917
The simplified rewrites must now be converted into meta-equalities.  The
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   918
rule {\tt eq_reflection} converts equality rewrites, while {\tt
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   919
  iff_reflection} converts if-and-only-if rewrites.  The latter possibility
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   920
can arise in two other ways: the negative theorem~$\neg P$ is converted to
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   921
$P\equiv{\tt False}$, and any other theorem~$P$ is converted to
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   922
$P\equiv{\tt True}$.  The rules {\tt iff_reflection_F} and {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   923
  iff_reflection_T} accomplish this conversion.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   924
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   925
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   926
val iff_reflection_F = P_iff_F RS iff_reflection;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   927
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   928
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   929
val iff_reflection_T = P_iff_T RS iff_reflection;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   930
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   931
The function {\tt mk_meta_eq} converts a theorem to a meta-equality
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   932
using the case analysis described above.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   933
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   934
fun mk_meta_eq th = case concl_of th of
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   935
    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   936
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   937
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   938
  | _                           => th RS iff_reflection_T;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   939
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   940
The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   941
be composed together and supplied below to {\tt setmksimps}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   942
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   943
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   944
\subsection{Making the initial simpset}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   945
It is time to assemble these items.  We open module {\tt Simplifier} to
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   946
gain access to its components.  We define the infix operator
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   947
\ttindexbold{addcongs} to insert congruence rules; given a list of theorems,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   948
it converts their conclusions into meta-equalities and passes them to
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   949
\ttindex{addeqcongs}.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   950
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   951
open Simplifier;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   952
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   953
infix addcongs;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   954
fun ss addcongs congs =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   955
    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   956
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   957
The list {\tt IFOL_rews} contains the default rewrite rules for first-order
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   958
logic.  The first of these is the reflexive law expressed as the
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   959
equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is clearly useless.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   960
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   961
val IFOL_rews =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   962
   [refl RS P_iff_T] \at conj_rews \at disj_rews \at not_rews \at 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   963
    imp_rews \at iff_rews \at quant_rews;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   964
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   965
The list {\tt triv_rls} contains trivial theorems for the solver.  Any
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   966
subgoal that is simplified to one of these will be removed.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   967
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   968
val notFalseI = int_prove_fun "~False";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   969
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   970
\end{ttbox}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   971
%
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   972
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   973
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   974
  mk_meta_eq}.  It solves simplified subgoals using {\tt triv_rls} and
2613
cc4eb23d37b3 Updated documentation of IFOL_ss
paulson
parents: 2567
diff changeset
   975
assumptions, and by detecting contradictions.  
cc4eb23d37b3 Updated documentation of IFOL_ss
paulson
parents: 2567
diff changeset
   976
It uses \ttindex{asm_simp_tac} to tackle subgoals of
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   977
conditional rewrites.  It takes {\tt IFOL_rews} as rewrite rules.  
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   978
Other simpsets built from {\tt IFOL_ss} will inherit these items.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   979
In particular, {\tt FOL_ss} extends {\tt IFOL_ss} with classical rewrite
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   980
rules such as $\neg\neg P\bimp P$.
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   981
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   982
\index{*addsimps}\index{*addcongs}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   983
\begin{ttbox}
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2628
diff changeset
   984
fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls \at prems),
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   985
                                 atac, etac FalseE];
2632
1612b99395d4 corrected minor mistakes
oheimb
parents: 2628
diff changeset
   986
fun   safe_solver prems = FIRST'[match_tac (triv_rls \at prems),
2628
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   987
                                 eq_assume_tac, ematch_tac [FalseE]];
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   988
val IFOL_ss = empty_ss setsubgoaler asm_simp_tac
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   989
                       setSSolver   safe_solver
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   990
                       setSolver  unsafe_solver
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   991
                       setmksimps (map mk_meta_eq o atomize o gen_all)
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   992
                       addsimps IFOL_simps
1fe7c9f599c2 description of del(eq)congs, safe and unsafe solver
oheimb
parents: 2613
diff changeset
   993
                       addcongs [imp_cong];
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   994
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   995
This simpset takes {\tt imp_cong} as a congruence rule in order to use
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   996
contextual information to simplify the conclusions of implications:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   997
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   998
   (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   999
\]
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1000
By adding the congruence rule {\tt conj_cong}, we could obtain a similar
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1001
effect for conjunctions.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1002
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1003
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1004
\subsection{Case splitting}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1005
To set up case splitting, we must prove the theorem below and pass it to
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1006
\ttindexbold{mk_case_split_tac}.  The tactic \ttindexbold{split_tac} uses
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1007
{\tt mk_meta_eq}, defined above, to convert the splitting rules to
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1008
meta-equalities.
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1009
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1010
val meta_iffD = 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1011
    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1012
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1013
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1014
fun split_tac splits =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1015
    mk_case_split_tac meta_iffD (map mk_meta_eq splits);
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1016
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1017
%
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1018
The splitter replaces applications of a given function; the right-hand side
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1019
of the replacement can be anything.  For example, here is a splitting rule
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1020
for conditional expressions:
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1021
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1022
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1023
\] 
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1024
Another example is the elimination operator (which happens to be
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
  1025
called~$split$) for Cartesian products:
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1026
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1027
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1028
\] 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1029
Case splits should be allowed only when necessary; they are expensive
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1030
and hard to control.  Here is a typical example of use, where {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1031
  expand_if} is the first rule above:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1032
\begin{ttbox}
3112
0f764be1583a fixed simplifier examples;
wenzelm
parents: 3108
diff changeset
  1033
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1034
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1035
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1036
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1037
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1038
\index{simplification|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1039
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
  1040