Theory Stone_Relation_Algebras.Semirings

(* Title:      Semirings
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at>

section ‹Semirings›

text ‹
This theory develops a hierarchy of idempotent semirings.
All kinds of semiring considered here are bounded semilattices, but many lack additional properties typically assumed for semirings.
In particular, we consider the variants of semirings, in which
\item multiplication is not required to be associative;
\item a right zero and unit of multiplication need not exist;
\item multiplication has a left residual;
\item multiplication from the left is not required to distribute over addition;
\item the semilattice order has a greatest element.
We have applied results from this theory a number of papers for unifying computation models.
For example, see cite"Guttmann2012c" for various relational and matrix-based computation models and cite"BerghammerGuttmann2015b" for multirelational models.

The main results in this theory relate different ways of defining reflexive-transitive closures as discussed in cite"BerghammerGuttmann2015b".

theory Semirings

imports Fixpoints


subsection ‹Idempotent Semirings›

text ‹
The following definitions are standard for relations.
Putting them into a general class that depends only on the signature facilitates reuse.
Coreflexives are sometimes called partial identities, subidentities, monotypes or tests.

class times_one_ord = times + one + ord

abbreviation reflexive   :: "'a  bool" where "reflexive x    1  x"
abbreviation coreflexive :: "'a  bool" where "coreflexive x  x  1"

abbreviation transitive  :: "'a  bool" where "transitive x   x * x  x"
abbreviation dense_rel   :: "'a  bool" where "dense_rel x    x  x * x"
abbreviation idempotent  :: "'a  bool" where "idempotent x   x * x = x"

abbreviation preorder    :: "'a  bool" where "preorder x     reflexive x  transitive x"

abbreviation "coreflexives  { x . coreflexive x }"


text ‹
The first algebra is a very weak idempotent semiring, in which multiplication is not necessarily associative.

class non_associative_left_semiring = bounded_semilattice_sup_bot + times + one +
  assumes mult_left_sub_dist_sup: "x * y  x * z  x * (y  z)"
  assumes mult_right_dist_sup: "(x  y) * z = x * z  y * z"
  assumes mult_left_zero [simp]: "bot * x = bot"
  assumes mult_left_one [simp]: "1 * x = x"
  assumes mult_sub_right_one: "x  x * 1"

subclass times_one_ord .

text ‹
We first show basic isotonicity and subdistributivity properties of multiplication.

lemma mult_left_isotone:
  "x  y  x * z  y * z"
  using mult_right_dist_sup sup_right_divisibility by auto

lemma mult_right_isotone:
  "x  y  z * x  z * y"
  using mult_left_sub_dist_sup sup.bounded_iff sup_right_divisibility by auto

lemma mult_isotone:
  "w  y  x  z  w * x  y * z"
  using order_trans mult_left_isotone mult_right_isotone by blast

lemma affine_isotone:
  "isotone (λx . y * x  z)"
  using isotone_def mult_right_isotone sup_left_isotone by auto

lemma mult_left_sub_dist_sup_left:
  "x * y  x * (y  z)"
  by (simp add: mult_right_isotone)

lemma mult_left_sub_dist_sup_right:
  "x * z  x * (y  z)"
  by (simp add: mult_right_isotone)

lemma mult_right_sub_dist_sup_left:
  "x * z  (x  y) * z"
  by (simp add: mult_left_isotone)

lemma mult_right_sub_dist_sup_right:
  "y * z  (x  y) * z"
  by (simp add: mult_left_isotone)

lemma case_split_left:
  assumes "1  w  z"
      and "w * x  y"
      and "z * x  y"
    shows "x  y"
proof -
  have "(w  z) * x  y"
    by (simp add: assms(2-3) mult_right_dist_sup)
  thus ?thesis
    by (metis assms(1) dual_order.trans mult_left_one mult_left_isotone)

lemma case_split_left_equal:
  "w  z = 1  w * x = w * y  z * x = z * y  x = y"
  by (metis mult_left_one mult_right_dist_sup)

text ‹
Next we consider under which semiring operations the above properties are closed.

lemma reflexive_one_closed:
  "reflexive 1"
  by simp

lemma reflexive_sup_closed:
  "reflexive x  reflexive (x  y)"
  by (simp add: le_supI1)

lemma reflexive_mult_closed:
  "reflexive x  reflexive y  reflexive (x * y)"
  using mult_isotone by fastforce

lemma coreflexive_bot_closed:
  "coreflexive bot"
  by simp

lemma coreflexive_one_closed:
  "coreflexive 1"
  by simp

lemma coreflexive_sup_closed:
  "coreflexive x  coreflexive y  coreflexive (x  y)"
  by simp

lemma coreflexive_mult_closed:
  "coreflexive x  coreflexive y  coreflexive (x * y)"
  using mult_isotone by fastforce

lemma transitive_bot_closed:
  "transitive bot"
  by simp

lemma transitive_one_closed:
  "transitive 1"
  by simp

lemma dense_bot_closed:
  "dense_rel bot"
  by simp

lemma dense_one_closed:
  "dense_rel 1"
  by simp

lemma dense_sup_closed:
  "dense_rel x  dense_rel y  dense_rel (x  y)"
  by (metis mult_right_dist_sup order_lesseq_imp sup.mono mult_left_sub_dist_sup_left mult_left_sub_dist_sup_right)

lemma idempotent_bot_closed:
  "idempotent bot"
  by simp

lemma idempotent_one_closed:
  "idempotent 1"
  by simp

lemma preorder_one_closed:
  "preorder 1"
  by simp

lemma coreflexive_transitive:
  "coreflexive x  transitive x"
  using mult_left_isotone by fastforce

lemma preorder_idempotent:
  "preorder x  idempotent x"
  using order.antisym mult_isotone by fastforce

text ‹
We study the following three ways of defining reflexive-transitive closures.
Each of them is given as a least prefixpoint, but the underlying functions are different.
They implement left recursion, right recursion and symmetric recursion, respectively.

abbreviation Lf :: "'a  ('a  'a)" where "Lf y  (λx . 1  x * y)"
abbreviation Rf :: "'a  ('a  'a)" where "Rf y  (λx . 1  y * x)"
abbreviation Sf :: "'a  ('a  'a)" where "Sf y  (λx . 1  y  x * x)"

abbreviation lstar :: "'a  'a" where "lstar y   (Lf y)"
abbreviation rstar :: "'a  'a" where "rstar y   (Rf y)"
abbreviation sstar :: "'a  'a" where "sstar y   (Sf y)"

text ‹
All functions are isotone and, therefore, if the prefixpoints exist they are also fixpoints.

lemma lstar_rec_isotone:
  "isotone (Lf y)"
  using isotone_def sup_right_divisibility sup_right_isotone mult_right_sub_dist_sup_right by auto

lemma rstar_rec_isotone:
  "isotone (Rf y)"
  using isotone_def sup_right_divisibility sup_right_isotone mult_left_sub_dist_sup_right by auto

lemma sstar_rec_isotone:
  "isotone (Sf y)"
  using isotone_def sup_right_isotone mult_isotone by auto

lemma lstar_fixpoint:
  "has_least_prefixpoint (Lf y)  lstar y = μ (Lf y)"
  by (simp add: pmu_mu lstar_rec_isotone)

lemma rstar_fixpoint:
  "has_least_prefixpoint (Rf y)  rstar y = μ (Rf y)"
  by (simp add: pmu_mu rstar_rec_isotone)

lemma sstar_fixpoint:
  "has_least_prefixpoint (Sf y)  sstar y = μ (Sf y)"
  by (simp add: pmu_mu sstar_rec_isotone)

lemma sstar_increasing:
  "has_least_prefixpoint (Sf y)  y  sstar y"
  using order_trans pmu_unfold sup_ge1 sup_ge2 by blast

text ‹
The fixpoint given by right recursion is always below the one given by symmetric recursion.

lemma rstar_below_sstar:
  assumes "has_least_prefixpoint (Rf y)"
      and "has_least_prefixpoint (Sf y)"
    shows "rstar y  sstar y"
proof -
  have "y  sstar y"
    using assms(2) pmu_unfold by force
  hence "Rf y (sstar y)  Sf y (sstar y)"
    by (meson sup.cobounded1 sup.mono mult_left_isotone)
  also have "...  sstar y"
    using assms(2) pmu_unfold by blast
  finally show ?thesis
    using assms(1) is_least_prefixpoint_def least_prefixpoint by auto


text ‹
Our next structure adds one half of the associativity property.
This inequality holds, for example, for multirelations under the compositions defined by Parikh and Peleg cite"Parikh1983" and "Peleg1987".
The converse inequality requires up-closed multirelations for Parikh's composition.

class pre_left_semiring = non_associative_left_semiring +
  assumes mult_semi_associative: "(x * y) * z  x * (y * z)"

lemma mult_one_associative [simp]:
  "x * 1 * y = x * y"
  by (metis dual_order.antisym mult_left_isotone mult_left_one mult_semi_associative mult_sub_right_one)

lemma mult_sup_associative_one:
  "(x * (y * 1)) * z  x * (y * z)"
  by (metis mult_semi_associative mult_one_associative)

lemma rstar_increasing:
  assumes "has_least_prefixpoint (Rf y)"
    shows "y  rstar y"
proof -
  have "Rf y (rstar y)  rstar y"
    using assms pmu_unfold by blast
  thus ?thesis
    by (metis le_supE mult_right_isotone mult_sub_right_one sup.absorb_iff2)


text ‹
For the next structure we add a left residual operation.
Such a residual is available, for example, for multirelations.

The operator notation for binary division is introduced in a class that requires a unary inverse.
This is appropriate for fields, but too strong in the present context of semirings.
We therefore reintroduce it without requiring a unary inverse.

  inverse_divide (infixl "'/" 70)

  divide (infixl "'/" 70)

class residuated_pre_left_semiring = pre_left_semiring + divide +
  assumes lres_galois: "x * y  z  x  z / y"

text ‹
We first derive basic properties of left residuals from the Galois connection.

lemma lres_left_isotone:
  "x  y  x / z  y / z"
  using dual_order.trans lres_galois by blast

lemma lres_right_antitone:
  "x  y  z / y  z / x"
  using dual_order.trans lres_galois mult_right_isotone by blast

lemma lres_inverse:
  "(x / y) * y  x"
  by (simp add: lres_galois)

lemma lres_one:
  "x / 1  x"
  using mult_sub_right_one order_trans lres_inverse by blast

lemma lres_mult_sub_lres_lres:
  "x / (z * y)  (x / y) / z"
  using lres_galois mult_semi_associative order.trans by blast

lemma mult_lres_sub_assoc:
  "x * (y / z)  (x * y) / z"
  by (meson dual_order.trans lres_galois mult_right_isotone lres_inverse lres_mult_sub_lres_lres)

text ‹
With the help of a left residual, it follows that left recursion is below right recursion.

lemma lstar_below_rstar:
  assumes "has_least_prefixpoint (Lf y)"
      and "has_least_prefixpoint (Rf y)"
    shows "lstar y  rstar y"
proof -
  have "y * (rstar y / y) * y  y * rstar y"
    using lres_galois mult_lres_sub_assoc by auto
  also have "...  rstar y"
    using assms(2) le_supE pmu_unfold by blast
  finally have "y * (rstar y / y)  rstar y / y"
    by (simp add: lres_galois)
  hence "Rf y (rstar y / y)  rstar y / y"
    using assms(2) lres_galois rstar_increasing by fastforce
  hence "rstar y  rstar y / y"
    using assms(2) is_least_prefixpoint_def least_prefixpoint by auto
  hence "Lf y (rstar y)  rstar y"
    using assms(2) lres_galois pmu_unfold by fastforce
  thus ?thesis
    using assms(1) is_least_prefixpoint_def least_prefixpoint by auto

text ‹
Moreover, right recursion gives the same result as symmetric recursion.
The next proof follows an argument of cite‹Satz 10.1.5› in "Berghammer2012".

lemma rstar_sstar:
  assumes "has_least_prefixpoint (Rf y)"
      and "has_least_prefixpoint (Sf y)"
    shows "rstar y = sstar y"
proof -
  have "Rf y (rstar y / rstar y) * rstar y  rstar y  y * ((rstar y / rstar y) * rstar y)"
    using mult_right_dist_sup mult_semi_associative sup_right_isotone by auto
  also have "...  rstar y  y * rstar y"
    using mult_right_isotone sup_right_isotone lres_inverse by blast
  also have "...  rstar y"
    using assms(1) pmu_unfold by fastforce
  finally have "Rf y (rstar y / rstar y)  rstar y / rstar y"
    by (simp add: lres_galois)
  hence "rstar y * rstar y  rstar y"
    using assms(1) is_least_prefixpoint_def least_prefixpoint lres_galois by auto
  hence "y  rstar y * rstar y  rstar y"
    by (simp add: assms(1) rstar_increasing)
  hence "Sf y (rstar y)  rstar y"
    using assms(1) pmu_unfold by force
  hence "sstar y  rstar y"
    using assms(2) is_least_prefixpoint_def least_prefixpoint by auto
  thus ?thesis
    by (simp add: assms order.antisym rstar_below_sstar)


context monoid_mult

lemma monoid_power_closed:
  assumes "P 1" "P x" "y z . P y  P z  P (y * z)"
    shows "P (x ^ n)"
proof (induct n)
  case 0
  thus ?case
    by (simp add: assms(1))
  case (Suc n)
  thus ?case
    by (simp add: assms(2,3))


text ‹
In the next structure we add full associativity of multiplication, as well as a right unit.
Still, multiplication does not need to have a right zero and does not need to distribute over addition from the left.

class idempotent_left_semiring = non_associative_left_semiring + monoid_mult

subclass pre_left_semiring
  by unfold_locales (simp add: mult_assoc)

lemma zero_right_mult_decreasing:
  "x * bot  x"
  by (metis bot_least mult_1_right mult_right_isotone)

text ‹
The following result shows that for dense coreflexives there are two equivalent ways to express that a property is preserved.
In the setting of Kleene algebras, this is well known for tests, which form a Boolean subalgebra.
The point here is that only very few properties of tests are needed to show the equivalence.

lemma test_preserves_equation:
  assumes "dense_rel p"
      and "coreflexive p"
    shows "p * x  x * p  p * x = p * x * p"
  assume 1: "p * x  x * p"
  have "p * x  p * p * x"
    by (simp add: assms(1) mult_left_isotone)
  also have "...  p * x * p"
    using 1 by (simp add: mult_right_isotone mult_assoc)
  finally show "p * x = p * x * p"
    using assms(2) order.antisym mult_right_isotone by fastforce
  assume "p * x = p * x * p"
  thus "p * x  x * p"
    by (metis assms(2) mult_left_isotone mult_left_one)


text ‹
The next structure has both distributivity properties of multiplication.
Only a right zero is missing from full semirings.
This is important as many computation models do not have a right zero of sequential composition.

class idempotent_left_zero_semiring = idempotent_left_semiring +
  assumes mult_left_dist_sup: "x * (y  z) = x * y  x * z"

lemma case_split_right:
  assumes "1  w  z"
      and "x * w  y"
      and "x * z  y"
    shows "x  y"
proof -
  have "x * (w  z)  y"
    by (simp add: assms(2-3) mult_left_dist_sup)
  thus ?thesis
    by (metis assms(1) dual_order.trans mult_1_right mult_right_isotone)

lemma case_split_right_equal:
  "w  z = 1  x * w = y * w  x * z = y * z  x = y"
  by (metis mult_1_right mult_left_dist_sup)

text ‹
This is the first structure we can connect to the semirings provided by Isabelle/HOL.

sublocale semiring: ordered_semiring sup bot less_eq less times
  apply unfold_locales
  using sup_right_isotone apply blast
  apply (simp add: mult_right_dist_sup)
  apply (simp add: mult_left_dist_sup)
  apply (simp add: mult_right_isotone)
  by (simp add: mult_left_isotone)

sublocale semiring: semiring_numeral 1 times sup ..


text ‹
Completing this part of the hierarchy, we obtain idempotent semirings by adding a right zero of multiplication.

class idempotent_semiring = idempotent_left_zero_semiring +
  assumes mult_right_zero [simp]: "x * bot = bot"

sublocale semiring: semiring_0 sup bot times
  by unfold_locales simp_all


subsection ‹Bounded Idempotent Semirings›

text ‹
All of the following semirings have a greatest element in the underlying semilattice order.
With this element, we can express further standard properties of relations.
We extend each class in the above hierarchy in turn.

class times_top = times + top

abbreviation vector     :: "'a  bool" where "vector x      x * top = x"
abbreviation covector   :: "'a  bool" where "covector x    top * x = x"
abbreviation total      :: "'a  bool" where "total x       x * top = top"
abbreviation surjective :: "'a  bool" where "surjective x  top * x = top"

abbreviation "vectors    { x . vector x }"
abbreviation "covectors  { x . covector x }"


class bounded_non_associative_left_semiring = non_associative_left_semiring + top +
  assumes sup_right_top [simp]: "x  top = top"

subclass times_top .

text ‹
We first give basic properties of the greatest element.

lemma sup_left_top [simp]:
  "top  x = top"
  using sup_right_top sup.commute by fastforce

lemma top_greatest [simp]:
  "x  top"
  by (simp add: le_iff_sup)

lemma top_left_mult_increasing:
  "x  top * x"
  by (metis mult_left_isotone mult_left_one top_greatest)

lemma top_right_mult_increasing:
  "x  x * top"
  using mult_right_isotone mult_sub_right_one order_trans top_greatest by blast

lemma top_mult_top [simp]:
  "top * top = top"
  by (simp add: order.antisym top_left_mult_increasing)

text ‹
Closure of the above properties under the semiring operations is considered next.

lemma vector_bot_closed:
  "vector bot"
  by simp

lemma vector_top_closed:
  "vector top"
  by simp

lemma vector_sup_closed:
  "vector x  vector y  vector (x  y)"
  by (simp add: mult_right_dist_sup)

lemma covector_top_closed:
  "covector top"
  by simp

lemma total_one_closed:
  "total 1"
  by simp

lemma total_top_closed:
  "total top"
  by simp

lemma total_sup_closed:
  "total x  total (x  y)"
  by (simp add: mult_right_dist_sup)

lemma surjective_one_closed:
  "surjective 1"
  by (simp add: order.antisym mult_sub_right_one)

lemma surjective_top_closed:
  "surjective top"
  by simp

lemma surjective_sup_closed:
  "surjective x  surjective (x  y)"
  by (metis le_iff_sup mult_left_sub_dist_sup_left sup_left_top)

lemma reflexive_top_closed:
  "reflexive top"
  by simp

lemma transitive_top_closed:
  "transitive top"
  by simp

lemma dense_top_closed:
  "dense_rel top"
  by simp

lemma idempotent_top_closed:
  "idempotent top"
  by simp

lemma preorder_top_closed:
  "preorder top"
  by simp


text ‹
Some closure properties require at least half of associativity.

class bounded_pre_left_semiring = pre_left_semiring + bounded_non_associative_left_semiring

lemma vector_mult_closed:
  "vector y  vector (x * y)"
  by (metis order.antisym mult_semi_associative top_right_mult_increasing)

lemma surjective_mult_closed:
  "surjective x  surjective y  surjective (x * y)"
  by (metis order.antisym mult_semi_associative top_greatest)


text ‹
We next consider residuals with the greatest element.

class bounded_residuated_pre_left_semiring = residuated_pre_left_semiring + bounded_pre_left_semiring

lemma lres_top_decreasing:
  "x / top  x"
  using lres_inverse order.trans top_right_mult_increasing by blast

lemma top_lres_absorb [simp]:
  "top / x = top"
  using order.antisym lres_galois top_greatest by blast

lemma covector_lres_closed:
  "covector x  covector (x / y)"
  by (metis order.antisym mult_lres_sub_assoc top_left_mult_increasing)


text ‹
Some closure properties require full associativity.

class bounded_idempotent_left_semiring = bounded_pre_left_semiring + idempotent_left_semiring

lemma covector_mult_closed:
  "covector x  covector (x * y)"
  by (metis mult_assoc)

lemma total_mult_closed:
  "total x  total y  total (x * y)"
  by (simp add: mult_assoc)

lemma total_power_closed:
  "total x  total (x ^ n)"
  apply (rule monoid_power_closed)
  using total_mult_closed by auto

lemma surjective_power_closed:
  "surjective x  surjective (x ^ n)"
  apply (rule monoid_power_closed)
  using surjective_mult_closed by auto


text ‹
Some closure properties require distributivity from the left.

class bounded_idempotent_left_zero_semiring = bounded_idempotent_left_semiring + idempotent_left_zero_semiring

lemma covector_sup_closed:
  "covector x  covector y  covector (x  y)"
  by (simp add: mult_left_dist_sup)


text ‹
Our final structure is an idempotent semiring with a greatest element.

class bounded_idempotent_semiring = bounded_idempotent_left_zero_semiring + idempotent_semiring

lemma covector_bot_closed:
  "covector bot"
  by simp