# Theory Stone_Relation_Algebras.Semirings

(* Title:      Semirings
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

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
\begin{itemize}
\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.
\end{itemize}
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

begin

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
begin

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

end

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

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

lemma mult_left_sub_dist_sup_right:
"x * z ≤ x * (y ⊔ z)"

lemma mult_right_sub_dist_sup_left:
"x * z ≤ (x ⊔ y) * z"

lemma mult_right_sub_dist_sup_right:
"y * z ≤ (x ⊔ y) * z"

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"
thus ?thesis
by (metis assms(1) dual_order.trans mult_left_one mult_left_isotone)
qed

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

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 ≡ pμ (Lf y)"
abbreviation rstar :: "'a ⇒ 'a" where "rstar y ≡ pμ (Rf y)"
abbreviation sstar :: "'a ⇒ 'a" where "sstar y ≡ pμ (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)"

lemma rstar_fixpoint:
"has_least_prefixpoint (Rf y) ⟹ rstar y = μ (Rf y)"

lemma sstar_fixpoint:
"has_least_prefixpoint (Sf y) ⟹ sstar y = μ (Sf y)"

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
qed

end

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

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

end

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

no_notation
inverse_divide (infixl "'/" 70)

notation
divide (infixl "'/" 70)

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

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"

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

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

end

context monoid_mult
begin

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
next
case (Suc n)
thus ?case
qed

end

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
begin

subclass pre_left_semiring

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"
proof
assume 1: "p * x ≤ x * p"
have "p * x ≤ p * p * x"
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
next
assume "p * x = p * x * p"
thus "p * x ≤ x * p"
by (metis assms(2) mult_left_isotone mult_left_one)
qed

end

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

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"
thus ?thesis
by (metis assms(1) dual_order.trans mult_1_right mult_right_isotone)
qed

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

sublocale semiring: semiring_numeral 1 times sup ..

end

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

sublocale semiring: semiring_0 sup bot times
by unfold_locales simp_all

end

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
begin

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

end

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

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"

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"

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

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

lemma surjective_one_closed:
"surjective 1"

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

end

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

class bounded_pre_left_semiring = pre_left_semiring + bounded_non_associative_left_semiring
begin

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)

end

text ‹
We next consider residuals with the greatest element.
›

class bounded_residuated_pre_left_semiring = residuated_pre_left_semiring + bounded_pre_left_semiring
begin

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)

end

text ‹
Some closure properties require full associativity.
›

class bounded_idempotent_left_semiring = bounded_pre_left_semiring + idempotent_left_semiring
begin

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

lemma total_mult_closed:
"total x ⟹ total y ⟹ total (x * y)"

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

end

text ‹
Some closure properties require distributivity from the left.
›

class bounded_idempotent_left_zero_semiring = bounded_idempotent_left_semiring + idempotent_left_zero_semiring
begin

lemma covector_sup_closed:
"covector x ⟹ covector y ⟹ covector (x ⊔ y)"

end

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

class bounded_idempotent_semiring = bounded_idempotent_left_zero_semiring + idempotent_semiring
begin

lemma covector_bot_closed:
"covector bot"
by simp

end

end