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