# Theory Dioid

(* Title:      From Semilattices to Dioids
Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
Tjark Weber <tjark.weber at it.uu.se>
*)

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)"

lemma add_left_idem [ac_simps]: "x + (x + y) = x + y"

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"
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
show "x ≤ y ⟹ y ≤ x ⟹ x = y"
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"
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 (* join_semilattice *)

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

sublocale join: bounded_semilattice_sup_bot "(+)" "(≤)" "(<)" 0

lemma no_trivial_inverse: "x ≠ 0 ⟹ ¬(∃y. x + y = 0)"

end (* join_semilattice_zero *)

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
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
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

semigroup reduct of a near dioid is a semilattice. Near dioids are
therefore ordered by the semilattice order.›

subclass join_semilattice

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"
hence "(x + y) ⋅ z = y ⋅ z"
by simp
thus "x ⋅ z ≤ y ⋅ z"
qed

lemma "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
(* nitpick [expect=genuine] -- "3-element counterexample" *)
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 (* near_dioid *)

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

lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
proof -
assume "x ≤ y"
hence "x + y = y"
also have "z ⋅ x + z ⋅ y ≤ z ⋅ (x + y)"
using subdistl_var by blast
moreover have "... = z ⋅ y"
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"

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"
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 (* pre_dioid *)

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

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 (* ab_near_semiring_one *)

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"

end (* ab_near_semiring_one_zerol *)

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 (* ab_pre_semiring_one_zerol *)

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}"

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 (*selective_near_semiring*)

class selective_semiring = selective_near_semiring + semiring_one_zero

begin

subclass dioid_one_zero ..

end (* selective_semiring *)

end