doc-src/Logics/LK.tex
author wenzelm
Sat, 01 Jul 2000 19:49:20 +0200
changeset 9226 cbe6144f0f15
parent 7116 8c1caac3e54e
child 9695 ec7d7f877712
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
291
a615050a7494 first draft of Springer volume
lcp
parents: 264
diff changeset
     2
\chapter{First-Order Sequent Calculus}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
     3
\index{sequent calculus|(}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
     4
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
     5
The theory~\thydx{LK} implements classical first-order logic through Gentzen's
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
     6
sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
     7
Resembling the method of semantic tableaux, the calculus is well suited for
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
     8
backwards proof.  Assertions have the form \(\Gamma\turn \Delta\), where
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
     9
\(\Gamma\) and \(\Delta\) are lists of formulae.  Associative unification,
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    10
simulated by higher-order unification, handles lists
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    11
(\S\ref{sec:assoc-unification} presents details, if you are interested).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    13
The logic is many-sorted, using Isabelle's type classes.  The class of
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    14
first-order terms is called \cldx{term}.  No types of individuals are
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    15
provided, but extensions can define types such as {\tt nat::term} and type
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    16
constructors such as {\tt list::(term)term}.  Below, the type variable
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    17
$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    18
are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    19
belongs to class {\tt logic}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    21
\LK{} implements a classical logic theorem prover that is nearly as powerful
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    22
as the generic classical reasoner.  The simplifier is now available too.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    24
To work in LK, start up Isabelle specifying  \texttt{Sequents} as the
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    25
object-logic.  Once in Isabelle, change the context to theory \texttt{LK.thy}:
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    26
\begin{ttbox}
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    27
isabelle Sequents
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    28
context LK.thy;
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    29
\end{ttbox}
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    30
Model logic and linear logic are also available, but unfortunately they are
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    31
not documented.
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
    32
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    37
  \it name      &\it meta-type          & \it description       \\ 
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    38
  \cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    39
  \cdx{Seqof}   & $[o,sobj]\To sobj$    & singleton sequence    \\
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    40
  \cdx{Not}     & $o\To o$              & negation ($\neg$)     \\
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    41
  \cdx{True}    & $o$                   & tautology ($\top$)    \\
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    42
  \cdx{False}   & $o$                   & absurdity ($\bot$)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\begin{tabular}{llrrr} 
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    49
  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    50
  \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    51
        universal quantifier ($\forall$) \\
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    52
  \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    53
        existential quantifier ($\exists$) \\
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    54
  \sdx{THE} & \cdx{The}  & $(\alpha\To o)\To \alpha$ & 10 & 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    55
        definite description ($\iota$)
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\subcaption{Binders} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\begin{center}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    61
\index{*"= symbol}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    62
\index{&@{\tt\&} symbol}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    63
\index{*"| symbol}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    64
\index{*"-"-"> symbol}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    65
\index{*"<"-"> symbol}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\begin{tabular}{rrrr} 
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    67
    \it symbol  & \it meta-type         & \it priority & \it description \\ 
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
    68
    \tt = &     $[\alpha,\alpha]\To o$  & Left 50 & equality ($=$) \\
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
    \tt \& &    $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
    \tt | &     $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
    \tt --> &   $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
    \tt <-> &   $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\subcaption{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\begin{tabular}{rrr} 
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
    79
  \it external          & \it internal  & \it description \\ 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
  \tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
        sequent $\Gamma\turn \Delta$ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\subcaption{Translations} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\caption{Syntax of {\tt LK}} \label{lk-syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
\dquotes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
\[\begin{array}{rcl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
    prop & = & sequence " |- " sequence 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
sequence & = & elem \quad (", " elem)^* \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
         & | & empty 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\\[2ex]
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    97
    elem & = & "\$ " term \\
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    98
         & | & formula  \\
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
    99
         & | & "<<" sequence ">>" 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
 formula & = & \hbox{expression of type~$o$} \\
111
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   102
         & | & term " = " term \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   103
         & | & "\ttilde\ " 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
         & | & formula " | " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   106
         & | & formula " --> " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   107
         & | & formula " <-> " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   108
         & | & "ALL~" id~id^* " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   109
         & | & "EX~~" id~id^* " . " formula \\
1b3cddf41b2d Various updates for Isabelle-93
lcp
parents: 104
diff changeset
   110
         & | & "THE~" id~     " . " formula
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\caption{Grammar of {\tt LK}} \label{lk-grammar}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\begin{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   121
\tdx{basic}       $H, P, $G |- $E, P, $F
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   122
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   123
\tdx{contRS}      $H |- $E, $S, $S, $F ==> $H |- $E, $S, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   124
\tdx{contLS}      $H, $S, $S, $G |- $E ==> $H, $S, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   125
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   126
\tdx{thinRS}      $H |- $E, $F ==> $H |- $E, $S, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   127
\tdx{thinLS}      $H, $G |- $E ==> $H, $S, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   128
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   129
\tdx{cut}         [| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   130
\subcaption{Structural rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   132
\tdx{refl}        $H |- $E, a=a, $F
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   133
\tdx{subst}       $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   134
\subcaption{Equality rules}
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   135
\end{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   137
\caption{Basic Rules of {\tt LK}}  \label{lk-basic-rules}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   138
\end{figure}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   139
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   140
\begin{figure} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   141
\begin{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   142
\tdx{True_def}    True  == False-->False
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   143
\tdx{iff_def}     P<->Q == (P-->Q) & (Q-->P)
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   144
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   145
\tdx{conjR}   [| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   146
\tdx{conjL}   $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   148
\tdx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   149
\tdx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   150
            
841
14b96e3bd4ab fixed minor typos;
wenzelm
parents: 333
diff changeset
   151
\tdx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   152
\tdx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   153
            
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   154
\tdx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   155
\tdx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   157
\tdx{FalseL}  $H, False, $G |- $E
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   159
\tdx{allR}    (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   160
\tdx{allL}    $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   161
            
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   162
\tdx{exR}     $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   163
\tdx{exL}     (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   164
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   165
\tdx{The}     [| $H |- $E, P(a), $F;  !!x. $H, P(x) |- $E, x=a, $F |] ==>
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   166
        $H |- $E, P(THE x. P(x)), $F
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   167
\subcaption{Logical rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   170
\caption{Rules of {\tt LK}}  \label{lk-rules}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
\section{Syntax and rules of inference}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   175
\index{*sobj type}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   176
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
by the representation of sequents.  Type $sobj\To sobj$ represents a list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
of formulae.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   181
The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   182
satisfying~$P[a]$, if one exists and is unique.  Since all terms in \LK{}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
denote something, a description is always meaningful, but we do not know
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
its value unless $P[x]$ defines it uniquely.  The Isabelle notation is
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   185
\hbox{\tt THE $x$.\ $P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules})
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   186
does not entail the Axiom of Choice because it requires uniqueness.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   188
Conditional expressions are available with the notation 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   189
\[ \dquotes
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   190
   "if"~formula~"then"~term~"else"~term. \]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   191
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   192
Figure~\ref{lk-grammar} presents the grammar of \LK.  Traditionally,
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   193
\(\Gamma\) and \(\Delta\) are meta-variables for sequences.  In Isabelle's
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   194
notation, the prefix~\verb|$| on a term makes it range over sequences.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   195
In a sequent, anything not prefixed by \verb|$| is taken as a formula.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   197
The notation \texttt{<<$sequence$>>} stands for a sequence of formul\ae{}.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   198
For example, you can declare the constant \texttt{imps} to consist of two
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   199
implications: 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   200
\begin{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   201
consts     P,Q,R :: o
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   202
constdefs imps :: seq'=>seq'
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   203
         "imps == <<P --> Q, Q --> R>>"
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   204
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   205
Then you can use it in axioms and goals, for example
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   206
\begin{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   207
Goalw [imps_def] "P, $imps |- R";  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   208
{\out Level 0}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   209
{\out P, $imps |- R}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   210
{\out  1. P, P --> Q, Q --> R |- R}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   211
by (Fast_tac 1);
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   212
{\out Level 1}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   213
{\out P, $imps |- R}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   214
{\out No subgoals!}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   215
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   216
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   217
Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   218
\thydx{LK}.  The connective $\bimp$ is defined using $\conj$ and $\imp$.  The
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   219
axiom for basic sequents is expressed in a form that provides automatic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   220
thinning: redundant formulae are simply ignored.  The other rules are
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   221
expressed in the form most suitable for backward proof; exchange and
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   222
contraction rules are not normally required, although they are provided
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   223
anyway. 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   224
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   225
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   226
\begin{figure} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   227
\begin{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   228
\tdx{thinR}        $H |- $E, $F ==> $H |- $E, P, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   229
\tdx{thinL}        $H, $G |- $E ==> $H, P, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   230
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   231
\tdx{contR}        $H |- $E, P, P, $F ==> $H |- $E, P, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   232
\tdx{contL}        $H, P, P, $G |- $E ==> $H, P, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   233
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   234
\tdx{symR}         $H |- $E, $F, a=b ==> $H |- $E, b=a, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   235
\tdx{symL}         $H, $G, b=a |- $E ==> $H, a=b, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   236
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   237
\tdx{transR}       [| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   238
             ==> $H|- $E, a=c, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   239
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   240
\tdx{TrueR}        $H |- $E, True, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   241
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   242
\tdx{iffR}         [| $H, P |- $E, Q, $F;  $H, Q |- $E, P, $F |]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   243
             ==> $H |- $E, P<->Q, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   244
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   245
\tdx{iffL}         [| $H, $G |- $E, P, Q;  $H, Q, P, $G |- $E |]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   246
             ==> $H, P<->Q, $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   247
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   248
\tdx{allL_thin}    $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   249
\tdx{exR_thin}     $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   250
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   251
\tdx{the_equality} [| $H |- $E, P(a), $F;  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   252
                !!x. $H, P(x) |- $E, x=a, $F |] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   253
             ==> $H |- $E, (THE x. P(x)) = a, $F
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   254
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   255
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   256
\caption{Derived rules for {\tt LK}} \label{lk-derived}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   257
\end{figure}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
Figure~\ref{lk-derived} presents derived rules, including rules for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
$\bimp$.  The weakened quantifier rules discard each quantification after a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
single use; in an automatic proof procedure, they guarantee termination,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
but are incomplete.  Multiple use of a quantifier can be obtained by a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
contraction rule, which in backward proof duplicates a formula.  The tactic
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   264
{\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
specifying the formula to duplicate.
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   266
See theory {\tt Sequents/LK0} in the sources for complete listings of
3148
f081757ce757 tuned ref to src;
wenzelm
parents: 3137
diff changeset
   267
the rules and derived rules.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   269
To support the simplifier, hundreds of equivalences are proved for
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   270
the logical connectives and for if-then-else expressions.  See the file
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   271
\texttt{Sequents/simpdata.ML}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   273
\section{Automatic Proof}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   274
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   275
\LK{} instantiates Isabelle's simplifier.  Both equality ($=$) and the
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   276
biconditional ($\bimp$) may be used for rewriting.  The tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   277
\texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}).  With
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   278
sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   279
required; all the formulae{} in the sequent will be simplified.  The
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   280
left-hand formulae{} are taken as rewrite rules.  (Thus, the behaviour is what
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   281
you would normally expect from calling \texttt{Asm_full_simp_tac}.)
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   282
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   283
For classical reasoning, several tactics are available:
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   284
\begin{ttbox} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   285
Safe_tac : int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   286
Step_tac : int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   287
Fast_tac : int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   288
Best_tac : int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   289
Pc_tac   : int -> tactic
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   290
\end{ttbox}
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   291
These refer not to the standard classical reasoner but to a separate one
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   292
provided for the sequent calculus.  Two commands are available for adding new
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   293
sequent calculus rules, safe or unsafe, to the default ``theorem pack'':
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   294
\begin{ttbox} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   295
Add_safes   : thm list -> unit
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   296
Add_unsafes : thm list -> unit
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   297
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   298
To control the set of rules for individual invocations, lower-case versions of
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   299
all these primitives are available.  Sections~\ref{sec:thm-pack}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   300
and~\ref{sec:sequent-provers} give full details.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   301
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   302
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
\section{Tactics for the cut rule}
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   304
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
According to the cut-elimination theorem, the cut rule can be eliminated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
from proofs of sequents.  But the rule is still essential.  It can be used
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
to structure a proof into lemmas, avoiding repeated proofs of the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
formula.  More importantly, the cut rule can not be eliminated from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
derivations of rules.  For example, there is a trivial cut-free proof of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
the sequent \(P\conj Q\turn Q\conj P\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
Noting this, we might want to derive a rule for swapping the conjuncts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
in a right-hand formula:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
\[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
P$.  Most cuts directly involve a premise of the rule being derived (a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
meta-assumption).  In a few cases, the cut formula is not part of any
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
premise, but serves as a bridge between the premises and the conclusion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
In such proofs, the cut formula is specified by calling an appropriate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
cutR_tac : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
cutL_tac : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
These tactics refine a subgoal into two by applying the cut rule.  The cut
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
formula is given as a string, and replaces some other formula in the sequent.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   327
\begin{ttdescription}
264
ca6eb7e6e94f correction to cut tactics
lcp
parents: 111
diff changeset
   328
\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
then deletes some formula from the right side of subgoal~$i$, replacing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
that formula by~$P$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
264
ca6eb7e6e94f correction to cut tactics
lcp
parents: 111
diff changeset
   333
\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
291
a615050a7494 first draft of Springer volume
lcp
parents: 264
diff changeset
   335
then deletes some formula from the left side of the new subgoal $i+1$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
replacing that formula by~$P$.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   337
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
All the structural rules --- cut, contraction, and thinning --- can be
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   339
applied to particular formulae using {\tt res_inst_tac}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
\section{Tactics for sequents}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
forms_of_seq       : term -> term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
could_res          : term * term -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
could_resolve_seq  : term * term -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
filseq_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
Associative unification is not as efficient as it might be, in part because
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
the representation of lists defeats some of Isabelle's internal
333
2ca08f62df33 final Springer copy
lcp
parents: 316
diff changeset
   351
optimisations.  The following operations implement faster rule application,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
and may have other uses.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   353
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\item[\ttindexbold{forms_of_seq} {\it t}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
returns the list of all formulae in the sequent~$t$, removing sequence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   358
\item[\ttindexbold{could_res} ($t$,$u$)] 
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
tests whether two formula lists could be resolved.  List $t$ is from a
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   360
premise or subgoal, while $u$ is from the conclusion of an object-rule.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
Assuming that each formula in $u$ is surrounded by sequence variables, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
checks that each conclusion formula is unifiable (using {\tt could_unify})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
with some subgoal formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   365
\item[\ttindexbold{could_resolve_seq} ($t$,$u$)] 
291
a615050a7494 first draft of Springer volume
lcp
parents: 264
diff changeset
   366
  tests whether two sequents could be resolved.  Sequent $t$ is a premise
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   367
  or subgoal, while $u$ is the conclusion of an object-rule.  It simply
291
a615050a7494 first draft of Springer volume
lcp
parents: 264
diff changeset
   368
  calls {\tt could_res} twice to check that both the left and the right
a615050a7494 first draft of Springer volume
lcp
parents: 264
diff changeset
   369
  sides of the sequents are compatible.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
\item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
applicable to subgoal~$i$.  If more than {\it maxr\/} theorems are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
applicable then the tactic fails.  Otherwise it calls {\tt resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   376
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
\section{A simple example of classical reasoning} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
classical treatment of the existential quantifier.  Classical reasoning
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
is easy using~{\LK}, as you can see by comparing this proof with the one
6072
5583261db33d removal of FOL, ZF to a separate manual
paulson
parents: 5151
diff changeset
   383
given in the FOL manual~\cite{isabelle-ZF}.  From a logical point of view, the
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   384
proofs are essentially the same; the key step here is to use \tdx{exR}
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   385
rather than the weaker~\tdx{exR_thin}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\begin{ttbox}
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   387
Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
{\out  1.  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
by (resolve_tac [exR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
{\out  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
There are now two formulae on the right side.  Keeping the existential one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
in reserve, we break down the universal one.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
{\out  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
{\out  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
become an assumption;  instead, it moves to the left side.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
resulting subgoal cannot be instantiated to a basic sequent: the bound
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
variable~$x$ is not unifiable with the unknown~$\Var{x}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
{\out by: tactic failed}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\end{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   416
We reuse the existential formula using~\tdx{exR_thin}, which discards
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   417
it; we shall not need it a third time.  We again break down the resulting
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
by (resolve_tac [exR_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
{\out  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
{\out  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
{\out  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   434
step is instantiating~$\Var{x@7}$ to $\lambda x. x$,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
transforming~$\Var{x@7}(x)$ into~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
This theorem can be proved automatically.  Because it involves quantifier
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
duplication, we employ best-first search:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
\begin{ttbox}
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   445
Goal "|- EX y. ALL x. P(y)-->P(x)";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
{\out  1.  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
by (best_tac LK_dup_pack 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
\section{A more complex proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
Many of Pelletier's test problems for theorem provers \cite{pelletier86}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
can be solved automatically.  Problem~39 concerns set theory, asserting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
that there is no Russell set --- a set consisting of those sets that are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
not members of themselves:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
\[  \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   463
This does not require special properties of membership; we may generalize
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   464
$x\in y$ to an arbitrary predicate~$F(x,y)$.  The theorem, which is trivial
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   465
for \texttt{Fast_tac}, has a short manual proof.  See the directory {\tt
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   466
  Sequents/LK} for many more examples.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
We set the main goal and move the negated formula to the left.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\begin{ttbox}
5151
1e944fe5ce96 Got rid of obsolete "goal" commands.
paulson
parents: 3148
diff changeset
   470
Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
{\out  1.  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
{\out  1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
The right side is empty; we strip both quantifiers from the formula on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
left.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\begin{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   482
by (resolve_tac [exL] 1);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
{\out  1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
by (resolve_tac [allL_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
{\out  1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
\end{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   491
The rule \tdx{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
both true or both false.  It yields two subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
by (resolve_tac [iffL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
{\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
{\out  2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
subgoals.  Beginning with subgoal~2, we move a negated formula to the left
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
and create a basic sequent.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
by (resolve_tac [notL] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
{\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
{\out  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
by (resolve_tac [basic] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
{\out  1. !!x.  |- F(x,x), ~ F(x,x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
{\out  1. !!x. F(x,x) |- F(x,x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
{\out Level 8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
\end{ttbox}
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   525
7116
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   526
\section{*Unification for lists}\label{sec:assoc-unification}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   527
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   528
Higher-order unification includes associative unification as a special
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   529
case, by an encoding that involves function composition
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   530
\cite[page~37]{huet78}.  To represent lists, let $C$ be a new constant.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   531
The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   532
represented by
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   533
\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))).  \]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   534
The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   535
of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   536
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   537
Unlike orthodox associative unification, this technique can represent certain
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   538
infinite sets of unifiers by flex-flex equations.   But note that the term
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   539
$\lambda x. C(t,\Var{a})$ does not represent any list.  Flex-flex constraints
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   540
containing such garbage terms may accumulate during a proof.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   541
\index{flex-flex constraints}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   542
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   543
This technique lets Isabelle formalize sequent calculus rules,
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   544
where the comma is the associative operator:
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   545
\[ \infer[(\conj\hbox{-left})]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   546
         {\Gamma,P\conj Q,\Delta \turn \Theta}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   547
         {\Gamma,P,Q,\Delta \turn \Theta}  \] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   548
Multiple unifiers occur whenever this is resolved against a goal containing
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   549
more than one conjunction on the left.  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   550
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   551
\LK{} exploits this representation of lists.  As an alternative, the
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   552
sequent calculus can be formalized using an ordinary representation of
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   553
lists, with a logic program for removing a formula from a list.  Amy Felty
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   554
has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   555
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   556
Explicit formalization of sequents can be tiresome.  But it gives precise
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   557
control over contraction and weakening, and is essential to handle relevant
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   558
and linear logics.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   559
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   560
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   561
\section{*Packaging sequent rules}\label{sec:thm-pack}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   562
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   563
The sequent calculi come with simple proof procedures.  These are incomplete
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   564
but are reasonably powerful for interactive use.  They expect rules to be
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   565
classified as \textbf{safe} or \textbf{unsafe}.  A rule is safe if applying it to a
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   566
provable goal always yields provable subgoals.  If a rule is safe then it can
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   567
be applied automatically to a goal without destroying our chances of finding a
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   568
proof.  For instance, all the standard rules of the classical sequent calculus
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   569
{\sc lk} are safe.  An unsafe rule may render the goal unprovable; typical
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   570
examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   571
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   572
Proof procedures use safe rules whenever possible, using an unsafe rule as a
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   573
last resort.  Those safe rules are preferred that generate the fewest
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   574
subgoals.  Safe rules are (by definition) deterministic, while the unsafe
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   575
rules require a search strategy, such as backtracking.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   576
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   577
A \textbf{pack} is a pair whose first component is a list of safe rules and
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   578
whose second is a list of unsafe rules.  Packs can be extended in an
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   579
obvious way to allow reasoning with various collections of rules.  For
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   580
clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   581
essentially a type synonym:
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   582
\begin{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   583
datatype pack = Pack of thm list * thm list;
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   584
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   585
Pattern-matching using constructor {\tt Pack} can inspect a pack's
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   586
contents.  Packs support the following operations:
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   587
\begin{ttbox} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   588
pack        : unit -> pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   589
pack_of     : theory -> pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   590
empty_pack  : pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   591
prop_pack   : pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   592
LK_pack     : pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   593
LK_dup_pack : pack
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   594
add_safes   : pack * thm list -> pack               \hfill\textbf{infix 4}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   595
add_unsafes : pack * thm list -> pack               \hfill\textbf{infix 4}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   596
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   597
\begin{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   598
\item[\ttindexbold{pack}] returns the pack attached to the current theory.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   599
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   600
\item[\ttindexbold{pack_of $thy$}] returns the pack attached to theory $thy$.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   601
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   602
\item[\ttindexbold{empty_pack}] is the empty pack.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   603
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   604
\item[\ttindexbold{prop_pack}] contains the propositional rules, namely
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   605
those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   606
rules {\tt basic} and {\tt refl}.  These are all safe.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   607
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   608
\item[\ttindexbold{LK_pack}] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   609
extends {\tt prop_pack} with the safe rules {\tt allR}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   610
and~{\tt exL} and the unsafe rules {\tt allL_thin} and
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   611
{\tt exR_thin}.  Search using this is incomplete since quantified
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   612
formulae are used at most once.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   613
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   614
\item[\ttindexbold{LK_dup_pack}] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   615
extends {\tt prop_pack} with the safe rules {\tt allR}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   616
and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   617
Search using this is complete, since quantified formulae may be reused, but
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   618
frequently fails to terminate.  It is generally unsuitable for depth-first
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   619
search.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   620
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   621
\item[$pack$ \ttindexbold{add_safes} $rules$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   622
adds some safe~$rules$ to the pack~$pack$.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   623
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   624
\item[$pack$ \ttindexbold{add_unsafes} $rules$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   625
adds some unsafe~$rules$ to the pack~$pack$.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   626
\end{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   627
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   628
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   629
\section{*Proof procedures}\label{sec:sequent-provers}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   630
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   631
The \LK{} proof procedure is similar to the classical reasoner
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   632
described in 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   633
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   634
            {Chap.\ts\ref{chap:classical}}.  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   635
%
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   636
In fact it is simpler, since it works directly with sequents rather than
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   637
simulating them.  There is no need to distinguish introduction rules from
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   638
elimination rules, and of course there is no swap rule.  As always,
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   639
Isabelle's classical proof procedures are less powerful than resolution
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   640
theorem provers.  But they are more natural and flexible, working with an
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   641
open-ended set of rules.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   642
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   643
Backtracking over the choice of a safe rule accomplishes nothing: applying
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   644
them in any order leads to essentially the same result.  Backtracking may
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   645
be necessary over basic sequents when they perform unification.  Suppose
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   646
that~0, 1, 2,~3 are constants in the subgoals
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   647
\[  \begin{array}{c}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   648
      P(0), P(1), P(2) \turn P(\Var{a})  \\
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   649
      P(0), P(2), P(3) \turn P(\Var{a})  \\
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   650
      P(1), P(3), P(2) \turn P(\Var{a})  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   651
    \end{array}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   652
\]
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   653
The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   654
and this can only be discovered by search.  The tactics given below permit
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   655
backtracking only over axioms, such as {\tt basic} and {\tt refl};
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   656
otherwise they are deterministic.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   657
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   658
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   659
\subsection{Method A}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   660
\begin{ttbox} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   661
reresolve_tac   : thm list -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   662
repeat_goal_tac : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   663
pc_tac          : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   664
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   665
These tactics use a method developed by Philippe de Groote.  A subgoal is
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   666
refined and the resulting subgoals are attempted in reverse order.  For
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   667
some reason, this is much faster than attempting the subgoals in order.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   668
The method is inherently depth-first.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   669
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   670
At present, these tactics only work for rules that have no more than two
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   671
premises.  They fail --- return no next state --- if they can do nothing.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   672
\begin{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   673
\item[\ttindexbold{reresolve_tac} $thms$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   674
repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   675
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   676
\item[\ttindexbold{repeat_goal_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   677
applies the safe rules in the pack to a goal and the resulting subgoals.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   678
If no safe rule is applicable then it applies an unsafe rule and continues.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   679
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   680
\item[\ttindexbold{pc_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   681
applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   682
\end{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   683
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   684
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   685
\subsection{Method B}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   686
\begin{ttbox} 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   687
safe_tac : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   688
step_tac : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   689
fast_tac : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   690
best_tac : pack -> int -> tactic
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   691
\end{ttbox}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   692
These tactics are analogous to those of the generic classical
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   693
reasoner.  They use `Method~A' only on safe rules.  They fail if they
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   694
can do nothing.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   695
\begin{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   696
\item[\ttindexbold{safe_goal_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   697
applies the safe rules in the pack to a goal and the resulting subgoals.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   698
It ignores the unsafe rules.  
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   699
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   700
\item[\ttindexbold{step_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   701
either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   702
rule.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   703
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   704
\item[\ttindexbold{fast_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   705
applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   706
Despite its name, it is frequently slower than {\tt pc_tac}.
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   707
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   708
\item[\ttindexbold{best_tac} $pack$ $i$] 
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   709
applies {\tt step_tac} using best-first search to solve subgoal~$i$.  It is
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   710
particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   711
\end{ttdescription}
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   712
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   713
8c1caac3e54e simplifier and improved classical reasoner
paulson
parents: 6072
diff changeset
   714
316
813ee27cd4d5 penultimate Springer draft
lcp
parents: 291
diff changeset
   715
\index{sequent calculus|)}