Quelle  Dioid.thy

(* 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
 . A join semilattice (or upper semilattice) is either a
  in which every pair of elements has a join (or least upper
 ), or a set endowed with an associative, commutative, idempotent
  operation. It is well known that the order-theoretic definition
  the algebraic one and vice versa. We start from the algebraic
  because it is easily expandable to dioids, using
 's type class mechanism.

  Isabelle/HOL, a type class @{class semilattice_sup} is available.
 , we cannot use this type class because we need the symbol~‹+› for the join operation in the dioid expansion and subclass
  in Isabelle/HOL require the two type classes involved to have
  same fixed signature.

  {\em add\_assoc} as a name for the first assumption in class
 \em join\_semilattice} would lead to name clashes: we will later
  classes that inherit from @{class semigroup_add}, which
  its own assumption {\em add\_assoc}, and prove that these are
  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
  in class @{class plus_ord}.

  show some simple order-based properties of semilattices. The
  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
  least element with respect to the order, and therefore often
  by~‹⊥›. Semilattices with a least element are often
  \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
  of near rings to the semiring case. They have been
 , for instance, in G.~Pilz's book~cite‹"pilz83nearrings"› on
  rings. According to his definition, a near semiring consists of
  additive and a multiplicative semigroup that interact via a single
  law (left or right). The additive semigroup is not
  to be commutative. The definition is influenced by partial
  semigroups.

  only consider near semirings in which addition is commutative, and
  which the right distributivity law holds. We call such near
  \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
  is idempotent. This generalises the notion of (additively)
  semirings by dropping one distributivity law. Near dioids
  a starting point for process algebras.

  modelling variants of dioids as variants of semirings in which
  is idempotent we follow the tradition of
 ~cite‹"birkhoff67lattices"›, but deviate from the definitions
  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)
  reduct of a near dioid is a semilattice. Near dioids are
  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
  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
  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
  equivalent to left subdistributivity, as we have seen. The
  structures form the basis of probabilistic Kleene
 ~cite‹"mciverweber05pka"› and game
 ~cite‹"venema03gamealgebra"›. We are not aware that these
  have a special name, so we baptise them \emph{pre-dioids}.

  do not explicitly define pre-semirings since we have no application
  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})
  near semirings, and dioids from near dioids. Dioids are therefore
  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
  operation of finite iteration or Kleene star on dioids. We do not
  left and right units separately since we have no application
  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
  lead to annoying redundant proof obligations in mutual
  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 ‹
  now axiomatise an additive unit~$0$ for nearsemirings. The zero is
  required to satisfy annihilation properties with respect to
 . Due to applications we distinguish a zero which is
  a left annihilator from one that is also a right annihilator.
  briefly, we call zero either a left unit or a unit.

  and dioids with a right zero only can be obtained from those
  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 ‹
  the order of multiplication in a semiring (or dioid) gives
  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
  of \emph{dioid}. Some important models, e.g. max-plus and
 -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