doc-src/Ref/simplifier.tex
author lcp
Mon, 21 Mar 1994 11:02:57 +0100
changeset 286 e7efbf03562b
parent 133 2322fd6d57a1
child 323 361a71713176
permissions -rw-r--r--
first draft of Springer book
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
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
provides a suite of simplification tactics.  This rewriting package is less
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
general than its predecessor --- it works only for the equality relation,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
not arbitrary preorders --- but it is fast and flexible.  It performs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
conditional and unconditional rewriting and uses contextual information
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
(``local assumptions'').  It provides a few general hooks, which can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
provide automatic case splits during rewriting, for example.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
simplifier is set up for many of Isabelle's logics: {\tt FOL}, {\tt ZF},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
{\tt LCF} and {\tt HOL}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    16
\section{Simplification sets}\index{simplification sets} 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
The simplification tactics are controlled by {\bf simpsets}.  These consist
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
of five components: rewrite rules, congruence rules, the subgoaler, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
solver and the looper.  Normally, the simplifier is set up with sensible
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
defaults, so that most simplifier calls specify only rewrite rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
Sophisticated usage of the other components can be highly effective, but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
most users should never worry about them.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
\subsection{Rewrite rules}\index{rewrite rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
Rewrite rules are theorems like $Suc(\Var{m}) + \Var{n} = \Var{m} +
122
db9043a8e372 replaced \un by \union in "Simplification sets"
clasohm
parents: 104
diff changeset
    26
Suc(\Var{n})$, $\Var{P}\conj\Var{P} \bimp \Var{P}$, or $\Var{A} \union \Var{B}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
\equiv \{x.x\in A \disj x\in B\}$.  {\bf Conditional} rewrites such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
$\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} = 0$ are permitted; the conditions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
can be arbitrary terms.  The infix operation \ttindex{addsimps} adds new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
rewrite rules, while \ttindex{delsimps} deletes rewrite rules from a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
simpset.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
Theorems added via \ttindex{addsimps} need not be equalities to start with.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
Each simpset contains a (user-definable) function for extracting equalities
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
from arbitrary theorems.  For example $\neg(x\in \{\})$ could be turned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
into $x\in \{\} \equiv False$.  This function can be set with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\ttindex{setmksimps} but only the definer of a logic should need to do
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
this.  Exceptionally, one may want to install a selective version of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\ttindex{mksimps} in order to filter out looping rewrite rules arising from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
local assumptions (see below).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
Internally, all rewrite rules are translated into meta-equalities:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
theorems with conclusion $lhs \equiv rhs$.  To this end every simpset contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
a function of type \verb$thm -> thm list$ to extract a list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
of meta-equalities from a given theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\begin{warn}\index{rewrite rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
  The left-hand side of a rewrite rule must look like a first-order term:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
  after eta-contraction, none of its unknowns should have arguments.  Hence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
  ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
  x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
  $\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not.  However, you can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
  replace the offending subterms by new variables and conditions: $\Var{y} =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
  \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
  acceptable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\subsection {Congruence rules}\index{congruence rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
Congruence rules are meta-equalities of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\[ \List{\dots} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
   f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
They control the simplification of the arguments of certain constants.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
example, some arguments can be simplified under additional assumptions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\[ \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
    66
   \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
This rule assumes $Q@1$ and any rewrite rules it implies, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
simplifying~$P@2$.  Such ``local'' assumptions are effective for rewriting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
formulae such as $x=0\imp y+x=y$.  The next example makes similar use of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
such contextual information in bounded quantifiers:
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    72
\begin{eqnarray*}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    73
  &&\List{\Var{A}=\Var{B};\; 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    74
          \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
    75
 &&\qquad\qquad
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    76
    (\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
    77
\end{eqnarray*}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
This congruence rule supplies contextual information for simplifying the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
arms of a conditional expressions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
         \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
A congruence rule can also suppress simplification of certain arguments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
Here is an alternative congruence rule for conditional expressions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\[ \Var{p}=\Var{q} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
   if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
Only the first argument is simplified; the others remain unchanged.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
This can make simplification much faster, but may require an extra case split
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
to prove the goal.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
    94
Congruence rules are added using \ttindexbold{addeqcongs}.  Their conclusion
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
must be a meta-equality, as in the examples above.  It is more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
natural to derive the rules with object-logic equality, for example
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\[ \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
    98
   \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\]
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   100
Each object-logic should define an operator called \ttindex{addcongs} that
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   101
expects object-equalities and translates them into meta-equalities.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   103
\subsection{The subgoaler}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
The subgoaler is the tactic used to solve subgoals arising out of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
conditional rewrite rules or congruence rules.  The default should be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
simplification itself.  Occasionally this strategy needs to be changed.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
example, if the premise of a conditional rule is an instance of its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m} < \Var{n}$, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
default strategy could loop.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
The subgoaler can be set explicitly with \ttindex{setsubgoaler}.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
example, the subgoaler
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE' 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
                     asm_simp_tac ss;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
tries to solve the subgoal with one of the premises and calls
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
simplification only if that fails; here {\tt prems_of_ss} extracts the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
current premises from a simpset.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   121
\subsection{The solver}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   122
The solver is a tactic that attempts to solve a subgoal after
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   123
simplification.  Typically it just proves trivial subgoals such as {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   124
  True} and $t=t$; it could use sophisticated means such as
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   125
\verb$fast_tac$.  The solver is set using \ttindex{setsolver}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   126
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   127
The tactic is presented with the full goal, including the asssumptions.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   128
Hence it can use those assumptions (say by calling {\tt assume_tac}) even
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   129
inside {\tt simp_tac}, which otherwise does not use assumptions.  The
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   130
solver is also supplied a list of theorems, namely assumptions that hold in
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   131
the local context.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
  Rewriting does not instantiate unknowns.  Trying to rewrite $a\in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
  \Var{A}$ with the rule $\Var{x}\in \{\Var{x}\}$ leads nowhere.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
  solver, however, is an arbitrary tactic and may instantiate unknowns as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
  it pleases.  This is the only way the simplifier can handle a conditional
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
  rewrite rule whose condition contains extra variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
  If you want to supply your own subgoaler or solver, read on.  The subgoaler
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
  is also used to solve the premises of congruence rules, which are usually
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
  of the form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
  needs to be instantiated with the result. Hence the subgoaler should call
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
  the simplifier at some point. The simplifier will then call the solver,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
  which must therefore be prepared to solve goals of the form $t = \Var{x}$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
  usually by reflexivity. In particular, reflexivity should be tried before
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
  any of the fancy tactics like {\tt fast_tac}. It may even happen that, due
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
  to simplification, the subgoal is no longer an equality. For example $False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
  \bimp \Var{Q}$ could be rewritten to $\neg\Var{Q}$, in which case the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
  solver must also try resolving with the theorem $\neg False$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
  If the simplifier aborts with the message {\tt Failed congruence proof!},
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   155
  it is due to the subgoaler or solver that failed to prove a premise of a
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
  congruence rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
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}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
\indexbold{*SIMPLIFIER}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   172
\indexbold{*simpset}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   173
\indexbold{*simp_tac}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   174
\indexbold{*asm_simp_tac}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   175
\indexbold{*asm_full_simp_tac}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   176
\indexbold{*addeqcongs}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   177
\indexbold{*addsimps}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   178
\indexbold{*delsimps}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   179
\indexbold{*empty_ss}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   180
\indexbold{*merge_ss}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   181
\indexbold{*setsubgoaler}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   182
\indexbold{*setsolver}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   183
\indexbold{*setloop}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   184
\indexbold{*setmksimps}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   185
\indexbold{*prems_of_ss}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   186
\indexbold{*rep_ss}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
infix addsimps addeqcongs delsimps
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
      setsubgoaler setsolver setloop setmksimps;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
signature SIMPLIFIER =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
  type simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
  val simp_tac:          simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
  val asm_simp_tac:      simpset -> int -> tactic
133
2322fd6d57a1 Reformatting of SIMPLIFIER figure
lcp
parents: 122
diff changeset
   196
  val asm_full_simp_tac: simpset -> int -> tactic\smallskip
2322fd6d57a1 Reformatting of SIMPLIFIER figure
lcp
parents: 122
diff changeset
   197
  val addeqcongs:   simpset * thm list -> simpset
2322fd6d57a1 Reformatting of SIMPLIFIER figure
lcp
parents: 122
diff changeset
   198
  val addsimps:     simpset * thm list -> simpset
2322fd6d57a1 Reformatting of SIMPLIFIER figure
lcp
parents: 122
diff changeset
   199
  val delsimps:     simpset * thm list -> simpset
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
  val empty_ss:     simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
  val merge_ss:     simpset * simpset -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
  val setsolver:    simpset * (thm list -> int -> tactic) -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
  val setloop:      simpset * (int -> tactic) -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
  val setmksimps:   simpset * (thm -> thm list) -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
  val prems_of_ss:  simpset -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
  val rep_ss:       simpset -> \{simps: thm list, congs: thm list\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
\caption{The signature \ttindex{SIMPLIFIER}} \label{SIMPLIFIER}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
\section{The simplification tactics} \label{simp-tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
\index{simplification!tactics|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\index{tactics!simplification|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
The actual simplification work is performed by the following tactics.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
rewriting strategy is strictly bottom up, except for congruence rules, which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
are applied while descending into a term.  Conditions in conditional rewrite
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
rules are solved recursively before the rewrite rule is applied.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
There are three basic simplification tactics:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\item[\ttindexbold{simp_tac} $ss$ $i$] simplifies subgoal~$i$ using the rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
  in~$ss$.  It may solve the subgoal completely if it has become trivial,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
  using the solver.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
\item[\ttindexbold{asm_simp_tac}] is like \verb$simp_tac$, but also uses
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
  assumptions as additional rewrite rules.
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.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
\end{description}
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}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\index{simplification!example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
Assume we are working within {\tt FOL} and that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\item[\tt Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
\item[\tt add_0] is the rewrite rule $0+n = n$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
\item[\tt add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\item[\tt induct] is the induction rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
\item[\tt FOL_ss] is a basic simpset for {\tt FOL}.\footnote
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
{These examples reside on the file {\tt FOL/ex/nat.ML}.} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
We create a simpset for natural numbers by extending~{\tt FOL_ss}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
val add_ss = FOL_ss addsimps [add_0, add_Suc];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   258
Proofs by induction typically involve simplification.  Here is a proof
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   259
that~0 is a right identity:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
goal Nat.thy "m+0 = m";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
{\out  1. m + 0 = m}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   265
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   266
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
   267
base case and inductive step as two subgoals:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   268
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
{\out  1. 0 + 0 = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
{\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   275
Simplification solves the first subgoal trivially:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
by (simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
{\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
The remaining subgoal requires \ttindex{asm_simp_tac} in order to use the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
induction hypothesis as a rewrite rule:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
by (asm_simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
The next proof is similar.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
goal Nat.thy "m+Suc(n) = Suc(m+n)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
{\out  1. m + Suc(n) = Suc(m + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   297
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   298
We again perform induction on~$m$ and get two subgoals:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   299
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
{\out  1. 0 + Suc(n) = Suc(0 + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   304
{\out  2. !!x. x + Suc(n) = Suc(x + n) ==>}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   305
{\out          Suc(x) + Suc(n) = Suc(Suc(x) + n)}
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
Simplification solves the first subgoal, this time rewriting two
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   308
occurrences of~0:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   309
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
by (simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
{\out m + Suc(n) = Suc(m + n)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   313
{\out  1. !!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)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
Switching tracing on illustrates how the simplifier solves the remaining
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
subgoal: 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
trace_simp := true;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
by (asm_simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
{\out Rewriting:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
{\out Suc(x) + Suc(n) == Suc(x + Suc(n))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
{\out Rewriting:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
{\out x + Suc(n) == Suc(x + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
{\out Rewriting:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
{\out Suc(x) + n == Suc(x + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
{\out Rewriting:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
{\out Suc(Suc(x + n)) = Suc(Suc(x + n)) == True}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   333
Many variations are possible.  At Level~1 (in either example) we could have
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   334
solved both subgoals at once using the tactical \ttindex{ALLGOALS}:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
by (ALLGOALS (asm_simp_tac add_ss));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   344
the law $f(Suc(n)) = Suc(f(n))$:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
val [prem] = goal Nat.thy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
    "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
{\out  1. f(i + j) = i + f(j)}
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   351
{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   352
{\out             [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\ttbreak
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
by (res_inst_tac [("n","i")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
{\out  1. f(0 + j) = 0 + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
{\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
We simplify each subgoal in turn.  The first one is trivial:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
by (simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
{\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
The remaining subgoal requires rewriting by the premise, so we add it to
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   368
{\tt add_ss}:\footnote{The previous
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   369
  simplifier required congruence rules for function variables like~$f$ in
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   370
  order to simplify their arguments.  The present simplifier can be given
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   371
  congruence rules to realize non-standard simplification of a function's
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   372
  arguments, but this is seldom necessary.}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
by (asm_simp_tac (add_ss addsimps [prem]) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   380
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   381
\section{Setting up the simplifier}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   382
\index{simplification!setting up|bold}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   383
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   384
Setting up the simplifier for new logics is complicated.  This section
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   385
describes how the simplifier is installed for first-order logic; the code
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   386
is largely taken from {\tt FOL/simpdata.ML}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   387
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   388
The simplifier and the case splitting tactic, which resides in a separate
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   389
file, are not part of Pure Isabelle.  They must be loaded explicitly:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   390
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   391
use "../Provers/simplifier.ML";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   392
use "../Provers/splitter.ML";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   393
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   394
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   395
Simplification works by reducing various object-equalities to
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   396
meta-equality.  It requires axioms stating that equal terms and equivalent
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   397
formulae are also equal at the meta-level.  The file {\tt FOL/ifol.thy}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   398
contains the two lines
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   399
\begin{ttbox}\indexbold{*eq_reflection}\indexbold{*iff_reflection}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   400
eq_reflection   "(x=y)   ==> (x==y)"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   401
iff_reflection  "(P<->Q) ==> (P==Q)"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   402
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   403
Of course, you should only assert such axioms if they are true for your
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   404
particular logic.  In Constructive Type Theory, equality is a ternary
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   405
relation of the form $a=b\in A$; the type~$A$ determines the meaning of the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   406
equality effectively as a partial equivalence relation.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   407
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   408
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   409
\subsection{A collection of standard rewrite rules}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   410
The file begins by proving lots of standard rewrite rules about the logical
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   411
connectives.  These include cancellation laws and associative laws but
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   412
certainly not commutative laws, which would case looping.  To prove the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   413
laws easily, it defines a function that echoes the desired law and then
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   414
supplies it the theorem prover for intuitionistic \FOL:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   415
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   416
fun int_prove_fun s = 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   417
 (writeln s;  
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   418
  prove_goal IFOL.thy s
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   419
   (fn prems => [ (cut_facts_tac prems 1), 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   420
                  (Int.fast_tac 1) ]));
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   421
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   422
The following rewrite rules about conjunction are a selection of those
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   423
proved on {\tt FOL/simpdata.ML}.  Later, these will be supplied to the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   424
standard simpset.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   425
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   426
val conj_rews = map int_prove_fun
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   427
 ["P & True <-> P",      "True & P <-> P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   428
  "P & False <-> False", "False & P <-> False",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   429
  "P & P <-> P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   430
  "P & ~P <-> False",    "~P & P <-> False",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   431
  "(P & Q) & R <-> P & (Q & R)"];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   432
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   433
The file also proves some distributive laws.  As they can cause exponential
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   434
blowup, they will not be included in the standard simpset.  Instead they
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   435
are merely bound to an \ML{} identifier.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   436
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   437
val distrib_rews  = map int_prove_fun
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   438
 ["P & (Q | R) <-> P&Q | P&R", 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   439
  "(Q | R) & P <-> Q&P | R&P",
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   440
  "(P | Q --> R) <-> (P --> R) & (Q --> R)"];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   441
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   442
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   443
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   444
\subsection{Functions for preprocessing the rewrite rules}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   445
The next step is to define the function for preprocessing rewrite rules.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   446
This will be installed by calling {\tt setmksimps} below.  Preprocessing
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   447
occurs whenever rewrite rules are added, whether by user command or
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   448
automatically.  Preprocessing involves extracting atomic rewrites at the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   449
object-level, then reflecting them to the meta-level.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   450
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   451
To start, the function {\tt gen_all} strips any meta-level
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   452
quantifiers from the front of the given theorem.  Usually there are none
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   453
anyway.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   454
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   455
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   456
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   457
The function {\tt atomize} analyses a theorem in order to extract
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   458
atomic rewrite rules.  The head of all the patterns, matched by the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   459
wildcard~{\tt _}, is the coercion function {\tt Trueprop}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   460
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   461
fun atomize th = case concl_of th of 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   462
    _ $ (Const("op &",_) $ _ $ _)   => atomize(th RS conjunct1) \at
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   463
                                       atomize(th RS conjunct2)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   464
  | _ $ (Const("op -->",_) $ _ $ _) => atomize(th RS mp)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   465
  | _ $ (Const("All",_) $ _)        => atomize(th RS spec)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   466
  | _ $ (Const("True",_))           => []
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   467
  | _ $ (Const("False",_))          => []
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   468
  | _                               => [th];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   469
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   470
There are several cases, depending upon the form of the conclusion:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   471
\begin{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   472
\item Conjunction: extract rewrites from both conjuncts.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   473
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   474
\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
   475
  extract rewrites from~$Q$; these will be conditional rewrites with the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   476
  condition~$P$.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   477
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   478
\item Universal quantification: remove the quantifier, replacing the bound
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   479
  variable by a schematic variable, and extract rewrites from the body.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   480
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   481
\item {\tt True} and {\tt False} contain no useful rewrites.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   482
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   483
\item Anything else: return the theorem in a singleton list.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   484
\end{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   485
The resulting theorems are not literally atomic --- they could be
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   486
disjunctive, for example --- but are brokwn down as much as possible.  See
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   487
the file {\tt ZF/simpdata.ML} for a sophisticated translation of
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   488
set-theoretic formulae into rewrite rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   490
The simplified rewrites must now be converted into meta-equalities.  The
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   491
axiom {\tt eq_reflection} converts equality rewrites, while {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   492
  iff_reflection} converts if-and-only-if rewrites.  The latter possibility
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   493
can arise in two other ways: the negative theorem~$\neg P$ is converted to
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   494
$P\equiv{\tt False}$, and any other theorem~$\neg P$ is converted to
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   495
$P\equiv{\tt True}$.  The rules {\tt iff_reflection_F} and {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   496
  iff_reflection_T} accomplish this conversion.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   497
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   498
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   499
val iff_reflection_F = P_iff_F RS iff_reflection;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   500
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   501
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   502
val iff_reflection_T = P_iff_T RS iff_reflection;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   503
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   504
The function {\tt mk_meta_eq} converts a theorem to a meta-equality
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   505
using the case analysis described above.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   506
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   507
fun mk_meta_eq th = case concl_of th of
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   508
    _ $ (Const("op =",_)$_$_)   => th RS eq_reflection
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   509
  | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   510
  | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   511
  | _                           => th RS iff_reflection_T;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   512
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   513
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
   514
be composed together and supplied below to {\tt setmksimps}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   515
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   516
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   517
\subsection{Making the initial simpset}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   518
It is time to assemble these items.  We open module {\tt Simplifier} to
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   519
gain access to its components.  The infix operator \ttindexbold{addcongs}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   520
handles congruence rules; given a list of theorems, it converts their
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   521
conclusions into meta-equalities and passes them to \ttindex{addeqcongs}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   522
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   523
open Simplifier;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   524
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   525
infix addcongs;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   526
fun ss addcongs congs =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   527
    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   528
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   529
The list {\tt IFOL_rews} contains the default rewrite rules for first-order
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   530
logic.  The first of these is the reflexive law expressed as the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   531
equivalence $(a=a)\bimp{\tt True}$; if we provided it as $a=a$ it would
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   532
cause looping.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   533
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   534
val IFOL_rews =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   535
   [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
   536
    imp_rews \at iff_rews \at quant_rews;
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   537
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   538
The list {\tt triv_rls} contains trivial theorems for the solver.  Any
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   539
subgoal that is simplified to one of these will be removed.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   540
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   541
val notFalseI = int_prove_fun "~False";
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   542
val triv_rls = [TrueI,refl,iff_refl,notFalseI];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   543
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   544
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   545
The basic simpset for intuitionistic \FOL{} starts with \ttindex{empty_ss}.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   546
It preprocess rewrites using {\tt gen_all}, {\tt atomize} and {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   547
  mk_meta_eq}.  It solves simplified subgoals using {\tt triv_rls} and
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   548
assumptions.  It uses \ttindex{asm_simp_tac} to tackle subgoals of
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   549
conditional rewrites.  It takes {\tt IFOL_rews} as rewrite rules.  
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   550
Other simpsets built from {\tt IFOL_ss} will inherit these items.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   551
\index{*setmksimps}\index{*setsolver}\index{*setsubgoaler}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   552
\index{*addsimps}\index{*addcongs}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   553
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   554
val IFOL_ss = 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   555
  empty_ss 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   556
  setmksimps (map mk_meta_eq o atomize o gen_all)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   557
  setsolver  (fn prems => resolve_tac (triv_rls \at prems) ORELSE' 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   558
                          assume_tac)
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   559
  setsubgoaler asm_simp_tac
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   560
  addsimps IFOL_rews
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   561
  addcongs [imp_cong];
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   562
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   563
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
   564
contextual information to simplify the conclusions of implications:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   565
\[ \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
   566
   (\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   567
\]
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   568
By adding the congruence rule {\tt conj_cong}, we could obtain a similar
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   569
effect for conjunctions.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   570
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   571
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   572
\subsection{Case splitting}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   573
To set up case splitting, we must prove a theorem of the form shown below
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   574
and pass it to \ttindexbold{mk_case_split_tac}.  The tactic
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   575
\ttindexbold{split_tac} uses {\tt mk_meta_eq} to convert the splitting
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   576
rules to meta-equalities.
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   577
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   578
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   579
val meta_iffD = 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   580
    prove_goal FOL.thy "[| P==Q; Q |] ==> P"
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   581
        (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1])
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   582
\ttbreak
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   583
fun split_tac splits =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   584
    mk_case_split_tac meta_iffD (map mk_meta_eq splits);
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
%
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   587
The splitter is designed for rules roughly of the form
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   588
\[ \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
   589
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   590
\] 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   591
where the right-hand side can be anything.  Another example is the
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   592
elimination operator (which happens to be called~$split$) for Cartesian
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   593
products:
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   594
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   595
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   596
\] 
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   597
Case splits should be allowed only when necessary; they are expensive
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   598
and hard to control.  Here is a typical example of use, where {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   599
  expand_if} is the first rule above:
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
by (simp_tac (prop_rec_ss setloop (split_tac [expand_if])) 1);
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   602
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   603
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\index{simplification|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
286
e7efbf03562b first draft of Springer book
lcp
parents: 133
diff changeset
   608