doc-src/Logics/LK.tex
 author haftmann Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) changeset 21915 4e63c55f4cb4 parent 19152 d81fae81f385 child 42637 381fdcab0f36 permissions -rw-r--r--
different handling of type variable names
     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 Modal 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 cannot 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|)}
`