# 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"

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)

end

text ‹Every PAS is a relational abelian semigroup.›

context pas
begin

sublocale rel_pas: rel_ab_semigroup "R"
apply standard

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

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"

lemma one_fun_var2 [simp]: "x ∉ E ⟹ 1 x = ⊥"

lemma times_fun_canc: "(f * g) x = ⨆{f y * g (rquot x y) | y. y ≼⇩R x}"
apply (rule antisym)

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"

lemma one_fun_prod2 [simp]: "y ∉ E ⟹ 1 (x, y) = ⊥"

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}"

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"
moreover hence "h x ⋅ g z ≤ (h ⋅ g) (x ⊕ z)"
moreover hence "(h * g) (x ⊕ z) ≤ f (z ⊕ x)"
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)"
}
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)