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