Intro/document/foundations.tex

4 inference rules in Isabelle's meta-logic; combining rules by resolution.
262 \section{Formalizing logical rules in Isabelle}
276 all $x$', and expresses {\bf generality} in rules and axiom schemes.
307 the inference rules, we shall need to relate the two levels; accordingly,
318 \subsection{Expressing propositional rules}
319 \index{rules!propositional}
320 We shall illustrate the use of the meta-logic by formalizing the rules of
324 One of the simplest rules is $(\conj E1)$.  Making
335 Isabelle adopts notational conventions to ease the writing of rules.  We may
343 Using these conventions, the conjunction rules become the following axioms.
349 Next, consider the disjunction rules.  The discharge of assumption in
376 \subsection{Quantifier rules and substitution}
377 \index{quantifiers}\index{rules!quantifier}\index{substitution|bold}
387 inference rules that involve substitution for bound variables.
390 A logic may attach provisos to certain of its rules, especially quantifier
391 rules.  We cannot hope to formalize arbitrary provisos.  Fortunately, those
392 typical of quantifier rules always have the same form, namely `$x$ not free in
435 also contains grammar rules, specified using mixfix declarations.
491 The meta-logic is defined by a collection of inference rules, including
492 equational rules for the $\lambda$-calculus and logical rules.  The rules
494 Fig.\ts\ref{fol-fig}.  Proofs performed using the primitive meta-rules
495 would be lengthy; Isabelle proofs normally use certain derived rules.
614 \subsection{Joining rules by resolution} \label{joining}
617 \phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules.
625 The substitution~$s$ may instantiate unknowns in both rules.  In short,
639 Resolution expects the rules to have no outer quantifiers~($\Forall$).
642 rules into a standard form with all free variables converted into
646 When resolving two rules, the unknowns in the first rule are renamed, by
658 object-level rule\index{rules!derived}
660 Joining rules in this fashion is a simple way of proving theorems.  The
661 derived rules are conservative extensions of the object-logic, and may permit
685 The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for
687 x.P(x)$, while the conclusions of all the rules are atomic (they have the form
712 When resolving two rules, Isabelle lifts the first one if necessary.  The
771 Resolution is convenient for deriving simple rules and for reasoning
960 Basic tactics execute the meta-rules described above, operating on a
961 given subgoal.  The {\bf resolution tactics} take a list of rules and
966 unifiers.  If there are no matching rules or assumptions then no next
998 with elimination rules.  Elim-resolution applies an elimination rule to an
1003 can also serve to derive rules.
1018 $P\disj Q$ is redundant.  Other elimination rules behave
1034 from natural deduction rules.  It lets an elimination rule consume an
1092 \subsection{Destruction rules} \label{destruct}
1093 \index{rules!destruction}\index{rules!elimination}
1097 elimination rule.  The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and
1099 parlance, such rules are called {\bf destruction rules}; they are readable
1100 and easy to use in forward proof.  The rules $({\disj}E)$, $({\bot}E)$ and
1106 $({\exists}E)$ as destruction rules.  But we can write general elimination
1107 rules for $\conj$, $\imp$ and~$\forall$:
1113 Because they are concise, destruction rules are simpler to derive than the
1114 corresponding elimination rules.  To facilitate their use in backward
1128 \subsection{Deriving rules by resolution}  \label{deriving}
1129 \index{rules!derived|bold}\index{meta-assumptions!syntax of}
1131 system of natural deduction rules.  Each theorem may depend upon
1139 new object-level rules.  To derive the rule