%!TEX root = logics-ZF.tex

 \chapter{First-Order Logic}

 \index{first-order logic|(}

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

   nk}.  Intuitionistic first-order logic is defined first, as theory

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

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

 provided.  The intuitionistic prover works with derived rules to simplify

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

 classical reasoner, which simulates a sequent calculus.

 \section{Syntax and rules of inference}

 The logic is many-sorted, using Isabelle's type classes.  The class of

 first-order terms is called \cldx{term} and is a subclass of \isa{logic}.

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

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

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

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

 are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which

 belongs to class~\cldx{logic}.  Figure~\ref{fol-syntax} gives the syntax.

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

 Figure~\ref{fol-rules} shows the inference rules with their names.

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

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

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

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

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

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

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

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

 Some intuitionistic derived rules are shown in

 Fig.\ts\ref{fol-int-derived}, again with their names.  These include

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

 deduction typically involves a combination of forward and backward

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

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

 rules badly, so sequent-style rules are derived to eliminate conjunctions,

 implications, and universal quantifiers.  Used with elim-resolution,

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

 re-inserts the quantified formula for later use.  The rules

 \isa{conj\_impE}, etc., support the intuitionistic proof procedure

 (see~\S\ref{fol-int-prover}).

 See the on-line theory library for complete listings of the rules and

 derived rules.

 \begin{figure} 

 \begin{center}

 \begin{tabular}{rrr} 

   \it name      &\it meta-type  & \it description \\ 

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

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

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

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

 \end{tabular}

 \end{center}

 \subcaption{Constants}

 \begin{center}

 \begin{tabular}{llrrr} 

   \it symbol &\it name     &\it meta-type & \it priority & \it description \\

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

         universal quantifier ($\forall$) \\

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

         existential quantifier ($\exists$) \\

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

         unique existence ($\exists!$)

 \end{tabular}

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

 \end{center}

 \subcaption{Binders} 

 \begin{center}

 \index{*"= symbol}

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

 \index{*"| symbol}

 \index{*"-"-"> symbol}

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

 \begin{tabular}{rrrr} 

   \it symbol    & \it meta-type         & \it priority & \it description \\ 

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

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

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

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

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

 \end{tabular}

 \end{center}

 \subcaption{Infixes}

 \dquotes

 \[\begin{array}{rcl}

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

          & | & term " = " term \quad| \quad term " \ttilde= " term \\

          & | & "\ttilde\ " formula \\

          & | & formula " \& " formula \\

          & | & formula " | " formula \\

          & | & formula " --> " formula \\

          & | & formula " <-> " formula \\

          & | & "ALL~" id~id^* " . " formula \\

          & | & "EX~~" id~id^* " . " formula \\

          & | & "EX!~" id~id^* " . " formula

   \end{array}

 \]

 \subcaption{Grammar}

 \caption{Syntax of \texttt{FOL}} \label{fol-syntax}

 \end{figure}

 \begin{figure} 

 \begin{ttbox}

 \tdx{refl}        a=a

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

 \subcaption{Equality rules}

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

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

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

 \tdx{disjI1}      P ==> P|Q

 \tdx{disjI2}      Q ==> P|Q

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

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

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

 \tdx{FalseE}      False ==> P

 \subcaption{Propositional rules}

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

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

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

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

 \subcaption{Quantifier rules}

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

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

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

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

 \subcaption{Definitions}

 \end{ttbox}

 \caption{Rules of intuitionistic logic} \label{fol-rules}

 \end{figure}

 \begin{figure} 

 \begin{ttbox}

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

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

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

 \subcaption{Derived equality rules}

 \tdx{TrueI}     True

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

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

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

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

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

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

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

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

           |] ==> R

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

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

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

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

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

 \subcaption{Sequent-style elimination rules}

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

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

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

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

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

              S ==> R |] ==> R

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

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

 \end{ttbox}

 \subcaption{Intuitionistic simplification of implication}

 \caption{Derived rules for intuitionistic logic} \label{fol-int-derived}

 \end{figure}

 \section{Generic packages}

 FOL instantiates most of Isabelle's generic packages.

 \begin{itemize}

 \item 

 It instantiates the simplifier, which is invoked through the method 

 \isa{simp}.  Both equality ($=$) and the biconditional

 ($\bimp$) may be used for rewriting.  

 \item 

 It instantiates the classical reasoner, which is invoked mainly through the 

 methods \isa{blast} and \isa{auto}.  See~\S\ref{fol-cla-prover}

 for details. 

 %

 %\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for

 %  an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's

 %  general substitution rule.

 \end{itemize}

 \begin{warn}\index{simplification!of conjunctions}%

   Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous.  The

   left part of a conjunction helps in simplifying the right part.  This effect

   is not available by default: it can be slow.  It can be obtained by

   including the theorem \isa{conj_cong}\index{*conj_cong (rule)}%

   as a congruence rule in

   simplification, \isa{simp cong:\ conj\_cong}.

 \end{warn}

 \section{Intuitionistic proof procedures} \label{fol-int-prover}

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

 difficulties for automated proof.  In intuitionistic logic, the assumption

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

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

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

 proof must be abandoned.  Thus intuitionistic propositional logic requires

 backtracking.  

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

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

 twice:

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

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

 \]

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

 Instead, it simplifies implications using derived rules

 (Fig.\ts\ref{fol-int-derived}).  It reduces the antecedents of implications

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

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

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

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

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

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

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

 has demonstrated their completeness for propositional

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

 for first-order logic because they discard universally quantified

 assumptions after a single use. These are \ML{} functions, and are listed

 below with their \ML{} type:

 \begin{ttbox} 

 mp_tac              : int -> tactic

 eq_mp_tac           : int -> tactic

 IntPr.safe_step_tac : int -> tactic

 IntPr.safe_tac      :        tactic

 IntPr.inst_step_tac : int -> tactic

 IntPr.step_tac      : int -> tactic

 IntPr.fast_tac      : int -> tactic

 IntPr.best_tac      : int -> tactic

 \end{ttbox}

 Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the

 tactics of Isabelle's classical reasoner.  There are no corresponding

 Isar methods, but you can use the 

 \isa{tactic} method to call \ML{} tactics in an Isar script:

 \begin{isabelle}

 \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})

 \end{isabelle}

 Here is a description of each tactic:

 \begin{ttdescription}

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

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

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

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

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

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

 produce multiple outcomes, enumerating all suitable pairs of assumptions.

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

 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it

 is safe.

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

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

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

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

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

 \item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},

 but allows unknowns to be instantiated.

 \item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt

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

   the intuitionistic proof procedure.

 \item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using

 depth-first search, to solve subgoal~$i$.

 \item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using

 best-first search (guided by the size of the proof state) to solve subgoal~$i$.

 \end{ttdescription}

 Here are some of the theorems that \texttt{IntPr.fast_tac} proves

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

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

 \begin{ttbox}

 ~~P & ~~(P --> Q) --> ~~Q

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

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

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

 \end{ttbox}

 \begin{figure} 

 \begin{ttbox}

 \tdx{excluded_middle}    ~P | P

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

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

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

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

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

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

 \end{ttbox}

 \caption{Derived rules for classical logic} \label{fol-cla-derived}

 \end{figure}

 \section{Classical proof procedures} \label{fol-cla-prover}

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

 the rule

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

 \noindent

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

 derives classical introduction rules for $\disj$ and~$\exists$, as well as

 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see

 Fig.\ts\ref{fol-cla-derived}).

 The classical reasoner is installed.  The most useful methods are

 \isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning

 combined with simplification), but the full range of

 methods is available, including \isa{clarify},

 \isa{fast}, \isa{best} and \isa{force}. 

  See the 

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

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

 and the \emph{Tutorial}~\cite{isa-tutorial}

 for more discussion of classical proof methods.

 \section{An intuitionistic example}

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

 \cite[pages~222--3]{paulson87}. It illustrates the treatment of

 quantifier reasoning, which is different in Isabelle than it is in

 {\sc lcf}-based theorem provers such as {\sc hol}.  

 The theory header specifies that we are working in intuitionistic

 logic by designating \isa{IFOL} rather than \isa{FOL} as the parent

 theory:

 \begin{isabelle}

 \isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline

 \isacommand{begin}

 \end{isabelle}

 The proof begins by entering the goal, then applying the rule $({\imp}I)$.

 \begin{isabelle}

 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline

 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\

 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))

 \isanewline

 \isacommand{apply}\ (rule\ impI)\isanewline

 \ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\

 \isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)

 \end{isabelle}

 Isabelle's output is shown as it would appear using Proof General.

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

 $({\imp}I)$ replaces~\isa{\isasymlongrightarrow}

 by~\isa{\isasymLongrightarrow}, so that

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

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

 \begin{isabelle}

 \isacommand{apply}\ (rule\ allI)\isanewline

 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\

 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\)

 \end{isabelle}

 Applying $({\forall}I)$ replaces the \isa{\isasymforall

 x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}

 (or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's 

 meta universal quantifier.  The bound variable is a {\bf parameter} of

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

 $({\exists}E)$.  What happens if the wrong rule is chosen?

 \begin{isabelle}

 \isacommand{apply}\ (rule\ exI)\isanewline

 \ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\

 \isasymLongrightarrow \ Q(x,\ ?y2(x))

 \end{isabelle}

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

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

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

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

 \begin{isabelle}

 \isacommand{apply}\ (erule\ exE)\isanewline

 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x))

 \end{isabelle}

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

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

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

 Using Proof General, we can return to the critical point, marked

 $(*)$ above.  This time we apply $({\exists}E)$:

 \begin{isabelle}

 \isacommand{apply}\ (erule\ exE)\isanewline

 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\

 \isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)

 \end{isabelle}

 We now have two parameters and no scheme variables.  Applying

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

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

 example demonstrates.

 \begin{isabelle}

 \isacommand{apply}\ (rule\ exI)\isanewline

 \ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\

 \isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))

 \isanewline

 \isacommand{apply}\ (erule\ allE)\isanewline

 \ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \

 Q(x,\ ?y3(x,\ y))

 \end{isabelle}

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

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

 x} and \isa{?y3(x,y)} with~\isa{y}.

 \begin{isabelle}

 \isacommand{apply}\ assumption\isanewline

 No\ subgoals!\isanewline

 \isacommand{done}

 \end{isabelle}

 The theorem was proved in six method invocations, not counting the

 abandoned ones.  But proof checking is tedious, and the \ML{} tactic

 \ttindex{IntPr.fast_tac} can prove the theorem in one step.

 \begin{isabelle}

 \isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline

 \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\

 \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))

 \isanewline

 \isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline

 No\ subgoals!

 \end{isabelle}

 \section{An example of intuitionistic negation}

 The following example demonstrates the specialized forms of implication

 elimination.  Even propositional formulae can be difficult to prove from

 the basic rules; the specialized rules help considerably.  

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

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

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

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

 \footnote{This remark holds only for propositional logic, not if $P$ is

   allowed to contain quantifiers.}

 %

 Proving $\neg\neg P$ intuitionistically is

 much harder than proving~$P$ classically.

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

 Q)\disj (Q\imp P)$.  The first step is apply the

 \isa{unfold} method, which expands

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

 and allows use of the special implication rules.

 \begin{isabelle}

 \isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline

 \ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))

 \isanewline

 \isacommand{apply}\ (unfold\ not\_def)\isanewline

 \ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%

 \end{isabelle}

 The next step is a trivial use of $(\imp I)$.

 \begin{isabelle}

 \isacommand{apply}\ (rule\ impI)\isanewline

 \ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%

 \end{isabelle}

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

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

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

 assumption into two assumptions, one for each disjunct.

 \begin{isabelle}

 \isacommand{apply}\ (erule\ disj\_impE)\isanewline

 \ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \

 False

 \end{isabelle}

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

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

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

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

 \begin{isabelle}

 \isacommand{apply}\ (erule\ imp\_impE)\isanewline

 \ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline

 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \

 False

 \end{isabelle}

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

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

 applying \tdx{imp_impE} is simpler.

 \begin{isabelle}

 \ \isacommand{apply}\ (erule\ imp\_impE)\isanewline

 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline

 \ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline

 \ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%

 \end{isabelle}

 The three subgoals are all trivial.

 \begin{isabelle}

 \isacommand{apply}\ assumption\ \isanewline

 \ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\

 False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline

 \ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\

 \isasymlongrightarrow \ False;\ False\isasymrbrakk \

 \isasymLongrightarrow \ False%

 \isanewline

 \isacommand{apply}\ (erule\ FalseE)+\isanewline

 No\ subgoals!\isanewline

 \isacommand{done}

 \end{isabelle}

 This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}.

 \section{A classical example} \label{fol-cla-example}

 To illustrate classical logic, we shall prove the theorem

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

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

 $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must

 work in a theory based on classical logic, the theory \isa{FOL}:

 \begin{isabelle}

 \isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline

 \isacommand{begin}

 \end{isabelle}

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

 above.  Its key step is its first rule, \tdx{exCI}, a classical

 version of~$(\exists I)$ that allows multiple instantiation of the

 quantifier.

 \begin{isabelle}

 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline

 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)

 \isanewline

 \isacommand{apply}\ (rule\ exCI)\isanewline

 \ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x)

 \end{isabelle}

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

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

 steps are routine.

 \begin{isabelle}

 \isacommand{apply}\ (rule\ allI)\isanewline

 \ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x)

 \isanewline

 \isacommand{apply}\ (rule\ impI)\isanewline

 \ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x)

 \end{isabelle}

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

 is equivalent to applying~$(\exists I)$ again.

 \begin{isabelle}

 \isacommand{apply}\ (erule\ allE)\isanewline

 \ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x)

 \end{isabelle}

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

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

 using \ttindex{erule}.

 \begin{isabelle}

 \isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline

 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa)

 \end{isabelle}

 The operand of \isa{erule} above denotes the following theorem:

 \begin{isabelle}

 \ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\

 \isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \

 ?P1(x)\isasymrbrakk \

 \isasymLongrightarrow \ ?P%

 \end{isabelle}

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

 \begin{isabelle}

 \isacommand{apply}\ (rule\ impI)\isanewline

 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa)

 \end{isabelle}

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

 \index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}

 and~\isa{P(?y3(x))}.   The proof never instantiates the

 unknown~\isa{?a}.

 \begin{isabelle}

 \isacommand{apply}\ (erule\ notE)\isanewline

 \ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x)

 \isanewline

 \isacommand{apply}\ assumption\isanewline

 No\ subgoals!\isanewline

 \isacommand{done}

 \end{isabelle}

 The civilised way to prove this theorem is using the

 \methdx{blast} method, which automatically uses the classical form

 of the rule~$(\exists I)$:

 \begin{isabelle}

 \isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline

 \ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)

 \isanewline

 \isacommand{by}\ blast\isanewline

 No\ subgoals!

 \end{isabelle}

 If this theorem seems counterintuitive, then perhaps you are an

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

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

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

 \section{Derived rules and the classical tactics}

 Classical first-order logic can be extended with the propositional

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

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

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

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

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

 formula.  Introducing further abbreviations makes the problem worse.

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

 directly, without reference to its definition.  The simple identity

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

 suggests that the

 $if$-introduction rule should be

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

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

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

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

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

 \]

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

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

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

 equation~$(if)$.

 \begin{isabelle}

 \isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline

 \isacommand{begin}\isanewline

 \isacommand{constdefs}\isanewline

 \ \ if\ ::\ "[o,o,o]=>o"\isanewline

 \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"

 \end{isabelle}

 We create the file \texttt{If.thy} containing these declarations.  (This file

 is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing

 \begin{isabelle}

 use_thy "If";  

 \end{isabelle}

 loads that theory and sets it to be the current context.

 \subsection{Deriving the introduction rule}

 The derivations of the introduction and elimination rules demonstrate the

 methods for rewriting with definitions.  Classical reasoning is required,

 so we use \isa{blast}.

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

 concludes $if(P,Q,R)$.  We propose this lemma and immediately simplify

 using \isa{if\_def} to expand the definition of \isa{if} in the

 subgoal.

 \begin{isabelle}

 \isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\

 |]\ ==>\ if(P,Q,R)"\isanewline

 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R)

 \isanewline

 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline

 \ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \

 R

 \end{isabelle}

 The rule's premises, although expressed using meta-level implication

 (\isa{\isasymLongrightarrow}) are passed as ordinary implications to

 \methdx{blast}.  

 \begin{isabelle}

 \isacommand{apply}\ blast\isanewline

 No\ subgoals!\isanewline

 \isacommand{done}

 \end{isabelle}

 \subsection{Deriving the elimination rule}

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

 The conclusion is simply $S$.

 \begin{isabelle}

 \isacommand{lemma}\ ifE:\isanewline

 \ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline

 \ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%

 \isanewline

 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline

 \ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%

 \end{isabelle}

 The proof script is the same as before: \isa{simp} followed by

 \isa{blast}:

 \begin{isabelle}

 \isacommand{apply}\ blast\isanewline

 No\ subgoals!\isanewline

 \isacommand{done}

 \end{isabelle}

 \subsection{Using the derived rules}

 Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural

 proofs of theorems such as the following:

 \begin{eqnarray*}

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

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

 \end{eqnarray*}

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

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

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

 \begin{isabelle}

 \isacommand{lemma}\ if\_commute:\isanewline

 \ \ \ \ \ "if(P,\ if(Q,A,B),\

 if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline

 \isacommand{apply}\ (rule\ iffI)\isanewline

 \ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))

 \end{isabelle}

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

 \begin{isabelle}

 \isacommand{apply}\ (erule\ ifE)\isanewline

 \ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))

 \isanewline

 \isacommand{apply}\ (erule\ ifE)\isanewline

 \ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))

 \end{isabelle}

 %

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

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

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

 \begin{isabelle}

 \isacommand{apply}\ (rule\ ifI)\isanewline

 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline

 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline

 \ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))

 \isanewline

 \isacommand{apply}\ (rule\ ifI)\isanewline

 \ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline

 \ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline

 \ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline

 \ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline

 \ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline

 \isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))

 \end{isabelle}

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

 third, by contradiction.  This is getting tedious.  We could use the classical

 reasoner, but first let us extend the default claset with the derived rules

 for~$if$.

 \begin{isabelle}

 \isacommand{declare}\ ifI\ [intro!]\isanewline

 \isacommand{declare}\ ifE\ [elim!]

 \end{isabelle}

 With these declarations, we could have proved this theorem with a single

 call to \isa{blast}.  Here is another example:

 \begin{isabelle}

 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline

 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))

 \isanewline

 \isacommand{by}\ blast

 \end{isabelle}

 \subsection{Derived rules versus definitions}

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

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

 us redo the previous proof:

 \begin{isabelle}

 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline

 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B))

 \end{isabelle}

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

 \begin{isabelle}

 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline

 \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline

 \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B)

 \end{isabelle}

 We are left with a subgoal in pure first-order logic, and it falls to

 \isa{blast}:

 \begin{isabelle}

 \isacommand{apply}\ blast\isanewline

 No\ subgoals!

 \end{isabelle}

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

 approach has its merits, but it can be slow.  In these examples, proofs

 using the derived rules for~\isa{if} run about six

 times faster  than proofs using just the rules of first-order logic.

 Expanding definitions can also make it harder to diagnose errors. 

 Suppose we are having difficulties in proving some goal.  If by expanding

 definitions we have made it unreadable, then we have little hope of

 diagnosing the problem.

 Attempts at program verification often yield invalid assertions.

 Let us try to prove one:

 \begin{isabelle}

 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline

 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\

 A))

 \end{isabelle}

 Calling \isa{blast} yields an uninformative failure message. We can

 get a closer look at the situation by applying \methdx{auto}.

 \begin{isabelle}

 \isacommand{apply}\ auto\isanewline

 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline

 \ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline

 \ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline

 \ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \

 False

 \end{isabelle}

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

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

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

 We can repeat this analysis by expanding definitions, using just the rules of

 first-order logic:

 \begin{isabelle}

 \isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline

 \ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\

 A))

 \isanewline

 \isacommand{apply}\ (simp\ add:\ if\_def)\isanewline

 \ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline

 \isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A)

 \end{isabelle}

 Again \isa{blast} would fail, so we try \methdx{auto}:

 \begin{isabelle}

 \isacommand{apply}\ (auto)\ \isanewline

 \ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline

 \ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline

 \ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline

 \ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline

 \ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline

 \ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline

 \ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline

 \ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%

 \end{isabelle}

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

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

 Expanding your definitions usually makes proofs more difficult.  This is

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

 \index{first-order logic|)}