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;
     1 %% $Id$

     2 \chapter{Substitution Tactics} \label{substitution}

     3 \index{tactics!substitution|(}\index{equality|(}

     4

     5 Replacing equals by equals is a basic form of reasoning.  Isabelle supports

     6 several kinds of equality reasoning.  {\bf Substitution} means replacing

     7 free occurrences of~$t$ by~$u$ in a subgoal.  This is easily done, given an

     8 equality $t=u$, provided the logic possesses the appropriate rule.  The

     9 tactic \texttt{hyp_subst_tac} performs substitution even in the assumptions.

    10 But it works via object-level implication, and therefore must be specially

    11 set up for each suitable object-logic.

    12

    13 Substitution should not be confused with object-level {\bf rewriting}.

    14 Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by

    15 corresponding instances of~$u$, and continues until it reaches a normal

    16 form.  Substitution handles one-off' replacements by particular

    17 equalities while rewriting handles general equations.

    18 Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.

    19

    20

    21 \section{Substitution rules}

    22 \index{substitution!rules}\index{*subst theorem}

    23 Many logics include a substitution rule of the form

    24 $$  25 \List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp   26 \Var{P}(\Var{b}) \eqno(subst)   27$$

    28 In backward proof, this may seem difficult to use: the conclusion

    29 $\Var{P}(\Var{b})$ admits far too many unifiers.  But, if the theorem {\tt

    30 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule

    31 $\Var{P}(t) \Imp \Var{P}(u).$

    32 Provided $u$ is not an unknown, resolution with this rule is

    33 well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$

    34 expresses~$Q$ in terms of its dependence upon~$u$.  There are still $2^k$

    35 unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that

    36 the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in

    37 subgoal~$i$, use

    38 \begin{ttbox}

    39 resolve_tac [eqth RS subst] $$i$${\it.}

    40 \end{ttbox}

    41 To replace $t$ by~$u$ in

    42 subgoal~$i$, use

    43 \begin{ttbox}

    44 resolve_tac [eqth RS ssubst] $$i$${\it,}

    45 \end{ttbox}

    46 where \tdxbold{ssubst} is the swapped' substitution rule

    47 $$  48 \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp   49 \Var{P}(\Var{a}). \eqno(ssubst)   50$$

    51 If \tdx{sym} denotes the symmetry rule

    52 $$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$$, then \texttt{ssubst} is just

    53 \hbox{\tt sym RS subst}.  Many logics with equality include the rules {\tt

    54 subst} and \texttt{ssubst}, as well as \texttt{refl}, \texttt{sym} and \texttt{trans}

    55 (for the usual equality laws).  Examples include \texttt{FOL} and \texttt{HOL},

    56 but not \texttt{CTT} (Constructive Type Theory).

    57

    58 Elim-resolution is well-behaved with assumptions of the form $t=u$.

    59 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use

    60 \begin{ttbox}

    61 eresolve_tac [subst] $$i$$    {\rm or}    eresolve_tac [ssubst] $$i$${\it.}

    62 \end{ttbox}

    63

    64 Logics HOL, FOL and ZF define the tactic \ttindexbold{stac} by

    65 \begin{ttbox}

    66 fun stac eqth = CHANGED o rtac (eqth RS ssubst);

    67 \end{ttbox}

    68 Now \texttt{stac~eqth} is like \texttt{resolve_tac [eqth RS ssubst]} but with the

    69 valuable property of failing if the substitution has no effect.

    70

    71

    72 \section{Substitution in the hypotheses}

    73 \index{assumptions!substitution in}

    74 Substitution rules, like other rules of natural deduction, do not affect

    75 the assumptions.  This can be inconvenient.  Consider proving the subgoal

    76 $\List{c=a; c=b} \Imp a=b.$

    77 Calling \texttt{eresolve_tac\ts[ssubst]\ts$$i$$} simply discards the

    78 assumption~$c=a$, since $c$ does not occur in~$a=b$.  Of course, we can

    79 work out a solution.  First apply \texttt{eresolve_tac\ts[subst]\ts$$i$$},

    80 replacing~$a$ by~$c$:

    81 $c=b \Imp c=b$

    82 Equality reasoning can be difficult, but this trivial proof requires

    83 nothing more sophisticated than substitution in the assumptions.

    84 Object-logics that include the rule~$(subst)$ provide tactics for this

    85 purpose:

    86 \begin{ttbox}

    87 hyp_subst_tac       : int -> tactic

    88 bound_hyp_subst_tac : int -> tactic

    89 \end{ttbox}

    90 \begin{ttdescription}

    91 \item[\ttindexbold{hyp_subst_tac} {\it i}]

    92   selects an equality assumption of the form $t=u$ or $u=t$, where $t$ is a

    93   free variable or parameter.  Deleting this assumption, it replaces $t$

    94   by~$u$ throughout subgoal~$i$, including the other assumptions.

    95

    96 \item[\ttindexbold{bound_hyp_subst_tac} {\it i}]

    97   is similar but only substitutes for parameters (bound variables).

    98   Uses for this are discussed below.

    99 \end{ttdescription}

   100 The term being replaced must be a free variable or parameter.  Substitution

   101 for constants is usually unhelpful, since they may appear in other

   102 theorems.  For instance, the best way to use the assumption $0=1$ is to

   103 contradict a theorem that states $0\not=1$, rather than to replace 0 by~1

   104 in the subgoal!

   105

   106 Substitution for unknowns, such as $\Var{x}=0$, is a bad idea: we might prove

   107 the subgoal more easily by instantiating~$\Var{x}$ to~1.

   108 Substitution for free variables is unhelpful if they appear in the

   109 premises of a rule being derived: the substitution affects object-level

   110 assumptions, not meta-level assumptions.  For instance, replacing~$a$

   111 by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, use

   112 \texttt{bound_hyp_subst_tac}; alternatively, call \ttindex{cut_facts_tac} to

   113 insert the atomic premises as object-level assumptions.

   114

   115

   116 \section{Setting up the package}

   117 Many Isabelle object-logics, such as \texttt{FOL}, \texttt{HOL} and their

   118 descendants, come with \texttt{hyp_subst_tac} already defined.  A few others,

   119 such as \texttt{CTT}, do not support this tactic because they lack the

   120 rule~$(subst)$.  When defining a new logic that includes a substitution

   121 rule and implication, you must set up \texttt{hyp_subst_tac} yourself.  It

   122 is packaged as the \ML{} functor \ttindex{HypsubstFun}, which takes the

   123 argument signature~\texttt{HYPSUBST_DATA}:

   124 \begin{ttbox}

   125 signature HYPSUBST_DATA =

   126   sig

   127   structure Simplifier : SIMPLIFIER

   128   val dest_Trueprop    : term -> term

   129   val dest_eq          : term -> term*term*typ

   130   val dest_imp         : term -> term*term

   131   val eq_reflection    : thm         (* a=b ==> a==b *)

   132   val rev_eq_reflection: thm         (* a==b ==> a=b *)

   133   val imp_intr         : thm         (*(P ==> Q) ==> P-->Q *)

   134   val rev_mp           : thm         (* [| P;  P-->Q |] ==> Q *)

   135   val subst            : thm         (* [| a=b;  P(a) |] ==> P(b) *)

   136   val sym              : thm         (* a=b ==> b=a *)

   137   val thin_refl        : thm         (* [|x=x; P|] ==> P *)

   138   end;

   139 \end{ttbox}

   140 Thus, the functor requires the following items:

   141 \begin{ttdescription}

   142 \item[Simplifier] should be an instance of the simplifier (see

   143   Chapter~\ref{chap:simplification}).

   144

   145 \item[\ttindexbold{dest_Trueprop}] should coerce a meta-level formula to the

   146   corresponding object-level one.  Typically, it should return $P$ when

   147   applied to the term $\texttt{Trueprop}\,P$ (see example below).

   148

   149 \item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is

   150   the type of~$t$ and~$u$, when applied to the \ML{} term that

   151   represents~$t=u$.  For other terms, it should raise an exception.

   152

   153 \item[\ttindexbold{dest_imp}] should return the pair~$(P,Q)$ when applied to

   154   the \ML{} term that represents the implication $P\imp Q$.  For other terms,

   155   it should raise an exception.

   156

   157 \item[\tdxbold{eq_reflection}] is the theorem discussed

   158   in~\S\ref{sec:setting-up-simp}.

   159

   160 \item[\tdxbold{rev_eq_reflection}] is the reverse of \texttt{eq_reflection}.

   161

   162 \item[\tdxbold{imp_intr}] should be the implies introduction

   163 rule $(\Var{P}\Imp\Var{Q})\Imp \Var{P}\imp\Var{Q}$.

   164

   165 \item[\tdxbold{rev_mp}] should be the reversed' implies elimination

   166 rule $\List{\Var{P}; \;\Var{P}\imp\Var{Q}} \Imp \Var{Q}$.

   167

   168 \item[\tdxbold{subst}] should be the substitution rule

   169 $\List{\Var{a}=\Var{b};\; \Var{P}(\Var{a})} \Imp \Var{P}(\Var{b})$.

   170

   171 \item[\tdxbold{sym}] should be the symmetry rule

   172 $\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$.

   173

   174 \item[\tdxbold{thin_refl}] should be the rule

   175 $\List{\Var{a}=\Var{a};\; \Var{P}} \Imp \Var{P}$, which is used to erase

   176 trivial equalities.

   177 \end{ttdescription}

   178 %

   179 The functor resides in file \texttt{Provers/hypsubst.ML} in the Isabelle

   180 distribution directory.  It is not sensitive to the precise formalization

   181 of the object-logic.  It is not concerned with the names of the equality

   182 and implication symbols, or the types of formula and terms.

   183

   184 Coding the functions \texttt{dest_Trueprop}, \texttt{dest_eq} and

   185 \texttt{dest_imp} requires knowledge of Isabelle's representation of terms.

   186 For \texttt{FOL}, they are declared by

   187 \begin{ttbox}

   188 fun dest_Trueprop (Const ("Trueprop", _) $P) = P   189 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);   190   191 fun dest_eq (Const("op =",T)$ t $u) = (t, u, domain_type T)   192   193 fun dest_imp (Const("op -->",_)$ A $B) = (A, B)   194 | dest_imp t = raise TERM ("dest_imp", [t]);   195 \end{ttbox}   196 Recall that \texttt{Trueprop} is the coercion from type~$o$to type~$prop$,   197 while \hbox{\tt op =} is the internal name of the infix operator~\texttt{=}.   198 Function \ttindexbold{domain_type}, given the function type$S\To T$, returns   199 the type~$S\$.  Pattern-matching expresses the function concisely, using

   200 wildcards~({\tt_}) for the types.

   201

   202 The tactic \texttt{hyp_subst_tac} works as follows.  First, it identifies a

   203 suitable equality assumption, possibly re-orienting it using~\texttt{sym}.

   204 Then it moves other assumptions into the conclusion of the goal, by repeatedly

   205 calling \texttt{etac~rev_mp}.  Then, it uses \texttt{asm_full_simp_tac} or

   206 \texttt{ssubst} to substitute throughout the subgoal.  (If the equality

   207 involves unknowns then it must use \texttt{ssubst}.)  Then, it deletes the

   208 equality.  Finally, it moves the assumptions back to their original positions

   209 by calling \hbox{\tt resolve_tac\ts[imp_intr]}.

   210

   211 \index{equality|)}\index{tactics!substitution|)}

   212

   213

   214 %%% Local Variables:

   215 %%% mode: latex

   216 %%% TeX-master: "ref"

   217 %%% End:
`