semantics.wp.states
Abstract States, Actions, and Guards
The whole development is parameterized by the choice of state types. This used to be in a module, but this just results in modules polluting everything.
Require Import base.
Parameter state : Type.
Parameter action : Type.
Parameter guard : Type.
Parameter actionE : action -> state -> state.
Parameter guardE : guard -> state -> bool.
Coercion actionE : action >-> Funclass.
Coercion guardE : guard >-> Funclass.
Parameter action_eq : action -> action -> bool.
Parameter guard_eq : guard -> guard -> bool.
Axiom action_eqP : Equality.axiom action_eq.
Axiom guard_eqP : Equality.axiom guard_eq.
Canonical action_eqMixin := EqMixin action_eqP.
Canonical action_eqType := Eval hnf in EqType action action_eqMixin.
Canonical guard_eqMixin := EqMixin guard_eqP.
Canonical guard_eqType := Eval hnf in EqType guard guard_eqMixin.
Parameter state : Type.
Parameter action : Type.
Parameter guard : Type.
Parameter actionE : action -> state -> state.
Parameter guardE : guard -> state -> bool.
Coercion actionE : action >-> Funclass.
Coercion guardE : guard >-> Funclass.
Parameter action_eq : action -> action -> bool.
Parameter guard_eq : guard -> guard -> bool.
Axiom action_eqP : Equality.axiom action_eq.
Axiom guard_eqP : Equality.axiom guard_eq.
Canonical action_eqMixin := EqMixin action_eqP.
Canonical action_eqType := Eval hnf in EqType action action_eqMixin.
Canonical guard_eqMixin := EqMixin guard_eqP.
Canonical guard_eqType := Eval hnf in EqType guard guard_eqMixin.