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