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