Theory Dioid

(* Title:      From Semilattices to Dioids
   Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at>
               Tjark Weber < at>

section ‹Dioids›

theory Dioid
imports Signatures

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"

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

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)"
  assume "x  y"
  hence "x + y = y"
    by (simp add: less_eq_def)
  thus "z. x + z = y"
    by auto
  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

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"


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


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)

lemma "x  y  z  x  z  y"
  (* nitpick [expect=genuine] -- "3-element counterexample" *)

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


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

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)

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

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 

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)

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


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


text ‹The following lemma is relevant to propositional Hoare logic.›

lemma phl_skip: "x  1  1  x"
  by simp


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"


text ‹Note that we do not require~$0 \neq 1$.›

lemma add_zeror [simp]: "x + 0 = x"
  by (subst add_commute) simp

end (* ab_near_semiring_one_zerol *)

class ab_pre_semiring_one_zerol = ab_near_semiring_one_zerol + ab_pre_semiring


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

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

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"


lemma select_alt: "x + y  {x,y}"
  by (simp add:

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


subclass dioid_one_zero ..

end (* selective_semiring *)