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|)}