doc-src/Ref/simp.tex
author wenzelm
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 1100 74921c7613e7
child 9695 ec7d7f877712
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%%%THIS DOCUMENTS THE OBSOLETE SIMPLIFIER!!!!
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
Object-level rewriting is not primitive in Isabelle.  For efficiency,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
perhaps it ought to be.  On the other hand, it is difficult to conceive of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
a general mechanism that could accommodate the diversity of rewriting found
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
in different logics.  Hence rewriting in Isabelle works via resolution,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
using unknowns as place-holders for simplified terms.  This chapter
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
describes a generic simplification package, the functor~\ttindex{SimpFun},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
which expects the basic laws of equational logic and returns a suite of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
simplification tactics.  The code lives in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
\verb$Provers/simp.ML$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
This rewriting package is not as general as one might hope (using it for {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
HOL} is not quite as convenient as it could be; rewriting modulo equations is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
not supported~\ldots) but works well for many logics.  It performs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
conditional and unconditional rewriting and handles multiple reduction
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
relations and local assumptions.  It also has a facility for automatic case
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
splits by expanding conditionals like {\it if-then-else\/} during rewriting.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
For many of Isabelle's logics ({\tt FOL}, {\tt ZF}, {\tt LCF} and {\tt HOL})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
the simplifier has been set up already. Hence we start by describing the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
functions provided by the simplifier --- those functions exported by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
\ttindex{SimpFun} through its result signature \ttindex{SIMP} shown in
286
e7efbf03562b first draft of Springer book
lcp
parents: 104
diff changeset
    25
Fig.\ts\ref{SIMP}.  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\section{Simplification sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\index{simplification sets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
The simplification tactics are controlled by {\bf simpsets}, which consist of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
three things:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
\begin{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
\item {\bf Rewrite rules}, which are theorems like 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
$\Var{m} + succ(\Var{n}) = succ(\Var{m} + \Var{n})$.  {\bf Conditional}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
rewrites such as $m<n \Imp m/n = 0$ are permitted.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\index{rewrite rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\item {\bf Congruence rules}, which typically have the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\index{congruence rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\[ \List{\Var{x@1} = \Var{y@1}; \ldots; \Var{x@n} = \Var{y@n}} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
   f(\Var{x@1},\ldots,\Var{x@n}) = f(\Var{y@1},\ldots,\Var{y@n}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\item The {\bf auto-tactic}, which attempts to solve the simplified
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
subgoal, say by recognizing it as a tautology.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\end{enumerate}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\subsection{Congruence rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
Congruence rules enable the rewriter to simplify subterms.  Without a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
congruence rule for the function~$g$, no argument of~$g$ can be rewritten.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
Congruence rules can be generalized in the following ways:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
{\bf Additional assumptions} are allowed:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\[ \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
    55
   \Imp (\Var{P@1} \imp \Var{P@2}) \bimp (\Var{Q@1} \imp \Var{Q@2})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
This rule assumes $Q@1$, and any rewrite rules it contains, while
1100
74921c7613e7 trivial change
lcp
parents: 323
diff changeset
    58
simplifying~$P@2$.  Such `local' assumptions are effective for rewriting
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
formulae such as $x=0\imp y+x=y$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
{\bf Additional quantifiers} are allowed, typically for binding operators:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\[ \List{\Forall z. \Var{P}(z) \bimp \Var{Q}(z)} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
   \forall x.\Var{P}(x) \bimp \forall x.\Var{Q}(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
{\bf Different equalities} can be mixed.  The following example
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
enables the transition from formula rewriting to term rewriting:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
\[ \List{\Var{x@1}=\Var{y@1};\Var{x@2}=\Var{y@2}} \Imp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
   (\Var{x@1}=\Var{x@2}) \bimp (\Var{y@1}=\Var{y@2})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
It is not necessary to assert a separate congruence rule for each constant,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
provided your logic contains suitable substitution rules. The function {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
mk_congs} derives congruence rules from substitution
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
rules~\S\ref{simp-tactics}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
\begin{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\indexbold{*SIMP}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
infix 4 addrews addcongs delrews delcongs setauto;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
signature SIMP =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
  type simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
  val empty_ss  : simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
  val addcongs  : simpset * thm list -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
  val addrews   : simpset * thm list -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
  val delcongs  : simpset * thm list -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
  val delrews   : simpset * thm list -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
  val print_ss  : simpset -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
  val setauto   : simpset * (int -> tactic) -> simpset
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
  val ASM_SIMP_CASE_TAC : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
  val ASM_SIMP_TAC      : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
  val CASE_TAC          : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
  val SIMP_CASE2_TAC    : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
  val SIMP_THM          : simpset -> thm -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
  val SIMP_TAC          : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
  val SIMP_CASE_TAC     : simpset -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
  val mk_congs          : theory -> string list -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
  val mk_typed_congs    : theory -> (string*string) list -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
  val tracing   : bool ref
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\caption{The signature {\tt SIMP}} \label{SIMP}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\subsection{The abstract type {\tt simpset}}\label{simp-simpsets}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
Simpsets are values of the abstract type \ttindexbold{simpset}.  They are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
manipulated by the following functions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\index{simplification sets|bold}
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   113
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
\item[\ttindexbold{empty_ss}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
is the empty simpset.  It has no congruence or rewrite rules and its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
auto-tactic always fails.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   118
\item[$ss$ \ttindexbold{addcongs} $thms$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
is the simpset~$ss$ plus the congruence rules~$thms$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   121
\item[$ss$ \ttindexbold{delcongs} $thms$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
is the simpset~$ss$ minus the congruence rules~$thms$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   124
\item[$ss$ \ttindexbold{addrews} $thms$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
is the simpset~$ss$ plus the rewrite rules~$thms$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   127
\item[$ss$ \ttindexbold{delrews} $thms$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
is the simpset~$ss$ minus the rewrite rules~$thms$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   130
\item[$ss$ \ttindexbold{setauto} $tacf$] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
is the simpset~$ss$ with $tacf$ for its auto-tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\item[\ttindexbold{print_ss} $ss$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
prints all the congruence and rewrite rules in the simpset~$ss$.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   135
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
Adding a rule to a simpset already containing it, or deleting one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
from a simpset not containing it, generates a warning message.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
In principle, any theorem can be used as a rewrite rule.  Before adding a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
theorem to a simpset, {\tt addrews} preprocesses the theorem to extract the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
maximum amount of rewriting from it.  Thus it need not have the form $s=t$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
In {\tt FOL} for example, an atomic formula $P$ is transformed into the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
rewrite rule $P \bimp True$.  This preprocessing is not fixed but logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
dependent.  The existing logics like {\tt FOL} are fairly clever in this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
respect.  For a more precise description see {\tt mk_rew_rules} in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\S\ref{SimpFun-input}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
The auto-tactic is applied after simplification to solve a goal.  This may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
be the overall goal or some subgoal that arose during conditional
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
rewriting.  Calling ${\tt auto_tac}~i$ must either solve exactly
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
subgoal~$i$ or fail.  If it succeeds without reducing the number of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
subgoals by one, havoc and strange exceptions may result.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
A typical auto-tactic is {\tt ares_tac [TrueI]}, which attempts proof by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
assumption and resolution with the theorem $True$.  In explicitly typed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
logics, the auto-tactic can be used to solve simple type checking
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
obligations.  Some applications demand a sophisticated auto-tactic such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
{\tt fast_tac}, but this could make simplification slow.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
Rewriting never instantiates unknowns in subgoals.  (It uses
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\ttindex{match_tac} rather than \ttindex{resolve_tac}.)  However, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
auto-tactic is permitted to instantiate unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
\section{The simplification tactics} \label{simp-tactics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
\index{simplification!tactics|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
\index{tactics!simplification|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
The actual simplification work is performed by the following tactics.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
rewriting strategy is strictly bottom up.  Conditions in conditional rewrite
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
rules are solved recursively before the rewrite rule is applied.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
There are two basic simplification tactics:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   174
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\item[\ttindexbold{SIMP_TAC} $ss$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
simplifies subgoal~$i$ using the rules in~$ss$.  It may solve the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
subgoal completely if it has become trivial, using the auto-tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
(\S\ref{simp-simpsets}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\item[\ttindexbold{ASM_SIMP_TAC}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
is like \verb$SIMP_TAC$, but also uses assumptions as additional
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
rewrite rules.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   183
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
Many logics have conditional operators like {\it if-then-else}.  If the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
simplifier has been set up with such case splits (see~\ttindex{case_splits}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
in \S\ref{SimpFun-input}), there are tactics which automatically alternate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
between simplification and case splitting:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   188
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\item[\ttindexbold{SIMP_CASE_TAC}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
is like {\tt SIMP_TAC} but also performs automatic case splits.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
More precisely, after each simplification phase the tactic tries to apply a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
theorem in \ttindex{case_splits}.  If this succeeds, the tactic calls
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
itself recursively on the result.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
\item[\ttindexbold{ASM_SIMP_CASE_TAC}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
is like {\tt SIMP_CASE_TAC}, but also uses assumptions for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
rewriting.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\item[\ttindexbold{SIMP_CASE2_TAC}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
is like {\tt SIMP_CASE_TAC}, but also tries to solve the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
pre-conditions of conditional simplification rules by repeated case splits.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
\item[\ttindexbold{CASE_TAC}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
tries to break up a goal using a rule in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\ttindex{case_splits}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\item[\ttindexbold{SIMP_THM}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
simplifies a theorem using assumptions and case splitting.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   209
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
Finally there are two useful functions for generating congruence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
rules for constants and free variables:
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   212
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\item[\ttindexbold{mk_congs} $thy$ $cs$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
computes a list of congruence rules, one for each constant in $cs$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
Remember that the name of an infix constant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\verb$+$ is \verb$op +$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\item[\ttindexbold{mk_typed_congs}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
computes congruence rules for explicitly typed free variables and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
constants.  Its second argument is a list of name and type pairs.  Names
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
can be either free variables like {\tt P}, or constants like \verb$op =$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
For example in {\tt FOL}, the pair
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\verb$("f","'a => 'a")$ generates the rule \verb$?x = ?y ==> f(?x) = f(?y)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
Such congruence rules are necessary for goals with free variables whose
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
arguments need to be rewritten.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   226
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
Both functions work correctly only if {\tt SimpFun} has been supplied with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
necessary substitution rules.  The details are discussed in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
\S\ref{SimpFun-input} under {\tt subst_thms}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
Using the simplifier effectively may take a bit of experimentation. In
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
particular it may often happen that simplification stops short of what you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
expected or runs forever. To diagnose these problems, the simplifier can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
traced. The reference variable \ttindexbold{tracing} controls the output of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
tracing information.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\index{tracing!of simplification}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\section{Example: using the simplifier}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\index{simplification!example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
Assume we are working within {\tt FOL} and that
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   243
\begin{ttdescription}
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   244
\item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   245
\item[add_0] is the rewrite rule $0+n = n$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   246
\item[add_Suc] is the rewrite rule $Suc(m)+n = Suc(m+n)$,
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   247
\item[induct] is the induction rule
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
$\List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n)$.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   249
\item[FOL_ss] is a basic simpset for {\tt FOL}.
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   250
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
We generate congruence rules for $Suc$ and for the infix operator~$+$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
prths nat_congs;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
{\out ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
{\out [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
We create a simpset for natural numbers by extending~{\tt FOL_ss}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
val add_ss = FOL_ss  addcongs nat_congs  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
                     addrews  [add_0, add_Suc];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
Proofs by induction typically involve simplification:\footnote
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
{These examples reside on the file {\tt FOL/ex/nat.ML}.} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
goal Nat.thy "m+0 = m";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
{\out  1. m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\ttbreak
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
{\out  1. 0 + 0 = 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
{\out  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
Simplification solves the first subgoal:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
by (SIMP_TAC add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
{\out  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
The remaining subgoal requires \ttindex{ASM_SIMP_TAC} in order to use the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
induction hypothesis as a rewrite rule:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
by (ASM_SIMP_TAC add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
{\out m + 0 = m}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
The next proof is similar.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
goal Nat.thy "m+Suc(n) = Suc(m+n)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
{\out  1. m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
\ttbreak
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
{\out  1. 0 + Suc(n) = Suc(0 + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
{\out  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
Using the tactical \ttindex{ALLGOALS}, a single command simplifies all the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
subgoals:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
by (ALLGOALS (ASM_SIMP_TAC add_ss));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
{\out m + Suc(n) = Suc(m + n)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
Some goals contain free function variables.  The simplifier must have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
congruence rules for those function variables, or it will be unable to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
simplify their arguments:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
val f_congs = mk_typed_congs Nat.thy [("f","nat => nat")];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
val f_ss = add_ss addcongs f_congs;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
prths f_congs;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
{\out ?Xa = ?Ya ==> f(?Xa) = f(?Ya)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
Here is a conjecture to be proved for an arbitrary function~$f$ satisfying
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
the law $f(Suc(n)) = Suc(f(n))$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
val [prem] = goal Nat.thy
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
    "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
{\out  1. f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
\ttbreak
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
by (res_inst_tac [("n","i")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
{\out  1. f(0 + j) = 0 + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
{\out  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
We simplify each subgoal in turn.  The first one is trivial:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
by (SIMP_TAC f_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
{\out  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
The remaining subgoal requires rewriting by the premise, shown
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
below, so we add it to {\tt f_ss}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
prth prem;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
{\out f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
by (ASM_SIMP_TAC (f_ss addrews [prem]) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
{\out f(i + j) = i + f(j)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\section{Setting up the simplifier} \label{SimpFun-input}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
\index{simplification!setting up|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
To set up a simplifier for a new logic, the \ML\ functor
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
\ttindex{SimpFun} needs to be supplied with theorems to justify
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
rewriting.  A rewrite relation must be reflexive and transitive; symmetry
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
is not necessary.  Hence the package is also applicable to non-symmetric
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
relations such as occur in operational semantics.  In the sequel, $\gg$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
denotes some {\bf reduction relation}: a binary relation to be used for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
rewriting.  Several reduction relations can be used at once.  In {\tt FOL},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
both $=$ (on terms) and $\bimp$ (on formulae) can be used for rewriting.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
The argument to {\tt SimpFun} is a structure with signature
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
\ttindexbold{SIMP_DATA}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
signature SIMP_DATA =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
  val case_splits  : (thm * string) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
  val dest_red     : term -> term * term * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
  val mk_rew_rules : thm -> thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
  val norm_thms    : (thm*thm) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
  val red1         : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
  val red2         : thm 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
  val refl_thms    : thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
  val subst_thms   : thm list 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
  val trans_thms   : thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
The components of {\tt SIMP_DATA} need to be instantiated as follows.  Many
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
of these components are lists, and can be empty.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   385
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\item[\ttindexbold{refl_thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
supplies reflexivity theorems of the form $\Var{x} \gg
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\Var{x}$.  They must not have additional premises as, for example,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
$\Var{x}\in\Var{A} \Imp \Var{x} = \Var{x}\in\Var{A}$ in type theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\item[\ttindexbold{trans_thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
supplies transitivity theorems of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
$\List{\Var{x}\gg\Var{y}; \Var{y}\gg\Var{z}} \Imp {\Var{x}\gg\Var{z}}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
\item[\ttindexbold{red1}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
is a theorem of the form $\List{\Var{P}\gg\Var{Q};
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\Var{P}} \Imp \Var{Q}$, where $\gg$ is a relation between formulae, such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
$\bimp$ in {\tt FOL}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
\item[\ttindexbold{red2}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
is a theorem of the form $\List{\Var{P}\gg\Var{Q};
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\Var{Q}} \Imp \Var{P}$, where $\gg$ is a relation between formulae, such as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
$\bimp$ in {\tt FOL}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
\item[\ttindexbold{mk_rew_rules}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
is a function that extracts rewrite rules from theorems.  A rewrite rule is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
a theorem of the form $\List{\ldots}\Imp s \gg t$.  In its simplest form,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
{\tt mk_rew_rules} maps a theorem $t$ to the singleton list $[t]$.  More
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
sophisticated versions may do things like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\[
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
\begin{array}{l@{}r@{\quad\mapsto\quad}l}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
\mbox{create formula rewrites:}& P & [P \bimp True] \\[.5ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
\mbox{remove negations:}& \lnot P & [P \bimp False] \\[.5ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\mbox{create conditional rewrites:}& P\imp s\gg t & [P\Imp s\gg t] \\[.5ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\mbox{break up conjunctions:}& 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
        (s@1 \gg@1 t@1) \conj (s@2 \gg@2 t@2) & [s@1 \gg@1 t@1, s@2 \gg@2 t@2]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
The more theorems are turned into rewrite rules, the better.  The function
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
is used in two places:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\item 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
$ss$~\ttindex{addrews}~$thms$ applies {\tt mk_rew_rules} to each element of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
$thms$ before adding it to $ss$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
\item 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
simplification with assumptions (as in \ttindex{ASM_SIMP_TAC}) uses
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
{\tt mk_rew_rules} to turn assumptions into rewrite rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
\item[\ttindexbold{case_splits}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
supplies expansion rules for case splits.  The simplifier is designed
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
for rules roughly of the kind
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
\conj (\lnot\Var{Q} \imp \Var{P}(\Var{y})) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
but is insensitive to the form of the right-hand side.  Other examples
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
include product types, where $split ::
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
(\alpha\To\beta\To\gamma)\To\alpha*\beta\To\gamma$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
{<}a,b{>} \imp \Var{P}(\Var{f}(a,b))) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
Each theorem in the list is paired with the name of the constant being
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
eliminated, {\tt"if"} and {\tt"split"} in the examples above.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\item[\ttindexbold{norm_thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
supports an optimization.  It should be a list of pairs of rules of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
form $\Var{x} \gg norm(\Var{x})$ and $norm(\Var{x}) \gg \Var{x}$.  These
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
introduce and eliminate {\tt norm}, an arbitrary function that should be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
used nowhere else.  This function serves to tag subterms that are in normal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
form.  Such rules can speed up rewriting significantly!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
\item[\ttindexbold{subst_thms}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
supplies substitution rules of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
\[ \List{\Var{x} \gg \Var{y}; \Var{P}(\Var{x})} \Imp \Var{P}(\Var{y}) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
They are used to derive congruence rules via \ttindex{mk_congs} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
\ttindex{mk_typed_congs}.  If $f :: [\tau@1,\cdots,\tau@n]\To\tau$ is a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
constant or free variable, the computation of a congruence rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
\[\List{\Var{x@1} \gg@1 \Var{y@1}; \ldots; \Var{x@n} \gg@n \Var{y@n}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
\Imp f(\Var{x@1},\ldots,\Var{x@n}) \gg f(\Var{y@1},\ldots,\Var{y@n}) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
requires a reflexivity theorem for some reduction ${\gg} ::
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
\alpha\To\alpha\To\sigma$ such that $\tau$ is an instance of $\alpha$.  If a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
suitable reflexivity law is missing, no congruence rule for $f$ can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
generated.   Otherwise an $n$-ary congruence rule of the form shown above is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
derived, subject to the availability of suitable substitution laws for each
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
argument position.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
A substitution law is suitable for argument $i$ if it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
uses a reduction ${\gg@i} :: \alpha@i\To\alpha@i\To\sigma@i$ such that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
$\tau@i$ is an instance of $\alpha@i$.  If a suitable substitution law for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
argument $i$ is missing, the $i^{th}$ premise of the above congruence rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
cannot be generated and hence argument $i$ cannot be rewritten.  In the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
worst case, if there are no suitable substitution laws at all, the derived
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
congruence simply degenerates into a reflexivity law.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
\item[\ttindexbold{dest_red}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
takes reductions apart.  Given a term $t$ representing the judgement
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
\mbox{$a \gg b$}, \verb$dest_red$~$t$ should return a triple $(c,ta,tb)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
where $ta$ and $tb$ represent $a$ and $b$, and $c$ is a term of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
\verb$Const(_,_)$, the reduction constant $\gg$.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
Suppose the logic has a coercion function like $Trueprop::o\To prop$, as do
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
{\tt FOL} and~{\tt HOL}\@.  If $\gg$ is a binary operator (not necessarily
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
infix), the following definition does the job:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
\begin{verbatim}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
   fun dest_red( _ $ (c $ ta $ tb) ) = (c,ta,tb);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\end{verbatim}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
The wildcard pattern {\tt_} matches the coercion function.
323
361a71713176 penultimate Springer draft
lcp
parents: 286
diff changeset
   488
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\section{A sample instantiation}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
Here is the instantiation of {\tt SIMP_DATA} for {\FOL}.  The code for {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
structure FOL_SimpData : SIMP_DATA =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
  struct
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
  val refl_thms      = [ \(\Var{x}=\Var{x}\), \(\Var{P}\bimp\Var{P}\) ]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
  val trans_thms     = [ \(\List{\Var{x}=\Var{y};\Var{y}=\Var{z}}\Imp\Var{x}=\Var{z}\),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
                         \(\List{\Var{P}\bimp\Var{Q};\Var{Q}\bimp\Var{R}}\Imp\Var{P}\bimp\Var{R}\) ]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
  val red1           = \(\List{\Var{P}\bimp\Var{Q}; \Var{P}} \Imp \Var{Q}\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
  val red2           = \(\List{\Var{P}\bimp\Var{Q}; \Var{Q}} \Imp \Var{P}\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
  val mk_rew_rules   = ...
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
  val case_splits    = [ \(\Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
                           \((\Var{Q} \imp \Var{P}(\Var{x})) \conj (\lnot\Var{Q} \imp \Var{P}(\Var{y}))\) ]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
  val norm_thms      = [ (\(\Var{x}=norm(\Var{x})\),\(norm(\Var{x})=\Var{x}\)),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
                        (\(\Var{P}\bimp{}NORM(\Var{P}\)), \(NORM(\Var{P})\bimp\Var{P}\)) ]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
  val subst_thms     = [ \(\List{\Var{x}=\Var{y}; \Var{P}(\Var{x})}\Imp\Var{P}(\Var{y})\) ]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
  val dest_red       = fn (_ $ (opn $ lhs $ rhs)) => (opn,lhs,rhs)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
  end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
\index{simplification|)}