doc-src/ZF/FOL.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 8249 3fc32155372c
child 14154 3bc0128e2c74
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
     1 %% $Id$
     2 \chapter{First-Order Logic}
     3 \index{first-order logic|(}
     4 
     5 Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
     6   nk}.  Intuitionistic first-order logic is defined first, as theory
     7 \thydx{IFOL}.  Classical logic, theory \thydx{FOL}, is
     8 obtained by adding the double negation rule.  Basic proof procedures are
     9 provided.  The intuitionistic prover works with derived rules to simplify
    10 implications in the assumptions.  Classical~\texttt{FOL} employs Isabelle's
    11 classical reasoner, which simulates a sequent calculus.
    12 
    13 \section{Syntax and rules of inference}
    14 The logic is many-sorted, using Isabelle's type classes.  The class of
    15 first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
    16 No types of individuals are provided, but extensions can define types such
    17 as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
    18 (see the examples directory, \texttt{FOL/ex}).  Below, the type variable
    19 $\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
    20 are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
    21 belongs to class~\cldx{logic}.  Figure~\ref{fol-syntax} gives the syntax.
    22 Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
    23 
    24 Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
    25 Negation is defined in the usual way for intuitionistic logic; $\neg P$
    26 abbreviates $P\imp\bot$.  The biconditional~($\bimp$) is defined through
    27 $\conj$ and~$\imp$; introduction and elimination rules are derived for it.
    28 
    29 The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
    30 of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
    31 quantifications.  For instance, $\exists!x\;y.P(x,y)$ abbreviates
    32 $\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
    33 exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
    34 
    35 Some intuitionistic derived rules are shown in
    36 Fig.\ts\ref{fol-int-derived}, again with their \ML\ names.  These include
    37 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
    38 deduction typically involves a combination of forward and backward
    39 reasoning, particularly with the destruction rules $(\conj E)$,
    40 $({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
    41 rules badly, so sequent-style rules are derived to eliminate conjunctions,
    42 implications, and universal quantifiers.  Used with elim-resolution,
    43 \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
    44 re-inserts the quantified formula for later use.  The rules {\tt
    45 conj_impE}, etc., support the intuitionistic proof procedure
    46 (see~\S\ref{fol-int-prover}).
    47 
    48 See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
    49 \texttt{FOL/intprover.ML} for complete listings of the rules and
    50 derived rules.
    51 
    52 \begin{figure} 
    53 \begin{center}
    54 \begin{tabular}{rrr} 
    55   \it name      &\it meta-type  & \it description \\ 
    56   \cdx{Trueprop}& $o\To prop$           & coercion to $prop$\\
    57   \cdx{Not}     & $o\To o$              & negation ($\neg$) \\
    58   \cdx{True}    & $o$                   & tautology ($\top$) \\
    59   \cdx{False}   & $o$                   & absurdity ($\bot$)
    60 \end{tabular}
    61 \end{center}
    62 \subcaption{Constants}
    63 
    64 \begin{center}
    65 \begin{tabular}{llrrr} 
    66   \it symbol &\it name     &\it meta-type & \it priority & \it description \\
    67   \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 & 
    68         universal quantifier ($\forall$) \\
    69   \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
    70         existential quantifier ($\exists$) \\
    71   \texttt{EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 & 
    72         unique existence ($\exists!$)
    73 \end{tabular}
    74 \index{*"E"X"! symbol}
    75 \end{center}
    76 \subcaption{Binders} 
    77 
    78 \begin{center}
    79 \index{*"= symbol}
    80 \index{&@{\tt\&} symbol}
    81 \index{*"| symbol}
    82 \index{*"-"-"> symbol}
    83 \index{*"<"-"> symbol}
    84 \begin{tabular}{rrrr} 
    85   \it symbol    & \it meta-type         & \it priority & \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$) 
    91 \end{tabular}
    92 \end{center}
    93 \subcaption{Infixes}
    94 
    95 \dquotes
    96 \[\begin{array}{rcl}
    97  formula & = & \hbox{expression of type~$o$} \\
    98          & | & term " = " term \quad| \quad term " \ttilde= " term \\
    99          & | & "\ttilde\ " formula \\
   100          & | & formula " \& " formula \\
   101          & | & formula " | " formula \\
   102          & | & formula " --> " formula \\
   103          & | & formula " <-> " formula \\
   104          & | & "ALL~" id~id^* " . " formula \\
   105          & | & "EX~~" id~id^* " . " formula \\
   106          & | & "EX!~" id~id^* " . " formula
   107   \end{array}
   108 \]
   109 \subcaption{Grammar}
   110 \caption{Syntax of \texttt{FOL}} \label{fol-syntax}
   111 \end{figure}
   112 
   113 
   114 \begin{figure} 
   115 \begin{ttbox}
   116 \tdx{refl}        a=a
   117 \tdx{subst}       [| a=b;  P(a) |] ==> P(b)
   118 \subcaption{Equality rules}
   119 
   120 \tdx{conjI}       [| P;  Q |] ==> P&Q
   121 \tdx{conjunct1}   P&Q ==> P
   122 \tdx{conjunct2}   P&Q ==> Q
   123 
   124 \tdx{disjI1}      P ==> P|Q
   125 \tdx{disjI2}      Q ==> P|Q
   126 \tdx{disjE}       [| P|Q;  P ==> R;  Q ==> R |] ==> R
   127 
   128 \tdx{impI}        (P ==> Q) ==> P-->Q
   129 \tdx{mp}          [| P-->Q;  P |] ==> Q
   130 
   131 \tdx{FalseE}      False ==> P
   132 \subcaption{Propositional rules}
   133 
   134 \tdx{allI}        (!!x. P(x))  ==> (ALL x.P(x))
   135 \tdx{spec}        (ALL x.P(x)) ==> P(x)
   136 
   137 \tdx{exI}         P(x) ==> (EX x.P(x))
   138 \tdx{exE}         [| EX x.P(x);  !!x. P(x) ==> R |] ==> R
   139 \subcaption{Quantifier rules}
   140 
   141 \tdx{True_def}    True        == False-->False
   142 \tdx{not_def}     ~P          == P-->False
   143 \tdx{iff_def}     P<->Q       == (P-->Q) & (Q-->P)
   144 \tdx{ex1_def}     EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
   145 \subcaption{Definitions}
   146 \end{ttbox}
   147 
   148 \caption{Rules of intuitionistic logic} \label{fol-rules}
   149 \end{figure}
   150 
   151 
   152 \begin{figure} 
   153 \begin{ttbox}
   154 \tdx{sym}       a=b ==> b=a
   155 \tdx{trans}     [| a=b;  b=c |] ==> a=c
   156 \tdx{ssubst}    [| b=a;  P(a) |] ==> P(b)
   157 \subcaption{Derived equality rules}
   158 
   159 \tdx{TrueI}     True
   160 
   161 \tdx{notI}      (P ==> False) ==> ~P
   162 \tdx{notE}      [| ~P;  P |] ==> R
   163 
   164 \tdx{iffI}      [| P ==> Q;  Q ==> P |] ==> P<->Q
   165 \tdx{iffE}      [| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R
   166 \tdx{iffD1}     [| P <-> Q;  P |] ==> Q            
   167 \tdx{iffD2}     [| P <-> Q;  Q |] ==> P
   168 
   169 \tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |]  ==>  EX! x. P(x)
   170 \tdx{ex1E}      [| EX! x.P(x);  !!x.[| P(x);  ALL y. P(y) --> y=x |] ==> R 
   171           |] ==> R
   172 \subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)}
   173 
   174 \tdx{conjE}     [| P&Q;  [| P; Q |] ==> R |] ==> R
   175 \tdx{impE}      [| P-->Q;  P;  Q ==> R |] ==> R
   176 \tdx{allE}      [| ALL x.P(x);  P(x) ==> R |] ==> R
   177 \tdx{all_dupE}  [| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R |] ==> R
   178 \subcaption{Sequent-style elimination rules}
   179 
   180 \tdx{conj_impE} [| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R
   181 \tdx{disj_impE} [| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R
   182 \tdx{imp_impE}  [| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R
   183 \tdx{not_impE}  [| ~P --> S;  P ==> False;  S ==> R |] ==> R
   184 \tdx{iff_impE}  [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
   185              S ==> R |] ==> R
   186 \tdx{all_impE}  [| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R
   187 \tdx{ex_impE}   [| (EX x.P(x))-->S;  P(a)-->S ==> R |] ==> R
   188 \end{ttbox}
   189 \subcaption{Intuitionistic simplification of implication}
   190 \caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
   191 \end{figure}
   192 
   193 
   194 \section{Generic packages}
   195 FOL instantiates most of Isabelle's generic packages.
   196 \begin{itemize}
   197 \item 
   198 It instantiates the simplifier.  Both equality ($=$) and the biconditional
   199 ($\bimp$) may be used for rewriting.  Tactics such as \texttt{Asm_simp_tac} and
   200 \texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
   201 most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},
   202 for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
   203 for classical logic.  See the file
   204 \texttt{FOL/simpdata.ML} for a complete listing of the simplification
   205 rules%
   206 \iflabelundefined{sec:setting-up-simp}{}%
   207         {, and \S\ref{sec:setting-up-simp} for discussion}.
   208 
   209 \item 
   210 It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
   211 for details. 
   212 
   213 \item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
   214   an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's
   215   general substitution rule.
   216 \end{itemize}
   217 
   218 \begin{warn}\index{simplification!of conjunctions}%
   219   Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
   220   left part of a conjunction helps in simplifying the right part.  This effect
   221   is not available by default: it can be slow.  It can be obtained by
   222   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
   223 \end{warn}
   224 
   225 
   226 \section{Intuitionistic proof procedures} \label{fol-int-prover}
   227 Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
   228 difficulties for automated proof.  In intuitionistic logic, the assumption
   229 $P\imp Q$ cannot be treated like $\neg P\disj Q$.  Given $P\imp Q$, we may
   230 use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
   231 use of $P\imp Q$.  If the proof of~$P$ fails then the whole branch of the
   232 proof must be abandoned.  Thus intuitionistic propositional logic requires
   233 backtracking.  
   234 
   235 For an elementary example, consider the intuitionistic proof of $Q$ from
   236 $P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is needed
   237 twice:
   238 \[ \infer[({\imp}E)]{Q}{P\imp Q &
   239        \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} 
   240 \]
   241 The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
   242 Instead, it simplifies implications using derived rules
   243 (Fig.\ts\ref{fol-int-derived}).  It reduces the antecedents of implications
   244 to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
   245 The rules \tdx{conj_impE} and \tdx{disj_impE} are 
   246 straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
   247 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
   248 S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires
   249 backtracking.  All the rules are derived in the same simple manner.
   250 
   251 Dyckhoff has independently discovered similar rules, and (more importantly)
   252 has demonstrated their completeness for propositional
   253 logic~\cite{dyckhoff}.  However, the tactics given below are not complete
   254 for first-order logic because they discard universally quantified
   255 assumptions after a single use.
   256 \begin{ttbox} 
   257 mp_tac              : int -> tactic
   258 eq_mp_tac           : int -> tactic
   259 IntPr.safe_step_tac : int -> tactic
   260 IntPr.safe_tac      :        tactic
   261 IntPr.inst_step_tac : int -> tactic
   262 IntPr.step_tac      : int -> tactic
   263 IntPr.fast_tac      : int -> tactic
   264 IntPr.best_tac      : int -> tactic
   265 \end{ttbox}
   266 Most of these belong to the structure \texttt{IntPr} and resemble the
   267 tactics of Isabelle's classical reasoner.
   268 
   269 \begin{ttdescription}
   270 \item[\ttindexbold{mp_tac} {\it i}] 
   271 attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
   272 subgoal $i$.  For each assumption of the form $\neg P$ or $P\imp Q$, it
   273 searches for another assumption unifiable with~$P$.  By
   274 contradiction with $\neg P$ it can solve the subgoal completely; by Modus
   275 Ponens it can replace the assumption $P\imp Q$ by $Q$.  The tactic can
   276 produce multiple outcomes, enumerating all suitable pairs of assumptions.
   277 
   278 \item[\ttindexbold{eq_mp_tac} {\it i}] 
   279 is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
   280 is safe.
   281 
   282 \item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
   283 subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
   284 care not to instantiate unknowns), or \texttt{hyp_subst_tac}. 
   285 
   286 \item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all 
   287 subgoals.  It is deterministic, with at most one outcome.
   288 
   289 \item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
   290 but allows unknowns to be instantiated.
   291 
   292 \item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
   293     inst_step_tac}, or applies an unsafe rule.  This is the basic step of
   294   the intuitionistic proof procedure.
   295 
   296 \item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
   297 depth-first search, to solve subgoal~$i$.
   298 
   299 \item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
   300 best-first search (guided by the size of the proof state) to solve subgoal~$i$.
   301 \end{ttdescription}
   302 Here are some of the theorems that \texttt{IntPr.fast_tac} proves
   303 automatically.  The latter three date from {\it Principia Mathematica}
   304 (*11.53, *11.55, *11.61)~\cite{principia}.
   305 \begin{ttbox}
   306 ~~P & ~~(P --> Q) --> ~~Q
   307 (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
   308 (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
   309 (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
   310 \end{ttbox}
   311 
   312 
   313 
   314 \begin{figure} 
   315 \begin{ttbox}
   316 \tdx{excluded_middle}    ~P | P
   317 
   318 \tdx{disjCI}    (~Q ==> P) ==> P|Q
   319 \tdx{exCI}      (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
   320 \tdx{impCE}     [| P-->Q; ~P ==> R; Q ==> R |] ==> R
   321 \tdx{iffCE}     [| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
   322 \tdx{notnotD}   ~~P ==> P
   323 \tdx{swap}      ~P ==> (~Q ==> P) ==> Q
   324 \end{ttbox}
   325 \caption{Derived rules for classical logic} \label{fol-cla-derived}
   326 \end{figure}
   327 
   328 
   329 \section{Classical proof procedures} \label{fol-cla-prover}
   330 The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
   331 the rule
   332 $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
   333 \noindent
   334 Natural deduction in classical logic is not really all that natural.  FOL
   335 derives classical introduction rules for $\disj$ and~$\exists$, as well as
   336 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
   337 Fig.\ts\ref{fol-cla-derived}).
   338 
   339 The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
   340 Best_tac} refer to the default claset (\texttt{claset()}), which works for most
   341 purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
   342 propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
   343 rules.  See the file \texttt{FOL/cladata.ML} for lists of the
   344 classical rules, and 
   345 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
   346         {Chap.\ts\ref{chap:classical}} 
   347 for more discussion of classical proof methods.
   348 
   349 
   350 \section{An intuitionistic example}
   351 Here is a session similar to one in {\em Logic and Computation}
   352 \cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
   353 from {\sc lcf}-based theorem provers such as {\sc hol}.  
   354 
   355 First, we specify that we are working in intuitionistic logic:
   356 \begin{ttbox}
   357 context IFOL.thy;
   358 \end{ttbox}
   359 The proof begins by entering the goal, then applying the rule $({\imp}I)$.
   360 \begin{ttbox}
   361 Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   362 {\out Level 0}
   363 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   364 {\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   365 \ttbreak
   366 by (resolve_tac [impI] 1);
   367 {\out Level 1}
   368 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   369 {\out  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
   370 \end{ttbox}
   371 In this example, we shall never have more than one subgoal.  Applying
   372 $({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
   373 \(\ex{y}\all{x}Q(x,y)\) an assumption.  We have the choice of
   374 $({\exists}E)$ and $({\forall}I)$; let us try the latter.
   375 \begin{ttbox}
   376 by (resolve_tac [allI] 1);
   377 {\out Level 2}
   378 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   379 {\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   380 \end{ttbox}
   381 Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
   382 changing the universal quantifier from object~($\forall$) to
   383 meta~($\Forall$).  The bound variable is a {\bf parameter} of the
   384 subgoal.  We now must choose between $({\exists}I)$ and $({\exists}E)$.  What
   385 happens if the wrong rule is chosen?
   386 \begin{ttbox}
   387 by (resolve_tac [exI] 1);
   388 {\out Level 3}
   389 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   390 {\out  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
   391 \end{ttbox}
   392 The new subgoal~1 contains the function variable {\tt?y2}.  Instantiating
   393 {\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
   394 though~\texttt{x} is a bound variable.  Now we analyse the assumption
   395 \(\exists y.\forall x. Q(x,y)\) using elimination rules:
   396 \begin{ttbox}
   397 by (eresolve_tac [exE] 1);
   398 {\out Level 4}
   399 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   400 {\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
   401 \end{ttbox}
   402 Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
   403 existential quantifier from the assumption.  But the subgoal is unprovable:
   404 there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
   405 Using \texttt{choplev} we can return to the critical point.  This time we
   406 apply $({\exists}E)$:
   407 \begin{ttbox}
   408 choplev 2;
   409 {\out Level 2}
   410 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   411 {\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   412 \ttbreak
   413 by (eresolve_tac [exE] 1);
   414 {\out Level 3}
   415 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   416 {\out  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
   417 \end{ttbox}
   418 We now have two parameters and no scheme variables.  Applying
   419 $({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
   420 applied to those parameters.  Parameters should be produced early, as this
   421 example demonstrates.
   422 \begin{ttbox}
   423 by (resolve_tac [exI] 1);
   424 {\out Level 4}
   425 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   426 {\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
   427 \ttbreak
   428 by (eresolve_tac [allE] 1);
   429 {\out Level 5}
   430 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   431 {\out  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
   432 \end{ttbox}
   433 The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
   434 parameters.  The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
   435 x} and \verb|?y3(x,y)| with~\texttt{y}.
   436 \begin{ttbox}
   437 by (assume_tac 1);
   438 {\out Level 6}
   439 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   440 {\out No subgoals!}
   441 \end{ttbox}
   442 The theorem was proved in six tactic steps, not counting the abandoned
   443 ones.  But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
   444 theorem in one step.
   445 \begin{ttbox}
   446 Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   447 {\out Level 0}
   448 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   449 {\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   450 by (IntPr.fast_tac 1);
   451 {\out Level 1}
   452 {\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
   453 {\out No subgoals!}
   454 \end{ttbox}
   455 
   456 
   457 \section{An example of intuitionistic negation}
   458 The following example demonstrates the specialized forms of implication
   459 elimination.  Even propositional formulae can be difficult to prove from
   460 the basic rules; the specialized rules help considerably.  
   461 
   462 Propositional examples are easy to invent.  As Dummett notes~\cite[page
   463 28]{dummett}, $\neg P$ is classically provable if and only if it is
   464 intuitionistically provable;  therefore, $P$ is classically provable if and
   465 only if $\neg\neg P$ is intuitionistically provable.%
   466 \footnote{Of course this holds only for propositional logic, not if $P$ is
   467   allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
   468 much harder than proving~$P$ classically.
   469 
   470 Our example is the double negation of the classical tautology $(P\imp
   471 Q)\disj (Q\imp P)$.  When stating the goal, we command Isabelle to expand
   472 negations to implications using the definition $\neg P\equiv P\imp\bot$.
   473 This allows use of the special implication rules.
   474 \begin{ttbox}
   475 Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
   476 {\out Level 0}
   477 {\out ~ ~ ((P --> Q) | (Q --> P))}
   478 {\out  1. ((P --> Q) | (Q --> P) --> False) --> False}
   479 \end{ttbox}
   480 The first step is trivial.
   481 \begin{ttbox}
   482 by (resolve_tac [impI] 1);
   483 {\out Level 1}
   484 {\out ~ ~ ((P --> Q) | (Q --> P))}
   485 {\out  1. (P --> Q) | (Q --> P) --> False ==> False}
   486 \end{ttbox}
   487 By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
   488 that formula is not a theorem of intuitionistic logic.  Instead we apply
   489 the specialized implication rule \tdx{disj_impE}.  It splits the
   490 assumption into two assumptions, one for each disjunct.
   491 \begin{ttbox}
   492 by (eresolve_tac [disj_impE] 1);
   493 {\out Level 2}
   494 {\out ~ ~ ((P --> Q) | (Q --> P))}
   495 {\out  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
   496 \end{ttbox}
   497 We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
   498 their negations are inconsistent.  Applying \tdx{imp_impE} breaks down
   499 the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
   500 assumptions~$P$ and~$\neg Q$.
   501 \begin{ttbox}
   502 by (eresolve_tac [imp_impE] 1);
   503 {\out Level 3}
   504 {\out ~ ~ ((P --> Q) | (Q --> P))}
   505 {\out  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
   506 {\out  2. [| (Q --> P) --> False; False |] ==> False}
   507 \end{ttbox}
   508 Subgoal~2 holds trivially; let us ignore it and continue working on
   509 subgoal~1.  Thanks to the assumption~$P$, we could prove $Q\imp P$;
   510 applying \tdx{imp_impE} is simpler.
   511 \begin{ttbox}
   512 by (eresolve_tac [imp_impE] 1);
   513 {\out Level 4}
   514 {\out ~ ~ ((P --> Q) | (Q --> P))}
   515 {\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
   516 {\out  2. [| P; Q --> False; False |] ==> Q}
   517 {\out  3. [| (Q --> P) --> False; False |] ==> False}
   518 \end{ttbox}
   519 The three subgoals are all trivial.
   520 \begin{ttbox}
   521 by (REPEAT (eresolve_tac [FalseE] 2));
   522 {\out Level 5}
   523 {\out ~ ~ ((P --> Q) | (Q --> P))}
   524 {\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
   525 \ttbreak
   526 by (assume_tac 1);
   527 {\out Level 6}
   528 {\out ~ ~ ((P --> Q) | (Q --> P))}
   529 {\out No subgoals!}
   530 \end{ttbox}
   531 This proof is also trivial for \texttt{IntPr.fast_tac}.
   532 
   533 
   534 \section{A classical example} \label{fol-cla-example}
   535 To illustrate classical logic, we shall prove the theorem
   536 $\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
   537 follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
   538 $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we switch to
   539 classical logic:
   540 \begin{ttbox}
   541 context FOL.thy;
   542 \end{ttbox}
   543 
   544 The formal proof does not conform in any obvious way to the sketch given
   545 above.  The key inference is the first one, \tdx{exCI}; this classical
   546 version of~$(\exists I)$ allows multiple instantiation of the quantifier.
   547 \begin{ttbox}
   548 Goal "EX y. ALL x. P(y)-->P(x)";
   549 {\out Level 0}
   550 {\out EX y. ALL x. P(y) --> P(x)}
   551 {\out  1. EX y. ALL x. P(y) --> P(x)}
   552 \ttbreak
   553 by (resolve_tac [exCI] 1);
   554 {\out Level 1}
   555 {\out EX y. ALL x. P(y) --> P(x)}
   556 {\out  1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
   557 \end{ttbox}
   558 We can either exhibit a term {\tt?a} to satisfy the conclusion of
   559 subgoal~1, or produce a contradiction from the assumption.  The next
   560 steps are routine.
   561 \begin{ttbox}
   562 by (resolve_tac [allI] 1);
   563 {\out Level 2}
   564 {\out EX y. ALL x. P(y) --> P(x)}
   565 {\out  1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
   566 \ttbreak
   567 by (resolve_tac [impI] 1);
   568 {\out Level 3}
   569 {\out EX y. ALL x. P(y) --> P(x)}
   570 {\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
   571 \end{ttbox}
   572 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
   573 in effect applies~$(\exists I)$ again.
   574 \begin{ttbox}
   575 by (eresolve_tac [allE] 1);
   576 {\out Level 4}
   577 {\out EX y. ALL x. P(y) --> P(x)}
   578 {\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
   579 \end{ttbox}
   580 In classical logic, a negated assumption is equivalent to a conclusion.  To
   581 get this effect, we create a swapped version of $(\forall I)$ and apply it
   582 using \ttindex{eresolve_tac}; we could equivalently have applied $(\forall
   583 I)$ using \ttindex{swap_res_tac}.
   584 \begin{ttbox}
   585 allI RSN (2,swap);
   586 {\out val it = "[| ~(ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
   587 by (eresolve_tac [it] 1);
   588 {\out Level 5}
   589 {\out EX y. ALL x. P(y) --> P(x)}
   590 {\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
   591 \end{ttbox}
   592 The previous conclusion, \texttt{P(x)}, has become a negated assumption.
   593 \begin{ttbox}
   594 by (resolve_tac [impI] 1);
   595 {\out Level 6}
   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 subgoal has three assumptions.  We produce a contradiction between the
   600 \index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt
   601   P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.
   602 \begin{ttbox}
   603 by (eresolve_tac [notE] 1);
   604 {\out Level 7}
   605 {\out EX y. ALL x. P(y) --> P(x)}
   606 {\out  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
   607 \ttbreak
   608 by (assume_tac 1);
   609 {\out Level 8}
   610 {\out EX y. ALL x. P(y) --> P(x)}
   611 {\out No subgoals!}
   612 \end{ttbox}
   613 The civilised way to prove this theorem is through \ttindex{Blast_tac},
   614 which automatically uses the classical version of~$(\exists I)$:
   615 \begin{ttbox}
   616 Goal "EX y. ALL x. P(y)-->P(x)";
   617 {\out Level 0}
   618 {\out EX y. ALL x. P(y) --> P(x)}
   619 {\out  1. EX y. ALL x. P(y) --> P(x)}
   620 by (Blast_tac 1);
   621 {\out Depth = 0}
   622 {\out Depth = 1}
   623 {\out Depth = 2}
   624 {\out Level 1}
   625 {\out EX y. ALL x. P(y) --> P(x)}
   626 {\out No subgoals!}
   627 \end{ttbox}
   628 If this theorem seems counterintuitive, then perhaps you are an
   629 intuitionist.  In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
   630 requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
   631 which we cannot do without further knowledge about~$P$.
   632 
   633 
   634 \section{Derived rules and the classical tactics}
   635 Classical first-order logic can be extended with the propositional
   636 connective $if(P,Q,R)$, where 
   637 $$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$
   638 Theorems about $if$ can be proved by treating this as an abbreviation,
   639 replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals.  But
   640 this duplicates~$P$, causing an exponential blowup and an unreadable
   641 formula.  Introducing further abbreviations makes the problem worse.
   642 
   643 Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
   644 directly, without reference to its definition.  The simple identity
   645 \[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \]
   646 suggests that the
   647 $if$-introduction rule should be
   648 \[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]}  &  \infer*{R}{[\neg P]}} \]
   649 The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
   650 elimination rules for~$\disj$ and~$\conj$.
   651 \[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]}
   652                                   & \infer*{S}{[\neg P,R]}} 
   653 \]
   654 Having made these plans, we get down to work with Isabelle.  The theory of
   655 classical logic, \texttt{FOL}, is extended with the constant
   656 $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
   657 equation~$(if)$.
   658 \begin{ttbox}
   659 If = FOL +
   660 consts  if     :: [o,o,o]=>o
   661 rules   if_def "if(P,Q,R) == P&Q | ~P&R"
   662 end
   663 \end{ttbox}
   664 We create the file \texttt{If.thy} containing these declarations.  (This file
   665 is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing
   666 \begin{ttbox}
   667 use_thy "If";  
   668 \end{ttbox}
   669 loads that theory and sets it to be the current context.
   670 
   671 
   672 \subsection{Deriving the introduction rule}
   673 
   674 The derivations of the introduction and elimination rules demonstrate the
   675 methods for rewriting with definitions.  Classical reasoning is required,
   676 so we use \texttt{blast_tac}.
   677 
   678 The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
   679 concludes $if(P,Q,R)$.  We propose the conclusion as the main goal
   680 using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
   681 of $if$ in the subgoal.
   682 \begin{ttbox}
   683 val prems = Goalw [if_def]
   684     "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
   685 {\out Level 0}
   686 {\out if(P,Q,R)}
   687 {\out  1. P & Q | ~ P & R}
   688 \end{ttbox}
   689 The premises (bound to the {\ML} variable \texttt{prems}) are passed as
   690 introduction rules to \ttindex{blast_tac}.  Remember that \texttt{claset()} refers
   691 to the default classical set.
   692 \begin{ttbox}
   693 by (blast_tac (claset() addIs prems) 1);
   694 {\out Level 1}
   695 {\out if(P,Q,R)}
   696 {\out No subgoals!}
   697 qed "ifI";
   698 \end{ttbox}
   699 
   700 
   701 \subsection{Deriving the elimination rule}
   702 The elimination rule has three premises, two of which are themselves rules.
   703 The conclusion is simply $S$.
   704 \begin{ttbox}
   705 val major::prems = Goalw [if_def]
   706    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
   707 {\out Level 0}
   708 {\out S}
   709 {\out  1. S}
   710 \end{ttbox}
   711 The major premise contains an occurrence of~$if$, but the version returned
   712 by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
   713 definition expanded.  Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
   714 assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
   715 \begin{ttbox}
   716 by (cut_facts_tac [major] 1);
   717 {\out Level 1}
   718 {\out S}
   719 {\out  1. P & Q | ~ P & R ==> S}
   720 \ttbreak
   721 by (blast_tac (claset() addIs prems) 1);
   722 {\out Level 2}
   723 {\out S}
   724 {\out No subgoals!}
   725 qed "ifE";
   726 \end{ttbox}
   727 As you may recall from
   728 \iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
   729         {\S\ref{definitions}}, there are other
   730 ways of treating definitions when deriving a rule.  We can start the
   731 proof using \texttt{Goal}, which does not expand definitions, instead of
   732 \texttt{Goalw}.  We can use \ttindex{rew_tac}
   733 to expand definitions in the subgoals---perhaps after calling
   734 \ttindex{cut_facts_tac} to insert the rule's premises.  We can use
   735 \ttindex{rewrite_rule}, which is a meta-inference rule, to expand
   736 definitions in the premises directly.
   737 
   738 
   739 \subsection{Using the derived rules}
   740 The rules just derived have been saved with the {\ML} names \tdx{ifI}
   741 and~\tdx{ifE}.  They permit natural proofs of theorems such as the
   742 following:
   743 \begin{eqnarray*}
   744     if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
   745     if(if(P,Q,R), A, B)         & \bimp & if(P,if(Q,A,B),if(R,A,B))
   746 \end{eqnarray*}
   747 Proofs also require the classical reasoning rules and the $\bimp$
   748 introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}). 
   749 
   750 To display the $if$-rules in action, let us analyse a proof step by step.
   751 \begin{ttbox}
   752 Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   753 {\out Level 0}
   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 \ttbreak
   757 by (resolve_tac [iffI] 1);
   758 {\out Level 1}
   759 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   760 {\out  1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}
   761 {\out  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   762 \end{ttbox}
   763 The $if$-elimination rule can be applied twice in succession.
   764 \begin{ttbox}
   765 by (eresolve_tac [ifE] 1);
   766 {\out Level 2}
   767 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   768 {\out  1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   769 {\out  2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   770 {\out  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   771 \ttbreak
   772 by (eresolve_tac [ifE] 1);
   773 {\out Level 3}
   774 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   775 {\out  1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}
   776 {\out  2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   777 {\out  3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   778 {\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   779 \end{ttbox}
   780 %
   781 In the first two subgoals, all assumptions have been reduced to atoms.  Now
   782 $if$-introduction can be applied.  Observe how the $if$-rules break down
   783 occurrences of $if$ when they become the outermost connective.
   784 \begin{ttbox}
   785 by (resolve_tac [ifI] 1);
   786 {\out Level 4}
   787 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   788 {\out  1. [| P; Q; A; Q |] ==> if(P,A,C)}
   789 {\out  2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
   790 {\out  3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   791 {\out  4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   792 {\out  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   793 \ttbreak
   794 by (resolve_tac [ifI] 1);
   795 {\out Level 5}
   796 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   797 {\out  1. [| P; Q; A; Q; P |] ==> A}
   798 {\out  2. [| P; Q; A; Q; ~ P |] ==> C}
   799 {\out  3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
   800 {\out  4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
   801 {\out  5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
   802 {\out  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
   803 \end{ttbox}
   804 Where do we stand?  The first subgoal holds by assumption; the second and
   805 third, by contradiction.  This is getting tedious.  We could use the classical
   806 reasoner, but first let us extend the default claset with the derived rules
   807 for~$if$.
   808 \begin{ttbox}
   809 AddSIs [ifI];
   810 AddSEs [ifE];
   811 \end{ttbox}
   812 Now we can revert to the
   813 initial proof state and let \ttindex{blast_tac} solve it.  
   814 \begin{ttbox}
   815 choplev 0;
   816 {\out Level 0}
   817 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   818 {\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   819 by (Blast_tac 1);
   820 {\out Level 1}
   821 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
   822 {\out No subgoals!}
   823 \end{ttbox}
   824 This tactic also solves the other example.
   825 \begin{ttbox}
   826 Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
   827 {\out Level 0}
   828 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   829 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   830 \ttbreak
   831 by (Blast_tac 1);
   832 {\out Level 1}
   833 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   834 {\out No subgoals!}
   835 \end{ttbox}
   836 
   837 
   838 \subsection{Derived rules versus definitions}
   839 Dispensing with the derived rules, we can treat $if$ as an
   840 abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let
   841 us redo the previous proof:
   842 \begin{ttbox}
   843 choplev 0;
   844 {\out Level 0}
   845 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   846 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   847 \end{ttbox}
   848 This time, simply unfold using the definition of $if$:
   849 \begin{ttbox}
   850 by (rewtac if_def);
   851 {\out Level 1}
   852 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   853 {\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
   854 {\out     P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
   855 \end{ttbox}
   856 We are left with a subgoal in pure first-order logic, which is why the 
   857 classical reasoner can prove it given \texttt{FOL_cs} alone.  (We could, of 
   858 course, have used \texttt{Blast_tac}.)
   859 \begin{ttbox}
   860 by (blast_tac FOL_cs 1);
   861 {\out Level 2}
   862 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
   863 {\out No subgoals!}
   864 \end{ttbox}
   865 Expanding definitions reduces the extended logic to the base logic.  This
   866 approach has its merits --- especially if the prover for the base logic is
   867 good --- but can be slow.  In these examples, proofs using the default
   868 claset (which includes the derived rules) run about six times faster 
   869 than proofs using \texttt{FOL_cs}.
   870 
   871 Expanding definitions also complicates error diagnosis.  Suppose we are having
   872 difficulties in proving some goal.  If by expanding definitions we have
   873 made it unreadable, then we have little hope of diagnosing the problem.
   874 
   875 Attempts at program verification often yield invalid assertions.
   876 Let us try to prove one:
   877 \begin{ttbox}
   878 Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
   879 {\out Level 0}
   880 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   881 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   882 by (Blast_tac 1);
   883 {\out by: tactic failed}
   884 \end{ttbox}
   885 This failure message is uninformative, but we can get a closer look at the
   886 situation by applying \ttindex{Step_tac}.
   887 \begin{ttbox}
   888 by (REPEAT (Step_tac 1));
   889 {\out Level 1}
   890 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   891 {\out  1. [| A; ~ P; R; ~ P; R |] ==> B}
   892 {\out  2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
   893 {\out  3. [| ~ P; R; B; ~ P; R |] ==> A}
   894 {\out  4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
   895 \end{ttbox}
   896 Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
   897 while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
   898 $true\bimp false$, which is of course invalid.
   899 
   900 We can repeat this analysis by expanding definitions, using just the rules of
   901 FOL:
   902 \begin{ttbox}
   903 choplev 0;
   904 {\out Level 0}
   905 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   906 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   907 \ttbreak
   908 by (rewtac if_def);
   909 {\out Level 1}
   910 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   911 {\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
   912 {\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
   913 by (blast_tac FOL_cs 1);
   914 {\out by: tactic failed}
   915 \end{ttbox}
   916 Again we apply \ttindex{step_tac}:
   917 \begin{ttbox}
   918 by (REPEAT (step_tac FOL_cs 1));
   919 {\out Level 2}
   920 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
   921 {\out  1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
   922 {\out  2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
   923 {\out  3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
   924 {\out  4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
   925 {\out  5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
   926 {\out  6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
   927 {\out  7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
   928 {\out  8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
   929 \end{ttbox}
   930 Subgoal~1 yields the same countermodel as before.  But each proof step has
   931 taken six times as long, and the final result contains twice as many subgoals.
   932 
   933 Expanding definitions causes a great increase in complexity.  This is why
   934 the classical prover has been designed to accept derived rules.
   935 
   936 \index{first-order logic|)}