doc-src/Ref/substitution.tex
 author wenzelm Mon Aug 28 13:52:38 2000 +0200 (2000-08-28) changeset 9695 ec7d7f877712 parent 9524 5721615da108 child 20975 5bfa2e4ed789 permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
 lcp@104  1 %% $Id$  lcp@104  2 \chapter{Substitution Tactics} \label{substitution}  lcp@323  3 \index{tactics!substitution|(}\index{equality|(}  lcp@323  4 lcp@104  5 Replacing equals by equals is a basic form of reasoning. Isabelle supports  lcp@332  6 several kinds of equality reasoning. {\bf Substitution} means replacing  lcp@104  7 free occurrences of~$t$ by~$u$ in a subgoal. This is easily done, given an  lcp@332  8 equality $t=u$, provided the logic possesses the appropriate rule. The  paulson@4596  9 tactic \texttt{hyp_subst_tac} performs substitution even in the assumptions.  lcp@332  10 But it works via object-level implication, and therefore must be specially  lcp@332  11 set up for each suitable object-logic.  lcp@104  12 lcp@104  13 Substitution should not be confused with object-level {\bf rewriting}.  lcp@104  14 Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by  lcp@104  15 corresponding instances of~$u$, and continues until it reaches a normal  lcp@104  16 form. Substitution handles one-off' replacements by particular  lcp@332  17 equalities while rewriting handles general equations.  nipkow@3950  18 Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.  lcp@104  19 lcp@104  20 lcp@323  21 \section{Substitution rules}  lcp@323  22 \index{substitution!rules}\index{*subst theorem}  lcp@323  23 Many logics include a substitution rule of the form  wenzelm@3108  24 $$ wenzelm@3108  25 \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp  wenzelm@3108  26 \Var{P}(\Var{b}) \eqno(subst)  wenzelm@3108  27 $$  lcp@104  28 In backward proof, this may seem difficult to use: the conclusion  lcp@104  29 $\Var{P}(\Var{b})$ admits far too many unifiers. But, if the theorem {\tt  lcp@104  30 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule  lcp@104  31 $\Var{P}(t) \Imp \Var{P}(u).$  lcp@104  32 Provided $u$ is not an unknown, resolution with this rule is  lcp@104  33 well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$  lcp@104  34 expresses~$Q$ in terms of its dependence upon~$u$. There are still $2^k$  lcp@104  35 unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that  lcp@104  36 the first unifier includes all the occurrences.} To replace $u$ by~$t$ in  lcp@104  37 subgoal~$i$, use  lcp@104  38 \begin{ttbox}  lcp@332  39 resolve_tac [eqth RS subst] $$i$${\it.}  lcp@104  40 \end{ttbox}  lcp@104  41 To replace $t$ by~$u$ in  lcp@104  42 subgoal~$i$, use  lcp@104  43 \begin{ttbox}  lcp@332  44 resolve_tac [eqth RS ssubst] $$i$${\it,}  lcp@104  45 \end{ttbox}  lcp@323  46 where \tdxbold{ssubst} is the swapped' substitution rule  wenzelm@3108  47 $$ wenzelm@3108  48 \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp  wenzelm@3108  49 \Var{P}(\Var{a}). \eqno(ssubst)  wenzelm@3108  50 $$  lcp@323  51 If \tdx{sym} denotes the symmetry rule  paulson@4596  52 $$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$$, then \texttt{ssubst} is just  lcp@104  53 \hbox{\tt sym RS subst}. Many logics with equality include the rules {\tt  paulson@4596  54 subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans}  paulson@4596  55 (for the usual equality laws). Examples include \texttt{FOL} and \texttt{HOL},  paulson@4596  56 but not \texttt{CTT} (Constructive Type Theory).  lcp@104  57 lcp@104  58 Elim-resolution is well-behaved with assumptions of the form $t=u$.  lcp@104  59 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use  lcp@104  60 \begin{ttbox}  lcp@332  61 eresolve_tac [subst] $$i$$ {\rm or} eresolve_tac [ssubst] $$i$${\it.}  lcp@104  62 \end{ttbox}  lcp@104  63 wenzelm@9695  64 Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by  paulson@2038  65 \begin{ttbox}  paulson@2038  66 fun stac eqth = CHANGED o rtac (eqth RS ssubst);  paulson@2038  67 \end{ttbox}  paulson@4596  68 Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the  paulson@2038  69 valuable property of failing if the substitution has no effect.  paulson@2038  70 lcp@104  71 lcp@104  72 \section{Substitution in the hypotheses}  lcp@323  73 \index{assumptions!substitution in}  lcp@104  74 Substitution rules, like other rules of natural deduction, do not affect  lcp@104  75 the assumptions. This can be inconvenient. Consider proving the subgoal  lcp@104  76 $\List{c=a; c=b} \Imp a=b.$  paulson@4596  77 Calling \texttt{eresolve_tac\ts[ssubst]\ts$$i$$} simply discards the  lcp@104  78 assumption~$c=a$, since $c$ does not occur in~$a=b$. Of course, we can  paulson@4596  79 work out a solution. First apply \texttt{eresolve_tac\ts[subst]\ts$$i$$},  lcp@104  80 replacing~$a$ by~$c$:  wenzelm@4374  81 $c=b \Imp c=b$  lcp@104  82 Equality reasoning can be difficult, but this trivial proof requires  lcp@104  83 nothing more sophisticated than substitution in the assumptions.  lcp@323  84 Object-logics that include the rule~$(subst)$ provide tactics for this  lcp@104  85 purpose:  lcp@104  86 \begin{ttbox}  lcp@323  87 hyp_subst_tac : int -> tactic  lcp@323  88 bound_hyp_subst_tac : int -> tactic  lcp@104  89 \end{ttbox}  lcp@323  90 \begin{ttdescription}  lcp@104  91 \item[\ttindexbold{hyp_subst_tac} {\it i}]  lcp@323  92  selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a  lcp@323  93  free variable or parameter. Deleting this assumption, it replaces $t$  lcp@323  94  by~$u$ throughout subgoal~$i$, including the other assumptions.  lcp@323  95 lcp@323  96 \item[\ttindexbold{bound_hyp_subst_tac} {\it i}]  lcp@323  97  is similar but only substitutes for parameters (bound variables).  lcp@323  98  Uses for this are discussed below.  lcp@323  99 \end{ttdescription}  lcp@104  100 The term being replaced must be a free variable or parameter. Substitution  lcp@104  101 for constants is usually unhelpful, since they may appear in other  lcp@104  102 theorems. For instance, the best way to use the assumption $0=1$ is to  lcp@104  103 contradict a theorem that states $0\not=1$, rather than to replace 0 by~1  lcp@104  104 in the subgoal!  lcp@104  105 paulson@2038  106 Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove  paulson@2038  107 the subgoal more easily by instantiating~$\Var{x}$ to~1.  paulson@2038  108 Substitution for free variables is unhelpful if they appear in the  paulson@2038  109 premises of a rule being derived: the substitution affects object-level  lcp@104  110 assumptions, not meta-level assumptions. For instance, replacing~$a$  lcp@323  111 by~$b$ could make the premise~$P(a)$ worthless. To avoid this problem, use  paulson@4596  112 \texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to  lcp@323  113 insert the atomic premises as object-level assumptions.  lcp@104  114 lcp@104  115 wenzelm@6618  116 \section{Setting up the package}  paulson@4596  117 Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their  paulson@4596  118 descendants, come with \texttt{hyp_subst_tac} already defined. A few others,  paulson@4596  119 such as \texttt{CTT}, do not support this tactic because they lack the  lcp@104  120 rule~$(subst)$. When defining a new logic that includes a substitution  paulson@4596  121 rule and implication, you must set up \texttt{hyp_subst_tac} yourself. It  lcp@104  122 is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the  paulson@4596  123 argument signature~\texttt{HYPSUBST_DATA}:  lcp@104  124 \begin{ttbox}  lcp@104  125 signature HYPSUBST_DATA =  lcp@104  126  sig  paulson@2038  127  structure Simplifier : SIMPLIFIER  paulson@4596  128  val dest_Trueprop : term -> term  paulson@4596  129  val dest_eq : term -> term*term*typ  paulson@4596  130  val dest_imp : term -> term*term  paulson@8136  131  val eq_reflection : thm (* a=b ==> a==b *)  wenzelm@9524  132  val rev_eq_reflection: thm (* a==b ==> a=b *)  paulson@8136  133  val imp_intr : thm (*(P ==> Q) ==> P-->Q *)  paulson@8136  134  val rev_mp : thm (* [| P; P-->Q |] ==> Q *)  paulson@8136  135  val subst : thm (* [| a=b; P(a) |] ==> P(b) *)  paulson@8136  136  val sym : thm (* a=b ==> b=a *)  paulson@8136  137  val thin_refl : thm (* [|x=x; P|] ==> P *)  lcp@104  138  end;  lcp@104  139 \end{ttbox}  lcp@104  140 Thus, the functor requires the following items:  lcp@323  141 \begin{ttdescription}  paulson@2038  142 \item[Simplifier] should be an instance of the simplifier (see  nipkow@3950  143  Chapter~\ref{chap:simplification}).  paulson@4596  144   paulson@4596  145 \item[\ttindexbold{dest_Trueprop}] should coerce a meta-level formula to the  paulson@4596  146  corresponding object-level one. Typically, it should return $P$ when  paulson@4596  147  applied to the term $\texttt{Trueprop}\,P$ (see example below).  paulson@4596  148   paulson@4596  149 \item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is  paulson@4596  150  the type of~$t$ and~$u$, when applied to the \ML{} term that  paulson@4596  151  represents~$t=u$. For other terms, it should raise an exception.  paulson@4596  152   paulson@4596  153 \item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to  paulson@4596  154  the \ML{} term that represents the implication $P\imp Q$. For other terms,  paulson@4596  155  it should raise an exception.  lcp@104  156 paulson@2038  157 \item[\tdxbold{eq_reflection}] is the theorem discussed  wenzelm@9524  158  in~\S\ref{sec:setting-up-simp}.  wenzelm@9524  159   wenzelm@9524  160 \item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.  lcp@104  161 lcp@323  162 \item[\tdxbold{imp_intr}] should be the implies introduction  lcp@104  163 rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.  lcp@104  164 lcp@323  165 \item[\tdxbold{rev_mp}] should be the reversed' implies elimination  lcp@104  166 rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.  lcp@104  167 paulson@2038  168 \item[\tdxbold{subst}] should be the substitution rule  paulson@2038  169 $\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.  paulson@2038  170 paulson@2038  171 \item[\tdxbold{sym}] should be the symmetry rule  paulson@2038  172 $\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.  paulson@4596  173 paulson@4596  174 \item[\tdxbold{thin_refl}] should be the rule  paulson@4596  175 $\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase  paulson@4596  176 trivial equalities.  lcp@323  177 \end{ttdescription}  paulson@2038  178 %  paulson@4596  179 The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle  lcp@104  180 distribution directory. It is not sensitive to the precise formalization  lcp@104  181 of the object-logic. It is not concerned with the names of the equality  paulson@4596  182 and implication symbols, or the types of formula and terms.  paulson@4596  183 paulson@4596  184 Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and  paulson@4596  185 \texttt{dest_imp} requires knowledge of Isabelle's representation of terms.  paulson@4596  186 For \texttt{FOL}, they are declared by  lcp@104  187 \begin{ttbox}  paulson@4596  188 fun dest_Trueprop (Const ("Trueprop", _) $P) = P  paulson@4596  189  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);  paulson@4596  190 paulson@4596  191 fun dest_eq (Const("op =",T)$ t $u) = (t, u, domain_type T)  paulson@4596  192 paulson@4596  193 fun dest_imp (Const("op -->",_)$ A $B) = (A, B)  paulson@4596  194  | dest_imp t = raise TERM ("dest_imp", [t]);  lcp@104  195 \end{ttbox}  paulson@4596  196 Recall that \texttt{Trueprop} is the coercion from type~$o$to type~$prop$,  paulson@4596  197 while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}.  paulson@4596  198 Function \ttindexbold{domain_type}, given the function type$S\To T$, returns  paulson@4596  199 the type~$S\$. Pattern-matching expresses the function concisely, using  paulson@4596  200 wildcards~({\tt_}) for the types.  lcp@104  201 paulson@4596  202 The tactic \texttt{hyp_subst_tac} works as follows. First, it identifies a  paulson@4596  203 suitable equality assumption, possibly re-orienting it using~\texttt{sym}.  paulson@4596  204 Then it moves other assumptions into the conclusion of the goal, by repeatedly  paulson@4596  205 calling \texttt{etac~rev_mp}. Then, it uses \texttt{asm_full_simp_tac} or  paulson@4596  206 \texttt{ssubst} to substitute throughout the subgoal. (If the equality  paulson@4596  207 involves unknowns then it must use \texttt{ssubst}.) Then, it deletes the  paulson@2038  208 equality. Finally, it moves the assumptions back to their original positions  paulson@2038  209 by calling \hbox{\tt resolve_tac\ts[imp_intr]}.  lcp@104  210 lcp@323  211 \index{equality|)}\index{tactics!substitution|)}  wenzelm@5371  212 wenzelm@5371  213 wenzelm@5371  214 %%% Local Variables:  wenzelm@5371  215 %%% mode: latex  wenzelm@5371  216 %%% TeX-master: "ref"  wenzelm@5371  217 %%% End: `