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