summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Logics/LK.tex

author | haftmann |

Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) | |

changeset 21915 | 4e63c55f4cb4 |

parent 19152 | d81fae81f385 |

child 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

different handling of type variable names

1 %% $Id$

2 \chapter{First-Order Sequent Calculus}

3 \index{sequent calculus|(}

5 The theory~\thydx{LK} implements classical first-order logic through Gentzen's

6 sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).

7 Resembling the method of semantic tableaux, the calculus is well suited for

8 backwards proof. Assertions have the form \(\Gamma\turn \Delta\), where

9 \(\Gamma\) and \(\Delta\) are lists of formulae. Associative unification,

10 simulated by higher-order unification, handles lists

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

13 The logic is many-sorted, using Isabelle's type classes. The class of

14 first-order terms is called \cldx{term}. No types of individuals are

15 provided, but extensions can define types such as {\tt nat::term} and type

16 constructors such as {\tt list::(term)term}. Below, the type variable

17 $\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers

18 are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which

19 belongs to class {\tt logic}.

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.

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

25 object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:

26 \begin{ttbox}

27 isabelle Sequents

28 context LK.thy;

29 \end{ttbox}

30 Modal logic and linear logic are also available, but unfortunately they are

31 not documented.

34 \begin{figure}

35 \begin{center}

36 \begin{tabular}{rrr}

37 \it name &\it meta-type & \it description \\

38 \cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\

39 \cdx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\

40 \cdx{Not} & $o\To o$ & negation ($\neg$) \\

41 \cdx{True} & $o$ & tautology ($\top$) \\

42 \cdx{False} & $o$ & absurdity ($\bot$)

43 \end{tabular}

44 \end{center}

45 \subcaption{Constants}

47 \begin{center}

48 \begin{tabular}{llrrr}

49 \it symbol &\it name &\it meta-type & \it priority & \it description \\

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

51 universal quantifier ($\forall$) \\

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

53 existential quantifier ($\exists$) \\

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

55 definite description ($\iota$)

56 \end{tabular}

57 \end{center}

58 \subcaption{Binders}

60 \begin{center}

61 \index{*"= symbol}

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

63 \index{*"| symbol}

64 \index{*"-"-"> symbol}

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

66 \begin{tabular}{rrrr}

67 \it symbol & \it meta-type & \it priority & \it description \\

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

69 \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\

70 \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\

71 \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\

72 \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)

73 \end{tabular}

74 \end{center}

75 \subcaption{Infixes}

77 \begin{center}

78 \begin{tabular}{rrr}

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

80 \tt $\Gamma$ |- $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) &

81 sequent $\Gamma\turn \Delta$

82 \end{tabular}

83 \end{center}

84 \subcaption{Translations}

85 \caption{Syntax of {\tt LK}} \label{lk-syntax}

86 \end{figure}

89 \begin{figure}

90 \dquotes

91 \[\begin{array}{rcl}

92 prop & = & sequence " |- " sequence

93 \\[2ex]

94 sequence & = & elem \quad (", " elem)^* \\

95 & | & empty

96 \\[2ex]

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

98 & | & formula \\

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

100 \\[2ex]

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

102 & | & term " = " term \\

103 & | & "\ttilde\ " formula \\

104 & | & formula " \& " formula \\

105 & | & formula " | " formula \\

106 & | & formula " --> " formula \\

107 & | & formula " <-> " formula \\

108 & | & "ALL~" id~id^* " . " formula \\

109 & | & "EX~~" id~id^* " . " formula \\

110 & | & "THE~" id~ " . " formula

111 \end{array}

112 \]

113 \caption{Grammar of {\tt LK}} \label{lk-grammar}

114 \end{figure}

119 \begin{figure}

120 \begin{ttbox}

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

123 \tdx{contRS} $H |- $E, $S, $S, $F ==> $H |- $E, $S, $F

124 \tdx{contLS} $H, $S, $S, $G |- $E ==> $H, $S, $G |- $E

126 \tdx{thinRS} $H |- $E, $F ==> $H |- $E, $S, $F

127 \tdx{thinLS} $H, $G |- $E ==> $H, $S, $G |- $E

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

130 \subcaption{Structural rules}

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

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

134 \subcaption{Equality rules}

135 \end{ttbox}

137 \caption{Basic Rules of {\tt LK}} \label{lk-basic-rules}

138 \end{figure}

140 \begin{figure}

141 \begin{ttbox}

142 \tdx{True_def} True == False-->False

143 \tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)

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

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

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

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

152 \tdx{impL} [| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E

154 \tdx{notR} $H, P |- $E, $F ==> $H |- $E, ~P, $F

155 \tdx{notL} $H, $G |- $E, P ==> $H, ~P, $G |- $E

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

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

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

165 \tdx{The} [| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] ==>

166 $H |- $E, P(THE x. P(x)), $F

167 \subcaption{Logical rules}

168 \end{ttbox}

170 \caption{Rules of {\tt LK}} \label{lk-rules}

171 \end{figure}

174 \section{Syntax and rules of inference}

175 \index{*sobj type}

177 Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated

178 by the representation of sequents. Type $sobj\To sobj$ represents a list

179 of formulae.

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

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

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

184 unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE

185 $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not

186 entail the Axiom of Choice because it requires uniqueness.

188 Conditional expressions are available with the notation

189 \[ \dquotes

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

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

193 \(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's

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

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

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}

217 Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory

218 \thydx{LK}. The connective $\bimp$ is defined using $\conj$ and $\imp$. The

219 axiom for basic sequents is expressed in a form that provides automatic

220 thinning: redundant formulae are simply ignored. The other rules are

221 expressed in the form most suitable for backward proof; exchange and

222 contraction rules are not normally required, although they are provided

223 anyway.

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

231 \tdx{contR} $H |- $E, P, P, $F ==> $H |- $E, P, $F

232 \tdx{contL} $H, P, P, $G |- $E ==> $H, P, $G |- $E

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

237 \tdx{transR} [| $H|- $E, $F, a=b; $H|- $E, $F, b=c |]

238 ==> $H|- $E, a=c, $F

240 \tdx{TrueR} $H |- $E, True, $F

242 \tdx{iffR} [| $H, P |- $E, Q, $F; $H, Q |- $E, P, $F |]

243 ==> $H |- $E, P<->Q, $F

245 \tdx{iffL} [| $H, $G |- $E, P, Q; $H, Q, P, $G |- $E |]

246 ==> $H, P<->Q, $G |- $E

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

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}

256 \caption{Derived rules for {\tt LK}} \label{lk-derived}

257 \end{figure}

259 Figure~\ref{lk-derived} presents derived rules, including rules for

260 $\bimp$. The weakened quantifier rules discard each quantification after a

261 single use; in an automatic proof procedure, they guarantee termination,

262 but are incomplete. Multiple use of a quantifier can be obtained by a

263 contraction rule, which in backward proof duplicates a formula. The tactic

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

265 specifying the formula to duplicate.

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

267 the rules and derived rules.

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

270 the logical connectives and for if-then-else expressions. See the file

271 \texttt{Sequents/simpdata.ML}.

273 \section{Automatic Proof}

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

276 biconditional ($\bimp$) may be used for rewriting. The tactic

277 \texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With

278 sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not

279 required; all the formulae{} in the sequent will be simplified. The left-hand

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

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

283 For classical reasoning, several tactics are available:

284 \begin{ttbox}

285 Safe_tac : int -> tactic

286 Step_tac : int -> tactic

287 Fast_tac : int -> tactic

288 Best_tac : int -> tactic

289 Pc_tac : int -> tactic

290 \end{ttbox}

291 These refer not to the standard classical reasoner but to a separate one

292 provided for the sequent calculus. Two commands are available for adding new

293 sequent calculus rules, safe or unsafe, to the default ``theorem pack'':

294 \begin{ttbox}

295 Add_safes : thm list -> unit

296 Add_unsafes : thm list -> unit

297 \end{ttbox}

298 To control the set of rules for individual invocations, lower-case versions of

299 all these primitives are available. Sections~\ref{sec:thm-pack}

300 and~\ref{sec:sequent-provers} give full details.

303 \section{Tactics for the cut rule}

305 According to the cut-elimination theorem, the cut rule can be eliminated

306 from proofs of sequents. But the rule is still essential. It can be used

307 to structure a proof into lemmas, avoiding repeated proofs of the same

308 formula. More importantly, the cut rule cannot be eliminated from

309 derivations of rules. For example, there is a trivial cut-free proof of

310 the sequent \(P\conj Q\turn Q\conj P\).

311 Noting this, we might want to derive a rule for swapping the conjuncts

312 in a right-hand formula:

313 \[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]

314 The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj

315 P$. Most cuts directly involve a premise of the rule being derived (a

316 meta-assumption). In a few cases, the cut formula is not part of any

317 premise, but serves as a bridge between the premises and the conclusion.

318 In such proofs, the cut formula is specified by calling an appropriate

319 tactic.

321 \begin{ttbox}

322 cutR_tac : string -> int -> tactic

323 cutL_tac : string -> int -> tactic

324 \end{ttbox}

325 These tactics refine a subgoal into two by applying the cut rule. The cut

326 formula is given as a string, and replaces some other formula in the sequent.

327 \begin{ttdescription}

328 \item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and

329 applies the cut rule to subgoal~$i$. It then deletes some formula from the

330 right side of subgoal~$i$, replacing that formula by~$P$.

332 \item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and

333 applies the cut rule to subgoal~$i$. It then deletes some formula from the

334 left side of the new subgoal $i+1$, replacing that formula by~$P$.

335 \end{ttdescription}

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

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

340 \section{Tactics for sequents}

341 \begin{ttbox}

342 forms_of_seq : term -> term list

343 could_res : term * term -> bool

344 could_resolve_seq : term * term -> bool

345 filseq_resolve_tac : thm list -> int -> int -> tactic

346 \end{ttbox}

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

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

349 optimisations. The following operations implement faster rule application,

350 and may have other uses.

351 \begin{ttdescription}

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

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

354 variables.

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

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

358 premise or subgoal, while $u$ is from the conclusion of an object-rule.

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

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

361 with some subgoal formula.

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

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

365 or subgoal, while $u$ is the conclusion of an object-rule. It simply

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

367 sides of the sequents are compatible.

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

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

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

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

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

374 \end{ttdescription}

377 \section{A simple example of classical reasoning}

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

379 classical treatment of the existential quantifier. Classical reasoning is

380 easy using~LK, as you can see by comparing this proof with the one given in

381 the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs

382 are essentially the same; the key step here is to use \tdx{exR} rather than

383 the weaker~\tdx{exR_thin}.

384 \begin{ttbox}

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

386 {\out Level 0}

387 {\out |- EX y. ALL x. P(y) --> P(x)}

388 {\out 1. |- EX y. ALL x. P(y) --> P(x)}

389 by (resolve_tac [exR] 1);

390 {\out Level 1}

391 {\out |- EX y. ALL x. P(y) --> P(x)}

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

393 \end{ttbox}

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

395 in reserve, we break down the universal one.

396 \begin{ttbox}

397 by (resolve_tac [allR] 1);

398 {\out Level 2}

399 {\out |- EX y. ALL x. P(y) --> P(x)}

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

401 by (resolve_tac [impR] 1);

402 {\out Level 3}

403 {\out |- EX y. ALL x. P(y) --> P(x)}

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

405 \end{ttbox}

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

407 assumption; instead, it moves to the left side. The resulting subgoal cannot

408 be instantiated to a basic sequent: the bound variable~$x$ is not unifiable

409 with the unknown~$\Var{x}$.

410 \begin{ttbox}

411 by (resolve_tac [basic] 1);

412 {\out by: tactic failed}

413 \end{ttbox}

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

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

416 formula.

417 \begin{ttbox}

418 by (resolve_tac [exR_thin] 1);

419 {\out Level 4}

420 {\out |- EX y. ALL x. P(y) --> P(x)}

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

422 by (resolve_tac [allR] 1);

423 {\out Level 5}

424 {\out |- EX y. ALL x. P(y) --> P(x)}

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

426 by (resolve_tac [impR] 1);

427 {\out Level 6}

428 {\out |- EX y. ALL x. P(y) --> P(x)}

429 {\out 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}

430 \end{ttbox}

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

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

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

434 \begin{ttbox}

435 by (resolve_tac [basic] 1);

436 {\out Level 7}

437 {\out |- EX y. ALL x. P(y) --> P(x)}

438 {\out No subgoals!}

439 \end{ttbox}

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

441 duplication, we employ best-first search:

442 \begin{ttbox}

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

444 {\out Level 0}

445 {\out |- EX y. ALL x. P(y) --> P(x)}

446 {\out 1. |- EX y. ALL x. P(y) --> P(x)}

447 by (best_tac LK_dup_pack 1);

448 {\out Level 1}

449 {\out |- EX y. ALL x. P(y) --> P(x)}

450 {\out No subgoals!}

451 \end{ttbox}

455 \section{A more complex proof}

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

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

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

459 not members of themselves:

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

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

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

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

464 Sequents/LK} for many more examples.

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

467 \begin{ttbox}

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

469 {\out Level 0}

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

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

472 by (resolve_tac [notR] 1);

473 {\out Level 1}

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

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

476 \end{ttbox}

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

478 left.

479 \begin{ttbox}

480 by (resolve_tac [exL] 1);

481 {\out Level 2}

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

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

484 by (resolve_tac [allL_thin] 1);

485 {\out Level 3}

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

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

488 \end{ttbox}

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

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

491 \begin{ttbox}

492 by (resolve_tac [iffL] 1);

493 {\out Level 4}

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

495 {\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}

496 {\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}

497 \end{ttbox}

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

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

500 and create a basic sequent.

501 \begin{ttbox}

502 by (resolve_tac [notL] 2);

503 {\out Level 5}

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

505 {\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}

506 {\out 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}

507 by (resolve_tac [basic] 2);

508 {\out Level 6}

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

510 {\out 1. !!x. |- F(x,x), ~ F(x,x)}

511 \end{ttbox}

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

513 \begin{ttbox}

514 by (resolve_tac [notR] 1);

515 {\out Level 7}

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

517 {\out 1. !!x. F(x,x) |- F(x,x)}

518 by (resolve_tac [basic] 1);

519 {\out Level 8}

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

521 {\out No subgoals!}

522 \end{ttbox}

524 \section{*Unification for lists}\label{sec:assoc-unification}

526 Higher-order unification includes associative unification as a special

527 case, by an encoding that involves function composition

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

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

530 represented by

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

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

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

535 Unlike orthodox associative unification, this technique can represent certain

536 infinite sets of unifiers by flex-flex equations. But note that the term

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

538 containing such garbage terms may accumulate during a proof.

539 \index{flex-flex constraints}

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.

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

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.

559 \section{*Packaging sequent rules}\label{sec:thm-pack}

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

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.

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

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

577 way to allow reasoning with various collections of rules. For clarity, LK

578 declares \mltydx{pack} as an \ML{} datatype, although is essentially a type

579 synonym:

580 \begin{ttbox}

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

582 \end{ttbox}

583 Pattern-matching using constructor {\tt Pack} can inspect a pack's

584 contents. Packs support the following operations:

585 \begin{ttbox}

586 pack : unit -> pack

587 pack_of : theory -> pack

588 empty_pack : pack

589 prop_pack : pack

590 LK_pack : pack

591 LK_dup_pack : pack

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

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

594 \end{ttbox}

595 \begin{ttdescription}

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

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

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

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.

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.

612 \item[\ttindexbold{LK_dup_pack}]

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

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

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

616 frequently fails to terminate. It is generally unsuitable for depth-first

617 search.

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

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

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

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

624 \end{ttdescription}

627 \section{*Proof procedures}\label{sec:sequent-provers}

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

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

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

632 %

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

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

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

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

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

638 open-ended set of rules.

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.

656 \subsection{Method A}

657 \begin{ttbox}

658 reresolve_tac : thm list -> int -> tactic

659 repeat_goal_tac : pack -> int -> tactic

660 pc_tac : pack -> int -> tactic

661 \end{ttbox}

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

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

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

665 The method is inherently depth-first.

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.

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.

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

678 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.

679 \end{ttdescription}

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.

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

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

699 rule.

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

702 applies {\tt step_tac} using depth-first search to solve subgoal~$i$.

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

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

706 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is

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

708 \end{ttdescription}

712 \index{sequent calculus|)}