104

1 
%% $Id$

287

2 
\chapter{FirstOrder logic}

104

3 
The directory~\ttindexbold{FOL} contains theories for firstorder logic


4 
based on Gentzen's natural deduction systems (which he called {\sc nj} and


5 
{\sc nk}). Intuitionistic logic is defined first; then classical logic is


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


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


8 
implications in the assumptions. Classical logic makes use of Isabelle's


9 
generic prover for classical reasoning, which simulates a sequent calculus.


10 


11 
\section{Syntax and rules of inference}


12 
The logic is manysorted, using Isabelle's type classes. The


13 
class of firstorder terms is called {\it term} and is a subclass of


14 
{\it logic}. No types of individuals


15 
are provided, but extensions can define types such as $nat::term$ and type


16 
constructors such as $list::(term)term$. See the examples directory.


17 
Below, the type variable $\alpha$ ranges over class {\it term\/}; the


18 
equality symbol and quantifiers are polymorphic (manysorted). The type of


19 
formulae is~{\it o}, which belongs to class {\it logic}.


20 
Figure~\ref{folsyntax} gives the syntax. Note that $a$\verb~=$b$ is


21 
translated to \verb~($a$=$b$\verb).


22 


23 
The intuitionistic theory has the \ML\ identifier


24 
\ttindexbold{IFOL.thy}. Figure~\ref{folrules} shows the inference


25 
rules with their~\ML\ names. Negation is defined in the usual way for


26 
intuitionistic logic; $\neg P$ abbreviates $P\imp\bot$. The


27 
biconditional~($\bimp$) is defined through $\conj$ and~$\imp$; introduction


28 
and elimination rules are derived for it.


29 


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


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


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


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


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


35 


36 
Some intuitionistic derived rules are shown in

287

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

104

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


39 
deduction typically involves a combination of forwards and backwards


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


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


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


43 
implications, and universal quantifiers. Used with elimresolution,


44 
\ttindex{allE} eliminates a universal quantifier while \ttindex{all_dupE}


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


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


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


48 

287

49 
See the files {\tt FOL/ifol.thy}, {\tt FOL/ifol.ML} and


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

104

51 
derived rules.


52 


53 
\begin{figure}


54 
\begin{center}


55 
\begin{tabular}{rrr}

111

56 
\it name &\it metatype & \it description \\


57 
\idx{Trueprop}& $o\To prop$ & coercion to $prop$\\


58 
\idx{Not} & $o\To o$ & negation ($\neg$) \\


59 
\idx{True} & $o$ & tautology ($\top$) \\


60 
\idx{False} & $o$ & absurdity ($\bot$)

104

61 
\end{tabular}


62 
\end{center}


63 
\subcaption{Constants}


64 


65 
\begin{center}


66 
\begin{tabular}{llrrr}

111

67 
\it symbol &\it name &\it metatype & \it precedence & \it description \\

104

68 
\idx{ALL} & \idx{All} & $(\alpha\To o)\To o$ & 10 &

111

69 
universal quantifier ($\forall$) \\

104

70 
\idx{EX} & \idx{Ex} & $(\alpha\To o)\To o$ & 10 &

111

71 
existential quantifier ($\exists$) \\

104

72 
\idx{EX!} & \idx{Ex1} & $(\alpha\To o)\To o$ & 10 &

111

73 
unique existence ($\exists!$)

104

74 
\end{tabular}


75 
\end{center}


76 
\subcaption{Binders}


77 


78 
\begin{center}


79 
\indexbold{*"=}


80 
\indexbold{&@{\tt\&}}


81 
\indexbold{*"}


82 
\indexbold{*""">}


83 
\indexbold{*"<"">}


84 
\begin{tabular}{rrrr}

111

85 
\it symbol & \it metatype & \it precedence & \it description \\


86 
\tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\


87 
\tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\


88 
\tt  & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\


89 
\tt > & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\


90 
\tt <> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)

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}


117 
\idx{refl} a=a


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


119 
\subcaption{Equality rules}


120 


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


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


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


124 


125 
\idx{disjI1} P ==> PQ


126 
\idx{disjI2} Q ==> PQ


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


128 


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


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


131 


132 
\idx{FalseE} False ==> P


133 
\subcaption{Propositional rules}


134 


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


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


137 


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


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


140 
\subcaption{Quantifier rules}


141 


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


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


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


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


146 
\subcaption{Definitions}


147 
\end{ttbox}


148 


149 
\caption{Rules of intuitionistic {\tt FOL}} \label{folrules}


150 
\end{figure}


151 


152 


153 
\begin{figure}


154 
\begin{ttbox}


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


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


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


158 
\subcaption{Derived equality rules}


159 


160 
\idx{TrueI} True


161 


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


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


164 


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


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


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


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


169 


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


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


172 
] ==> R


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


174 


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


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


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


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


179 
\subcaption{Sequentstyle elimination rules}


180 


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


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


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


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


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


186 
S ==> R ] ==> R


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


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


189 
\end{ttbox}


190 
\subcaption{Intuitionistic simplification of implication}


191 
\caption{Derived rules for {\tt FOL}} \label{folintderived}


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

104

209 
rules.


210 
\item


211 
It instantiates the classical reasoning module. See~\S\ref{folclaprover}


212 
for details.


213 
\end{itemize}


214 


215 


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


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


218 
difficulties for automated proof. Given $P\imp Q$ we may assume $Q$


219 
provided we can prove $P$. In classical logic the proof of $P$ can assume


220 
$\neg P$, but the intuitionistic proof of $P$ may require repeated use of


221 
$P\imp Q$. If the proof of $P$ fails then the whole branch of the proof


222 
must be abandoned. Thus intuitionistic propositional logic requires


223 
backtracking. For an elementary example, consider the intuitionistic proof


224 
of $Q$ from $P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is


225 
needed twice:


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


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


228 
\]


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


230 
Instead, it simplifies implications using derived rules

287

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

104

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


233 
The rules \ttindex{conj_impE} and \ttindex{disj_impE} are


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


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


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


237 
backtracking. Observe that \ttindex{imp_impE} does not admit the (unsound)


238 
inference of~$P$ from $(P\imp Q)\imp S$. All the rules are derived in


239 
essentially the same simple manner.


240 


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


242 
has demonstrated their completeness for propositional


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


244 
for firstorder logic because they discard universally quantified


245 
assumptions after a single use.


246 
\begin{ttbox}


247 
mp_tac : int > tactic


248 
eq_mp_tac : int > tactic


249 
Int.safe_step_tac : int > tactic


250 
Int.safe_tac : tactic


251 
Int.step_tac : int > tactic


252 
Int.fast_tac : int > tactic


253 
Int.best_tac : int > tactic


254 
\end{ttbox}


255 
Most of these belong to the structure \ttindexbold{Int}. They are


256 
similar or identical to tactics (with the same names) provided by

287

257 
Isabelle's classical module (see the {\em Reference Manual\/}).

104

258 


259 
\begin{description}


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


261 
attempts to use \ttindex{notE} or \ttindex{impE} within the assumptions in


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


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


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


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


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


267 


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


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


270 
is safe.


271 


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


273 
subgoal~$i$. This may include proof by assumption or Modus Ponens, taking


274 
care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.


275 


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


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


278 


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


280 
but allows unknowns to be instantiated.


281 


282 
\item[\ttindexbold{step_tac} $i$] tries {\tt safe_tac} or {\tt


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


284 
proof procedure.


285 


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


287 
certain unsafe inferences. This is the basic step of the intuitionistic


288 
proof procedure.


289 


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


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


292 


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


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


295 
\end{description}


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


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


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


299 
\begin{ttbox}


300 
~~P & ~~(P > Q) > ~~Q


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


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


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


304 
\end{ttbox}


305 


306 


307 


308 
\begin{figure}


309 
\begin{ttbox}


310 
\idx{excluded_middle} ~P  P


311 


312 
\idx{disjCI} (~Q ==> P) ==> PQ


313 
\idx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)


314 
\idx{impCE} [ P>Q; ~P ==> R; Q ==> R ] ==> R


315 
\idx{iffCE} [ P<>Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R


316 
\idx{notnotD} ~~P ==> P


317 
\idx{swap} ~P ==> (~Q ==> P) ==> Q


318 
\end{ttbox}


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


320 
\end{figure}


321 


322 


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


324 
The classical theory has the \ML\ identifier \ttindexbold{FOL.thy}. It


325 
consists of intuitionistic logic plus the rule


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


327 
\noindent


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


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


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

287

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

104

332 


333 
The classical reasoning module is set up for \FOL, as the


334 
structure~\ttindexbold{Cla}. This structure is open, so \ML{} identifiers


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


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


337 
with negated assumptions.


338 


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


340 
\begin{ttbox}


341 
prop_cs : claset


342 
FOL_cs : claset


343 
FOL_dup_cs : claset


344 
\end{ttbox}


345 
\begin{description}


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


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


348 
along with the rule~\ttindex{refl}.


349 


350 
\item[\ttindexbold{FOL_cs}]


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


352 
and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for


353 
unique existence. Search using this is incomplete since quantified


354 
formulae are used at most once.


355 


356 
\item[\ttindexbold{FOL_dup_cs}]


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


358 
and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as


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


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


361 
generally unsuitable for depthfirst search.


362 
\end{description}


363 
\noindent

287

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

104

365 
classical rules, and the {\em Reference Manual} for more discussion of


366 
classical proof methods.


367 


368 


369 
\section{An intuitionistic example}


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


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


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


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


374 
$({\imp}I)$.


375 
\begin{ttbox}


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


377 
{\out Level 0}


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


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


380 
\ttbreak


381 
by (resolve_tac [impI] 1);


382 
{\out Level 1}


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


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


385 
\end{ttbox}


386 
In this example we will never have more than one subgoal. Applying


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


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


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


390 
\begin{ttbox}


391 
by (resolve_tac [allI] 1);


392 
{\out Level 2}


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


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


395 
\end{ttbox}


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


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


398 
meta~($\Forall$). The bound variable is a {\em parameter\/} of the


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


400 
happens if the wrong rule is chosen?


401 
\begin{ttbox}


402 
by (resolve_tac [exI] 1);


403 
{\out Level 3}


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


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


406 
\end{ttbox}


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


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


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


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


411 
\begin{ttbox}


412 
by (eresolve_tac [exE] 1);


413 
{\out Level 4}


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


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


416 
\end{ttbox}


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


418 
existential quantifier from the assumption. But the subgoal is unprovable.


419 
There is no way to unify {\tt ?y2(x)} with the bound variable~{\tt y}:


420 
assigning \verb%x.y to {\tt ?y2} is illegal because {\tt ?y2} is in the


421 
scope of the bound variable {\tt y}. Using \ttindex{choplev} we


422 
can return to the mistake. This time we apply $({\exists}E)$:


423 
\begin{ttbox}


424 
choplev 2;


425 
{\out Level 2}


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


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


428 
\ttbreak


429 
by (eresolve_tac [exE] 1);


430 
{\out Level 3}


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


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


433 
\end{ttbox}


434 
We now have two parameters and no scheme variables. Parameters should be


435 
produced early. Applying $({\exists}I)$ and $({\forall}E)$ will produce


436 
two scheme variables.


437 
\begin{ttbox}


438 
by (resolve_tac [exI] 1);


439 
{\out Level 4}


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


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


442 
\ttbreak


443 
by (eresolve_tac [allE] 1);


444 
{\out Level 5}


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


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


447 
\end{ttbox}


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


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


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


451 
\begin{ttbox}


452 
by (assume_tac 1);


453 
{\out Level 6}


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


455 
{\out No subgoals!}


456 
\end{ttbox}


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


458 
ones. But proof checking is tedious; {\tt Int.fast_tac} proves the


459 
theorem in one step.


460 
\begin{ttbox}


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


462 
{\out Level 0}


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


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


465 
by (Int.fast_tac 1);


466 
{\out Level 1}


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


468 
{\out No subgoals!}


469 
\end{ttbox}


470 


471 


472 
\section{An example of intuitionistic negation}


473 
The following example demonstrates the specialized forms of implication


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


475 
the basic rules; the specialized rules help considerably.


476 


477 
Propositional examples are easy to invent, for as Dummett notes~\cite[page


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


479 
intuitionistically provable. Therefore, $P$ is classically provable if and


480 
only if $\neg\neg P$ is intuitionistically provable. In both cases, $P$


481 
must be a propositional formula (no quantifiers). Our example,


482 
accordingly, is the double negation of a classical tautology: $(P\imp


483 
Q)\disj (Q\imp P)$.


484 


485 
When stating the goal, we command Isabelle to expand the negation symbol,


486 
using the definition $\neg P\equiv P\imp\bot$. Although negation possesses


487 
derived rules that effect precisely this definition  the automatic


488 
tactics apply them  it seems more straightforward to unfold the


489 
negations.


490 
\begin{ttbox}


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


492 
{\out Level 0}


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


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


495 
\end{ttbox}


496 
The first step is trivial.


497 
\begin{ttbox}


498 
by (resolve_tac [impI] 1);


499 
{\out Level 1}


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


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


502 
\end{ttbox}


503 
Proving $(P\imp Q)\disj (Q\imp P)$ would suffice, but this formula is


504 
constructively invalid. Instead we apply \ttindex{disj_impE}. It splits


505 
the assumption into two parts, one for each disjunct.


506 
\begin{ttbox}


507 
by (eresolve_tac [disj_impE] 1);


508 
{\out Level 2}


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


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


511 
\end{ttbox}


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


513 
their negations are inconsistent. Applying \ttindex{imp_impE} breaks down


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


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


516 
\begin{ttbox}


517 
by (eresolve_tac [imp_impE] 1);


518 
{\out Level 3}


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


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


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


522 
\end{ttbox}


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


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


525 
applying \ttindex{imp_impE} is simpler.


526 
\begin{ttbox}


527 
by (eresolve_tac [imp_impE] 1);


528 
{\out Level 4}


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


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


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


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


533 
\end{ttbox}


534 
The three subgoals are all trivial.


535 
\begin{ttbox}


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


537 
{\out Level 5}


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


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

287

540 
\ttbreak

104

541 
by (assume_tac 1);


542 
{\out Level 6}


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


544 
{\out No subgoals!}


545 
\end{ttbox}


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


547 


548 


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


550 
To illustrate classical logic, we shall prove the theorem


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


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


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


554 


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


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


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


558 
\begin{ttbox}


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


560 
{\out Level 0}


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


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


563 
\ttbreak


564 
by (resolve_tac [exCI] 1);


565 
{\out Level 1}


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


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


568 
\end{ttbox}


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


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


571 
steps routinely break down the conclusion and assumption.


572 
\begin{ttbox}


573 
by (resolve_tac [allI] 1);


574 
{\out Level 2}


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


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


577 
\ttbreak


578 
by (resolve_tac [impI] 1);


579 
{\out Level 3}


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


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


582 
\ttbreak


583 
by (eresolve_tac [allE] 1);


584 
{\out Level 4}


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


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


587 
\end{ttbox}


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


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


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


591 
I)$ using \ttindex{swap_res_tac}.


592 
\begin{ttbox}


593 
allI RSN (2,swap);


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


595 
by (eresolve_tac [it] 1);


596 
{\out Level 5}


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


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


599 
\end{ttbox}


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


601 
we apply~$({\imp}I)$:


602 
\begin{ttbox}


603 
by (resolve_tac [impI] 1);


604 
{\out Level 6}


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


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


607 
\end{ttbox}


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


609 
assumptions~\verb~P(x) and~{\tt P(?y3(x))}. The proof never instantiates


610 
the unknown~{\tt?a}.


611 
\begin{ttbox}


612 
by (eresolve_tac [notE] 1);


613 
{\out Level 7}


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


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


616 
\ttbreak


617 
by (assume_tac 1);


618 
{\out Level 8}


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


620 
{\out No subgoals!}


621 
\end{ttbox}


622 
The civilized way to prove this theorem is through \ttindex{best_tac},


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


624 
\begin{ttbox}


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


626 
{\out Level 0}


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


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


629 
by (best_tac FOL_dup_cs 1);


630 
{\out Level 1}


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


632 
{\out No subgoals!}


633 
\end{ttbox}


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


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


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


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


638 


639 


640 
\section{Derived rules and the classical tactics}


641 
Classical firstorder logic can be extended with the propositional


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


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


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


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


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


647 
formula. Introducing further abbreviations makes the problem worse.


648 


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


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


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


652 
suggests that the


653 
$if$introduction rule should be

157

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

104

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


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


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


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


659 
\]


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


661 
classical logic, \ttindex{FOL}, is extended with the constant


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


663 
equation~$(if)$.


664 
\begin{ttbox}


665 
If = FOL +


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


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


668 
end


669 
\end{ttbox}


670 
The derivations of the introduction and elimination rules demonstrate the


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


672 
so we use \ttindex{fast_tac}.


673 


674 


675 
\subsection{Deriving the introduction rule}


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


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


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


679 
of $if$ in the subgoal.


680 
\begin{ttbox}


681 
val prems = goalw If.thy [if_def]


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


683 
{\out Level 0}


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


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


686 
\end{ttbox}


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


688 
introduction rules to \ttindex{fast_tac}:


689 
\begin{ttbox}


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


691 
{\out Level 1}


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


693 
{\out No subgoals!}


694 
val ifI = result();


695 
\end{ttbox}


696 


697 


698 
\subsection{Deriving the elimination rule}


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


700 
The conclusion is simply $S$.


701 
\begin{ttbox}


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


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


704 
{\out Level 0}


705 
{\out S}


706 
{\out 1. S}


707 
\end{ttbox}


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


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


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


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


712 
\begin{ttbox}


713 
by (cut_facts_tac [major] 1);


714 
{\out Level 1}


715 
{\out S}


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


717 
\ttbreak


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


719 
{\out Level 2}


720 
{\out S}


721 
{\out No subgoals!}


722 
val ifE = result();


723 
\end{ttbox}


724 
As you may recall from {\em Introduction to Isabelle}, there are other


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


726 
proof using \ttindex{goal}, which does not expand definitions, instead of


727 
\ttindex{goalw}. We can use \ttindex{rewrite_goals_tac}


728 
to expand definitions in the subgoals  perhaps after calling


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


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


731 
definitions in the premises directly.


732 


733 


734 
\subsection{Using the derived rules}


735 
The rules just derived have been saved with the {\ML} names \ttindex{ifI}


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


737 
following:


738 
\begin{eqnarray*}

111

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


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

104

741 
\end{eqnarray*}


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


743 
introduction rule (called~\ttindex{iffI}: do not confuse with~\ttindex{ifI}).


744 


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


746 
\begin{ttbox}


747 
goal If.thy


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


749 
{\out Level 0}


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


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


752 
\ttbreak


753 
by (resolve_tac [iffI] 1);


754 
{\out Level 1}


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


758 
\end{ttbox}


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


760 
\begin{ttbox}


761 
by (eresolve_tac [ifE] 1);


762 
{\out Level 2}


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


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


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


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


767 
\ttbreak


768 
by (eresolve_tac [ifE] 1);


769 
{\out Level 3}


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


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


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


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


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


775 
\end{ttbox}


776 


777 
In the first two subgoals, all formulae have been reduced to atoms. Now


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


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


780 
\begin{ttbox}


781 
by (resolve_tac [ifI] 1);


782 
{\out Level 4}


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


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


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


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


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


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


789 
\ttbreak


790 
by (resolve_tac [ifI] 1);


791 
{\out Level 5}


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


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


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


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


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


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


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


799 
\end{ttbox}


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


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


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


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


804 
for~$if$.


805 
\begin{ttbox}


806 
choplev 0;


807 
{\out Level 0}


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


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


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


811 
by (fast_tac if_cs 1);


812 
{\out Level 1}


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


814 
{\out No subgoals!}


815 
\end{ttbox}


816 
This tactic also solves the other example.


817 
\begin{ttbox}


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


819 
{\out Level 0}


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


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


822 
\ttbreak


823 
by (fast_tac if_cs 1);


824 
{\out Level 1}


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


826 
{\out No subgoals!}


827 
\end{ttbox}


828 


829 


830 
\subsection{Derived rules versus definitions}


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


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


833 
us redo the previous proof:


834 
\begin{ttbox}


835 
choplev 0;


836 
{\out Level 0}


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


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

287

839 
\end{ttbox}


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


841 
\begin{ttbox}

104

842 
by (rewrite_goals_tac [if_def]);


843 
{\out Level 1}


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


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


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

287

847 
\end{ttbox}


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


849 
\begin{ttbox}

104

850 
by (fast_tac FOL_cs 1);


851 
{\out Level 2}


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


853 
{\out No subgoals!}


854 
\end{ttbox}


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


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


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


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


859 


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


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


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


863 


864 
Attempts at program verification often yield invalid assertions.


865 
Let us try to prove one:


866 
\begin{ttbox}


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


868 
{\out Level 0}


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


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


871 
by (fast_tac FOL_cs 1);


872 
{\out by: tactic failed}


873 
\end{ttbox}


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


875 
situation by applying \ttindex{step_tac}.


876 
\begin{ttbox}


877 
by (REPEAT (step_tac if_cs 1));


878 
{\out Level 1}


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


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


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


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


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


884 
\end{ttbox}


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


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


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


888 


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


890 
the rules of {\FOL}:


891 
\begin{ttbox}


892 
choplev 0;


893 
{\out Level 0}


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


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


896 
\ttbreak


897 
by (rewrite_goals_tac [if_def]);


898 
{\out Level 1}


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


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


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


902 
by (fast_tac FOL_cs 1);


903 
{\out by: tactic failed}


904 
\end{ttbox}


905 
Again we apply \ttindex{step_tac}:


906 
\begin{ttbox}


907 
by (REPEAT (step_tac FOL_cs 1));


908 
{\out Level 2}


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


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


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


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


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


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


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


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


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


918 
\end{ttbox}


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


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


921 


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


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