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}

874

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


618 
which automatically uses the classical version of~$(\exists I)$:

104

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

874

624 
by (deepen_tac FOL_cs 0 1);


625 
{\out Depth = 0}


626 
{\out Depth = 2}

104

627 
{\out Level 1}


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


629 
{\out No subgoals!}


630 
\end{ttbox}


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


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


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


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


635 


636 


637 
\section{Derived rules and the classical tactics}


638 
Classical firstorder logic can be extended with the propositional


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


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


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


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


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


644 
formula. Introducing further abbreviations makes the problem worse.


645 


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


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

313

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

104

649 
suggests that the


650 
$if$introduction rule should be

157

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

104

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


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


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


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


656 
\]


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

313

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


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

104

660 
equation~$(if)$.


661 
\begin{ttbox}


662 
If = FOL +


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


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


665 
end


666 
\end{ttbox}


667 
The derivations of the introduction and elimination rules demonstrate the


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

313

669 
so we use {\tt fast_tac}.

104

670 


671 


672 
\subsection{Deriving the introduction rule}


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


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


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


676 
of $if$ in the subgoal.


677 
\begin{ttbox}


678 
val prems = goalw If.thy [if_def]


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


680 
{\out Level 0}


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


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


683 
\end{ttbox}


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


685 
introduction rules to \ttindex{fast_tac}:


686 
\begin{ttbox}


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


688 
{\out Level 1}


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


690 
{\out No subgoals!}


691 
val ifI = result();


692 
\end{ttbox}


693 


694 


695 
\subsection{Deriving the elimination rule}


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


697 
The conclusion is simply $S$.


698 
\begin{ttbox}


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


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


701 
{\out Level 0}


702 
{\out S}


703 
{\out 1. S}


704 
\end{ttbox}


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


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


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


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


709 
\begin{ttbox}


710 
by (cut_facts_tac [major] 1);


711 
{\out Level 1}


712 
{\out S}


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


714 
\ttbreak


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


716 
{\out Level 2}


717 
{\out S}


718 
{\out No subgoals!}


719 
val ifE = result();


720 
\end{ttbox}

313

721 
As you may recall from


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


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

104

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

313

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


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

104

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 metainference rule, to expand


730 
definitions in the premises directly.


731 


732 


733 
\subsection{Using the derived rules}

313

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


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

104

736 
following:


737 
\begin{eqnarray*}

111

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

104

740 
\end{eqnarray*}


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

313

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

104

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}

333

775 
%


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

104

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

287

838 
\end{ttbox}


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


840 
\begin{ttbox}

104

841 
by (rewrite_goals_tac [if_def]);


842 
{\out Level 1}


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


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


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

287

846 
\end{ttbox}


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


848 
\begin{ttbox}

104

849 
by (fast_tac FOL_cs 1);


850 
{\out Level 2}


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


852 
{\out No subgoals!}


853 
\end{ttbox}


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


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


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


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


858 


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


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


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


862 


863 
Attempts at program verification often yield invalid assertions.


864 
Let us try to prove one:


865 
\begin{ttbox}


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


867 
{\out Level 0}


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


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


870 
by (fast_tac FOL_cs 1);


871 
{\out by: tactic failed}


872 
\end{ttbox}


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


874 
situation by applying \ttindex{step_tac}.


875 
\begin{ttbox}


876 
by (REPEAT (step_tac if_cs 1));


877 
{\out Level 1}


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


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


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


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


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


883 
\end{ttbox}


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


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


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


887 


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


889 
the rules of {\FOL}:


890 
\begin{ttbox}


891 
choplev 0;


892 
{\out Level 0}


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


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


895 
\ttbreak


896 
by (rewrite_goals_tac [if_def]);


897 
{\out Level 1}


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


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


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


901 
by (fast_tac FOL_cs 1);


902 
{\out by: tactic failed}


903 
\end{ttbox}


904 
Again we apply \ttindex{step_tac}:


905 
\begin{ttbox}


906 
by (REPEAT (step_tac FOL_cs 1));


907 
{\out Level 2}


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


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


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


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


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


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


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


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


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


917 
\end{ttbox}


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


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


920 


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


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

313

923 


924 
\index{firstorder logic)}
