43 subgoal~$i$ of the proof state. |
43 subgoal~$i$ of the proof state. |
44 |
44 |
45 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] |
45 \item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] |
46 \index{elim-resolution} |
46 \index{elim-resolution} |
47 performs elim-resolution with the rules, which should normally be |
47 performs elim-resolution with the rules, which should normally be |
48 elimination rules. It resolves with a rule, solves its first premise by |
48 elimination rules. It resolves with a rule, proves its first premise by |
49 assumption, and finally {\em deletes\/} that assumption from any new |
49 assumption, and finally \emph{deletes} that assumption from any new |
50 subgoals. |
50 subgoals. (To rotate a rule's premises, |
|
51 see \texttt{rotate_prems} in~\S\ref{MiscellaneousForwardRules}.) |
51 |
52 |
52 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] |
53 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] |
53 \index{forward proof}\index{destruct-resolution} |
54 \index{forward proof}\index{destruct-resolution} |
54 performs destruct-resolution with the rules, which normally should |
55 performs destruct-resolution with the rules, which normally should |
55 be destruction rules. This replaces an assumption by the result of |
56 be destruction rules. This replaces an assumption by the result of |
71 \item[\ttindexbold{assume_tac} {\it i}] |
72 \item[\ttindexbold{assume_tac} {\it i}] |
72 attempts to solve subgoal~$i$ by assumption. |
73 attempts to solve subgoal~$i$ by assumption. |
73 |
74 |
74 \item[\ttindexbold{eq_assume_tac}] |
75 \item[\ttindexbold{eq_assume_tac}] |
75 is like {\tt assume_tac} but does not use unification. It succeeds (with a |
76 is like {\tt assume_tac} but does not use unification. It succeeds (with a |
76 {\em unique\/} next state) if one of the assumptions is identical to the |
77 \emph{unique} next state) if one of the assumptions is identical to the |
77 subgoal's conclusion. Since it does not instantiate variables, it cannot |
78 subgoal's conclusion. Since it does not instantiate variables, it cannot |
78 make other subgoals unprovable. It is intended to be called from proof |
79 make other subgoals unprovable. It is intended to be called from proof |
79 strategies, not interactively. |
80 strategies, not interactively. |
80 \end{ttdescription} |
81 \end{ttdescription} |
81 |
82 |
114 \end{ttbox} |
115 \end{ttbox} |
115 These tactics are designed for applying rules such as substitution and |
116 These tactics are designed for applying rules such as substitution and |
116 induction, which cause difficulties for higher-order unification. The |
117 induction, which cause difficulties for higher-order unification. The |
117 tactics accept explicit instantiations for unknowns in the rule --- |
118 tactics accept explicit instantiations for unknowns in the rule --- |
118 typically, in the rule's conclusion. Each instantiation is a pair |
119 typically, in the rule's conclusion. Each instantiation is a pair |
119 {\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading |
120 {\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading |
120 question mark! |
121 question mark! |
121 \begin{itemize} |
122 \begin{itemize} |
122 \item If $v$ is the type unknown {\tt'a}, then |
123 \item If $v$ is the type unknown {\tt'a}, then |
123 the rule must contain a type unknown \verb$?'a$ of some |
124 the rule must contain a type unknown \verb$?'a$ of some |
124 sort~$s$, and $e$ should be a type of sort $s$. |
125 sort~$s$, and $e$ should be a type of sort $s$. |