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