(* 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)" 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 (* 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 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" 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" (* 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 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 (* 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" 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" 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 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}" 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 (*selective_near_semiring*) class selective_semiring = selective_near_semiring + semiring_one_zero begin subclass dioid_one_zero .. end (* selective_semiring *) end