doc-src/Logics/FOL.tex
 changeset 104 d8205bb279a7 child 111 1b3cddf41b2d
equal inserted replaced
103:30bd42401ab2 104:d8205bb279a7

     1 %% $Id$

     2 \chapter{First-order logic}

     3 The directory~\ttindexbold{FOL} contains theories for first-order logic

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

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

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

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

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

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

    10

    11 \section{Syntax and rules of inference}

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

    13 class of first-order terms is called {\it term} and is a subclass of

    14 {\it logic}.  No types of individuals

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

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

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

    18 equality symbol and quantifiers are polymorphic (many-sorted).  The type of

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

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

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

    22

    23 The intuitionistic theory has the \ML\ identifier

    24 \ttindexbold{IFOL.thy}.  Figure~\ref{fol-rules} shows the inference

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

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

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

    28 and elimination rules are derived for it.

    29

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

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

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

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

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

    35

    36 Some intuitionistic derived rules are shown in

    37 Figure~\ref{fol-int-derived}, again with their \ML\ names.  These include

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

    39 deduction typically involves a combination of forwards and backwards

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

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

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

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

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

    45 re-inserts the quantified formula for later use.  The rules {\tt

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

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

    48

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

    50 \ttindexbold{FOL/int-prover.ML} for complete listings of the rules and

    51 derived rules.

    52

    53 \begin{figure}

    54 \begin{center}

    55 \begin{tabular}{rrr}

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

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

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

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

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

    61 \end{tabular}

    62 \end{center}

    63 \subcaption{Constants}

    64

    65 \begin{center}

    66 \begin{tabular}{llrrr}

    67   \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\

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

    69 	universal quantifier ($\forall$) \\

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

    71 	existential quantifier ($\exists$) \\

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

    73 	unique existence ($\exists!$)

    74 \end{tabular}

    75 \end{center}

    76 \subcaption{Binders}

    77

    78 \begin{center}

    79 \indexbold{*"=}

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

    81 \indexbold{*"|}

    82 \indexbold{*"-"-">}

    83 \indexbold{*"<"-">}

    84 \begin{tabular}{rrrr}

    85   \it symbol  	& \it meta-type & \it precedence & \it description \\

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

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

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

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

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

    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 \\    99 & | & term " \ttilde= " term \\    100 & | & "\ttilde\ " formula \\    101 & | & formula " \& " formula \\    102 & | & formula " | " formula \\    103 & | & formula " --> " formula \\    104 & | & formula " <-> " formula \\    105 & | & "ALL~" id~id^* " . " formula \\    106 & | & "EX~~" id~id^* " . " formula \\    107 & | & "EX!~" id~id^* " . " formula    108 \end{array}    109$

   110 \subcaption{Grammar}

   111 \caption{Syntax of {\tt FOL}} \label{fol-syntax}

   112 \end{figure}

   113

   114

   115 \begin{figure}

   116 \begin{ttbox}

   117 \idx{refl}        a=a

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

   119 \subcaption{Equality rules}

   120

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

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

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

   124

   125 \idx{disjI1}      P ==> P|Q

   126 \idx{disjI2}      Q ==> P|Q

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

   128

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

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

   131

   132 \idx{FalseE}      False ==> P

   133 \subcaption{Propositional rules}

   134

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

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

   137

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

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

   140 \subcaption{Quantifier rules}

   141

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

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

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

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

   146 \subcaption{Definitions}

   147 \end{ttbox}

   148

   149 \caption{Rules of intuitionistic {\tt FOL}} \label{fol-rules}

   150 \end{figure}

   151

   152

   153 \begin{figure}

   154 \begin{ttbox}

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

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

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

   158 \subcaption{Derived equality rules}

   159

   160 \idx{TrueI}     True

   161

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

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

   164

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

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

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

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

   169

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

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

   172           |] ==> R

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

   174

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

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

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

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

   179 \subcaption{Sequent-style elimination rules}

   180

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

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

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

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

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

   186              S ==> R |] ==> R

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

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

   189 \end{ttbox}

   190 \subcaption{Intuitionistic simplification of implication}

   191 \caption{Derived rules for {\tt FOL}} \label{fol-int-derived}

   192 \end{figure}

   193

   194

   195 \section{Generic packages}

   196 \FOL{} instantiates most of Isabelle's generic packages;

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

   198 \begin{itemize}

   199 \item

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

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

   202 throughout a subgoal and its hypotheses.

   203 \item

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

   205 set for intuitionistic first-order logic, while \ttindexbold{FOL_ss} is the

   206 simplification set for classical logic.  Both equality ($=$) and the

   207 biconditional ($\bimp$) may be used for rewriting.  See the file

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

   209 rules.

   210 \item

   211 It instantiates the classical reasoning module.  See~\S\ref{fol-cla-prover}

   212 for details.

   213 \end{itemize}

   214

   215

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

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

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

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

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

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

   222 must be abandoned.  Thus intuitionistic propositional logic requires

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

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

   225 needed twice:

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

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

   230 Instead, it simplifies implications using derived rules

   231 (Figure~\ref{fol-int-derived}).  It reduces the antecedents of implications

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

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

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

   235 $(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp    236 S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires

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

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

   239 essentially the same simple manner.

   240

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

   242 has demonstrated their completeness for propositional

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

   244 for first-order logic because they discard universally quantified

   245 assumptions after a single use.

   246 \begin{ttbox}

   247 mp_tac            : int -> tactic

   248 eq_mp_tac         : int -> tactic

   249 Int.safe_step_tac : int -> tactic

   250 Int.safe_tac      :        tactic

   251 Int.step_tac      : int -> tactic

   252 Int.fast_tac      : int -> tactic

   253 Int.best_tac      : int -> tactic

   254 \end{ttbox}

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

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

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

   258

   259 \begin{description}

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

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

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

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

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

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

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

   267

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

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

   270 is safe.

   271

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

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

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

   275

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

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

   278

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

   280 but allows unknowns to be instantiated.

   281

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

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

   284 proof procedure.

   285

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

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

   288 proof procedure.

   289

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

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

   292

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

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

   295 \end{description}

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

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

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

   299 \begin{ttbox}

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

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

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

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

   304 \end{ttbox}

   305

   306

   307

   308 \begin{figure}

   309 \begin{ttbox}

   310 \idx{excluded_middle}    ~P | P

   311

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

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

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

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

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

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

   318 \end{ttbox}

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

   320 \end{figure}

   321

   322

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

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

   325 consists of intuitionistic logic plus the rule

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

   327 \noindent

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

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

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

   331 rule (see Figure~\ref{fol-cla-derived}).

   332

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

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

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

   336 Single-step proofs can be performed, using \ttindex{swap_res_tac} to deal

   337 with negated assumptions.

   338

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

   340 \begin{ttbox}

   341 prop_cs    : claset

   342 FOL_cs     : claset

   343 FOL_dup_cs : claset

   344 \end{ttbox}

   345 \begin{description}

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

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

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

   349

   350 \item[\ttindexbold{FOL_cs}]

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

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

   353 unique existence.  Search using this is incomplete since quantified

   354 formulae are used at most once.

   355

   356 \item[\ttindexbold{FOL_dup_cs}]

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

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

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

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

   361 generally unsuitable for depth-first search.

   362 \end{description}

   363 \noindent

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

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

   366 classical proof methods.

   367

   368

   369 \section{An intuitionistic example}

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

   371 \cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently

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

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

   374 $({\imp}I)$.

   375 \begin{ttbox}

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

   377 {\out Level 0}

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

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

   380 \ttbreak

   381 by (resolve_tac [impI] 1);

   382 {\out Level 1}

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

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

   385 \end{ttbox}

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

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

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

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

   390 \begin{ttbox}

   391 by (resolve_tac [allI] 1);

   392 {\out Level 2}

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

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

   395 \end{ttbox}

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

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

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

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

   400 happens if the wrong rule is chosen?

   401 \begin{ttbox}

   402 by (resolve_tac [exI] 1);

   403 {\out Level 3}

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

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

   406 \end{ttbox}

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

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

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

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

   411 \begin{ttbox}

   412 by (eresolve_tac [exE] 1);

   413 {\out Level 4}

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

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

   416 \end{ttbox}

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

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

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

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

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

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

   423 \begin{ttbox}

   424 choplev 2;

   425 {\out Level 2}

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

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

   428 \ttbreak

   429 by (eresolve_tac [exE] 1);

   430 {\out Level 3}

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

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

   433 \end{ttbox}

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

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

   436 two scheme variables.

   437 \begin{ttbox}

   438 by (resolve_tac [exI] 1);

   439 {\out Level 4}

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

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

   442 \ttbreak

   443 by (eresolve_tac [allE] 1);

   444 {\out Level 5}

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

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

   447 \end{ttbox}

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

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

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

   451 \begin{ttbox}

   452 by (assume_tac 1);

   453 {\out Level 6}

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

   455 {\out No subgoals!}

   456 \end{ttbox}

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

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

   459 theorem in one step.

   460 \begin{ttbox}

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

   462 {\out Level 0}

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

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

   465 by (Int.fast_tac 1);

   466 {\out Level 1}

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

   468 {\out No subgoals!}

   469 \end{ttbox}

   470

   471

   472 \section{An example of intuitionistic negation}

   473 The following example demonstrates the specialized forms of implication

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

   475 the basic rules; the specialized rules help considerably.

   476

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

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

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

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

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

   482 accordingly, is the double negation of a classical tautology: $(P\imp    483 Q)\disj (Q\imp P)$.

   484

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

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

   487 derived rules that effect precisely this definition --- the automatic

   488 tactics apply them --- it seems more straightforward to unfold the

   489 negations.

   490 \begin{ttbox}

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

   492 {\out Level 0}

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

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

   495 \end{ttbox}

   496 The first step is trivial.

   497 \begin{ttbox}

   498 by (resolve_tac [impI] 1);

   499 {\out Level 1}

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

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

   502 \end{ttbox}

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

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

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

   506 \begin{ttbox}

   507 by (eresolve_tac [disj_impE] 1);

   508 {\out Level 2}

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

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

   511 \end{ttbox}

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

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

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

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

   516 \begin{ttbox}

   517 by (eresolve_tac [imp_impE] 1);

   518 {\out Level 3}

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

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

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

   522 \end{ttbox}

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

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

   525 applying \ttindex{imp_impE} is simpler.

   526 \begin{ttbox}

   527 by (eresolve_tac [imp_impE] 1);

   528 {\out Level 4}

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

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

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

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

   533 \end{ttbox}

   534 The three subgoals are all trivial.

   535 \begin{ttbox}

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

   537 {\out Level 5}

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

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

   540 by (assume_tac 1);

   541 {\out Level 6}

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

   543 {\out No subgoals!}

   544 \end{ttbox}

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

   546

   547

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

   549 To illustrate classical logic, we shall prove the theorem

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

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

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

   553

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

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

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

   557 \begin{ttbox}

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

   559 {\out Level 0}

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

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

   562 \ttbreak

   563 by (resolve_tac [exCI] 1);

   564 {\out Level 1}

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

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

   567 \end{ttbox}

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

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

   570 steps routinely break down the conclusion and assumption.

   571 \begin{ttbox}

   572 by (resolve_tac [allI] 1);

   573 {\out Level 2}

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

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

   576 \ttbreak

   577 by (resolve_tac [impI] 1);

   578 {\out Level 3}

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

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

   581 \ttbreak

   582 by (eresolve_tac [allE] 1);

   583 {\out Level 4}

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

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

   586 \end{ttbox}

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

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

   589 using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall    590 I)$ using \ttindex{swap_res_tac}.

   591 \begin{ttbox}

   592 allI RSN (2,swap);

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

   594 by (eresolve_tac [it] 1);

   595 {\out Level 5}

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

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

   598 \end{ttbox}

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

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

   601 \begin{ttbox}

   602 by (resolve_tac [impI] 1);

   603 {\out Level 6}

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

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

   606 \end{ttbox}

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

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

   609 the unknown~{\tt?a}.

   610 \begin{ttbox}

   611 by (eresolve_tac [notE] 1);

   612 {\out Level 7}

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

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

   615 \ttbreak

   616 by (assume_tac 1);

   617 {\out Level 8}

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

   619 {\out No subgoals!}

   620 \end{ttbox}

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

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

   623 \begin{ttbox}

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

   625 {\out Level 0}

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

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

   628 by (best_tac FOL_dup_cs 1);

   629 {\out Level 1}

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

   631 {\out No subgoals!}

   632 \end{ttbox}

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

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

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

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

   637

   638

   639 \section{Derived rules and the classical tactics}

   640 Classical first-order logic can be extended with the propositional

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

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

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

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

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

   646 formula.  Introducing further abbreviations makes the problem worse.

   647

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

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

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

   651 suggests that the

   652 $if$-introduction rule should be

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

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

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

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

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

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

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

   662 equation~$(if)$.

   663 \begin{ttbox}

   664 If = FOL +

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

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

   667 end

   668 \end{ttbox}

   669 The derivations of the introduction and elimination rules demonstrate the

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

   671 so we use \ttindex{fast_tac}.

   672

   673

   674 \subsection{Deriving the introduction rule}

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

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

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

   678 of $if$ in the subgoal.

   679 \begin{ttbox}

   680 val prems = goalw If.thy [if_def]

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

   682 {\out Level 0}

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

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

   685 \end{ttbox}

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

   687 introduction rules to \ttindex{fast_tac}:

   688 \begin{ttbox}

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

   690 {\out Level 1}

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

   692 {\out No subgoals!}

   693 val ifI = result();

   694 \end{ttbox}

   695

   696

   697 \subsection{Deriving the elimination rule}

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

   699 The conclusion is simply $S$.

   700 \begin{ttbox}

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

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

   703 {\out Level 0}

   704 {\out S}

   705 {\out  1. S}

   706 \end{ttbox}

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

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

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

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

   711 \begin{ttbox}

   712 by (cut_facts_tac [major] 1);

   713 {\out Level 1}

   714 {\out S}

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

   716 \ttbreak

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

   718 {\out Level 2}

   719 {\out S}

   720 {\out No subgoals!}

   721 val ifE = result();

   722 \end{ttbox}

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

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

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

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

   727 to expand definitions in the subgoals --- perhaps after calling

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

   729 \ttindex{rewrite_rule}, which is a meta-inference rule, to expand

   730 definitions in the premises directly.

   731

   732

   733 \subsection{Using the derived rules}

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

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

   736 following:

   737 \begin{eqnarray*}

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

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

   740 \end{eqnarray*}

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

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

   743

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

   745 \begin{ttbox}

   746 goal If.thy

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

   748 {\out Level 0}

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

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

   751 \ttbreak

   752 by (resolve_tac [iffI] 1);

   753 {\out Level 1}

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

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

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

   757 \end{ttbox}

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

   759 \begin{ttbox}

   760 by (eresolve_tac [ifE] 1);

   761 {\out Level 2}

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

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

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

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

   766 \ttbreak

   767 by (eresolve_tac [ifE] 1);

   768 {\out Level 3}

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

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

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

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

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

   774 \end{ttbox}

   775

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

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

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

   779 \begin{ttbox}

   780 by (resolve_tac [ifI] 1);

   781 {\out Level 4}

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

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

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

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

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

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

   788 \ttbreak

   789 by (resolve_tac [ifI] 1);

   790 {\out Level 5}

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

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

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

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

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

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

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

   798 \end{ttbox}

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

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

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

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

   803 for~$if$.

   804 \begin{ttbox}

   805 choplev 0;

   806 {\out Level 0}

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

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

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

   810 by (fast_tac if_cs 1);

   811 {\out Level 1}

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

   813 {\out No subgoals!}

   814 \end{ttbox}

   815 This tactic also solves the other example.

   816 \begin{ttbox}

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

   818 {\out Level 0}

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

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

   821 \ttbreak

   822 by (fast_tac if_cs 1);

   823 {\out Level 1}

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

   825 {\out No subgoals!}

   826 \end{ttbox}

   827

   828

   829 \subsection{Derived rules versus definitions}

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

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

   832 us redo the previous proof:

   833 \begin{ttbox}

   834 choplev 0;

   835 {\out Level 0}

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

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

   838 \ttbreak

   839 by (rewrite_goals_tac [if_def]);

   840 {\out Level 1}

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

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

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

   844 \ttbreak

   845 by (fast_tac FOL_cs 1);

   846 {\out Level 2}

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

   848 {\out No subgoals!}

   849 \end{ttbox}

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

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

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

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

   854

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

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

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

   858

   859 Attempts at program verification often yield invalid assertions.

   860 Let us try to prove one:

   861 \begin{ttbox}

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

   863 {\out Level 0}

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

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

   866 by (fast_tac FOL_cs 1);

   867 {\out by: tactic failed}

   868 \end{ttbox}

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

   870 situation by applying \ttindex{step_tac}.

   871 \begin{ttbox}

   872 by (REPEAT (step_tac if_cs 1));

   873 {\out Level 1}

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

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

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

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

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

   879 \end{ttbox}

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

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

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

   883

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

   885 the rules of {\FOL}:

   886 \begin{ttbox}

   887 choplev 0;

   888 {\out Level 0}

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

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

   891 \ttbreak

   892 by (rewrite_goals_tac [if_def]);

   893 {\out Level 1}

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

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

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

   897 by (fast_tac FOL_cs 1);

   898 {\out by: tactic failed}

   899 \end{ttbox}

   900 Again we apply \ttindex{step_tac}:

   901 \begin{ttbox}

   902 by (REPEAT (step_tac FOL_cs 1));

   903 {\out Level 2}

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

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

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

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

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

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

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

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

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

   913 \end{ttbox}

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

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

   916

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

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