author paulson Wed, 11 May 2005 17:45:38 +0200 changeset 15952 ad9e27c1b2c8 parent 15951 63ac2e550040 child 15953 902b556e4bc0
documented new subst method
--- a/doc-src/TutorialI/Rules/rules.tex	Wed May 11 16:30:24 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed May 11 17:45:38 2005 +0200
@@ -705,12 +705,39 @@
Crucially, \isa{?P} is a function
variable.  It can be replaced by a $\lambda$-term
with one bound variable, whose occurrences identify the places
-in which $s$ will be replaced by~$t$.  The proof above requires
-the term \isa{{\isasymlambda}x.~x=s}.
+in which $s$ will be replaced by~$t$.  The proof above requires \isa{?P}
+to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then
+be \isa{s=s} and the conclusion will be \isa{t=s}.

-The \isa{simp} method replaces equals by equals, but the substitution
-rule gives us more control.  The \methdx{subst} method is the easiest way to
-use the substitution rule.  Suppose a
+The \isa{simp} method also replaces equals by equals, but the substitution
+rule gives us more control.  Consider this proof:
+\begin{isabelle}
+\isacommand{lemma}\
+"\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\
+odd\ x"\isanewline
+\isacommand{by}\ (erule\ ssubst)
+\end{isabelle}
+%
+The assumption \isa{x\ =\ f\ x}, if used for rewriting, would loop,
+replacing \isa{x} by \isa{f x} and then by
+\isa{f(f x)} and so forth. (Here \isa{simp}
+would see the danger and would re-orient the equality, but in more complicated
+cases it can be fooled.) When we apply the substitution rule,
+Isabelle replaces every
+\isa{x} in the subgoal by \isa{f x} just once. It cannot loop.  The
+resulting subgoal is trivial by assumption, so the \isacommand{by} command
+proves it implicitly.
+
+We are using the \isa{erule} method in a novel way. Hitherto,
+the conclusion of the rule was just a variable such as~\isa{?R}, but it may
+be any term. The conclusion is unified with the subgoal just as
+it would be with the \isa{rule} method. At the same time \isa{erule} looks
+for an assumption that matches the rule's first premise, as usual.  With
+\isa{ssubst} the effect is to find, use and delete an equality
+assumption.
+
+The \methdx{subst} method performs individual substitutions. In simple cases,
+it closely resembles a use of the substitution rule.  Suppose a
proof has reached this point:
\begin{isabelle}
\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y%
@@ -740,31 +767,15 @@
As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}.

\medskip
-The \isa{subst} method is convenient, but to see how it works, let us
-examine an explicit use of the rule \isa{ssubst}.
-Consider this proof:
+This use of the \methdx{subst} method has the same effect as the command
\begin{isabelle}
-\isacommand{lemma}\
-"\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\
-odd\ x"\isanewline
-\isacommand{by}\ (erule\ ssubst)
+\isacommand{apply}\ (rule\ mult_commute [THEN ssubst])
\end{isabelle}
-%
-The simplifier might loop, replacing \isa{x} by \isa{f x} and then by
-\isa{f(f x)} and so forth. (Here \isa{simp}
-can see the danger and would re-orient the equality, but in more complicated
-cases it can be fooled.) When we apply substitution,  Isabelle replaces every
-\isa{x} in the subgoal by \isa{f x} just once: it cannot loop.  The
-resulting subgoal is trivial by assumption, so the \isacommand{by} command
-proves it implicitly.
-
-We are using the \isa{erule} method in a novel way. Hitherto,
-the conclusion of the rule was just a variable such as~\isa{?R}, but it may
-be any term. The conclusion is unified with the subgoal just as
-it would be with the \isa{rule} method. At the same time \isa{erule} looks
-for an assumption that matches the rule's first premise, as usual.  With
-\isa{ssubst} the effect is to find, use and delete an equality
-assumption.
+The attribute \isa{THEN}, which combines two rules, is described in
+{\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than
+applying the substitution rule. It can perform substitutions in a subgoal's
+assumptions. Moreover, if the subgoal contains more than one occurrence of
+the left-hand side of the equality, the \methdx{subst} method lets us specify which occurrence should be replaced.

\subsection{Unification and Its Pitfalls}
@@ -1819,6 +1830,8 @@
\subsection{Modifying a Theorem using {\tt\slshape of},  {\tt\slshape where}
and {\tt\slshape THEN}}

+\label{sec:THEN}
+
Let us reproduce our examples in Isabelle.  Recall that in
{\S}\ref{sec:recdef-simplification} we declared the recursive function
\isa{gcd}:\index{*gcd (constant)|(}
@@ -1962,11 +1975,14 @@
\isa{[of "?k*m"]} will be rejected.
\end{warn}

-\begin{exercise}
-In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
-can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
-% answer  rule (mult_commute [THEN ssubst])
-\end{exercise}
+%Answer is now included in that section! Is a modified version of this
+%  exercise worth including? E.g. find a difference between the two ways
+%  of substituting.
+%\begin{exercise}
+%In {\S}\ref{sec:subst} the method \isa{subst\ mult_commute} was applied.  How
+%can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}?
+%% answer  rule (mult_commute [THEN ssubst])
+%\end{exercise}

\subsection{Modifying a Theorem using {\tt\slshape OF}}