Theory Partial_Semigroup_Lifting
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"
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)"
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"
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