doc-src/Ref/substitution.tex
author lcp
Wed, 10 Nov 1993 05:00:57 +0100
changeset 104 d8205bb279a7
child 148 67d046de093e
permissions -rw-r--r--
Initial revision
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{Substitution Tactics} \label{substitution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{substitution|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
Replacing equals by equals is a basic form of reasoning.  Isabelle supports
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
several kinds of equality reasoning.  {\bf Substitution} means to replace
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
free occurrences of~$t$ by~$u$ in a subgoal.  This is easily done, given an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
equality $t=u$, provided the logic possesses the appropriate rule ---
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
unless you want to substitute even in the assumptions.  The tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\ttindex{hyp_subst_tac} performs substitution in the assumptions, but it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
works via object-level implication, and therefore must be specially set up
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
for each suitable object-logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
Substitution should not be confused with object-level {\bf rewriting}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
corresponding instances of~$u$, and continues until it reaches a normal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
form.  Substitution handles `one-off' replacements by particular
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
equalities, while rewriting handles general equalities.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\section{Simple substitution}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\index{substitution!simple}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
Many logics include a substitution rule of the form\indexbold{*subst}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
   \Var{P}(\Var{b})  \eqno(subst)$$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
In backward proof, this may seem difficult to use: the conclusion
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
$\Var{P}(\Var{b})$ admits far too many unifiers.  But, if the theorem {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\[ \Var{P}(t) \Imp \Var{P}(u). \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
Provided $u$ is not an unknown, resolution with this rule is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
expresses~$Q$ in terms of its dependence upon~$u$.  There are still $2^k$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
subgoal~$i$, use
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
resolve_tac [eqth RS subst] \(i\) {\it.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
To replace $t$ by~$u$ in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
subgoal~$i$, use
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
resolve_tac [eqth RS ssubst] \(i\) {\it,}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
where \ttindexbold{ssubst} is the `swapped' substitution rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
$$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
   \Var{P}(\Var{a}).  \eqno(ssubst)$$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
If \ttindex{sym} denotes the symmetry rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then {\tt ssubst} is just
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
\hbox{\tt sym RS subst}.  Many logics with equality include the rules {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
subst} and {\tt ssubst}, as well as {\tt refl}, {\tt sym} and {\tt trans}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
(for the usual equality laws).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
Elim-resolution is well-behaved with assumptions of the form $t=u$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
eresolve_tac [subst] \(i\)    {\it or}    eresolve_tac [ssubst] \(i\) {\it.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\section{Substitution in the hypotheses}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
\index{substitution!in hypotheses}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
Substitution rules, like other rules of natural deduction, do not affect
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
the assumptions.  This can be inconvenient.  Consider proving the subgoal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
\[ \List{c=a; c=b} \Imp a=b. \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
Calling \hbox{\tt eresolve_tac [ssubst] \(i\)} simply discards the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
assumption~$c=a$, since $c$ does not occur in~$a=b$.  Of course, we can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
work out a solution.  First apply \hbox{\tt eresolve_tac [subst] \(i\)},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
replacing~$a$ by~$c$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\[ \List{c=b} \Imp c=b \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
Equality reasoning can be difficult, but this trivial proof requires
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
nothing more sophisticated than substitution in the assumptions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
Object-logics that include the rule~$(subst)$ provide a tactic for this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
purpose:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
hyp_subst_tac : int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\item[\ttindexbold{hyp_subst_tac} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
free variable or parameter.  Deleting this assumption, it replaces $t$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
by~$u$ throughout subgoal~$i$, including the other assumptions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
The term being replaced must be a free variable or parameter.  Substitution
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
for constants is usually unhelpful, since they may appear in other
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
theorems.  For instance, the best way to use the assumption $0=1$ is to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
in the subgoal!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
Replacing a free variable causes similar problems if they appear in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
premises of a rule being derived --- the substitution affects object-level
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
assumptions, not meta-level assumptions.  For instance, replacing~$a$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, call
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\ttindex{cut_facts_tac} to insert the atomic premises as object-level
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
assumptions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\section{Setting up {\tt hyp_subst_tac}} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
Many Isabelle object-logics, such as {\tt FOL}, {\tt HOL} and their
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
descendants, come with {\tt hyp_subst_tac} already defined.  A few others,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
such as {\tt CTT}, do not support this tactic because they lack the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
rule~$(subst)$.  When defining a new logic that includes a substitution
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
rule and implication, you must set up {\tt hyp_subst_tac} yourself.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
argument signature~\ttindexbold{HYPSUBST_DATA}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
signature HYPSUBST_DATA =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
  sig
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
  val subst      : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
  val sym        : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
  val rev_cut_eq : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
  val imp_intr   : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
  val rev_mp     : thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
  val dest_eq    : term -> term*term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
  end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
Thus, the functor requires the following items:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\item[\ttindexbold{subst}] should be the substitution rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
\item[\ttindexbold{sym}] should be the symmetry rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
\item[\ttindexbold{rev_cut_eq}] should have the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
$\List{\Var{a}=\Var{b};\; \Var{a}=\Var{b}\Imp\Var{R}} \Imp \Var{R}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
\item[\ttindexbold{imp_intr}] should be the implies introduction
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\item[\ttindexbold{rev_mp}] should be the ``reversed'' implies elimination
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
rule $\List{\Var{P};  \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
applied to the \ML{} term that represents~$t=u$.  For other terms, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
should raise exception~\ttindex{Match}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
The functor resides in {\tt Provers/hypsubst.ML} on the Isabelle
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
distribution directory.  It is not sensitive to the precise formalization
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
of the object-logic.  It is not concerned with the names of the equality
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
and implication symbols, or the types of formula and terms.  Coding the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
function {\tt dest_eq} requires knowledge of Isabelle's representation of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
terms.  For {\tt FOL} it is defined by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_)$t$u)) = (t,u);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
Here {\tt Trueprop} is the coercion from type'~$o$ to type~$prop$, while
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
Pattern-matching expresses the function concisely, using wildcards~({\tt_})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
to hide the types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
Given a subgoal of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\ttindexbold{hyp_subst_tac} locates a suitable equality
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
assumption and moves it to the last position using elim-resolution on {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
rev_cut_eq} (possibly re-orienting it using~{\tt sym}):
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\[ \List{P@1; \cdots ; P@n; t=u} \Imp Q \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
Using $n$ calls of \hbox{\tt eresolve_tac [rev_mp]}, it creates the subgoal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\[ \List{t=u} \Imp P@1\imp \cdots \imp P@n \imp Q \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
By \hbox{\tt eresolve_tac [ssubst]}, it replaces~$t$ by~$u$ throughout:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
\[ P'@1\imp \cdots \imp P'@n \imp Q' \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
Finally, using $n$ calls of \hbox{\tt resolve_tac [imp_intr]}, it restores
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
$P'@1$, \ldots, $P'@n$ as assumptions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\[ \List{P'@n; \cdots ; P'@1} \Imp Q' \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
\index{substitution|)}