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" 
  by standard (simp_all add: mult_assoc)

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"
  by (simp add: add_assocD)

lemma add_assocD_var2: " D x y ∧ D (x ⋅ y) z ⟹ D y z ∧ D x (y ⋅ z)"
  by (simp add: add_assocD)

lemma add_assoc_var: " D y z ∧ D x (y ⋅ z) ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
  by (simp add: add_assoc add_assocD)
    
    
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"
  by (metis gR_rel_def add_assoc add_assocD_var2)
    
lemma gL_rel_trans: "x ≼⇩L y ⟹ y ≼⇩L z ⟹ x ≼⇩L z"
  by (metis gL_rel_def add_assocD_var1 add_assoc_var) 
    
lemma gR_add_isol: "D z y ⟹ x ≼⇩R y ⟹ z ⋅ x ≼⇩R z ⋅ y" 
  apply (simp add: gR_rel_def)
  using add_assocD_var1 add_assoc_var by blast
    
lemma gL_add_isor: "D y z ⟹ x ≼⇩L y ⟹ x ⋅ z ≼⇩L y ⋅ z"    
  apply (simp add: gL_rel_def)
  by (metis add_assoc add_assocD_var2)
 
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'"
  by (simp add: add_cancl)
    
lemma unique_resr: "D z x ⟹ D z' x  ⟹ z ⋅ x = y ⟹ z' ⋅ x = y ⟹ z = z'"
  by (simp add: add_cancr)

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)"
  using gR_rel_def add_cancl by force

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"
  using gR_rel_def add_canc1 by force
    
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"    
  by (metis gR_rel_def add_assoc add_assocD_var2 rquot_prop)

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"
  using gR_rel_def add_assocD add_canc1 by fastforce

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)"
  by (simp add: rquot_D)
 
lemma ex_add_galois: "D x z ⟹ (∃y. x ⋅ z = y ⟷ rquot y x = z)"
  using add_canc1 by force
    

             
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
  apply (simp add: strict_gR_rel_def)
  using gR_rel_def unitr_ex apply force
  using gR_rel_trans by blast
    
sublocale gL: preorder gL_rel strict_gL_rel
  apply standard
  apply (simp add: strict_gL_rel_def)
  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"
  by (metis add_cancl unitr_ex)
    
lemma canc_unitl: "D e x ⟹ e ⋅ x = x ⟹ e ∈ E"
  by (metis add_cancr unitl_ex)
    
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)
  by (metis canc_unitr add_assoc add_assocD_var2 pos_unitl)
    
sublocale pcpmL: order gL_rel strict_gL_rel
  apply standard
  apply (clarsimp simp: gL_rel_def)
  by (metis canc_unitl add_assoc add_assocD_var1 pos_unitr)
  
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"
  by (auto simp add: add_comm)

lemma add_comm': "D x y ⟹ x ⊕ y = y ⊕ x"
  by (auto simp add: add_comm)
  
lemma gL_gH_rel: "(x ≼⇩L y) = (x ≼⇩H y)"
  apply (simp add: gH_rel_def gL_rel_def gR_rel_def)
  using add_comm by force
    
lemma gR_gH_rel: "(x ≼⇩R y) = (x ≼⇩H y)"
  apply (simp add: gH_rel_def gL_rel_def gR_rel_def)
  using add_comm by blast

lemma annilr: "annil x = annir x"
  by (metis annil_def annir_def add_comm)
  
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"
  by (simp add: E_eq_one)
  
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
  using add_comm pos_alt by fastforce
    

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)
  using partial_semigroup_class.add_assocD apply force
  by (simp add: partial_semigroup_class.add_assoc)

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
  by (simp add: partial_monoid_class.units_eq prod_eq_iff)

end
  
instance prod :: (type, pas) pas
  apply (standard, simp add: D_prod_def times_prod_def)
  using pas_class.add_comm by force

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
  by (standard, auto simp: D_prod_def times_prod_def add_cancr add_cancl)
    
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
  using add_cancl 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↓)"
    by (simp add: loc_fin)
  hence "finite {y. ∃z. D y z ∧ y ⊕ z = x}"
    by (simp add: partial_semigroup_class.gR_downset_def partial_semigroup_class.gR_rel_def)
  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)↓)"
    by (simp add: partial_semigroup_class.gR_downset_def partial_semigroup_class.gR_rel_def)
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)
  apply (meson partial_semigroup_class.add_assocD)
  by (simp add: partial_semigroup_class.add_assoc)

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)
  by (simp add: partial_monoid_class.units_eq prod.expand)

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 (simp_all add: sd_prod_def sd_D_def)  
   apply (clarsimp, metis act_assoc act_assocD act_distrib act_distribD add_assocD) 
  by (clarsimp, metis act_assoc act_assocD act_distrib act_distribD add_assoc 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