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 

7116

21 
\LK{} implements a classical logic theorem prover that is nearly as powerful


22 
as 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$

316

182 
satisfying~$P[a]$, if one exists and is unique. Since all terms in \LK{}

104

183 
denote something, a description is always meaningful, but we do not know


184 
its value unless $P[x]$ defines it uniquely. The Isabelle notation is

7116

185 
\hbox{\tt THE $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lkrules})

316

186 
does not 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 

316

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


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 

7116

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


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


281 
you would 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}

264

328 
\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}]

104

329 
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It


330 
then deletes some formula from the right side of subgoal~$i$, replacing


331 
that formula by~$P$.


332 

264

333 
\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}]

104

334 
reads an \LK{} formula~$P$, and applies the cut rule to subgoal~$i$. It

291

335 
then deletes some formula from the left side of the new subgoal $i+1$,

104

336 
replacing that formula by~$P$.

316

337 
\end{ttdescription}

104

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

316

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

104

340 


341 


342 
\section{Tactics for sequents}


343 
\begin{ttbox}


344 
forms_of_seq : term > term list


345 
could_res : term * term > bool


346 
could_resolve_seq : term * term > bool


347 
filseq_resolve_tac : thm list > int > int > tactic


348 
\end{ttbox}


349 
Associative unification is not as efficient as it might be, in part because


350 
the representation of lists defeats some of Isabelle's internal

333

351 
optimisations. The following operations implement faster rule application,

104

352 
and may have other uses.

316

353 
\begin{ttdescription}

104

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


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


356 
variables.


357 

316

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

104

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

316

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

104

361 
Assuming that each formula in $u$ is surrounded by sequence variables, it


362 
checks that each conclusion formula is unifiable (using {\tt could_unify})


363 
with some subgoal formula.


364 

316

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

291

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

316

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

291

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


369 
sides of the sequents are compatible.

104

370 


371 
\item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}]


372 
uses {\tt filter_thms could_resolve} to extract the {\it thms} that are


373 
applicable to subgoal~$i$. If more than {\it maxr\/} theorems are


374 
applicable then the tactic fails. Otherwise it calls {\tt resolve_tac}.


375 
Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.

316

376 
\end{ttdescription}

104

377 


378 


379 
\section{A simple example of classical reasoning}


380 
The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the


381 
classical treatment of the existential quantifier. Classical reasoning


382 
is easy using~{\LK}, as you can see by comparing this proof with the one

6072

383 
given in the FOL manual~\cite{isabelleZF}. From a logical point of view, the

316

384 
proofs are essentially the same; the key step here is to use \tdx{exR}


385 
rather than the weaker~\tdx{exR_thin}.

104

386 
\begin{ttbox}

5151

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

104

388 
{\out Level 0}


389 
{\out  EX y. ALL x. P(y) > P(x)}


390 
{\out 1.  EX y. ALL x. P(y) > P(x)}


391 
by (resolve_tac [exR] 1);


392 
{\out Level 1}


393 
{\out  EX y. ALL x. P(y) > P(x)}


394 
{\out 1.  ALL x. P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)}


395 
\end{ttbox}


396 
There are now two formulae on the right side. Keeping the existential one


397 
in reserve, we break down the universal one.


398 
\begin{ttbox}


399 
by (resolve_tac [allR] 1);


400 
{\out Level 2}


401 
{\out  EX y. ALL x. P(y) > P(x)}


402 
{\out 1. !!x.  P(?x) > P(x), EX x. ALL xa. P(x) > P(xa)}


403 
by (resolve_tac [impR] 1);


404 
{\out Level 3}


405 
{\out  EX y. ALL x. P(y) > P(x)}


406 
{\out 1. !!x. P(?x)  P(x), EX x. ALL xa. P(x) > P(xa)}


407 
\end{ttbox}


408 
Because {\LK} is a sequent calculus, the formula~$P(\Var{x})$ does not


409 
become an assumption; instead, it moves to the left side. The


410 
resulting subgoal cannot be instantiated to a basic sequent: the bound


411 
variable~$x$ is not unifiable with the unknown~$\Var{x}$.


412 
\begin{ttbox}


413 
by (resolve_tac [basic] 1);


414 
{\out by: tactic failed}


415 
\end{ttbox}

316

416 
We reuse the existential formula using~\tdx{exR_thin}, which discards


417 
it; we shall not need it a third time. We again break down the resulting

104

418 
formula.


419 
\begin{ttbox}


420 
by (resolve_tac [exR_thin] 1);


421 
{\out Level 4}


422 
{\out  EX y. ALL x. P(y) > P(x)}


423 
{\out 1. !!x. P(?x)  P(x), ALL xa. P(?x7(x)) > P(xa)}


424 
by (resolve_tac [allR] 1);


425 
{\out Level 5}


426 
{\out  EX y. ALL x. P(y) > P(x)}


427 
{\out 1. !!x xa. P(?x)  P(x), P(?x7(x)) > P(xa)}


428 
by (resolve_tac [impR] 1);


429 
{\out Level 6}


430 
{\out  EX y. ALL x. P(y) > P(x)}


431 
{\out 1. !!x xa. P(?x), P(?x7(x))  P(x), P(xa)}


432 
\end{ttbox}


433 
Subgoal~1 seems to offer lots of possibilities. Actually the only useful

5151

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

104

435 
transforming~$\Var{x@7}(x)$ into~$x$.


436 
\begin{ttbox}


437 
by (resolve_tac [basic] 1);


438 
{\out Level 7}


439 
{\out  EX y. ALL x. P(y) > P(x)}


440 
{\out No subgoals!}


441 
\end{ttbox}


442 
This theorem can be proved automatically. Because it involves quantifier


443 
duplication, we employ bestfirst search:


444 
\begin{ttbox}

5151

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

104

446 
{\out Level 0}


447 
{\out  EX y. ALL x. P(y) > P(x)}


448 
{\out 1.  EX y. ALL x. P(y) > P(x)}


449 
by (best_tac LK_dup_pack 1);


450 
{\out Level 1}


451 
{\out  EX y. ALL x. P(y) > P(x)}


452 
{\out No subgoals!}


453 
\end{ttbox}


454 


455 


456 


457 
\section{A more complex proof}


458 
Many of Pelletier's test problems for theorem provers \cite{pelletier86}


459 
can be solved automatically. Problem~39 concerns set theory, asserting


460 
that there is no Russell set  a set consisting of those sets that are


461 
not members of themselves:


462 
\[ \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]

7116

463 
This does not require special properties of membership; we may generalize


464 
$x\in y$ to an arbitrary predicate~$F(x,y)$. The theorem, which is trivial


465 
for \texttt{Fast_tac}, has a short manual proof. See the directory {\tt


466 
Sequents/LK} for many more examples.

104

467 


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


469 
\begin{ttbox}

5151

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

104

471 
{\out Level 0}


472 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


473 
{\out 1.  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


474 
by (resolve_tac [notR] 1);


475 
{\out Level 1}


476 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


477 
{\out 1. EX x. ALL y. F(y,x) <> ~ F(y,y) }


478 
\end{ttbox}


479 
The right side is empty; we strip both quantifiers from the formula on the


480 
left.


481 
\begin{ttbox}

316

482 
by (resolve_tac [exL] 1);

104

483 
{\out Level 2}


484 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


485 
{\out 1. !!x. ALL y. F(y,x) <> ~ F(y,y) }


486 
by (resolve_tac [allL_thin] 1);


487 
{\out Level 3}


488 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


489 
{\out 1. !!x. F(?x2(x),x) <> ~ F(?x2(x),?x2(x)) }


490 
\end{ttbox}

316

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

104

492 
both true or both false. It yields two subgoals.


493 
\begin{ttbox}


494 
by (resolve_tac [iffL] 1);


495 
{\out Level 4}


496 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


497 
{\out 1. !!x.  F(?x2(x),x), ~ F(?x2(x),?x2(x))}


498 
{\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) }


499 
\end{ttbox}


500 
We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both


501 
subgoals. Beginning with subgoal~2, we move a negated formula to the left


502 
and create a basic sequent.


503 
\begin{ttbox}


504 
by (resolve_tac [notL] 2);


505 
{\out Level 5}


506 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


507 
{\out 1. !!x.  F(?x2(x),x), ~ F(?x2(x),?x2(x))}


508 
{\out 2. !!x. F(?x2(x),x)  F(?x2(x),?x2(x))}


509 
by (resolve_tac [basic] 2);


510 
{\out Level 6}


511 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


512 
{\out 1. !!x.  F(x,x), ~ F(x,x)}


513 
\end{ttbox}


514 
Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.


515 
\begin{ttbox}


516 
by (resolve_tac [notR] 1);


517 
{\out Level 7}


518 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


519 
{\out 1. !!x. F(x,x)  F(x,x)}


520 
by (resolve_tac [basic] 1);


521 
{\out Level 8}


522 
{\out  ~ (EX x. ALL y. F(y,x) <> ~ F(y,y))}


523 
{\out No subgoals!}


524 
\end{ttbox}

316

525 

7116

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


527 


528 
Higherorder unification includes associative unification as a special


529 
case, by an encoding that involves function composition


530 
\cite[page~37]{huet78}. To represent lists, let $C$ be a new constant.


531 
The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is


532 
represented by


533 
\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))). \]


534 
The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways


535 
of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.


536 


537 
Unlike orthodox associative unification, this technique can represent certain


538 
infinite sets of unifiers by flexflex equations. But note that the term


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


540 
containing such garbage terms may accumulate during a proof.


541 
\index{flexflex constraints}


542 


543 
This technique lets Isabelle formalize sequent calculus rules,


544 
where the comma is the associative operator:


545 
\[ \infer[(\conj\hbox{left})]


546 
{\Gamma,P\conj Q,\Delta \turn \Theta}


547 
{\Gamma,P,Q,\Delta \turn \Theta} \]


548 
Multiple unifiers occur whenever this is resolved against a goal containing


549 
more than one conjunction on the left.


550 


551 
\LK{} exploits this representation of lists. As an alternative, the


552 
sequent calculus can be formalized using an ordinary representation of


553 
lists, with a logic program for removing a formula from a list. Amy Felty


554 
has applied this technique using the language $\lambda$Prolog~\cite{felty91a}.


555 


556 
Explicit formalization of sequents can be tiresome. But it gives precise


557 
control over contraction and weakening, and is essential to handle relevant


558 
and linear logics.


559 


560 


561 
\section{*Packaging sequent rules}\label{sec:thmpack}


562 


563 
The sequent calculi come with simple proof procedures. These are incomplete


564 
but are reasonably powerful for interactive use. They expect rules to be


565 
classified as \textbf{safe} or \textbf{unsafe}. A rule is safe if applying it to a


566 
provable goal always yields provable subgoals. If a rule is safe then it can


567 
be applied automatically to a goal without destroying our chances of finding a


568 
proof. For instance, all the standard rules of the classical sequent calculus


569 
{\sc lk} are safe. An unsafe rule may render the goal unprovable; typical


570 
examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.


571 


572 
Proof procedures use safe rules whenever possible, using an unsafe rule as a


573 
last resort. Those safe rules are preferred that generate the fewest


574 
subgoals. Safe rules are (by definition) deterministic, while the unsafe


575 
rules require a search strategy, such as backtracking.


576 


577 
A \textbf{pack} is a pair whose first component is a list of safe rules and


578 
whose second is a list of unsafe rules. Packs can be extended in an


579 
obvious way to allow reasoning with various collections of rules. For


580 
clarity, \LK{} declares \mltydx{pack} as an \ML{} datatype, although is


581 
essentially a type synonym:


582 
\begin{ttbox}


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


584 
\end{ttbox}


585 
Patternmatching using constructor {\tt Pack} can inspect a pack's


586 
contents. Packs support the following operations:


587 
\begin{ttbox}


588 
pack : unit > pack


589 
pack_of : theory > pack


590 
empty_pack : pack


591 
prop_pack : pack


592 
LK_pack : pack


593 
LK_dup_pack : pack


594 
add_safes : pack * thm list > pack \hfill\textbf{infix 4}


595 
add_unsafes : pack * thm list > pack \hfill\textbf{infix 4}


596 
\end{ttbox}


597 
\begin{ttdescription}


598 
\item[\ttindexbold{pack}] returns the pack attached to the current theory.


599 


600 
\item[\ttindexbold{pack_of $thy$}] returns the pack attached to theory $thy$.


601 


602 
\item[\ttindexbold{empty_pack}] is the empty pack.


603 


604 
\item[\ttindexbold{prop_pack}] contains the propositional rules, namely


605 
those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the


606 
rules {\tt basic} and {\tt refl}. These are all safe.


607 


608 
\item[\ttindexbold{LK_pack}]


609 
extends {\tt prop_pack} with the safe rules {\tt allR}


610 
and~{\tt exL} and the unsafe rules {\tt allL_thin} and


611 
{\tt exR_thin}. Search using this is incomplete since quantified


612 
formulae are used at most once.


613 


614 
\item[\ttindexbold{LK_dup_pack}]


615 
extends {\tt prop_pack} with the safe rules {\tt allR}


616 
and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.


617 
Search using this is complete, since quantified formulae may be reused, but


618 
frequently fails to terminate. It is generally unsuitable for depthfirst


619 
search.


620 


621 
\item[$pack$ \ttindexbold{add_safes} $rules$]


622 
adds some safe~$rules$ to the pack~$pack$.


623 


624 
\item[$pack$ \ttindexbold{add_unsafes} $rules$]


625 
adds some unsafe~$rules$ to the pack~$pack$.


626 
\end{ttdescription}


627 


628 


629 
\section{*Proof procedures}\label{sec:sequentprovers}


630 


631 
The \LK{} proof procedure is similar to the classical reasoner


632 
described in


633 
\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%


634 
{Chap.\ts\ref{chap:classical}}.


635 
%


636 
In fact it is simpler, since it works directly with sequents rather than


637 
simulating them. There is no need to distinguish introduction rules from


638 
elimination rules, and of course there is no swap rule. As always,


639 
Isabelle's classical proof procedures are less powerful than resolution


640 
theorem provers. But they are more natural and flexible, working with an


641 
openended set of rules.


642 


643 
Backtracking over the choice of a safe rule accomplishes nothing: applying


644 
them in any order leads to essentially the same result. Backtracking may


645 
be necessary over basic sequents when they perform unification. Suppose


646 
that~0, 1, 2,~3 are constants in the subgoals


647 
\[ \begin{array}{c}


648 
P(0), P(1), P(2) \turn P(\Var{a}) \\


649 
P(0), P(2), P(3) \turn P(\Var{a}) \\


650 
P(1), P(3), P(2) \turn P(\Var{a})


651 
\end{array}


652 
\]


653 
The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,


654 
and this can only be discovered by search. The tactics given below permit


655 
backtracking only over axioms, such as {\tt basic} and {\tt refl};


656 
otherwise they are deterministic.


657 


658 


659 
\subsection{Method A}


660 
\begin{ttbox}


661 
reresolve_tac : thm list > int > tactic


662 
repeat_goal_tac : pack > int > tactic


663 
pc_tac : pack > int > tactic


664 
\end{ttbox}


665 
These tactics use a method developed by Philippe de Groote. A subgoal is


666 
refined and the resulting subgoals are attempted in reverse order. For


667 
some reason, this is much faster than attempting the subgoals in order.


668 
The method is inherently depthfirst.


669 


670 
At present, these tactics only work for rules that have no more than two


671 
premises. They fail  return no next state  if they can do nothing.


672 
\begin{ttdescription}


673 
\item[\ttindexbold{reresolve_tac} $thms$ $i$]


674 
repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.


675 


676 
\item[\ttindexbold{repeat_goal_tac} $pack$ $i$]


677 
applies the safe rules in the pack to a goal and the resulting subgoals.


678 
If no safe rule is applicable then it applies an unsafe rule and continues.


679 


680 
\item[\ttindexbold{pc_tac} $pack$ $i$]


681 
applies {\tt repeat_goal_tac} using depthfirst search to solve subgoal~$i$.


682 
\end{ttdescription}


683 


684 


685 
\subsection{Method B}


686 
\begin{ttbox}


687 
safe_tac : pack > int > tactic


688 
step_tac : pack > int > tactic


689 
fast_tac : pack > int > tactic


690 
best_tac : pack > int > tactic


691 
\end{ttbox}


692 
These tactics are analogous to those of the generic classical


693 
reasoner. They use `Method~A' only on safe rules. They fail if they


694 
can do nothing.


695 
\begin{ttdescription}


696 
\item[\ttindexbold{safe_goal_tac} $pack$ $i$]


697 
applies the safe rules in the pack to a goal and the resulting subgoals.


698 
It ignores the unsafe rules.


699 


700 
\item[\ttindexbold{step_tac} $pack$ $i$]


701 
either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe


702 
rule.


703 


704 
\item[\ttindexbold{fast_tac} $pack$ $i$]


705 
applies {\tt step_tac} using depthfirst search to solve subgoal~$i$.


706 
Despite its name, it is frequently slower than {\tt pc_tac}.


707 


708 
\item[\ttindexbold{best_tac} $pack$ $i$]


709 
applies {\tt step_tac} using bestfirst search to solve subgoal~$i$. It is


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


711 
\end{ttdescription}


712 


713 


714 

316

715 
\index{sequent calculus)}
