doc-src/Logics/LK.tex
 author paulson Wed, 28 Jul 1999 13:42:20 +0200 changeset 7116 8c1caac3e54e parent 6072 5583261db33d child 9695 ec7d7f877712 permissions -rw-r--r--
simplifier and improved classical reasoner
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 104 d8205bb279a7 Initial revision lcp parents: diff changeset  1 %% $Id$  291 a615050a7494 first draft of Springer volume lcp parents: 264 diff changeset  2 \chapter{First-Order Sequent Calculus}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  3 \index{sequent calculus|(}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  4 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  5 The theory~\thydx{LK} implements classical first-order logic through Gentzen's  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  6 sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  7 Resembling the method of semantic tableaux, the calculus is well suited for  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  8 backwards proof. Assertions have the form $$\Gamma\turn \Delta$$, where  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  9 $$\Gamma$$ and $$\Delta$$ are lists of formulae. Associative unification,  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  10 simulated by higher-order unification, handles lists  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  11 (\S\ref{sec:assoc-unification} presents details, if you are interested).  104 d8205bb279a7 Initial revision lcp parents: diff changeset  12 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  13 The logic is many-sorted, using Isabelle's type classes. The class of  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  14 first-order terms is called \cldx{term}. No types of individuals are  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  15 provided, but extensions can define types such as {\tt nat::term} and type  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  16 constructors such as {\tt list::(term)term}. Below, the type variable  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  17 $\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  18 are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  19 belongs to class {\tt logic}.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  20 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  21 \LK{} implements a classical logic theorem prover that is nearly as powerful  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  22 as the generic classical reasoner. The simplifier is now available too.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  23 5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  24 To work in LK, start up Isabelle specifying \texttt{Sequents} as the  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  25 object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  26 \begin{ttbox}  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  27 isabelle Sequents  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  28 context LK.thy;  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  29 \end{ttbox}  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  30 Model logic and linear logic are also available, but unfortunately they are  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  31 not documented.  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  32 104 d8205bb279a7 Initial revision lcp parents: diff changeset  33 d8205bb279a7 Initial revision lcp parents: diff changeset  34 \begin{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  35 \begin{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  36 \begin{tabular}{rrr}  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  37  \it name &\it meta-type & \it description \\  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  38  \cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  39  \cdx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  40  \cdx{Not} & $o\To o$ & negation ($\neg$) \\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  41  \cdx{True} & $o$ & tautology ($\top$) \\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  42  \cdx{False} & $o$ & absurdity ($\bot$)  104 d8205bb279a7 Initial revision lcp parents: diff changeset  43 \end{tabular}  d8205bb279a7 Initial revision lcp parents: diff changeset  44 \end{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  45 \subcaption{Constants}  d8205bb279a7 Initial revision lcp parents: diff changeset  46 d8205bb279a7 Initial revision lcp parents: diff changeset  47 \begin{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  48 \begin{tabular}{llrrr}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  49  \it symbol &\it name &\it meta-type & \it priority & \it description \\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  50  \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  51  universal quantifier ($\forall$) \\  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  52  \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  53  existential quantifier ($\exists$) \\  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  54  \sdx{THE} & \cdx{The} & $(\alpha\To o)\To \alpha$ & 10 &  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  55  definite description ($\iota$)  104 d8205bb279a7 Initial revision lcp parents: diff changeset  56 \end{tabular}  d8205bb279a7 Initial revision lcp parents: diff changeset  57 \end{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  58 \subcaption{Binders}  d8205bb279a7 Initial revision lcp parents: diff changeset  59 d8205bb279a7 Initial revision lcp parents: diff changeset  60 \begin{center}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  61 \index{*"= symbol}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  62 \index{&@{\tt\&} symbol}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  63 \index{*"| symbol}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  64 \index{*"-"-"> symbol}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  65 \index{*"<"-"> symbol}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  66 \begin{tabular}{rrrr}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  67  \it symbol & \it meta-type & \it priority & \it description \\  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  68  \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\  104 d8205bb279a7 Initial revision lcp parents: diff changeset  69  \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\  d8205bb279a7 Initial revision lcp parents: diff changeset  70  \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\  d8205bb279a7 Initial revision lcp parents: diff changeset  71  \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\  d8205bb279a7 Initial revision lcp parents: diff changeset  72  \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)  d8205bb279a7 Initial revision lcp parents: diff changeset  73 \end{tabular}  d8205bb279a7 Initial revision lcp parents: diff changeset  74 \end{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  75 \subcaption{Infixes}  d8205bb279a7 Initial revision lcp parents: diff changeset  76 d8205bb279a7 Initial revision lcp parents: diff changeset  77 \begin{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  78 \begin{tabular}{rrr}  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  79  \it external & \it internal & \it description \\  104 d8205bb279a7 Initial revision lcp parents: diff changeset  80  \tt $\Gamma$ |- $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) &  d8205bb279a7 Initial revision lcp parents: diff changeset  81  sequent $\Gamma\turn \Delta$  d8205bb279a7 Initial revision lcp parents: diff changeset  82 \end{tabular}  d8205bb279a7 Initial revision lcp parents: diff changeset  83 \end{center}  d8205bb279a7 Initial revision lcp parents: diff changeset  84 \subcaption{Translations}  d8205bb279a7 Initial revision lcp parents: diff changeset  85 \caption{Syntax of {\tt LK}} \label{lk-syntax}  d8205bb279a7 Initial revision lcp parents: diff changeset  86 \end{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  87 d8205bb279a7 Initial revision lcp parents: diff changeset  88 d8205bb279a7 Initial revision lcp parents: diff changeset  89 \begin{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  90 \dquotes  d8205bb279a7 Initial revision lcp parents: diff changeset  91 $\begin{array}{rcl}  d8205bb279a7 Initial revision lcp parents: diff changeset  92  prop & = & sequence " |- " sequence  d8205bb279a7 Initial revision lcp parents: diff changeset  93 \\[2ex]  d8205bb279a7 Initial revision lcp parents: diff changeset  94 sequence & = & elem \quad (", " elem)^* \\  d8205bb279a7 Initial revision lcp parents: diff changeset  95  & | & empty  d8205bb279a7 Initial revision lcp parents: diff changeset  96 \\[2ex]  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  97  elem & = & "\ " term \\  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  98  & | & formula \\  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  99  & | & "<<" sequence ">>"  104 d8205bb279a7 Initial revision lcp parents: diff changeset  100 \\[2ex]  d8205bb279a7 Initial revision lcp parents: diff changeset  101  formula & = & \hbox{expression of type~o} \\  111 1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  102  & | & term " = " term \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  103  & | & "\ttilde\ " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  104  & | & formula " \& " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  105  & | & formula " | " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  106  & | & formula " --> " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  107  & | & formula " <-> " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  108  & | & "ALL~" id~id^* " . " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  109  & | & "EX~~" id~id^* " . " formula \\  1b3cddf41b2d Various updates for Isabelle-93 lcp parents: 104 diff changeset  110  & | & "THE~" id~ " . " formula  104 d8205bb279a7 Initial revision lcp parents: diff changeset  111  \end{array}  d8205bb279a7 Initial revision lcp parents: diff changeset  112 $  d8205bb279a7 Initial revision lcp parents: diff changeset  113 \caption{Grammar of {\tt LK}} \label{lk-grammar}  d8205bb279a7 Initial revision lcp parents: diff changeset  114 \end{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  115 d8205bb279a7 Initial revision lcp parents: diff changeset  116 d8205bb279a7 Initial revision lcp parents: diff changeset  117 d8205bb279a7 Initial revision lcp parents: diff changeset  118 d8205bb279a7 Initial revision lcp parents: diff changeset  119 \begin{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  120 \begin{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  121 \tdx{basic} $H, P,$G |- $E, P,$F  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  122 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  123 \tdx{contRS} $H |-$E, $S,$S, $F ==>$H |- $E,$S, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  124 \tdx{contLS}$H, $S,$S, $G |-$E ==> $H,$S, $G |-$E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  125 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  126 \tdx{thinRS} $H |-$E, $F ==>$H |- $E,$S, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  127 \tdx{thinLS}$H, $G |-$E ==> $H,$S, $G |-$E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  128 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  129 \tdx{cut} [| $H |-$E, P; $H, P |-$E |] ==> $H |-$E  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  130 \subcaption{Structural rules}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  131 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  132 \tdx{refl} $H |-$E, a=a, $F  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  133 \tdx{subst}$H(a), $G(a) |-$E(a) ==> $H(b), a=b,$G(b) |- $E(b)  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  134 \subcaption{Equality rules}  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  135 \end{ttbox}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  136 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  137 \caption{Basic Rules of {\tt LK}} \label{lk-basic-rules}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  138 \end{figure}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  139 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  140 \begin{figure}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  141 \begin{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  142 \tdx{True_def} True == False-->False  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  143 \tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  144 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  145 \tdx{conjR} [|$H|- $E, P,$F; $H|-$E, Q, $F |] ==>$H|- $E, P&Q,$F  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  146 \tdx{conjL} $H, P, Q,$G |- $E ==>$H, P & Q, $G |-$E  104 d8205bb279a7 Initial revision lcp parents: diff changeset  147 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  148 \tdx{disjR} $H |-$E, P, Q, $F ==>$H |- $E, P|Q,$F  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  149 \tdx{disjL} [| $H, P,$G |- $E;$H, Q, $G |-$E |] ==> $H, P|Q,$G |- $E  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  150   841 14b96e3bd4ab fixed minor typos; wenzelm parents: 333 diff changeset  151 \tdx{impR}$H, P |- $E, Q,$F ==> $H |-$E, P-->Q, $F  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  152 \tdx{impL} [|$H,$G |-$E,P; $H, Q,$G |- $E |] ==>$H, P-->Q, $G |-$E  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  153   813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  154 \tdx{notR} $H, P |-$E, $F ==>$H |- $E, ~P,$F  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  155 \tdx{notL} $H,$G |- $E, P ==>$H, ~P, $G |-$E  104 d8205bb279a7 Initial revision lcp parents: diff changeset  156 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  157 \tdx{FalseL} $H, False,$G |- $E  104 d8205bb279a7 Initial revision lcp parents: diff changeset  158 5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  159 \tdx{allR} (!!x.$H|- $E, P(x),$F) ==> $H|-$E, ALL x. P(x), $F  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  160 \tdx{allL}$H, P(x), $G, ALL x. P(x) |-$E ==> $H, ALL x. P(x),$G|- $E  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  161   5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  162 \tdx{exR}$H|- $E, P(x),$F, EX x. P(x) ==> $H|-$E, EX x. P(x), $F  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  163 \tdx{exL} (!!x.$H, P(x), $G|-$E) ==> $H, EX x. P(x),$G|- $E  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  164 5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  165 \tdx{The} [|$H |- $E, P(a),$F; !!x. $H, P(x) |-$E, x=a, $F |] ==>  1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  166 $H |- $E, P(THE x. P(x)),$F  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  167 \subcaption{Logical rules}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  168 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  169 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  170 \caption{Rules of {\tt LK}} \label{lk-rules}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  171 \end{figure}  d8205bb279a7 Initial revision lcp parents: diff changeset  172 d8205bb279a7 Initial revision lcp parents: diff changeset  173 d8205bb279a7 Initial revision lcp parents: diff changeset  174 \section{Syntax and rules of inference}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  175 \index{*sobj type}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  176 104 d8205bb279a7 Initial revision lcp parents: diff changeset  177 Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated  d8205bb279a7 Initial revision lcp parents: diff changeset  178 by the representation of sequents. Type $sobj\To sobj$ represents a list  d8205bb279a7 Initial revision lcp parents: diff changeset  179 of formulae.  d8205bb279a7 Initial revision lcp parents: diff changeset  180 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  181 The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  182 satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  183 denote something, a description is always meaningful, but we do not know  d8205bb279a7 Initial revision lcp parents: diff changeset  184 its value unless $P[x]$ defines it uniquely. The Isabelle notation is  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  185 \hbox{\tt THE $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules})  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  186 does not entail the Axiom of Choice because it requires uniqueness.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  187 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  188 Conditional expressions are available with the notation  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  189 $\dquotes  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  190  "if"~formula~"then"~term~"else"~term.$  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  191 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  192 Figure~\ref{lk-grammar} presents the grammar of \LK. Traditionally,  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  193 $$\Gamma$$ and $$\Delta$$ are meta-variables for sequences. In Isabelle's  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  194 notation, the prefix~\verb|$| on a term makes it range over sequences.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  195 In a sequent, anything not prefixed by \verb|$| is taken as a formula.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  196 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  197 The notation \texttt{<<$sequence$>>} stands for a sequence of formul\ae{}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  198 For example, you can declare the constant \texttt{imps} to consist of two  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  199 implications:  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  200 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  201 consts P,Q,R :: o  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  202 constdefs imps :: seq'=>seq'  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  203  "imps == <

Q, Q --> R>>"  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  204 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  205 Then you can use it in axioms and goals, for example  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  206 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  207 Goalw [imps_def] "P, $imps |- R";  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  208 {\out Level 0}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  209 {\out P,$imps |- R}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  210 {\out 1. P, P --> Q, Q --> R |- R}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  211 by (Fast_tac 1);  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  212 {\out Level 1}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  213 {\out P, $imps |- R}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  214 {\out No subgoals!}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  215 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  216 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  217 Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  218 \thydx{LK}. The connective$\bimp$is defined using$\conj$and$\imp$. The  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  219 axiom for basic sequents is expressed in a form that provides automatic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  220 thinning: redundant formulae are simply ignored. The other rules are  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  221 expressed in the form most suitable for backward proof; exchange and  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  222 contraction rules are not normally required, although they are provided  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  223 anyway.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  224 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  225 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  226 \begin{figure}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  227 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  228 \tdx{thinR}$H |- $E,$F ==> $H |-$E, P, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  229 \tdx{thinL}$H, $G |-$E ==> $H, P,$G |- $E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  230 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  231 \tdx{contR}$H |- $E, P, P,$F ==> $H |-$E, P, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  232 \tdx{contL}$H, P, P, $G |-$E ==> $H, P,$G |- $E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  233 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  234 \tdx{symR}$H |- $E,$F, a=b ==> $H |-$E, b=a, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  235 \tdx{symL}$H, $G, b=a |-$E ==> $H, a=b,$G |- $E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  236 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  237 \tdx{transR} [|$H|- $E,$F, a=b; $H|-$E, $F, b=c |]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  238  ==>$H|- $E, a=c,$F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  239 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  240 \tdx{TrueR} $H |-$E, True, $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  241 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  242 \tdx{iffR} [|$H, P |- $E, Q,$F; $H, Q |-$E, P, $F |]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  243  ==>$H |- $E, P<->Q,$F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  244 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  245 \tdx{iffL} [| $H,$G |- $E, P, Q;$H, Q, P, $G |-$E |]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  246  ==> $H, P<->Q,$G |- $E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  247 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  248 \tdx{allL_thin}$H, P(x), $G |-$E ==> $H, ALL x. P(x),$G |- $E  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  249 \tdx{exR_thin}$H |- $E, P(x),$F ==> $H |-$E, EX x. P(x), $F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  250 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  251 \tdx{the_equality} [|$H |- $E, P(a),$F;  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  252  !!x. $H, P(x) |-$E, x=a, $F |]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  253  ==>$H |- $E, (THE x. P(x)) = a,$F  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  254 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  255 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  256 \caption{Derived rules for {\tt LK}} \label{lk-derived}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  257 \end{figure}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  258 d8205bb279a7 Initial revision lcp parents: diff changeset  259 Figure~\ref{lk-derived} presents derived rules, including rules for  d8205bb279a7 Initial revision lcp parents: diff changeset  260 $\bimp$. The weakened quantifier rules discard each quantification after a  d8205bb279a7 Initial revision lcp parents: diff changeset  261 single use; in an automatic proof procedure, they guarantee termination,  d8205bb279a7 Initial revision lcp parents: diff changeset  262 but are incomplete. Multiple use of a quantifier can be obtained by a  d8205bb279a7 Initial revision lcp parents: diff changeset  263 contraction rule, which in backward proof duplicates a formula. The tactic  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  264 {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,  104 d8205bb279a7 Initial revision lcp parents: diff changeset  265 specifying the formula to duplicate.  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  266 See theory {\tt Sequents/LK0} in the sources for complete listings of  3148 f081757ce757 tuned ref to src; wenzelm parents: 3137 diff changeset  267 the rules and derived rules.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  268 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  269 To support the simplifier, hundreds of equivalences are proved for  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  270 the logical connectives and for if-then-else expressions. See the file  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  271 \texttt{Sequents/simpdata.ML}.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  272 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  273 \section{Automatic Proof}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  274 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  275 \LK{} instantiates Isabelle's simplifier. Both equality ($=$) and the  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  276 biconditional ($\bimp$) may be used for rewriting. The tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  277 \texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  278 sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  279 required; all the formulae{} in the sequent will be simplified. The  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  280 left-hand formulae{} are taken as rewrite rules. (Thus, the behaviour is what  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  281 you would normally expect from calling \texttt{Asm_full_simp_tac}.)  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  282 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  283 For classical reasoning, several tactics are available:  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  284 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  285 Safe_tac : int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  286 Step_tac : int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  287 Fast_tac : int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  288 Best_tac : int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  289 Pc_tac : int -> tactic  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  290 \end{ttbox}  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  291 These refer not to the standard classical reasoner but to a separate one  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  292 provided for the sequent calculus. Two commands are available for adding new  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  293 sequent calculus rules, safe or unsafe, to the default theorem pack'':  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  294 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  295 Add_safes : thm list -> unit  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  296 Add_unsafes : thm list -> unit  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  297 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  298 To control the set of rules for individual invocations, lower-case versions of  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  299 all these primitives are available. Sections~\ref{sec:thm-pack}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  300 and~\ref{sec:sequent-provers} give full details.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  301 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  302 104 d8205bb279a7 Initial revision lcp parents: diff changeset  303 \section{Tactics for the cut rule}  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  304 104 d8205bb279a7 Initial revision lcp parents: diff changeset  305 According to the cut-elimination theorem, the cut rule can be eliminated  d8205bb279a7 Initial revision lcp parents: diff changeset  306 from proofs of sequents. But the rule is still essential. It can be used  d8205bb279a7 Initial revision lcp parents: diff changeset  307 to structure a proof into lemmas, avoiding repeated proofs of the same  d8205bb279a7 Initial revision lcp parents: diff changeset  308 formula. More importantly, the cut rule can not be eliminated from  d8205bb279a7 Initial revision lcp parents: diff changeset  309 derivations of rules. For example, there is a trivial cut-free proof of  d8205bb279a7 Initial revision lcp parents: diff changeset  310 the sequent $$P\conj Q\turn Q\conj P$$.  d8205bb279a7 Initial revision lcp parents: diff changeset  311 Noting this, we might want to derive a rule for swapping the conjuncts  d8205bb279a7 Initial revision lcp parents: diff changeset  312 in a right-hand formula:  d8205bb279a7 Initial revision lcp parents: diff changeset  313 $\Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P$  d8205bb279a7 Initial revision lcp parents: diff changeset  314 The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj  d8205bb279a7 Initial revision lcp parents: diff changeset  315 P$. Most cuts directly involve a premise of the rule being derived (a  d8205bb279a7 Initial revision lcp parents: diff changeset  316 meta-assumption). In a few cases, the cut formula is not part of any  d8205bb279a7 Initial revision lcp parents: diff changeset  317 premise, but serves as a bridge between the premises and the conclusion.  d8205bb279a7 Initial revision lcp parents: diff changeset  318 In such proofs, the cut formula is specified by calling an appropriate  d8205bb279a7 Initial revision lcp parents: diff changeset  319 tactic.  d8205bb279a7 Initial revision lcp parents: diff changeset  320 d8205bb279a7 Initial revision lcp parents: diff changeset  321 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  322 cutR_tac : string -> int -> tactic  d8205bb279a7 Initial revision lcp parents: diff changeset  323 cutL_tac : string -> int -> tactic  d8205bb279a7 Initial revision lcp parents: diff changeset  324 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  325 These tactics refine a subgoal into two by applying the cut rule. The cut  d8205bb279a7 Initial revision lcp parents: diff changeset  326 formula is given as a string, and replaces some other formula in the sequent.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  327 \begin{ttdescription}  264 ca6eb7e6e94f correction to cut tactics lcp parents: 111 diff changeset  328 \item[\ttindexbold{cutR_tac} {\it P\/} {\it i}]  104 d8205bb279a7 Initial revision lcp parents: diff changeset  329 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It  d8205bb279a7 Initial revision lcp parents: diff changeset  330 then deletes some formula from the right side of subgoal~$i$, replacing  d8205bb279a7 Initial revision lcp parents: diff changeset  331 that formula by~$P$.  d8205bb279a7 Initial revision lcp parents: diff changeset  332 264 ca6eb7e6e94f correction to cut tactics lcp parents: 111 diff changeset  333 \item[\ttindexbold{cutL_tac} {\it P\/} {\it i}]  104 d8205bb279a7 Initial revision lcp parents: diff changeset  334 reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It  291 a615050a7494 first draft of Springer volume lcp parents: 264 diff changeset  335 then deletes some formula from the left side of the new subgoal $i+1$,  104 d8205bb279a7 Initial revision lcp parents: diff changeset  336 replacing that formula by~$P$.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  337 \end{ttdescription}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  338 All the structural rules --- cut, contraction, and thinning --- can be  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  339 applied to particular formulae using {\tt res_inst_tac}.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  340 d8205bb279a7 Initial revision lcp parents: diff changeset  341 d8205bb279a7 Initial revision lcp parents: diff changeset  342 \section{Tactics for sequents}  d8205bb279a7 Initial revision lcp parents: diff changeset  343 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  344 forms_of_seq : term -> term list  d8205bb279a7 Initial revision lcp parents: diff changeset  345 could_res : term * term -> bool  d8205bb279a7 Initial revision lcp parents: diff changeset  346 could_resolve_seq : term * term -> bool  d8205bb279a7 Initial revision lcp parents: diff changeset  347 filseq_resolve_tac : thm list -> int -> int -> tactic  d8205bb279a7 Initial revision lcp parents: diff changeset  348 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  349 Associative unification is not as efficient as it might be, in part because  d8205bb279a7 Initial revision lcp parents: diff changeset  350 the representation of lists defeats some of Isabelle's internal  333 2ca08f62df33 final Springer copy lcp parents: 316 diff changeset  351 optimisations. The following operations implement faster rule application,  104 d8205bb279a7 Initial revision lcp parents: diff changeset  352 and may have other uses.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  353 \begin{ttdescription}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  354 \item[\ttindexbold{forms_of_seq} {\it t}]  d8205bb279a7 Initial revision lcp parents: diff changeset  355 returns the list of all formulae in the sequent~$t$, removing sequence  d8205bb279a7 Initial revision lcp parents: diff changeset  356 variables.  d8205bb279a7 Initial revision lcp parents: diff changeset  357 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  358 \item[\ttindexbold{could_res} ($t$,$u$)]  104 d8205bb279a7 Initial revision lcp parents: diff changeset  359 tests whether two formula lists could be resolved. List $t$ is from a  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  360 premise or subgoal, while $u$ is from the conclusion of an object-rule.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  361 Assuming that each formula in $u$ is surrounded by sequence variables, it  d8205bb279a7 Initial revision lcp parents: diff changeset  362 checks that each conclusion formula is unifiable (using {\tt could_unify})  d8205bb279a7 Initial revision lcp parents: diff changeset  363 with some subgoal formula.  d8205bb279a7 Initial revision lcp parents: diff changeset  364 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  365 \item[\ttindexbold{could_resolve_seq} ($t$,$u$)]  291 a615050a7494 first draft of Springer volume lcp parents: 264 diff changeset  366  tests whether two sequents could be resolved. Sequent $t$ is a premise  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  367  or subgoal, while $u$ is the conclusion of an object-rule. It simply  291 a615050a7494 first draft of Springer volume lcp parents: 264 diff changeset  368  calls {\tt could_res} twice to check that both the left and the right  a615050a7494 first draft of Springer volume lcp parents: 264 diff changeset  369  sides of the sequents are compatible.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  370 d8205bb279a7 Initial revision lcp parents: diff changeset  371 \item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}]  d8205bb279a7 Initial revision lcp parents: diff changeset  372 uses {\tt filter_thms could_resolve} to extract the {\it thms} that are  d8205bb279a7 Initial revision lcp parents: diff changeset  373 applicable to subgoal~$i$. If more than {\it maxr\/} theorems are  d8205bb279a7 Initial revision lcp parents: diff changeset  374 applicable then the tactic fails. Otherwise it calls {\tt resolve_tac}.  d8205bb279a7 Initial revision lcp parents: diff changeset  375 Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  376 \end{ttdescription}  104 d8205bb279a7 Initial revision lcp parents: diff changeset  377 d8205bb279a7 Initial revision lcp parents: diff changeset  378 d8205bb279a7 Initial revision lcp parents: diff changeset  379 \section{A simple example of classical reasoning}  d8205bb279a7 Initial revision lcp parents: diff changeset  380 The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the  d8205bb279a7 Initial revision lcp parents: diff changeset  381 classical treatment of the existential quantifier. Classical reasoning  d8205bb279a7 Initial revision lcp parents: diff changeset  382 is easy using~{\LK}, as you can see by comparing this proof with the one  6072 5583261db33d removal of FOL, ZF to a separate manual paulson parents: 5151 diff changeset  383 given in the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  384 proofs are essentially the same; the key step here is to use \tdx{exR}  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  385 rather than the weaker~\tdx{exR_thin}.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  386 \begin{ttbox}  5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  387 Goal "|- EX y. ALL x. P(y)-->P(x)";  104 d8205bb279a7 Initial revision lcp parents: diff changeset  388 {\out Level 0}  d8205bb279a7 Initial revision lcp parents: diff changeset  389 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  390 {\out 1. |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  391 by (resolve_tac [exR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  392 {\out Level 1}  d8205bb279a7 Initial revision lcp parents: diff changeset  393 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  394 {\out 1. |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  395 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  396 There are now two formulae on the right side. Keeping the existential one  d8205bb279a7 Initial revision lcp parents: diff changeset  397 in reserve, we break down the universal one.  d8205bb279a7 Initial revision lcp parents: diff changeset  398 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  399 by (resolve_tac [allR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  400 {\out Level 2}  d8205bb279a7 Initial revision lcp parents: diff changeset  401 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  402 {\out 1. !!x. |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  403 by (resolve_tac [impR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  404 {\out Level 3}  d8205bb279a7 Initial revision lcp parents: diff changeset  405 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  406 {\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  407 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  408 Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not  d8205bb279a7 Initial revision lcp parents: diff changeset  409 become an assumption; instead, it moves to the left side. The  d8205bb279a7 Initial revision lcp parents: diff changeset  410 resulting subgoal cannot be instantiated to a basic sequent: the bound  d8205bb279a7 Initial revision lcp parents: diff changeset  411 variable~$x$ is not unifiable with the unknown~$\Var{x}$.  d8205bb279a7 Initial revision lcp parents: diff changeset  412 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  413 by (resolve_tac [basic] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  414 {\out by: tactic failed}  d8205bb279a7 Initial revision lcp parents: diff changeset  415 \end{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  416 We reuse the existential formula using~\tdx{exR_thin}, which discards  813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  417 it; we shall not need it a third time. We again break down the resulting  104 d8205bb279a7 Initial revision lcp parents: diff changeset  418 formula.  d8205bb279a7 Initial revision lcp parents: diff changeset  419 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  420 by (resolve_tac [exR_thin] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  421 {\out Level 4}  d8205bb279a7 Initial revision lcp parents: diff changeset  422 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  423 {\out 1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  424 by (resolve_tac [allR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  425 {\out Level 5}  d8205bb279a7 Initial revision lcp parents: diff changeset  426 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  427 {\out 1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  428 by (resolve_tac [impR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  429 {\out Level 6}  d8205bb279a7 Initial revision lcp parents: diff changeset  430 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  431 {\out 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}  d8205bb279a7 Initial revision lcp parents: diff changeset  432 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  433 Subgoal~1 seems to offer lots of possibilities. Actually the only useful  5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  434 step is instantiating~$\Var{x@7}$ to $\lambda x. x$,  104 d8205bb279a7 Initial revision lcp parents: diff changeset  435 transforming~$\Var{x@7}(x)$ into~$x$.  d8205bb279a7 Initial revision lcp parents: diff changeset  436 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  437 by (resolve_tac [basic] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  438 {\out Level 7}  d8205bb279a7 Initial revision lcp parents: diff changeset  439 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  440 {\out No subgoals!}  d8205bb279a7 Initial revision lcp parents: diff changeset  441 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  442 This theorem can be proved automatically. Because it involves quantifier  d8205bb279a7 Initial revision lcp parents: diff changeset  443 duplication, we employ best-first search:  d8205bb279a7 Initial revision lcp parents: diff changeset  444 \begin{ttbox}  5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  445 Goal "|- EX y. ALL x. P(y)-->P(x)";  104 d8205bb279a7 Initial revision lcp parents: diff changeset  446 {\out Level 0}  d8205bb279a7 Initial revision lcp parents: diff changeset  447 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  448 {\out 1. |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  449 by (best_tac LK_dup_pack 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  450 {\out Level 1}  d8205bb279a7 Initial revision lcp parents: diff changeset  451 {\out |- EX y. ALL x. P(y) --> P(x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  452 {\out No subgoals!}  d8205bb279a7 Initial revision lcp parents: diff changeset  453 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  454 d8205bb279a7 Initial revision lcp parents: diff changeset  455 d8205bb279a7 Initial revision lcp parents: diff changeset  456 d8205bb279a7 Initial revision lcp parents: diff changeset  457 \section{A more complex proof}  d8205bb279a7 Initial revision lcp parents: diff changeset  458 Many of Pelletier's test problems for theorem provers \cite{pelletier86}  d8205bb279a7 Initial revision lcp parents: diff changeset  459 can be solved automatically. Problem~39 concerns set theory, asserting  d8205bb279a7 Initial revision lcp parents: diff changeset  460 that there is no Russell set --- a set consisting of those sets that are  d8205bb279a7 Initial revision lcp parents: diff changeset  461 not members of themselves:  d8205bb279a7 Initial revision lcp parents: diff changeset  462 $\turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y)$  7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  463 This does not require special properties of membership; we may generalize  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  464 $x\in y$ to an arbitrary predicate~$F(x,y)$. The theorem, which is trivial  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  465 for \texttt{Fast_tac}, has a short manual proof. See the directory {\tt  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  466  Sequents/LK} for many more examples.  104 d8205bb279a7 Initial revision lcp parents: diff changeset  467 d8205bb279a7 Initial revision lcp parents: diff changeset  468 We set the main goal and move the negated formula to the left.  d8205bb279a7 Initial revision lcp parents: diff changeset  469 \begin{ttbox}  5151 1e944fe5ce96 Got rid of obsolete "goal" commands. paulson parents: 3148 diff changeset  470 Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";  104 d8205bb279a7 Initial revision lcp parents: diff changeset  471 {\out Level 0}  d8205bb279a7 Initial revision lcp parents: diff changeset  472 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  473 {\out 1. |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  474 by (resolve_tac [notR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  475 {\out Level 1}  d8205bb279a7 Initial revision lcp parents: diff changeset  476 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  477 {\out 1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}  d8205bb279a7 Initial revision lcp parents: diff changeset  478 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  479 The right side is empty; we strip both quantifiers from the formula on the  d8205bb279a7 Initial revision lcp parents: diff changeset  480 left.  d8205bb279a7 Initial revision lcp parents: diff changeset  481 \begin{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  482 by (resolve_tac [exL] 1);  104 d8205bb279a7 Initial revision lcp parents: diff changeset  483 {\out Level 2}  d8205bb279a7 Initial revision lcp parents: diff changeset  484 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  485 {\out 1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}  d8205bb279a7 Initial revision lcp parents: diff changeset  486 by (resolve_tac [allL_thin] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  487 {\out Level 3}  d8205bb279a7 Initial revision lcp parents: diff changeset  488 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  489 {\out 1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}  d8205bb279a7 Initial revision lcp parents: diff changeset  490 \end{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  491 The rule \tdx{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either  104 d8205bb279a7 Initial revision lcp parents: diff changeset  492 both true or both false. It yields two subgoals.  d8205bb279a7 Initial revision lcp parents: diff changeset  493 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  494 by (resolve_tac [iffL] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  495 {\out Level 4}  d8205bb279a7 Initial revision lcp parents: diff changeset  496 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  497 {\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}  d8205bb279a7 Initial revision lcp parents: diff changeset  498 {\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}  d8205bb279a7 Initial revision lcp parents: diff changeset  499 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  500 We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both  d8205bb279a7 Initial revision lcp parents: diff changeset  501 subgoals. Beginning with subgoal~2, we move a negated formula to the left  d8205bb279a7 Initial revision lcp parents: diff changeset  502 and create a basic sequent.  d8205bb279a7 Initial revision lcp parents: diff changeset  503 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  504 by (resolve_tac [notL] 2);  d8205bb279a7 Initial revision lcp parents: diff changeset  505 {\out Level 5}  d8205bb279a7 Initial revision lcp parents: diff changeset  506 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  507 {\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}  d8205bb279a7 Initial revision lcp parents: diff changeset  508 {\out 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}  d8205bb279a7 Initial revision lcp parents: diff changeset  509 by (resolve_tac [basic] 2);  d8205bb279a7 Initial revision lcp parents: diff changeset  510 {\out Level 6}  d8205bb279a7 Initial revision lcp parents: diff changeset  511 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  512 {\out 1. !!x. |- F(x,x), ~ F(x,x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  513 \end{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  514 Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.  d8205bb279a7 Initial revision lcp parents: diff changeset  515 \begin{ttbox}  d8205bb279a7 Initial revision lcp parents: diff changeset  516 by (resolve_tac [notR] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  517 {\out Level 7}  d8205bb279a7 Initial revision lcp parents: diff changeset  518 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  519 {\out 1. !!x. F(x,x) |- F(x,x)}  d8205bb279a7 Initial revision lcp parents: diff changeset  520 by (resolve_tac [basic] 1);  d8205bb279a7 Initial revision lcp parents: diff changeset  521 {\out Level 8}  d8205bb279a7 Initial revision lcp parents: diff changeset  522 {\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}  d8205bb279a7 Initial revision lcp parents: diff changeset  523 {\out No subgoals!}  d8205bb279a7 Initial revision lcp parents: diff changeset  524 \end{ttbox}  316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  525 7116 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  526 \section{*Unification for lists}\label{sec:assoc-unification}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  527 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  528 Higher-order unification includes associative unification as a special  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  529 case, by an encoding that involves function composition  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  530 \cite[page~37]{huet78}. To represent lists, let $C$ be a new constant.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  531 The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  532 represented by  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  533 $\lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))).$  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  534 The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  535 of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  536 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  537 Unlike orthodox associative unification, this technique can represent certain  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  538 infinite sets of unifiers by flex-flex equations. But note that the term  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  539 $\lambda x. C(t,\Var{a})$ does not represent any list. Flex-flex constraints  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  540 containing such garbage terms may accumulate during a proof.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  541 \index{flex-flex constraints}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  542 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  543 This technique lets Isabelle formalize sequent calculus rules,  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  544 where the comma is the associative operator:  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  545 $\infer[(\conj\hbox{-left})]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  546  {\Gamma,P\conj Q,\Delta \turn \Theta}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  547  {\Gamma,P,Q,\Delta \turn \Theta}$  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  548 Multiple unifiers occur whenever this is resolved against a goal containing  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  549 more than one conjunction on the left.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  550 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  551 \LK{} exploits this representation of lists. As an alternative, the  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  552 sequent calculus can be formalized using an ordinary representation of  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  553 lists, with a logic program for removing a formula from a list. Amy Felty  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  554 has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  555 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  556 Explicit formalization of sequents can be tiresome. But it gives precise  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  557 control over contraction and weakening, and is essential to handle relevant  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  558 and linear logics.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  559 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  560 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  561 \section{*Packaging sequent rules}\label{sec:thm-pack}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  562 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  563 The sequent calculi come with simple proof procedures. These are incomplete  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  564 but are reasonably powerful for interactive use. They expect rules to be  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  565 classified as \textbf{safe} or \textbf{unsafe}. A rule is safe if applying it to a  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  566 provable goal always yields provable subgoals. If a rule is safe then it can  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  567 be applied automatically to a goal without destroying our chances of finding a  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  568 proof. For instance, all the standard rules of the classical sequent calculus  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  569 {\sc lk} are safe. An unsafe rule may render the goal unprovable; typical  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  570 examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  571 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  572 Proof procedures use safe rules whenever possible, using an unsafe rule as a  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  573 last resort. Those safe rules are preferred that generate the fewest  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  574 subgoals. Safe rules are (by definition) deterministic, while the unsafe  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  575 rules require a search strategy, such as backtracking.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  576 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  577 A \textbf{pack} is a pair whose first component is a list of safe rules and  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  578 whose second is a list of unsafe rules. Packs can be extended in an  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  579 obvious way to allow reasoning with various collections of rules. For  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  580 clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  581 essentially a type synonym:  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  582 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  583 datatype pack = Pack of thm list * thm list;  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  584 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  585 Pattern-matching using constructor {\tt Pack} can inspect a pack's  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  586 contents. Packs support the following operations:  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  587 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  588 pack : unit -> pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  589 pack_of : theory -> pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  590 empty_pack : pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  591 prop_pack : pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  592 LK_pack : pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  593 LK_dup_pack : pack  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  594 add_safes : pack * thm list -> pack \hfill\textbf{infix 4}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  595 add_unsafes : pack * thm list -> pack \hfill\textbf{infix 4}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  596 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  597 \begin{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  598 \item[\ttindexbold{pack}] returns the pack attached to the current theory.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  599 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  600 \item[\ttindexbold{pack_of $thy$}] returns the pack attached to theory $thy$.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  601 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  602 \item[\ttindexbold{empty_pack}] is the empty pack.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  603 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  604 \item[\ttindexbold{prop_pack}] contains the propositional rules, namely  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  605 those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  606 rules {\tt basic} and {\tt refl}. These are all safe.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  607 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  608 \item[\ttindexbold{LK_pack}]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  609 extends {\tt prop_pack} with the safe rules {\tt allR}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  610 and~{\tt exL} and the unsafe rules {\tt allL_thin} and  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  611 {\tt exR_thin}. Search using this is incomplete since quantified  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  612 formulae are used at most once.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  613 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  614 \item[\ttindexbold{LK_dup_pack}]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  615 extends {\tt prop_pack} with the safe rules {\tt allR}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  616 and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  617 Search using this is complete, since quantified formulae may be reused, but  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  618 frequently fails to terminate. It is generally unsuitable for depth-first  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  619 search.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  620 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  621 \item[$pack$ \ttindexbold{add_safes} $rules$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  622 adds some safe~$rules$ to the pack~$pack$.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  623 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  624 \item[$pack$ \ttindexbold{add_unsafes} $rules$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  625 adds some unsafe~$rules$ to the pack~$pack$.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  626 \end{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  627 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  628 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  629 \section{*Proof procedures}\label{sec:sequent-provers}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  630 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  631 The \LK{} proof procedure is similar to the classical reasoner  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  632 described in  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  633 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  634  {Chap.\ts\ref{chap:classical}}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  635 %  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  636 In fact it is simpler, since it works directly with sequents rather than  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  637 simulating them. There is no need to distinguish introduction rules from  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  638 elimination rules, and of course there is no swap rule. As always,  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  639 Isabelle's classical proof procedures are less powerful than resolution  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  640 theorem provers. But they are more natural and flexible, working with an  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  641 open-ended set of rules.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  642 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  643 Backtracking over the choice of a safe rule accomplishes nothing: applying  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  644 them in any order leads to essentially the same result. Backtracking may  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  645 be necessary over basic sequents when they perform unification. Suppose  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  646 that~0, 1, 2,~3 are constants in the subgoals  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  647 $\begin{array}{c}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  648  P(0), P(1), P(2) \turn P(\Var{a}) \\  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  649  P(0), P(2), P(3) \turn P(\Var{a}) \\  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  650  P(1), P(3), P(2) \turn P(\Var{a})  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  651  \end{array}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  652 $  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  653 The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  654 and this can only be discovered by search. The tactics given below permit  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  655 backtracking only over axioms, such as {\tt basic} and {\tt refl};  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  656 otherwise they are deterministic.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  657 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  658 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  659 \subsection{Method A}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  660 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  661 reresolve_tac : thm list -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  662 repeat_goal_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  663 pc_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  664 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  665 These tactics use a method developed by Philippe de Groote. A subgoal is  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  666 refined and the resulting subgoals are attempted in reverse order. For  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  667 some reason, this is much faster than attempting the subgoals in order.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  668 The method is inherently depth-first.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  669 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  670 At present, these tactics only work for rules that have no more than two  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  671 premises. They fail --- return no next state --- if they can do nothing.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  672 \begin{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  673 \item[\ttindexbold{reresolve_tac} $thms$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  674 repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  675 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  676 \item[\ttindexbold{repeat_goal_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  677 applies the safe rules in the pack to a goal and the resulting subgoals.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  678 If no safe rule is applicable then it applies an unsafe rule and continues.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  679 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  680 \item[\ttindexbold{pc_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  681 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  682 \end{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  683 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  684 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  685 \subsection{Method B}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  686 \begin{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  687 safe_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  688 step_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  689 fast_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  690 best_tac : pack -> int -> tactic  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  691 \end{ttbox}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  692 These tactics are analogous to those of the generic classical  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  693 reasoner. They use Method~A' only on safe rules. They fail if they  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  694 can do nothing.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  695 \begin{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  696 \item[\ttindexbold{safe_goal_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  697 applies the safe rules in the pack to a goal and the resulting subgoals.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  698 It ignores the unsafe rules.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  699 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  700 \item[\ttindexbold{step_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  701 either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  702 rule.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  703 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  704 \item[\ttindexbold{fast_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  705 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  706 Despite its name, it is frequently slower than {\tt pc_tac}.  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  707 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  708 \item[\ttindexbold{best_tac} $pack$ $i$]  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  709 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  710 particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  711 \end{ttdescription}  8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  712 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  713 8c1caac3e54e simplifier and improved classical reasoner paulson parents: 6072 diff changeset  714 316 813ee27cd4d5 penultimate Springer draft lcp parents: 291 diff changeset  715 \index{sequent calculus|)} `