1.1 --- a/src/Doc/ROOT Sun Nov 11 21:08:11 2012 +0100
1.2 +++ b/src/Doc/ROOT Mon Nov 12 21:17:58 2012 +0100
1.3 @@ -262,7 +262,6 @@
1.4 "../manual.bib"
1.5 "document/build"
1.6 "document/root.tex"
1.7 - "document/substitution.tex"
1.8 "document/syntax.tex"
1.9 "document/thm.tex"
1.10
2.1 --- a/src/Doc/Ref/document/root.tex Sun Nov 11 21:08:11 2012 +0100
2.2 +++ b/src/Doc/Ref/document/root.tex Mon Nov 12 21:17:58 2012 +0100
2.3 @@ -42,7 +42,6 @@
2.4
2.5 \input{thm}
2.6 \input{syntax}
2.7 -\input{substitution}
2.8
2.9 %%seealso's must be last so that they appear last in the index entries
2.10 \index{meta-rewriting|seealso{tactics, theorems}}
3.1 --- a/src/Doc/Ref/document/substitution.tex Sun Nov 11 21:08:11 2012 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,217 +0,0 @@
3.4 -
3.5 -\chapter{Substitution Tactics} \label{substitution}
3.6 -\index{tactics!substitution|(}\index{equality|(}
3.7 -
3.8 -Replacing equals by equals is a basic form of reasoning. Isabelle supports
3.9 -several kinds of equality reasoning. {\bf Substitution} means replacing
3.10 -free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an
3.11 -equality $t=u$, provided the logic possesses the appropriate rule. The
3.12 -tactic \texttt{hyp_subst_tac} performs substitution even in the assumptions.
3.13 -But it works via object-level implication, and therefore must be specially
3.14 -set up for each suitable object-logic.
3.15 -
3.16 -Substitution should not be confused with object-level {\bf rewriting}.
3.17 -Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
3.18 -corresponding instances of~$u$, and continues until it reaches a normal
3.19 -form. Substitution handles `one-off' replacements by particular
3.20 -equalities while rewriting handles general equations.
3.21 -Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.
3.22 -
3.23 -
3.24 -\section{Substitution rules}
3.25 -\index{substitution!rules}\index{*subst theorem}
3.26 -Many logics include a substitution rule of the form
3.27 -$$
3.28 -\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp
3.29 -\Var{P}(\Var{b}) \eqno(subst)
3.30 -$$
3.31 -In backward proof, this may seem difficult to use: the conclusion
3.32 -$\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt
3.33 -eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
3.34 -\[ \Var{P}(t) \Imp \Var{P}(u). \]
3.35 -Provided $u$ is not an unknown, resolution with this rule is
3.36 -well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$
3.37 -expresses~$Q$ in terms of its dependence upon~$u$. There are still $2^k$
3.38 -unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that
3.39 -the first unifier includes all the occurrences.} To replace $u$ by~$t$ in
3.40 -subgoal~$i$, use
3.41 -\begin{ttbox}
3.42 -resolve_tac [eqth RS subst] \(i\){\it.}
3.43 -\end{ttbox}
3.44 -To replace $t$ by~$u$ in
3.45 -subgoal~$i$, use
3.46 -\begin{ttbox}
3.47 -resolve_tac [eqth RS ssubst] \(i\){\it,}
3.48 -\end{ttbox}
3.49 -where \tdxbold{ssubst} is the `swapped' substitution rule
3.50 -$$
3.51 -\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp
3.52 -\Var{P}(\Var{a}). \eqno(ssubst)
3.53 -$$
3.54 -If \tdx{sym} denotes the symmetry rule
3.55 -\(\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}\), then \texttt{ssubst} is just
3.56 -\hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt
3.57 -subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans}
3.58 -(for the usual equality laws). Examples include \texttt{FOL} and \texttt{HOL},
3.59 -but not \texttt{CTT} (Constructive Type Theory).
3.60 -
3.61 -Elim-resolution is well-behaved with assumptions of the form $t=u$.
3.62 -To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
3.63 -\begin{ttbox}
3.64 -eresolve_tac [subst] \(i\) {\rm or} eresolve_tac [ssubst] \(i\){\it.}
3.65 -\end{ttbox}
3.66 -
3.67 -Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by
3.68 -\begin{ttbox}
3.69 -fun stac eqth = CHANGED o rtac (eqth RS ssubst);
3.70 -\end{ttbox}
3.71 -Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the
3.72 -valuable property of failing if the substitution has no effect.
3.73 -
3.74 -
3.75 -\section{Substitution in the hypotheses}
3.76 -\index{assumptions!substitution in}
3.77 -Substitution rules, like other rules of natural deduction, do not affect
3.78 -the assumptions. This can be inconvenient. Consider proving the subgoal
3.79 -\[ \List{c=a; c=b} \Imp a=b. \]
3.80 -Calling \texttt{eresolve_tac\ts[ssubst]\ts\(i\)} simply discards the
3.81 -assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can
3.82 -work out a solution. First apply \texttt{eresolve_tac\ts[subst]\ts\(i\)},
3.83 -replacing~$a$ by~$c$:
3.84 -\[ c=b \Imp c=b \]
3.85 -Equality reasoning can be difficult, but this trivial proof requires
3.86 -nothing more sophisticated than substitution in the assumptions.
3.87 -Object-logics that include the rule~$(subst)$ provide tactics for this
3.88 -purpose:
3.89 -\begin{ttbox}
3.90 -hyp_subst_tac : int -> tactic
3.91 -bound_hyp_subst_tac : int -> tactic
3.92 -\end{ttbox}
3.93 -\begin{ttdescription}
3.94 -\item[\ttindexbold{hyp_subst_tac} {\it i}]
3.95 - selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a
3.96 - free variable or parameter. Deleting this assumption, it replaces $t$
3.97 - by~$u$ throughout subgoal~$i$, including the other assumptions.
3.98 -
3.99 -\item[\ttindexbold{bound_hyp_subst_tac} {\it i}]
3.100 - is similar but only substitutes for parameters (bound variables).
3.101 - Uses for this are discussed below.
3.102 -\end{ttdescription}
3.103 -The term being replaced must be a free variable or parameter. Substitution
3.104 -for constants is usually unhelpful, since they may appear in other
3.105 -theorems. For instance, the best way to use the assumption $0=1$ is to
3.106 -contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
3.107 -in the subgoal!
3.108 -
3.109 -Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove
3.110 -the subgoal more easily by instantiating~$\Var{x}$ to~1.
3.111 -Substitution for free variables is unhelpful if they appear in the
3.112 -premises of a rule being derived: the substitution affects object-level
3.113 -assumptions, not meta-level assumptions. For instance, replacing~$a$
3.114 -by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use
3.115 -\texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to
3.116 -insert the atomic premises as object-level assumptions.
3.117 -
3.118 -
3.119 -\section{Setting up the package}
3.120 -Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their
3.121 -descendants, come with \texttt{hyp_subst_tac} already defined. A few others,
3.122 -such as \texttt{CTT}, do not support this tactic because they lack the
3.123 -rule~$(subst)$. When defining a new logic that includes a substitution
3.124 -rule and implication, you must set up \texttt{hyp_subst_tac} yourself. It
3.125 -is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the
3.126 -argument signature~\texttt{HYPSUBST_DATA}:
3.127 -\begin{ttbox}
3.128 -signature HYPSUBST_DATA =
3.129 - sig
3.130 - structure Simplifier : SIMPLIFIER
3.131 - val dest_Trueprop : term -> term
3.132 - val dest_eq : term -> (term*term)*typ
3.133 - val dest_imp : term -> term*term
3.134 - val eq_reflection : thm (* a=b ==> a==b *)
3.135 - val rev_eq_reflection: thm (* a==b ==> a=b *)
3.136 - val imp_intr : thm (*(P ==> Q) ==> P-->Q *)
3.137 - val rev_mp : thm (* [| P; P-->Q |] ==> Q *)
3.138 - val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
3.139 - val sym : thm (* a=b ==> b=a *)
3.140 - val thin_refl : thm (* [|x=x; P|] ==> P *)
3.141 - end;
3.142 -\end{ttbox}
3.143 -Thus, the functor requires the following items:
3.144 -\begin{ttdescription}
3.145 -\item[Simplifier] should be an instance of the simplifier (see
3.146 - Chapter~\ref{chap:simplification}).
3.147 -
3.148 -\item[\ttindexbold{dest_Trueprop}] should coerce a meta-level formula to the
3.149 - corresponding object-level one. Typically, it should return $P$ when
3.150 - applied to the term $\texttt{Trueprop}\,P$ (see example below).
3.151 -
3.152 -\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is
3.153 - the type of~$t$ and~$u$, when applied to the \ML{} term that
3.154 - represents~$t=u$. For other terms, it should raise an exception.
3.155 -
3.156 -\item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to
3.157 - the \ML{} term that represents the implication $P\imp Q$. For other terms,
3.158 - it should raise an exception.
3.159 -
3.160 -\item[\tdxbold{eq_reflection}] is the theorem discussed
3.161 - in~\S\ref{sec:setting-up-simp}.
3.162 -
3.163 -\item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.
3.164 -
3.165 -\item[\tdxbold{imp_intr}] should be the implies introduction
3.166 -rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.
3.167 -
3.168 -\item[\tdxbold{rev_mp}] should be the `reversed' implies elimination
3.169 -rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.
3.170 -
3.171 -\item[\tdxbold{subst}] should be the substitution rule
3.172 -$\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.
3.173 -
3.174 -\item[\tdxbold{sym}] should be the symmetry rule
3.175 -$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.
3.176 -
3.177 -\item[\tdxbold{thin_refl}] should be the rule
3.178 -$\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase
3.179 -trivial equalities.
3.180 -\end{ttdescription}
3.181 -%
3.182 -The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle
3.183 -distribution directory. It is not sensitive to the precise formalization
3.184 -of the object-logic. It is not concerned with the names of the equality
3.185 -and implication symbols, or the types of formula and terms.
3.186 -
3.187 -Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and
3.188 -\texttt{dest_imp} requires knowledge of Isabelle's representation of terms.
3.189 -For \texttt{FOL}, they are declared by
3.190 -\begin{ttbox}
3.191 -fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
3.192 - | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
3.193 -
3.194 -fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
3.195 -
3.196 -fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
3.197 - | dest_imp t = raise TERM ("dest_imp", [t]);
3.198 -\end{ttbox}
3.199 -Recall that \texttt{Trueprop} is the coercion from type~$o$ to type~$prop$,
3.200 -while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}.
3.201 -Function \ttindexbold{domain_type}, given the function type $S\To T$, returns
3.202 -the type~$S$. Pattern-matching expresses the function concisely, using
3.203 -wildcards~({\tt_}) for the types.
3.204 -
3.205 -The tactic \texttt{hyp_subst_tac} works as follows. First, it identifies a
3.206 -suitable equality assumption, possibly re-orienting it using~\texttt{sym}.
3.207 -Then it moves other assumptions into the conclusion of the goal, by repeatedly
3.208 -calling \texttt{etac~rev_mp}. Then, it uses \texttt{asm_full_simp_tac} or
3.209 -\texttt{ssubst} to substitute throughout the subgoal. (If the equality
3.210 -involves unknowns then it must use \texttt{ssubst}.) Then, it deletes the
3.211 -equality. Finally, it moves the assumptions back to their original positions
3.212 -by calling \hbox{\tt resolve_tac\ts[imp_intr]}.
3.213 -
3.214 -\index{equality|)}\index{tactics!substitution|)}
3.215 -
3.216 -
3.217 -%%% Local Variables:
3.218 -%%% mode: latex
3.219 -%%% TeX-master: "ref"
3.220 -%%% End: