3.2.5 Theorems

Axioms, invariants and guards can be marked as theorems. This means that the validity of the theorems must be proven from the axioms, invariants or guards declared before the theorem.

Sometimes an axiom/invariant/guard marked as theorem is also called a derived axiom/invariant/guard.

3.2.5.1 Axioms

For an axiom $A_{thm}$, $A_ b$ denotes (the conjunction of) all axioms declared in extended contexts and the axioms already declared in the current context before the axiom in question.

 

An axiom as theorem

Name

label/THM

Goal

$A_ b(\mathbf{c}) \mathbin \Rightarrow A_{thm}(\mathbf{c})$

3.2.5.2 Invariants

For an invariant $I_{thm}$, $I_ b$ denotes (the conjunction of) all the model’s invariants declared before the theorem.

 

An invariant as theorem

Name

label/THM

Goal

$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land I_ b(\mathbf{c},\mathbf{v},\mathbf{w}) \mathbin \Rightarrow I_{thm}(\mathbf{c},\mathbf{v},\mathbf{w})$

3.2.5.3 Guards

For an invariant $H_{thm}$, $H_ b$ denotes (the conjunction of) all the event’s guards declared before the theorem.

 

A guard as theorem

Name

label/THM

Goal

$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land H_ b(\mathbf{c},\mathbf{w},\mathbf{u}) \mathbin \Rightarrow H_{thm}(\mathbf{c},\mathbf{w},\mathbf{u})$