User Manual for Rodin v.2.3: Contexts

2.7.1 Contexts

A context has the following components:

Sets: User-defined types can be declared in the SETS section (See also 3.3.4).
Constants: indexconstant We can declare constants here. The type of each constant must be given by the axioms.
Axioms: The axioms are a list of predicates. indexaxiom They describe what can be taken for granted when developing a model. The axioms can be later used in proofs that occur in components that use (“see”) this context. Each axiom has a label attached to it.
Theorems: Axioms can be marked as theorems. In that case, we declare that the predicate is provable by using the axioms that are written before the theorem. Theorems can be used later in proofs just like the axioms.
Extends: A context may extend an arbitrary number of other contexts. Extending another context $A$ has the effect that we can make use of all constants and axioms declared in $A$ and we can add new constants and axioms.

Rodin automatically generates proof obligations (often abbreviated as PO) for properties that should be proven. Each proof obligation has a name that explains where it comes from. There are two kind of proof obligations generated in a context:

Each theorem must be proven. The proof obligation’s name has the form label/THM, where label is the theorem’s label.
Some expressions are not obviously well-defined. E.g. the axiom $x \div y > 2$ is only meaningful if $y$ is different from 0. Thus Rodin generates the proof obligation $y\neq 0$ . A well-defined proof obligation has the name label/WD.

The order of the axioms and theorems matter because the proof of a theorem or the degree to which an expression is well-definded may depend on the axioms and theorems that are already written. This is necessary to avoid circular reasoning.

Rodin Handbook

2.7.1 Contexts