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