doc-src/Ref/substitution.tex
 changeset 332 01b87a921967 parent 323 361a71713176 child 2038 26b62963806c
--- a/doc-src/Ref/substitution.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/substitution.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -3,19 +3,18 @@
\index{tactics!substitution|(}\index{equality|(}

Replacing equals by equals is a basic form of reasoning.  Isabelle supports
-several kinds of equality reasoning.  {\bf Substitution} means to replace
+several kinds of equality reasoning.  {\bf Substitution} means replacing
free occurrences of~$t$ by~$u$ in a subgoal.  This is easily done, given an
-equality $t=u$, provided the logic possesses the appropriate rule ---
-unless you want to substitute even in the assumptions.  The tactic
-{\tt hyp_subst_tac} performs substitution in the assumptions, but it
-works via object-level implication, and therefore must be specially set up
-for each suitable object-logic.
+equality $t=u$, provided the logic possesses the appropriate rule.  The
+tactic {\tt hyp_subst_tac} performs substitution even in the assumptions.
+But it works via object-level implication, and therefore must be specially
+set up for each suitable object-logic.

Substitution should not be confused with object-level {\bf rewriting}.
Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
corresponding instances of~$u$, and continues until it reaches a normal
form.  Substitution handles one-off' replacements by particular
-equalities, while rewriting handles general equalities.
+equalities while rewriting handles general equations.
Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.

@@ -35,12 +34,12 @@
the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in
subgoal~$i$, use
\begin{ttbox}
-resolve_tac [eqth RS subst] $$i$$ {\it.}
+resolve_tac [eqth RS subst] $$i$${\it.}
\end{ttbox}
To replace $t$ by~$u$ in
subgoal~$i$, use
\begin{ttbox}
-resolve_tac [eqth RS ssubst] $$i$$ {\it,}
+resolve_tac [eqth RS ssubst] $$i$${\it,}
\end{ttbox}
where \tdxbold{ssubst} is the swapped' substitution rule
 \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
@@ -55,7 +54,7 @@
Elim-resolution is well-behaved with assumptions of the form $t=u$.
To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
\begin{ttbox}
-eresolve_tac [subst] $$i$$    {\it or}    eresolve_tac [ssubst] $$i$$ {\it.}
+eresolve_tac [subst] $$i$$    {\rm or}    eresolve_tac [ssubst] $$i$${\it.}
\end{ttbox}

@@ -93,7 +92,7 @@
contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
in the subgoal!

-Replacing a free variable causes similar problems if they appear in the
assumptions, not meta-level assumptions.  For instance, replacing~$a$
by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, use
Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
$\List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q,$ it locates a suitable