Theory Partial_Semigroup_Lifting

(* Title: Liftings of Partial Semigroups
   Author: Brijesh Dongol, Victor Gomes, Ian J Hayes, Georg Struth
   Maintainer: Victor Gomes <>
               Georg Struth <> 

section ‹Liftings of Partial Semigroups›

theory Partial_Semigroup_Lifting
  imports Partial_Semigroups Binary_Modalities

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 

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


text ‹Every partial monoid is a relational monoid.›
context partial_monoid 
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)


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

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

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


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
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]*)
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]*)
  by standard (simp_all add: times_fun_def rel_partial_semigroup.rel_fun_Sup_distr rel_magma.rel_fun_Sup_distl_weak)

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) x = f x"
text ‹Functions from partial monoids into unital quantales form unital quantales.›
instantiation "fun" :: (partial_monoid, unital_quantale) unital_quantale

definition one_fun :: "'a  'b" where

  by standard (simp_all add: one_fun_def times_fun_def)

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