doc-src/ZF/FOL.tex
author paulson
Wed, 13 Jan 1999 16:36:36 +0100
changeset 6121 5fe77b9b5185
child 8249 3fc32155372c
permissions -rw-r--r--
the separate FOL and ZF logics manual, with new material on datatypes and inductive definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6121
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     1
%% $Id$
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     2
\chapter{First-Order Logic}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     3
\index{first-order logic|(}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     4
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     5
Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     6
  nk}.  Intuitionistic first-order logic is defined first, as theory
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     7
\thydx{IFOL}.  Classical logic, theory \thydx{FOL}, is
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     8
obtained by adding the double negation rule.  Basic proof procedures are
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
     9
provided.  The intuitionistic prover works with derived rules to simplify
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    10
implications in the assumptions.  Classical~\texttt{FOL} employs Isabelle's
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    11
classical reasoner, which simulates a sequent calculus.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    12
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    13
\section{Syntax and rules of inference}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    14
The logic is many-sorted, using Isabelle's type classes.  The class of
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    15
first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    17
as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    19
$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    24
Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    36
Fig.\ts\ref{fol-int-derived}, again with their \ML\ names.  These include
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}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    44
re-inserts the quantified formula for later use.  The rules {\tt
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    45
conj_impE}, etc., support the intuitionistic proof procedure
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    48
See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    49
\texttt{FOL/intprover.ML} for complete listings of the rules and
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    50
derived rules.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    51
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    52
\begin{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    53
\begin{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    54
\begin{tabular}{rrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    55
  \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
    56
  \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
    57
  \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
    58
  \cdx{True}    & $o$                   & tautology ($\top$) \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    59
  \cdx{False}   & $o$                   & absurdity ($\bot$)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    60
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    61
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    62
\subcaption{Constants}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    63
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    64
\begin{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    65
\begin{tabular}{llrrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    66
  \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
    67
  \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
    68
        universal quantifier ($\forall$) \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    69
  \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
    70
        existential quantifier ($\exists$) \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    71
  \texttt{EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 & 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    72
        unique existence ($\exists!$)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    73
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    74
\index{*"E"X"! symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    75
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    76
\subcaption{Binders} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    77
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    78
\begin{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    79
\index{*"= symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    80
\index{&@{\tt\&} symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    81
\index{*"| symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    82
\index{*"-"-"> symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    83
\index{*"<"-"> symbol}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    84
\begin{tabular}{rrrr} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    85
  \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
    86
  \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
    87
  \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
    88
  \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
    89
  \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
    90
  \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
    91
\end{tabular}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    92
\end{center}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    93
\subcaption{Infixes}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    94
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    95
\dquotes
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    96
\[\begin{array}{rcl}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    97
 formula & = & \hbox{expression of type~$o$} \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
    98
         & | & 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
    99
         & | & "\ttilde\ " 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
         & | & formula " <-> " formula \\
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   104
         & | & "ALL~" 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
         & | & "EX!~" id~id^* " . " formula
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   107
  \end{array}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   108
\]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   109
\subcaption{Grammar}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   110
\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
   111
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   114
\begin{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   115
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   116
\tdx{refl}        a=a
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   117
\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
   118
\subcaption{Equality rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   119
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   120
\tdx{conjI}       [| P;  Q |] ==> P&Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   121
\tdx{conjunct1}   P&Q ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   122
\tdx{conjunct2}   P&Q ==> Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   123
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   124
\tdx{disjI1}      P ==> P|Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   125
\tdx{disjI2}      Q ==> P|Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   126
\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
   127
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   128
\tdx{impI}        (P ==> Q) ==> P-->Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   129
\tdx{mp}          [| P-->Q;  P |] ==> Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   130
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   131
\tdx{FalseE}      False ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   132
\subcaption{Propositional rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   133
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   134
\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
   135
\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
   136
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   137
\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
   138
\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
   139
\subcaption{Quantifier rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   140
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   141
\tdx{True_def}    True        == False-->False
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   142
\tdx{not_def}     ~P          == P-->False
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   143
\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
   144
\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
   145
\subcaption{Definitions}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   146
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   147
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   148
\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
   149
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   152
\begin{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   153
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   154
\tdx{sym}       a=b ==> b=a
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   155
\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
   156
\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
   157
\subcaption{Derived equality rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   158
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   159
\tdx{TrueI}     True
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   160
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   161
\tdx{notI}      (P ==> False) ==> ~P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   162
\tdx{notE}      [| ~P;  P |] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   163
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   164
\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
   165
\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
   166
\tdx{iffD1}     [| P <-> Q;  P |] ==> Q            
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   167
\tdx{iffD2}     [| P <-> Q;  Q |] ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   168
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   169
\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
   170
\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
   171
          |] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   172
\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
   173
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   174
\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
   175
\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
   176
\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
   177
\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
   178
\subcaption{Sequent-style elimination rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   179
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   180
\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
   181
\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
   182
\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
   183
\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
   184
\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
   185
             S ==> R |] ==> R
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   186
\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
   187
\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
   188
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   189
\subcaption{Intuitionistic simplification of implication}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   190
\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
   191
\end{figure}
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
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   194
\section{Generic packages}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   195
\FOL{} instantiates most of Isabelle's generic packages.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   196
\begin{itemize}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   197
\item 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   198
It instantiates the simplifier.  Both equality ($=$) and the biconditional
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   199
($\bimp$) may be used for rewriting.  Tactics such as \texttt{Asm_simp_tac} and
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   200
\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   201
most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   202
for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   203
for classical logic.  See the file
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   204
\texttt{FOL/simpdata.ML} for a complete listing of the simplification
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   205
rules%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   206
\iflabelundefined{sec:setting-up-simp}{}%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   207
        {, and \S\ref{sec:setting-up-simp} for discussion}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   208
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   209
\item 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   210
It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   211
for details. 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   212
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   213
\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   214
  for an equality throughout a subgoal and its hypotheses.  This tactic uses
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   215
  \FOL's general substitution rule.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   216
\end{itemize}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   217
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   218
\begin{warn}\index{simplification!of conjunctions}%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   219
  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   220
  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
   221
  is not available by default: it can be slow.  It can be obtained by
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   222
  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   223
\end{warn}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   224
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   225
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   226
\section{Intuitionistic proof procedures} \label{fol-int-prover}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   227
Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   228
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
   229
$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
   230
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
   231
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
   232
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
   233
backtracking.  
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   234
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   235
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
   236
$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
   237
twice:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   238
\[ \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
   239
       \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
   240
\]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   241
The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   242
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
   243
(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
   244
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
   245
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
   246
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
   247
$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   248
S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   249
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
   250
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   251
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
   252
has demonstrated their completeness for propositional
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   253
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
   254
for first-order logic because they discard universally quantified
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   255
assumptions after a single use.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   256
\begin{ttbox} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   257
mp_tac              : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   258
eq_mp_tac           : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   259
IntPr.safe_step_tac : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   260
IntPr.safe_tac      :        tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   261
IntPr.inst_step_tac : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   262
IntPr.step_tac      : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   263
IntPr.fast_tac      : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   264
IntPr.best_tac      : int -> tactic
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   265
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   266
Most of these belong to the structure \texttt{IntPr} and resemble the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   267
tactics of Isabelle's classical reasoner.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   268
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   269
\begin{ttdescription}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   270
\item[\ttindexbold{mp_tac} {\it i}] 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   271
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
   272
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
   273
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
   274
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
   275
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
   276
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
   277
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   278
\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
   279
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
   280
is safe.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   281
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   282
\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
   283
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
   284
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
   285
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   286
\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
   287
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
   288
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   289
\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
   290
but allows unknowns to be instantiated.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   291
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   292
\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
   293
    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
   294
  the intuitionistic proof procedure.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   295
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   296
\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
   297
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
   298
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   299
\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
   300
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
   301
\end{ttdescription}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   302
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
   303
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
   304
(*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
   305
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   306
~~P & ~~(P --> Q) --> ~~Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   307
(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
   308
(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
   309
(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
   310
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   311
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   312
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
\begin{figure} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   315
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   316
\tdx{excluded_middle}    ~P | P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   317
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   318
\tdx{disjCI}    (~Q ==> P) ==> P|Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   319
\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
   320
\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
   321
\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
   322
\tdx{notnotD}   ~~P ==> P
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   323
\tdx{swap}      ~P ==> (~Q ==> P) ==> Q
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   324
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   325
\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
   326
\end{figure}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   327
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   328
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   329
\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
   330
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
   331
the rule
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   332
$$ \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
   333
\noindent
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   334
Natural deduction in classical logic is not really all that natural.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   335
{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   336
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   337
rule (see Fig.\ts\ref{fol-cla-derived}).
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   338
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   339
The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   340
Best_tac} refer to the default claset (\texttt{claset()}), which works for most
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   341
purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   342
propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   343
rules.  See the file \texttt{FOL/cladata.ML} for lists of the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   344
classical rules, and 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   345
\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
   346
        {Chap.\ts\ref{chap:classical}} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   347
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
   348
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   349
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   350
\section{An intuitionistic example}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   351
Here is a session similar to one in {\em Logic and Computation}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   352
\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   353
from {\sc lcf}-based theorem provers such as {\sc hol}.  
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   354
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   355
First, we specify that we are working in intuitionistic logic:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   356
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   357
context IFOL.thy;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   358
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   359
The proof begins by entering the goal, then applying the rule $({\imp}I)$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   360
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   361
Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   362
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   363
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   364
{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   365
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   366
by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   367
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   368
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   369
{\out  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   370
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   371
In this example, we shall never have more than one subgoal.  Applying
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   372
$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   373
\(\ex{y}\all{x}Q(x,y)\) an assumption.  We have the choice of
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   374
$({\exists}E)$ and $({\forall}I)$; let us try the latter.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   375
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   376
by (resolve_tac [allI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   377
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   378
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   379
{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   380
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   381
Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   382
changing the universal quantifier from object~($\forall$) to
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   383
meta~($\Forall$).  The bound variable is a {\bf parameter} of the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   384
subgoal.  We now must choose between $({\exists}I)$ and $({\exists}E)$.  What
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   385
happens if the wrong rule is chosen?
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   386
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   387
by (resolve_tac [exI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   388
{\out Level 3}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   389
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   390
{\out  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   391
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   392
The new subgoal~1 contains the function variable {\tt?y2}.  Instantiating
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   393
{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   394
though~\texttt{x} is a bound variable.  Now we analyse the assumption
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   395
\(\exists y.\forall x. Q(x,y)\) using elimination rules:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   396
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   397
by (eresolve_tac [exE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   398
{\out Level 4}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   399
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   400
{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   401
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   402
Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   403
existential quantifier from the assumption.  But the subgoal is unprovable:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   404
there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   405
Using \texttt{choplev} we can return to the critical point.  This time we
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   406
apply $({\exists}E)$:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   407
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   408
choplev 2;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   409
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   410
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   411
{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   412
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   413
by (eresolve_tac [exE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   414
{\out Level 3}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   415
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   416
{\out  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   417
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   418
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
   419
$({\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
   420
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
   421
example demonstrates.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   422
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   423
by (resolve_tac [exI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   424
{\out Level 4}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   425
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   426
{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   427
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   428
by (eresolve_tac [allE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   429
{\out Level 5}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   430
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   431
{\out  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   432
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   433
The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   434
parameters.  The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   435
x} and \verb|?y3(x,y)| with~\texttt{y}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   436
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   437
by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   438
{\out Level 6}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   439
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   440
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   441
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   442
The theorem was proved in six tactic steps, not counting the abandoned
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   443
ones.  But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   444
theorem in one step.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   445
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   446
Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   447
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   448
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   449
{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   450
by (IntPr.fast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   451
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   452
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   453
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   454
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   455
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   456
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   457
\section{An example of intuitionistic negation}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   458
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
   459
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
   460
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
   461
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   462
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
   463
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
   464
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
   465
only if $\neg\neg P$ is intuitionistically provable.%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   466
\footnote{Of course this holds only for propositional logic, not if $P$ is
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   467
  allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   468
much harder than proving~$P$ classically.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   469
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   470
Our example is the double negation of the classical tautology $(P\imp
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   471
Q)\disj (Q\imp P)$.  When stating the goal, we command Isabelle to expand
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   472
negations to implications using the definition $\neg P\equiv P\imp\bot$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   473
This allows use of the special implication rules.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   474
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   475
Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   476
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   477
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   478
{\out  1. ((P --> Q) | (Q --> P) --> False) --> False}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   479
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   480
The first step is trivial.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   481
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   482
by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   483
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   484
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   485
{\out  1. (P --> Q) | (Q --> P) --> False ==> False}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   486
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   487
By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   488
that formula is not a theorem of intuitionistic logic.  Instead we apply
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   489
the specialized implication rule \tdx{disj_impE}.  It splits the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   490
assumption into two assumptions, one for each disjunct.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   491
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   492
by (eresolve_tac [disj_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   493
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   494
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   495
{\out  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   496
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   497
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
   498
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
   499
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
   500
assumptions~$P$ and~$\neg Q$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   501
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   502
by (eresolve_tac [imp_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   503
{\out Level 3}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   504
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   505
{\out  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   506
{\out  2. [| (Q --> P) --> False; False |] ==> False}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   507
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   508
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
   509
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
   510
applying \tdx{imp_impE} is simpler.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   511
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   512
by (eresolve_tac [imp_impE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   513
{\out Level 4}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   514
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   515
{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   516
{\out  2. [| P; Q --> False; False |] ==> Q}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   517
{\out  3. [| (Q --> P) --> False; False |] ==> False}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   518
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   519
The three subgoals are all trivial.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   520
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   521
by (REPEAT (eresolve_tac [FalseE] 2));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   522
{\out Level 5}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   523
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   524
{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   525
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   526
by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   527
{\out Level 6}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   528
{\out ~ ~ ((P --> Q) | (Q --> P))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   529
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   530
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   531
This proof is also trivial for \texttt{IntPr.fast_tac}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   532
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   533
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   534
\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
   535
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
   536
$\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
   537
follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   538
$\all{x}P(x)$ is true.  Either way the theorem holds.  First, we switch to
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   539
classical logic:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   540
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   541
context FOL.thy;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   542
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   543
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   544
The formal proof does not conform in any obvious way to the sketch given
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   545
above.  The key inference is the first one, \tdx{exCI}; this classical
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   546
version of~$(\exists I)$ allows multiple instantiation of the quantifier.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   547
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   548
Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   549
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   550
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   551
{\out  1. EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   552
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   553
by (resolve_tac [exCI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   554
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   555
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   556
{\out  1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   557
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   558
We can either exhibit a term {\tt?a} to satisfy the conclusion of
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   559
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
   560
steps are routine.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   561
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   562
by (resolve_tac [allI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   563
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   564
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   565
{\out  1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   566
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   567
by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   568
{\out Level 3}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   569
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   570
{\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   571
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   572
By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   573
in effect applies~$(\exists I)$ again.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   574
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   575
by (eresolve_tac [allE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   576
{\out Level 4}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   577
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   578
{\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   579
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   580
In classical logic, a negated assumption is equivalent to a conclusion.  To
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   581
get this effect, we create a swapped version of~$(\forall I)$ and apply it
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   582
using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   583
I)$ using \ttindex{swap_res_tac}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   584
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   585
allI RSN (2,swap);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   586
{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   587
by (eresolve_tac [it] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   588
{\out Level 5}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   589
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   590
{\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   591
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   592
The previous conclusion, \texttt{P(x)}, has become a negated assumption.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   593
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   594
by (resolve_tac [impI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   595
{\out Level 6}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   596
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   597
{\out  1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   598
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   599
The subgoal has three assumptions.  We produce a contradiction between the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   600
\index{assumptions!contradictory} assumptions~\verb|~P(x)| and~{\tt
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   601
  P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   602
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   603
by (eresolve_tac [notE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   604
{\out Level 7}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   605
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   606
{\out  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   607
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   608
by (assume_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   609
{\out Level 8}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   610
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   611
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   612
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   613
The civilised way to prove this theorem is through \ttindex{Blast_tac},
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   614
which automatically uses the classical version of~$(\exists I)$:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   615
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   616
Goal "EX y. ALL x. P(y)-->P(x)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   617
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   618
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   619
{\out  1. EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   620
by (Blast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   621
{\out Depth = 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   622
{\out Depth = 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   623
{\out Depth = 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   624
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   625
{\out EX y. ALL x. P(y) --> P(x)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   626
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   627
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   628
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
   629
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
   630
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
   631
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
   632
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   633
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   634
\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
   635
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
   636
connective $if(P,Q,R)$, where 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   637
$$ 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
   638
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
   639
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
   640
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
   641
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
   642
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   643
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
   644
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
   645
\[ 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
   646
suggests that the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   647
$if$-introduction rule should be
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   648
\[ \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
   649
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
   650
elimination rules for~$\disj$ and~$\conj$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   651
\[ \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
   652
                                  & \infer*{S}{[\neg P,R]}} 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   653
\]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   654
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
   655
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
   656
$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
   657
equation~$(if)$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   658
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   659
If = FOL +
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   660
consts  if     :: [o,o,o]=>o
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   661
rules   if_def "if(P,Q,R) == P&Q | ~P&R"
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   662
end
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   663
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   664
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
   665
is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   666
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   667
use_thy "If";  
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   668
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   669
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
   670
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   671
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   672
\subsection{Deriving the introduction rule}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   673
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   674
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
   675
methods for rewriting with definitions.  Classical reasoning is required,
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   676
so we use \texttt{blast_tac}.
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
The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   679
concludes $if(P,Q,R)$.  We propose the conclusion as the main goal
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   680
using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   681
of $if$ in the subgoal.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   682
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   683
val prems = Goalw [if_def]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   684
    "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   685
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   686
{\out if(P,Q,R)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   687
{\out  1. P & Q | ~ P & R}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   688
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   689
The premises (bound to the {\ML} variable \texttt{prems}) are passed as
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   690
introduction rules to \ttindex{blast_tac}.  Remember that \texttt{claset()} refers
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   691
to the default classical set.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   692
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   693
by (blast_tac (claset() addIs prems) 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   694
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   695
{\out if(P,Q,R)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   696
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   697
qed "ifI";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   698
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   699
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   700
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   701
\subsection{Deriving the elimination rule}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   702
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
   703
The conclusion is simply $S$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   704
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   705
val major::prems = Goalw [if_def]
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   706
   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   707
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   708
{\out S}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   709
{\out  1. S}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   710
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   711
The major premise contains an occurrence of~$if$, but the version returned
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   712
by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   713
definition expanded.  Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   714
assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   715
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   716
by (cut_facts_tac [major] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   717
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   718
{\out S}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   719
{\out  1. P & Q | ~ P & R ==> S}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   720
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   721
by (blast_tac (claset() addIs prems) 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   722
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   723
{\out S}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   724
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   725
qed "ifE";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   726
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   727
As you may recall from
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   728
\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   729
        {\S\ref{definitions}}, there are other
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   730
ways of treating definitions when deriving a rule.  We can start the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   731
proof using \texttt{Goal}, which does not expand definitions, instead of
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   732
\texttt{Goalw}.  We can use \ttindex{rew_tac}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   733
to expand definitions in the subgoals---perhaps after calling
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   734
\ttindex{cut_facts_tac} to insert the rule's premises.  We can use
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   735
\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   736
definitions in the premises directly.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   737
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   738
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   739
\subsection{Using the derived rules}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   740
The rules just derived have been saved with the {\ML} names \tdx{ifI}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   741
and~\tdx{ifE}.  They permit natural proofs of theorems such as the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   742
following:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   743
\begin{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   744
    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
   745
    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
   746
\end{eqnarray*}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   747
Proofs also require the classical reasoning rules and the $\bimp$
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   748
introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}). 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   749
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   750
To display the $if$-rules in action, let us analyse a proof step by step.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   751
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   752
Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> 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
   753
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   754
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   755
{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   756
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   757
by (resolve_tac [iffI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   758
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   759
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   760
{\out  1. if(P,if(Q,A,B),if(Q,C,D)) ==> 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
   761
{\out  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   762
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   763
The $if$-elimination rule can be applied twice in succession.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   764
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   765
by (eresolve_tac [ifE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   766
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   767
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   768
{\out  1. [| P; if(Q,A,B) |] ==> 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
   769
{\out  2. [| ~ P; if(Q,C,D) |] ==> 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
   770
{\out  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   771
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   772
by (eresolve_tac [ifE] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   773
{\out Level 3}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   774
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   775
{\out  1. [| P; Q; A |] ==> 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
   776
{\out  2. [| P; ~ Q; B |] ==> 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
   777
{\out  3. [| ~ P; if(Q,C,D) |] ==> 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
   778
{\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   779
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   780
%
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   781
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
   782
$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
   783
occurrences of $if$ when they become the outermost connective.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   784
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   785
by (resolve_tac [ifI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   786
{\out Level 4}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   787
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   788
{\out  1. [| P; Q; A; Q |] ==> if(P,A,C)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   789
{\out  2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   790
{\out  3. [| P; ~ Q; B |] ==> 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
   791
{\out  4. [| ~ P; if(Q,C,D) |] ==> 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
   792
{\out  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   793
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   794
by (resolve_tac [ifI] 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   795
{\out Level 5}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   796
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   797
{\out  1. [| P; Q; A; Q; P |] ==> A}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   798
{\out  2. [| P; Q; A; Q; ~ P |] ==> C}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   799
{\out  3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   800
{\out  4. [| P; ~ Q; B |] ==> 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
   801
{\out  5. [| ~ P; if(Q,C,D) |] ==> 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
   802
{\out  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   803
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   804
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
   805
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
   806
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
   807
for~$if$.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   808
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   809
AddSIs [ifI];
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   810
AddSEs [ifE];
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   811
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   812
Now we can revert to the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   813
initial proof state and let \ttindex{blast_tac} solve it.  
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   814
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   815
choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   816
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   817
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   818
{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   819
by (Blast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   820
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   821
{\out if(P,if(Q,A,B),if(Q,C,D)) <-> 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
   822
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   823
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   824
This tactic also solves the other example.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   825
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   826
Goal "if(if(P,Q,R), A, B) <-> 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
   827
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   828
{\out if(if(P,Q,R),A,B) <-> 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
   829
{\out  1. if(if(P,Q,R),A,B) <-> 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
   830
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   831
by (Blast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   832
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   833
{\out if(if(P,Q,R),A,B) <-> 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
   834
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   835
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   836
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   837
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   838
\subsection{Derived rules versus definitions}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   839
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
   840
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
   841
us redo the previous proof:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   842
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   843
choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   844
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   845
{\out if(if(P,Q,R),A,B) <-> 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
   846
{\out  1. if(if(P,Q,R),A,B) <-> 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
   847
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   848
This time, simply unfold using the definition of $if$:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   849
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   850
by (rewtac if_def);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   851
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   852
{\out if(if(P,Q,R),A,B) <-> 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
   853
{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   854
{\out     P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   855
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   856
We are left with a subgoal in pure first-order logic, which is why the 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   857
classical reasoner can prove it given \texttt{FOL_cs} alone.  (We could, of 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   858
course, have used \texttt{Blast_tac}.)
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   859
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   860
by (blast_tac FOL_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   861
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   862
{\out if(if(P,Q,R),A,B) <-> 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
   863
{\out No subgoals!}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   864
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   865
Expanding definitions reduces the extended logic to the base logic.  This
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   866
approach has its merits --- especially if the prover for the base logic is
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   867
good --- but can be slow.  In these examples, proofs using the default
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   868
claset (which includes the derived rules) run about six times faster 
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   869
than proofs using \texttt{FOL_cs}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   870
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   871
Expanding definitions also complicates error diagnosis.  Suppose we are having
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   872
difficulties in proving some goal.  If by expanding definitions we have
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   873
made it unreadable, then we have little hope of diagnosing the problem.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   874
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   875
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
   876
Let us try to prove one:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   877
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   878
Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   879
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   880
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   881
{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   882
by (Blast_tac 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   883
{\out by: tactic failed}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   884
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   885
This failure message is uninformative, but we can get a closer look at the
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   886
situation by applying \ttindex{Step_tac}.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   887
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   888
by (REPEAT (Step_tac 1));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   889
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   890
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   891
{\out  1. [| A; ~ P; R; ~ P; R |] ==> B}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   892
{\out  2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   893
{\out  3. [| ~ P; R; B; ~ P; R |] ==> A}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   894
{\out  4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   895
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   896
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
   897
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
   898
$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
   899
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   900
We can repeat this analysis by expanding definitions, using just
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   901
the rules of {\FOL}:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   902
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   903
choplev 0;
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   904
{\out Level 0}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   905
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   906
{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   907
\ttbreak
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   908
by (rewtac if_def);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   909
{\out Level 1}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   910
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   911
{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   912
{\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   913
by (blast_tac FOL_cs 1);
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   914
{\out by: tactic failed}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   915
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   916
Again we apply \ttindex{step_tac}:
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   917
\begin{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   918
by (REPEAT (step_tac FOL_cs 1));
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   919
{\out Level 2}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   920
{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   921
{\out  1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   922
{\out  2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   923
{\out  3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   924
{\out  4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   925
{\out  5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   926
{\out  6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   927
{\out  7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   928
{\out  8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   929
\end{ttbox}
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   930
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
   931
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
   932
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   933
Expanding definitions causes a great increase in complexity.  This is why
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   934
the classical prover has been designed to accept derived rules.
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   935
5fe77b9b5185 the separate FOL and ZF logics manual, with new material on datatypes and
paulson
parents:
diff changeset
   936
\index{first-order logic|)}