104

1 
%% $Id$

291

2 
\chapter{FirstOrder Sequent Calculus}

316

3 
\index{sequent calculus(}


4 

7116

5 
The theory~\thydx{LK} implements classical firstorder 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 higherorder unification, handles lists


11 
(\S\ref{sec:assocunification} presents details, if you are interested).

104

12 

316

13 
The logic is manysorted, using Isabelle's type classes. The class of


14 
firstorder 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 (manysorted). The type of formulae is~\tydx{o}, which


19 
belongs to class {\tt logic}.

104

20 

9695

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.

104

23 

5151

24 
To work in LK, start up Isabelle specifying \texttt{Sequents} as the


25 
objectlogic. 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 

104

33 


34 
\begin{figure}


35 
\begin{center}


36 
\begin{tabular}{rrr}

111

37 
\it name &\it metatype & \it description \\

316

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$)

104

43 
\end{tabular}


44 
\end{center}


45 
\subcaption{Constants}


46 


47 
\begin{center}


48 
\begin{tabular}{llrrr}

316

49 
\it symbol &\it name &\it metatype & \it priority & \it description \\


50 
\sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &

111

51 
universal quantifier ($\forall$) \\

316

52 
\sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &

111

53 
existential quantifier ($\exists$) \\

316

54 
\sdx{THE} & \cdx{The} & $(\alpha\To o)\To \alpha$ & 10 &

111

55 
definite description ($\iota$)

104

56 
\end{tabular}


57 
\end{center}


58 
\subcaption{Binders}


59 


60 
\begin{center}

316

61 
\index{*"= symbol}


62 
\index{&@{\tt\&} symbol}


63 
\index{*" symbol}


64 
\index{*"""> symbol}


65 
\index{*"<""> symbol}

104

66 
\begin{tabular}{rrrr}

316

67 
\it symbol & \it metatype & \it priority & \it description \\


68 
\tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\

104

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}

111

79 
\it external & \it internal & \it description \\

104

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{lksyntax}


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]

7116

97 
elem & = & "\$ " term \\


98 
&  & formula \\


99 
&  & "<<" sequence ">>"

104

100 
\\[2ex]


101 
formula & = & \hbox{expression of type~$o$} \\

111

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

104

111 
\end{array}


112 
\]


113 
\caption{Grammar of {\tt LK}} \label{lkgrammar}


114 
\end{figure}


115 


116 


117 


118 


119 
\begin{figure}


120 
\begin{ttbox}

316

121 
\tdx{basic} $H, P, $G  $E, P, $F

7116

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 

316

129 
\tdx{cut} [ $H  $E, P; $H, P  $E ] ==> $H  $E


130 
\subcaption{Structural rules}

104

131 

316

132 
\tdx{refl} $H  $E, a=a, $F

7116

133 
\tdx{subst} $H(a), $G(a)  $E(a) ==> $H(b), a=b, $G(b)  $E(b)

316

134 
\subcaption{Equality rules}

7116

135 
\end{ttbox}

104

136 

7116

137 
\caption{Basic Rules of {\tt LK}} \label{lkbasicrules}


138 
\end{figure}


139 


140 
\begin{figure}


141 
\begin{ttbox}

316

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

104

147 

316

148 
\tdx{disjR} $H  $E, P, Q, $F ==> $H  $E, PQ, $F


149 
\tdx{disjL} [ $H, P, $G  $E; $H, Q, $G  $E ] ==> $H, PQ, $G  $E


150 

841

151 
\tdx{impR} $H, P  $E, Q, $F ==> $H  $E, P>Q, $F

316

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

104

156 

316

157 
\tdx{FalseL} $H, False, $G  $E

104

158 

5151

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

316

161 

5151

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

316

164 

5151

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

316

167 
\subcaption{Logical rules}

104

168 
\end{ttbox}


169 

316

170 
\caption{Rules of {\tt LK}} \label{lkrules}

104

171 
\end{figure}


172 


173 


174 
\section{Syntax and rules of inference}

316

175 
\index{*sobj type}


176 

104

177 
Figure~\ref{lksyntax} 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 

7116

181 
The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$

9695

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{lkrules}) does not


186 
entail the Axiom of Choice because it requires uniqueness.

104

187 

7116

188 
Conditional expressions are available with the notation


189 
\[ \dquotes


190 
"if"~formula~"then"~term~"else"~term. \]


191 

9695

192 
Figure~\ref{lkgrammar} presents the grammar of LK. Traditionally,

316

193 
\(\Gamma\) and \(\Delta\) are metavariables for sequences. In Isabelle's

7116

194 
notation, the prefix~\verb$ on a term makes it range over sequences.

316

195 
In a sequent, anything not prefixed by \verb$ is taken as a formula.

104

196 

7116

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{lkbasicrules} and~\ref{lkrules} 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{lkderived}


257 
\end{figure}

104

258 


259 
Figure~\ref{lkderived} 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

316

264 
{\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,

104

265 
specifying the formula to duplicate.

7116

266 
See theory {\tt Sequents/LK0} in the sources for complete listings of

3148

267 
the rules and derived rules.

104

268 

7116

269 
To support the simplifier, hundreds of equivalences are proved for


270 
the logical connectives and for ifthenelse expressions. See the file


271 
\texttt{Sequents/simpdata.ML}.

104

272 

7116

273 
\section{Automatic Proof}

316

274 

9695

275 
LK instantiates Isabelle's simplifier. Both equality ($=$) and the

7116

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

9695

279 
required; all the formulae{} in the sequent will be simplified. The lefthand


280 
formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would


281 
normally expect from calling \texttt{Asm_full_simp_tac}.)

316

282 

7116

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

316

290 
\end{ttbox}

7116

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, lowercase versions of


299 
all these primitives are available. Sections~\ref{sec:thmpack}


300 
and~\ref{sec:sequentprovers} give full details.

316

301 


302 

104

303 
\section{Tactics for the cut rule}

7116

304 

104

305 
According to the cutelimination 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 cutfree 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 righthand 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 
metaassumption). 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.

316

327 
\begin{ttdescription}

9695

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$.

316

335 
\end{ttdescription}

104

336 
All the structural rules  cut, contraction, and thinning  can be

316

337 
applied to particular formulae using {\tt res_inst_tac}.

104

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

333

349 
optimisations. The following operations implement faster rule application,

104

350 
and may have other uses.

316

351 
\begin{ttdescription}

104

352 
\item[\ttindexbold{forms_of_seq} {\it t}]


353 
returns the list of all formulae in the sequent~$t$, removing sequence


354 
variables.


355 

316

356 
\item[\ttindexbold{could_res} ($t$,$u$)]

104

357 
tests whether two formula lists could be resolved. List $t$ is from a

316

358 
premise or subgoal, while $u$ is from the conclusion of an objectrule.

104

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 

316

363 
\item[\ttindexbold{could_resolve_seq} ($t$,$u$)]

291

364 
tests whether two sequents could be resolved. Sequent $t$ is a premise

316

365 
or subgoal, while $u$ is the conclusion of an objectrule. It simply

291

366 
calls {\tt could_res} twice to check that both the left and the right


367 
sides of the sequents are compatible.

104

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

316

374 
\end{ttdescription}

104

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

9695

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{isabelleZF}. 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}.

104

384 
\begin{ttbox}

5151

385 
Goal " EX y. ALL x. P(y)>P(x)";

104

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}

9695

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}$.

104

410 
\begin{ttbox}


411 
by (resolve_tac [basic] 1);


412 
{\out by: tactic failed}


413 
\end{ttbox}

316

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

104

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

5151

432 
step is instantiating~$\Var{x@7}$ to $\lambda x. x$,

104

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 bestfirst search:


442 
\begin{ttbox}

5151

443 
Goal " EX y. ALL x. P(y)>P(x)";

104

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) \]

7116

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.

104

465 


466 
We set the main goal and move the negated formula to the left.


467 
\begin{ttbox}

5151

468 
Goal " ~ (EX x. ALL y. F(y,x) <> ~F(y,y))";

104

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}

316

480 
by (resolve_tac [exL] 1);

104

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}

316

489 
The rule \tdx{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either

104

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}

316

523 

7116

524 
\section{*Unification for lists}\label{sec:assocunification}


525 


526 
Higherorder 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 flexflex equations. But note that the term


537 
$\lambda x. C(t,\Var{a})$ does not represent any list. Flexflex constraints


538 
containing such garbage terms may accumulate during a proof.


539 
\index{flexflex 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 

9695

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

7116

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:thmpack}


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

9695

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:

7116

580 
\begin{ttbox}


581 
datatype pack = Pack of thm list * thm list;


582 
\end{ttbox}


583 
Patternmatching 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 depthfirst


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:sequentprovers}


628 

9695

629 
The LK proof procedure is similar to the classical reasoner described in

7116

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 
openended 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 depthfirst.


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 depthfirst 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 depthfirst 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 bestfirst search to solve subgoal~$i$. It is


707 
particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).


708 
\end{ttdescription}


709 


710 


711 

316

712 
\index{sequent calculus)}
