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