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