|
1 %% $Id$ |
|
2 \chapter{First-order logic} |
|
3 The directory~\ttindexbold{FOL} contains theories for first-order logic |
|
4 based on Gentzen's natural deduction systems (which he called {\sc nj} and |
|
5 {\sc nk}). Intuitionistic logic is defined first; then classical logic is |
|
6 obtained by adding the double negation rule. Basic proof procedures are |
|
7 provided. The intuitionistic prover works with derived rules to simplify |
|
8 implications in the assumptions. Classical logic makes use of Isabelle's |
|
9 generic prover for classical reasoning, which simulates a sequent calculus. |
|
10 |
|
11 \section{Syntax and rules of inference} |
|
12 The logic is many-sorted, using Isabelle's type classes. The |
|
13 class of first-order terms is called {\it term} and is a subclass of |
|
14 {\it logic}. No types of individuals |
|
15 are provided, but extensions can define types such as $nat::term$ and type |
|
16 constructors such as $list::(term)term$. See the examples directory. |
|
17 Below, the type variable $\alpha$ ranges over class {\it term\/}; the |
|
18 equality symbol and quantifiers are polymorphic (many-sorted). The type of |
|
19 formulae is~{\it o}, which belongs to class {\it logic}. |
|
20 Figure~\ref{fol-syntax} gives the syntax. Note that $a$\verb|~=|$b$ is |
|
21 translated to \verb|~(|$a$=$b$\verb|)|. |
|
22 |
|
23 The intuitionistic theory has the \ML\ identifier |
|
24 \ttindexbold{IFOL.thy}. Figure~\ref{fol-rules} shows the inference |
|
25 rules with their~\ML\ names. Negation is defined in the usual way for |
|
26 intuitionistic logic; $\neg P$ abbreviates $P\imp\bot$. The |
|
27 biconditional~($\bimp$) is defined through $\conj$ and~$\imp$; introduction |
|
28 and elimination rules are derived for it. |
|
29 |
|
30 The unique existence quantifier, $\exists!x.P(x)$, is defined in terms |
|
31 of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested |
|
32 quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates |
|
33 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there |
|
34 exists a unique pair $(x,y)$ satisfying~$P(x,y)$. |
|
35 |
|
36 Some intuitionistic derived rules are shown in |
|
37 Figure~\ref{fol-int-derived}, again with their \ML\ names. These include |
|
38 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural |
|
39 deduction typically involves a combination of forwards and backwards |
|
40 reasoning, particularly with the destruction rules $(\conj E)$, |
|
41 $({\imp}E)$, and~$(\forall E)$. Isabelle's backwards style handles these |
|
42 rules badly, so sequent-style rules are derived to eliminate conjunctions, |
|
43 implications, and universal quantifiers. Used with elim-resolution, |
|
44 \ttindex{allE} eliminates a universal quantifier while \ttindex{all_dupE} |
|
45 re-inserts the quantified formula for later use. The rules {\tt |
|
46 conj_impE}, etc., support the intuitionistic proof procedure |
|
47 (see~\S\ref{fol-int-prover}). |
|
48 |
|
49 See the files \ttindexbold{FOL/ifol.thy}, \ttindexbold{FOL/ifol.ML} and |
|
50 \ttindexbold{FOL/int-prover.ML} for complete listings of the rules and |
|
51 derived rules. |
|
52 |
|
53 \begin{figure} |
|
54 \begin{center} |
|
55 \begin{tabular}{rrr} |
|
56 \it name &\it meta-type & \it description \\ |
|
57 \idx{Trueprop}& $o\To prop$ & coercion to $prop$\\ |
|
58 \idx{Not} & $o\To o$ & negation ($\neg$) \\ |
|
59 \idx{True} & $o$ & tautology ($\top$) \\ |
|
60 \idx{False} & $o$ & absurdity ($\bot$) |
|
61 \end{tabular} |
|
62 \end{center} |
|
63 \subcaption{Constants} |
|
64 |
|
65 \begin{center} |
|
66 \begin{tabular}{llrrr} |
|
67 \it symbol &\it name &\it meta-type & \it precedence & \it description \\ |
|
68 \idx{ALL} & \idx{All} & $(\alpha\To o)\To o$ & 10 & |
|
69 universal quantifier ($\forall$) \\ |
|
70 \idx{EX} & \idx{Ex} & $(\alpha\To o)\To o$ & 10 & |
|
71 existential quantifier ($\exists$) \\ |
|
72 \idx{EX!} & \idx{Ex1} & $(\alpha\To o)\To o$ & 10 & |
|
73 unique existence ($\exists!$) |
|
74 \end{tabular} |
|
75 \end{center} |
|
76 \subcaption{Binders} |
|
77 |
|
78 \begin{center} |
|
79 \indexbold{*"=} |
|
80 \indexbold{&@{\tt\&}} |
|
81 \indexbold{*"|} |
|
82 \indexbold{*"-"-">} |
|
83 \indexbold{*"<"-">} |
|
84 \begin{tabular}{rrrr} |
|
85 \it symbol & \it meta-type & \it precedence & \it description \\ |
|
86 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ |
|
87 \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ |
|
88 \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ |
|
89 \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ |
|
90 \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) |
|
91 \end{tabular} |
|
92 \end{center} |
|
93 \subcaption{Infixes} |
|
94 |
|
95 \dquotes |
|
96 \[\begin{array}{rcl} |
|
97 formula & = & \hbox{expression of type~$o$} \\ |
|
98 & | & term " = " term \\ |
|
99 & | & term " \ttilde= " term \\ |
|
100 & | & "\ttilde\ " formula \\ |
|
101 & | & formula " \& " formula \\ |
|
102 & | & formula " | " formula \\ |
|
103 & | & formula " --> " formula \\ |
|
104 & | & formula " <-> " formula \\ |
|
105 & | & "ALL~" id~id^* " . " formula \\ |
|
106 & | & "EX~~" id~id^* " . " formula \\ |
|
107 & | & "EX!~" id~id^* " . " formula |
|
108 \end{array} |
|
109 \] |
|
110 \subcaption{Grammar} |
|
111 \caption{Syntax of {\tt FOL}} \label{fol-syntax} |
|
112 \end{figure} |
|
113 |
|
114 |
|
115 \begin{figure} |
|
116 \begin{ttbox} |
|
117 \idx{refl} a=a |
|
118 \idx{subst} [| a=b; P(a) |] ==> P(b) |
|
119 \subcaption{Equality rules} |
|
120 |
|
121 \idx{conjI} [| P; Q |] ==> P&Q |
|
122 \idx{conjunct1} P&Q ==> P |
|
123 \idx{conjunct2} P&Q ==> Q |
|
124 |
|
125 \idx{disjI1} P ==> P|Q |
|
126 \idx{disjI2} Q ==> P|Q |
|
127 \idx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R |
|
128 |
|
129 \idx{impI} (P ==> Q) ==> P-->Q |
|
130 \idx{mp} [| P-->Q; P |] ==> Q |
|
131 |
|
132 \idx{FalseE} False ==> P |
|
133 \subcaption{Propositional rules} |
|
134 |
|
135 \idx{allI} (!!x. P(x)) ==> (ALL x.P(x)) |
|
136 \idx{spec} (ALL x.P(x)) ==> P(x) |
|
137 |
|
138 \idx{exI} P(x) ==> (EX x.P(x)) |
|
139 \idx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R |
|
140 \subcaption{Quantifier rules} |
|
141 |
|
142 \idx{True_def} True == False-->False |
|
143 \idx{not_def} ~P == P-->False |
|
144 \idx{iff_def} P<->Q == (P-->Q) & (Q-->P) |
|
145 \idx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x) |
|
146 \subcaption{Definitions} |
|
147 \end{ttbox} |
|
148 |
|
149 \caption{Rules of intuitionistic {\tt FOL}} \label{fol-rules} |
|
150 \end{figure} |
|
151 |
|
152 |
|
153 \begin{figure} |
|
154 \begin{ttbox} |
|
155 \idx{sym} a=b ==> b=a |
|
156 \idx{trans} [| a=b; b=c |] ==> a=c |
|
157 \idx{ssubst} [| b=a; P(a) |] ==> P(b) |
|
158 \subcaption{Derived equality rules} |
|
159 |
|
160 \idx{TrueI} True |
|
161 |
|
162 \idx{notI} (P ==> False) ==> ~P |
|
163 \idx{notE} [| ~P; P |] ==> R |
|
164 |
|
165 \idx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q |
|
166 \idx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R |
|
167 \idx{iffD1} [| P <-> Q; P |] ==> Q |
|
168 \idx{iffD2} [| P <-> Q; Q |] ==> P |
|
169 |
|
170 \idx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x) |
|
171 \idx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R |
|
172 |] ==> R |
|
173 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)} |
|
174 |
|
175 \idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R |
|
176 \idx{impE} [| P-->Q; P; Q ==> R |] ==> R |
|
177 \idx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R |
|
178 \idx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R |
|
179 \subcaption{Sequent-style elimination rules} |
|
180 |
|
181 \idx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R |
|
182 \idx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R |
|
183 \idx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R |
|
184 \idx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R |
|
185 \idx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; |
|
186 S ==> R |] ==> R |
|
187 \idx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R |
|
188 \idx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R |
|
189 \end{ttbox} |
|
190 \subcaption{Intuitionistic simplification of implication} |
|
191 \caption{Derived rules for {\tt FOL}} \label{fol-int-derived} |
|
192 \end{figure} |
|
193 |
|
194 |
|
195 \section{Generic packages} |
|
196 \FOL{} instantiates most of Isabelle's generic packages; |
|
197 see \ttindexbold{FOL/ROOT.ML} for details. |
|
198 \begin{itemize} |
|
199 \item |
|
200 Because it includes a general substitution rule, \FOL{} instantiates the |
|
201 tactic \ttindex{hyp_subst_tac}, which substitutes for an equality |
|
202 throughout a subgoal and its hypotheses. |
|
203 \item |
|
204 It instantiates the simplifier. \ttindexbold{IFOL_ss} is the simplification |
|
205 set for intuitionistic first-order logic, while \ttindexbold{FOL_ss} is the |
|
206 simplification set for classical logic. Both equality ($=$) and the |
|
207 biconditional ($\bimp$) may be used for rewriting. See the file |
|
208 \ttindexbold{FOL/simpdata.ML} for a complete listing of the simplification |
|
209 rules. |
|
210 \item |
|
211 It instantiates the classical reasoning module. See~\S\ref{fol-cla-prover} |
|
212 for details. |
|
213 \end{itemize} |
|
214 |
|
215 |
|
216 \section{Intuitionistic proof procedures} \label{fol-int-prover} |
|
217 Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose |
|
218 difficulties for automated proof. Given $P\imp Q$ we may assume $Q$ |
|
219 provided we can prove $P$. In classical logic the proof of $P$ can assume |
|
220 $\neg P$, but the intuitionistic proof of $P$ may require repeated use of |
|
221 $P\imp Q$. If the proof of $P$ fails then the whole branch of the proof |
|
222 must be abandoned. Thus intuitionistic propositional logic requires |
|
223 backtracking. For an elementary example, consider the intuitionistic proof |
|
224 of $Q$ from $P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is |
|
225 needed twice: |
|
226 \[ \infer[({\imp}E)]{Q}{P\imp Q & |
|
227 \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} |
|
228 \] |
|
229 The theorem prover for intuitionistic logic does not use~{\tt impE}.\@ |
|
230 Instead, it simplifies implications using derived rules |
|
231 (Figure~\ref{fol-int-derived}). It reduces the antecedents of implications |
|
232 to atoms and then uses Modus Ponens: from $P\imp Q$ and $P$ deduce~$Q$. |
|
233 The rules \ttindex{conj_impE} and \ttindex{disj_impE} are |
|
234 straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and |
|
235 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp |
|
236 S$. The other \ldots{\tt_impE} rules are unsafe; the method requires |
|
237 backtracking. Observe that \ttindex{imp_impE} does not admit the (unsound) |
|
238 inference of~$P$ from $(P\imp Q)\imp S$. All the rules are derived in |
|
239 essentially the same simple manner. |
|
240 |
|
241 Dyckhoff has independently discovered similar rules, and (more importantly) |
|
242 has demonstrated their completeness for propositional |
|
243 logic~\cite{dyckhoff}. However, the tactics given below are not complete |
|
244 for first-order logic because they discard universally quantified |
|
245 assumptions after a single use. |
|
246 \begin{ttbox} |
|
247 mp_tac : int -> tactic |
|
248 eq_mp_tac : int -> tactic |
|
249 Int.safe_step_tac : int -> tactic |
|
250 Int.safe_tac : tactic |
|
251 Int.step_tac : int -> tactic |
|
252 Int.fast_tac : int -> tactic |
|
253 Int.best_tac : int -> tactic |
|
254 \end{ttbox} |
|
255 Most of these belong to the structure \ttindexbold{Int}. They are |
|
256 similar or identical to tactics (with the same names) provided by |
|
257 Isabelle's classical module (see {\em The Isabelle Reference Manual\/}). |
|
258 |
|
259 \begin{description} |
|
260 \item[\ttindexbold{mp_tac} {\it i}] |
|
261 attempts to use \ttindex{notE} or \ttindex{impE} within the assumptions in |
|
262 subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it |
|
263 searches for another assumption unifiable with~$P$. By |
|
264 contradiction with $\neg P$ it can solve the subgoal completely; by Modus |
|
265 Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can |
|
266 produce multiple outcomes, enumerating all suitable pairs of assumptions. |
|
267 |
|
268 \item[\ttindexbold{eq_mp_tac} {\it i}] |
|
269 is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it |
|
270 is safe. |
|
271 |
|
272 \item[\ttindexbold{Int.safe_step_tac} $i$] performs a safe step on |
|
273 subgoal~$i$. This may include proof by assumption or Modus Ponens, taking |
|
274 care not to instantiate unknowns, or \ttindex{hyp_subst_tac}. |
|
275 |
|
276 \item[\ttindexbold{Int.safe_tac}] repeatedly performs safe steps on all |
|
277 subgoals. It is deterministic, with at most one outcome. |
|
278 |
|
279 \item[\ttindexbold{Int.inst_step_tac} $i$] is like {\tt safe_step_tac}, |
|
280 but allows unknowns to be instantiated. |
|
281 |
|
282 \item[\ttindexbold{step_tac} $i$] tries {\tt safe_tac} or {\tt |
|
283 inst_step_tac}, or applies an unsafe rule. This is the basic step of the |
|
284 proof procedure. |
|
285 |
|
286 \item[\ttindexbold{Int.step_tac} $i$] tries {\tt safe_tac} or |
|
287 certain unsafe inferences. This is the basic step of the intuitionistic |
|
288 proof procedure. |
|
289 |
|
290 \item[\ttindexbold{Int.fast_tac} $i$] applies {\tt step_tac}, using |
|
291 depth-first search, to solve subgoal~$i$. |
|
292 |
|
293 \item[\ttindexbold{Int.best_tac} $i$] applies {\tt step_tac}, using |
|
294 best-first search (guided by the size of the proof state) to solve subgoal~$i$. |
|
295 \end{description} |
|
296 Here are some of the theorems that {\tt Int.fast_tac} proves |
|
297 automatically. The latter three date from {\it Principia Mathematica} |
|
298 (*11.53, *11.55, *11.61)~\cite{principia}. |
|
299 \begin{ttbox} |
|
300 ~~P & ~~(P --> Q) --> ~~Q |
|
301 (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y))) |
|
302 (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y))) |
|
303 (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y))) |
|
304 \end{ttbox} |
|
305 |
|
306 |
|
307 |
|
308 \begin{figure} |
|
309 \begin{ttbox} |
|
310 \idx{excluded_middle} ~P | P |
|
311 |
|
312 \idx{disjCI} (~Q ==> P) ==> P|Q |
|
313 \idx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x) |
|
314 \idx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R |
|
315 \idx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R |
|
316 \idx{notnotD} ~~P ==> P |
|
317 \idx{swap} ~P ==> (~Q ==> P) ==> Q |
|
318 \end{ttbox} |
|
319 \caption{Derived rules for classical logic} \label{fol-cla-derived} |
|
320 \end{figure} |
|
321 |
|
322 |
|
323 \section{Classical proof procedures} \label{fol-cla-prover} |
|
324 The classical theory has the \ML\ identifier \ttindexbold{FOL.thy}. It |
|
325 consists of intuitionistic logic plus the rule |
|
326 $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ |
|
327 \noindent |
|
328 Natural deduction in classical logic is not really all that natural. |
|
329 {\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as |
|
330 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap |
|
331 rule (see Figure~\ref{fol-cla-derived}). |
|
332 |
|
333 The classical reasoning module is set up for \FOL, as the |
|
334 structure~\ttindexbold{Cla}. This structure is open, so \ML{} identifiers |
|
335 such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. |
|
336 Single-step proofs can be performed, using \ttindex{swap_res_tac} to deal |
|
337 with negated assumptions. |
|
338 |
|
339 {\FOL} defines the following classical rule sets: |
|
340 \begin{ttbox} |
|
341 prop_cs : claset |
|
342 FOL_cs : claset |
|
343 FOL_dup_cs : claset |
|
344 \end{ttbox} |
|
345 \begin{description} |
|
346 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely |
|
347 those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, |
|
348 along with the rule~\ttindex{refl}. |
|
349 |
|
350 \item[\ttindexbold{FOL_cs}] |
|
351 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE} |
|
352 and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for |
|
353 unique existence. Search using this is incomplete since quantified |
|
354 formulae are used at most once. |
|
355 |
|
356 \item[\ttindexbold{FOL_dup_cs}] |
|
357 extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE} |
|
358 and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as |
|
359 rules for unique existence. Search using this is complete --- quantified |
|
360 formulae may be duplicated --- but frequently fails to terminate. It is |
|
361 generally unsuitable for depth-first search. |
|
362 \end{description} |
|
363 \noindent |
|
364 See the file \ttindexbold{FOL/fol.ML} for derivations of the |
|
365 classical rules, and the {\em Reference Manual} for more discussion of |
|
366 classical proof methods. |
|
367 |
|
368 |
|
369 \section{An intuitionistic example} |
|
370 Here is a session similar to one in {\em Logic and Computation} |
|
371 \cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently |
|
372 from {\sc lcf}-based theorem provers such as {\sc hol}. The proof begins |
|
373 by entering the goal in intuitionistic logic, then applying the rule |
|
374 $({\imp}I)$. |
|
375 \begin{ttbox} |
|
376 goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; |
|
377 {\out Level 0} |
|
378 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
379 {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
380 \ttbreak |
|
381 by (resolve_tac [impI] 1); |
|
382 {\out Level 1} |
|
383 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
384 {\out 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)} |
|
385 \end{ttbox} |
|
386 In this example we will never have more than one subgoal. Applying |
|
387 $({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making |
|
388 \(\ex{y}\all{x}Q(x,y)\) an assumption. We have the choice of |
|
389 $({\exists}E)$ and $({\forall}I)$; let us try the latter. |
|
390 \begin{ttbox} |
|
391 by (resolve_tac [allI] 1); |
|
392 {\out Level 2} |
|
393 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
394 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)} |
|
395 \end{ttbox} |
|
396 Applying $({\forall}I)$ replaces the \hbox{\tt ALL x} by \hbox{\tt!!x}, |
|
397 changing the universal quantifier from object~($\forall$) to |
|
398 meta~($\Forall$). The bound variable is a {\em parameter\/} of the |
|
399 subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What |
|
400 happens if the wrong rule is chosen? |
|
401 \begin{ttbox} |
|
402 by (resolve_tac [exI] 1); |
|
403 {\out Level 3} |
|
404 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
405 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))} |
|
406 \end{ttbox} |
|
407 The new subgoal~1 contains the function variable {\tt?y2}. Instantiating |
|
408 {\tt?y2} can replace~{\tt?y2(x)} by a term containing~{\tt x}, even |
|
409 though~{\tt x} is a bound variable. Now we analyse the assumption |
|
410 \(\exists y.\forall x. Q(x,y)\) using elimination rules: |
|
411 \begin{ttbox} |
|
412 by (eresolve_tac [exE] 1); |
|
413 {\out Level 4} |
|
414 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
415 {\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))} |
|
416 \end{ttbox} |
|
417 Applying $(\exists E)$ has produced the parameter {\tt y} and stripped the |
|
418 existential quantifier from the assumption. But the subgoal is unprovable. |
|
419 There is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}: |
|
420 assigning \verb|%x.y| to {\tt ?y2} is illegal because {\tt ?y2} is in the |
|
421 scope of the bound variable {\tt y}. Using \ttindex{choplev} we |
|
422 can return to the mistake. This time we apply $({\exists}E)$: |
|
423 \begin{ttbox} |
|
424 choplev 2; |
|
425 {\out Level 2} |
|
426 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
427 {\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)} |
|
428 \ttbreak |
|
429 by (eresolve_tac [exE] 1); |
|
430 {\out Level 3} |
|
431 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
432 {\out 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)} |
|
433 \end{ttbox} |
|
434 We now have two parameters and no scheme variables. Parameters should be |
|
435 produced early. Applying $({\exists}I)$ and $({\forall}E)$ will produce |
|
436 two scheme variables. |
|
437 \begin{ttbox} |
|
438 by (resolve_tac [exI] 1); |
|
439 {\out Level 4} |
|
440 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
441 {\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))} |
|
442 \ttbreak |
|
443 by (eresolve_tac [allE] 1); |
|
444 {\out Level 5} |
|
445 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
446 {\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))} |
|
447 \end{ttbox} |
|
448 The subgoal has variables {\tt ?y3} and {\tt ?x4} applied to both |
|
449 parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt |
|
450 x} and \verb|?y3(x,y)| with~{\tt y}. |
|
451 \begin{ttbox} |
|
452 by (assume_tac 1); |
|
453 {\out Level 6} |
|
454 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
455 {\out No subgoals!} |
|
456 \end{ttbox} |
|
457 The theorem was proved in six tactic steps, not counting the abandoned |
|
458 ones. But proof checking is tedious; {\tt Int.fast_tac} proves the |
|
459 theorem in one step. |
|
460 \begin{ttbox} |
|
461 goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; |
|
462 {\out Level 0} |
|
463 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
464 {\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
465 by (Int.fast_tac 1); |
|
466 {\out Level 1} |
|
467 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))} |
|
468 {\out No subgoals!} |
|
469 \end{ttbox} |
|
470 |
|
471 |
|
472 \section{An example of intuitionistic negation} |
|
473 The following example demonstrates the specialized forms of implication |
|
474 elimination. Even propositional formulae can be difficult to prove from |
|
475 the basic rules; the specialized rules help considerably. |
|
476 |
|
477 Propositional examples are easy to invent, for as Dummett notes~\cite[page |
|
478 28]{dummett}, $\neg P$ is classically provable if and only if it is |
|
479 intuitionistically provable. Therefore, $P$ is classically provable if and |
|
480 only if $\neg\neg P$ is intuitionistically provable. In both cases, $P$ |
|
481 must be a propositional formula (no quantifiers). Our example, |
|
482 accordingly, is the double negation of a classical tautology: $(P\imp |
|
483 Q)\disj (Q\imp P)$. |
|
484 |
|
485 When stating the goal, we command Isabelle to expand the negation symbol, |
|
486 using the definition $\neg P\equiv P\imp\bot$. Although negation possesses |
|
487 derived rules that effect precisely this definition --- the automatic |
|
488 tactics apply them --- it seems more straightforward to unfold the |
|
489 negations. |
|
490 \begin{ttbox} |
|
491 goalw IFOL.thy [not_def] "~ ~ ((P-->Q) | (Q-->P))"; |
|
492 {\out Level 0} |
|
493 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
494 {\out 1. ((P --> Q) | (Q --> P) --> False) --> False} |
|
495 \end{ttbox} |
|
496 The first step is trivial. |
|
497 \begin{ttbox} |
|
498 by (resolve_tac [impI] 1); |
|
499 {\out Level 1} |
|
500 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
501 {\out 1. (P --> Q) | (Q --> P) --> False ==> False} |
|
502 \end{ttbox} |
|
503 Proving $(P\imp Q)\disj (Q\imp P)$ would suffice, but this formula is |
|
504 constructively invalid. Instead we apply \ttindex{disj_impE}. It splits |
|
505 the assumption into two parts, one for each disjunct. |
|
506 \begin{ttbox} |
|
507 by (eresolve_tac [disj_impE] 1); |
|
508 {\out Level 2} |
|
509 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
510 {\out 1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False} |
|
511 \end{ttbox} |
|
512 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but |
|
513 their negations are inconsistent. Applying \ttindex{imp_impE} breaks down |
|
514 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new |
|
515 assumptions~$P$ and~$\neg Q$. |
|
516 \begin{ttbox} |
|
517 by (eresolve_tac [imp_impE] 1); |
|
518 {\out Level 3} |
|
519 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
520 {\out 1. [| (Q --> P) --> False; P; Q --> False |] ==> Q} |
|
521 {\out 2. [| (Q --> P) --> False; False |] ==> False} |
|
522 \end{ttbox} |
|
523 Subgoal~2 holds trivially; let us ignore it and continue working on |
|
524 subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$; |
|
525 applying \ttindex{imp_impE} is simpler. |
|
526 \begin{ttbox} |
|
527 by (eresolve_tac [imp_impE] 1); |
|
528 {\out Level 4} |
|
529 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
530 {\out 1. [| P; Q --> False; Q; P --> False |] ==> P} |
|
531 {\out 2. [| P; Q --> False; False |] ==> Q} |
|
532 {\out 3. [| (Q --> P) --> False; False |] ==> False} |
|
533 \end{ttbox} |
|
534 The three subgoals are all trivial. |
|
535 \begin{ttbox} |
|
536 by (REPEAT (eresolve_tac [FalseE] 2)); |
|
537 {\out Level 5} |
|
538 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
539 {\out 1. [| P; Q --> False; Q; P --> False |] ==> P} |
|
540 by (assume_tac 1); |
|
541 {\out Level 6} |
|
542 {\out ~ ~ ((P --> Q) | (Q --> P))} |
|
543 {\out No subgoals!} |
|
544 \end{ttbox} |
|
545 This proof is also trivial for {\tt Int.fast_tac}. |
|
546 |
|
547 |
|
548 \section{A classical example} \label{fol-cla-example} |
|
549 To illustrate classical logic, we shall prove the theorem |
|
550 $\ex{y}\all{x}P(y)\imp P(x)$. Classically, the theorem can be proved as |
|
551 follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise |
|
552 $\all{x}P(x)$ is true. Either way the theorem holds. |
|
553 |
|
554 The formal proof does not conform in any obvious way to the sketch given |
|
555 above. The key inference is the first one, \ttindex{exCI}; this classical |
|
556 version of~$(\exists I)$ allows multiple instantiation of the quantifier. |
|
557 \begin{ttbox} |
|
558 goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; |
|
559 {\out Level 0} |
|
560 {\out EX y. ALL x. P(y) --> P(x)} |
|
561 {\out 1. EX y. ALL x. P(y) --> P(x)} |
|
562 \ttbreak |
|
563 by (resolve_tac [exCI] 1); |
|
564 {\out Level 1} |
|
565 {\out EX y. ALL x. P(y) --> P(x)} |
|
566 {\out 1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)} |
|
567 \end{ttbox} |
|
568 We now can either exhibit a term {\tt?a} to satisfy the conclusion of |
|
569 subgoal~1, or produce a contradiction from the assumption. The next |
|
570 steps routinely break down the conclusion and assumption. |
|
571 \begin{ttbox} |
|
572 by (resolve_tac [allI] 1); |
|
573 {\out Level 2} |
|
574 {\out EX y. ALL x. P(y) --> P(x)} |
|
575 {\out 1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)} |
|
576 \ttbreak |
|
577 by (resolve_tac [impI] 1); |
|
578 {\out Level 3} |
|
579 {\out EX y. ALL x. P(y) --> P(x)} |
|
580 {\out 1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)} |
|
581 \ttbreak |
|
582 by (eresolve_tac [allE] 1); |
|
583 {\out Level 4} |
|
584 {\out EX y. ALL x. P(y) --> P(x)} |
|
585 {\out 1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)} |
|
586 \end{ttbox} |
|
587 In classical logic, a negated assumption is equivalent to a conclusion. To |
|
588 get this effect, we create a swapped version of $(\forall I)$ and apply it |
|
589 using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall |
|
590 I)$ using \ttindex{swap_res_tac}. |
|
591 \begin{ttbox} |
|
592 allI RSN (2,swap); |
|
593 {\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm} |
|
594 by (eresolve_tac [it] 1); |
|
595 {\out Level 5} |
|
596 {\out EX y. ALL x. P(y) --> P(x)} |
|
597 {\out 1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)} |
|
598 \end{ttbox} |
|
599 The previous conclusion, {\tt P(x)}, has become a negated assumption; |
|
600 we apply~$({\imp}I)$: |
|
601 \begin{ttbox} |
|
602 by (resolve_tac [impI] 1); |
|
603 {\out Level 6} |
|
604 {\out EX y. ALL x. P(y) --> P(x)} |
|
605 {\out 1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)} |
|
606 \end{ttbox} |
|
607 The subgoal has three assumptions. We produce a contradiction between the |
|
608 assumptions~\verb|~P(x)| and~{\tt P(?y3(x))}. The proof never instantiates |
|
609 the unknown~{\tt?a}. |
|
610 \begin{ttbox} |
|
611 by (eresolve_tac [notE] 1); |
|
612 {\out Level 7} |
|
613 {\out EX y. ALL x. P(y) --> P(x)} |
|
614 {\out 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)} |
|
615 \ttbreak |
|
616 by (assume_tac 1); |
|
617 {\out Level 8} |
|
618 {\out EX y. ALL x. P(y) --> P(x)} |
|
619 {\out No subgoals!} |
|
620 \end{ttbox} |
|
621 The civilized way to prove this theorem is through \ttindex{best_tac}, |
|
622 supplying the classical version of~$(\exists I)$: |
|
623 \begin{ttbox} |
|
624 goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; |
|
625 {\out Level 0} |
|
626 {\out EX y. ALL x. P(y) --> P(x)} |
|
627 {\out 1. EX y. ALL x. P(y) --> P(x)} |
|
628 by (best_tac FOL_dup_cs 1); |
|
629 {\out Level 1} |
|
630 {\out EX y. ALL x. P(y) --> P(x)} |
|
631 {\out No subgoals!} |
|
632 \end{ttbox} |
|
633 If this theorem seems counterintuitive, then perhaps you are an |
|
634 intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$ |
|
635 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$, |
|
636 which we cannot do without further knowledge about~$P$. |
|
637 |
|
638 |
|
639 \section{Derived rules and the classical tactics} |
|
640 Classical first-order logic can be extended with the propositional |
|
641 connective $if(P,Q,R)$, where |
|
642 $$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$ |
|
643 Theorems about $if$ can be proved by treating this as an abbreviation, |
|
644 replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But |
|
645 this duplicates~$P$, causing an exponential blowup and an unreadable |
|
646 formula. Introducing further abbreviations makes the problem worse. |
|
647 |
|
648 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$ |
|
649 directly, without reference to its definition. The simple identity |
|
650 \[ if(P,Q,R) \bimp (P\imp Q)\conj (\neg P\imp R) \] |
|
651 suggests that the |
|
652 $if$-introduction rule should be |
|
653 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{P} & \infer*{R}{\neg P}} \] |
|
654 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the |
|
655 elimination rules for~$\disj$ and~$\conj$. |
|
656 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} |
|
657 & \infer*{S}{[\neg P,R]}} |
|
658 \] |
|
659 Having made these plans, we get down to work with Isabelle. The theory of |
|
660 classical logic, \ttindex{FOL}, is extended with the constant |
|
661 $if::[o,o,o]\To o$. The axiom \ttindexbold{if_def} asserts the |
|
662 equation~$(if)$. |
|
663 \begin{ttbox} |
|
664 If = FOL + |
|
665 consts if :: "[o,o,o]=>o" |
|
666 rules if_def "if(P,Q,R) == P&Q | ~P&R" |
|
667 end |
|
668 \end{ttbox} |
|
669 The derivations of the introduction and elimination rules demonstrate the |
|
670 methods for rewriting with definitions. Classical reasoning is required, |
|
671 so we use \ttindex{fast_tac}. |
|
672 |
|
673 |
|
674 \subsection{Deriving the introduction rule} |
|
675 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, |
|
676 concludes $if(P,Q,R)$. We propose the conclusion as the main goal |
|
677 using~\ttindex{goalw}, which uses {\tt if_def} to rewrite occurrences |
|
678 of $if$ in the subgoal. |
|
679 \begin{ttbox} |
|
680 val prems = goalw If.thy [if_def] |
|
681 "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)"; |
|
682 {\out Level 0} |
|
683 {\out if(P,Q,R)} |
|
684 {\out 1. P & Q | ~ P & R} |
|
685 \end{ttbox} |
|
686 The premises (bound to the {\ML} variable {\tt prems}) are passed as |
|
687 introduction rules to \ttindex{fast_tac}: |
|
688 \begin{ttbox} |
|
689 by (fast_tac (FOL_cs addIs prems) 1); |
|
690 {\out Level 1} |
|
691 {\out if(P,Q,R)} |
|
692 {\out No subgoals!} |
|
693 val ifI = result(); |
|
694 \end{ttbox} |
|
695 |
|
696 |
|
697 \subsection{Deriving the elimination rule} |
|
698 The elimination rule has three premises, two of which are themselves rules. |
|
699 The conclusion is simply $S$. |
|
700 \begin{ttbox} |
|
701 val major::prems = goalw If.thy [if_def] |
|
702 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S"; |
|
703 {\out Level 0} |
|
704 {\out S} |
|
705 {\out 1. S} |
|
706 \end{ttbox} |
|
707 The major premise contains an occurrence of~$if$, but the version returned |
|
708 by \ttindex{goalw} (and bound to the {\ML} variable~{\tt major}) has the |
|
709 definition expanded. Now \ttindex{cut_facts_tac} inserts~{\tt major} as an |
|
710 assumption in the subgoal, so that \ttindex{fast_tac} can break it down. |
|
711 \begin{ttbox} |
|
712 by (cut_facts_tac [major] 1); |
|
713 {\out Level 1} |
|
714 {\out S} |
|
715 {\out 1. P & Q | ~ P & R ==> S} |
|
716 \ttbreak |
|
717 by (fast_tac (FOL_cs addIs prems) 1); |
|
718 {\out Level 2} |
|
719 {\out S} |
|
720 {\out No subgoals!} |
|
721 val ifE = result(); |
|
722 \end{ttbox} |
|
723 As you may recall from {\em Introduction to Isabelle}, there are other |
|
724 ways of treating definitions when deriving a rule. We can start the |
|
725 proof using \ttindex{goal}, which does not expand definitions, instead of |
|
726 \ttindex{goalw}. We can use \ttindex{rewrite_goals_tac} |
|
727 to expand definitions in the subgoals --- perhaps after calling |
|
728 \ttindex{cut_facts_tac} to insert the rule's premises. We can use |
|
729 \ttindex{rewrite_rule}, which is a meta-inference rule, to expand |
|
730 definitions in the premises directly. |
|
731 |
|
732 |
|
733 \subsection{Using the derived rules} |
|
734 The rules just derived have been saved with the {\ML} names \ttindex{ifI} |
|
735 and~\ttindex{ifE}. They permit natural proofs of theorems such as the |
|
736 following: |
|
737 \begin{eqnarray*} |
|
738 if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ |
|
739 if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) |
|
740 \end{eqnarray*} |
|
741 Proofs also require the classical reasoning rules and the $\bimp$ |
|
742 introduction rule (called~\ttindex{iffI}: do not confuse with~\ttindex{ifI}). |
|
743 |
|
744 To display the $if$-rules in action, let us analyse a proof step by step. |
|
745 \begin{ttbox} |
|
746 goal If.thy |
|
747 "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; |
|
748 {\out Level 0} |
|
749 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
750 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
751 \ttbreak |
|
752 by (resolve_tac [iffI] 1); |
|
753 {\out Level 1} |
|
754 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
755 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))} |
|
756 {\out 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} |
|
757 \end{ttbox} |
|
758 The $if$-elimination rule can be applied twice in succession. |
|
759 \begin{ttbox} |
|
760 by (eresolve_tac [ifE] 1); |
|
761 {\out Level 2} |
|
762 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
763 {\out 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
764 {\out 2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
765 {\out 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} |
|
766 \ttbreak |
|
767 by (eresolve_tac [ifE] 1); |
|
768 {\out Level 3} |
|
769 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
770 {\out 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
771 {\out 2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
772 {\out 3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
773 {\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} |
|
774 \end{ttbox} |
|
775 |
|
776 In the first two subgoals, all formulae have been reduced to atoms. Now |
|
777 $if$-introduction can be applied. Observe how the $if$-rules break down |
|
778 occurrences of $if$ when they become the outermost connective. |
|
779 \begin{ttbox} |
|
780 by (resolve_tac [ifI] 1); |
|
781 {\out Level 4} |
|
782 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
783 {\out 1. [| P; Q; A; Q |] ==> if(P,A,C)} |
|
784 {\out 2. [| P; Q; A; ~ Q |] ==> if(P,B,D)} |
|
785 {\out 3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
786 {\out 4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
787 {\out 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} |
|
788 \ttbreak |
|
789 by (resolve_tac [ifI] 1); |
|
790 {\out Level 5} |
|
791 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
792 {\out 1. [| P; Q; A; Q; P |] ==> A} |
|
793 {\out 2. [| P; Q; A; Q; ~ P |] ==> C} |
|
794 {\out 3. [| P; Q; A; ~ Q |] ==> if(P,B,D)} |
|
795 {\out 4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
796 {\out 5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))} |
|
797 {\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))} |
|
798 \end{ttbox} |
|
799 Where do we stand? The first subgoal holds by assumption; the second and |
|
800 third, by contradiction. This is getting tedious. Let us revert to the |
|
801 initial proof state and let \ttindex{fast_tac} solve it. The classical |
|
802 rule set {\tt if_cs} contains the rules of~{\FOL} plus the derived rules |
|
803 for~$if$. |
|
804 \begin{ttbox} |
|
805 choplev 0; |
|
806 {\out Level 0} |
|
807 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
808 {\out 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
809 val if_cs = FOL_cs addSIs [ifI] addSEs[ifE]; |
|
810 by (fast_tac if_cs 1); |
|
811 {\out Level 1} |
|
812 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))} |
|
813 {\out No subgoals!} |
|
814 \end{ttbox} |
|
815 This tactic also solves the other example. |
|
816 \begin{ttbox} |
|
817 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; |
|
818 {\out Level 0} |
|
819 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
820 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
821 \ttbreak |
|
822 by (fast_tac if_cs 1); |
|
823 {\out Level 1} |
|
824 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
825 {\out No subgoals!} |
|
826 \end{ttbox} |
|
827 |
|
828 |
|
829 \subsection{Derived rules versus definitions} |
|
830 Dispensing with the derived rules, we can treat $if$ as an |
|
831 abbreviation, and let \ttindex{fast_tac} prove the expanded formula. Let |
|
832 us redo the previous proof: |
|
833 \begin{ttbox} |
|
834 choplev 0; |
|
835 {\out Level 0} |
|
836 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
837 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
838 \ttbreak |
|
839 by (rewrite_goals_tac [if_def]); |
|
840 {\out Level 1} |
|
841 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
842 {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} |
|
843 {\out P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)} |
|
844 \ttbreak |
|
845 by (fast_tac FOL_cs 1); |
|
846 {\out Level 2} |
|
847 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))} |
|
848 {\out No subgoals!} |
|
849 \end{ttbox} |
|
850 Expanding definitions reduces the extended logic to the base logic. This |
|
851 approach has its merits --- especially if the prover for the base logic is |
|
852 good --- but can be slow. In these examples, proofs using {\tt if_cs} (the |
|
853 derived rules) run about six times faster than proofs using {\tt FOL_cs}. |
|
854 |
|
855 Expanding definitions also complicates error diagnosis. Suppose we are having |
|
856 difficulties in proving some goal. If by expanding definitions we have |
|
857 made it unreadable, then we have little hope of diagnosing the problem. |
|
858 |
|
859 Attempts at program verification often yield invalid assertions. |
|
860 Let us try to prove one: |
|
861 \begin{ttbox} |
|
862 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; |
|
863 {\out Level 0} |
|
864 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
865 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
866 by (fast_tac FOL_cs 1); |
|
867 {\out by: tactic failed} |
|
868 \end{ttbox} |
|
869 This failure message is uninformative, but we can get a closer look at the |
|
870 situation by applying \ttindex{step_tac}. |
|
871 \begin{ttbox} |
|
872 by (REPEAT (step_tac if_cs 1)); |
|
873 {\out Level 1} |
|
874 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
875 {\out 1. [| A; ~ P; R; ~ P; R |] ==> B} |
|
876 {\out 2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A} |
|
877 {\out 3. [| ~ P; R; B; ~ P; R |] ==> A} |
|
878 {\out 4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R} |
|
879 \end{ttbox} |
|
880 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false |
|
881 while~$R$ and~$A$ are true. This truth assignment reduces the main goal to |
|
882 $true\bimp false$, which is of course invalid. |
|
883 |
|
884 We can repeat this analysis by expanding definitions, using just |
|
885 the rules of {\FOL}: |
|
886 \begin{ttbox} |
|
887 choplev 0; |
|
888 {\out Level 0} |
|
889 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
890 {\out 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
891 \ttbreak |
|
892 by (rewrite_goals_tac [if_def]); |
|
893 {\out Level 1} |
|
894 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
895 {\out 1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->} |
|
896 {\out P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)} |
|
897 by (fast_tac FOL_cs 1); |
|
898 {\out by: tactic failed} |
|
899 \end{ttbox} |
|
900 Again we apply \ttindex{step_tac}: |
|
901 \begin{ttbox} |
|
902 by (REPEAT (step_tac FOL_cs 1)); |
|
903 {\out Level 2} |
|
904 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))} |
|
905 {\out 1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B} |
|
906 {\out 2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q} |
|
907 {\out 3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R} |
|
908 {\out 4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R} |
|
909 {\out 5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A} |
|
910 {\out 6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A} |
|
911 {\out 7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P} |
|
912 {\out 8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q} |
|
913 \end{ttbox} |
|
914 Subgoal~1 yields the same countermodel as before. But each proof step has |
|
915 taken six times as long, and the final result contains twice as many subgoals. |
|
916 |
|
917 Expanding definitions causes a great increase in complexity. This is why |
|
918 the classical prover has been designed to accept derived rules. |