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 
FOL_dup_cs : claset


343 
\end{ttbox}

313

344 
\begin{ttdescription}

104

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


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

313

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

104

348 


349 
\item[\ttindexbold{FOL_cs}]

313

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


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

104

352 
unique existence. Search using this is incomplete since quantified


353 
formulae are used at most once.


354 


355 
\item[\ttindexbold{FOL_dup_cs}]

313

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


357 
and the unsafe rules {\tt all_dupE} and~{\tt exCI}, as well as

104

358 
rules for unique existence. Search using this is complete  quantified


359 
formulae may be duplicated  but frequently fails to terminate. It is


360 
generally unsuitable for depthfirst search.

313

361 
\end{ttdescription}

104

362 
\noindent

333

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

313

364 
classical rules, and


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


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


367 
for more discussion of classical proof methods.

104

368 


369 


370 
\section{An intuitionistic example}


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


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


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


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


375 
$({\imp}I)$.


376 
\begin{ttbox}


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


378 
{\out Level 0}


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


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


381 
\ttbreak


382 
by (resolve_tac [impI] 1);


383 
{\out Level 1}


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


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


386 
\end{ttbox}

313

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

104

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


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


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


391 
\begin{ttbox}


392 
by (resolve_tac [allI] 1);


393 
{\out Level 2}


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


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


396 
\end{ttbox}


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


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

313

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

104

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


401 
happens if the wrong rule is chosen?


402 
\begin{ttbox}


403 
by (resolve_tac [exI] 1);


404 
{\out Level 3}


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


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


407 
\end{ttbox}


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


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


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


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


412 
\begin{ttbox}


413 
by (eresolve_tac [exE] 1);


414 
{\out Level 4}


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


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


417 
\end{ttbox}


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

313

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


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


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


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

104

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}

313

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


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


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


437 
example demonstrates.

104

438 
\begin{ttbox}


439 
by (resolve_tac [exI] 1);


440 
{\out Level 4}


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


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


443 
\ttbreak


444 
by (eresolve_tac [allE] 1);


445 
{\out Level 5}


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


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


448 
\end{ttbox}


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


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


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


452 
\begin{ttbox}


453 
by (assume_tac 1);


454 
{\out Level 6}


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


456 
{\out No subgoals!}


457 
\end{ttbox}


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

313

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

104

460 
theorem in one step.


461 
\begin{ttbox}


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


463 
{\out Level 0}


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


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


466 
by (Int.fast_tac 1);


467 
{\out Level 1}


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


469 
{\out No subgoals!}


470 
\end{ttbox}


471 


472 


473 
\section{An example of intuitionistic negation}


474 
The following example demonstrates the specialized forms of implication


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


476 
the basic rules; the specialized rules help considerably.


477 

313

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

104

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

313

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


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


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


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


484 
much harder than proving~$P$ classically.

104

485 

313

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


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


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


489 
This allows use of the special implication rules.

104

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}

313

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


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


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


506 
assumption into two assumptions, one for each disjunct.

104

507 
\begin{ttbox}


508 
by (eresolve_tac [disj_impE] 1);


509 
{\out Level 2}


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


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


512 
\end{ttbox}


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

313

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

104

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


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


517 
\begin{ttbox}


518 
by (eresolve_tac [imp_impE] 1);


519 
{\out Level 3}


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


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


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


523 
\end{ttbox}


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


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

313

526 
applying \tdx{imp_impE} is simpler.

104

527 
\begin{ttbox}


528 
by (eresolve_tac [imp_impE] 1);


529 
{\out Level 4}


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


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


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


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


534 
\end{ttbox}


535 
The three subgoals are all trivial.


536 
\begin{ttbox}


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


538 
{\out Level 5}


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


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

287

541 
\ttbreak

104

542 
by (assume_tac 1);


543 
{\out Level 6}


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


545 
{\out No subgoals!}


546 
\end{ttbox}


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


548 


549 


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


551 
To illustrate classical logic, we shall prove the theorem

313

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

104

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


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


555 


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

313

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

104

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


559 
\begin{ttbox}


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


561 
{\out Level 0}


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


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


564 
\ttbreak


565 
by (resolve_tac [exCI] 1);


566 
{\out Level 1}


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


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


569 
\end{ttbox}

313

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

104

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

313

572 
steps are routine.

104

573 
\begin{ttbox}


574 
by (resolve_tac [allI] 1);


575 
{\out Level 2}


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


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


578 
\ttbreak


579 
by (resolve_tac [impI] 1);


580 
{\out Level 3}


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


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

313

583 
\end{ttbox}


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

333

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

313

586 
\begin{ttbox}

104

587 
by (eresolve_tac [allE] 1);


588 
{\out Level 4}


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


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


591 
\end{ttbox}


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

313

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

104

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


595 
I)$ using \ttindex{swap_res_tac}.


596 
\begin{ttbox}


597 
allI RSN (2,swap);


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


599 
by (eresolve_tac [it] 1);


600 
{\out Level 5}


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


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


603 
\end{ttbox}

313

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

104

605 
\begin{ttbox}


606 
by (resolve_tac [impI] 1);


607 
{\out Level 6}


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


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


610 
\end{ttbox}


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

313

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


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

104

614 
\begin{ttbox}


615 
by (eresolve_tac [notE] 1);


616 
{\out Level 7}


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


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


619 
\ttbreak


620 
by (assume_tac 1);


621 
{\out Level 8}


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


623 
{\out No subgoals!}


624 
\end{ttbox}

333

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

104

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


627 
\begin{ttbox}


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


629 
{\out Level 0}


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


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


632 
by (best_tac FOL_dup_cs 1);


633 
{\out Level 1}


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


635 
{\out No subgoals!}


636 
\end{ttbox}


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


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


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


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


641 


642 


643 
\section{Derived rules and the classical tactics}


644 
Classical firstorder logic can be extended with the propositional


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


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


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


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


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


650 
formula. Introducing further abbreviations makes the problem worse.


651 


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


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

313

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

104

655 
suggests that the


656 
$if$introduction rule should be

157

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

104

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


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


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


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


662 
\]


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

313

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


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

104

666 
equation~$(if)$.


667 
\begin{ttbox}


668 
If = FOL +


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


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


671 
end


672 
\end{ttbox}


673 
The derivations of the introduction and elimination rules demonstrate the


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

313

675 
so we use {\tt fast_tac}.

104

676 


677 


678 
\subsection{Deriving the introduction rule}


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


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


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


682 
of $if$ in the subgoal.


683 
\begin{ttbox}


684 
val prems = goalw If.thy [if_def]


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


686 
{\out Level 0}


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


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


689 
\end{ttbox}


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


691 
introduction rules to \ttindex{fast_tac}:


692 
\begin{ttbox}


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


694 
{\out Level 1}


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


696 
{\out No subgoals!}


697 
val ifI = result();


698 
\end{ttbox}


699 


700 


701 
\subsection{Deriving the elimination rule}


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


703 
The conclusion is simply $S$.


704 
\begin{ttbox}


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


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


707 
{\out Level 0}


708 
{\out S}


709 
{\out 1. S}


710 
\end{ttbox}


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


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


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


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


715 
\begin{ttbox}


716 
by (cut_facts_tac [major] 1);


717 
{\out Level 1}


718 
{\out S}


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


720 
\ttbreak


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


722 
{\out Level 2}


723 
{\out S}


724 
{\out No subgoals!}


725 
val ifE = result();


726 
\end{ttbox}

313

727 
As you may recall from


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


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

104

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

313

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


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

104

733 
to expand definitions in the subgoals  perhaps after calling


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


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


736 
definitions in the premises directly.


737 


738 


739 
\subsection{Using the derived rules}

313

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


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

104

742 
following:


743 
\begin{eqnarray*}

111

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


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

104

746 
\end{eqnarray*}


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

313

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

104

749 


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


751 
\begin{ttbox}


752 
goal If.thy


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


754 
{\out Level 0}


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


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


757 
\ttbreak


758 
by (resolve_tac [iffI] 1);


759 
{\out Level 1}


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. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}


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


763 
\end{ttbox}


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


765 
\begin{ttbox}


766 
by (eresolve_tac [ifE] 1);


767 
{\out Level 2}


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


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


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


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


772 
\ttbreak


773 
by (eresolve_tac [ifE] 1);


774 
{\out Level 3}


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


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


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


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


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


780 
\end{ttbox}

333

781 
%


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

104

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


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


785 
\begin{ttbox}


786 
by (resolve_tac [ifI] 1);


787 
{\out Level 4}


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


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


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


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


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


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


794 
\ttbreak


795 
by (resolve_tac [ifI] 1);


796 
{\out Level 5}


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


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


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


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


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


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


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


804 
\end{ttbox}


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


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


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


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


809 
for~$if$.


810 
\begin{ttbox}


811 
choplev 0;


812 
{\out Level 0}


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


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


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


816 
by (fast_tac if_cs 1);


817 
{\out Level 1}


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


819 
{\out No subgoals!}


820 
\end{ttbox}


821 
This tactic also solves the other example.


822 
\begin{ttbox}


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


824 
{\out Level 0}


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


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


827 
\ttbreak


828 
by (fast_tac if_cs 1);


829 
{\out Level 1}


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


831 
{\out No subgoals!}


832 
\end{ttbox}


833 


834 


835 
\subsection{Derived rules versus definitions}


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


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


838 
us redo the previous proof:


839 
\begin{ttbox}


840 
choplev 0;


841 
{\out Level 0}


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


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

287

844 
\end{ttbox}


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


846 
\begin{ttbox}

104

847 
by (rewrite_goals_tac [if_def]);


848 
{\out Level 1}


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


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


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

287

852 
\end{ttbox}


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


854 
\begin{ttbox}

104

855 
by (fast_tac FOL_cs 1);


856 
{\out Level 2}


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


858 
{\out No subgoals!}


859 
\end{ttbox}


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


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


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


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


864 


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


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


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


868 


869 
Attempts at program verification often yield invalid assertions.


870 
Let us try to prove one:


871 
\begin{ttbox}


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


873 
{\out Level 0}


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


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


876 
by (fast_tac FOL_cs 1);


877 
{\out by: tactic failed}


878 
\end{ttbox}


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


880 
situation by applying \ttindex{step_tac}.


881 
\begin{ttbox}


882 
by (REPEAT (step_tac if_cs 1));


883 
{\out Level 1}


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


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


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


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


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


889 
\end{ttbox}


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


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


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


893 


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


895 
the rules of {\FOL}:


896 
\begin{ttbox}


897 
choplev 0;


898 
{\out Level 0}


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


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


901 
\ttbreak


902 
by (rewrite_goals_tac [if_def]);


903 
{\out Level 1}


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


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


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


907 
by (fast_tac FOL_cs 1);


908 
{\out by: tactic failed}


909 
\end{ttbox}


910 
Again we apply \ttindex{step_tac}:


911 
\begin{ttbox}


912 
by (REPEAT (step_tac FOL_cs 1));


913 
{\out Level 2}


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


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


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


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


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


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


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


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


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


923 
\end{ttbox}


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


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


926 


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


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

313

929 


930 
\index{firstorder logic)}
