1 |
|
2 \chapter{Tactics} \label{tactics} |
|
3 \index{tactics|(} |
|
4 |
|
5 \section{Other basic tactics} |
|
6 |
|
7 \subsection{Inserting premises and facts}\label{cut_facts_tac} |
|
8 \index{tactics!for inserting facts}\index{assumptions!inserting} |
|
9 \begin{ttbox} |
|
10 cut_facts_tac : thm list -> int -> tactic |
|
11 \end{ttbox} |
|
12 These tactics add assumptions to a subgoal. |
|
13 \begin{ttdescription} |
|
14 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] |
|
15 adds the {\it thms} as new assumptions to subgoal~$i$. Once they have |
|
16 been inserted as assumptions, they become subject to tactics such as {\tt |
|
17 eresolve_tac} and {\tt rewrite_goals_tac}. Only rules with no premises |
|
18 are inserted: Isabelle cannot use assumptions that contain $\Imp$ |
|
19 or~$\Forall$. Sometimes the theorems are premises of a rule being |
|
20 derived, returned by~{\tt goal}; instead of calling this tactic, you |
|
21 could state the goal with an outermost meta-quantifier. |
|
22 |
|
23 \end{ttdescription} |
|
24 |
|
25 |
|
26 \subsection{Composition: resolution without lifting} |
|
27 \index{tactics!for composition} |
|
28 \begin{ttbox} |
|
29 compose_tac: (bool * thm * int) -> int -> tactic |
|
30 \end{ttbox} |
|
31 {\bf Composing} two rules means resolving them without prior lifting or |
|
32 renaming of unknowns. This low-level operation, which underlies the |
|
33 resolution tactics, may occasionally be useful for special effects. |
|
34 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a |
|
35 rule, then passes the result to {\tt compose_tac}. |
|
36 \begin{ttdescription} |
|
37 \item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$] |
|
38 refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to |
|
39 have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need |
|
40 not be atomic; thus $m$ determines the number of new subgoals. If |
|
41 $flag$ is {\tt true} then it performs elim-resolution --- it solves the |
|
42 first premise of~$rule$ by assumption and deletes that assumption. |
|
43 \end{ttdescription} |
|
44 |
|
45 |
|
46 \section{*Managing lots of rules} |
|
47 These operations are not intended for interactive use. They are concerned |
|
48 with the processing of large numbers of rules in automatic proof |
|
49 strategies. Higher-order resolution involving a long list of rules is |
|
50 slow. Filtering techniques can shorten the list of rules given to |
|
51 resolution, and can also detect whether a subgoal is too flexible, |
|
52 with too many rules applicable. |
|
53 |
|
54 \subsection{Combined resolution and elim-resolution} \label{biresolve_tac} |
|
55 \index{tactics!resolution} |
|
56 \begin{ttbox} |
|
57 biresolve_tac : (bool*thm)list -> int -> tactic |
|
58 bimatch_tac : (bool*thm)list -> int -> tactic |
|
59 subgoals_of_brl : bool*thm -> int |
|
60 lessb : (bool*thm) * (bool*thm) -> bool |
|
61 \end{ttbox} |
|
62 {\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs. For each |
|
63 pair, it applies resolution if the flag is~{\tt false} and |
|
64 elim-resolution if the flag is~{\tt true}. A single tactic call handles a |
|
65 mixture of introduction and elimination rules. |
|
66 |
|
67 \begin{ttdescription} |
|
68 \item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] |
|
69 refines the proof state by resolution or elim-resolution on each rule, as |
|
70 indicated by its flag. It affects subgoal~$i$ of the proof state. |
|
71 |
|
72 \item[\ttindexbold{bimatch_tac}] |
|
73 is like {\tt biresolve_tac}, but performs matching: unknowns in the |
|
74 proof state are never updated (see~{\S}\ref{match_tac}). |
|
75 |
|
76 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] |
|
77 returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the |
|
78 pair (if applied to a suitable subgoal). This is $n$ if the flag is |
|
79 {\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number |
|
80 of premises of the rule. Elim-resolution yields one fewer subgoal than |
|
81 ordinary resolution because it solves the major premise by assumption. |
|
82 |
|
83 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] |
|
84 returns the result of |
|
85 \begin{ttbox} |
|
86 subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2} |
|
87 \end{ttbox} |
|
88 \end{ttdescription} |
|
89 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it |
|
90 (flag,rule)$ pairs by the number of new subgoals they will yield. Thus, |
|
91 those that yield the fewest subgoals should be tried first. |
|
92 |
|
93 |
|
94 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac} |
|
95 \index{discrimination nets|bold} |
|
96 \index{tactics!resolution} |
|
97 \begin{ttbox} |
|
98 net_resolve_tac : thm list -> int -> tactic |
|
99 net_match_tac : thm list -> int -> tactic |
|
100 net_biresolve_tac: (bool*thm) list -> int -> tactic |
|
101 net_bimatch_tac : (bool*thm) list -> int -> tactic |
|
102 filt_resolve_tac : thm list -> int -> int -> tactic |
|
103 could_unify : term*term->bool |
|
104 filter_thms : (term*term->bool) -> int*term*thm list -> thm{\ts}list |
|
105 \end{ttbox} |
|
106 The module {\tt Net} implements a discrimination net data structure for |
|
107 fast selection of rules \cite[Chapter 14]{charniak80}. A term is |
|
108 classified by the symbol list obtained by flattening it in preorder. |
|
109 The flattening takes account of function applications, constants, and free |
|
110 and bound variables; it identifies all unknowns and also regards |
|
111 \index{lambda abs@$\lambda$-abstractions} |
|
112 $\lambda$-abstractions as unknowns, since they could $\eta$-contract to |
|
113 anything. |
|
114 |
|
115 A discrimination net serves as a polymorphic dictionary indexed by terms. |
|
116 The module provides various functions for inserting and removing items from |
|
117 nets. It provides functions for returning all items whose term could match |
|
118 or unify with a target term. The matching and unification tests are |
|
119 overly lax (due to the identifications mentioned above) but they serve as |
|
120 useful filters. |
|
121 |
|
122 A net can store introduction rules indexed by their conclusion, and |
|
123 elimination rules indexed by their major premise. Isabelle provides |
|
124 several functions for `compiling' long lists of rules into fast |
|
125 resolution tactics. When supplied with a list of theorems, these functions |
|
126 build a discrimination net; the net is used when the tactic is applied to a |
|
127 goal. To avoid repeatedly constructing the nets, use currying: bind the |
|
128 resulting tactics to \ML{} identifiers. |
|
129 |
|
130 \begin{ttdescription} |
|
131 \item[\ttindexbold{net_resolve_tac} {\it thms}] |
|
132 builds a discrimination net to obtain the effect of a similar call to {\tt |
|
133 resolve_tac}. |
|
134 |
|
135 \item[\ttindexbold{net_match_tac} {\it thms}] |
|
136 builds a discrimination net to obtain the effect of a similar call to {\tt |
|
137 match_tac}. |
|
138 |
|
139 \item[\ttindexbold{net_biresolve_tac} {\it brls}] |
|
140 builds a discrimination net to obtain the effect of a similar call to {\tt |
|
141 biresolve_tac}. |
|
142 |
|
143 \item[\ttindexbold{net_bimatch_tac} {\it brls}] |
|
144 builds a discrimination net to obtain the effect of a similar call to {\tt |
|
145 bimatch_tac}. |
|
146 |
|
147 \item[\ttindexbold{filt_resolve_tac} {\it thms} {\it maxr} {\it i}] |
|
148 uses discrimination nets to extract the {\it thms} that are applicable to |
|
149 subgoal~$i$. If more than {\it maxr\/} theorems are applicable then the |
|
150 tactic fails. Otherwise it calls {\tt resolve_tac}. |
|
151 |
|
152 This tactic helps avoid runaway instantiation of unknowns, for example in |
|
153 type inference. |
|
154 |
|
155 \item[\ttindexbold{could_unify} ({\it t},{\it u})] |
|
156 returns {\tt false} if~$t$ and~$u$ are `obviously' non-unifiable, and |
|
157 otherwise returns~{\tt true}. It assumes all variables are distinct, |
|
158 reporting that {\tt ?a=?a} may unify with {\tt 0=1}. |
|
159 |
|
160 \item[\ttindexbold{filter_thms} $could\; (limit,prem,thms)$] |
|
161 returns the list of potentially resolvable rules (in {\it thms\/}) for the |
|
162 subgoal {\it prem}, using the predicate {\it could\/} to compare the |
|
163 conclusion of the subgoal with the conclusion of each rule. The resulting list |
|
164 is no longer than {\it limit}. |
|
165 \end{ttdescription} |
|
166 |
|
167 \index{tactics|)} |
|
168 |
|
169 |
|
170 %%% Local Variables: |
|
171 %%% mode: latex |
|
172 %%% TeX-master: "ref" |
|
173 %%% End: |
|