Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

===== Rule (calculus) =====

==== In Logics ====
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 ====
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.

Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools