Logics/document/LK.tex

129 \subcaption{Structural rules}
133 \subcaption{Equality rules}
136 \caption{Basic Rules of {\tt LK}}  \label{lk-basic-rules}
166 \subcaption{Logical rules}
169 \caption{Rules of {\tt LK}}  \label{lk-rules}
173 \section{Syntax and rules of inference}
184   $x$.\ $P[x]$}.  The corresponding rule (Fig.\ts\ref{lk-rules}) does not
216 Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory
219 thinning: redundant formulae are simply ignored.  The other rules are
221 contraction rules are not normally required, although they are provided
255 \caption{Derived rules for {\tt LK}} \label{lk-derived}
258 Figure~\ref{lk-derived} presents derived rules, including rules for
259 $\bimp$.  The weakened quantifier rules discard each quantification after a
263 {\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
266 the rules and derived rules.
279 formulae{} are taken as rewrite rules.  (Thus, the behaviour is what you would
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
308 derivations of rules.  For example, there is a trivial cut-free proof of
335 All the structural rules --- cut, contraction, and thinning --- can be
540 This technique lets Isabelle formalize sequent calculus rules,
558 \section{*Packaging sequent rules}\label{sec:thm-pack}
561 but are reasonably powerful for interactive use.  They expect rules to be
565 proof.  For instance, all the standard rules of the classical sequent calculus
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
601 \item[\ttindexbold{prop_pack}] contains the propositional rules, namely
603 rules {\tt basic} and {\tt refl}.  These are all safe.
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}.
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$.
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,
637 open-ended set of rules.
666 At present, these tactics only work for rules that have no more than two
673 applies the safe rules in the pack to a goal and the resulting subgoals.
689 reasoner.  They use `Method~A' only on safe rules.  They fail if they
693 applies the safe rules in the pack to a goal and the resulting subgoals.
694 It ignores the unsafe rules.
697 either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe