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