doc-src/Ref/substitution.tex
 changeset 104 d8205bb279a7 child 148 67d046de093e
equal inserted replaced
103:30bd42401ab2 104:d8205bb279a7

     1 %% $Id$

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

     3 \index{substitution|(}

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

     5 several kinds of equality reasoning.  {\bf Substitution} means to replace

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

     7 equality $t=u$, provided the logic possesses the appropriate rule ---

     8 unless you want to substitute even in the assumptions.  The tactic

     9 \ttindex{hyp_subst_tac} performs substitution in the assumptions, but it

    10 works via object-level implication, and therefore must be specially set up

    11 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 equalities.
       
    18 Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
       
    19 
       
    20 
       
    21 \section{Simple substitution}
       
    22 \index{substitution!simple}
       
    23 Many logics include a substitution rule of the form\indexbold{*subst}
       
    24 $$\List{\Var{a}=\Var{b}; \Var{P}(\Var{a})} \Imp     25 \Var{P}(\Var{b}) \eqno(subst)$$
       
    26 In backward proof, this may seem difficult to use: the conclusion
       
    27 $\Var{P}(\Var{b})$ admits far too many unifiers.  But, if the theorem {\tt
       
    28 eqth} asserts $t=u$, then \hbox{\tt eqth RS subst} is the derived rule
       
    29 $\Var{P}(t) \Imp \Var{P}(u).$
       
    30 Provided $u$ is not an unknown, resolution with this rule is
       
    31 well-behaved.\footnote{Unifying $\Var{P}(u)$ with a formula~$Q$
       
    32 expresses~$Q$ in terms of its dependence upon~$u$.  There are still $2^k$
       
    33 unifiers, if $Q$ has $k$ occurrences of~$u$, but Isabelle ensures that
       
    34 the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in
       
    35 subgoal~$i$, use
       
    36 \begin{ttbox} 
       
    37 resolve_tac [eqth RS subst] $$i$$ {\it.}
       
    38 \end{ttbox}
       
    39 To replace $t$ by~$u$ in
       
    40 subgoal~$i$, use
       
    41 \begin{ttbox} 
       
    42 resolve_tac [eqth RS ssubst] $$i$$ {\it,}
       
    43 \end{ttbox}
       
    44 where \ttindexbold{ssubst} is the swapped' substitution rule

    45 $$\List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp     46 \Var{P}(\Var{a}). \eqno(ssubst)$$

    47 If \ttindex{sym} denotes the symmetry rule

    48 $$\Var{a}=\Var{b}\Imp\Var{b}=\Var{a}$$, then {\tt ssubst} is just

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

    50 subst} and {\tt ssubst}, as well as {\tt refl}, {\tt sym} and {\tt trans}

    51 (for the usual equality laws).

    52

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

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

    55 \begin{ttbox}

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

    57 \end{ttbox}

    58

    59

    60 \section{Substitution in the hypotheses}

    61 \index{substitution!in hypotheses}

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

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

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

    65 Calling \hbox{\tt eresolve_tac [ssubst] $$i$$} simply discards the

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

    67 work out a solution.  First apply \hbox{\tt eresolve_tac [subst] $$i$$},

    68 replacing~$a$ by~$c$:

    69 $\List{c=b} \Imp c=b$

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

    71 nothing more sophisticated than substitution in the assumptions.

    72 Object-logics that include the rule~$(subst)$ provide a tactic for this

    73 purpose:

    74 \begin{ttbox}

    75 hyp_subst_tac : int -> tactic

    76 \end{ttbox}

    77 \begin{description}

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

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

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

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

    82 \end{description}

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

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

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

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

    87 in the subgoal!

    88

    89 Replacing a free variable causes similar problems if they appear in the

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

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

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

    93 \ttindex{cut_facts_tac} to insert the atomic premises as object-level

    94 assumptions.

    95

    96

    97 \section{Setting up {\tt hyp_subst_tac}}

    98 Many Isabelle object-logics, such as {\tt FOL}, {\tt HOL} and their

    99 descendants, come with {\tt hyp_subst_tac} already defined.  A few others,

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

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

   102 rule and implication, you must set up {\tt hyp_subst_tac} yourself.  It

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

   104 argument signature~\ttindexbold{HYPSUBST_DATA}:

   105 \begin{ttbox}

   106 signature HYPSUBST_DATA =

   107   sig

   108   val subst      : thm

   109   val sym        : thm

   110   val rev_cut_eq : thm

   111   val imp_intr   : thm

   112   val rev_mp     : thm

   113   val dest_eq    : term -> term*term

   114   end;

   115 \end{ttbox}

   116 Thus, the functor requires the following items:

   117 \begin{description}

   118 \item[\ttindexbold{subst}] should be the substitution rule

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

   120

   121 \item[\ttindexbold{sym}] should be the symmetry rule

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

   123

   124 \item[\ttindexbold{rev_cut_eq}] should have the form

   125 $\List{\Var{a}=\Var{b};\; \Var{a}=\Var{b}\Imp\Var{R}} \Imp \Var{R}$.

   126

   127 \item[\ttindexbold{imp_intr}] should be the implies introduction

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

   129

   130 \item[\ttindexbold{rev_mp}] should be the reversed'' implies elimination

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

   132

   133 \item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when

   134 applied to the \ML{} term that represents~$t=u$.  For other terms, it

   135 should raise exception~\ttindex{Match}.

   136 \end{description}

   137 The functor resides in {\tt Provers/hypsubst.ML} on the Isabelle

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

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

   140 and implication symbols, or the types of formula and terms.  Coding the

   141 function {\tt dest_eq} requires knowledge of Isabelle's representation of

   142 terms.  For {\tt FOL} it is defined by

   143 \begin{ttbox}

   144 fun dest_eq (Const("Trueprop",_) $(Const("op =",_)$t$u)) = (t,u);    145 \end{ttbox}    146 Here {\tt Trueprop} is the coercion from type'~$o$to type~$prop$, while    147 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.    148 Pattern-matching expresses the function concisely, using wildcards~({\tt_})    149 to hide the types.    150     151 Given a subgoal of the form    152 $\List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q,$    153 \ttindexbold{hyp_subst_tac} locates a suitable equality    154 assumption and moves it to the last position using elim-resolution on {\tt    155 rev_cut_eq} (possibly re-orienting it using~{\tt sym}):    156 $\List{P@1; \cdots ; P@n; t=u} \Imp Q$    157 Using$n$calls of \hbox{\tt eresolve_tac [rev_mp]}, it creates the subgoal    158 $\List{t=u} \Imp P@1\imp \cdots \imp P@n \imp Q$    159 By \hbox{\tt eresolve_tac [ssubst]}, it replaces~$t$by~$u$throughout:    160 $P'@1\imp \cdots \imp P'@n \imp Q'$    161 Finally, using$n$calls of \hbox{\tt resolve_tac [imp_intr]}, it restores    162$P'@1$, \ldots,$P'@n\$ as assumptions:

   163 $\List{P'@n; \cdots ; P'@1} \Imp Q'$

   164

   165 \index{substitution|)}