User Manual for Rodin v.2.3: Well-definedness proof obligations

3.2.4 Well-definedness proof obligations

There are several locations where well-definedness proof obligations can occur. In the reference of the mathematical notation the well-definedness conditions of each operator are defined by the $\mathcal{L}$ -operator (see 3.3.1.2).

For well-definedness conditions the order of axioms, invariants and guards is important. Trivial ( $\mathord {\top }$ ) well-definedness conditions are usually not shown in Rodin.

3.2.4.1 Axioms

For an axiom $A_ w$ , let $A_ b$ denote (the conjunction of) all axioms declared in extended contexts and the axioms already declared in the current context before the axiom in question.

	Well-definedness of an axiom
Name	label/WD
Goal	$A_ b(\mathbf{c}) \mathbin \Rightarrow \mathcal{L}(A_ w(\mathbf{c}))$

3.2.4.2 Invariants

For an invariant $J_ w$ , let $J_ b$ denote (the conjunction of) all the model’s invariants declared before the theorem.

	Well-definedness of an invariant
Name	label/WD
Goal	$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J_ b(\mathbf{c},\mathbf{v},\mathbf{w}) \mathbin \Rightarrow \mathcal{L}(J_ w(\mathbf{c},\mathbf{v},\mathbf{w}))$

3.2.4.3 Guards

For an invariant $H_ w$ , let $H_ b$ denote (the conjunction of) all the model’s invariants declared before the theorem.

	Well-definedness of a guard
Name	eventname/guardlabel/WD
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 \mathcal{L}(H_ w(\mathbf{c},\mathbf{w},\mathbf{u}))$

3.2.4.4 Witnesses

A witness $W$ may contain well-definedness conditions.

	Well-definedness of a witness
Name	eventlabel/witnesslabel/WWD
Goal	$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land \mathcal{T}({\mathbf{t},\mathbf{u}},\mathbf{w},\mathbf{u},\mathbf{w}’)\mathbin \Rightarrow \mathcal{L}(W)$

3.2.4.5 Actions

The assignment $a$ of each action with the label $\textsf{actionlabel}$ of an event must be well-defined.

	Well-definedness of an action
Name	eventlabel/actionlabel/WD
Goal	$A(\mathbf{c})\land I(\mathbf{c},\mathbf{v})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\land G(\mathbf{c},\mathbf{v},\mathbf{t})\land H(\mathbf{c},\mathbf{w},\mathbf{u})\mathbin \Rightarrow \mathcal{L}(~ a~ )$

3.2.4.6 Variants

A variant $V(\mathbf{c},\mathbf{w})$ must be well-defined.

	Well-definedness of a variant
Name	VWD
Goal	$A(\mathbf{c})\land J(\mathbf{c},\mathbf{v},\mathbf{w})\mathbin \Rightarrow \mathcal{L}(V(\mathbf{c},\mathbf{w}))$

Rodin Handbook