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