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: