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