src/Doc/ZF/document/FOL.tex
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30099
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
     1
%!TEX root = logics-ZF.tex
6121
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}
43077
7d69154d824b Workaround for bug involving makeindex, hyperref and the | symbol
paulson
parents: 30099
diff changeset
    80
\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
6121
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}
30099
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   363
\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   364
\isacommand{begin}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   365
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   366
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
   367
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   368
\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
   369
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   370
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   371
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   372
\isacommand{apply}\ (rule\ impI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   373
\ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   374
\isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   375
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   376
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
   377
In this example, we shall never have more than one subgoal.  Applying
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   378
$({\imp}I)$ replaces~\isa{\isasymlongrightarrow}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   379
by~\isa{\isasymLongrightarrow}, so that
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   380
\(\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
   381
$({\exists}E)$ and $({\forall}I)$; let us try the latter.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   382
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   383
\isacommand{apply}\ (rule\ allI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   384
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   385
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   386
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   387
Applying $({\forall}I)$ replaces the \isa{\isasymforall
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   388
x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   389
(or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   390
meta universal quantifier.  The bound variable is a {\bf parameter} of
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   391
the subgoal.  We now must choose between $({\exists}I)$ and
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   392
$({\exists}E)$.  What happens if the wrong rule is chosen?
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   393
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   394
\isacommand{apply}\ (rule\ exI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   395
\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   396
\isasymLongrightarrow \ Q(x,\ ?y2(x))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   397
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   398
The new subgoal~1 contains the function variable \isa{?y2}.  Instantiating
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   399
\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
   400
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
   401
\(\exists y.\forall x. Q(x,y)\) using elimination rules:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   402
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   403
\isacommand{apply}\ (erule\ exE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   404
\ 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
   405
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   406
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
   407
existential quantifier from the assumption.  But the subgoal is unprovable:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   408
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
   409
Using Proof General, we can return to the critical point, marked
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   410
$(*)$ above.  This time we apply $({\exists}E)$:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   411
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   412
\isacommand{apply}\ (erule\ exE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   413
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   414
\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   415
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   416
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
   417
$({\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
   418
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
   419
example demonstrates.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   420
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   421
\isacommand{apply}\ (rule\ exI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   422
\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   423
\isasymLongrightarrow \ Q(x,\ ?y3(x,\ y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   424
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   425
\isacommand{apply}\ (erule\ allE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   426
\ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   427
Q(x,\ ?y3(x,\ y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   428
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   429
The subgoal has variables \isa{?y3} and \isa{?x4} applied to both
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   430
parameters.  The obvious projection functions unify \isa{?x4(x,y)} with~\isa{
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   431
x} and \isa{?y3(x,y)} with~\isa{y}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   432
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   433
\isacommand{apply}\ assumption\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   434
No\ subgoals!\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   435
\isacommand{done}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   436
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   437
The theorem was proved in six method invocations, not counting the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   438
abandoned ones.  But proof checking is tedious, and the \ML{} tactic
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   439
\ttindex{IntPr.fast_tac} can prove the theorem in one step.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   440
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   441
\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
   442
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   443
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   444
\isanewline
30099
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   445
\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   446
No\ subgoals!
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   447
\end{isabelle}
6121
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   450
\section{An example of intuitionistic negation}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   451
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
   452
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
   453
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
   454
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   455
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
   456
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
   457
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
   458
only if $\neg\neg P$ is intuitionistically provable.%
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   459
\footnote{This remark holds only for propositional logic, not if $P$ is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   460
  allowed to contain quantifiers.}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   461
%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   462
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
   463
much harder than proving~$P$ classically.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   464
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   465
Our example is the double negation of the classical tautology $(P\imp
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   466
Q)\disj (Q\imp P)$.  The first step is apply the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   467
\isa{unfold} method, which expands
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   468
negations to implications using the definition $\neg P\equiv P\imp\bot$
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   469
and allows use of the special implication rules.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   470
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   471
\isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   472
\ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   473
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   474
\isacommand{apply}\ (unfold\ not\_def)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   475
\ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   476
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   477
The next step is a trivial use of $(\imp I)$.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   478
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   479
\isacommand{apply}\ (rule\ impI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   480
\ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   481
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   482
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
   483
that formula is not a theorem of intuitionistic logic.  Instead, we
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   484
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
   485
assumption into two assumptions, one for each disjunct.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   486
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   487
\isacommand{apply}\ (erule\ disj\_impE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   488
\ 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
   489
False
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   490
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   491
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
   492
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
   493
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
   494
assumptions~$P$ and~$\neg Q$.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   495
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   496
\isacommand{apply}\ (erule\ imp\_impE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   497
\ 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
   498
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   499
False
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   500
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   501
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
   502
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
   503
applying \tdx{imp_impE} is simpler.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   504
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   505
\ \isacommand{apply}\ (erule\ imp\_impE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   506
\ 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
   507
\ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   508
\ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   509
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   510
The three subgoals are all trivial.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   511
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   512
\isacommand{apply}\ assumption\ \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   513
\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   514
False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   515
\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   516
\isasymlongrightarrow \ False;\ False\isasymrbrakk \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   517
\isasymLongrightarrow \ False%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   518
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   519
\isacommand{apply}\ (erule\ FalseE)+\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   520
No\ subgoals!\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   521
\isacommand{done}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   522
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   523
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
   524
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   525
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   526
\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
   527
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
   528
$\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
   529
follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   530
$\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
   531
work in a theory based on classical logic, the theory \isa{FOL}:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   532
\begin{isabelle}
30099
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   533
\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   534
\isacommand{begin}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   535
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   536
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   537
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
   538
above.  Its key step is its first rule, \tdx{exCI}, a classical
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   539
version of~$(\exists I)$ that allows multiple instantiation of the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   540
quantifier.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   541
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   542
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   543
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   544
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   545
\isacommand{apply}\ (rule\ exCI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   546
\ 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
   547
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   548
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
   549
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
   550
steps are routine.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   551
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   552
\isacommand{apply}\ (rule\ allI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   553
\ 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
   554
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   555
\isacommand{apply}\ (rule\ impI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   556
\ 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
   557
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   558
By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   559
is equivalent to applying~$(\exists I)$ again.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   560
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   561
\isacommand{apply}\ (erule\ allE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   562
\ 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
   563
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   564
In classical logic, a negated assumption is equivalent to a conclusion.  To
8249
3fc32155372c fixed some overfull lines
paulson
parents: 6121
diff changeset
   565
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
   566
using \ttindex{erule}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   567
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   568
\isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   569
\ 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
   570
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   571
The operand of \isa{erule} above denotes the following theorem:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   572
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   573
\ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   574
\isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   575
?P1(x)\isasymrbrakk \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   576
\isasymLongrightarrow \ ?P%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   577
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   578
The previous conclusion, \isa{P(x)}, has become a negated assumption.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   579
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   580
\isacommand{apply}\ (rule\ impI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   581
\ 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
   582
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   583
The subgoal has three assumptions.  We produce a contradiction between the
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   584
\index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   585
and~\isa{P(?y3(x))}.   The proof never instantiates the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   586
unknown~\isa{?a}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   587
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   588
\isacommand{apply}\ (erule\ notE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   589
\ 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
   590
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   591
\isacommand{apply}\ assumption\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   592
No\ subgoals!\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   593
\isacommand{done}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   594
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   595
The civilised way to prove this theorem is using the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   596
\methdx{blast} method, which automatically uses the classical form
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   597
of the rule~$(\exists I)$:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   598
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   599
\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   600
\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   601
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   602
\isacommand{by}\ blast\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   603
No\ subgoals!
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   604
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   605
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
   606
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
   607
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
   608
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
   609
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   610
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   611
\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
   612
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
   613
connective $if(P,Q,R)$, where 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   614
$$ 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
   615
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
   616
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
   617
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
   618
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
   619
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   620
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
   621
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
   622
\[ 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
   623
suggests that the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   624
$if$-introduction rule should be
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   625
\[ \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
   626
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
   627
elimination rules for~$\disj$ and~$\conj$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   628
\[ \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
   629
                                  & \infer*{S}{[\neg P,R]}} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   630
\]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   631
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
   632
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
   633
$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
   634
equation~$(if)$.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   635
\begin{isabelle}
30099
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   636
\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline
dde11464969c Updated the theory syntax. Corrected an error in a command.
paulson
parents: 14158
diff changeset
   637
\isacommand{begin}\isanewline
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   638
\isacommand{constdefs}\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   639
\ \ if\ ::\ "[o,o,o]=>o"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   640
\ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   641
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   642
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
   643
is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   644
\begin{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   645
use_thy "If";  
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   646
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   647
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
   648
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   649
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   650
\subsection{Deriving the introduction rule}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   651
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   652
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
   653
methods for rewriting with definitions.  Classical reasoning is required,
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   654
so we use \isa{blast}.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   655
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   656
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
   657
concludes $if(P,Q,R)$.  We propose this lemma and immediately simplify
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   658
using \isa{if\_def} to expand the definition of \isa{if} in the
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   659
subgoal.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   660
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   661
\isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   662
|]\ ==>\ if(P,Q,R)"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   663
\ 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
   664
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   665
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   666
\ 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
   667
R
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   668
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   669
The rule's premises, although expressed using meta-level implication
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   670
(\isa{\isasymLongrightarrow}) are passed as ordinary implications to
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   671
\methdx{blast}.  
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   672
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   673
\isacommand{apply}\ blast\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   674
No\ subgoals!\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   675
\isacommand{done}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   676
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   677
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   678
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   679
\subsection{Deriving the elimination rule}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   680
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
   681
The conclusion is simply $S$.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   682
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   683
\isacommand{lemma}\ ifE:\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   684
\ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   685
\ 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
   686
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   687
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   688
\ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   689
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   690
The proof script is the same as before: \isa{simp} followed by
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   691
\isa{blast}:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   692
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   693
\isacommand{apply}\ blast\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   694
No\ subgoals!\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   695
\isacommand{done}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   696
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   697
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   698
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   699
\subsection{Using the derived rules}
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   700
Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   701
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
   702
\begin{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   703
    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
   704
    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
   705
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   706
Proofs also require the classical reasoning rules and the $\bimp$
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   707
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
   708
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   709
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
   710
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   711
\isacommand{lemma}\ if\_commute:\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   712
\ \ \ \ \ "if(P,\ if(Q,A,B),\
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   713
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
   714
\isacommand{apply}\ (rule\ iffI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   715
\ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   716
\isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   717
\ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   718
\isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   719
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   720
The $if$-elimination rule can be applied twice in succession.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   721
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   722
\isacommand{apply}\ (erule\ ifE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   723
\ 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
   724
\ 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
   725
\ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   726
\isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   727
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   728
\isacommand{apply}\ (erule\ ifE)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   729
\ 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
   730
\ 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
   731
\ 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
   732
\ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   733
\isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   734
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   735
%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   736
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
   737
$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
   738
occurrences of $if$ when they become the outermost connective.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   739
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   740
\isacommand{apply}\ (rule\ ifI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   741
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   742
\ 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
   743
\ 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
   744
\ 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
   745
\ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   746
\isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   747
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   748
\isacommand{apply}\ (rule\ ifI)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   749
\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   750
\ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   751
\ 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
   752
\ 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
   753
\ 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
   754
\ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   755
\isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   756
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   757
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
   758
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
   759
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
   760
for~$if$.
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   761
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   762
\isacommand{declare}\ ifI\ [intro!]\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   763
\isacommand{declare}\ ifE\ [elim!]
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   764
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   765
With these declarations, we could have proved this theorem with a single
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   766
call to \isa{blast}.  Here is another example:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   767
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   768
\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
   769
\ 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
   770
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   771
\isacommand{by}\ blast
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   772
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   773
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   774
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   775
\subsection{Derived rules versus definitions}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   776
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
   777
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
   778
us redo the previous proof:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   779
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   780
\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
   781
\ 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
   782
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   783
This time, we simply unfold using the definition of $if$:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   784
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   785
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   786
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   787
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   788
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   789
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
   790
\isa{blast}:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   791
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   792
\isacommand{apply}\ blast\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   793
No\ subgoals!
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   794
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   795
Expanding definitions reduces the extended logic to the base logic.  This
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   796
approach has its merits, but it can be slow.  In these examples, proofs
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   797
using the derived rules for~\isa{if} run about six
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   798
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
   799
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   800
Expanding definitions can also make it harder to diagnose errors. 
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   801
Suppose we are having difficulties in proving some goal.  If by expanding
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   802
definitions we have made it unreadable, then we have little hope of
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   803
diagnosing the problem.
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   804
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   805
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
   806
Let us try to prove one:
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   807
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   808
\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
   809
\ 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
   810
A))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   811
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   812
Calling \isa{blast} yields an uninformative failure message. We can
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   813
get a closer look at the situation by applying \methdx{auto}.
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   814
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   815
\isacommand{apply}\ auto\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   816
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   817
\ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   818
\ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   819
\ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   820
False
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   821
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   822
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
   823
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
   824
$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
   825
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 8249
diff changeset
   826
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
   827
first-order logic:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   828
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   829
\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
   830
\ 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
   831
A))
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   832
\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   833
\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   834
\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   835
\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A)
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   836
\end{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   837
Again \isa{blast} would fail, so we try \methdx{auto}:
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   838
\begin{isabelle}
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   839
\isacommand{apply}\ (auto)\ \isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   840
\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   841
\ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   842
\ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   843
\ 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
   844
\ 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
   845
\ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   846
\ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   847
\ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q%
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   848
\end{isabelle}
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   849
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
   850
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
   851
14154
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   852
Expanding your definitions usually makes proofs more difficult.  This is
3bc0128e2c74 partial conversion to Isar format
paulson
parents: 9695
diff changeset
   853
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
   854
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   855
\index{first-order logic|)}