104

1 
%% $Id$

313

2 
\chapter{FirstOrder Logic}


3 
\index{firstorder logic(}


4 


5 
Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc


6 
nk}. Intuitionistic firstorder logic is defined first, as theory


7 
\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is

104

8 
obtained by adding the double negation rule. Basic proof procedures are


9 
provided. The intuitionistic prover works with derived rules to simplify

313

10 
implications in the assumptions. Classical~{\tt FOL} employs Isabelle's


11 
classical reasoner, which simulates a sequent calculus.

104

12 


13 
\section{Syntax and rules of inference}

313

14 
The logic is manysorted, using Isabelle's type classes. The class of


15 
firstorder terms is called \cldx{term} and is a subclass of {\tt logic}.


16 
No types of individuals are provided, but extensions can define types such


17 
as {\tt nat::term} and type constructors such as {\tt list::(term)term}


18 
(see the examples directory, {\tt FOL/ex}). Below, the type variable


19 
$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers


20 
are polymorphic (manysorted). The type of formulae is~\tydx{o}, which


21 
belongs to class~\cldx{logic}. Figure~\ref{folsyntax} gives the syntax.


22 
Note that $a$\verb~=$b$ is translated to $\neg(a=b)$.

104

23 

313

24 
Figure~\ref{folrules} shows the inference rules with their~\ML\ names.


25 
Negation is defined in the usual way for intuitionistic logic; $\neg P$


26 
abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through


27 
$\conj$ and~$\imp$; introduction and elimination rules are derived for it.

104

28 


29 
The unique existence quantifier, $\exists!x.P(x)$, is defined in terms


30 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested


31 
quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates


32 
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there


33 
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.


34 


35 
Some intuitionistic derived rules are shown in

287

36 
Fig.\ts\ref{folintderived}, again with their \ML\ names. These include

104

37 
rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural

333

38 
deduction typically involves a combination of forward and backward

104

39 
reasoning, particularly with the destruction rules $(\conj E)$,

333

40 
$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these

104

41 
rules badly, so sequentstyle rules are derived to eliminate conjunctions,


42 
implications, and universal quantifiers. Used with elimresolution,

313

43 
\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}

104

44 
reinserts the quantified formula for later use. The rules {\tt


45 
conj_impE}, etc., support the intuitionistic proof procedure


46 
(see~\S\ref{folintprover}).


47 

333

48 
See the files {\tt FOL/IFOL.thy}, {\tt FOL/IFOL.ML} and

287

49 
{\tt FOL/intprover.ML} for complete listings of the rules and

104

50 
derived rules.


51 


52 
\begin{figure}


53 
\begin{center}


54 
\begin{tabular}{rrr}

111

55 
\it name &\it metatype & \it description \\

313

56 
\cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\


57 
\cdx{Not} & $o\To o$ & negation ($\neg$) \\


58 
\cdx{True} & $o$ & tautology ($\top$) \\


59 
\cdx{False} & $o$ & absurdity ($\bot$)

104

60 
\end{tabular}


61 
\end{center}


62 
\subcaption{Constants}


63 


64 
\begin{center}


65 
\begin{tabular}{llrrr}

313

66 
\it symbol &\it name &\it metatype & \it priority & \it description \\


67 
\sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &

111

68 
universal quantifier ($\forall$) \\

313

69 
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &

111

70 
existential quantifier ($\exists$) \\

313

71 
{\tt EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 &

111

72 
unique existence ($\exists!$)

104

73 
\end{tabular}

313

74 
\index{*"E"X"! symbol}

104

75 
\end{center}


76 
\subcaption{Binders}


77 


78 
\begin{center}

313

79 
\index{*"= symbol}


80 
\index{&@{\tt\&} symbol}


81 
\index{*" symbol}


82 
\index{*"""> symbol}


83 
\index{*"<""> symbol}

104

84 
\begin{tabular}{rrrr}

313

85 
\it symbol & \it metatype & \it priority & \it description \\

111

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$)

104

91 
\end{tabular}


92 
\end{center}


93 
\subcaption{Infixes}


94 


95 
\dquotes


96 
\[\begin{array}{rcl}


97 
formula & = & \hbox{expression of type~$o$} \\

111

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

104

108 
\end{array}


109 
\]


110 
\subcaption{Grammar}


111 
\caption{Syntax of {\tt FOL}} \label{folsyntax}


112 
\end{figure}


113 


114 


115 
\begin{figure}


116 
\begin{ttbox}

313

117 
\tdx{refl} a=a


118 
\tdx{subst} [ a=b; P(a) ] ==> P(b)

104

119 
\subcaption{Equality rules}


120 

313

121 
\tdx{conjI} [ P; Q ] ==> P&Q


122 
\tdx{conjunct1} P&Q ==> P


123 
\tdx{conjunct2} P&Q ==> Q

104

124 

313

125 
\tdx{disjI1} P ==> PQ


126 
\tdx{disjI2} Q ==> PQ


127 
\tdx{disjE} [ PQ; P ==> R; Q ==> R ] ==> R

104

128 

313

129 
\tdx{impI} (P ==> Q) ==> P>Q


130 
\tdx{mp} [ P>Q; P ] ==> Q

104

131 

313

132 
\tdx{FalseE} False ==> P

104

133 
\subcaption{Propositional rules}


134 

313

135 
\tdx{allI} (!!x. P(x)) ==> (ALL x.P(x))


136 
\tdx{spec} (ALL x.P(x)) ==> P(x)

104

137 

313

138 
\tdx{exI} P(x) ==> (EX x.P(x))


139 
\tdx{exE} [ EX x.P(x); !!x. P(x) ==> R ] ==> R

104

140 
\subcaption{Quantifier rules}


141 

313

142 
\tdx{True_def} True == False>False


143 
\tdx{not_def} ~P == P>False


144 
\tdx{iff_def} P<>Q == (P>Q) & (Q>P)


145 
\tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)

104

146 
\subcaption{Definitions}


147 
\end{ttbox}


148 

313

149 
\caption{Rules of intuitionistic logic} \label{folrules}

104

150 
\end{figure}


151 


152 


153 
\begin{figure}


154 
\begin{ttbox}

313

155 
\tdx{sym} a=b ==> b=a


156 
\tdx{trans} [ a=b; b=c ] ==> a=c


157 
\tdx{ssubst} [ b=a; P(a) ] ==> P(b)

104

158 
\subcaption{Derived equality rules}


159 

313

160 
\tdx{TrueI} True

104

161 

313

162 
\tdx{notI} (P ==> False) ==> ~P


163 
\tdx{notE} [ ~P; P ] ==> R

104

164 

313

165 
\tdx{iffI} [ P ==> Q; Q ==> P ] ==> P<>Q


166 
\tdx{iffE} [ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R


167 
\tdx{iffD1} [ P <> Q; P ] ==> Q


168 
\tdx{iffD2} [ P <> Q; Q ] ==> P

104

169 

313

170 
\tdx{ex1I} [ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)


171 
\tdx{ex1E} [ EX! x.P(x); !!x.[ P(x); ALL y. P(y) > y=x ] ==> R

104

172 
] ==> R


173 
\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}


174 

313

175 
\tdx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R


176 
\tdx{impE} [ P>Q; P; Q ==> R ] ==> R


177 
\tdx{allE} [ ALL x.P(x); P(x) ==> R ] ==> R


178 
\tdx{all_dupE} [ ALL x.P(x); [ P(x); ALL x.P(x) ] ==> R ] ==> R

104

179 
\subcaption{Sequentstyle elimination rules}


180 

313

181 
\tdx{conj_impE} [ (P&Q)>S; P>(Q>S) ==> R ] ==> R


182 
\tdx{disj_impE} [ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R


183 
\tdx{imp_impE} [ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R


184 
\tdx{not_impE} [ ~P > S; P ==> False; S ==> R ] ==> R


185 
\tdx{iff_impE} [ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P;

104

186 
S ==> R ] ==> R

313

187 
\tdx{all_impE} [ (ALL x.P(x))>S; !!x.P(x); S ==> R ] ==> R


188 
\tdx{ex_impE} [ (EX x.P(x))>S; P(a)>S ==> R ] ==> R

104

189 
\end{ttbox}


190 
\subcaption{Intuitionistic simplification of implication}

313

191 
\caption{Derived rules for intuitionistic logic} \label{folintderived}

104

192 
\end{figure}


193 


194 


195 
\section{Generic packages}


196 
\FOL{} instantiates most of Isabelle's generic packages;

287

197 
see {\tt FOL/ROOT.ML} for details.

104

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 firstorder 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

287

208 
{\tt FOL/simpdata.ML} for a complete listing of the simplification

313

209 
rules%


210 
\iflabelundefined{sec:settingupsimp}{}%


211 
{, and \S\ref{sec:settingupsimp} for discussion}.


212 

104

213 
\item

313

214 
It instantiates the classical reasoner. See~\S\ref{folclaprover}

104

215 
for details.


216 
\end{itemize}


217 


218 


219 
\section{Intuitionistic proof procedures} \label{folintprover}


220 
Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose

313

221 
difficulties for automated proof. In intuitionistic logic, the assumption


222 
$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may


223 
use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated


224 
use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the


225 
proof must be abandoned. Thus intuitionistic propositional logic requires


226 
backtracking.


227 


228 
For an elementary example, consider the intuitionistic proof of $Q$ from


229 
$P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed


230 
twice:

104

231 
\[ \infer[({\imp}E)]{Q}{P\imp Q &


232 
\infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}}


233 
\]


234 
The theorem prover for intuitionistic logic does not use~{\tt impE}.\@


235 
Instead, it simplifies implications using derived rules

287

236 
(Fig.\ts\ref{folintderived}). It reduces the antecedents of implications

313

237 
to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.


238 
The rules \tdx{conj_impE} and \tdx{disj_impE} are

104

239 
straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and


240 
$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp


241 
S$. The other \ldots{\tt_impE} rules are unsafe; the method requires

313

242 
backtracking. All the rules are derived in the same simple manner.

104

243 


244 
Dyckhoff has independently discovered similar rules, and (more importantly)


245 
has demonstrated their completeness for propositional


246 
logic~\cite{dyckhoff}. However, the tactics given below are not complete


247 
for firstorder logic because they discard universally quantified


248 
assumptions after a single use.


249 
\begin{ttbox}


250 
mp_tac : int > tactic


251 
eq_mp_tac : int > tactic


252 
Int.safe_step_tac : int > tactic


253 
Int.safe_tac : tactic

313

254 
Int.inst_step_tac : int > tactic

104

255 
Int.step_tac : int > tactic


256 
Int.fast_tac : int > tactic


257 
Int.best_tac : int > tactic


258 
\end{ttbox}

313

259 
Most of these belong to the structure {\tt Int} and resemble the


260 
tactics of Isabelle's classical reasoner.

104

261 

313

262 
\begin{ttdescription}

104

263 
\item[\ttindexbold{mp_tac} {\it i}]

313

264 
attempts to use \tdx{notE} or \tdx{impE} within the assumptions in

104

265 
subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it


266 
searches for another assumption unifiable with~$P$. By


267 
contradiction with $\neg P$ it can solve the subgoal completely; by Modus


268 
Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can


269 
produce multiple outcomes, enumerating all suitable pairs of assumptions.


270 


271 
\item[\ttindexbold{eq_mp_tac} {\it i}]


272 
is like {\tt mp_tac} {\it i}, but may not instantiate unknowns  thus, it


273 
is safe.


274 


275 
\item[\ttindexbold{Int.safe_step_tac} $i$] performs a safe step on

313

276 
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking


277 
care not to instantiate unknowns), or {\tt hyp_subst_tac}.

104

278 


279 
\item[\ttindexbold{Int.safe_tac}] repeatedly performs safe steps on all


280 
subgoals. It is deterministic, with at most one outcome.


281 


282 
\item[\ttindexbold{Int.inst_step_tac} $i$] is like {\tt safe_step_tac},


283 
but allows unknowns to be instantiated.


284 

313

285 
\item[\ttindexbold{Int.step_tac} $i$] tries {\tt safe_tac} or {\tt


286 
inst_step_tac}, or applies an unsafe rule. This is the basic step of


287 
the intuitionistic proof procedure.

104

288 


289 
\item[\ttindexbold{Int.fast_tac} $i$] applies {\tt step_tac}, using


290 
depthfirst search, to solve subgoal~$i$.


291 


292 
\item[\ttindexbold{Int.best_tac} $i$] applies {\tt step_tac}, using


293 
bestfirst search (guided by the size of the proof state) to solve subgoal~$i$.

313

294 
\end{ttdescription}

104

295 
Here are some of the theorems that {\tt Int.fast_tac} proves


296 
automatically. The latter three date from {\it Principia Mathematica}


297 
(*11.53, *11.55, *11.61)~\cite{principia}.


298 
\begin{ttbox}


299 
~~P & ~~(P > Q) > ~~Q


300 
(ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))


301 
(EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))


302 
(EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))


303 
\end{ttbox}


304 


305 


306 


307 
\begin{figure}


308 
\begin{ttbox}

313

309 
\tdx{excluded_middle} ~P  P

104

310 

313

311 
\tdx{disjCI} (~Q ==> P) ==> PQ


312 
\tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)


313 
\tdx{impCE} [ P>Q; ~P ==> R; Q ==> R ] ==> R


314 
\tdx{iffCE} [ P<>Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R


315 
\tdx{notnotD} ~~P ==> P


316 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q

104

317 
\end{ttbox}


318 
\caption{Derived rules for classical logic} \label{folcladerived}


319 
\end{figure}


320 


321 


322 
\section{Classical proof procedures} \label{folclaprover}

313

323 
The classical theory, \thydx{FOL}, consists of intuitionistic logic plus


324 
the rule

104

325 
$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$


326 
\noindent


327 
Natural deduction in classical logic is not really all that natural.


328 
{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as


329 
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap

287

330 
rule (see Fig.\ts\ref{folcladerived}).

104

331 

313

332 
The classical reasoner is set up for \FOL, as the


333 
structure~{\tt Cla}. This structure is open, so \ML{} identifiers

104

334 
such as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.


335 
Singlestep proofs can be performed, using \ttindex{swap_res_tac} to deal

313

336 
with negated assumptions.\index{assumptions!negated}

104

337 


338 
{\FOL} defines the following classical rule sets:


339 
\begin{ttbox}


340 
prop_cs : claset


341 
FOL_cs : claset


342 
\end{ttbox}

313

343 
\begin{ttdescription}

104

344 
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely


345 
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,

313

346 
along with the rule~{\tt refl}.

104

347 


348 
\item[\ttindexbold{FOL_cs}]

313

349 
extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE}


350 
and the unsafe rules {\tt allE} and~{\tt exI}, as well as rules for

104

351 
unique existence. Search using this is incomplete since quantified


352 
formulae are used at most once.

313

353 
\end{ttdescription}

104

354 
\noindent

333

355 
See the file {\tt FOL/FOL.ML} for derivations of the

313

356 
classical rules, and


357 
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%


358 
{Chap.\ts\ref{chap:classical}}


359 
for more discussion of classical proof methods.

104

360 


361 


362 
\section{An intuitionistic example}


363 
Here is a session similar to one in {\em Logic and Computation}


364 
\cite[pages~2223]{paulson87}. Isabelle treats quantifiers differently


365 
from {\sc lcf}based theorem provers such as {\sc hol}. The proof begins


366 
by entering the goal in intuitionistic logic, then applying the rule


367 
$({\imp}I)$.


368 
\begin{ttbox}


369 
goal IFOL.thy "(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


370 
{\out Level 0}


371 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


372 
{\out 1. (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


373 
\ttbreak


374 
by (resolve_tac [impI] 1);


375 
{\out Level 1}


376 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


377 
{\out 1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}


378 
\end{ttbox}

313

379 
In this example, we shall never have more than one subgoal. Applying

104

380 
$({\imp}I)$ replaces~\verb> by~\verb==>, making


381 
\(\ex{y}\all{x}Q(x,y)\) an assumption. We have the choice of


382 
$({\exists}E)$ and $({\forall}I)$; let us try the latter.


383 
\begin{ttbox}


384 
by (resolve_tac [allI] 1);


385 
{\out Level 2}


386 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


387 
{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}


388 
\end{ttbox}


389 
Applying $({\forall}I)$ replaces the \hbox{\tt ALL x} by \hbox{\tt!!x},


390 
changing the universal quantifier from object~($\forall$) to

313

391 
meta~($\Forall$). The bound variable is a {\bf parameter} of the

104

392 
subgoal. We now must choose between $({\exists}I)$ and $({\exists}E)$. What


393 
happens if the wrong rule is chosen?


394 
\begin{ttbox}


395 
by (resolve_tac [exI] 1);


396 
{\out Level 3}


397 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


398 
{\out 1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}


399 
\end{ttbox}


400 
The new subgoal~1 contains the function variable {\tt?y2}. Instantiating


401 
{\tt?y2} can replace~{\tt?y2(x)} by a term containing~{\tt x}, even


402 
though~{\tt x} is a bound variable. Now we analyse the assumption


403 
\(\exists y.\forall x. Q(x,y)\) using elimination rules:


404 
\begin{ttbox}


405 
by (eresolve_tac [exE] 1);


406 
{\out Level 4}


407 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


408 
{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}


409 
\end{ttbox}


410 
Applying $(\exists E)$ has produced the parameter {\tt y} and stripped the

313

411 
existential quantifier from the assumption. But the subgoal is unprovable:


412 
there is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}.


413 
Using {\tt choplev} we can return to the critical point. This time we


414 
apply $({\exists}E)$:

104

415 
\begin{ttbox}


416 
choplev 2;


417 
{\out Level 2}


418 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


419 
{\out 1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}


420 
\ttbreak


421 
by (eresolve_tac [exE] 1);


422 
{\out Level 3}


423 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


424 
{\out 1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}


425 
\end{ttbox}

313

426 
We now have two parameters and no scheme variables. Applying


427 
$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are


428 
applied to those parameters. Parameters should be produced early, as this


429 
example demonstrates.

104

430 
\begin{ttbox}


431 
by (resolve_tac [exI] 1);


432 
{\out Level 4}


433 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


434 
{\out 1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}


435 
\ttbreak


436 
by (eresolve_tac [allE] 1);


437 
{\out Level 5}


438 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


439 
{\out 1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}


440 
\end{ttbox}


441 
The subgoal has variables {\tt ?y3} and {\tt ?x4} applied to both


442 
parameters. The obvious projection functions unify {\tt?x4(x,y)} with~{\tt


443 
x} and \verb?y3(x,y) with~{\tt y}.


444 
\begin{ttbox}


445 
by (assume_tac 1);


446 
{\out Level 6}


447 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


448 
{\out No subgoals!}


449 
\end{ttbox}


450 
The theorem was proved in six tactic steps, not counting the abandoned

313

451 
ones. But proof checking is tedious; \ttindex{Int.fast_tac} proves the

104

452 
theorem in one step.


453 
\begin{ttbox}


454 
goal IFOL.thy "(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


455 
{\out Level 0}


456 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


457 
{\out 1. (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


458 
by (Int.fast_tac 1);


459 
{\out Level 1}


460 
{\out (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))}


461 
{\out No subgoals!}


462 
\end{ttbox}


463 


464 


465 
\section{An example of intuitionistic negation}


466 
The following example demonstrates the specialized forms of implication


467 
elimination. Even propositional formulae can be difficult to prove from


468 
the basic rules; the specialized rules help considerably.


469 

313

470 
Propositional examples are easy to invent. As Dummett notes~\cite[page

104

471 
28]{dummett}, $\neg P$ is classically provable if and only if it is

313

472 
intuitionistically provable; therefore, $P$ is classically provable if and


473 
only if $\neg\neg P$ is intuitionistically provable.%


474 
\footnote{Of course this holds only for propositional logic, not if $P$ is


475 
allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is


476 
much harder than proving~$P$ classically.

104

477 

313

478 
Our example is the double negation of the classical tautology $(P\imp


479 
Q)\disj (Q\imp P)$. When stating the goal, we command Isabelle to expand


480 
negations to implications using the definition $\neg P\equiv P\imp\bot$.


481 
This allows use of the special implication rules.

104

482 
\begin{ttbox}


483 
goalw IFOL.thy [not_def] "~ ~ ((P>Q)  (Q>P))";


484 
{\out Level 0}


485 
{\out ~ ~ ((P > Q)  (Q > P))}


486 
{\out 1. ((P > Q)  (Q > P) > False) > False}


487 
\end{ttbox}


488 
The first step is trivial.


489 
\begin{ttbox}


490 
by (resolve_tac [impI] 1);


491 
{\out Level 1}


492 
{\out ~ ~ ((P > Q)  (Q > P))}


493 
{\out 1. (P > Q)  (Q > P) > False ==> False}


494 
\end{ttbox}

313

495 
By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but


496 
that formula is not a theorem of intuitionistic logic. Instead we apply


497 
the specialized implication rule \tdx{disj_impE}. It splits the


498 
assumption into two assumptions, one for each disjunct.

104

499 
\begin{ttbox}


500 
by (eresolve_tac [disj_impE] 1);


501 
{\out Level 2}


502 
{\out ~ ~ ((P > Q)  (Q > P))}


503 
{\out 1. [ (P > Q) > False; (Q > P) > False ] ==> False}


504 
\end{ttbox}


505 
We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but

313

506 
their negations are inconsistent. Applying \tdx{imp_impE} breaks down

104

507 
the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new


508 
assumptions~$P$ and~$\neg Q$.


509 
\begin{ttbox}


510 
by (eresolve_tac [imp_impE] 1);


511 
{\out Level 3}


512 
{\out ~ ~ ((P > Q)  (Q > P))}


513 
{\out 1. [ (Q > P) > False; P; Q > False ] ==> Q}


514 
{\out 2. [ (Q > P) > False; False ] ==> False}


515 
\end{ttbox}


516 
Subgoal~2 holds trivially; let us ignore it and continue working on


517 
subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$;

313

518 
applying \tdx{imp_impE} is simpler.

104

519 
\begin{ttbox}


520 
by (eresolve_tac [imp_impE] 1);


521 
{\out Level 4}


522 
{\out ~ ~ ((P > Q)  (Q > P))}


523 
{\out 1. [ P; Q > False; Q; P > False ] ==> P}


524 
{\out 2. [ P; Q > False; False ] ==> Q}


525 
{\out 3. [ (Q > P) > False; False ] ==> False}


526 
\end{ttbox}


527 
The three subgoals are all trivial.


528 
\begin{ttbox}


529 
by (REPEAT (eresolve_tac [FalseE] 2));


530 
{\out Level 5}


531 
{\out ~ ~ ((P > Q)  (Q > P))}


532 
{\out 1. [ P; Q > False; Q; P > False ] ==> P}

287

533 
\ttbreak

104

534 
by (assume_tac 1);


535 
{\out Level 6}


536 
{\out ~ ~ ((P > Q)  (Q > P))}


537 
{\out No subgoals!}


538 
\end{ttbox}


539 
This proof is also trivial for {\tt Int.fast_tac}.


540 


541 


542 
\section{A classical example} \label{folclaexample}


543 
To illustrate classical logic, we shall prove the theorem

313

544 
$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as

104

545 
follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise


546 
$\all{x}P(x)$ is true. Either way the theorem holds.


547 


548 
The formal proof does not conform in any obvious way to the sketch given

313

549 
above. The key inference is the first one, \tdx{exCI}; this classical

104

550 
version of~$(\exists I)$ allows multiple instantiation of the quantifier.


551 
\begin{ttbox}


552 
goal FOL.thy "EX y. ALL x. P(y)>P(x)";


553 
{\out Level 0}


554 
{\out EX y. ALL x. P(y) > P(x)}


555 
{\out 1. EX y. ALL x. P(y) > P(x)}


556 
\ttbreak


557 
by (resolve_tac [exCI] 1);


558 
{\out Level 1}


559 
{\out EX y. ALL x. P(y) > P(x)}


560 
{\out 1. ALL y. ~ (ALL x. P(y) > P(x)) ==> ALL x. P(?a) > P(x)}


561 
\end{ttbox}

313

562 
We can either exhibit a term {\tt?a} to satisfy the conclusion of

104

563 
subgoal~1, or produce a contradiction from the assumption. The next

313

564 
steps are routine.

104

565 
\begin{ttbox}


566 
by (resolve_tac [allI] 1);


567 
{\out Level 2}


568 
{\out EX y. ALL x. P(y) > P(x)}


569 
{\out 1. !!x. ALL y. ~ (ALL x. P(y) > P(x)) ==> P(?a) > P(x)}


570 
\ttbreak


571 
by (resolve_tac [impI] 1);


572 
{\out Level 3}


573 
{\out EX y. ALL x. P(y) > P(x)}


574 
{\out 1. !!x. [ ALL y. ~ (ALL x. P(y) > P(x)); P(?a) ] ==> P(x)}

313

575 
\end{ttbox}


576 
By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$

333

577 
in effect applies~$(\exists I)$ again.

313

578 
\begin{ttbox}

104

579 
by (eresolve_tac [allE] 1);


580 
{\out Level 4}


581 
{\out EX y. ALL x. P(y) > P(x)}


582 
{\out 1. !!x. [ P(?a); ~ (ALL xa. P(?y3(x)) > P(xa)) ] ==> P(x)}


583 
\end{ttbox}


584 
In classical logic, a negated assumption is equivalent to a conclusion. To

313

585 
get this effect, we create a swapped version of~$(\forall I)$ and apply it

104

586 
using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall


587 
I)$ using \ttindex{swap_res_tac}.


588 
\begin{ttbox}


589 
allI RSN (2,swap);


590 
{\out val it = "[ ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) ] ==> ?Q" : thm}


591 
by (eresolve_tac [it] 1);


592 
{\out Level 5}


593 
{\out EX y. ALL x. P(y) > P(x)}


594 
{\out 1. !!x xa. [ P(?a); ~ P(x) ] ==> P(?y3(x)) > P(xa)}


595 
\end{ttbox}

313

596 
The previous conclusion, {\tt P(x)}, has become a negated assumption.

104

597 
\begin{ttbox}


598 
by (resolve_tac [impI] 1);


599 
{\out Level 6}


600 
{\out EX y. ALL x. P(y) > P(x)}


601 
{\out 1. !!x xa. [ P(?a); ~ P(x); P(?y3(x)) ] ==> P(xa)}


602 
\end{ttbox}


603 
The subgoal has three assumptions. We produce a contradiction between the

313

604 
\index{assumptions!contradictory} assumptions~\verb~P(x) and~{\tt


605 
P(?y3(x))}. The proof never instantiates the unknown~{\tt?a}.

104

606 
\begin{ttbox}


607 
by (eresolve_tac [notE] 1);


608 
{\out Level 7}


609 
{\out EX y. ALL x. P(y) > P(x)}


610 
{\out 1. !!x xa. [ P(?a); P(?y3(x)) ] ==> P(x)}


611 
\ttbreak


612 
by (assume_tac 1);


613 
{\out Level 8}


614 
{\out EX y. ALL x. P(y) > P(x)}


615 
{\out No subgoals!}


616 
\end{ttbox}

333

617 
The civilised way to prove this theorem is through \ttindex{best_tac},

104

618 
supplying the classical version of~$(\exists I)$:


619 
\begin{ttbox}


620 
goal FOL.thy "EX y. ALL x. P(y)>P(x)";


621 
{\out Level 0}


622 
{\out EX y. ALL x. P(y) > P(x)}


623 
{\out 1. EX y. ALL x. P(y) > P(x)}


624 
by (best_tac FOL_dup_cs 1);


625 
{\out Level 1}


626 
{\out EX y. ALL x. P(y) > P(x)}


627 
{\out No subgoals!}


628 
\end{ttbox}


629 
If this theorem seems counterintuitive, then perhaps you are an


630 
intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$


631 
requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,


632 
which we cannot do without further knowledge about~$P$.


633 


634 


635 
\section{Derived rules and the classical tactics}


636 
Classical firstorder logic can be extended with the propositional


637 
connective $if(P,Q,R)$, where


638 
$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$


639 
Theorems about $if$ can be proved by treating this as an abbreviation,


640 
replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But


641 
this duplicates~$P$, causing an exponential blowup and an unreadable


642 
formula. Introducing further abbreviations makes the problem worse.


643 


644 
Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$


645 
directly, without reference to its definition. The simple identity

313

646 
\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]

104

647 
suggests that the


648 
$if$introduction rule should be

157

649 
\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \]

104

650 
The $if$elimination rule reflects the definition of $if(P,Q,R)$ and the


651 
elimination rules for~$\disj$ and~$\conj$.


652 
\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}


653 
& \infer*{S}{[\neg P,R]}}


654 
\]


655 
Having made these plans, we get down to work with Isabelle. The theory of

313

656 
classical logic, {\tt FOL}, is extended with the constant


657 
$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the

104

658 
equation~$(if)$.


659 
\begin{ttbox}


660 
If = FOL +


661 
consts if :: "[o,o,o]=>o"


662 
rules if_def "if(P,Q,R) == P&Q  ~P&R"


663 
end


664 
\end{ttbox}


665 
The derivations of the introduction and elimination rules demonstrate the


666 
methods for rewriting with definitions. Classical reasoning is required,

313

667 
so we use {\tt fast_tac}.

104

668 


669 


670 
\subsection{Deriving the introduction rule}


671 
The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,


672 
concludes $if(P,Q,R)$. We propose the conclusion as the main goal


673 
using~\ttindex{goalw}, which uses {\tt if_def} to rewrite occurrences


674 
of $if$ in the subgoal.


675 
\begin{ttbox}


676 
val prems = goalw If.thy [if_def]


677 
"[ P ==> Q; ~ P ==> R ] ==> if(P,Q,R)";


678 
{\out Level 0}


679 
{\out if(P,Q,R)}


680 
{\out 1. P & Q  ~ P & R}


681 
\end{ttbox}


682 
The premises (bound to the {\ML} variable {\tt prems}) are passed as


683 
introduction rules to \ttindex{fast_tac}:


684 
\begin{ttbox}


685 
by (fast_tac (FOL_cs addIs prems) 1);


686 
{\out Level 1}


687 
{\out if(P,Q,R)}


688 
{\out No subgoals!}


689 
val ifI = result();


690 
\end{ttbox}


691 


692 


693 
\subsection{Deriving the elimination rule}


694 
The elimination rule has three premises, two of which are themselves rules.


695 
The conclusion is simply $S$.


696 
\begin{ttbox}


697 
val major::prems = goalw If.thy [if_def]


698 
"[ if(P,Q,R); [ P; Q ] ==> S; [ ~ P; R ] ==> S ] ==> S";


699 
{\out Level 0}


700 
{\out S}


701 
{\out 1. S}


702 
\end{ttbox}


703 
The major premise contains an occurrence of~$if$, but the version returned


704 
by \ttindex{goalw} (and bound to the {\ML} variable~{\tt major}) has the


705 
definition expanded. Now \ttindex{cut_facts_tac} inserts~{\tt major} as an


706 
assumption in the subgoal, so that \ttindex{fast_tac} can break it down.


707 
\begin{ttbox}


708 
by (cut_facts_tac [major] 1);


709 
{\out Level 1}


710 
{\out S}


711 
{\out 1. P & Q  ~ P & R ==> S}


712 
\ttbreak


713 
by (fast_tac (FOL_cs addIs prems) 1);


714 
{\out Level 2}


715 
{\out S}


716 
{\out No subgoals!}


717 
val ifE = result();


718 
\end{ttbox}

313

719 
As you may recall from


720 
\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%


721 
{\S\ref{definitions}}, there are other

104

722 
ways of treating definitions when deriving a rule. We can start the

313

723 
proof using {\tt goal}, which does not expand definitions, instead of


724 
{\tt goalw}. We can use \ttindex{rewrite_goals_tac}

104

725 
to expand definitions in the subgoals  perhaps after calling


726 
\ttindex{cut_facts_tac} to insert the rule's premises. We can use


727 
\ttindex{rewrite_rule}, which is a metainference rule, to expand


728 
definitions in the premises directly.


729 


730 


731 
\subsection{Using the derived rules}

313

732 
The rules just derived have been saved with the {\ML} names \tdx{ifI}


733 
and~\tdx{ifE}. They permit natural proofs of theorems such as the

104

734 
following:


735 
\begin{eqnarray*}

111

736 
if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\


737 
if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B))

104

738 
\end{eqnarray*}


739 
Proofs also require the classical reasoning rules and the $\bimp$

313

740 
introduction rule (called~\tdx{iffI}: do not confuse with~{\tt ifI}).

104

741 


742 
To display the $if$rules in action, let us analyse a proof step by step.


743 
\begin{ttbox}


744 
goal If.thy


745 
"if(P, if(Q,A,B), if(Q,C,D)) <> if(Q, if(P,A,C), if(P,B,D))";


746 
{\out Level 0}


747 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


748 
{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


749 
\ttbreak


750 
by (resolve_tac [iffI] 1);


751 
{\out Level 1}


752 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


753 
{\out 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}


754 
{\out 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}


755 
\end{ttbox}


756 
The $if$elimination rule can be applied twice in succession.


757 
\begin{ttbox}


758 
by (eresolve_tac [ifE] 1);


759 
{\out Level 2}


760 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


761 
{\out 1. [ P; if(Q,A,B) ] ==> if(Q,if(P,A,C),if(P,B,D))}


762 
{\out 2. [ ~ P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))}


763 
{\out 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}


764 
\ttbreak


765 
by (eresolve_tac [ifE] 1);


766 
{\out Level 3}


767 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


768 
{\out 1. [ P; Q; A ] ==> if(Q,if(P,A,C),if(P,B,D))}


769 
{\out 2. [ P; ~ Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))}


770 
{\out 3. [ ~ P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))}


771 
{\out 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}


772 
\end{ttbox}

333

773 
%


774 
In the first two subgoals, all assumptions have been reduced to atoms. Now

104

775 
$if$introduction can be applied. Observe how the $if$rules break down


776 
occurrences of $if$ when they become the outermost connective.


777 
\begin{ttbox}


778 
by (resolve_tac [ifI] 1);


779 
{\out Level 4}


780 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


781 
{\out 1. [ P; Q; A; Q ] ==> if(P,A,C)}


782 
{\out 2. [ P; Q; A; ~ Q ] ==> if(P,B,D)}


783 
{\out 3. [ P; ~ Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))}


784 
{\out 4. [ ~ P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))}


785 
{\out 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}


786 
\ttbreak


787 
by (resolve_tac [ifI] 1);


788 
{\out Level 5}


789 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


790 
{\out 1. [ P; Q; A; Q; P ] ==> A}


791 
{\out 2. [ P; Q; A; Q; ~ P ] ==> C}


792 
{\out 3. [ P; Q; A; ~ Q ] ==> if(P,B,D)}


793 
{\out 4. [ P; ~ Q; B ] ==> if(Q,if(P,A,C),if(P,B,D))}


794 
{\out 5. [ ~ P; if(Q,C,D) ] ==> if(Q,if(P,A,C),if(P,B,D))}


795 
{\out 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}


796 
\end{ttbox}


797 
Where do we stand? The first subgoal holds by assumption; the second and


798 
third, by contradiction. This is getting tedious. Let us revert to the


799 
initial proof state and let \ttindex{fast_tac} solve it. The classical


800 
rule set {\tt if_cs} contains the rules of~{\FOL} plus the derived rules


801 
for~$if$.


802 
\begin{ttbox}


803 
choplev 0;


804 
{\out Level 0}


805 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


806 
{\out 1. if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


807 
val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];


808 
by (fast_tac if_cs 1);


809 
{\out Level 1}


810 
{\out if(P,if(Q,A,B),if(Q,C,D)) <> if(Q,if(P,A,C),if(P,B,D))}


811 
{\out No subgoals!}


812 
\end{ttbox}


813 
This tactic also solves the other example.


814 
\begin{ttbox}


815 
goal If.thy "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,A,B))";


816 
{\out Level 0}


817 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}


818 
{\out 1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}


819 
\ttbreak


820 
by (fast_tac if_cs 1);


821 
{\out Level 1}


822 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}


823 
{\out No subgoals!}


824 
\end{ttbox}


825 


826 


827 
\subsection{Derived rules versus definitions}


828 
Dispensing with the derived rules, we can treat $if$ as an


829 
abbreviation, and let \ttindex{fast_tac} prove the expanded formula. Let


830 
us redo the previous proof:


831 
\begin{ttbox}


832 
choplev 0;


833 
{\out Level 0}


834 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}


835 
{\out 1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}

287

836 
\end{ttbox}


837 
This time, simply unfold using the definition of $if$:


838 
\begin{ttbox}

104

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)}

287

844 
\end{ttbox}


845 
We are left with a subgoal in pure firstorder logic:


846 
\begin{ttbox}

104

847 
by (fast_tac FOL_cs 1);


848 
{\out Level 2}


849 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,A,B))}


850 
{\out No subgoals!}


851 
\end{ttbox}


852 
Expanding definitions reduces the extended logic to the base logic. This


853 
approach has its merits  especially if the prover for the base logic is


854 
good  but can be slow. In these examples, proofs using {\tt if_cs} (the


855 
derived rules) run about six times faster than proofs using {\tt FOL_cs}.


856 


857 
Expanding definitions also complicates error diagnosis. Suppose we are having


858 
difficulties in proving some goal. If by expanding definitions we have


859 
made it unreadable, then we have little hope of diagnosing the problem.


860 


861 
Attempts at program verification often yield invalid assertions.


862 
Let us try to prove one:


863 
\begin{ttbox}


864 
goal If.thy "if(if(P,Q,R), A, B) <> if(P, if(Q,A,B), if(R,B,A))";


865 
{\out Level 0}


866 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


867 
{\out 1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


868 
by (fast_tac FOL_cs 1);


869 
{\out by: tactic failed}


870 
\end{ttbox}


871 
This failure message is uninformative, but we can get a closer look at the


872 
situation by applying \ttindex{step_tac}.


873 
\begin{ttbox}


874 
by (REPEAT (step_tac if_cs 1));


875 
{\out Level 1}


876 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


877 
{\out 1. [ A; ~ P; R; ~ P; R ] ==> B}


878 
{\out 2. [ B; ~ P; ~ R; ~ P; ~ R ] ==> A}


879 
{\out 3. [ ~ P; R; B; ~ P; R ] ==> A}


880 
{\out 4. [ ~ P; ~ R; A; ~ B; ~ P ] ==> R}


881 
\end{ttbox}


882 
Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false


883 
while~$R$ and~$A$ are true. This truth assignment reduces the main goal to


884 
$true\bimp false$, which is of course invalid.


885 


886 
We can repeat this analysis by expanding definitions, using just


887 
the rules of {\FOL}:


888 
\begin{ttbox}


889 
choplev 0;


890 
{\out Level 0}


891 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


892 
{\out 1. if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


893 
\ttbreak


894 
by (rewrite_goals_tac [if_def]);


895 
{\out Level 1}


896 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


897 
{\out 1. (P & Q  ~ P & R) & A  ~ (P & Q  ~ P & R) & B <>}


898 
{\out P & (Q & A  ~ Q & B)  ~ P & (R & B  ~ R & A)}


899 
by (fast_tac FOL_cs 1);


900 
{\out by: tactic failed}


901 
\end{ttbox}


902 
Again we apply \ttindex{step_tac}:


903 
\begin{ttbox}


904 
by (REPEAT (step_tac FOL_cs 1));


905 
{\out Level 2}


906 
{\out if(if(P,Q,R),A,B) <> if(P,if(Q,A,B),if(R,B,A))}


907 
{\out 1. [ A; ~ P; R; ~ P; R; ~ False ] ==> B}


908 
{\out 2. [ A; ~ P; R; R; ~ False; ~ B; ~ B ] ==> Q}


909 
{\out 3. [ B; ~ P; ~ R; ~ P; ~ A ] ==> R}


910 
{\out 4. [ B; ~ P; ~ R; ~ Q; ~ A ] ==> R}


911 
{\out 5. [ B; ~ R; ~ P; ~ A; ~ R; Q; ~ False ] ==> A}


912 
{\out 6. [ ~ P; R; B; ~ P; R; ~ False ] ==> A}


913 
{\out 7. [ ~ P; ~ R; A; ~ B; ~ R ] ==> P}


914 
{\out 8. [ ~ P; ~ R; A; ~ B; ~ R ] ==> Q}


915 
\end{ttbox}


916 
Subgoal~1 yields the same countermodel as before. But each proof step has


917 
taken six times as long, and the final result contains twice as many subgoals.


918 


919 
Expanding definitions causes a great increase in complexity. This is why


920 
the classical prover has been designed to accept derived rules.

313

921 


922 
\index{firstorder logic)}
