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