Logics/document/LK.tex

6 Resembling the method of semantic tableaux, the calculus is well suited for
7 backwards proof.  Assertions have the form \(\Gamma\turn \Delta\), where
15 constructors such as {\tt list::(term)term}.  Below, the type variable
16 $\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
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}:
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
185 entail the Axiom of Choice because it requires uniqueness.
187 Conditional expressions are available with the notation
191 Figure~\ref{lk-grammar} presents the grammar of LK.  Traditionally,
193 notation, the prefix~\verb|$| on a term makes it range over sequences.
197 For example, you can declare the constant \texttt{imps} to consist of two
216 Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory
220 expressed in the form most suitable for backward proof; exchange and
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
274 LK instantiates Isabelle's simplifier.  Both equality ($=$) and the
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
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'':
297 To control the set of rules for individual invocations, lower-case versions of
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
309 the sequent \(P\conj Q\turn Q\conj P\).
310 Noting this, we might want to derive a rule for swapping the conjuncts
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
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.
328   applies the cut rule to subgoal~$i$.  It then deletes some formula from the
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$.
335 All the structural rules --- cut, contraction, and thinning --- can be
347 the representation of lists defeats some of Isabelle's internal
352 returns the list of all formulae in the sequent~$t$, removing sequence
357 premise or subgoal, while $u$ is from the conclusion of an object-rule.
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.
369 uses {\tt filter_thms could_resolve} to extract the {\it thms} that 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}.
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}.
393 There are now two formulae on the right side.  Keeping the existential one
394 in reserve, we break down the universal one.
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}$.
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
430 Subgoal~1 seems to offer lots of possibilities.  Actually the only useful
462 for \texttt{Fast_tac}, has a short manual proof.  See the directory {\tt
465 We set the main goal and move the negated formula to the left.
476 The right side is empty; we strip both quantifiers from the formula on the
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
511 Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
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.
535 infinite sets of unifiers by flex-flex equations.   But note that the term
541 where the comma is the associative operator:
546 more than one conjunction on the left.
548 LK exploits this representation of lists.  As an alternative, the sequent
551 technique using the language $\lambda$Prolog~\cite{felty91a}.
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}.
570 last resort.  Those safe rules are preferred that generate the fewest
571 subgoals.  Safe rules are (by definition) deterministic, while the unsafe
583 contents.  Packs support the following operations:
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
606 extends {\tt prop_pack} with the safe rules {\tt allR}
607 and~{\tt exL} and the unsafe rules {\tt allL_thin} and
612 extends {\tt prop_pack} with the safe rules {\tt allR}
613 and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.
619 adds some safe~$rules$ to the pack~$pack$.
622 adds some unsafe~$rules$ to the pack~$pack$.
628 The LK proof procedure is similar to the classical reasoner described in
629 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
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
642 that~0, 1, 2,~3 are constants in the subgoals
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.
670 repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
673 applies the safe rules in the pack to a goal and the resulting subgoals.
688 These tactics are analogous to those of the generic classical
693 applies the safe rules in the pack to a goal and the resulting subgoals.
694 It ignores the unsafe rules.