
diff -r d468d72a458f -r 83bd9eb1c70c doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Mon Aug 27 17:11:55 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,217 +0,0 @@
-
-\chapter{Substitution Tactics} \label{substitution}
-\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 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.  The
-tactic \texttt{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 equations.
-Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.
-
-
-\section{Substitution rules}
-\index{substitution!rules}\index{*subst theorem}
-Many logics include a substitution rule of the form
-$$
-\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp 
-\Var{P}(\Var{b})  \eqno(subst)
-$$
-In backward proof, this may seem difficult to use: the conclusion
-$\Var{P}(\Var{b})$ admits far too many unifiers.  But, if the theorem {\tt
-eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
-\[ \Var{P}(t) \Imp \Var{P}(u). \]
-Provided $u$ is not an unknown, resolution with this rule is
-well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$
-expresses~$Q$ in terms of its dependence upon~$u$.  There are still $2^k$
-unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that
-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.}
-\end{ttbox}
-To replace $t$ by~$u$ in
-subgoal~$i$, use
-\begin{ttbox} 
-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 
-\Var{P}(\Var{a}).  \eqno(ssubst)
-$$
-If \tdx{sym} denotes the symmetry rule
-\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then \texttt{ssubst} is just
-\hbox{\tt sym RS subst}.  Many logics with equality include the rules {\tt
-subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans}
-(for the usual equality laws).  Examples include \texttt{FOL} and \texttt{HOL},
-but not \texttt{CTT} (Constructive Type Theory).
-
-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\)    {\rm or}    eresolve_tac [ssubst] \(i\){\it.}
-\end{ttbox}
-
-Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
-\begin{ttbox} 
-fun stac eqth = CHANGED o rtac (eqth RS ssubst);
-\end{ttbox}
-Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the
-valuable property of failing if the substitution has no effect.
-
-
-\section{Substitution in the hypotheses}
-\index{assumptions!substitution in}
-Substitution rules, like other rules of natural deduction, do not affect
-the assumptions.  This can be inconvenient.  Consider proving the subgoal
-\[ \List{c=a; c=b} \Imp a=b. \]
-Calling \texttt{eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the
-assumption~$c=a$, since $c$ does not occur in~$a=b$.  Of course, we can
-work out a solution.  First apply \texttt{eresolve_tac\ts[subst]\ts\(i\)},
-replacing~$a$ by~$c$:
-\[ c=b \Imp c=b \]
-Equality reasoning can be difficult, but this trivial proof requires
-nothing more sophisticated than substitution in the assumptions.
-Object-logics that include the rule~$(subst)$ provide tactics for this
-purpose:
-\begin{ttbox} 
-hyp_subst_tac       : int -> tactic
-bound_hyp_subst_tac : int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{hyp_subst_tac} {\it i}] 
-  selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a
-  free variable or parameter.  Deleting this assumption, it replaces $t$
-  by~$u$ throughout subgoal~$i$, including the other assumptions.
-
-\item[\ttindexbold{bound_hyp_subst_tac} {\it i}] 
-  is similar but only substitutes for parameters (bound variables).
-  Uses for this are discussed below.
-\end{ttdescription}
-The term being replaced must be a free variable or parameter.  Substitution
-for constants is usually unhelpful, since they may appear in other
-theorems.  For instance, the best way to use the assumption $0=1$ is to
-contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
-in the subgoal!
-
-Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove
-the subgoal more easily by instantiating~$\Var{x}$ to~1.
-Substitution for free variables is unhelpful if they appear in the
-premises of a rule being derived: the substitution affects object-level
-assumptions, not meta-level assumptions.  For instance, replacing~$a$
-by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, use
-\texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to
-insert the atomic premises as object-level assumptions.
-
-
-\section{Setting up the package} 
-Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their
-descendants, come with \texttt{hyp_subst_tac} already defined.  A few others,
-such as \texttt{CTT}, do not support this tactic because they lack the
-rule~$(subst)$.  When defining a new logic that includes a substitution
-rule and implication, you must set up \texttt{hyp_subst_tac} yourself.  It
-is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the
-argument signature~\texttt{HYPSUBST_DATA}:
-\begin{ttbox} 
-signature HYPSUBST_DATA =
-  sig
-  structure Simplifier : SIMPLIFIER
-  val dest_Trueprop    : term -> term
-  val dest_eq          : term -> (term*term)*typ
-  val dest_imp         : term -> term*term
-  val eq_reflection    : thm         (* a=b ==> a==b *)
-  val rev_eq_reflection: thm         (* a==b ==> a=b *)
-  val imp_intr         : thm         (*(P ==> Q) ==> P-->Q *)
-  val rev_mp           : thm         (* [| P;  P-->Q |] ==> Q *)
-  val subst            : thm         (* [| a=b;  P(a) |] ==> P(b) *)
-  val sym              : thm         (* a=b ==> b=a *)
-  val thin_refl        : thm         (* [|x=x; P|] ==> P *)
-  end;
-\end{ttbox}
-Thus, the functor requires the following items:
-\begin{ttdescription}
-\item[Simplifier] should be an instance of the simplifier (see
-  Chapter~\ref{chap:simplification}).
-  
-\item[\ttindexbold{dest_Trueprop}] should coerce a meta-level formula to the
-  corresponding object-level one.  Typically, it should return $P$ when
-  applied to the term $\texttt{Trueprop}\,P$ (see example below).
-  
-\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is
-  the type of~$t$ and~$u$, when applied to the \ML{} term that
-  represents~$t=u$.  For other terms, it should raise an exception.
-  
-\item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to
-  the \ML{} term that represents the implication $P\imp Q$.  For other terms,
-  it should raise an exception.
-
-\item[\tdxbold{eq_reflection}] is the theorem discussed
-  in~\S\ref{sec:setting-up-simp}.
-  
-\item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.
-
-\item[\tdxbold{imp_intr}] should be the implies introduction
-rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.
-
-\item[\tdxbold{rev_mp}] should be the `reversed' implies elimination
-rule $\List{\Var{P};  \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.
-
-\item[\tdxbold{subst}] should be the substitution rule
-$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.
-
-\item[\tdxbold{sym}] should be the symmetry rule
-$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.
-
-\item[\tdxbold{thin_refl}] should be the rule
-$\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase
-trivial equalities.
-\end{ttdescription}
-%
-The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle
-distribution directory.  It is not sensitive to the precise formalization
-of the object-logic.  It is not concerned with the names of the equality
-and implication symbols, or the types of formula and terms.  
-
-Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and
-\texttt{dest_imp} requires knowledge of Isabelle's representation of terms.
-For \texttt{FOL}, they are declared by
-\begin{ttbox} 
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
-  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-
-fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
-
-fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
-  | dest_imp  t = raise TERM ("dest_imp", [t]);
-\end{ttbox}
-Recall that \texttt{Trueprop} is the coercion from type~$o$ to type~$prop$,
-while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}.
-Function \ttindexbold{domain_type}, given the function type $S\To T$, returns
-the type~$S$.  Pattern-matching expresses the function concisely, using
-wildcards~({\tt_}) for the types.
-
-The tactic \texttt{hyp_subst_tac} works as follows.  First, it identifies a
-suitable equality assumption, possibly re-orienting it using~\texttt{sym}.
-Then it moves other assumptions into the conclusion of the goal, by repeatedly
-calling \texttt{etac~rev_mp}.  Then, it uses \texttt{asm_full_simp_tac} or
-\texttt{ssubst} to substitute throughout the subgoal.  (If the equality
-involves unknowns then it must use \texttt{ssubst}.)  Then, it deletes the
-equality.  Finally, it moves the assumptions back to their original positions
-by calling \hbox{\tt resolve_tac\ts[imp_intr]}.
-
-\index{equality|)}\index{tactics!substitution|)}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End: 




