104

1 
%% $Id$


2 
\chapter{Firstorder logic}


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


37 
Figure~\ref{folintderived}, again with their \ML\ names. These include


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


39 
deduction typically involves a combination of forwards and backwards


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


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


42 
rules badly, so 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 


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

111

50 
\ttindexbold{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;


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


198 
\begin{itemize}


199 
\item


200 
Because it includes a general substitution rule, \FOL{} instantiates the


201 
tactic \ttindex{hyp_subst_tac}, which substitutes for an equality


202 
throughout a subgoal and its hypotheses.


203 
\item


204 
It instantiates the simplifier. \ttindexbold{IFOL_ss} is the simplification


205 
set for intuitionistic 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


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


209 
rules.


210 
\item


211 
It instantiates the classical reasoning module. See~\S\ref{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


231 
(Figure~\ref{folintderived}). It reduces the antecedents of implications


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


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


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


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


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


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


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


239 
essentially the same simple manner.


240 


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


242 
has demonstrated their completeness for propositional


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


244 
for 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


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


258 


259 
\begin{description}


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


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


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


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


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


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


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


267 


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


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


270 
is safe.


271 


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


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


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


275 


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


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


278 


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


280 
but allows unknowns to be instantiated.


281 


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


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


284 
proof procedure.


285 


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


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


288 
proof procedure.


289 


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


291 
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


331 
rule (see Figure~\ref{folcladerived}).


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


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


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


366 
classical proof methods.


367 


368 


369 
\section{An intuitionistic example}


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


371 
\cite[pages~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}


540 
by (assume_tac 1);


541 
{\out Level 6}


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


543 
{\out No subgoals!}


544 
\end{ttbox}


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


546 


547 


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


549 
To illustrate classical logic, we shall prove the theorem


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


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


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


553 


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


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


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


557 
\begin{ttbox}


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


559 
{\out Level 0}


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


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


562 
\ttbreak


563 
by (resolve_tac [exCI] 1);


564 
{\out Level 1}


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


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


567 
\end{ttbox}


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


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


570 
steps routinely break down the conclusion and assumption.


571 
\begin{ttbox}


572 
by (resolve_tac [allI] 1);


573 
{\out Level 2}


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


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


576 
\ttbreak


577 
by (resolve_tac [impI] 1);


578 
{\out Level 3}


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


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


581 
\ttbreak


582 
by (eresolve_tac [allE] 1);


583 
{\out Level 4}


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


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


586 
\end{ttbox}


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


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


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


590 
I)$ using \ttindex{swap_res_tac}.


591 
\begin{ttbox}


592 
allI RSN (2,swap);


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


594 
by (eresolve_tac [it] 1);


595 
{\out Level 5}


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


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


598 
\end{ttbox}


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


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


601 
\begin{ttbox}


602 
by (resolve_tac [impI] 1);


603 
{\out Level 6}


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


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


606 
\end{ttbox}


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


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


609 
the unknown~{\tt?a}.


610 
\begin{ttbox}


611 
by (eresolve_tac [notE] 1);


612 
{\out Level 7}


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


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


615 
\ttbreak


616 
by (assume_tac 1);


617 
{\out Level 8}


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


619 
{\out No subgoals!}


620 
\end{ttbox}


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


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


623 
\begin{ttbox}


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


625 
{\out Level 0}


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


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


628 
by (best_tac FOL_dup_cs 1);


629 
{\out Level 1}


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


631 
{\out No subgoals!}


632 
\end{ttbox}


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


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


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


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


637 


638 


639 
\section{Derived rules and the classical tactics}


640 
Classical firstorder logic can be extended with the propositional


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


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


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


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


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


646 
formula. Introducing further abbreviations makes the problem worse.


647 


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


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


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


651 
suggests that the


652 
$if$introduction rule should be

157

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

104

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


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


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


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


658 
\]


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


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


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


662 
equation~$(if)$.


663 
\begin{ttbox}


664 
If = FOL +


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


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


667 
end


668 
\end{ttbox}


669 
The derivations of the introduction and elimination rules demonstrate the


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


671 
so we use \ttindex{fast_tac}.


672 


673 


674 
\subsection{Deriving the introduction rule}


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


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


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


678 
of $if$ in the subgoal.


679 
\begin{ttbox}


680 
val prems = goalw If.thy [if_def]


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


682 
{\out Level 0}


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


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


685 
\end{ttbox}


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


687 
introduction rules to \ttindex{fast_tac}:


688 
\begin{ttbox}


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


690 
{\out Level 1}


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


692 
{\out No subgoals!}


693 
val ifI = result();


694 
\end{ttbox}


695 


696 


697 
\subsection{Deriving the elimination rule}


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


699 
The conclusion is simply $S$.


700 
\begin{ttbox}


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


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


703 
{\out Level 0}


704 
{\out S}


705 
{\out 1. S}


706 
\end{ttbox}


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


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


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


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


711 
\begin{ttbox}


712 
by (cut_facts_tac [major] 1);


713 
{\out Level 1}


714 
{\out S}


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


716 
\ttbreak


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


718 
{\out Level 2}


719 
{\out S}


720 
{\out No subgoals!}


721 
val ifE = result();


722 
\end{ttbox}


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


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


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


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


727 
to expand definitions in the subgoals  perhaps after calling


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


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


730 
definitions in the premises directly.


731 


732 


733 
\subsection{Using the derived rules}


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


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


736 
following:


737 
\begin{eqnarray*}

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$


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


743 


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


745 
\begin{ttbox}


746 
goal If.thy


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


748 
{\out Level 0}


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


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


751 
\ttbreak


752 
by (resolve_tac [iffI] 1);


753 
{\out Level 1}


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


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


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


757 
\end{ttbox}


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


759 
\begin{ttbox}


760 
by (eresolve_tac [ifE] 1);


761 
{\out Level 2}


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


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


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


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


766 
\ttbreak


767 
by (eresolve_tac [ifE] 1);


768 
{\out Level 3}


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


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


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


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


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


774 
\end{ttbox}


775 


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


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


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


779 
\begin{ttbox}


780 
by (resolve_tac [ifI] 1);


781 
{\out Level 4}


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


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


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


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


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


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


788 
\ttbreak


789 
by (resolve_tac [ifI] 1);


790 
{\out Level 5}


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


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


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


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


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


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


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


798 
\end{ttbox}


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


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


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


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


803 
for~$if$.


804 
\begin{ttbox}


805 
choplev 0;


806 
{\out Level 0}


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


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


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


810 
by (fast_tac if_cs 1);


811 
{\out Level 1}


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


813 
{\out No subgoals!}


814 
\end{ttbox}


815 
This tactic also solves the other example.


816 
\begin{ttbox}


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


818 
{\out Level 0}


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


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


821 
\ttbreak


822 
by (fast_tac if_cs 1);


823 
{\out Level 1}


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


825 
{\out No subgoals!}


826 
\end{ttbox}


827 


828 


829 
\subsection{Derived rules versus definitions}


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


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


832 
us redo the previous proof:


833 
\begin{ttbox}


834 
choplev 0;


835 
{\out Level 0}


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


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


838 
\ttbreak


839 
by (rewrite_goals_tac [if_def]);


840 
{\out Level 1}


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


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


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


844 
\ttbreak


845 
by (fast_tac FOL_cs 1);


846 
{\out Level 2}


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


848 
{\out No subgoals!}


849 
\end{ttbox}


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


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


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


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


854 


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


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


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


858 


859 
Attempts at program verification often yield invalid assertions.


860 
Let us try to prove one:


861 
\begin{ttbox}


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


863 
{\out Level 0}


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


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


866 
by (fast_tac FOL_cs 1);


867 
{\out by: tactic failed}


868 
\end{ttbox}


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


870 
situation by applying \ttindex{step_tac}.


871 
\begin{ttbox}


872 
by (REPEAT (step_tac if_cs 1));


873 
{\out Level 1}


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


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


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


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


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


879 
\end{ttbox}


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


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


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


883 


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


885 
the rules of {\FOL}:


886 
\begin{ttbox}


887 
choplev 0;


888 
{\out Level 0}


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


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


891 
\ttbreak


892 
by (rewrite_goals_tac [if_def]);


893 
{\out Level 1}


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


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


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


897 
by (fast_tac FOL_cs 1);


898 
{\out by: tactic failed}


899 
\end{ttbox}


900 
Again we apply \ttindex{step_tac}:


901 
\begin{ttbox}


902 
by (REPEAT (step_tac FOL_cs 1));


903 
{\out Level 2}


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


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


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


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


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


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


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


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


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


913 
\end{ttbox}


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


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


916 


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


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