Isabelle/HOL Support Wiki

In a logical calculus, a rule is given by

$\displaystyle\quad\frac{\alpha_1, \dots, \alpha_k}{\beta}$

with $\alpha_1, \dots, \alpha_k, \beta$ formula in the considered logic. Of course, $\beta$ might depend on any combination of the $\alpha_i$.

The meaning is this: If you can prove $\alpha_1, \dots, \alpha_k$ in your calculus, you can also prove $\beta$. In other terms, a set of rules together with some axioms (rules with $k=0$) gives an inductive definition of the set of theorems in your theory.

A rule is correct if and only if $\beta$ is valid if all $\alpha_1, \dots, \alpha_k$ are valid. That means you can never get an inconsistent theory if you have only correct rules and valid axioms.

In Isabelle/HOL, rules are theorems in PURE logics. They are denoted as

$\quad[| P_1; \dots ; P_n |] \Longrightarrow Q$

which is equivalent to above definition.

The nice things about Isabelle/HOL is that you can use your own theorems as rules if they have this format. You can tell Isabelle to transform a theorem into this form (if possible) by using the rule_format directive.