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} `