# Theory Partial_Semigroups

```(* Title: Partial Semigroups
Author: Brijesh Dongol, Victor Gomes, Ian J Hayes, Georg Struth
Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
Georg Struth <g.struth@sheffield.ac.uk>
*)

section ‹Partial Semigroups›

theory Partial_Semigroups
imports Main

begin

notation times (infixl "⋅" 70)
and times (infixl "⊕" 70)

subsection ‹Partial Semigroups›

text ‹In this context, partiality is modelled by a definedness constraint \$D\$ instead of a bottom element,
which would make the algebra total. This is common practice in mathematics.›

class partial_times = times +
fixes D :: "'a ⇒ 'a ⇒ bool"

text ‹The definedness constraints for associativity state that the right-hand side of the associativity
law is defined if and only if the left-hand side is and that, in this case, both sides are equal. This and
slightly different constraints can be found in the literature.›

class partial_semigroup = partial_times +
assumes add_assocD: "D y z ∧ D x (y ⋅ z) ⟷ D x y ∧ D (x ⋅ y) z"
and add_assoc: "D x y ∧ D (x ⋅ y) z ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"

text ‹Every semigroup is a partial semigroup.›

sublocale semigroup_mult ⊆ sg: partial_semigroup _ "λx y. True"

context partial_semigroup
begin

text ‹The following abbreviation is useful for sublocale statements.›

abbreviation (input) "R x y z ≡ D y z ∧ x = y ⋅ z"

lemma add_assocD_var1: "D y z ∧ D x (y ⋅ z) ⟹ D x y ∧ D (x ⋅ y) z"

lemma add_assocD_var2: " D x y ∧ D (x ⋅ y) z ⟹ D y z ∧ D x (y ⋅ z)"

lemma add_assoc_var: " D y z ∧ D x (y ⋅ z) ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"

subsection ‹Green's Preorders and Green's Relations›

text ‹We define the standard Green's preorders and Green's relations. They are usually defined on monoids.
On (partial) semigroups, we only obtain transitive relations.›

definition gR_rel :: "'a ⇒ 'a ⇒ bool" (infix "≼⇩R" 50) where
"x ≼⇩R y = (∃z. D x z ∧ x ⋅ z = y)"

definition strict_gR_rel :: "'a ⇒ 'a ⇒ bool" (infix "≺⇩R" 50) where
"x ≺⇩R y = (x ≼⇩R y ∧ ¬ y ≼⇩R x)"

definition gL_rel :: "'a ⇒ 'a ⇒ bool" (infix "≼⇩L" 50) where
"x ≼⇩L y = (∃z. D z x ∧ z ⋅ x = y)"

definition strict_gL_rel :: "'a ⇒ 'a ⇒ bool" (infix "≺⇩L" 50) where
"x ≺⇩L y = (x ≼⇩L y ∧ ¬ y ≼⇩L x)"

definition gH_rel :: "'a ⇒ 'a ⇒ bool" (infix "≼⇩H" 50) where
"x ≼⇩H y = (x ≼⇩L y ∧ x ≼⇩R y)"

definition gJ_rel :: "'a ⇒ 'a ⇒ bool" (infix "≼⇩J" 50) where
"x ≼⇩J y = (∃v w. D v x ∧ D (v ⋅ x) w ∧ (v ⋅ x) ⋅ w = y)"

definition "gR x y = (x ≼⇩R y ∧ y ≼⇩R x)"

definition "gL x y = (x ≼⇩L y ∧ y ≼⇩L x)"

definition "gH x y = (x ≼⇩H y ∧ y ≼⇩H x)"

definition "gJ x y = (x ≼⇩J y ∧ y ≼⇩J x)"

definition gR_downset :: "'a ⇒ 'a set" ("_↓" [100]100) where
"x↓ ≡ {y. y ≼⇩R x}"

text ‹The following counterexample rules out reflexivity.›

lemma "x ≼⇩R x" (* nitpick [expect=genuine] *)
oops

lemma gR_rel_trans: "x ≼⇩R y ⟹ y ≼⇩R z ⟹ x ≼⇩R z"

lemma gL_rel_trans: "x ≼⇩L y ⟹ y ≼⇩L z ⟹ x ≼⇩L z"

lemma gR_add_isol: "D z y ⟹ x ≼⇩R y ⟹ z ⋅ x ≼⇩R z ⋅ y"

lemma gL_add_isor: "D y z ⟹ x ≼⇩L y ⟹ x ⋅ z ≼⇩L y ⋅ z"

definition annil :: "'a ⇒ bool" where
"annil x = (∀y. D x y ∧ x ⋅ y = x)"

definition annir :: "'a ⇒ bool" where
"annir x = (∀y. D y x ∧ y ⋅ x = x)"

end

subsection ‹Morphisms›

definition ps_morphism :: "('a::partial_semigroup ⇒ 'b::partial_semigroup) ⇒ bool" where
"ps_morphism f = (∀x y. D x y ⟶ D (f x) (f y) ∧ f (x ⋅ y) = (f x) ⋅ (f y))"

definition strong_ps_morphism :: "('a::partial_semigroup ⇒ 'b::partial_semigroup) ⇒ bool" where
"strong_ps_morphism f = (ps_morphism f ∧ (∀x y. D (f x) (f y) ⟶ D x y))"

subsection ‹ Locally Finite Partial Semigroups›

text ‹In locally finite partial semigroups,  elements can only be split in finitely many ways.›

class locally_finite_partial_semigroup = partial_semigroup +
assumes loc_fin: "finite (x↓)"

subsection ‹Cancellative Partial Semigroups›

class cancellative_partial_semigroup = partial_semigroup +
assumes add_cancl: "D z x ⟹ D z y ⟹ z ⋅ x = z ⋅ y ⟹ x = y"
and add_cancr: "D x z ⟹ D y z ⟹ x ⋅ z = y ⋅ z ⟹ x = y"

begin

lemma unique_resl: "D x z ⟹ D x z' ⟹ x ⋅ z = y ⟹ x ⋅ z' = y ⟹ z = z'"

lemma unique_resr: "D z x ⟹ D z' x  ⟹ z ⋅ x = y ⟹ z' ⋅ x = y ⟹ z = z'"

lemma gR_rel_mult: "D x y ⟹ x ≼⇩R x ⋅ y"
using gR_rel_def by force

lemma gL_rel_mult: "D x y ⟹ y ≼⇩L x ⋅ y"
using gL_rel_def by force

text ‹By cancellation, the element z is uniquely defined for each pair x y, provided it exists.
In both cases, z is therefore a function of x and y; it is a quotient or residual of x y.›

lemma quotr_unique: "x ≼⇩R y  ⟹ (∃!z. D x z ∧ y = x ⋅ z)"

lemma quotl_unique: "x ≼⇩L y ⟹ (∃!z. D z x ∧ y = z ⋅ x)"
using gL_rel_def unique_resr by force

definition "rquot y x = (THE z. D x z ∧ x ⋅ z = y)"

definition "lquot y x = (THE z. D z x ∧ z ⋅ x = y)"

lemma rquot_prop: "D x z ∧ y = x ⋅ z ⟹ z = rquot y x"
by (metis (mono_tags, lifting) rquot_def the_equality unique_resl)

lemma rquot_mult: "x ≼⇩R y ⟹ z = rquot y x ⟹ x ⋅ z = y"
using gR_rel_def rquot_prop by force

lemma rquot_D: "x ≼⇩R y ⟹ z = rquot y x ⟹ D x z"
using gR_rel_def rquot_prop by force

lemma add_rquot: "x ≼⇩R y ⟹ (D x z ∧ x ⊕ z = y ⟷ z = rquot y x)"
using gR_rel_def rquot_prop by fastforce

lemma add_canc1: "D x y ⟹ rquot (x ⋅ y) x = y"
using rquot_prop by simp

lemma add_canc2: "x ≼⇩R y ⟹ x ⋅ (rquot y x) = y"

lemma add_canc2_prop: "x ≼⇩R y ⟹ rquot y x ≼⇩L y"
using gL_rel_mult rquot_D rquot_mult by fastforce

text ‹The next set of lemmas establishes standard Galois connections for cancellative partial semigroups.›

lemma gR_galois_imp1: "D x z ⟹ x ⋅ z ≼⇩R y ⟹ z ≼⇩R rquot y x"

lemma gR_galois_imp21: "x ≼⇩R y ⟹ z ≼⇩R rquot y x ⟹ x ⋅ z ≼⇩R y"
using gR_add_isol rquot_D rquot_mult by fastforce

lemma gR_galois_imp22: "x ≼⇩R y ⟹ z ≼⇩R rquot y x ⟹ D x z"

lemma gR_galois: "x ≼⇩R y ⟹ (D x z ∧ x ⋅ z ≼⇩R y ⟷ z ≼⇩R rquot y x)"
using gR_galois_imp1 gR_galois_imp21 gR_galois_imp22  by blast

lemma gR_rel_defined: "x ≼⇩R y ⟹ D x (rquot y x)"

lemma ex_add_galois: "D x z ⟹ (∃y. x ⋅ z = y ⟷ rquot y x = z)"

end

subsection ‹Partial Monoids›

text ‹We allow partial monoids with multiple units. This is similar to and inspired by small categories.›

class partial_monoid = partial_semigroup +
fixes E :: "'a set"
assumes unitl_ex: "∃e ∈ E. D e x ∧ e ⋅ x = x"
and unitr_ex: "∃e ∈ E. D x e ∧ x ⋅ e = x"
and units_eq: "e1 ∈ E ⟹ e2 ∈ E ⟹ D e1 e2 ⟹ e1 = e2"

text ‹Every monoid is a partial monoid.›

sublocale monoid_mult ⊆ mon: partial_monoid _ "λx y. True" "{1}"
by (standard; simp_all)

context partial_monoid
begin

lemma units_eq_var: "e1 ∈ E ⟹ e2 ∈ E ⟹ e1 ≠ e2 ⟹ ¬ D e1 e2"
using units_eq by force

text ‹In partial monoids, Green's relations become preorders, but need not be partial orders.›

sublocale gR: preorder gR_rel strict_gR_rel
apply standard
using gR_rel_def unitr_ex apply force
using gR_rel_trans by blast

sublocale gL: preorder gL_rel strict_gL_rel
apply standard
using gL_rel_def unitl_ex apply force
using gL_rel_trans by blast

lemma "x ≼⇩R y ⟹ y ≼⇩R x ⟹ x = y" (* nitpick [expect=genuine] *)
oops

lemma "annil x ⟹ annil y ⟹ x = y" (* nitpick [expext=genuine] *)
oops

lemma  "annir x ⟹ annir y ⟹ x = y" (* nitpick [expect=genuine] *)
oops

end

text ‹Next we define partial monoid morphisms.›

definition pm_morphism :: "('a::partial_monoid ⇒ 'b::partial_monoid) ⇒ bool" where
"pm_morphism f = (ps_morphism f ∧ (∀e. e ∈ E ⟶ (f e) ∈ E))"

definition strong_pm_morphism :: "('a::partial_monoid ⇒ 'b::partial_monoid) ⇒ bool" where
"strong_pm_morphism f = (pm_morphism f ∧ (∀e. (f e) ∈ E ⟶ e ∈ E))"

text ‹Partial Monoids with a single unit form a special case.›

class partial_monoid_one = partial_semigroup + one +
assumes oneDl: "D x 1"
and oneDr: "D 1 x"
and oner: "x ⋅ 1 = x"
and onel: "1 ⋅ x = x"

begin

sublocale pmo: partial_monoid _ _ "{1}"
by standard (simp_all add: oneDr onel oneDl oner)

end

subsection ‹Cancellative Partial Monoids›

class cancellative_partial_monoid = cancellative_partial_semigroup + partial_monoid

begin

lemma canc_unitr: "D x e ⟹ x ⋅ e = x ⟹ e ∈ E"

lemma canc_unitl: "D e x ⟹ e ⋅ x = x ⟹ e ∈ E"

end

subsection ‹Positive Partial Monoids›

class positive_partial_monoid  = partial_monoid +
assumes posl: "D x y ⟹ x ⋅ y ∈ E ⟹ x ∈ E"
and posr: "D x y ⟹ x ⋅ y ∈ E ⟹ y ∈ E"

begin

lemma pos_unitl: "D x y ⟹ e ∈ E ⟹ x ⋅ y = e ⟹ x = e"
by (metis posl posr unitr_ex units_eq_var)

lemma pos_unitr: "D x y ⟹ e ∈ E ⟹ x ⋅ y = e ⟹ y = e"
by (metis posl posr unitr_ex units_eq_var)

end

subsection ‹Positive Cancellative Partial Monoids›

class positive_cancellative_partial_monoid = positive_partial_monoid + cancellative_partial_monoid

begin

text ‹In positive cancellative monoids, the Green's relations are partial orders.›

sublocale pcpmR: order gR_rel strict_gR_rel
apply standard
apply (clarsimp simp: gR_rel_def)

sublocale pcpmL: order gL_rel strict_gL_rel
apply standard
apply (clarsimp simp: gL_rel_def)

end

subsection ‹From Partial Abelian Semigroups to Partial Abelian Monoids›

text ‹Next we define partial abelian semigroups. These are interesting, e.g., for the foundations
of quantum mechanics and as resource monoids in separation logic.›

class pas = partial_semigroup +
assumes add_comm: "D x y ⟹ D y x ∧ x ⊕ y = y ⊕ x"

begin

lemma D_comm: "D x y ⟷ D y x"

lemma add_comm': "D x y ⟹ x ⊕ y = y ⊕ x"

lemma gL_gH_rel: "(x ≼⇩L y) = (x ≼⇩H y)"
apply (simp add: gH_rel_def gL_rel_def gR_rel_def)

lemma gR_gH_rel: "(x ≼⇩R y) = (x ≼⇩H y)"
apply (simp add: gH_rel_def gL_rel_def gR_rel_def)

lemma annilr: "annil x = annir x"

lemma anni_unique: "annil x ⟹ annil y ⟹ x = y"
by (metis annilr annil_def annir_def)

end

text ‹The following classes collect families of partially ordered abelian semigroups and monoids.›

class locally_finite_pas = pas + locally_finite_partial_semigroup

class pam = pas + partial_monoid

class cancellative_pam = pam + cancellative_partial_semigroup

class positive_pam = pam + positive_partial_monoid

class positive_cancellative_pam  = positive_pam + cancellative_pam

class generalised_effect_algebra = pas + partial_monoid_one

class cancellative_pam_one = cancellative_pam + partial_monoid_one

class positive_cancellative_pam_one = positive_cancellative_pam  + cancellative_pam_one

context cancellative_pam_one
begin

lemma E_eq_one: "E = {1}"
by (metis oneDr oner unitl_ex units_eq singleton_iff subsetI subset_antisym)

lemma one_in_E: "1 ∈ E"

end

subsection ‹Alternative Definitions›

text ‹PAS's can be axiomatised more compactly as follows.›

class pas_alt = partial_times +
assumes pas_alt_assoc: "D x y ∧ D (x ⊕ y) z ⟹ D y z ∧ D x (y ⊕ z) ∧ (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
and pas_alt_comm: "D x y ⟹ D y x ∧ x ⊕ y = y ⊕ x"

sublocale pas_alt ⊆ palt: pas
apply standard
using pas_alt_assoc pas_alt_comm by blast+

text ‹Positive abelian PAM's can be axiomatised more compactly as well.›

class pam_pos_alt = pam +
assumes pos_alt: "D x y ⟹ e ∈ E ⟹ x ⊕ y = e ⟹ x = e"

sublocale pam_pos_alt ⊆ ppalt: positive_pam
apply standard
using pos_alt apply force

subsection ‹Product Constructions›

text ‹We consider two kinds of product construction. The first one combines partial semigroups with sets,
the second one partial semigroups with partial semigroups. The first one is interesting for
Separation Logic. Semidirect product constructions are considered later.›

instantiation prod :: (type, partial_semigroup) partial_semigroup
begin

definition "D_prod x y = (fst x = fst y ∧ D (snd x) (snd y))"
for x y :: "'a × 'b"

definition times_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
"times_prod x y = (fst x, snd x ⋅ snd y)"

instance
apply (standard, simp_all add: D_prod_def times_prod_def)

end

instantiation prod :: (type, partial_monoid) partial_monoid
begin

definition E_prod :: "('a × 'b) set" where
"E_prod = {x. snd x ∈ E}"

instance
apply (standard, simp_all add: D_prod_def times_prod_def E_prod_def)
using partial_monoid_class.unitl_ex apply fastforce
using partial_monoid_class.unitr_ex apply fastforce

end

instance prod :: (type, pas) pas
apply (standard, simp add: D_prod_def times_prod_def)

lemma prod_div1: "(x1::'a, y1::'b::pas) ≼⇩R (x2::'a, y2::'b::pas) ⟹ x1 = x2"
by (force simp: partial_semigroup_class.gR_rel_def times_prod_def)

lemma prod_div2: "(x1, y1) ≼⇩R (x2, y2) ⟹ y1 ≼⇩R y2"
by (force simp: partial_semigroup_class.gR_rel_def D_prod_def times_prod_def)

lemma prod_div_eq: "(x1, y1) ≼⇩R (x2, y2) ⟷ x1 = x2 ∧ y1 ≼⇩R y2"
by (force simp: partial_semigroup_class.gR_rel_def D_prod_def times_prod_def)

instance prod :: (type, pam) pam
by standard

instance prod :: (type, cancellative_pam) cancellative_pam

lemma prod_res_eq: "(x1, y1) ≼⇩R (x2::'a,y2::'b::cancellative_pam)
⟹ rquot (x2, y2) (x1, y1) = (x1, rquot y2 y1)"
apply (clarsimp simp: partial_semigroup_class.gR_rel_def D_prod_def times_prod_def rquot_def)
apply (rule theI2 conjI)
apply force
by (rule the_equality, auto simp: add_cancl)

instance prod :: (type, positive_pam) positive_pam
apply (standard, simp_all add: E_prod_def D_prod_def times_prod_def)
using positive_partial_monoid_class.posl apply blast
using positive_partial_monoid_class.posr by blast

instance prod :: (type, positive_cancellative_pam) positive_cancellative_pam ..

instance prod :: (type, locally_finite_pas) locally_finite_pas
proof (standard, case_tac x, clarsimp)
fix s :: 'a and x :: 'b
have "finite (x↓)"
hence "finite {y. ∃z. D y z ∧ y ⊕ z = x}"
hence "finite {(s, y)| y. ∃z. D y z ∧ y ⊕ z = x}"
by (drule_tac f="λy. (s, y)" in finite_image_set)
moreover have "{y. ∃z1 z2. D y (z1, z2) ∧ y ⊕ (z1, z2) = (s, x)}
⊆ {(s, y)| y. ∃z. D y z ∧ y ⊕ z = x}"
by (auto simp: D_prod_def times_prod_def)
ultimately have "finite {y. ∃z1 z2. D y (z1, z2) ∧ y ⊕ (z1, z2) = (s, x)}"
by (auto intro: finite_subset)
thus "finite ((s, x)↓)"
qed

text ‹Next we consider products of two partial semigroups.›

definition ps_prod_D :: "'a :: partial_semigroup × 'b :: partial_semigroup ⇒ 'a × 'b  ⇒ bool"
where "ps_prod_D x y ≡ D (fst x) (fst y) ∧ D (snd x) (snd y)"

definition ps_prod_times :: "'a :: partial_semigroup × 'b :: partial_semigroup ⇒ 'a × 'b ⇒ 'a × 'b"
where "ps_prod_times x y = (fst x ⋅ fst y, snd x ⋅ snd y)"

interpretation ps_prod: partial_semigroup ps_prod_times ps_prod_D
apply (standard, simp_all add: ps_prod_D_def ps_prod_times_def)

interpretation pas_prod: pas ps_prod_times "ps_prod_D :: 'a :: pas × 'b :: pas ⇒ 'a × 'b  ⇒ bool"
by (standard, clarsimp simp: ps_prod_D_def ps_prod_times_def pas_class.add_comm)

definition pm_prod_E :: "('a :: partial_monoid × 'b :: partial_monoid) set" where
"pm_prod_E = {x. fst x ∈ E ∧ snd x ∈ E}"

interpretation pm_prod: partial_monoid ps_prod_times ps_prod_D pm_prod_E
apply standard
apply (simp_all add: ps_prod_times_def ps_prod_D_def pm_prod_E_def)
apply (metis partial_monoid_class.unitl_ex prod.collapse)
apply (metis partial_monoid_class.unitr_ex prod.collapse)

interpretation pam_prod: pam ps_prod_times ps_prod_D "pm_prod_E :: ('a :: pam × 'a :: pam) set" ..

subsection ‹Partial Semigroup Actions and Semidirect Products›

text ‹(Semi)group actions are a standard mathematical construction. We generalise this to partial
semigroups and monoids. We use it to define semidirect products of partial semigroups. A generalisation
to wreath products might be added in the future.›

text ‹First we define the (left) action of a partial semigroup on a set. A right action could be defined in a similar way,
but we do not pursue this at the moment.›

locale partial_sg_laction =
fixes Dla :: "'a::partial_semigroup ⇒ 'b ⇒ bool"
and act :: "'a::partial_semigroup ⇒ 'b ⇒ 'b" ("α")
assumes act_assocD: "D x y ∧ Dla (x ⋅ y) p ⟷ Dla y p ∧ Dla x (α y p)"
and act_assoc: "D x y ∧ Dla (x ⋅ y) p ⟹ α (x ⋅ y) p = α x (α y p)"

text ‹Next we define the action of a partial semigroup on another partial semigroup.
In the tradition of semigroup theory we use addition as a non-commutative operation for the second semigroup.›

locale partial_sg_sg_laction = partial_sg_laction +
assumes act_distribD: "D (p::'b::partial_semigroup) q ∧ Dla (x::'a::partial_semigroup) (p ⊕ q) ⟷ Dla x p ∧ Dla x q ∧ D (α x p) (α x q)"
and act_distrib: "D p q ∧ Dla x (p ⊕ q) ⟹ α x (p ⊕ q) = (α x p) ⊕ (α x q)"

begin

text ‹Next we define the semidirect product as a partial operation and show that the semidirect
product of two partial semigroups forms a partial semigroup.›

definition sd_D :: "('a × 'b) ⇒ ('a × 'b) ⇒ bool" where
"sd_D x y ≡ D (fst x) (fst y) ∧ Dla (fst x) (snd y) ∧ D (snd x) (α (fst x) (snd y))"

definition sd_prod :: "('a × 'b) ⇒ ('a × 'b) ⇒ ('a × 'b)" where
"sd_prod x y = ((fst x) ⋅ (fst y), (snd x) ⊕ (α (fst x) (snd y)))"

sublocale dp_semigroup: partial_semigroup sd_prod sd_D
apply unfold_locales
apply (clarsimp, metis act_assoc act_assocD act_distrib act_distribD add_assocD)

end

text ‹Finally we define the semigroup action for two partial monoids and show that the semidirect product of two partial monoids
is a partial monoid.›

locale partial_mon_sg_laction = partial_sg_sg_laction Dla
for Dla :: "'a::partial_monoid ⇒ 'b::partial_semigroup ⇒ bool" +
assumes act_unitl: "e ∈ E ⟹ Dla e p ∧ α e p = p"

locale partial_mon_mon_laction = partial_mon_sg_laction _ Dla
for Dla :: "'a::partial_monoid ⇒ 'b::partial_monoid ⇒ bool" +
assumes act_annir: "e ∈ Ea ⟹ Dla x e ∧ α x e = e"

begin

definition sd_E :: "('a × 'b) set" where
"sd_E = {x. fst x ∈ E ∧ snd x ∈ E}"

sublocale dp_semigroup : partial_monoid sd_prod sd_D sd_E
apply unfold_locales
apply (simp_all add: sd_prod_def sd_D_def sd_E_def)
apply (metis act_annir eq_fst_iff eq_snd_iff mem_Collect_eq partial_monoid_class.unitl_ex)
apply (metis act_annir eq_fst_iff eq_snd_iff partial_monoid_class.unitr_ex)
by (metis act_annir partial_monoid_class.units_eq prod_eqI)

end

end
```