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