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