doc-src/Logics/LK.tex
author lcp
Wed, 10 Nov 1993 05:00:57 +0100
changeset 104 d8205bb279a7
child 111 1b3cddf41b2d
permissions -rw-r--r--
Initial revision
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 sequent calculus}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
The directory~\ttindexbold{LK} implements classical first-order logic through
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
Gentzen's sequent calculus (see Gallier~\cite{gallier86} or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
Takeuti~\cite{takeuti87}).  Resembling the method of semantic tableaux, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
calculus is well suited for backwards proof.  Assertions have the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
\(\Gamma\turn \Delta\), where \(\Gamma\) and \(\Delta\) are lists of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
formulae.  Associative unification, simulated by higher-order unification,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
handles lists.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
The logic is many-sorted, using Isabelle's type classes.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
class of first-order terms is called {\it term}.  No types of individuals
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
are provided, but extensions can define types such as $nat::term$ and type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
constructors such as $list::(term)term$.  Below, the type variable $\alpha$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
ranges over class {\it term\/}; the equality symbol and quantifiers are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
polymorphic (many-sorted).  The type of formulae is~{\it o}, which belongs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
to class {\it logic}.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
No generic packages are instantiated, since Isabelle does not provide
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
packages for sequent calculi at present.  \LK{} implements a classical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
logic theorem prover that is as powerful as the generic classical module,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
except that it does not perform equality reasoning.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
\section{Unification for lists}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
Higher-order unification includes associative unification as a special
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
case, by an encoding that involves function composition
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\cite[page~37]{huet78}.  To represent lists, let $C$ be a new constant.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
The empty list is $\lambda x.x$, while $[t@1,t@2,\ldots,t@n]$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
represented by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\[ \lambda x.C(t@1,C(t@2,\ldots,C(t@n,x))).  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
Unlike orthodox associative unification, this technique can represent certain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
infinite sets of unifiers by flex-flex equations.   But note that the term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
$\lambda x.C(t,\Var{a})$ does not represent any list.  Flex-flex equations
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
containing such garbage terms may accumulate during a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
This technique lets Isabelle formalize sequent calculus rules,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
where the comma is the associative operator:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\[ \infer[\conj\hbox{-left}]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
	 {\Gamma,P\conj Q,\Delta \turn \Theta}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
         {\Gamma,P,Q,\Delta \turn \Theta}  \] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
Multiple unifiers occur whenever this is resolved against a goal containing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
more than one conjunction on the left.  Explicit formalization of sequents
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
can be tiresome, but gives precise control over contraction and weakening,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
needed to handle relevant and linear logics.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\LK{} exploits this representation of lists.  As an alternative, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
sequent calculus can be formalized using an ordinary representation of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
lists, with a logic program for removing a formula from a list.  Amy Felty
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
\begin{tabular}{rrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
  \it name    	&\it meta-type 		& \it description	\\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
  \idx{Trueprop}& $o\To prop$		& coercion to $prop$	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
  \idx{Seqof}   & $[o,sobj]\To sobj$  	& singleton sequence	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
  \idx{Not}	& $o\To o$		& negation ($\neg$) 	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
  \idx{True}	& $o$			& tautology ($\top$) 	\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
  \idx{False}	& $o$			& absurdity ($\bot$)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\subcaption{Constants}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\begin{tabular}{llrrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
  \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
  \idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
	universal quantifier ($\forall$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
  \idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
	existential quantifier ($\exists$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
  \idx{THE} & \idx{The}  & $(\alpha\To o)\To \alpha$ & 10 & 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
	definite description ($\iota$)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\subcaption{Binders} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\indexbold{*"=}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\indexbold{&@{\tt\&}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\indexbold{*"|}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\indexbold{*"-"-">}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\indexbold{*"<"-">}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
\begin{tabular}{rrrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
    \it symbol  & \it meta-type & \it precedence & \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
    \tt = &     $[\alpha,\alpha]\To o$   & Left 50 & equality ($=$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
    \tt \& &    $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
    \tt | &     $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
    \tt --> &   $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
    \tt <-> &   $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\subcaption{Infixes}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\begin{tabular}{rrr} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
  \it external		& \it internal	& \it description \\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
  \tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
        sequent $\Gamma\turn \Delta$ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\subcaption{Translations} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
\caption{Syntax of {\tt LK}} \label{lk-syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
\dquotes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\[\begin{array}{rcl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
    prop & = & sequence " |- " sequence 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
\\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
sequence & = & elem \quad (", " elem)^* \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
         & | & empty 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
    elem & = & "\$ " id \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
         & | & "\$ " var \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
         & | & formula 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\\[2ex]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
 formula & = & \hbox{expression of type~$o$} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
	 & | & term " = " term \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
	 & | & "\ttilde\ " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
	 & | & formula " \& " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
	 & | & formula " | " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
	 & | & formula " --> " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
	 & | & formula " <-> " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
	 & | & "ALL~" id~id^* " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
	 & | & "EX~~" id~id^* " . " formula \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
	 & | & "THE~" id~     " . " formula
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
  \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
\caption{Grammar of {\tt LK}} \label{lk-grammar}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
\idx{basic}       $H, P, $G |- $E, P, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\idx{thinR}       $H |- $E, $F ==> $H |- $E, P, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\idx{thinL}       $H, $G |- $E ==> $H, P, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\idx{cut}         [| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
\subcaption{Structural rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\idx{refl}        $H |- $E, a=a, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
\idx{sym}         $H |- $E, a=b, $F ==> $H |- $E, b=a, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\idx{trans}       [| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
            $H|- $E, a=c, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
\subcaption{Equality rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\idx{True_def}    True  == False-->False
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
\idx{iff_def}     P<->Q == (P-->Q) & (Q-->P)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\idx{conjR}   [| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\idx{conjL}   $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\idx{disjR}   $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
\idx{disjL}   [| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
            
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\idx{impR}    $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\idx{impL}    [| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
            
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
\idx{notR}    $H, P |- $E, $F ==> $H |- $E, ~P, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
\idx{notL}    $H, $G |- $E, P ==> $H, ~P, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
\idx{FalseL}  $H, False, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
\subcaption{Propositional rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
\idx{allR}    (!!x.$H|- $E, P(x), $F) ==> $H|- $E, ALL x.P(x), $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
\idx{allL}    $H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G|- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
            
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
\idx{exR}     $H|- $E, P(x), $F, EX x.P(x) ==> $H|- $E, EX x.P(x), $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
\idx{exL}     (!!x.$H, P(x), $G|- $E) ==> $H, EX x.P(x), $G|- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
\idx{The}     [| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
        $H |- $E, P(THE x.P(x)), $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
\subcaption{Quantifier rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
\caption{Rules of {\tt LK}}  \label{lk-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\begin{figure} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
\idx{conR}        $H |- $E, P, $F, P ==> $H |- $E, P, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\idx{conL}        $H, P, $G, P |- $E ==> $H, P, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
\idx{symL}        $H, $G, B = A |- $E ==> $H, A = B, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
\idx{TrueR}       $H |- $E, True, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
\idx{iffR}        [| $H, P |- $E, Q, $F;  $H, Q |- $E, P, $F |] ==> 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
            $H |- $E, P<->Q, $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
\idx{iffL}        [| $H, $G |- $E, P, Q;  $H, Q, P, $G |- $E |] ==>
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
            $H, P<->Q, $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
\idx{allL_thin}   $H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
\idx{exR_thin}    $H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\caption{Derived rules for {\tt LK}} \label{lk-derived}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
\section{Syntax and rules of inference}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
by the representation of sequents.  Type $sobj\To sobj$ represents a list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
of formulae.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
The {\bf definite description} operator~$\iota x.P(x)$ stands for the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
unique~$a$ satisfying~$P(a)$, if such exists.  Since all terms in \LK{}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
denote something, a description is always meaningful, but we do not know
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
its value unless $P[x]$ defines it uniquely.  The Isabelle notation is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\hbox{\tt THE $x$.$P[x]$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
Traditionally, \(\Gamma\) and \(\Delta\) are meta-variables for sequences.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
In Isabelle's notation, the prefix~\verb|$| on a variable makes it range
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
over sequences.  In a sequent, anything not prefixed by \verb|$| is taken
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
as a formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
The theory has the \ML\ identifier \ttindexbold{LK.thy}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
Figure~\ref{lk-rules} presents the rules.  The connective $\bimp$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
defined using $\conj$ and $\imp$.  The axiom for basic sequents is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
expressed in a form that provides automatic thinning: redundant formulae
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
are simply ignored.  The other rules are expressed in the form most
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
suitable for backward proof --- they do not require exchange or contraction
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
rules.  The contraction rules are actually derivable (via cut) in this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
formulation.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
Figure~\ref{lk-derived} presents derived rules, including rules for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
$\bimp$.  The weakened quantifier rules discard each quantification after a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
single use; in an automatic proof procedure, they guarantee termination,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
but are incomplete.  Multiple use of a quantifier can be obtained by a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
contraction rule, which in backward proof duplicates a formula.  The tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
\ttindex{res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
specifying the formula to duplicate.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
See the files \ttindexbold{LK/lk.thy} and \ttindexbold{LK/lk.ML}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
for complete listings of the rules and derived rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
\section{Tactics for the cut rule}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
According to the cut-elimination theorem, the cut rule can be eliminated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
from proofs of sequents.  But the rule is still essential.  It can be used
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
to structure a proof into lemmas, avoiding repeated proofs of the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
formula.  More importantly, the cut rule can not be eliminated from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
derivations of rules.  For example, there is a trivial cut-free proof of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
the sequent \(P\conj Q\turn Q\conj P\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
Noting this, we might want to derive a rule for swapping the conjuncts
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
in a right-hand formula:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
P$.  Most cuts directly involve a premise of the rule being derived (a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
meta-assumption).  In a few cases, the cut formula is not part of any
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
premise, but serves as a bridge between the premises and the conclusion.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
In such proofs, the cut formula is specified by calling an appropriate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
tactic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
cutR_tac : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
cutL_tac : string -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
These tactics refine a subgoal into two by applying the cut rule.  The cut
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
formula is given as a string, and replaces some other formula in the sequent.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\item[\ttindexbold{cutR_tac} {\it formula} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
then deletes some formula from the right side of subgoal~$i$, replacing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
that formula by~$P$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
\item[\ttindexbold{cutL_tac} {\it formula} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$.  It
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
then deletes some formula from the let side of the new subgoal $i+1$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
replacing that formula by~$P$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
All the structural rules --- cut, contraction, and thinning --- can be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
applied to particular formulae using \ttindex{res_inst_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
\section{Tactics for sequents}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
forms_of_seq       : term -> term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
could_res          : term * term -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
could_resolve_seq  : term * term -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
filseq_resolve_tac : thm list -> int -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
Associative unification is not as efficient as it might be, in part because
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
the representation of lists defeats some of Isabelle's internal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
optimizations.  The following operations implement faster rule application,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
and may have other uses.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
\item[\ttindexbold{forms_of_seq} {\it t}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
returns the list of all formulae in the sequent~$t$, removing sequence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
\item[\ttindexbold{could_res} $(t,u)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
tests whether two formula lists could be resolved.  List $t$ is from a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
premise (subgoal), while $u$ is from the conclusion of an object-rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
Assuming that each formula in $u$ is surrounded by sequence variables, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
checks that each conclusion formula is unifiable (using {\tt could_unify})
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
with some subgoal formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
\item[\ttindexbold{could_resolve} $(t,u)$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
tests whether two sequents could be resolved.  Sequent $t$ is a premise
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
(subgoal), while $u$ is the conclusion of an object-rule.  It uses {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
could_res} to check the left and right sides of the two sequents.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
\item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
applicable to subgoal~$i$.  If more than {\it maxr\/} theorems are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
applicable then the tactic fails.  Otherwise it calls {\tt resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\section{Packaging sequent rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
For theorem proving, rules can be classified as {\bf safe} or {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
unsafe}.  An unsafe rule (typically a weakened quantifier rule) may reduce
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
a provable goal to an unprovable set of subgoals, and should only be used
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
as a last resort.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
A {\bf pack} is a pair whose first component is a list of safe
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
rules, and whose second is a list of unsafe rules.  Packs can be extended
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
in an obvious way to allow reasoning with various collections of rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
For clarity, \LK{} declares the datatype
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
\ttindexbold{pack}:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
datatype pack = Pack of thm list * thm list;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
The contents of any pack can be inspected by pattern-matching.  Packs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
support the following operations:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
empty_pack  : pack
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
prop_pack   : pack
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
LK_pack     : pack
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
LK_dup_pack : pack
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
add_safes   : pack * thm list -> pack               \hfill{\bf infix 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
add_unsafes : pack * thm list -> pack               \hfill{\bf infix 4}
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{empty_pack}] is the empty pack.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\item[\ttindexbold{prop_pack}] contains the propositional rules, namely
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
rules \ttindex{basic} and \ttindex{refl}.  These are all safe.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
\item[\ttindexbold{LK_pack}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
extends {\tt prop_pack} with the safe rules \ttindex{allR}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
and~\ttindex{exL} and the unsafe rules \ttindex{allL_thin} and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\ttindex{exR_thin}.  Search using this is incomplete since quantified
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
formulae are used at most once.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
\item[\ttindexbold{LK_dup_pack}] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
extends {\tt prop_pack} with the safe rules \ttindex{allR}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
and~\ttindex{exL} and the unsafe rules \ttindex{allL} and~\ttindex{exR}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
Search using this is complete, since quantified formulae may be reused, but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
frequently fails to terminate.  It is generally unsuitable for depth-first
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
search.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
\item[$pack$ \ttindexbold{add_safes} $rules$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
adds some safe~$rules$ to the pack~$pack$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
\item[$pack$ \ttindexbold{add_unsafes} $rules$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
adds some unsafe~$rules$ to the pack~$pack$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
\section{Proof procedures}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
The \LK{} proof procedure is similar to the generic classical module
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
described in the {\em Reference Manual}.  In fact it is simpler, since it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
works directly with sequents rather than simulating them.  There is no need
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
to distinguish introduction rules from elimination rules, and of course
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
there is no swap rule.  As always, Isabelle's classical proof procedures
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
are less powerful than resolution theorem provers.  But they are more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
natural and flexible, working with an open-ended set of rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
Backtracking over the choice of a safe rule accomplishes nothing: applying
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
them in any order leads to essentially the same result.  Backtracking may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
be necessary over basic sequents when they perform unification.  Suppose
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
that~0, 1, 2,~3 are constants in the subgoals
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
\[  \begin{array}{c}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
      P(0), P(1), P(2) \turn P(\Var{a})  \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
      P(0), P(2), P(3) \turn P(\Var{a})  \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
      P(1), P(3), P(2) \turn P(\Var{a})  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
    \end{array}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
and this can only be discovered by search.  The tactics given below permit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
backtracking only over axioms, such as {\tt basic} and {\tt refl}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
\subsection{Method A}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
reresolve_tac   : thm list -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
repeat_goal_tac : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
pc_tac          : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
These tactics use a method developed by Philippe de Groote.  A subgoal is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
refined and the resulting subgoals are attempted in reverse order.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
some reason, this is much faster than attempting the subgoals in order.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
The method is inherently depth-first.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
At present, these tactics only work for rules that have no more than two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
premises.  They {\bf fail} if they can do nothing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
\item[\ttindexbold{reresolve_tac} $thms$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
\item[\ttindexbold{repeat_goal_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
applies the safe rules in the pack to a goal and the resulting subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
If no safe rule is applicable then it applies an unsafe rule and continues.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
\item[\ttindexbold{pc_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\subsection{Method B}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
safe_goal_tac : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
step_tac      : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
fast_tac      : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
best_tac      : pack -> int -> tactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
These tactics are precisely analogous to those of the generic classical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
module.  They use `Method~A' only on safe rules.  They {\bf fail} if they
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
can do nothing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
\item[\ttindexbold{safe_goal_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
applies the safe rules in the pack to a goal and the resulting subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
It ignores the unsafe rules.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
\item[\ttindexbold{step_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
rule.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
\item[\ttindexbold{fast_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
Despite the names, {\tt pc_tac} is frequently faster.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
\item[\ttindexbold{best_tac} $pack$ $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
applies {\tt step_tac} using best-first search to solve subgoal~$i$.  It is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
\section{A simple example of classical reasoning} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
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
   455
classical treatment of the existential quantifier.  Classical reasoning
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
is easy using~{\LK}, as you can see by comparing this proof with the one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
given in~\S\ref{fol-cla-example}.  From a logical point of view, the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
proofs are essentially the same; the key step here is to use \ttindex{exR}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
rather than the weaker~\ttindex{exR_thin}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
{\out  1.  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
by (resolve_tac [exR] 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. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
{\out  1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
There are now two formulae on the right side.  Keeping the existential one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
in reserve, we break down the universal one.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
{\out  1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
{\out  1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
become an assumption;  instead, it moves to the left side.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
resulting subgoal cannot be instantiated to a basic sequent: the bound
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
variable~$x$ is not unifiable with the unknown~$\Var{x}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
{\out by: tactic failed}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
We reuse the existential formula using~\ttindex{exR_thin}, which discards
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
it; we will not need it a third time.  We again break down the resulting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
formula.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
by (resolve_tac [exR_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
{\out  1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
by (resolve_tac [allR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
{\out  1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
by (resolve_tac [impR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
{\out  1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
step is instantiating~$\Var{x@7}$ to $\lambda x.x$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
transforming~$\Var{x@7}(x)$ into~$x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
This theorem can be proved automatically.  Because it involves quantifier
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
duplication, we employ best-first search:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
{\out  1.  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
by (best_tac LK_dup_pack 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
{\out  |- EX y. ALL x. P(y) --> P(x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
\section{A more complex proof}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
Many of Pelletier's test problems for theorem provers \cite{pelletier86}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
can be solved automatically.  Problem~39 concerns set theory, asserting
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
that there is no Russell set --- a set consisting of those sets that are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
not members of themselves:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
\[  \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
This does not require special properties of membership; we may
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
generalize $x\in y$ to an arbitrary predicate~$F(x,y)$.  The theorem has a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
short manual proof.  See the directory \ttindexbold{LK/ex} for many more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
examples.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
We set the main goal and move the negated formula to the left.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
{\out  1.  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
{\out  1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
by (resolve_tac [exL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
The right side is empty; we strip both quantifiers from the formula on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
left.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
{\out  1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
by (resolve_tac [allL_thin] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
{\out  1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
The rule \ttindex{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
both true or both false.  It yields two subgoals.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
by (resolve_tac [iffL] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
{\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
{\out  2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
subgoals.  Beginning with subgoal~2, we move a negated formula to the left
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
and create a basic sequent.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
by (resolve_tac [notL] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
{\out  1. !!x.  |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
{\out  2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
by (resolve_tac [basic] 2);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
{\out Level 6}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
{\out  1. !!x.  |- F(x,x), ~ F(x,x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
by (resolve_tac [notR] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
{\out Level 7}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
{\out  1. !!x. F(x,x) |- F(x,x)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
by (resolve_tac [basic] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
{\out Level 8}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
{\out  |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
\end{ttbox}