author | oheimb |
Fri, 01 May 1998 22:40:20 +0200 | |
changeset 4885 | 54fa88124d52 |
parent 4881 | d80faf83c82f |
child 5371 | e27558a68b8d |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
319 | 2 |
\chapter{The Classical Reasoner}\label{chap:classical} |
286 | 3 |
\index{classical reasoner|(} |
308 | 4 |
\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} |
5 |
||
3108 | 6 |
Although Isabelle is generic, many users will be working in some |
7 |
extension of classical first-order logic. Isabelle's set theory~{\tt |
|
4398 | 8 |
ZF} is built upon theory~\texttt{FOL}, while {\HOL} |
3108 | 9 |
conceptually contains first-order logic as a fragment. |
10 |
Theorem-proving in predicate logic is undecidable, but many |
|
308 | 11 |
researchers have developed strategies to assist in this task. |
104 | 12 |
|
286 | 13 |
Isabelle's classical reasoner is an \ML{} functor that accepts certain |
104 | 14 |
information about a logic and delivers a suite of automatic tactics. Each |
15 |
tactic takes a collection of rules and executes a simple, non-clausal proof |
|
16 |
procedure. They are slow and simplistic compared with resolution theorem |
|
17 |
provers, but they can save considerable time and effort. They can prove |
|
18 |
theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in |
|
19 |
seconds: |
|
20 |
\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x)) |
|
21 |
\imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \] |
|
22 |
\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x)) |
|
23 |
\imp \neg (\exists z. \forall x. F(x,z)) |
|
24 |
\] |
|
308 | 25 |
% |
26 |
The tactics are generic. They are not restricted to first-order logic, and |
|
27 |
have been heavily used in the development of Isabelle's set theory. Few |
|
28 |
interactive proof assistants provide this much automation. The tactics can |
|
29 |
be traced, and their components can be called directly; in this manner, |
|
30 |
any proof can be viewed interactively. |
|
104 | 31 |
|
3716 | 32 |
The simplest way to apply the classical reasoner (to subgoal~$i$) is to type |
2479 | 33 |
\begin{ttbox} |
3089 | 34 |
by (Blast_tac \(i\)); |
2479 | 35 |
\end{ttbox} |
3716 | 36 |
This command quickly proves most simple formulas of the predicate calculus or |
37 |
set theory. To attempt to prove \emph{all} subgoals using a combination of |
|
38 |
rewriting and classical reasoning, try |
|
3224 | 39 |
\begin{ttbox} |
4507 | 40 |
by Auto_tac; |
3224 | 41 |
\end{ttbox} |
3716 | 42 |
To do all obvious logical steps, even if they do not prove the |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
43 |
subgoal, type one of the following: |
3716 | 44 |
\begin{ttbox} |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
45 |
by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
46 |
by Safe_tac; \emph{\textrm{applies to all subgoals}} |
3716 | 47 |
\end{ttbox} |
48 |
You need to know how the classical reasoner works in order to use it |
|
49 |
effectively. There are many tactics to choose from, including {\tt |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
50 |
Fast_tac} and \texttt{Best_tac}. |
2479 | 51 |
|
3108 | 52 |
We shall first discuss the underlying principles, then present the |
53 |
classical reasoner. Finally, we shall see how to instantiate it for |
|
54 |
new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already |
|
55 |
installed. |
|
104 | 56 |
|
57 |
||
58 |
\section{The sequent calculus} |
|
59 |
\index{sequent calculus} |
|
60 |
Isabelle supports natural deduction, which is easy to use for interactive |
|
61 |
proof. But natural deduction does not easily lend itself to automation, |
|
62 |
and has a bias towards intuitionism. For certain proofs in classical |
|
63 |
logic, it can not be called natural. The {\bf sequent calculus}, a |
|
64 |
generalization of natural deduction, is easier to automate. |
|
65 |
||
66 |
A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$ |
|
308 | 67 |
and~$\Delta$ are sets of formulae.% |
68 |
\footnote{For first-order logic, sequents can equivalently be made from |
|
69 |
lists or multisets of formulae.} The sequent |
|
104 | 70 |
\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \] |
71 |
is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj |
|
72 |
Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true, |
|
73 |
while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf |
|
74 |
basic} if its left and right sides have a common formula, as in $P,Q\turn |
|
75 |
Q,R$; basic sequents are trivially valid. |
|
76 |
||
77 |
Sequent rules are classified as {\bf right} or {\bf left}, indicating which |
|
78 |
side of the $\turn$~symbol they operate on. Rules that operate on the |
|
79 |
right side are analogous to natural deduction's introduction rules, and |
|
308 | 80 |
left rules are analogous to elimination rules. |
81 |
Recall the natural deduction rules for |
|
82 |
first-order logic, |
|
83 |
\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}% |
|
84 |
{Fig.\ts\ref{fol-fig}}. |
|
85 |
The sequent calculus analogue of~$({\imp}I)$ is the rule |
|
3108 | 86 |
$$ |
87 |
\ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q} |
|
88 |
\eqno({\imp}R) |
|
89 |
$$ |
|
104 | 90 |
This breaks down some implication on the right side of a sequent; $\Gamma$ |
91 |
and $\Delta$ stand for the sets of formulae that are unaffected by the |
|
92 |
inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the |
|
93 |
single rule |
|
3108 | 94 |
$$ |
95 |
\ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q} |
|
96 |
\eqno({\disj}R) |
|
97 |
$$ |
|
104 | 98 |
This breaks down some disjunction on the right side, replacing it by both |
99 |
disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic. |
|
100 |
||
101 |
To illustrate the use of multiple formulae on the right, let us prove |
|
102 |
the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we |
|
103 |
reduce this formula to a basic sequent: |
|
104 |
\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)} |
|
105 |
{\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;} |
|
106 |
{\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad} |
|
107 |
{P, Q \turn Q, P\qquad\qquad}}} |
|
108 |
\] |
|
109 |
This example is typical of the sequent calculus: start with the desired |
|
110 |
theorem and apply rules backwards in a fairly arbitrary manner. This yields a |
|
111 |
surprisingly effective proof procedure. Quantifiers add few complications, |
|
112 |
since Isabelle handles parameters and schematic variables. See Chapter~10 |
|
113 |
of {\em ML for the Working Programmer}~\cite{paulson91} for further |
|
114 |
discussion. |
|
115 |
||
116 |
||
117 |
\section{Simulating sequents by natural deduction} |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
118 |
Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@. |
104 | 119 |
But natural deduction is easier to work with, and most object-logics employ |
120 |
it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn |
|
121 |
Q@1,\ldots,Q@n$ by the Isabelle formula |
|
122 |
\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \] |
|
123 |
where the order of the assumptions and the choice of~$Q@1$ are arbitrary. |
|
124 |
Elim-resolution plays a key role in simulating sequent proofs. |
|
125 |
||
126 |
We can easily handle reasoning on the left. |
|
308 | 127 |
As discussed in |
128 |
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, |
|
104 | 129 |
elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ |
130 |
achieves a similar effect as the corresponding sequent rules. For the |
|
131 |
other connectives, we use sequent-style elimination rules instead of |
|
308 | 132 |
destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that |
133 |
the rule $(\neg L)$ has no effect under our representation of sequents! |
|
3108 | 134 |
$$ |
135 |
\ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L) |
|
136 |
$$ |
|
104 | 137 |
What about reasoning on the right? Introduction rules can only affect the |
308 | 138 |
formula in the conclusion, namely~$Q@1$. The other right-side formulae are |
319 | 139 |
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. |
140 |
\index{assumptions!negated} |
|
141 |
In order to operate on one of these, it must first be exchanged with~$Q@1$. |
|
104 | 142 |
Elim-resolution with the {\bf swap} rule has this effect: |
3108 | 143 |
$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$ |
104 | 144 |
To ensure that swaps occur only when necessary, each introduction rule is |
145 |
converted into a swapped form: it is resolved with the second premise |
|
146 |
of~$(swap)$. The swapped form of~$({\conj}I)$, which might be |
|
147 |
called~$({\neg\conj}E)$, is |
|
148 |
\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \] |
|
149 |
Similarly, the swapped form of~$({\imp}I)$ is |
|
150 |
\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \] |
|
151 |
Swapped introduction rules are applied using elim-resolution, which deletes |
|
152 |
the negated formula. Our representation of sequents also requires the use |
|
153 |
of ordinary introduction rules. If we had no regard for readability, we |
|
154 |
could treat the right side more uniformly by representing sequents as |
|
155 |
\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \] |
|
156 |
||
157 |
||
158 |
\section{Extra rules for the sequent calculus} |
|
159 |
As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$ |
|
160 |
must be replaced by sequent-style elimination rules. In addition, we need |
|
161 |
rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj |
|
162 |
Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that |
|
163 |
simulates $({\disj}R)$: |
|
164 |
\[ (\neg Q\Imp P) \Imp P\disj Q \] |
|
165 |
The destruction rule $({\imp}E)$ is replaced by |
|
332 | 166 |
\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \] |
104 | 167 |
Quantifier replication also requires special rules. In classical logic, |
308 | 168 |
$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules |
169 |
$(\exists R)$ and $(\forall L)$ are dual: |
|
104 | 170 |
\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P} |
171 |
{\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R) |
|
172 |
\qquad |
|
173 |
\ainfer{\forall x{.}P, \Gamma &\turn \Delta} |
|
174 |
{P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L) |
|
175 |
\] |
|
176 |
Thus both kinds of quantifier may be replicated. Theorems requiring |
|
177 |
multiple uses of a universal formula are easy to invent; consider |
|
308 | 178 |
\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \] |
179 |
for any~$n>1$. Natural examples of the multiple use of an existential |
|
180 |
formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$. |
|
104 | 181 |
|
182 |
Forgoing quantifier replication loses completeness, but gains decidability, |
|
183 |
since the search space becomes finite. Many useful theorems can be proved |
|
184 |
without replication, and the search generally delivers its verdict in a |
|
185 |
reasonable time. To adopt this approach, represent the sequent rules |
|
186 |
$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists |
|
187 |
E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination |
|
188 |
form: |
|
189 |
$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$ |
|
190 |
Elim-resolution with this rule will delete the universal formula after a |
|
191 |
single use. To replicate universal quantifiers, replace the rule by |
|
3108 | 192 |
$$ |
193 |
\List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q. |
|
194 |
\eqno(\forall E@3) |
|
195 |
$$ |
|
104 | 196 |
To replicate existential quantifiers, replace $(\exists I)$ by |
332 | 197 |
\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \] |
104 | 198 |
All introduction rules mentioned above are also useful in swapped form. |
199 |
||
200 |
Replication makes the search space infinite; we must apply the rules with |
|
286 | 201 |
care. The classical reasoner distinguishes between safe and unsafe |
104 | 202 |
rules, applying the latter only when there is no alternative. Depth-first |
203 |
search may well go down a blind alley; best-first search is better behaved |
|
204 |
in an infinite search space. However, quantifier replication is too |
|
205 |
expensive to prove any but the simplest theorems. |
|
206 |
||
207 |
||
208 |
\section{Classical rule sets} |
|
319 | 209 |
\index{classical sets} |
210 |
Each automatic tactic takes a {\bf classical set} --- a collection of |
|
104 | 211 |
rules, classified as introduction or elimination and as {\bf safe} or {\bf |
212 |
unsafe}. In general, safe rules can be attempted blindly, while unsafe |
|
213 |
rules must be used with care. A safe rule must never reduce a provable |
|
308 | 214 |
goal to an unprovable set of subgoals. |
104 | 215 |
|
308 | 216 |
The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any |
217 |
rule is unsafe whose premises contain new unknowns. The elimination |
|
218 |
rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution, |
|
219 |
which discards the assumption $\forall x{.}P(x)$ and replaces it by the |
|
220 |
weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for |
|
221 |
similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense: |
|
222 |
since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping. |
|
223 |
In classical first-order logic, all rules are safe except those mentioned |
|
224 |
above. |
|
104 | 225 |
|
226 |
The safe/unsafe distinction is vague, and may be regarded merely as a way |
|
227 |
of giving some rules priority over others. One could argue that |
|
228 |
$({\disj}E)$ is unsafe, because repeated application of it could generate |
|
229 |
exponentially many subgoals. Induction rules are unsafe because inductive |
|
230 |
proofs are difficult to set up automatically. Any inference is unsafe that |
|
231 |
instantiates an unknown in the proof state --- thus \ttindex{match_tac} |
|
232 |
must be used, rather than \ttindex{resolve_tac}. Even proof by assumption |
|
233 |
is unsafe if it instantiates unknowns shared with other subgoals --- thus |
|
234 |
\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. |
|
235 |
||
1099 | 236 |
\subsection{Adding rules to classical sets} |
319 | 237 |
Classical rule sets belong to the abstract type \mltydx{claset}, which |
286 | 238 |
supports the following operations (provided the classical reasoner is |
104 | 239 |
installed!): |
240 |
\begin{ttbox} |
|
1099 | 241 |
empty_cs : claset |
242 |
print_cs : claset -> unit |
|
4665 | 243 |
rep_cs : claset -> {safeEs: thm list, safeIs: thm list, |
244 |
hazEs: thm list, hazIs: thm list, |
|
245 |
swrappers: (string * wrapper) list, |
|
246 |
uwrappers: (string * wrapper) list, |
|
247 |
safe0_netpair: netpair, safep_netpair: netpair, |
|
248 |
haz_netpair: netpair, dup_netpair: netpair} |
|
1099 | 249 |
addSIs : claset * thm list -> claset \hfill{\bf infix 4} |
250 |
addSEs : claset * thm list -> claset \hfill{\bf infix 4} |
|
251 |
addSDs : claset * thm list -> claset \hfill{\bf infix 4} |
|
252 |
addIs : claset * thm list -> claset \hfill{\bf infix 4} |
|
253 |
addEs : claset * thm list -> claset \hfill{\bf infix 4} |
|
254 |
addDs : claset * thm list -> claset \hfill{\bf infix 4} |
|
1869 | 255 |
delrules : claset * thm list -> claset \hfill{\bf infix 4} |
104 | 256 |
\end{ttbox} |
3089 | 257 |
The add operations ignore any rule already present in the claset with the same |
258 |
classification (such as Safe Introduction). They print a warning if the rule |
|
259 |
has already been added with some other classification, but add the rule |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
260 |
anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the |
3089 | 261 |
claset, but see the warning below concerning destruction rules. |
308 | 262 |
\begin{ttdescription} |
104 | 263 |
\item[\ttindexbold{empty_cs}] is the empty classical set. |
264 |
||
4665 | 265 |
\item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$, |
266 |
which is the rules. All other parts are non-printable. |
|
267 |
||
268 |
\item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal |
|
4666 | 269 |
components, namely the safe introduction and elimination rules, the unsafe |
270 |
introduction and elimination rules, the lists of safe and unsafe wrappers |
|
271 |
(see \ref{sec:modifying-search}), and the internalized forms of the rules. |
|
1099 | 272 |
|
308 | 273 |
\item[$cs$ addSIs $rules$] \indexbold{*addSIs} |
274 |
adds safe introduction~$rules$ to~$cs$. |
|
104 | 275 |
|
308 | 276 |
\item[$cs$ addSEs $rules$] \indexbold{*addSEs} |
277 |
adds safe elimination~$rules$ to~$cs$. |
|
104 | 278 |
|
308 | 279 |
\item[$cs$ addSDs $rules$] \indexbold{*addSDs} |
280 |
adds safe destruction~$rules$ to~$cs$. |
|
104 | 281 |
|
308 | 282 |
\item[$cs$ addIs $rules$] \indexbold{*addIs} |
283 |
adds unsafe introduction~$rules$ to~$cs$. |
|
104 | 284 |
|
308 | 285 |
\item[$cs$ addEs $rules$] \indexbold{*addEs} |
286 |
adds unsafe elimination~$rules$ to~$cs$. |
|
104 | 287 |
|
308 | 288 |
\item[$cs$ addDs $rules$] \indexbold{*addDs} |
289 |
adds unsafe destruction~$rules$ to~$cs$. |
|
1869 | 290 |
|
291 |
\item[$cs$ delrules $rules$] \indexbold{*delrules} |
|
3089 | 292 |
deletes~$rules$ from~$cs$. It prints a warning for those rules that are not |
293 |
in~$cs$. |
|
308 | 294 |
\end{ttdescription} |
295 |
||
3089 | 296 |
\begin{warn} |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
297 |
If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete |
3089 | 298 |
it as follows: |
299 |
\begin{ttbox} |
|
300 |
\(cs\) delrules [make_elim \(rule\)] |
|
301 |
\end{ttbox} |
|
302 |
\par\noindent |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
303 |
This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert |
3089 | 304 |
the destruction rules to elimination rules by applying \ttindex{make_elim}, |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
305 |
and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively. |
3089 | 306 |
\end{warn} |
307 |
||
104 | 308 |
Introduction rules are those that can be applied using ordinary resolution. |
309 |
The classical set automatically generates their swapped forms, which will |
|
310 |
be applied using elim-resolution. Elimination rules are applied using |
|
286 | 311 |
elim-resolution. In a classical set, rules are sorted by the number of new |
312 |
subgoals they will yield; rules that generate the fewest subgoals will be |
|
313 |
tried first (see \S\ref{biresolve_tac}). |
|
104 | 314 |
|
1099 | 315 |
|
316 |
\subsection{Modifying the search step} |
|
4665 | 317 |
\label{sec:modifying-search} |
3716 | 318 |
For a given classical set, the proof strategy is simple. Perform as many safe |
319 |
inferences as possible; or else, apply certain safe rules, allowing |
|
320 |
instantiation of unknowns; or else, apply an unsafe rule. The tactics also |
|
321 |
eliminate assumptions of the form $x=t$ by substitution if they have been set |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
322 |
up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below). |
3716 | 323 |
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ |
324 |
and~$P$, then replace $P\imp Q$ by~$Q$. |
|
104 | 325 |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
326 |
The classical reasoning tactics --- except \texttt{blast_tac}! --- allow |
4649 | 327 |
you to modify this basic proof strategy by applying two lists of arbitrary |
328 |
{\bf wrapper tacticals} to it. |
|
329 |
The first wrapper list, which is considered to contain safe wrappers only, |
|
330 |
affects \ttindex{safe_step_tac} and all the tactics that call it. |
|
331 |
The second one, which may contain unsafe wrappers, affects \ttindex{step_tac}, |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
332 |
\ttindex{slow_step_tac}, and the tactics that call them. |
4649 | 333 |
A wrapper transforms each step of the search, for example |
334 |
by invoking other tactics before or alternatively to the original step tactic. |
|
335 |
All members of a wrapper list are applied in turn to the respective step tactic. |
|
336 |
||
337 |
Initially the two wrapper lists are empty, which means no modification of the |
|
338 |
step tactics. Safe and unsafe wrappers are added to a claset |
|
339 |
with the functions given below, supplying them with wrapper names. |
|
340 |
These names may be used to selectively delete wrappers. |
|
1099 | 341 |
|
342 |
\begin{ttbox} |
|
4649 | 343 |
type wrapper = (int -> tactic) -> (int -> tactic); |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
344 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
345 |
addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} |
4649 | 346 |
addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
347 |
addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
348 |
delSWrapper : claset * string -> claset \hfill{\bf infix 4} |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
349 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
350 |
addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} |
4649 | 351 |
addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
352 |
addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} |
|
353 |
delWrapper : claset * string -> claset \hfill{\bf infix 4} |
|
354 |
||
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
355 |
addSss : claset * simpset -> claset \hfill{\bf infix 4} |
2632 | 356 |
addss : claset * simpset -> claset \hfill{\bf infix 4} |
1099 | 357 |
\end{ttbox} |
358 |
% |
|
359 |
||
360 |
\begin{ttdescription} |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
361 |
\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
362 |
adds a new wrapper, which should yield a safe tactic, |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
363 |
to modify the existing safe step tactic. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
364 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
365 |
\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
366 |
adds the given tactic as safe wrapper, such that it is |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
367 |
applied {\em before} each safe step of the search. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
368 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
369 |
\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
370 |
adds the given tactic as safe wrapper, such that it is |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
371 |
applied when a safe step of the search would fail. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
372 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
373 |
\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
374 |
deletes the safe wrapper with the given name. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
375 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
376 |
\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
377 |
adds a new wrapper to modify the existing (unsafe) step tactic. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
378 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
379 |
\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
380 |
adds the given tactic as unsafe wrapper, such that it is |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
381 |
applied {\em before} each step of the search. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
382 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
383 |
\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
384 |
adds the given tactic as unsafe wrapper, such that it is |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
385 |
applied when a step of the search would fail. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
386 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
387 |
\item[$cs$ delWrapper $name$] \indexbold{*delWrapper} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
388 |
deletes the unsafe wrapper with the given name. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
389 |
|
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
390 |
\item[$cs$ addSss $ss$] \indexbold{*addss} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
391 |
adds the simpset~$ss$ to the classical set. The assumptions and goal will be |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
392 |
simplified, in a rather safe way, after each safe step of the search. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
393 |
|
1099 | 394 |
\item[$cs$ addss $ss$] \indexbold{*addss} |
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset
|
395 |
adds the simpset~$ss$ to the classical set. The assumptions and goal will be |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
396 |
simplified, before the each unsafe step of the search. |
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset
|
397 |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
398 |
\end{ttdescription} |
2631
5e5c78ba955e
description of safe vs. unsafe wrapper and the functions involved
oheimb
parents:
2479
diff
changeset
|
399 |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
400 |
\index{simplification!from classical reasoner} The wrapper tacticals |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
401 |
underly the operators addss and addSss, which are used as primitives |
4885 | 402 |
for the automatic tactics described in \S\ref{sec:automatic-tactics}. |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
403 |
Strictly speaking, both operators are not part of the classical reasoner. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
404 |
They should be defined when the simplifier is installed: |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
405 |
\begin{ttbox} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
406 |
infix 4 addSss addss; |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
407 |
fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac", |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
408 |
CHANGED o (safe_asm_full_simp_tac ss)); |
4885 | 409 |
fun cs addss ss = cs addbefore ("asm_full_simp_tac", |
410 |
asm_full_simp_tac ss); |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
411 |
\end{ttbox} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
412 |
\begin{warn} |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
413 |
Being defined as wrappers, these operators are inappropriate for adding more |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
414 |
than one simpset at a time: the simpset added last overwrites any earlier ones. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
415 |
When a simpset combined with a claset is to be augmented, this should done |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
416 |
{\em before} combining it with the claset. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
417 |
\end{warn} |
1099 | 418 |
|
104 | 419 |
|
420 |
\section{The classical tactics} |
|
3716 | 421 |
\index{classical reasoner!tactics} If installed, the classical module provides |
422 |
powerful theorem-proving tactics. Most of them have capitalized analogues |
|
423 |
that use the default claset; see \S\ref{sec:current-claset}. |
|
424 |
||
425 |
\subsection{Semi-automatic tactics} |
|
426 |
\begin{ttbox} |
|
427 |
clarify_tac : claset -> int -> tactic |
|
428 |
clarify_step_tac : claset -> int -> tactic |
|
429 |
\end{ttbox} |
|
430 |
Use these when the automatic tactics fail. They perform all the obvious |
|
431 |
logical inferences that do not split the subgoal. The result is a |
|
432 |
simpler subgoal that can be tackled by other means, such as by |
|
433 |
instantiating quantifiers yourself. |
|
434 |
\begin{ttdescription} |
|
435 |
\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on |
|
4597
a0bdee64194c
Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents:
4561
diff
changeset
|
436 |
subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}. |
3716 | 437 |
|
438 |
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on |
|
439 |
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj |
|
440 |
B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be |
|
441 |
performed provided they do not instantiate unknowns. Assumptions of the |
|
442 |
form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is |
|
443 |
applied. |
|
444 |
\end{ttdescription} |
|
445 |
||
104 | 446 |
|
3224 | 447 |
\subsection{The tableau prover} |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
448 |
The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover, |
3224 | 449 |
coded directly in \ML. It then reconstructs the proof using Isabelle |
450 |
tactics. It is faster and more powerful than the other classical |
|
451 |
reasoning tactics, but has major limitations too. |
|
3089 | 452 |
\begin{itemize} |
453 |
\item It does not use the wrapper tacticals described above, such as |
|
454 |
\ttindex{addss}. |
|
455 |
\item It ignores types, which can cause problems in \HOL. If it applies a rule |
|
456 |
whose types are inappropriate, then proof reconstruction will fail. |
|
457 |
\item It does not perform higher-order unification, as needed by the rule {\tt |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
458 |
rangeI} in {\HOL} and \texttt{RepFunI} in {\ZF}. There are often |
3089 | 459 |
alternatives to such rules, for example {\tt |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
460 |
range_eqI} and \texttt{RepFun_eqI}. |
3089 | 461 |
\item The message {\small\tt Function Var's argument not a bound variable\ } |
462 |
relates to the lack of higher-order unification. Function variables |
|
463 |
may only be applied to parameters of the subgoal. |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
464 |
\item Its proof strategy is more general than \texttt{fast_tac}'s but can be |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
465 |
slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt |
3089 | 466 |
fast_tac} and the other tactics described below. |
467 |
\end{itemize} |
|
468 |
% |
|
469 |
\begin{ttbox} |
|
470 |
blast_tac : claset -> int -> tactic |
|
471 |
Blast.depth_tac : claset -> int -> int -> tactic |
|
472 |
Blast.trace : bool ref \hfill{\bf initially false} |
|
473 |
\end{ttbox} |
|
474 |
The two tactics differ on how they bound the number of unsafe steps used in a |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
475 |
proof. While \texttt{blast_tac} starts with a bound of zero and increases it |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
476 |
successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound. |
3089 | 477 |
\begin{ttdescription} |
478 |
\item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove |
|
479 |
subgoal~$i$ using iterative deepening to increase the search bound. |
|
480 |
||
481 |
\item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries |
|
482 |
to prove subgoal~$i$ using a search bound of $lim$. Often a slow |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
483 |
proof using \texttt{blast_tac} can be made much faster by supplying the |
3089 | 484 |
successful search bound to this tactic instead. |
485 |
||
4317 | 486 |
\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover} |
3089 | 487 |
causes the tableau prover to print a trace of its search. At each step it |
488 |
displays the formula currently being examined and reports whether the branch |
|
489 |
has been closed, extended or split. |
|
490 |
\end{ttdescription} |
|
491 |
||
3224 | 492 |
|
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
493 |
\subsection{Automatic tactics}\label{sec:automatic-tactics} |
3224 | 494 |
\begin{ttbox} |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
495 |
type clasimpset = claset * simpset; |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
496 |
auto_tac : clasimpset -> tactic |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
497 |
force_tac : clasimpset -> int -> tactic |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
498 |
auto : unit -> unit |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
499 |
force : int -> unit |
3224 | 500 |
\end{ttbox} |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
501 |
The automatic tactics attempt to prove goals using a combination of |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
502 |
simplification and classical reasoning. |
4885 | 503 |
\begin{ttdescription} |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
504 |
\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
505 |
there are a lot of mostly trivial subgoals; it proves all the easy ones, |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
506 |
leaving the ones it cannot prove. |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
507 |
(Unfortunately, attempting to prove the hard ones may take a long time.) |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
508 |
\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
509 |
completely. It tries to apply all fancy tactics it knows about, |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
510 |
performing a rather exhaustive search. |
4885 | 511 |
\end{ttdescription} |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
512 |
They must be supplied both a simpset and a claset; therefore |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
513 |
they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which |
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
514 |
use the default claset and simpset (see \S\ref{sec:current-claset} below). |
4885 | 515 |
For interactive use, |
516 |
the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} |
|
517 |
while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);} |
|
3224 | 518 |
|
519 |
\subsection{Other classical tactics} |
|
332 | 520 |
\begin{ttbox} |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
521 |
fast_tac : claset -> int -> tactic |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
522 |
best_tac : claset -> int -> tactic |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
523 |
slow_tac : claset -> int -> tactic |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
524 |
slow_best_tac : claset -> int -> tactic |
332 | 525 |
\end{ttbox} |
3224 | 526 |
These tactics attempt to prove a subgoal using sequent-style reasoning. |
527 |
Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
528 |
effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
529 |
this subgoal or fail. The \texttt{slow_} versions conduct a broader |
3224 | 530 |
search.% |
531 |
\footnote{They may, when backtracking from a failed proof attempt, undo even |
|
532 |
the step of proving a subgoal by assumption.} |
|
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
533 |
|
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
534 |
The best-first tactics are guided by a heuristic function: typically, the |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
535 |
total size of the proof state. This function is supplied in the functor call |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
536 |
that sets up the classical reasoner. |
332 | 537 |
\begin{ttdescription} |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
538 |
\item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using |
3089 | 539 |
depth-first search, to prove subgoal~$i$. |
332 | 540 |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
541 |
\item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using |
3089 | 542 |
best-first search, to prove subgoal~$i$. |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
543 |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
544 |
\item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using |
3089 | 545 |
depth-first search, to prove subgoal~$i$. |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
546 |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
547 |
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} using |
3089 | 548 |
best-first search, to prove subgoal~$i$. |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
549 |
\end{ttdescription} |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
550 |
|
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
551 |
|
3716 | 552 |
\subsection{Depth-limited automatic tactics} |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
553 |
\begin{ttbox} |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
554 |
depth_tac : claset -> int -> int -> tactic |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
555 |
deepen_tac : claset -> int -> int -> tactic |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
556 |
\end{ttbox} |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
557 |
These work by exhaustive search up to a specified depth. Unsafe rules are |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
558 |
modified to preserve the formula they act on, so that it be used repeatedly. |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
559 |
They can prove more goals than \texttt{fast_tac} can but are much |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
560 |
slower, for example if the assumptions have many universal quantifiers. |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
561 |
|
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
562 |
The depth limits the number of unsafe steps. If you can estimate the minimum |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
563 |
number of unsafe steps needed, supply this value as~$m$ to save time. |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
564 |
\begin{ttdescription} |
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
565 |
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] |
3089 | 566 |
tries to prove subgoal~$i$ by exhaustive search up to depth~$m$. |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
567 |
|
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
568 |
\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
569 |
tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac} |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
570 |
repeatedly with increasing depths, starting with~$m$. |
332 | 571 |
\end{ttdescription} |
572 |
||
573 |
||
104 | 574 |
\subsection{Single-step tactics} |
575 |
\begin{ttbox} |
|
576 |
safe_step_tac : claset -> int -> tactic |
|
577 |
safe_tac : claset -> tactic |
|
578 |
inst_step_tac : claset -> int -> tactic |
|
579 |
step_tac : claset -> int -> tactic |
|
580 |
slow_step_tac : claset -> int -> tactic |
|
581 |
\end{ttbox} |
|
582 |
The automatic proof procedures call these tactics. By calling them |
|
583 |
yourself, you can execute these procedures one step at a time. |
|
308 | 584 |
\begin{ttdescription} |
104 | 585 |
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
586 |
subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may |
3716 | 587 |
include proof by assumption or Modus Ponens (taking care not to instantiate |
588 |
unknowns), or substitution. |
|
104 | 589 |
|
590 |
\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all |
|
3716 | 591 |
subgoals. It is deterministic, with at most one outcome. |
104 | 592 |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
593 |
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac}, |
104 | 594 |
but allows unknowns to be instantiated. |
595 |
||
1099 | 596 |
\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
597 |
procedure. The (unsafe) wrapper tacticals are applied to a tactic that tries |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
598 |
\texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$. |
104 | 599 |
|
600 |
\item[\ttindexbold{slow_step_tac}] |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
601 |
resembles \texttt{step_tac}, but allows backtracking between using safe |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
602 |
rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules. |
875
a0b71a4bbe5e
documented slow_tac, slow_best_tac, depth_tac, deepen_tac
lcp
parents:
332
diff
changeset
|
603 |
The resulting search space is larger. |
308 | 604 |
\end{ttdescription} |
104 | 605 |
|
3224 | 606 |
\subsection{The current claset}\label{sec:current-claset} |
4561 | 607 |
|
608 |
Each theory is equipped with an implicit \emph{current |
|
609 |
claset}\index{claset!current}. This is a default set of classical |
|
610 |
rules. The underlying idea is quite similar to that of a current |
|
611 |
simpset described in \S\ref{sec:simp-for-dummies}; please read that |
|
612 |
section, including its warnings. The implicit claset can be accessed |
|
613 |
as follows: |
|
614 |
\begin{ttbox} |
|
615 |
claset : unit -> claset |
|
616 |
claset_ref : unit -> claset ref |
|
617 |
claset_of : theory -> claset |
|
618 |
claset_ref_of : theory -> claset ref |
|
619 |
print_claset : theory -> unit |
|
620 |
\end{ttbox} |
|
621 |
||
622 |
The tactics |
|
1869 | 623 |
\begin{ttbox} |
3716 | 624 |
Blast_tac : int -> tactic |
4507 | 625 |
Auto_tac : tactic |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
626 |
Force_tac : int -> tactic |
3716 | 627 |
Fast_tac : int -> tactic |
628 |
Best_tac : int -> tactic |
|
629 |
Deepen_tac : int -> int -> tactic |
|
630 |
Clarify_tac : int -> tactic |
|
631 |
Clarify_step_tac : int -> tactic |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
632 |
Safe_tac : tactic |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
633 |
Safe_step_tac : int -> tactic |
3716 | 634 |
Step_tac : int -> tactic |
1869 | 635 |
\end{ttbox} |
4881
d80faf83c82f
corrected and updated description of wrapper mechanism (including addss)
oheimb
parents:
4666
diff
changeset
|
636 |
\indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac} |
3224 | 637 |
\indexbold{*Best_tac}\indexbold{*Fast_tac}% |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
638 |
\indexbold{*Deepen_tac} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
639 |
\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
640 |
\indexbold{*Safe_tac}\indexbold{*Safe_step_tac} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
641 |
\indexbold{*Step_tac} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
642 |
make use of the current claset. For example, \texttt{Blast_tac} is defined as |
1869 | 643 |
\begin{ttbox} |
4561 | 644 |
fun Blast_tac i st = blast_tac (claset()) i st; |
1869 | 645 |
\end{ttbox} |
4561 | 646 |
and gets the current claset, only after it is applied to a proof |
647 |
state. The functions |
|
1869 | 648 |
\begin{ttbox} |
649 |
AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit |
|
650 |
\end{ttbox} |
|
651 |
\indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs} |
|
652 |
\indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs} |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
3224
diff
changeset
|
653 |
are used to add rules to the current claset. They work exactly like their |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
654 |
lower case counterparts, such as \texttt{addSIs}. Calling |
1869 | 655 |
\begin{ttbox} |
656 |
Delrules : thm list -> unit |
|
657 |
\end{ttbox} |
|
3224 | 658 |
deletes rules from the current claset. |
104 | 659 |
|
660 |
\subsection{Other useful tactics} |
|
319 | 661 |
\index{tactics!for contradiction} |
662 |
\index{tactics!for Modus Ponens} |
|
104 | 663 |
\begin{ttbox} |
664 |
contr_tac : int -> tactic |
|
665 |
mp_tac : int -> tactic |
|
666 |
eq_mp_tac : int -> tactic |
|
667 |
swap_res_tac : thm list -> int -> tactic |
|
668 |
\end{ttbox} |
|
669 |
These can be used in the body of a specialized search. |
|
308 | 670 |
\begin{ttdescription} |
319 | 671 |
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory} |
672 |
solves subgoal~$i$ by detecting a contradiction among two assumptions of |
|
673 |
the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The |
|
674 |
tactic can produce multiple outcomes, enumerating all possible |
|
675 |
contradictions. |
|
104 | 676 |
|
677 |
\item[\ttindexbold{mp_tac} {\it i}] |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
678 |
is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in |
104 | 679 |
subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces |
680 |
$P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do |
|
681 |
nothing. |
|
682 |
||
683 |
\item[\ttindexbold{eq_mp_tac} {\it i}] |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
684 |
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it |
104 | 685 |
is safe. |
686 |
||
687 |
\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of |
|
688 |
the proof state using {\it thms}, which should be a list of introduction |
|
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
689 |
rules. First, it attempts to prove the goal using \texttt{assume_tac} or |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
690 |
\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting |
104 | 691 |
resolution and also elim-resolution with the swapped form. |
308 | 692 |
\end{ttdescription} |
104 | 693 |
|
694 |
\subsection{Creating swapped rules} |
|
695 |
\begin{ttbox} |
|
696 |
swapify : thm list -> thm list |
|
697 |
joinrules : thm list * thm list -> (bool * thm) list |
|
698 |
\end{ttbox} |
|
308 | 699 |
\begin{ttdescription} |
104 | 700 |
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the |
701 |
swapped versions of~{\it thms}, regarded as introduction rules. |
|
702 |
||
308 | 703 |
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})] |
104 | 704 |
joins introduction rules, their swapped versions, and elimination rules for |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
705 |
use with \ttindex{biresolve_tac}. Each rule is paired with~\texttt{false} |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
706 |
(indicating ordinary resolution) or~\texttt{true} (indicating |
104 | 707 |
elim-resolution). |
308 | 708 |
\end{ttdescription} |
104 | 709 |
|
710 |
||
3716 | 711 |
\section{Setting up the classical reasoner}\label{sec:classical-setup} |
319 | 712 |
\index{classical reasoner!setting up} |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
713 |
Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, have |
286 | 714 |
the classical reasoner already set up. When defining a new classical logic, |
715 |
you should set up the reasoner yourself. It consists of the \ML{} functor |
|
104 | 716 |
\ttindex{ClassicalFun}, which takes the argument |
3720
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
717 |
signature \texttt{ |
a5b9e0ade194
Safe_tac, Safe_step_tac, and minor corrections including \tt -> \texttt
paulson
parents:
3716
diff
changeset
|
718 |
CLASSICAL_DATA}: |
104 | 719 |
\begin{ttbox} |
720 |
signature CLASSICAL_DATA = |
|
721 |
sig |
|
722 |
val mp : thm |
|
723 |
val not_elim : thm |
|
724 |
val swap : thm |
|
725 |
val sizef : thm -> int |
|
726 |
val hyp_subst_tacs : (int -> tactic) list |
|
727 |
end; |
|
728 |
\end{ttbox} |
|
729 |
Thus, the functor requires the following items: |
|
308 | 730 |
\begin{ttdescription} |
319 | 731 |
\item[\tdxbold{mp}] should be the Modus Ponens rule |
104 | 732 |
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. |
733 |
||
319 | 734 |
\item[\tdxbold{not_elim}] should be the contradiction rule |
104 | 735 |
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$. |
736 |
||
319 | 737 |
\item[\tdxbold{swap}] should be the swap rule |
104 | 738 |
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. |
739 |
||
740 |
\item[\ttindexbold{sizef}] is the heuristic function used for best-first |
|
741 |
search. It should estimate the size of the remaining subgoals. A good |
|
742 |
heuristic function is \ttindex{size_of_thm}, which measures the size of the |
|
743 |
proof state. Another size function might ignore certain subgoals (say, |
|
744 |
those concerned with type checking). A heuristic function might simply |
|
745 |
count the subgoals. |
|
746 |
||
319 | 747 |
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in |
104 | 748 |
the hypotheses, typically created by \ttindex{HypsubstFun} (see |
749 |
Chapter~\ref{substitution}). This list can, of course, be empty. The |
|
750 |
tactics are assumed to be safe! |
|
308 | 751 |
\end{ttdescription} |
104 | 752 |
The functor is not at all sensitive to the formalization of the |
3108 | 753 |
object-logic. It does not even examine the rules, but merely applies |
754 |
them according to its fixed strategy. The functor resides in {\tt |
|
755 |
Provers/classical.ML} in the Isabelle sources. |
|
104 | 756 |
|
319 | 757 |
\index{classical reasoner|)} |