Session PSemigroupsConvolution

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

Theory Partial_Semigroup_Models

(* Title: Models of 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 ‹Models of Partial Semigroups›

theory Partial_Semigroup_Models
  imports Partial_Semigroups
    
begin
  
text ‹So far this section collects three models that we need for applications. Other interesting models might be
added in the future. These might include binary relations, formal power series and matrices, paths in graphs under fusion, 
program traces with alternating state and action symbols under fusion, partial orders under series and parallel products.›
  
subsection ‹Partial Monoids of Segments and Intervals›
  
text ‹Segments of a partial order are sub partial orders between two points. Segments generalise
intervals in that intervals are segments in linear orders. We formalise segments and intervals as pairs, 
where the first coordinate is smaller than the second one. Algebras of segments and intervals are interesting 
in Rota's work on the foundations of combinatorics as well as for interval logics and duration calculi.›
    
text ‹First we define the subtype of ordered pairs of one single type.›

typedef 'a dprod = "{(x::'a, y::'a). True}" 
  by simp

setup_lifting type_definition_dprod
  
text ‹Such pairs form partial semigroups and partial monoids with respect to fusion.›
  
instantiation dprod :: (type) partial_semigroup
begin 

lift_definition D_dprod :: "'a dprod  'a dprod  bool" is "λx y. (snd x = fst y)" .

lift_definition times_dprod :: "'a dprod  'a dprod  'a dprod" is "λx y. (fst x, snd y)"
  by simp

instance 
  by standard (transfer, force)+

end 

instantiation "dprod" :: (type) partial_monoid
begin 

lift_definition E_dprod :: "'a dprod set" is "{x. fst x = snd x}" 
  by simp

instance 
  by standard (transfer,force)+

end 
  
text ‹Next we define the type of segments.›
  
typedef (overloaded) 'a segment = "{x::('a::order × 'a::order). fst x  snd x}"
  by force

setup_lifting type_definition_segment
  
text ‹Segments form partial monoids as well.›
  
instantiation segment :: (order) partial_monoid
begin

lift_definition E_segment :: "'a segment set" is "{x. fst x = snd x}"
  by simp 

lift_definition D_segment :: "'a::order segment  'a segment  bool" 
  is "λx y. (snd x = fst y)" .
    
lift_definition times_segment :: "'a::order segment  'a segment  'a segment" 
  is "λx y. if snd x = fst y then (fst x, snd y) else x"
  by auto

instance 
  by standard (transfer, force)+
 
end
  
text ‹Next we define the function segm that maps segments-as-pairs to segments-as-sets.›
  
definition segm :: "'a::order segment  'a set" where 
  "segm x = {y. fst (Rep_segment x)  y  y  snd (Rep_segment x)}"
  
  thm Rep_segment

lemma segm_sub_morph: "snd (Rep_segment x) = fst (Rep_segment y)  segm x  segm y  segm (x  y)"
  apply (simp add: segm_def times_segment.rep_eq, safe)
  using Rep_segment dual_order.trans apply blast
  by (metis (mono_tags, lifting) Rep_segment dual_order.trans mem_Collect_eq)

text ‹The function segm is not generally a morphism.›
  
lemma "snd (Rep_segment x) = fst (Rep_segment y)  segm x  segm y = segm (x  y)" (* nitpick [expect=genuine] *)
oops

text ‹Intervals are segments over orders that satisfy Halpern and Shoham's  linear order property. This 
is still more general than linearity of the poset.›

class lip_order = order +
  assumes lip: "x  y  (v w. (x  v  v  y  x  w  w  y  v  w  w  v))"
    
text ‹The function segm is now a morphism.›
  
lemma segm_morph: "snd (Rep_segment x::('a::lip_order × 'a::lip_order)) = fst (Rep_segment y) 
     segm x  segm y = segm (x  y)"
  apply (simp add: segm_def times_segment_def)
  apply (transfer, clarsimp simp add: Abs_segment_inverse lip, safe)
  apply force+
  by (meson lip order_trans)
    
    
subsection ‹Cancellative PAM's of Partial Functions›

text ‹We show that partial functions under disjoint union form a positive cancellative PAM. 
This is interesting for modeling the heap in separation logic.›

type_synonym 'a pfun = "'a  'a option"

definition ortho :: "'a pfun  'a pfun  bool"
  where "ortho f g  dom f  dom g = {}"

lemma pfun_comm: "ortho x y  x ++ y = y ++ x"
  by (force simp: ortho_def intro!: map_add_comm)

lemma pfun_canc: "ortho z x  ortho z y  z ++ x = z ++ y  x = y"
  apply (auto simp: ortho_def map_add_def option.case_eq_if fun_eq_iff)
  by (metis domIff dom_restrict option.collapse restrict_map_def)

interpretation pfun: positive_cancellative_pam_one map_add ortho "{Map.empty}" Map.empty
  apply (standard, auto simp: ortho_def pfun_canc)
  by (simp_all add: inf_commute map_add_comm ortho_def pfun_canc)
    
subsection ‹PAM's of Disjoint Unions of Sets›
  
text ‹This simple disjoint union construction underlies important compositions of graphs or partial orders,
in particular in the context of complete joins and disjoint unions of graphs and of series and parallel products
of partial orders.›

instantiation set :: (type) pas
begin  

definition D_set :: "'a set  'a set  bool" where 
  "D_set x y  x  y = {}"

definition times_set :: "'a set  'a set  'a set" where
  "times_set x y = x  y"

instance
  by standard (auto simp: D_set_def times_set_def)

end

instantiation set :: (type) pam
begin 

definition E_set :: "'a set set" where
  "E_set = {{}}"

instance
  by standard (auto simp: D_set_def times_set_def E_set_def)

end
    
end


Theory Quantales

(* Title: Quantales
   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 ‹Quantales›
  
text ‹This entry will be merged eventually with other quantale entries and become a standalone one.›
  
theory Quantales
  imports Main

begin
  
notation sup (infixl "" 60)
  and inf (infixl "" 55)
  and top ("")
  and bot ("")
  and relcomp (infixl ";" 70) 
  and times (infixl "" 70)
  and Sup ("_" [900] 900)  
  and Inf ("_" [900] 900)
  
subsection ‹Properties of Complete Lattices›
  
lemma (in complete_lattice) Sup_sup_pred: "x  {y. P y} = {y. y = x  P y}"
  apply (rule order.antisym)
   apply (simp add: Collect_mono Sup_subset_mono Sup_upper)
  using Sup_least Sup_upper sup.coboundedI2 by force

lemma (in complete_lattice) sup_Sup: "x  y = {x,y}"
  by simp
    
lemma (in complete_lattice) sup_Sup_var: "x  y = {z. z  {x,y}}"
  by (metis Collect_mem_eq sup_Sup)
    
lemma (in complete_boolean_algebra) shunt1: "x  y  z  x  -y  z"
proof standard
  assume "x  y  z"
  hence  "-y  (x  y)  -y  z"
    using sup.mono by blast
  hence "-y  x  -y  z"
    by (simp add: sup_inf_distrib1)
  thus "x  -y  z"
    by simp
next
  assume "x  - y  z"
  hence "x  y  (-y  z)  y"
    using inf_mono by auto
  thus  "x  y  z"
    using inf.boundedE inf_sup_distrib2 by auto
qed
  
lemma (in complete_boolean_algebra) meet_shunt: "x  y =   x  -y"
  by (metis bot_least inf_absorb2 inf_compl_bot_left2 shunt1 sup_absorb1)
  
lemma (in complete_boolean_algebra) join_shunt: "x  y =   -x  y"
  by (metis compl_sup compl_top_eq double_compl meet_shunt)
    

subsection ‹ Familes of Proto-Quantales›
  
text ‹Proto-Quanales are complete lattices equipped with an operation of composition or multiplication
that need not be associative.›
  
class proto_near_quantale = complete_lattice + times + 
  assumes Sup_distr: "X  y = {x  y |x. x  X}"
    
begin
  
lemma mult_botl [simp]: "  x = "
  using Sup_distr[where X="{}"] by auto
  
lemma sup_distr: "(x  y)  z = (x  z)  (y  z)"
  using Sup_distr[where X="{x, y}"] by (fastforce intro!: Sup_eqI)
    
lemma mult_isor: "x  y  x  z  y  z"
  by (metis sup.absorb_iff1 sup_distr)
    
definition bres :: "'a  'a  'a" (infixr "" 60) where 
  "x  z = {y. x  y  z}"

definition fres :: "'a  'a  'a" (infixl "" 60) where 
  "z  y = {x. x  y  z}"

lemma bres_galois_imp: "x  y  z  y  x  z"
  by (simp add: Sup_upper bres_def)
    
lemma fres_galois: "x  y  z  x  z  y"
proof 
  show "x  y  z  x  z  y"
    by (simp add: Sup_upper fres_def)
next
  assume "x  z  y"
  hence "x  y  {x. x  y  z}  y"
    by (simp add: fres_def mult_isor)
  also have "... = {x  y |x. x  y  z}"
    by (simp add: Sup_distr)
  also have "...  z"
    by (rule Sup_least, auto)
  finally show "x  y  z" .
qed
  
end
  
class proto_pre_quantale = proto_near_quantale + 
  assumes Sup_subdistl: "{x  y | y . y  Y}  x  Y"
    
begin

lemma sup_subdistl: "(x  y)  (x  z)  x  (y  z)"
  using Sup_subdistl[where Y="{y, z}"] Sup_le_iff by auto

lemma mult_isol: "x  y  z  x  z  y"
  by (metis le_iff_sup le_sup_iff sup_subdistl)

end
    
class weak_proto_quantale = proto_near_quantale +
  assumes weak_Sup_distl: "Y  {}  x  Y = {x  y |y. y  Y}" 
  
begin

subclass proto_pre_quantale
proof standard
  have a: "x Y. Y = {}  {x  y |y. y  Y}  x  Y"
    by simp
  have b: "x Y. Y  {}  {x  y |y. y  Y}  x  Y"
    by (simp add: weak_Sup_distl)
  show  "x Y. {x  y |y. y  Y}  x  Y"
    using a b by blast 
qed
  
lemma  sup_distl: "x  (y  z) = (x  y)  (x  z)"  
  using weak_Sup_distl[where Y="{y, z}"] by (fastforce intro!: Sup_eqI)

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

end
  
class proto_quantale = proto_near_quantale +
  assumes Sup_distl: "x  Y = {x  y |y. y  Y}"  

begin
  
subclass weak_proto_quantale
  by standard (simp add: Sup_distl)
    
lemma bres_galois: "x  y  z  y  x  z"
proof 
  show "x  y  z  y  x  z"
    by (simp add: Sup_upper bres_def)
next
  assume "y  x  z"
  hence "x  y  x  {y. x  y  z}"
    by (simp add: bres_def mult_isol)
  also have "... = {x  y |y. x  y  z}"
    by (simp add: Sup_distl)
  also have "...  z"
    by (rule Sup_least, auto)
  finally show "x  y  z" .
qed

end 
  
  
subsection ‹Families of Quantales›
  
class near_quantale = proto_near_quantale + semigroup_mult 
  
class unital_near_quantale = near_quantale + monoid_mult

begin

definition iter :: "'a  'a" where
  "iter x  {y. i. y = x ^ i}"

lemma iter_ref [simp]: "iter x  1"
  apply (simp add: iter_def)
  by (metis (mono_tags, lifting) Inf_lower local.power.power_0 mem_Collect_eq)
    
lemma le_top: "x    x"
  by (metis mult_isor mult.monoid_axioms top_greatest monoid.left_neutral)

end
  
class pre_quantale = proto_pre_quantale + semigroup_mult 
  
subclass (in pre_quantale) near_quantale ..
  
class unital_pre_quantale = pre_quantale + monoid_mult
  
subclass (in unital_pre_quantale) unital_near_quantale ..
    
class weak_quantale = weak_proto_quantale + semigroup_mult
  
subclass (in weak_quantale) pre_quantale ..
    
text ‹The following counterexample shows an important consequence of weakness: 
the absence of right annihilation.›
    
lemma (in weak_quantale) "x   = " (*nitpick[expect=genuine]*)
  oops
    
class unital_weak_quantale = weak_quantale + monoid_mult
  
lemma (in unital_weak_quantale) "x   = " (*nitpick[expect=genuine]*)
  oops
  
subclass (in unital_weak_quantale) unital_pre_quantale ..
    
class quantale = proto_quantale + semigroup_mult 
  
begin
  
subclass weak_quantale ..   

lemma mult_botr [simp]: "x   = "
  using Sup_distl[where Y="{}"] by auto

end
  
class unital_quantale = quantale + monoid_mult

subclass (in unital_quantale) unital_weak_quantale ..

class ab_quantale = quantale + ab_semigroup_mult

begin

lemma bres_fres_eq: "x  y = y  x" 
  by (simp add: fres_def bres_def mult_commute)

end

class ab_unital_quantale = ab_quantale + unital_quantale
  
class distrib_quantale = quantale + complete_distrib_lattice
  
class bool_quantale = quantale + complete_boolean_algebra 
  
class distrib_unital_quantale = unital_quantale + complete_distrib_lattice
  
class bool_unital_quantale = unital_quantale + complete_boolean_algebra 
  
class distrib_ab_quantale = distrib_quantale + ab_quantale
  
class bool_ab_quantale = bool_quantale + ab_quantale
  
class distrib_ab_unital_quantale = distrib_quantale + unital_quantale
  
class bool_ab_unital_quantale = bool_ab_quantale + unital_quantale
  
  
subsection ‹Quantales of Booleans and Complete Boolean Algebras›
  
instantiation bool :: bool_ab_unital_quantale
begin
  
definition "one_bool = True"
  
definition "times_bool = (λx y. x  y)"
  
instance
  by standard (auto simp: times_bool_def one_bool_def)
    
end
  
context complete_distrib_lattice
begin
  
interpretation cdl_quantale: distrib_quantale _ _ _ _ _ _ _ _ inf
  by standard (simp_all add: inf.assoc Setcompr_eq_image Sup_inf inf_Sup)
    
end

context complete_boolean_algebra
begin

interpretation cba_quantale: bool_ab_unital_quantale inf _ _ _ _ _ _ _ _ _ _ top
  apply standard
  apply (simp add: inf.assoc)
  apply (simp add: inf.commute)
  apply (simp add: Setcompr_eq_image Sup_inf)
  apply (simp add: Setcompr_eq_image inf_Sup)
  by simp_all
    
text ‹In this setting, residuation can be translated like classical implication.›
  
lemma cba_bres1: "x  y  z  x  cba_quantale.bres y z"
  using cba_quantale.bres_galois inf.commute by fastforce
    
lemma cba_bres2: "x  -y  z  x  cba_quantale.bres y z"
  using cba_bres1 shunt1 by auto
    
lemma cba_bres_prop: "cba_quantale.bres x y = -x  y"
  using cba_bres2 order.eq_iff by blast
  
end
  
text ‹Other models will follow.›
  
   
subsection ‹Products of Quantales›
  
definition "Inf_prod X = ({fst x |x. x  X}, {snd x |x.  x  X})"
  
definition "inf_prod x y = (fst x  fst y, snd x  snd y)"

definition "bot_prod = (bot,bot)"
  
definition "Sup_prod X = ({fst x |x. x  X}, {snd x |x.  x  X})"
    
definition "sup_prod x y = (fst x  fst y, snd x  snd y)"
    
definition "top_prod = (top,top)"
    
definition "less_eq_prod x y  less_eq (fst x) (fst y)  less_eq (snd x) (snd y)"

definition "less_prod x y  less_eq (fst x) (fst y)  less_eq (snd x) (snd y)  x  y"
  
definition "times_prod' x y = (fst x  fst y, snd x  snd y)"

definition "one_prod = (1,1)"
  
interpretation prod: complete_lattice Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::complete_lattice × 'b::complete_lattice)"
  apply standard
     apply (simp_all add: Inf_prod_def Sup_prod_def inf_prod_def sup_prod_def bot_prod_def top_prod_def less_eq_prod_def less_prod_def Sup_distl Sup_distr)
        apply force+
     apply (rule conjI, (rule Inf_lower, force)+)
    apply (rule conjI, (rule Inf_greatest, force)+)
   apply (rule conjI, (rule Sup_upper, force)+)
  by (rule conjI, (rule Sup_least, force)+)

interpretation prod: proto_near_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_near_quantale × 'b::proto_near_quantale)" times_prod'
  apply (standard, simp add: times_prod'_def Sup_prod_def)
  by (rule conjI, (simp add: Sup_distr, clarify, metis)+)
    
interpretation prod: proto_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_quantale × 'b::proto_quantale)" times_prod'
  apply (standard, simp add: times_prod'_def Sup_prod_def less_eq_prod_def)
  by (rule conjI, (simp add: Sup_distl, metis)+)

interpretation prod: unital_quantale one_prod times_prod' Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::unital_quantale × 'b::unital_quantale)" 
  by standard (simp_all add: one_prod_def times_prod'_def mult.assoc)
    

subsection ‹Quantale Modules and Semidirect Products›
  
text ‹Quantale modules are extensions of semigroup actions in that a quantale acts on a complete lattice.›
  
locale unital_quantale_module = 
  fixes act :: "'a::unital_quantale  'b::complete_lattice  'b" ("α")
  assumes act1: "α (x  y) p = α x (α y p)"
    and act2 [simp]: "α 1 p = p" 
    and act3: "α (X) p = {α x p |x. x  X}"
    and act4: "α x (P) = {α x p |p. p  P}"

context unital_quantale_module
begin
  
text ‹Actions are morphisms. The curried notation is particularly convenient for this.›
  
lemma act_morph1: "α (x  y) = (α x)  (α y)"
  by (simp add: fun_eq_iff act1)
    
lemma act_morph2: "α 1 = id"
  by (simp add: fun_eq_iff)
  
lemma emp_act: "α ({}) p = "
  by (simp only: act3, force)
    
lemma emp_act_var: "α  p = "
  using emp_act by auto

lemma act_emp: "α x ({}) = "
  by (simp only: act4, force)
    
lemma act_emp_var: "α x  = "
  using act_emp by auto
  
lemma act_sup_distl: "α x (p  q) = (α x p)  (α x q)"
proof-
  have "α x (p  q) = α x ({p,q})"
    by simp
  also have "... = {α x y |y. y  {p,q}}"
    by (rule act4)
  also have "... = {v. v = α x p  v = α x q}"
    by (metis empty_iff insert_iff)
  finally show ?thesis
    by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed
  
lemma act_sup_distr: "α (x  y) p = (α x p)  (α y p)"
  proof-
  have "α (x  y) p  = α ({x,y}) p"
    by simp
  also have "... = {α v p |v. v  {x,y}}"
    by (rule act3)
  also have "... = {v. v = α x p  v = α y p}"
    by (metis empty_iff insert_iff)
  finally show ?thesis
    by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed
  
lemma act_sup_distr_var: "α (x  y) = (α x)  (α y)"
  by (simp add: fun_eq_iff act_sup_distr)
    
text ‹Next we define the semidirect product of a  unital quantale and a complete lattice. ›
  
definition "sd_prod x y = (fst x  fst y, snd x  α (fst x) (snd y))"
   
lemma sd_distr_aux: 
  "{snd x |x. x  X}  {α (fst x) p |x. x  X} = {snd x  α (fst x) p |x. x  X}"
proof (rule antisym, rule sup_least) 
  show "{snd x |x. x  X}  {snd x  α (fst x) p |x. x  X}"
  proof (rule Sup_least)
    fix x :: 'b
    assume "x  {snd x |x. x  X}"
    hence "b pa. x  b = snd pa  α (fst pa) p  pa  X"
      by blast
    hence "b. x  b  {snd pa  α (fst pa) p |pa. pa  X}"
      by blast
    thus "x  {snd pa  α (fst pa) p |pa. pa  X}"
      by (meson Sup_upper sup.bounded_iff)
  qed  
next
  show "{α (fst x) p |x. x  X}  {snd x  α (fst x) p |x. x  X}"
  proof (rule Sup_least)
    fix x :: 'b
    assume "x  {α (fst x) p |x. x  X}"
    then have "b pa. b  x = snd pa  α (fst pa) p  pa  X"
      by blast
    then have "b. b  x  {snd pa  α (fst pa) p |pa. pa  X}"
      by blast
    then show "x  {snd pa  α (fst pa) p |pa. pa  X}"
      by (meson Sup_upper le_supE)
  qed
next
  show "{snd x  α (fst x) p |x. x  X}  {snd x |x. x  X}  {α (fst x) p |x. x  X}"
    apply (rule Sup_least)
    apply safe 
    apply (rule sup_least)
    apply (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI1)
    by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI2)
qed

lemma sd_distr: "sd_prod (Sup_prod X) y = Sup_prod {sd_prod x y |x. x  X}"
proof -
  have "sd_prod (Sup_prod X) y = sd_prod ({fst x |x. x  X}, {snd x |x. x  X}) y"
    by (simp add: Sup_prod_def)
  also have 
    "... = (({fst x |x. x  X})  fst y, ({snd x |x. x  X})  (α ({fst x | x. x  X})  (snd y)))"
    by (simp add: sd_prod_def)
  also have 
    "... = ({fst x  fst y|x. x  X}, ({snd x |x. x  X})  (α ({fst x | x. x  X})  (snd y)))"
    by (simp add: Sup_distr)
  also have 
    "... = ({fst x  fst y|x. x  X}, ( {snd x |x. x  X})  ({α (fst x) (snd y) | x. x  X}))"
    by (simp add: act3)
  also have "... = ({fst x  fst y|x. x  X}, {snd x  (α (fst x) (snd y)) | x. x  X})"
    by (simp only: sd_distr_aux)
  also have "... = Sup_prod {(fst x  fst y, snd x  (α (fst x) (snd y))) |x. x  X}"
    by (simp add: Sup_prod_def, metis)
  finally show ?thesis
    by (simp add: sd_prod_def)
qed
  
lemma sd_distl_aux: "Y  {}  p  ({α x (snd y) |y. y  Y}) = {p  α x (snd y) |y. y  Y}"
proof (rule antisym, rule sup_least)
  show "Y  {}  p  {p  α x (snd y) |y. y  Y}"
  proof -
    assume "Y  {}"
    hence "b. b  {p  α x (snd pa) |pa. pa  Y}  p  b"
      by fastforce
    thus "p  {p  α x (snd pa) |pa. pa  Y}"
      by (meson Sup_upper2)
  qed
next
  show "Y  {}  {α x (snd y) |y. y  Y}  {p  α x (snd y) |y. y  Y}"  
    apply (rule Sup_least)
  proof -
    fix xa :: 'b
    assume "xa  {α x (snd y) |y. y  Y}"
    then have "b. (pa. b = p  α x (snd pa)  pa  Y)  xa  b"
      by fastforce
    then have "b. b  {p  α x (snd pa) |pa. pa  Y}  xa  b"
      by blast
    then show "xa  {p  α x (snd pa) |pa. pa  Y}"
      by (meson Sup_upper2)
  qed
next
  show "Y  {}  {p  α x (snd y) |y. y  Y}  p  {α x (snd y) |y. y  Y}"
    apply (rule Sup_least)
    apply safe
    by (metis (mono_tags, lifting) Sup_le_iff le_sup_iff mem_Collect_eq sup_ge1 sup_ge2)
qed

lemma sd_distl: "Y  {}  sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y  Y}"
proof -
  assume a: "Y  {}"
  have "sd_prod x (Sup_prod Y) = sd_prod x ({fst y |y. y  Y}, {snd y |y. y  Y})"
    by (simp add: Sup_prod_def)
  also have "... = ((fst x)  ({fst y |y. y  Y}), (snd x  (α (fst x) ({snd y |y. y  Y}))))"
    by (simp add: sd_prod_def)
  also have "... = ({fst x  fst y |y. y  Y}, (snd x  (α (fst x) ({snd y |y. y  Y}))))"
    by (simp add: Sup_distl)
  also have "... = ({fst x  fst y |y. y  Y}, (snd x  ({α (fst x) (snd y) |y. y  Y})))"
    by (simp add: act4, meson)
  also have "... = ({fst x  fst y |y. y  Y}, {snd x  (α (fst x) (snd y)) |y. y  Y})"
    using a sd_distl_aux by blast
  also have "... = Sup_prod {(fst x  fst y, snd x  (α (fst x) (snd y))) |y. y  Y}"
    by (simp add: Sup_prod_def, metis)
  finally show ?thesis
    by (simp add: sd_prod_def)
qed
  
definition "sd_unit = (1,)"
 
lemma sd_unitl [simp]: "sd_prod sd_unit x = x"
  by (simp add: sd_prod_def sd_unit_def)    
    
lemma sd_unitr [simp]: "sd_prod x sd_unit = x"
  apply (simp add: sd_prod_def sd_unit_def)
  using act_emp by force
   
text ‹The following counterexamples rule out that semidirect products of quantales and complete lattices form quantales.
The reason is that the right annihilation law fails.›
  
lemma "sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y  Y}" (*nitpick[show_all,expect=genuine]*)
  oops
  
lemma "sd_prod x bot_prod = bot_prod" (*nitpick[show_all,expect=genuine]*)
  oops
    
text ‹However we can show that semidirect products of (unital) quantales with complete lattices form weak (unital) quantales. ›
    
interpretation dp_quantale: weak_quantale sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
  apply standard 
  apply (simp_all add: sd_distl sd_distr)
  apply (simp_all add: sd_prod_def Inf_prod_def Sup_prod_def bot_prod_def sup_prod_def top_prod_def inf_prod_def less_eq_prod_def less_prod_def)
  by (rule conjI, simp add: mult.assoc, simp add: act1 act_sup_distl sup_assoc) 
    
interpretation dpu_quantale: unital_weak_quantale sd_unit sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
  by (standard; simp_all)

end

end
  


Theory Binary_Modalities

(* Title: Binary Modalities
   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 ‹Binary Modalities and Relational Convolution›

theory Binary_Modalities
  imports Quantales

begin
 
subsection ‹Auxiliary Properties›
  
lemma SUP_is_Sup: "(SUP fF. f y) = {(f::'a  'b::proto_near_quantale) y |f. f  F}"
proof (rule antisym)
  fix f::"'a  'b::proto_near_quantale"
  have "f  F  f y  {f y |f. f  F}"
    by (simp add: Setcompr_eq_image)
  hence "f  F  f y  {f y |f. f  F}"
    by (simp add: Sup_upper)
  thus "(SUP fF. f y)  {(f::'a  'b::proto_near_quantale) y |f. f  F}"
    by (simp add: Setcompr_eq_image)
next 
  fix x
  have "x  {f y |f. f  F}  x  (SUP fF. f y) "
    using mk_disjoint_insert by force
  thus "Sup {(f::'a  'b::proto_near_quantale) y |f. f  F}  (SUP fF. f y)"
    by (simp add: Setcompr_eq_image)
qed

lemma bmod_auxl: "{x  g z |x. f. x = f y  f  F} = {f y  g z |f. f  F}"
  by force

lemma bmod_auxr: "{f y  x |x. g. x = g z  g  G} = {f y  g z |g. g  G}"
  by force

lemma bmod_assoc_aux1: 
  "{{(f :: 'a  'b::proto_near_quantale) u  g v  h w |u v. R y u v} |y w. R x y w} 
     = {(f u  g v)  h w |u v y w. R y u v  R x y w}"
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (intro Sup_least Sup_upper, force)
  apply (rule Sup_least, safe)
  by (rule Sup_upper2, auto)+
  
lemma bmod_assoc_aux2:   
  "{{(f::'a  'b::proto_near_quantale) u  g v  h w |v w. R y v w} |u y. R x u y} 
     = {f u  g v  h w |u v w y. R y v w  R x u y}" 
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (intro Sup_least Sup_upper, force)
  apply (rule Sup_least, safe)
  by (rule Sup_upper2, auto)+
    

subsection ‹Binary Modalities›
  
text ‹Most of the development in the papers mentioned in the introduction generalises to proto-near-quantales. Binary modalities 
are interesting for various substructural logics over ternary Kripke frames. They also arise, e.g., 
as chop modalities in interval logics or as separation conjunction in separation logic. Binary modalities can be understood as a convolution
operation parametrised by a ternary operation. Our development yields a 
unifying framework.›
  
text ‹We would prefer a notation that is more similar to our articles, that is, $f\ast_R g$, but we don' know how we could 
index an infix operator by a variable in Isabelle.›

definition bmod_comp :: "('a  'b  'c  bool)  ('b  'd::proto_near_quantale)  ('c  'd)  'a  'd" ("") where 
  " R f g x = {f y  g z |y z. R x y z}"

definition bmod_bres :: "('c  'b  'a  bool)  ('b  'd::proto_near_quantale)  ('c  'd)  'a  'd" ("") where 
  " R f g x = {(f y)  (g z) |y z. R z y x}"

definition bmod_fres :: "('b  'a  'c  bool)   ('b  'd::proto_near_quantale)  ('c  'd)  'a  'd" ("")where 
  " R f g x = {(f y)  (g z) |y z. R y x z}"

lemma bmod_un_rel: " (R  S) =  R   S"
  apply  (clarsimp simp: fun_eq_iff bmod_comp_def Sup_union_distrib[symmetric] Collect_disj_eq[symmetric])
  by (metis (no_types, lifting))

lemma bmod_Un_rel: " () f g x = { R f g x |R. R  }"
  apply (simp add: bmod_comp_def)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (rule Sup_upper2, force)
  apply (rule Sup_upper, force)
  apply (rule Sup_least, safe)+
  by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq)
    
lemma bmod_sup_fun1: " R (f  g) =  R f   R g"
  apply (clarsimp simp add: fun_eq_iff bmod_comp_def sup_distr)
  apply (rule antisym)
  apply (intro Sup_least, safe)
  apply (rule sup_least)
  apply (intro le_supI1 Sup_upper, force)
  apply (intro le_supI2 Sup_upper, force)
  apply (rule sup_least)
  by (intro Sup_least, safe, rule Sup_upper2, force, simp)+

lemma bmod_Sup_fun1: " R () g x = { R f g x |f. f  }"
proof -
  have " R ({f. f  }) g x = {{f y |f. f  }  g z |y z. R x y z}"
    by (simp add: bmod_comp_def SUP_is_Sup)
  also have "... = {{f y  g z |f. f  } |y z. R x y z}"
    by (simp add: Sup_distr bmod_auxl)
  also have "... = {{f y  g z |y z. R x y z} |f. f  }"
    apply (rule antisym)
    by ((rule Sup_least, safe)+ , (rule Sup_upper2, force, rule Sup_upper, force))+
  finally show ?thesis
    by (simp add: bmod_comp_def)
qed

lemma bmod_sup_fun2: " R (f::'a  'b::weak_proto_quantale) (g  h) =  R f g   R f h"
  apply (clarsimp simp add: fun_eq_iff bmod_comp_def sup_distl)
  apply (rule antisym)
  apply (intro Sup_least, safe)
  apply (rule sup_least)
  apply (intro le_supI1 Sup_upper, force)
  apply (intro le_supI2 Sup_upper, force)
  apply (rule sup_least)
  by (intro Sup_least, safe, rule Sup_upper2, force, simp)+
 
lemma bmod_Sup_fun2_weak:
  assumes "𝒢  {}"
  shows " R f (𝒢) x = { R f (g::'a  'b::weak_proto_quantale) x |g. g  𝒢}"
proof -
  have set: "z. {g z |g::'a  'b. g  𝒢}  {}"
    using assms by blast
  have " R f ({g. g  𝒢}) x = {f y  {g z |g. g  𝒢} |y z. R x y z}"
    by (simp add: bmod_comp_def SUP_is_Sup)
  also have "... = {{f y  g z |g. g  𝒢} |y z. R x y z}"
    by (simp add: weak_Sup_distl[OF set] bmod_auxr)           
  also have "... = {{f y  g z |y z. R x y z} |g. g  𝒢}"
    apply (rule antisym)
    by ((rule Sup_least, safe)+, (rule Sup_upper2, force, rule Sup_upper, force))+
  finally show ?thesis
    by (auto simp: bmod_comp_def)
qed
  
lemma bmod_Sup_fun2: " R f (𝒢) x = { R f (g::'a  'b::proto_quantale) x |g. g  𝒢}"
proof -
  have " R f ({g. g  𝒢}) x = {f y  {g z |g. g  𝒢} |y z. R x y z}"
    by (simp add:  bmod_comp_def SUP_is_Sup)
  also have "... = {{f y  g z |g. g  𝒢} |y z. R x y z}"
    by (simp add: Sup_distl bmod_auxr)
  also have "... =  {{f y  g z |y z. R x y z} |g. g  𝒢}"
    apply (rule antisym)
    by ((rule Sup_least, safe)+, (rule Sup_upper2, force, rule Sup_upper, force))+
  finally show ?thesis
    by (auto simp: bmod_comp_def)
qed

lemma bmod_comp_bres_galois: "(x.  R f g x  h x)  (x. g x   R f h x)" (* nitpick[expect=genuine] *)
  oops
    
text ‹The following Galois connection requires functions into proto-quantales.›
    
lemma bmod_comp_bres_galois: "(x.  R (f::'a  'b::proto_quantale) g x  h x)  (x. g x   R f h x)"
proof -
  have "(x.  R f g x  h x)  (x y z. R x y z  (f y)  (g z)  h x)"
    apply (simp add: bmod_comp_def, standard, safe)
    apply (metis (mono_tags, lifting) CollectI Sup_le_iff)
    by (rule Sup_least, force)
  also have "...   (x y z. R x y z  g z  (f y)  (h x))"
    by (simp add: bres_galois)
  finally show ?thesis
    apply (simp add: fun_eq_iff bmod_bres_def)
    apply standard
    using le_Inf_iff apply fastforce
    by (metis (mono_tags, lifting) CollectI le_Inf_iff)
qed 

lemma bmod_comp_fres_galois: "(x.  R f g x  h x)  (x. f x   R h g x)"
proof -
  have "(x.  R f g x  h x)  (x y z. R x y z  (f y)  (g z)  h x)"
    apply (simp add: bmod_comp_def, standard, safe)
    apply (metis (mono_tags, lifting) CollectI Sup_le_iff)
    by (rule Sup_least, force)
  also have "...   (x y z. R x y z  f y  (h x)  (g z))"
    by (simp add: fres_galois)
  finally show ?thesis
    apply (simp add: bmod_fres_def fun_eq_iff)
    apply standard
    using le_Inf_iff apply fastforce
    by (metis (mono_tags, lifting) CollectI le_Inf_iff)
qed 
  

subsection ‹Relational Convolution and Correspondence Theory›

text‹We now fix a ternary relation $\rho$ and can then hide the parameter in a convolution-style notation.›
  
class rel_magma = 
  fixes ρ :: "'a  'a  'a  bool"

begin
  
definition times_rel_fun :: "('a  'b::proto_near_quantale)  ('a  'b)  'a  'b" (infix "" 70) where
  "f  g =  ρ f g"
  
lemma rel_fun_Sup_distl_weak: 
  "G  {}  (f::'a  'b::weak_proto_quantale)  G = {f  g |g. g  G}"
proof- 
  fix f :: "'a  'b" and G :: "('a  'b) set" 
  assume a: "G  {}"
  show "f  G = {f  g |g. g  G}"
    apply (clarsimp simp: fun_eq_iff times_rel_fun_def bmod_Sup_fun2_weak[OF a])
    apply (rule antisym)
    apply (rule Sup_least, safe)
    apply (rule SUP_upper2, force+)
    apply (rule SUP_least, safe)
    by (rule Sup_upper2, force+)
qed
    
lemma rel_fun_Sup_distl: "(f::'a  'b::proto_quantale)  G = {f  g |g. g  G}"
  apply (clarsimp simp: fun_eq_iff times_rel_fun_def bmod_Sup_fun2)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (rule SUP_upper2, force+)
  apply (rule SUP_least, safe)
  by (rule Sup_upper2, force+)

lemma rel_fun_Sup_distr: "G  (f::'a  'b::proto_near_quantale) = {g  f |g. g  G}"
  apply (clarsimp simp: fun_eq_iff times_rel_fun_def bmod_Sup_fun1)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (rule SUP_upper2, force+)
  apply (rule SUP_least, safe)
  by (rule Sup_upper2, force+)

end

class rel_semigroup = rel_magma +
  assumes rel_assoc: "(y. ρ y u v  ρ x y w)  (z. ρ z v w  ρ x u z)"

begin
  
text ‹Nitpick produces counterexamples even for weak quantales. 
Hence one cannot generally lift functions into weak quantales to weak quantales.›
  
lemma bmod_assoc: " ρ ( ρ (f::'a  'b::weak_quantale) g) h x =  ρ f ( ρ g h) x"
  (*nitpick[show_all,expect=genuine]*)
    oops

lemma bmod_assoc: " ρ ( ρ (f::'a  'b::quantale) g) h x =  ρ f ( ρ g h) x"
proof -
  have " ρ ( ρ f g) h x = {{f u  g v  h z |u v. ρ y u v} |y z. ρ x y z}" 
    apply (simp add: bmod_comp_def Sup_distr)
    apply (rule antisym) 
    by (intro Sup_least Sup_upper, safe, intro exI conjI, simp_all, rule_tac f = Sup and g = Sup in cong, auto)+
  also have "... = {f u  g v  h z |u v y z. ρ y u v  ρ x y z}"
    by (simp add: bmod_assoc_aux1)
  also have "... = {f u  g v  h z |u v z y. ρ y v z  ρ x u y}" 
    apply (rule antisym)
    apply (rule Sup_least, rule Sup_upper, safe)
    using rel_assoc apply force
    apply (rule Sup_least, rule Sup_upper, safe)
    using rel_assoc by blast 
  also have "... = {{f u  g v  h z |v z. ρ y v z} |u y. ρ x u y}" 
    by (simp add: bmod_assoc_aux2)
  also have "... = {f u  {g v  h z |v z. ρ y v z} |u y. ρ x u y}" 
    apply (simp add: Sup_distl mult.assoc)
    apply (rule antisym)
    by (intro Sup_least Sup_upper, safe, intro exI conjI, simp_all, rule_tac f = Sup and g = Sup in cong, auto)+
  finally show ?thesis
    by (auto simp: bmod_comp_def)
qed

lemma rel_fun_assoc: "((f :: 'a  'b::quantale)  g)  h = f  (g  h)"
  by (simp add: times_rel_fun_def fun_eq_iff bmod_assoc[symmetric])

end

lemma " R ( R f f) f x =  R f ( R f f) x"
(*apply (simp add: bmod_comp_def) nitpick[expect=genuine] *)
oops

class rel_monoid = rel_semigroup + 
  fixes ξ :: "'a set"
  assumes unitl_ex: "e  ξ. ρ x e x" 
  and unitr_ex: "e  ξ. ρ x x e"
  and unitl_eq: "e  ξ  ρ x e y  x = y"
  and unitr_eq: "e  ξ  ρ x y e  x = y"

begin

lemma xi_prop: "e1  ξ  e2  ξ  e1  e2  ¬ ρ x e1 e2  ¬ ρ x e2 e1"
  using unitl_eq unitr_eq by blast

definition pid :: "'a   'b::unital_weak_quantale" ("δ") where
  "δ x = (if x  ξ then 1 else )"
  
text ‹Due to the absence of right annihilation, the right unit law fails for functions into weak quantales.›
  
lemma bmod_onel: " ρ f (δ::'a  'b::unital_weak_quantale) x = f x" 
(*nitpick[expect=genuine]*)
  oops
  
text ‹A unital quantale is required for this lifting.›
    
lemma bmod_onel: " ρ f (δ::'a  'b::unital_quantale) x = f x"
  apply (simp add: bmod_comp_def pid_def)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (simp add: bres_galois)
  using unitr_eq apply fastforce
  apply (metis bot.extremum)
  by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq unitr_ex)

lemma  bmod_oner: " ρ δ f x = f x"
  apply (simp add: bmod_comp_def pid_def)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (simp add: fres_galois)
  using unitl_eq apply fastforce
  apply (metis bot.extremum)
  by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq unitl_ex)

lemma pid_unitl [simp]: "δ  f = f"
  by (simp add: fun_eq_iff times_rel_fun_def bmod_oner)

lemma pid_unitr [simp]: "f  (δ::'a  'b::unital_quantale) = f"
  by (simp add: fun_eq_iff times_rel_fun_def bmod_onel)
    
lemma bmod_assoc_weak_aux: 
  "f u  {g v  h z |v z. ρ y v z} = {(f::'a  'b::weak_quantale) u  g v  h z |v z. ρ y v z}"
  apply (subst weak_Sup_distl)
  using unitl_ex apply force
  apply simp
  by (metis (no_types, lifting) mult.assoc)
    
lemma bmod_assoc_weak: " ρ ( ρ (f::'a  'b::weak_quantale) g) h x =  ρ f ( ρ g h) x"
proof -
  have " ρ ( ρ f g) h x = {{f u  g v  h z |u v. ρ y u v} |y z. ρ x y z}" 
    apply (simp add: bmod_comp_def Sup_distr)
    apply (rule antisym) 
    by (intro Sup_least Sup_upper, safe, intro exI conjI, simp_all, rule_tac f = Sup and g = Sup in cong, auto)+
  also have "... = {f u  g v  h z |u v y z. ρ y u v  ρ x y z}"
    by (simp add: bmod_assoc_aux1)
  also have "... = {f u  g v  h z |u v z y. ρ y v z  ρ x u y}" 
    apply (rule antisym)
    apply (rule Sup_least, rule Sup_upper, safe)
    using rel_assoc apply force
    apply (rule Sup_least, rule Sup_upper, safe)
    using rel_assoc by blast 
  also have "... = {{f u  g v  h z |v z. ρ y v z} |u y. ρ x u y}" 
    by (simp add: bmod_assoc_aux2)
  also have "... = {f u  {g v  h z |v z. ρ y v z} |u y. ρ x u y}"
    by (simp add: bmod_assoc_weak_aux) 
  finally show ?thesis
    by (auto simp: bmod_comp_def)
qed
  
lemma rel_fun_assoc_weak: "((f :: 'a  'b::weak_quantale)  g)  h = f  (g  h)"
  by (simp add: times_rel_fun_def fun_eq_iff bmod_assoc_weak[symmetric])

end

lemma (in rel_semigroup) "id. f x. ( ρ f id x = f x   ρ id f x = f x)"
(* apply (simp add: bmod_comp_def) nitpick [expect=genuine] *)
  oops

class rel_ab_semigroup = rel_semigroup +
  assumes rel_comm: x y z   ρ x z y" 

begin 

lemma bmod_comm: " ρ (f::'a  'b::ab_quantale) g =  ρ g f"
  by (simp add: fun_eq_iff bmod_comp_def mult.commute, meson rel_comm)

lemma " ρ f g =  ρ g f" (* nitpick [expect=genuine] *)
oops

lemma bmod_bres_fres_eq: " ρ (f::'a  'b::ab_quantale) g =  ρ g f"
  by (simp add: fun_eq_iff bmod_bres_def bmod_fres_def bres_fres_eq, meson rel_comm)

lemma rel_fun_comm: "(f :: 'a  'b::ab_quantale)  g = g  f"
  by (simp add: times_rel_fun_def bmod_comm)

end

class rel_ab_monoid = rel_ab_semigroup + rel_monoid
  
subsection ‹Lifting to Function Spaces›

text ‹We lift by interpretation, since we need sort instantiations to be
     used for functions from PAM's to Quantales. Both instantiations cannot be
     used in Isabelle at the same time.›
  
interpretation rel_fun: weak_proto_quantale Inf Sup inf less_eq less sup bot "top :: 'a::rel_magma  'b::weak_proto_quantale" times_rel_fun
  by standard (simp_all add: rel_fun_Sup_distr rel_fun_Sup_distl_weak)
  
interpretation rel_fun: proto_quantale Inf Sup inf less_eq less sup bot "top :: 'a::rel_magma  'b::proto_quantale" times_rel_fun
  by standard (simp add: rel_fun_Sup_distl)
    
text ‹Nitpick shows that the lifting of weak quantales to weak quantales does not work for relational semigroups, because associativity fails.›
  
interpretation rel_fun: weak_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup  'b::weak_quantale"
  (*apply standard  nitpick[expect=genuine]*)
  oops
    
text ‹Associativity is obtained when lifting from relational monoids, but the right unit law doesn't hold
 in the quantale on the function space, according to our above results. Hence the lifting results into a
non-unital quantale, in which only the left unit law holds, as shown above. We don't provide a special class for 
such quantales. Hence we lift only to non-unital quantales.›
    
interpretation rel_fun: weak_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_monoid  'b::unital_weak_quantale"
  by standard (simp_all add: rel_fun_assoc_weak) 

interpretation rel_fun2: quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup  'b::quantale" 
  by standard (simp add: rel_fun_assoc)
    
interpretation rel_fun2: distrib_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup  'b::distrib_quantale" times_rel_fun ..

interpretation rel_fun2: bool_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup  'b::bool_quantale" minus uminus times_rel_fun ..

interpretation rel_fun2: unital_quantale pid times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_monoid  'b::unital_quantale" 
  by (standard; simp)
    
interpretation rel_fun2: distrib_unital_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_monoid  'b::distrib_unital_quantale" pid times_rel_fun ..

interpretation rel_fun2: bool_unital_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_monoid  'b::bool_unital_quantale" minus uminus pid times_rel_fun ..

interpretation rel_fun: ab_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_ab_semigroup  'b::ab_quantale"
  by standard (simp add: rel_fun_comm)

interpretation rel_fun: ab_unital_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid  'b::ab_unital_quantale" pid ..

interpretation rel_fun2: distrib_ab_unital_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid  'b::distrib_ab_unital_quantale" times_rel_fun pid ..

interpretation rel_fun2: bool_ab_unital_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid  'b::bool_ab_unital_quantale" minus uminus pid ..
    
end

  
  
  

Theory Unary_Modalities

(* Title: Unary Modalities
   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 ‹Unary Modalities›

theory Unary_Modalities
  imports Binary_Modalities
begin
  
text ‹Unary modalites arise as specialisations of the binary ones; and as generalisations of the 
standard (multi-)modal operators from predicates to functions into complete lattices. They are interesting, for instance, 
in combination with partial semigroups or monoids, for modelling the Halpern-Shoham modalities in interval logics. ›
  
subsection ‹Forward and Backward Diamonds›

definition fdia :: "('a × 'b) set  ('b  'c::complete_lattice)  'a  'c" ("( |_ _ _)" [61,81] 82) where
  "( |R f x) = {f y|y. (x,y)  R}" 

definition bdia :: "('a × 'b) set  ('a  'c::complete_lattice)  'b  'c" ("( _| _ _)" [61,81] 82)where
  "(R| f y) = {f x |x. (x,y)  R}"  

definition c1 :: "'a  'b::unital_quantale" where
  "c1 x = 1"
  
text ‹The relationship with binary modalities is as follows.›
  
lemma fdia_bmod_comp: "( |R f x) =  (λx y z. (x,y)  R) f c1 x"
  by (simp add: fdia_def bmod_comp_def c1_def)

lemma bdia_bmod_comp: "(R| f x) =  (λy x z. (x,y)  R) f c1 x"
  by (simp add: bdia_def bmod_comp_def c1_def)

lemma bmod_fdia_comp: " R f g x = |{(x,(y,z)) |x y z. R x y z} (λ(x,y). (f x)  (g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma bmod_fdia_comp_var: 
  " R f g x = |{(x,(y,z)) |x y z. R x y z} (λ(x,y). (λ(v,w).(v  w)) (f x,g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma fdia_im: "( |R f x) = (f ` R `` {x})"
  apply (simp add: fdia_def)
  apply (rule antisym)
  apply (intro Sup_least, clarsimp simp: SUP_upper)
  by (intro SUP_least Sup_upper, force)

lemma fdia_un_rel: "fdia (R  S) = fdia R  fdia S" 
  apply (simp add: fun_eq_iff)
  by (clarsimp simp: fun_eq_iff fdia_im SUP_union Un_Image)

lemma fdia_Un_rel: "( | f x) = {|R f x |R. R  }" 
  apply (simp add: fdia_im)
  apply (rule antisym)
  apply (intro SUP_least, safe)
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp)
  apply (rule Sup_least)
  by (clarsimp simp: Image_mono SUP_subset_mono Sup_upper)

lemma fdia_sup_fun: "fdia R (f  g) = fdia R f  fdia R g" 
  by (simp add: fun_eq_iff fdia_im complete_lattice_class.SUP_sup_distrib)
    
lemma fdia_Sup_fun: "( |R () x) = {|R f x |f. f  } "
  apply (simp add: fdia_im)
  apply (rule antisym) 
  apply (rule SUP_least)+
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp) 
  apply (rule Sup_least, safe)
  apply (rule SUP_least)
  by (simp add: SUP_upper2)

lemma fdia_seq: "fdia (R ; S) f x  = fdia R (fdia S f) x"
  by (simp add: fdia_im relcomp_Image, metis Image_eq_UN SUP_UNION) 

lemma fdia_Id [simp]: "( |Id f x) = f x"
  by (simp add: fdia_def)
    
    
subsection ‹Forward and Backward Boxes›
  
definition fbox :: "('a × 'b) set  ('b  'c::complete_lattice)  'a  'c" ("|_] _ _" [61,81] 82) where
  "( |R] f x) = {f y|y. (x,y)  R}" 

definition bbox :: "('a × 'b) set  ('a  'c::complete_lattice)  'b  'c" ("[_| _ _" [61,81] 82)where
  "([R| f y) = {f x |x. (x,y)  R}"  
  
  
subsection ‹Symmetries and Dualities›
  
lemma fdia_fbox_demorgan: "( |R (f::'b  'c::complete_boolean_algebra) x) = - |R] (λy. -f y) x"
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto

lemma fbox_fdia_demorgan: "( |R] (f::'b  'c::complete_boolean_algebra) x) = - |R (λy. -f y) x"  
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)
    
lemma bdia_bbox_demorgan: "(R| (f::'b  'c::complete_boolean_algebra) x) = - [R| (λy. -f y) x"
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto
    
lemma bbox_bdia_demorgan: "( [R| (f::'b  'c::complete_boolean_algebra) x) = - R| (λy. -f y) x"  
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)
 
lemma fdia_bdia_conv: "( |R f x) = converse R| f x"
  by (simp add: fdia_def bdia_def) 

lemma fbox_bbox_conv: "( |R] f x) = [converse R| f x"
  by (simp add: fbox_def bbox_def)
    
lemma fdia_bbox_galois: "(x. ( |R f x)  g x)  (x. f x  [R| g x)"
  apply (standard, simp_all add: fdia_def bbox_def)
   apply safe
   apply (rule Inf_greatest)
   apply (force simp: Sup_le_iff)  
  apply (rule Sup_least)
  by (force simp: le_Inf_iff)  
    
lemma bdia_fbox_galois: "(x. (R| f x)  g x)  (x. f x  |R] g x)"
  apply (standard, simp_all add: bdia_def fbox_def)
   apply safe
   apply (rule Inf_greatest)
   apply (force simp: Sup_le_iff)  
  apply (rule Sup_least)
  by (force simp: le_Inf_iff)  
  
lemma dia_conjugate: 
  "(x. ( |R (f::'b  'c::complete_boolean_algebra) x)  g x = )  (x. f x  (R| g x) = )"
  by (simp add: meet_shunt fdia_bbox_galois bdia_bbox_demorgan)
    
lemma box_conjugate: 
  "(x. ( |R] (f::'b  'c::complete_boolean_algebra) x)  g x = )  (x. f x  ([R| g x) = )"
proof-
  have "(x. ( |R] f x)  g x = )  (x. -g x  |R] f x)"
    by (simp add: join_shunt sup_commute)
  also have "...  (x. -g x  - |R (λy. -f y) x)"
    by (simp add: fbox_fdia_demorgan) 
  also have "...  (x. ( |R (λy. -f y) x)  g x)"      
    by simp
  also have "...  (x. -f x  [R| g x)"
    by (simp add: fdia_bbox_galois)  
  finally show ?thesis
    by (simp add: join_shunt)
qed
  
end
                            

  

Theory Partial_Semigroup_Lifting

(* Title: Liftings of 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 ‹Liftings of Partial Semigroups›

theory Partial_Semigroup_Lifting
  imports Partial_Semigroups Binary_Modalities

begin  
  
text ‹First we show that partial semigroups are instances of relational semigroups. Then we extend the lifting results for relational 
semigroups to partial semigroups.›
  
  
subsection ‹Relational Semigroups and Partial Semigroups›
  
text ‹Every partial semigroup is a relational partial semigroup.›
  
context partial_semigroup 
begin

sublocale rel_partial_semigroup: rel_semigroup "R"
  by standard (metis add_assoc add_assocD)

end

text ‹Every partial monoid is a relational monoid.›
  
context partial_monoid 
begin
  
sublocale rel_partial_monoid: rel_monoid "R" "E"
  apply standard
    apply (metis unitl_ex)
    apply (metis unitr_ex)
   apply (metis add_assocD_var1 unitl_ex units_eq_var)
  by (metis add_assocD_var2 unitr_ex units_eq_var)

end

text ‹Every PAS is a relational abelian semigroup.›
  
context pas 
begin
  
sublocale rel_pas: rel_ab_semigroup "R"
  apply standard
  using add_comm by blast

end
  
text ‹Every PAM is a relational abelian monoid.›
  
context pam 
begin

sublocale rel_pam: rel_ab_monoid "R" "E" ..

end
  

subsection ‹Liftings of Partial Abelian Semigroups›

text ‹Functions from partial semigroups into weak quantales form weak proto-quantales.›  

instantiation "fun" :: (partial_semigroup, weak_quantale) weak_proto_quantale
begin
  
definition times_fun :: "('a  'b)  ('a  'b)  'a  'b" where
  "times_fun  rel_partial_semigroup.times_rel_fun"
  
text ‹The following counterexample shows that the associativity law may fail in convolution algebras
of functions from partial semigroups into weak quantales. ›
  
lemma "(rel_partial_semigroup.times_rel_fun (rel_partial_semigroup.times_rel_fun f f) f) x =
  (rel_partial_semigroup.times_rel_fun (f::'a::partial_semigroup  'b::weak_quantale) (rel_partial_semigroup.times_rel_fun f f)) x"
(*  nitpick[show_all]*)
  oops
    
lemma "rel_partial_semigroup.times_rel_fun (rel_partial_semigroup.times_rel_fun f g) h =
  rel_partial_semigroup.times_rel_fun (f::'a::partial_semigroup  'b::weak_quantale) (rel_partial_semigroup.times_rel_fun g h)"
(*  nitpick[show_all]*)
  oops
  
instance
  by standard (simp_all add: times_fun_def rel_partial_semigroup.rel_fun_Sup_distr rel_magma.rel_fun_Sup_distl_weak)

end
    
text ‹Functions from partial semigroups into quantales form quantales.›  
  
instance "fun" :: (partial_semigroup, quantale) quantale
  by standard (simp_all add: times_fun_def rel_partial_semigroup.rel_fun_assoc rel_magma.rel_fun_Sup_distl)

  
text ‹The following counterexample shows that the right unit law may fail in convolution algebras
of functions from partial monoids into weak unital quantales. ›
  
lemma "(rel_partial_semigroup.times_rel_fun (f::'a::partial_monoid  'b::unital_weak_quantale) rel_partial_monoid.pid) x = f x"
  (*nitpick[show_all]*)
  oops
    
text ‹Functions from partial monoids into unital quantales form unital quantales.›
    
instantiation "fun" :: (partial_monoid, unital_quantale) unital_quantale
begin

definition one_fun :: "'a  'b" where
  "one_fun  rel_partial_monoid.pid"

instance
  by standard (simp_all add: one_fun_def times_fun_def)

end
  
text ‹These lifting results extend to PASs and PAMs as expected.›

instance "fun" :: (pam, ab_quantale) ab_quantale
  by standard (simp_all add: times_fun_def rel_pas.rel_fun_comm)

instance "fun" :: (pam, bool_ab_quantale) bool_ab_quantale ..

instance "fun" :: (pam, bool_ab_unital_quantale) bool_ab_unital_quantale ..

sublocale ab_quantale < abq: pas "(*)" "λ_ _. True"
  apply standard
  apply (simp_all add: mult_assoc)
  by (simp add: mult_commute)

text ‹Finally we prove some identities that hold in function spaces.›
    
lemma times_fun_var: "(f * g) x = {f y * g z | y z. R x y z}"
  by (simp add: times_fun_def rel_partial_semigroup.times_rel_fun_def bmod_comp_def)

lemma times_fun_var2: "(f * g) = (λx. {f y * g z | y z. R x y z})"
  by (auto simp: times_fun_var)

lemma one_fun_var1 [simp]: "x  E  1 x = 1"
  by (simp add: one_fun_def rel_partial_monoid.pid_def)
    
lemma one_fun_var2 [simp]: "x  E  1 x = "
  by (simp add: one_fun_def rel_partial_monoid.pid_def)
    
lemma times_fun_canc: "(f * g) x = {f y * g (rquot x y) | y. y R x}"
  apply (rule antisym)
   apply (simp add: times_fun_var, intro Sup_subset_mono, simp add: Collect_mono_iff)
  using gR_rel_mult add_canc1 apply force 
  apply (simp add: times_fun_var, intro Sup_subset_mono, simp add: Collect_mono_iff)
  using gR_rel_defined add_canc2 by fastforce

lemma times_fun_prod: "(f * g) = (λ(x, y). {f (x, y1) * g (x, y2) | y1 y2. R y y1 y2})"
  by (auto simp: times_fun_var2 times_prod_def D_prod_def)

lemma one_fun_prod1 [simp]: "y  E  1 (x, y) = 1"
  by (simp add: E_prod_def)

lemma one_fun_prod2 [simp]: "y  E  1 (x, y) = "
  by (simp add: E_prod_def)

lemma fres_galois_funI: "x. (f * g) x  h x  f x  (h  g) x"
  by (meson fres_galois le_funD le_funI)
    
lemma times_fun_prod_canc: "(f * g) (x, y) = {f (x, z) * g (x, rquot y z) | z. z R y}"
  apply (simp add: times_fun_prod)
  by (metis (no_types, lifting) gR_rel_defined gR_rel_mult add_canc1 add_canc2)
    
text ‹The following statement shows, in a generalised setting, that the magic wand operator of separation
logic can be lifted from the heap subtraction operation generalised to a cancellative PAM.›

lemma fres_lift: "(fres f g) (x::'b::cancellative_pam) = {(f y)  (g z) | y z . z R y  x = rquot y z}"
proof (rule antisym)
  { fix h y z 
    assume assms: "h  g  f" "z R y" "x = rquot y z"
    moreover hence  "D z x" 
      using add_rquot by blast
    moreover hence "h x  g z  (h  g) (x  z)"
      using add_comm by (auto simp add: times_fun_var intro!: Sup_upper)
    moreover hence "(h * g) (x  z)  f (z  x)"
      by (simp add: ‹D z x calculation(1) le_funD add_comm)
    ultimately have "h x  (f (z  x))  (g z)"
      by (auto simp: fres_def intro: Sup_upper)
    from this and assms have "h (rquot y z)  (f y)  (g z)"
      by (simp add: add_canc2)
} 
  thus "(f  g) x  {(f y)  (g z) |y z. z R y  x = rquot y z}"
    by (clarsimp simp: fres_def intro!: Inf_greatest SUP_least)
next
  have "{(f y)  (g z) |y z. z R y  x = rquot y z}  Sup{x. x  g  f} x"
    apply (clarsimp simp: times_fun_var intro!: SUP_upper le_funI Sup_least)
    apply (simp add: fres_galois)
    apply (intro Inf_lower)
    apply safe
    by (metis gR_rel_mult add_canc1 add_comm)
  thus "{(f y)  (g z) |y z. z R y  x = rquot y z}  (f  g) x "
    by (simp add: fres_def)
qed

end