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

doc-src/Logics/LK.tex

author | wenzelm |

Wed Jul 25 12:38:54 2012 +0200 (2012-07-25) | |

changeset 48497 | ba61aceaa18a |

parent 43049 | 99985426c0bb |

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

some updates on "Building a repository version of Isabelle";

1 \chapter{First-Order Sequent Calculus}

2 \index{sequent calculus|(}

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

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

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

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

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

9 simulated by higher-order unification, handles lists

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

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

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

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

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

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

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

18 belongs to class {\tt logic}.

20 LK implements a classical logic theorem prover that is nearly as powerful as

21 the generic classical reasoner. The simplifier is now available too.

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

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

25 \begin{ttbox}

26 isabelle Sequents

27 context LK.thy;

28 \end{ttbox}

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

30 not documented.

33 \begin{figure}

34 \begin{center}

35 \begin{tabular}{rrr}

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

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

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

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

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

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

42 \end{tabular}

43 \end{center}

44 \subcaption{Constants}

46 \begin{center}

47 \begin{tabular}{llrrr}

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

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

50 universal quantifier ($\forall$) \\

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

52 existential quantifier ($\exists$) \\

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

54 definite description ($\iota$)

55 \end{tabular}

56 \end{center}

57 \subcaption{Binders}

59 \begin{center}

60 \index{*"= symbol}

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

62 \index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working

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

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

65 \begin{tabular}{rrrr}

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

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

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

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

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

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

72 \end{tabular}

73 \end{center}

74 \subcaption{Infixes}

76 \begin{center}

77 \begin{tabular}{rrr}

78 \it external & \it internal & \it description \\

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

80 sequent $\Gamma\turn \Delta$

81 \end{tabular}

82 \end{center}

83 \subcaption{Translations}

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

85 \end{figure}

88 \begin{figure}

89 \dquotes

90 \[\begin{array}{rcl}

91 prop & = & sequence " |- " sequence

92 \\[2ex]

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

94 & | & empty

95 \\[2ex]

96 elem & = & "\$ " term \\

97 & | & formula \\

98 & | & "<<" sequence ">>"

99 \\[2ex]

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

101 & | & term " = " term \\

102 & | & "\ttilde\ " formula \\

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

104 & | & formula " | " formula \\

105 & | & formula " --> " formula \\

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

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

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

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

110 \end{array}

111 \]

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

113 \end{figure}

118 \begin{figure}

119 \begin{ttbox}

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

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

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

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

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

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

129 \subcaption{Structural rules}

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

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

133 \subcaption{Equality rules}

134 \end{ttbox}

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

137 \end{figure}

139 \begin{figure}

140 \begin{ttbox}

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

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

144 \tdx{conjR} [| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F

145 \tdx{conjL} $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E

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

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

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

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

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

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

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

158 \tdx{allR} (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F

159 \tdx{allL} $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E

161 \tdx{exR} $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F

162 \tdx{exL} (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E

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

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

166 \subcaption{Logical rules}

167 \end{ttbox}

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

170 \end{figure}

173 \section{Syntax and rules of inference}

174 \index{*sobj type}

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

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

178 of formulae.

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

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

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

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

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

185 entail the Axiom of Choice because it requires uniqueness.

187 Conditional expressions are available with the notation

188 \[ \dquotes

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

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

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

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

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

196 The notation \texttt{<<$sequence$>>} stands for a sequence of formul\ae{}.

197 For example, you can declare the constant \texttt{imps} to consist of two

198 implications:

199 \begin{ttbox}

200 consts P,Q,R :: o

201 constdefs imps :: seq'=>seq'

202 "imps == <<P --> Q, Q --> R>>"

203 \end{ttbox}

204 Then you can use it in axioms and goals, for example

205 \begin{ttbox}

206 Goalw [imps_def] "P, $imps |- R";

207 {\out Level 0}

208 {\out P, $imps |- R}

209 {\out 1. P, P --> Q, Q --> R |- R}

210 by (Fast_tac 1);

211 {\out Level 1}

212 {\out P, $imps |- R}

213 {\out No subgoals!}

214 \end{ttbox}

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

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

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

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

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

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

222 anyway.

225 \begin{figure}

226 \begin{ttbox}

227 \tdx{thinR} $H |- $E, $F ==> $H |- $E, P, $F

228 \tdx{thinL} $H, $G |- $E ==> $H, P, $G |- $E

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

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

233 \tdx{symR} $H |- $E, $F, a=b ==> $H |- $E, b=a, $F

234 \tdx{symL} $H, $G, b=a |- $E ==> $H, a=b, $G |- $E

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

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

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

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

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

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

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

247 \tdx{allL_thin} $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E

248 \tdx{exR_thin} $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F

250 \tdx{the_equality} [| $H |- $E, P(a), $F;

251 !!x. $H, P(x) |- $E, x=a, $F |]

252 ==> $H |- $E, (THE x. P(x)) = a, $F

253 \end{ttbox}

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

256 \end{figure}

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

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

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

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

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

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

264 specifying the formula to duplicate.

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

266 the rules and derived rules.

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

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

270 \texttt{Sequents/simpdata.ML}.

272 \section{Automatic Proof}

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

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

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

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

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

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

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

282 For classical reasoning, several tactics are available:

283 \begin{ttbox}

284 Safe_tac : int -> tactic

285 Step_tac : int -> tactic

286 Fast_tac : int -> tactic

287 Best_tac : int -> tactic

288 Pc_tac : int -> tactic

289 \end{ttbox}

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

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

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

293 \begin{ttbox}

294 Add_safes : thm list -> unit

295 Add_unsafes : thm list -> unit

296 \end{ttbox}

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

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

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

302 \section{Tactics for the cut rule}

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

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

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

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

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

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

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

311 in a right-hand formula:

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

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

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

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

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

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

318 tactic.

320 \begin{ttbox}

321 cutR_tac : string -> int -> tactic

322 cutL_tac : string -> int -> tactic

323 \end{ttbox}

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

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

326 \begin{ttdescription}

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

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

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

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

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

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

334 \end{ttdescription}

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

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

339 \section{Tactics for sequents}

340 \begin{ttbox}

341 forms_of_seq : term -> term list

342 could_res : term * term -> bool

343 could_resolve_seq : term * term -> bool

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

345 \end{ttbox}

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

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

348 optimisations. The following operations implement faster rule application,

349 and may have other uses.

350 \begin{ttdescription}

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

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

353 variables.

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

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

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

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

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

360 with some subgoal formula.

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

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

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

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

366 sides of the sequents are compatible.

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

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

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

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

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

373 \end{ttdescription}

376 \section{A simple example of classical reasoning}

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

378 classical treatment of the existential quantifier. Classical reasoning is

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

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

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

382 the weaker~\tdx{exR_thin}.

383 \begin{ttbox}

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

385 {\out Level 0}

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

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

388 by (resolve_tac [exR] 1);

389 {\out Level 1}

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

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

392 \end{ttbox}

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

394 in reserve, we break down the universal one.

395 \begin{ttbox}

396 by (resolve_tac [allR] 1);

397 {\out Level 2}

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

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

400 by (resolve_tac [impR] 1);

401 {\out Level 3}

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

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

404 \end{ttbox}

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

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

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

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

409 \begin{ttbox}

410 by (resolve_tac [basic] 1);

411 {\out by: tactic failed}

412 \end{ttbox}

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

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

415 formula.

416 \begin{ttbox}

417 by (resolve_tac [exR_thin] 1);

418 {\out Level 4}

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

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

421 by (resolve_tac [allR] 1);

422 {\out Level 5}

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

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

425 by (resolve_tac [impR] 1);

426 {\out Level 6}

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

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

429 \end{ttbox}

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

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

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

433 \begin{ttbox}

434 by (resolve_tac [basic] 1);

435 {\out Level 7}

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

437 {\out No subgoals!}

438 \end{ttbox}

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

440 duplication, we employ best-first search:

441 \begin{ttbox}

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

443 {\out Level 0}

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

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

446 by (best_tac LK_dup_pack 1);

447 {\out Level 1}

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

449 {\out No subgoals!}

450 \end{ttbox}

454 \section{A more complex proof}

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

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

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

458 not members of themselves:

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

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

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

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

463 Sequents/LK} for many more examples.

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

466 \begin{ttbox}

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

468 {\out Level 0}

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

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

471 by (resolve_tac [notR] 1);

472 {\out Level 1}

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

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

475 \end{ttbox}

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

477 left.

478 \begin{ttbox}

479 by (resolve_tac [exL] 1);

480 {\out Level 2}

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

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

483 by (resolve_tac [allL_thin] 1);

484 {\out Level 3}

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

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

487 \end{ttbox}

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

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

490 \begin{ttbox}

491 by (resolve_tac [iffL] 1);

492 {\out Level 4}

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

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

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

496 \end{ttbox}

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

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

499 and create a basic sequent.

500 \begin{ttbox}

501 by (resolve_tac [notL] 2);

502 {\out Level 5}

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

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

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

506 by (resolve_tac [basic] 2);

507 {\out Level 6}

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

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

510 \end{ttbox}

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

512 \begin{ttbox}

513 by (resolve_tac [notR] 1);

514 {\out Level 7}

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

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

517 by (resolve_tac [basic] 1);

518 {\out Level 8}

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

520 {\out No subgoals!}

521 \end{ttbox}

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

525 Higher-order unification includes associative unification as a special

526 case, by an encoding that involves function composition

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

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

529 represented by

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

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

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

534 Unlike orthodox associative unification, this technique can represent certain

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

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

537 containing such garbage terms may accumulate during a proof.

538 \index{flex-flex constraints}

540 This technique lets Isabelle formalize sequent calculus rules,

541 where the comma is the associative operator:

542 \[ \infer[(\conj\hbox{-left})]

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

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

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

546 more than one conjunction on the left.

548 LK exploits this representation of lists. As an alternative, the sequent

549 calculus can be formalized using an ordinary representation of lists, with a

550 logic program for removing a formula from a list. Amy Felty has applied this

551 technique using the language $\lambda$Prolog~\cite{felty91a}.

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

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

555 and linear logics.

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

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

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

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

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

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

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

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

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

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

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

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

572 rules require a search strategy, such as backtracking.

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

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

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

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

578 synonym:

579 \begin{ttbox}

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

581 \end{ttbox}

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

583 contents. Packs support the following operations:

584 \begin{ttbox}

585 pack : unit -> pack

586 pack_of : theory -> pack

587 empty_pack : pack

588 prop_pack : pack

589 LK_pack : pack

590 LK_dup_pack : pack

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

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

593 \end{ttbox}

594 \begin{ttdescription}

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

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

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

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

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

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

605 \item[\ttindexbold{LK_pack}]

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

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

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

609 formulae are used at most once.

611 \item[\ttindexbold{LK_dup_pack}]

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

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

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

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

616 search.

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

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

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

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

623 \end{ttdescription}

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

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

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

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

631 %

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

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

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

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

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

637 open-ended set of rules.

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

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

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

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

643 \[ \begin{array}{c}

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

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

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

647 \end{array}

648 \]

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

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

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

652 otherwise they are deterministic.

655 \subsection{Method A}

656 \begin{ttbox}

657 reresolve_tac : thm list -> int -> tactic

658 repeat_goal_tac : pack -> int -> tactic

659 pc_tac : pack -> int -> tactic

660 \end{ttbox}

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

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

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

664 The method is inherently depth-first.

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

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

668 \begin{ttdescription}

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

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

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

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

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

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

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

678 \end{ttdescription}

681 \subsection{Method B}

682 \begin{ttbox}

683 safe_tac : pack -> int -> tactic

684 step_tac : pack -> int -> tactic

685 fast_tac : pack -> int -> tactic

686 best_tac : pack -> int -> tactic

687 \end{ttbox}

688 These tactics are analogous to those of the generic classical

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

690 can do nothing.

691 \begin{ttdescription}

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

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

694 It ignores the unsafe rules.

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

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

698 rule.

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

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

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

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

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

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

707 \end{ttdescription}

711 \index{sequent calculus|)}