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