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 |
|
104
|
6 |
Although Isabelle is generic, many users will be working in some extension
|
308
|
7 |
of classical first-order logic. Isabelle's set theory~{\tt ZF} is built
|
|
8 |
upon theory~{\tt FOL}, while higher-order logic contains first-order logic
|
|
9 |
as a fragment. Theorem-proving in predicate logic is undecidable, but many
|
|
10 |
researchers have developed strategies to assist in this task.
|
104
|
11 |
|
286
|
12 |
Isabelle's classical reasoner is an \ML{} functor that accepts certain
|
104
|
13 |
information about a logic and delivers a suite of automatic tactics. Each
|
|
14 |
tactic takes a collection of rules and executes a simple, non-clausal proof
|
|
15 |
procedure. They are slow and simplistic compared with resolution theorem
|
|
16 |
provers, but they can save considerable time and effort. They can prove
|
|
17 |
theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in
|
|
18 |
seconds:
|
|
19 |
\[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x))
|
|
20 |
\imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \]
|
|
21 |
\[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
|
|
22 |
\imp \neg (\exists z. \forall x. F(x,z))
|
|
23 |
\]
|
308
|
24 |
%
|
|
25 |
The tactics are generic. They are not restricted to first-order logic, and
|
|
26 |
have been heavily used in the development of Isabelle's set theory. Few
|
|
27 |
interactive proof assistants provide this much automation. The tactics can
|
|
28 |
be traced, and their components can be called directly; in this manner,
|
|
29 |
any proof can be viewed interactively.
|
104
|
30 |
|
332
|
31 |
We shall first discuss the underlying principles, then consider how to use
|
|
32 |
the classical reasoner. Finally, we shall see how to instantiate it for
|
|
33 |
new logics. The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already
|
|
34 |
installed.
|
104
|
35 |
|
|
36 |
|
|
37 |
\section{The sequent calculus}
|
|
38 |
\index{sequent calculus}
|
|
39 |
Isabelle supports natural deduction, which is easy to use for interactive
|
|
40 |
proof. But natural deduction does not easily lend itself to automation,
|
|
41 |
and has a bias towards intuitionism. For certain proofs in classical
|
|
42 |
logic, it can not be called natural. The {\bf sequent calculus}, a
|
|
43 |
generalization of natural deduction, is easier to automate.
|
|
44 |
|
|
45 |
A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
|
308
|
46 |
and~$\Delta$ are sets of formulae.%
|
|
47 |
\footnote{For first-order logic, sequents can equivalently be made from
|
|
48 |
lists or multisets of formulae.} The sequent
|
104
|
49 |
\[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
|
|
50 |
is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
|
|
51 |
Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
|
|
52 |
while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf
|
|
53 |
basic} if its left and right sides have a common formula, as in $P,Q\turn
|
|
54 |
Q,R$; basic sequents are trivially valid.
|
|
55 |
|
|
56 |
Sequent rules are classified as {\bf right} or {\bf left}, indicating which
|
|
57 |
side of the $\turn$~symbol they operate on. Rules that operate on the
|
|
58 |
right side are analogous to natural deduction's introduction rules, and
|
308
|
59 |
left rules are analogous to elimination rules.
|
|
60 |
Recall the natural deduction rules for
|
|
61 |
first-order logic,
|
|
62 |
\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
|
|
63 |
{Fig.\ts\ref{fol-fig}}.
|
|
64 |
The sequent calculus analogue of~$({\imp}I)$ is the rule
|
104
|
65 |
$$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
|
|
66 |
\eqno({\imp}R) $$
|
|
67 |
This breaks down some implication on the right side of a sequent; $\Gamma$
|
|
68 |
and $\Delta$ stand for the sets of formulae that are unaffected by the
|
|
69 |
inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the
|
|
70 |
single rule
|
|
71 |
$$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q}
|
|
72 |
\eqno({\disj}R) $$
|
|
73 |
This breaks down some disjunction on the right side, replacing it by both
|
|
74 |
disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic.
|
|
75 |
|
|
76 |
To illustrate the use of multiple formulae on the right, let us prove
|
|
77 |
the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we
|
|
78 |
reduce this formula to a basic sequent:
|
|
79 |
\[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)}
|
|
80 |
{\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;}
|
|
81 |
{\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad}
|
|
82 |
{P, Q \turn Q, P\qquad\qquad}}}
|
|
83 |
\]
|
|
84 |
This example is typical of the sequent calculus: start with the desired
|
|
85 |
theorem and apply rules backwards in a fairly arbitrary manner. This yields a
|
|
86 |
surprisingly effective proof procedure. Quantifiers add few complications,
|
|
87 |
since Isabelle handles parameters and schematic variables. See Chapter~10
|
|
88 |
of {\em ML for the Working Programmer}~\cite{paulson91} for further
|
|
89 |
discussion.
|
|
90 |
|
|
91 |
|
|
92 |
\section{Simulating sequents by natural deduction}
|
308
|
93 |
Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
|
104
|
94 |
But natural deduction is easier to work with, and most object-logics employ
|
|
95 |
it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
|
|
96 |
Q@1,\ldots,Q@n$ by the Isabelle formula
|
|
97 |
\[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \]
|
|
98 |
where the order of the assumptions and the choice of~$Q@1$ are arbitrary.
|
|
99 |
Elim-resolution plays a key role in simulating sequent proofs.
|
|
100 |
|
|
101 |
We can easily handle reasoning on the left.
|
308
|
102 |
As discussed in
|
|
103 |
\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}},
|
104
|
104 |
elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
|
|
105 |
achieves a similar effect as the corresponding sequent rules. For the
|
|
106 |
other connectives, we use sequent-style elimination rules instead of
|
308
|
107 |
destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that
|
|
108 |
the rule $(\neg L)$ has no effect under our representation of sequents!
|
104
|
109 |
$$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
|
|
110 |
\eqno({\neg}L) $$
|
|
111 |
What about reasoning on the right? Introduction rules can only affect the
|
308
|
112 |
formula in the conclusion, namely~$Q@1$. The other right-side formulae are
|
319
|
113 |
represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.
|
|
114 |
\index{assumptions!negated}
|
|
115 |
In order to operate on one of these, it must first be exchanged with~$Q@1$.
|
104
|
116 |
Elim-resolution with the {\bf swap} rule has this effect:
|
|
117 |
$$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap)$$
|
|
118 |
To ensure that swaps occur only when necessary, each introduction rule is
|
|
119 |
converted into a swapped form: it is resolved with the second premise
|
|
120 |
of~$(swap)$. The swapped form of~$({\conj}I)$, which might be
|
|
121 |
called~$({\neg\conj}E)$, is
|
|
122 |
\[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \]
|
|
123 |
Similarly, the swapped form of~$({\imp}I)$ is
|
|
124 |
\[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \]
|
|
125 |
Swapped introduction rules are applied using elim-resolution, which deletes
|
|
126 |
the negated formula. Our representation of sequents also requires the use
|
|
127 |
of ordinary introduction rules. If we had no regard for readability, we
|
|
128 |
could treat the right side more uniformly by representing sequents as
|
|
129 |
\[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \]
|
|
130 |
|
|
131 |
|
|
132 |
\section{Extra rules for the sequent calculus}
|
|
133 |
As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$
|
|
134 |
must be replaced by sequent-style elimination rules. In addition, we need
|
|
135 |
rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj
|
|
136 |
Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that
|
|
137 |
simulates $({\disj}R)$:
|
|
138 |
\[ (\neg Q\Imp P) \Imp P\disj Q \]
|
|
139 |
The destruction rule $({\imp}E)$ is replaced by
|
332
|
140 |
\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
|
104
|
141 |
Quantifier replication also requires special rules. In classical logic,
|
308
|
142 |
$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
|
|
143 |
$(\exists R)$ and $(\forall L)$ are dual:
|
104
|
144 |
\[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
|
|
145 |
{\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
|
|
146 |
\qquad
|
|
147 |
\ainfer{\forall x{.}P, \Gamma &\turn \Delta}
|
|
148 |
{P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L)
|
|
149 |
\]
|
|
150 |
Thus both kinds of quantifier may be replicated. Theorems requiring
|
|
151 |
multiple uses of a universal formula are easy to invent; consider
|
308
|
152 |
\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
|
|
153 |
for any~$n>1$. Natural examples of the multiple use of an existential
|
|
154 |
formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
|
104
|
155 |
|
|
156 |
Forgoing quantifier replication loses completeness, but gains decidability,
|
|
157 |
since the search space becomes finite. Many useful theorems can be proved
|
|
158 |
without replication, and the search generally delivers its verdict in a
|
|
159 |
reasonable time. To adopt this approach, represent the sequent rules
|
|
160 |
$(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists
|
|
161 |
E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination
|
|
162 |
form:
|
|
163 |
$$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$
|
|
164 |
Elim-resolution with this rule will delete the universal formula after a
|
|
165 |
single use. To replicate universal quantifiers, replace the rule by
|
|
166 |
$$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
|
|
167 |
\eqno(\forall E@3) $$
|
|
168 |
To replicate existential quantifiers, replace $(\exists I)$ by
|
332
|
169 |
\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
|
104
|
170 |
All introduction rules mentioned above are also useful in swapped form.
|
|
171 |
|
|
172 |
Replication makes the search space infinite; we must apply the rules with
|
286
|
173 |
care. The classical reasoner distinguishes between safe and unsafe
|
104
|
174 |
rules, applying the latter only when there is no alternative. Depth-first
|
|
175 |
search may well go down a blind alley; best-first search is better behaved
|
|
176 |
in an infinite search space. However, quantifier replication is too
|
|
177 |
expensive to prove any but the simplest theorems.
|
|
178 |
|
|
179 |
|
|
180 |
\section{Classical rule sets}
|
319
|
181 |
\index{classical sets}
|
|
182 |
Each automatic tactic takes a {\bf classical set} --- a collection of
|
104
|
183 |
rules, classified as introduction or elimination and as {\bf safe} or {\bf
|
|
184 |
unsafe}. In general, safe rules can be attempted blindly, while unsafe
|
|
185 |
rules must be used with care. A safe rule must never reduce a provable
|
308
|
186 |
goal to an unprovable set of subgoals.
|
104
|
187 |
|
308
|
188 |
The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any
|
|
189 |
rule is unsafe whose premises contain new unknowns. The elimination
|
|
190 |
rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
|
|
191 |
which discards the assumption $\forall x{.}P(x)$ and replaces it by the
|
|
192 |
weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for
|
|
193 |
similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense:
|
|
194 |
since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
|
|
195 |
In classical first-order logic, all rules are safe except those mentioned
|
|
196 |
above.
|
104
|
197 |
|
|
198 |
The safe/unsafe distinction is vague, and may be regarded merely as a way
|
|
199 |
of giving some rules priority over others. One could argue that
|
|
200 |
$({\disj}E)$ is unsafe, because repeated application of it could generate
|
|
201 |
exponentially many subgoals. Induction rules are unsafe because inductive
|
|
202 |
proofs are difficult to set up automatically. Any inference is unsafe that
|
|
203 |
instantiates an unknown in the proof state --- thus \ttindex{match_tac}
|
|
204 |
must be used, rather than \ttindex{resolve_tac}. Even proof by assumption
|
|
205 |
is unsafe if it instantiates unknowns shared with other subgoals --- thus
|
|
206 |
\ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
|
|
207 |
|
319
|
208 |
Classical rule sets belong to the abstract type \mltydx{claset}, which
|
286
|
209 |
supports the following operations (provided the classical reasoner is
|
104
|
210 |
installed!):
|
|
211 |
\begin{ttbox}
|
|
212 |
empty_cs : claset
|
|
213 |
addSIs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
214 |
addSEs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
215 |
addSDs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
216 |
addIs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
217 |
addEs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
218 |
addDs : claset * thm list -> claset \hfill{\bf infix 4}
|
|
219 |
print_cs : claset -> unit
|
|
220 |
\end{ttbox}
|
|
221 |
There are no operations for deletion from a classical set. The add
|
|
222 |
operations do not check for repetitions.
|
308
|
223 |
\begin{ttdescription}
|
104
|
224 |
\item[\ttindexbold{empty_cs}] is the empty classical set.
|
|
225 |
|
308
|
226 |
\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
|
|
227 |
adds safe introduction~$rules$ to~$cs$.
|
104
|
228 |
|
308
|
229 |
\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
|
|
230 |
adds safe elimination~$rules$ to~$cs$.
|
104
|
231 |
|
308
|
232 |
\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
|
|
233 |
adds safe destruction~$rules$ to~$cs$.
|
104
|
234 |
|
308
|
235 |
\item[$cs$ addIs $rules$] \indexbold{*addIs}
|
|
236 |
adds unsafe introduction~$rules$ to~$cs$.
|
104
|
237 |
|
308
|
238 |
\item[$cs$ addEs $rules$] \indexbold{*addEs}
|
|
239 |
adds unsafe elimination~$rules$ to~$cs$.
|
104
|
240 |
|
308
|
241 |
\item[$cs$ addDs $rules$] \indexbold{*addDs}
|
|
242 |
adds unsafe destruction~$rules$ to~$cs$.
|
104
|
243 |
|
308
|
244 |
\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
|
|
245 |
\end{ttdescription}
|
|
246 |
|
104
|
247 |
Introduction rules are those that can be applied using ordinary resolution.
|
|
248 |
The classical set automatically generates their swapped forms, which will
|
|
249 |
be applied using elim-resolution. Elimination rules are applied using
|
286
|
250 |
elim-resolution. In a classical set, rules are sorted by the number of new
|
|
251 |
subgoals they will yield; rules that generate the fewest subgoals will be
|
|
252 |
tried first (see \S\ref{biresolve_tac}).
|
104
|
253 |
|
|
254 |
For a given classical set, the proof strategy is simple. Perform as many
|
|
255 |
safe inferences as possible; or else, apply certain safe rules, allowing
|
|
256 |
instantiation of unknowns; or else, apply an unsafe rule. The tactics may
|
319
|
257 |
also apply {\tt hyp_subst_tac}, if they have been set up to do so (see
|
104
|
258 |
below). They may perform a form of Modus Ponens: if there are assumptions
|
|
259 |
$P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
|
|
260 |
|
|
261 |
|
|
262 |
\section{The classical tactics}
|
319
|
263 |
\index{classical reasoner!tactics}
|
104
|
264 |
If installed, the classical module provides several tactics (and other
|
|
265 |
operations) for simulating the classical sequent calculus.
|
|
266 |
|
332
|
267 |
\subsection{The automatic tactics}
|
|
268 |
\begin{ttbox}
|
|
269 |
fast_tac : claset -> int -> tactic
|
|
270 |
best_tac : claset -> int -> tactic
|
|
271 |
\end{ttbox}
|
|
272 |
Both of these tactics work by applying {\tt step_tac} repeatedly. Their
|
|
273 |
effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
|
|
274 |
solve this subgoal or fail.
|
|
275 |
\begin{ttdescription}
|
|
276 |
\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
|
|
277 |
depth-first search, to solve subgoal~$i$.
|
|
278 |
|
|
279 |
\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
|
|
280 |
best-first search, to solve subgoal~$i$. A heuristic function ---
|
|
281 |
typically, the total size of the proof state --- guides the search. This
|
|
282 |
function is supplied when the classical reasoner is set up.
|
|
283 |
\end{ttdescription}
|
|
284 |
|
|
285 |
|
104
|
286 |
\subsection{Single-step tactics}
|
|
287 |
\begin{ttbox}
|
|
288 |
safe_step_tac : claset -> int -> tactic
|
|
289 |
safe_tac : claset -> tactic
|
|
290 |
inst_step_tac : claset -> int -> tactic
|
|
291 |
step_tac : claset -> int -> tactic
|
|
292 |
slow_step_tac : claset -> int -> tactic
|
|
293 |
\end{ttbox}
|
|
294 |
The automatic proof procedures call these tactics. By calling them
|
|
295 |
yourself, you can execute these procedures one step at a time.
|
308
|
296 |
\begin{ttdescription}
|
104
|
297 |
\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
|
319
|
298 |
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
|
|
299 |
care not to instantiate unknowns), or {\tt hyp_subst_tac}.
|
104
|
300 |
|
|
301 |
\item[\ttindexbold{safe_tac} $cs$] repeatedly performs safe steps on all
|
|
302 |
subgoals. It is deterministic, with at most one outcome. If the automatic
|
|
303 |
tactics fail, try using {\tt safe_tac} to open up your formula; then you
|
|
304 |
can replicate certain quantifiers explicitly by applying appropriate rules.
|
|
305 |
|
|
306 |
\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
|
|
307 |
but allows unknowns to be instantiated.
|
|
308 |
|
332
|
309 |
\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. If this
|
104
|
310 |
fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
|
|
311 |
This is the basic step of the proof procedure.
|
|
312 |
|
|
313 |
\item[\ttindexbold{slow_step_tac}]
|
|
314 |
resembles {\tt step_tac}, but allows backtracking between using safe
|
|
315 |
rules with instantiation ({\tt inst_step_tac}) and using unsafe rules.
|
|
316 |
The resulting search space is too large for use in the standard proof
|
|
317 |
procedures, but {\tt slow_step_tac} is worth considering in special
|
|
318 |
situations.
|
308
|
319 |
\end{ttdescription}
|
104
|
320 |
|
|
321 |
|
|
322 |
\subsection{Other useful tactics}
|
319
|
323 |
\index{tactics!for contradiction}
|
|
324 |
\index{tactics!for Modus Ponens}
|
104
|
325 |
\begin{ttbox}
|
|
326 |
contr_tac : int -> tactic
|
|
327 |
mp_tac : int -> tactic
|
|
328 |
eq_mp_tac : int -> tactic
|
|
329 |
swap_res_tac : thm list -> int -> tactic
|
|
330 |
\end{ttbox}
|
|
331 |
These can be used in the body of a specialized search.
|
308
|
332 |
\begin{ttdescription}
|
319
|
333 |
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
|
|
334 |
solves subgoal~$i$ by detecting a contradiction among two assumptions of
|
|
335 |
the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
|
|
336 |
tactic can produce multiple outcomes, enumerating all possible
|
|
337 |
contradictions.
|
104
|
338 |
|
|
339 |
\item[\ttindexbold{mp_tac} {\it i}]
|
|
340 |
is like {\tt contr_tac}, but also attempts to perform Modus Ponens in
|
|
341 |
subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
|
|
342 |
$P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
|
|
343 |
nothing.
|
|
344 |
|
|
345 |
\item[\ttindexbold{eq_mp_tac} {\it i}]
|
|
346 |
is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
|
|
347 |
is safe.
|
|
348 |
|
|
349 |
\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
|
|
350 |
the proof state using {\it thms}, which should be a list of introduction
|
319
|
351 |
rules. First, it attempts to solve the goal using {\tt assume_tac} or
|
104
|
352 |
{\tt contr_tac}. It then attempts to apply each rule in turn, attempting
|
|
353 |
resolution and also elim-resolution with the swapped form.
|
308
|
354 |
\end{ttdescription}
|
104
|
355 |
|
|
356 |
\subsection{Creating swapped rules}
|
|
357 |
\begin{ttbox}
|
|
358 |
swapify : thm list -> thm list
|
|
359 |
joinrules : thm list * thm list -> (bool * thm) list
|
|
360 |
\end{ttbox}
|
308
|
361 |
\begin{ttdescription}
|
104
|
362 |
\item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
|
|
363 |
swapped versions of~{\it thms}, regarded as introduction rules.
|
|
364 |
|
308
|
365 |
\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
|
104
|
366 |
joins introduction rules, their swapped versions, and elimination rules for
|
|
367 |
use with \ttindex{biresolve_tac}. Each rule is paired with~{\tt false}
|
|
368 |
(indicating ordinary resolution) or~{\tt true} (indicating
|
|
369 |
elim-resolution).
|
308
|
370 |
\end{ttdescription}
|
104
|
371 |
|
|
372 |
|
286
|
373 |
\section{Setting up the classical reasoner}
|
319
|
374 |
\index{classical reasoner!setting up}
|
104
|
375 |
Isabelle's classical object-logics, including {\tt FOL} and {\tt HOL}, have
|
286
|
376 |
the classical reasoner already set up. When defining a new classical logic,
|
|
377 |
you should set up the reasoner yourself. It consists of the \ML{} functor
|
104
|
378 |
\ttindex{ClassicalFun}, which takes the argument
|
319
|
379 |
signature {\tt CLASSICAL_DATA}:
|
104
|
380 |
\begin{ttbox}
|
|
381 |
signature CLASSICAL_DATA =
|
|
382 |
sig
|
|
383 |
val mp : thm
|
|
384 |
val not_elim : thm
|
|
385 |
val swap : thm
|
|
386 |
val sizef : thm -> int
|
|
387 |
val hyp_subst_tacs : (int -> tactic) list
|
|
388 |
end;
|
|
389 |
\end{ttbox}
|
|
390 |
Thus, the functor requires the following items:
|
308
|
391 |
\begin{ttdescription}
|
319
|
392 |
\item[\tdxbold{mp}] should be the Modus Ponens rule
|
104
|
393 |
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
|
|
394 |
|
319
|
395 |
\item[\tdxbold{not_elim}] should be the contradiction rule
|
104
|
396 |
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
|
|
397 |
|
319
|
398 |
\item[\tdxbold{swap}] should be the swap rule
|
104
|
399 |
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
|
|
400 |
|
|
401 |
\item[\ttindexbold{sizef}] is the heuristic function used for best-first
|
|
402 |
search. It should estimate the size of the remaining subgoals. A good
|
|
403 |
heuristic function is \ttindex{size_of_thm}, which measures the size of the
|
|
404 |
proof state. Another size function might ignore certain subgoals (say,
|
|
405 |
those concerned with type checking). A heuristic function might simply
|
|
406 |
count the subgoals.
|
|
407 |
|
319
|
408 |
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
|
104
|
409 |
the hypotheses, typically created by \ttindex{HypsubstFun} (see
|
|
410 |
Chapter~\ref{substitution}). This list can, of course, be empty. The
|
|
411 |
tactics are assumed to be safe!
|
308
|
412 |
\end{ttdescription}
|
104
|
413 |
The functor is not at all sensitive to the formalization of the
|
|
414 |
object-logic. It does not even examine the rules, but merely applies them
|
|
415 |
according to its fixed strategy. The functor resides in {\tt
|
319
|
416 |
Provers/classical.ML} in the Isabelle distribution directory.
|
104
|
417 |
|
319
|
418 |
\index{classical reasoner|)}
|