Theory Kleene_Algebra.Dioid
section ‹Dioids›
theory Dioid
imports Signatures
begin
subsection ‹Join Semilattices›
text ‹Join semilattices can be axiomatised order-theoretically or
algebraically. A join semilattice (or upper semilattice) is either a
poset in which every pair of elements has a join (or least upper
bound), or a set endowed with an associative, commutative, idempotent
binary operation. It is well known that the order-theoretic definition
induces the algebraic one and vice versa. We start from the algebraic
axiomatisation because it is easily expandable to dioids, using
Isabelle's type class mechanism.
In Isabelle/HOL, a type class @{class semilattice_sup} is available.
Alas, we cannot use this type class because we need the symbol~‹+› for the join operation in the dioid expansion and subclass
proofs in Isabelle/HOL require the two type classes involved to have
the same fixed signature.
Using {\em add\_assoc} as a name for the first assumption in class
{\em join\_semilattice} would lead to name clashes: we will later
define classes that inherit from @{class semigroup_add}, which
provides its own assumption {\em add\_assoc}, and prove that these are
subclasses of {\em join\_semilattice}. Hence the primed name.
›
class join_semilattice = plus_ord +
assumes add_assoc' [ac_simps]: "(x + y) + z = x + (y + z)"
and add_comm [ac_simps] : "x + y = y + x"
and add_idem [simp]: "x + x = x"
begin
lemma add_left_comm [ac_simps]: "y + (x + z) = x + (y + z)"
using local.add_assoc' local.add_comm by auto
lemma add_left_idem [ac_simps]: "x + (x + y) = x + y"
unfolding add_assoc' [symmetric] by simp
text ‹The definition @{term "x ≤ y ⟷ x + y = y"} of the order is
hidden in class @{class plus_ord}.
We show some simple order-based properties of semilattices. The
first one states that every semilattice is a partial order.›
subclass order
proof
fix x y z :: 'a
show "x < y ⟷ x ≤ y ∧ ¬ y ≤ x"
using local.add_comm local.less_def local.less_eq_def by force
show "x ≤ x"
by (simp add: local.less_eq_def)
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
by (metis add_assoc' less_eq_def)
show "x ≤ y ⟹ y ≤ x ⟹ x = y"
by (simp add: local.add_comm local.less_eq_def)
qed
text ‹Next we show that joins are least upper bounds.›
sublocale join: semilattice_sup "(+)"
by (unfold_locales; simp add: ac_simps local.less_eq_def)
text ‹Next we prove that joins are isotone (order preserving).›
lemma add_iso: "x ≤ y ⟹ x + z ≤ y + z"
using join.sup_mono by blast
text ‹
The next lemma links the definition of order as @{term "x ≤ y ⟷ x + y = y"}
with a perhaps more conventional one known, e.g., from arithmetics.
›
lemma order_prop: "x ≤ y ⟷ (∃z. x + z = y)"
proof
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
thus "∃z. x + z = y"
by auto
next
assume "∃z. x + z = y"
then obtain c where "x + c = y"
by auto
hence "x + c ≤ y"
by simp
thus "x ≤ y"
by simp
qed
end
subsection ‹Join Semilattices with an Additive Unit›
text ‹We now expand join semilattices by an additive unit~$0$. Is
the least element with respect to the order, and therefore often
denoted by~‹⊥›. Semilattices with a least element are often
called \emph{bounded}.›
class join_semilattice_zero = join_semilattice + zero +
assumes add_zero_l [simp]: "0 + x = x"
begin
subclass comm_monoid_add
by (unfold_locales, simp_all add: add_assoc') (simp add: add_comm)
sublocale join: bounded_semilattice_sup_bot "(+)" "(≤)" "(<)" 0
by unfold_locales (simp add: local.order_prop)
lemma no_trivial_inverse: "x ≠ 0 ⟹ ¬(∃y. x + y = 0)"
by (metis local.add_0_right local.join.sup_left_idem)
end
subsection ‹Near Semirings›
text ‹\emph{Near semirings} (also called seminearrings) are
generalisations of near rings to the semiring case. They have been
studied, for instance, in G.~Pilz's book~\<^cite>‹"pilz83nearrings"› on
near rings. According to his definition, a near semiring consists of
an additive and a multiplicative semigroup that interact via a single
distributivity law (left or right). The additive semigroup is not
required to be commutative. The definition is influenced by partial
transformation semigroups.
We only consider near semirings in which addition is commutative, and
in which the right distributivity law holds. We call such near
semirings \emph{abelian}.›
class ab_near_semiring = ab_semigroup_add + semigroup_mult +
assumes distrib_right' [simp]: "(x + y) ⋅ z = x ⋅ z + y ⋅ z"
subclass (in semiring) ab_near_semiring
by (unfold_locales, metis distrib_right)
class ab_pre_semiring = ab_near_semiring +
assumes subdistl_eq: "z ⋅ x + z ⋅ (x + y) = z ⋅ (x + y)"
subsection ‹Variants of Dioids›
text ‹A \emph{near dioid} is an abelian near semiring in which
addition is idempotent. This generalises the notion of (additively)
idempotent semirings by dropping one distributivity law. Near dioids
are a starting point for process algebras.
By modelling variants of dioids as variants of semirings in which
addition is idempotent we follow the tradition of
Birkhoff~\<^cite>‹"birkhoff67lattices"›, but deviate from the definitions
in Gondran and Minoux's book~\<^cite>‹"gondran10graphs"›.›
class near_dioid = ab_near_semiring + plus_ord +
assumes add_idem' [simp]: "x + x = x"
begin
text ‹Since addition is idempotent, the additive (commutative)
semigroup reduct of a near dioid is a semilattice. Near dioids are
therefore ordered by the semilattice order.›
subclass join_semilattice
by unfold_locales (auto simp add: add.commute add.left_commute)
text ‹It follows that multiplication is right-isotone (but not
necessarily left-isotone).›
lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
proof -
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
hence "(x + y) ⋅ z = y ⋅ z"
by simp
thus "x ⋅ z ≤ y ⋅ z"
by (simp add: less_eq_def)
qed
lemma "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
oops
text ‹The next lemma states that, in every near dioid, left
isotonicity and left subdistributivity are equivalent.›
lemma mult_isol_equiv_subdistl:
"(∀x y z. x ≤ y ⟶ z ⋅ x ≤ z ⋅ y) ⟷ (∀x y z. z ⋅ x ≤ z ⋅ (x + y))"
by (metis local.join.sup_absorb2 local.join.sup_ge1)
text ‹The following lemma is relevant to propositional Hoare logic.›
lemma phl_cons1: "x ≤ w ⟹ w ⋅ y ≤ y ⋅ z ⟹ x ⋅ y ≤ y ⋅ z"
using dual_order.trans mult_isor by blast
end
text ‹We now make multiplication in near dioids left isotone, which
is equivalent to left subdistributivity, as we have seen. The
corresponding structures form the basis of probabilistic Kleene
algebras~\<^cite>‹"mciverweber05pka"› and game
algebras~\<^cite>‹"venema03gamealgebra"›. We are not aware that these
structures have a special name, so we baptise them \emph{pre-dioids}.
We do not explicitly define pre-semirings since we have no application
for them.›
class pre_dioid = near_dioid +
assumes subdistl: "z ⋅ x ≤ z ⋅ (x + y)"
begin
text ‹Now, obviously, left isotonicity follows from left subdistributivity.›
lemma subdistl_var: "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using local.mult_isol_equiv_subdistl local.subdistl by auto
subclass ab_pre_semiring
apply unfold_locales
by (simp add: local.join.sup_absorb2 local.subdistl)
lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
proof -
assume "x ≤ y"
hence "x + y = y"
by (simp add: less_eq_def)
also have "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using subdistl_var by blast
moreover have "... = z ⋅ y"
by (simp add: calculation)
ultimately show "z ⋅ x ≤ z ⋅ y"
by auto
qed
lemma mult_isol_var: "u ≤ x ⟹ v ≤ y ⟹ u ⋅ v ≤ x ⋅ y"
by (meson local.dual_order.trans local.mult_isor mult_isol)
lemma mult_double_iso: "x ≤ y ⟹ w ⋅ x ⋅ z ≤ w ⋅ y ⋅ z"
by (simp add: local.mult_isor mult_isol)
text ‹The following lemmas are relevant to propositional Hoare logic.›
lemma phl_cons2: "w ≤ x ⟹ z ⋅ y ≤ y ⋅ w ⟹ z ⋅ y ≤ y ⋅ x"
using local.order_trans mult_isol by blast
lemma phl_seq:
assumes "p ⋅ x ≤ x ⋅ r"
and "r ⋅ y ≤ y ⋅ q"
shows "p ⋅ (x ⋅ y) ≤ x ⋅ y ⋅ q"
proof -
have "p ⋅ x ⋅ y ≤ x ⋅ r ⋅ y"
using assms(1) mult_isor by blast
thus ?thesis
by (metis assms(2) order_prop order_trans subdistl mult_assoc)
qed
lemma phl_cond:
assumes "u ⋅ v ≤ v ⋅ u ⋅ v" and "u ⋅ w ≤ w ⋅ u ⋅ w"
and "⋀x y. u ⋅ (x + y) ≤ u ⋅ x + u ⋅ y"
and "u ⋅ v ⋅ x ≤ x ⋅ z" and "u ⋅ w ⋅ y ≤ y ⋅ z"
shows "u ⋅ (v ⋅ x + w ⋅ y) ≤ (v ⋅ x + w ⋅ y) ⋅ z"
proof -
have a: "u ⋅ v ⋅ x ≤ v ⋅ x ⋅ z" and b: "u ⋅ w ⋅ y ≤ w ⋅ y ⋅ z"
by (metis assms mult_assoc phl_seq)+
have "u ⋅ (v ⋅ x + w ⋅ y) ≤ u ⋅ v ⋅ x + u ⋅ w ⋅ y"
using assms(3) mult_assoc by auto
also have "... ≤ v ⋅ x ⋅ z + w ⋅ y ⋅ z"
using a b join.sup_mono by blast
finally show ?thesis
by simp
qed
lemma phl_export1:
assumes "x ⋅ y ≤ y ⋅ x ⋅ y"
and "(x ⋅ y) ⋅ z ≤ z ⋅ w"
shows "x ⋅ (y ⋅ z) ≤ (y ⋅ z) ⋅ w"
proof -
have "x ⋅ y ⋅ z ≤ y ⋅ x ⋅ y ⋅ z"
by (simp add: assms(1) mult_isor)
thus ?thesis
using assms(1) assms(2) mult_assoc phl_seq by auto
qed
lemma phl_export2:
assumes "z ⋅ w ≤ w ⋅ z ⋅ w"
and "x ⋅ y ≤ y ⋅ z"
shows "x ⋅ (y ⋅ w) ≤ y ⋅ w ⋅ (z ⋅ w)"
proof -
have "x ⋅ y ⋅ w ≤ y ⋅ z ⋅ w"
using assms(2) mult_isor by blast
thus ?thesis
by (metis assms(1) dual_order.trans order_prop subdistl mult_assoc)
qed
end
text ‹By adding a full left distributivity law we obtain semirings
(which are already available in Isabelle/HOL as @{class semiring})
from near semirings, and dioids from near dioids. Dioids are therefore
idempotent semirings.›
class dioid = near_dioid + semiring
subclass (in dioid) pre_dioid
by unfold_locales (simp add: local.distrib_left)
subsection ‹Families of Nearsemirings with a Multiplicative Unit›
text ‹Multiplicative units are important, for instance, for defining
an operation of finite iteration or Kleene star on dioids. We do not
introduce left and right units separately since we have no application
for this.›
class ab_near_semiring_one = ab_near_semiring + one +
assumes mult_onel [simp]: "1 ⋅ x = x"
and mult_oner [simp]: "x ⋅ 1 = x"
begin
subclass monoid_mult
by (unfold_locales, simp_all)
end
class ab_pre_semiring_one = ab_near_semiring_one + ab_pre_semiring
class near_dioid_one = near_dioid + ab_near_semiring_one
begin
text ‹The following lemma is relevant to propositional Hoare logic.›
lemma phl_skip: "x ⋅ 1 ≤ 1 ⋅ x"
by simp
end
text ‹For near dioids with one, it would be sufficient to require
$1+1=1$. This implies @{term "x+x=x"} for arbitray~@{term x} (but that
would lead to annoying redundant proof obligations in mutual
subclasses of @{class near_dioid_one} and @{class near_dioid} later).
›
class pre_dioid_one = pre_dioid + near_dioid_one
class dioid_one = dioid + near_dioid_one
subclass (in dioid_one) pre_dioid_one ..
subsection ‹Families of Nearsemirings with Additive Units›
text ‹
We now axiomatise an additive unit~$0$ for nearsemirings. The zero is
usually required to satisfy annihilation properties with respect to
multiplication. Due to applications we distinguish a zero which is
only a left annihilator from one that is also a right annihilator.
More briefly, we call zero either a left unit or a unit.
Semirings and dioids with a right zero only can be obtained from those
with a left unit by duality.
›
class ab_near_semiring_one_zerol = ab_near_semiring_one + zero +
assumes add_zerol [simp]: "0 + x = x"
and annil [simp]: "0 ⋅ x = 0"
begin
text ‹Note that we do not require~$0 \neq 1$.›
lemma add_zeror [simp]: "x + 0 = x"
by (subst add_commute) simp
end
class ab_pre_semiring_one_zerol = ab_near_semiring_one_zerol + ab_pre_semiring
begin
text ‹The following lemma shows that there is no point defining pre-semirings separately from dioids.›
lemma "1 + 1 = 1"
proof -
have "1 + 1 = 1 ⋅ 1 + 1 ⋅ (1 + 0)"
by simp
also have "... = 1 ⋅ (1 + 0)"
using subdistl_eq by presburger
finally show ?thesis
by simp
qed
end
class near_dioid_one_zerol = near_dioid_one + ab_near_semiring_one_zerol
subclass (in near_dioid_one_zerol) join_semilattice_zero
by (unfold_locales, simp)
class pre_dioid_one_zerol = pre_dioid_one + ab_near_semiring_one_zerol
subclass (in pre_dioid_one_zerol) near_dioid_one_zerol ..
class semiring_one_zerol = semiring + ab_near_semiring_one_zerol
class dioid_one_zerol = dioid_one + ab_near_semiring_one_zerol
subclass (in dioid_one_zerol) pre_dioid_one_zerol ..
text ‹We now make zero also a right annihilator.›
class ab_near_semiring_one_zero = ab_near_semiring_one_zerol +
assumes annir [simp]: "x ⋅ 0 = 0"
class semiring_one_zero = semiring + ab_near_semiring_one_zero
class near_dioid_one_zero = near_dioid_one_zerol + ab_near_semiring_one_zero
class pre_dioid_one_zero = pre_dioid_one_zerol + ab_near_semiring_one_zero
subclass (in pre_dioid_one_zero) near_dioid_one_zero ..
class dioid_one_zero = dioid_one_zerol + ab_near_semiring_one_zero
subclass (in dioid_one_zero) pre_dioid_one_zero ..
subclass (in dioid_one_zero) semiring_one_zero ..
subsection ‹Duality by Opposition›
text ‹
Swapping the order of multiplication in a semiring (or dioid) gives
another semiring (or dioid), called its \emph{dual} or
\emph{opposite}.
›
definition (in times) opp_mult (infixl ‹⊙› 70)
where "x ⊙ y ≡ y ⋅ x"
lemma (in semiring_1) dual_semiring_1:
"class.semiring_1 1 (⊙) (+) 0"
by unfold_locales (auto simp add: opp_mult_def mult.assoc distrib_right distrib_left)
lemma (in dioid_one_zero) dual_dioid_one_zero:
"class.dioid_one_zero (+) (⊙) 1 0 (≤) (<)"
by unfold_locales (auto simp add: opp_mult_def mult.assoc distrib_right distrib_left)
subsection ‹Selective Near Semirings›
text ‹In this section we briefly sketch a generalisation of the
notion of \emph{dioid}. Some important models, e.g. max-plus and
min-plus semirings, have that property.›
class selective_near_semiring = ab_near_semiring + plus_ord +
assumes select: "x + y = x ∨ x + y = y"
begin
lemma select_alt: "x + y ∈ {x,y}"
by (simp add: local.select)
text ‹It follows immediately that every selective near semiring is a near dioid.›
subclass near_dioid
by (unfold_locales, meson select)
text ‹Moreover, the order in a selective near semiring is obviously linear.›
subclass linorder
by (unfold_locales, metis add.commute join.sup.orderI select)
end
class selective_semiring = selective_near_semiring + semiring_one_zero
begin
subclass dioid_one_zero ..
end
end