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 |
|
lcp@104
|
6 |
\section{Classical rule sets}
|
lcp@319
|
7 |
\index{classical sets}
|
lcp@104
|
8 |
|
oheimb@5550
|
9 |
For elimination and destruction rules there are variants of the add operations
|
oheimb@5550
|
10 |
adding a rule in a way such that it is applied only if also its second premise
|
oheimb@5550
|
11 |
can be unified with an assumption of the current proof state:
|
oheimb@5576
|
12 |
\indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
|
oheimb@5550
|
13 |
\begin{ttbox}
|
oheimb@5550
|
14 |
addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
|
oheimb@5550
|
15 |
addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
|
oheimb@5550
|
16 |
addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
|
oheimb@5550
|
17 |
addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
|
oheimb@5550
|
18 |
\end{ttbox}
|
oheimb@5550
|
19 |
\begin{warn}
|
oheimb@5550
|
20 |
A rule to be added in this special way must be given a name, which is used
|
oheimb@5550
|
21 |
to delete it again -- when desired -- using \texttt{delSWrappers} or
|
oheimb@5550
|
22 |
\texttt{delWrappers}, respectively. This is because these add operations
|
oheimb@5550
|
23 |
are implemented as wrappers (see \ref{sec:modifying-search} below).
|
oheimb@5550
|
24 |
\end{warn}
|
oheimb@5550
|
25 |
|
lcp@1099
|
26 |
|
lcp@1099
|
27 |
\subsection{Modifying the search step}
|
oheimb@4665
|
28 |
\label{sec:modifying-search}
|
paulson@3716
|
29 |
For a given classical set, the proof strategy is simple. Perform as many safe
|
paulson@3716
|
30 |
inferences as possible; or else, apply certain safe rules, allowing
|
paulson@3716
|
31 |
instantiation of unknowns; or else, apply an unsafe rule. The tactics also
|
paulson@3716
|
32 |
eliminate assumptions of the form $x=t$ by substitution if they have been set
|
oheimb@11181
|
33 |
up to do so (see \texttt{hyp_subst_tacs} in~{\S}\ref{sec:classical-setup} below).
|
paulson@3716
|
34 |
They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$
|
paulson@3716
|
35 |
and~$P$, then replace $P\imp Q$ by~$Q$.
|
lcp@104
|
36 |
|
paulson@3720
|
37 |
The classical reasoning tactics --- except \texttt{blast_tac}! --- allow
|
oheimb@4649
|
38 |
you to modify this basic proof strategy by applying two lists of arbitrary
|
oheimb@4649
|
39 |
{\bf wrapper tacticals} to it.
|
oheimb@4649
|
40 |
The first wrapper list, which is considered to contain safe wrappers only,
|
oheimb@4649
|
41 |
affects \ttindex{safe_step_tac} and all the tactics that call it.
|
oheimb@5550
|
42 |
The second one, which may contain unsafe wrappers, affects the unsafe parts
|
oheimb@5550
|
43 |
of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
|
oheimb@4649
|
44 |
A wrapper transforms each step of the search, for example
|
oheimb@5550
|
45 |
by attempting other tactics before or after the original step tactic.
|
oheimb@4649
|
46 |
All members of a wrapper list are applied in turn to the respective step tactic.
|
oheimb@4649
|
47 |
|
oheimb@4649
|
48 |
Initially the two wrapper lists are empty, which means no modification of the
|
oheimb@4649
|
49 |
step tactics. Safe and unsafe wrappers are added to a claset
|
oheimb@4649
|
50 |
with the functions given below, supplying them with wrapper names.
|
oheimb@4649
|
51 |
These names may be used to selectively delete wrappers.
|
lcp@1099
|
52 |
|
lcp@1099
|
53 |
\begin{ttbox}
|
oheimb@4649
|
54 |
type wrapper = (int -> tactic) -> (int -> tactic);
|
oheimb@4881
|
55 |
|
oheimb@4881
|
56 |
addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
|
oheimb@4649
|
57 |
addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
|
oheimb@11181
|
58 |
addSafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
|
oheimb@4649
|
59 |
delSWrapper : claset * string -> claset \hfill{\bf infix 4}
|
oheimb@4881
|
60 |
|
oheimb@4881
|
61 |
addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
|
oheimb@4649
|
62 |
addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
|
oheimb@11181
|
63 |
addafter : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
|
oheimb@4649
|
64 |
delWrapper : claset * string -> claset \hfill{\bf infix 4}
|
oheimb@4649
|
65 |
|
oheimb@4881
|
66 |
addSss : claset * simpset -> claset \hfill{\bf infix 4}
|
oheimb@2632
|
67 |
addss : claset * simpset -> claset \hfill{\bf infix 4}
|
lcp@1099
|
68 |
\end{ttbox}
|
lcp@1099
|
69 |
%
|
lcp@1099
|
70 |
|
lcp@1099
|
71 |
\begin{ttdescription}
|
oheimb@4881
|
72 |
\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
|
oheimb@4881
|
73 |
adds a new wrapper, which should yield a safe tactic,
|
oheimb@4881
|
74 |
to modify the existing safe step tactic.
|
oheimb@4881
|
75 |
|
oheimb@4881
|
76 |
\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
|
oheimb@5550
|
77 |
adds the given tactic as a safe wrapper, such that it is tried
|
oheimb@5550
|
78 |
{\em before} each safe step of the search.
|
oheimb@4881
|
79 |
|
oheimb@11181
|
80 |
\item[$cs$ addSafter $(name,tac)$] \indexbold{*addSafter}
|
oheimb@5550
|
81 |
adds the given tactic as a safe wrapper, such that it is tried
|
oheimb@5550
|
82 |
when a safe step of the search would fail.
|
oheimb@4881
|
83 |
|
oheimb@4881
|
84 |
\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
|
oheimb@4881
|
85 |
deletes the safe wrapper with the given name.
|
oheimb@4881
|
86 |
|
oheimb@4881
|
87 |
\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
|
oheimb@4881
|
88 |
adds a new wrapper to modify the existing (unsafe) step tactic.
|
oheimb@4881
|
89 |
|
oheimb@4881
|
90 |
\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
|
oheimb@5550
|
91 |
adds the given tactic as an unsafe wrapper, such that it its result is
|
oheimb@5550
|
92 |
concatenated {\em before} the result of each unsafe step.
|
oheimb@4881
|
93 |
|
oheimb@11181
|
94 |
\item[$cs$ addafter $(name,tac)$] \indexbold{*addafter}
|
oheimb@5550
|
95 |
adds the given tactic as an unsafe wrapper, such that it its result is
|
oheimb@5550
|
96 |
concatenated {\em after} the result of each unsafe step.
|
oheimb@4881
|
97 |
|
oheimb@4881
|
98 |
\item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
|
oheimb@4881
|
99 |
deletes the unsafe wrapper with the given name.
|
oheimb@4881
|
100 |
|
oheimb@4881
|
101 |
\item[$cs$ addSss $ss$] \indexbold{*addss}
|
oheimb@4881
|
102 |
adds the simpset~$ss$ to the classical set. The assumptions and goal will be
|
oheimb@4881
|
103 |
simplified, in a rather safe way, after each safe step of the search.
|
oheimb@4881
|
104 |
|
lcp@1099
|
105 |
\item[$cs$ addss $ss$] \indexbold{*addss}
|
paulson@3485
|
106 |
adds the simpset~$ss$ to the classical set. The assumptions and goal will be
|
oheimb@4881
|
107 |
simplified, before the each unsafe step of the search.
|
oheimb@2631
|
108 |
|
oheimb@4881
|
109 |
\end{ttdescription}
|
oheimb@2631
|
110 |
|
oheimb@5550
|
111 |
\index{simplification!from classical reasoner}
|
oheimb@5550
|
112 |
Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
|
oheimb@5550
|
113 |
are not part of the classical reasoner.
|
oheimb@5550
|
114 |
, which are used as primitives
|
oheimb@11181
|
115 |
for the automatic tactics described in {\S}\ref{sec:automatic-tactics}, are
|
oheimb@5550
|
116 |
implemented as wrapper tacticals.
|
oheimb@5550
|
117 |
they
|
oheimb@4881
|
118 |
\begin{warn}
|
oheimb@4881
|
119 |
Being defined as wrappers, these operators are inappropriate for adding more
|
oheimb@4881
|
120 |
than one simpset at a time: the simpset added last overwrites any earlier ones.
|
oheimb@4881
|
121 |
When a simpset combined with a claset is to be augmented, this should done
|
oheimb@4881
|
122 |
{\em before} combining it with the claset.
|
oheimb@4881
|
123 |
\end{warn}
|
lcp@1099
|
124 |
|
lcp@104
|
125 |
|
lcp@104
|
126 |
\section{The classical tactics}
|
oheimb@5576
|
127 |
|
paulson@3224
|
128 |
\subsection{Other classical tactics}
|
lcp@332
|
129 |
\begin{ttbox}
|
lcp@875
|
130 |
slow_best_tac : claset -> int -> tactic
|
lcp@332
|
131 |
\end{ttbox}
|
lcp@875
|
132 |
|
lcp@332
|
133 |
\begin{ttdescription}
|
paulson@8136
|
134 |
\item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with
|
paulson@8136
|
135 |
best-first search to prove subgoal~$i$.
|
lcp@875
|
136 |
\end{ttdescription}
|
lcp@875
|
137 |
|
lcp@875
|
138 |
|
paulson@3716
|
139 |
\subsection{Depth-limited automatic tactics}
|
lcp@875
|
140 |
\begin{ttbox}
|
lcp@875
|
141 |
depth_tac : claset -> int -> int -> tactic
|
lcp@875
|
142 |
deepen_tac : claset -> int -> int -> tactic
|
lcp@875
|
143 |
\end{ttbox}
|
lcp@875
|
144 |
These work by exhaustive search up to a specified depth. Unsafe rules are
|
lcp@875
|
145 |
modified to preserve the formula they act on, so that it be used repeatedly.
|
paulson@3720
|
146 |
They can prove more goals than \texttt{fast_tac} can but are much
|
lcp@875
|
147 |
slower, for example if the assumptions have many universal quantifiers.
|
lcp@875
|
148 |
|
lcp@875
|
149 |
The depth limits the number of unsafe steps. If you can estimate the minimum
|
lcp@875
|
150 |
number of unsafe steps needed, supply this value as~$m$ to save time.
|
lcp@875
|
151 |
\begin{ttdescription}
|
lcp@875
|
152 |
\item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
|
paulson@3089
|
153 |
tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
|
lcp@875
|
154 |
|
lcp@875
|
155 |
\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
|
paulson@3720
|
156 |
tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac}
|
lcp@875
|
157 |
repeatedly with increasing depths, starting with~$m$.
|
lcp@332
|
158 |
\end{ttdescription}
|
lcp@332
|
159 |
|
lcp@332
|
160 |
|
lcp@104
|
161 |
\subsection{Other useful tactics}
|
lcp@319
|
162 |
\index{tactics!for contradiction}
|
lcp@319
|
163 |
\index{tactics!for Modus Ponens}
|
lcp@104
|
164 |
\begin{ttbox}
|
lcp@104
|
165 |
contr_tac : int -> tactic
|
lcp@104
|
166 |
mp_tac : int -> tactic
|
lcp@104
|
167 |
eq_mp_tac : int -> tactic
|
lcp@104
|
168 |
swap_res_tac : thm list -> int -> tactic
|
lcp@104
|
169 |
\end{ttbox}
|
lcp@104
|
170 |
These can be used in the body of a specialized search.
|
lcp@308
|
171 |
\begin{ttdescription}
|
lcp@319
|
172 |
\item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory}
|
lcp@319
|
173 |
solves subgoal~$i$ by detecting a contradiction among two assumptions of
|
lcp@319
|
174 |
the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The
|
lcp@319
|
175 |
tactic can produce multiple outcomes, enumerating all possible
|
lcp@319
|
176 |
contradictions.
|
lcp@104
|
177 |
|
lcp@104
|
178 |
\item[\ttindexbold{mp_tac} {\it i}]
|
paulson@3720
|
179 |
is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in
|
lcp@104
|
180 |
subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces
|
lcp@104
|
181 |
$P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do
|
lcp@104
|
182 |
nothing.
|
lcp@104
|
183 |
|
lcp@104
|
184 |
\item[\ttindexbold{eq_mp_tac} {\it i}]
|
paulson@3720
|
185 |
is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
|
lcp@104
|
186 |
is safe.
|
lcp@104
|
187 |
|
lcp@104
|
188 |
\item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of
|
lcp@104
|
189 |
the proof state using {\it thms}, which should be a list of introduction
|
paulson@3720
|
190 |
rules. First, it attempts to prove the goal using \texttt{assume_tac} or
|
paulson@3720
|
191 |
\texttt{contr_tac}. It then attempts to apply each rule in turn, attempting
|
lcp@104
|
192 |
resolution and also elim-resolution with the swapped form.
|
lcp@308
|
193 |
\end{ttdescription}
|
lcp@104
|
194 |
|
lcp@104
|
195 |
|
paulson@3716
|
196 |
\section{Setting up the classical reasoner}\label{sec:classical-setup}
|
lcp@319
|
197 |
\index{classical reasoner!setting up}
|
oheimb@5550
|
198 |
Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL},
|
oheimb@5550
|
199 |
have the classical reasoner already set up.
|
oheimb@5550
|
200 |
When defining a new classical logic, you should set up the reasoner yourself.
|
oheimb@5550
|
201 |
It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the
|
oheimb@5550
|
202 |
argument signature \texttt{CLASSICAL_DATA}:
|
lcp@104
|
203 |
\begin{ttbox}
|
lcp@104
|
204 |
signature CLASSICAL_DATA =
|
lcp@104
|
205 |
sig
|
lcp@104
|
206 |
val mp : thm
|
lcp@104
|
207 |
val not_elim : thm
|
lcp@104
|
208 |
val swap : thm
|
lcp@104
|
209 |
val sizef : thm -> int
|
lcp@104
|
210 |
val hyp_subst_tacs : (int -> tactic) list
|
lcp@104
|
211 |
end;
|
lcp@104
|
212 |
\end{ttbox}
|
lcp@104
|
213 |
Thus, the functor requires the following items:
|
lcp@308
|
214 |
\begin{ttdescription}
|
lcp@319
|
215 |
\item[\tdxbold{mp}] should be the Modus Ponens rule
|
lcp@104
|
216 |
$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
|
lcp@104
|
217 |
|
lcp@319
|
218 |
\item[\tdxbold{not_elim}] should be the contradiction rule
|
lcp@104
|
219 |
$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
|
lcp@104
|
220 |
|
lcp@319
|
221 |
\item[\tdxbold{swap}] should be the swap rule
|
lcp@104
|
222 |
$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
|
lcp@104
|
223 |
|
lcp@104
|
224 |
\item[\ttindexbold{sizef}] is the heuristic function used for best-first
|
lcp@104
|
225 |
search. It should estimate the size of the remaining subgoals. A good
|
lcp@104
|
226 |
heuristic function is \ttindex{size_of_thm}, which measures the size of the
|
lcp@104
|
227 |
proof state. Another size function might ignore certain subgoals (say,
|
paulson@6170
|
228 |
those concerned with type-checking). A heuristic function might simply
|
lcp@104
|
229 |
count the subgoals.
|
lcp@104
|
230 |
|
lcp@319
|
231 |
\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
|
lcp@104
|
232 |
the hypotheses, typically created by \ttindex{HypsubstFun} (see
|
lcp@104
|
233 |
Chapter~\ref{substitution}). This list can, of course, be empty. The
|
lcp@104
|
234 |
tactics are assumed to be safe!
|
lcp@308
|
235 |
\end{ttdescription}
|
lcp@104
|
236 |
The functor is not at all sensitive to the formalization of the
|
wenzelm@3108
|
237 |
object-logic. It does not even examine the rules, but merely applies
|
wenzelm@3108
|
238 |
them according to its fixed strategy. The functor resides in {\tt
|
wenzelm@3108
|
239 |
Provers/classical.ML} in the Isabelle sources.
|
lcp@104
|
240 |
|
lcp@319
|
241 |
\index{classical reasoner|)}
|
wenzelm@5371
|
242 |
|
wenzelm@5371
|
243 |
%%% Local Variables:
|
wenzelm@5371
|
244 |
%%% mode: latex
|
wenzelm@5371
|
245 |
%%% TeX-master: "ref"
|
wenzelm@5371
|
246 |
%%% End:
|