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