# 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 f∈F. 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}"
hence "f ∈ F ⟹ f y ≤ ⨆{f y |f. f ∈ F}"
thus "(SUP f∈F. f y) ≤ ⨆{(f::'a ⇒ 'b::proto_near_quantale) y |f. f ∈ F}"
next
fix x
have "x ∈ {f y |f. f ∈ F} ⟹ x ≤ (SUP f∈F. f y) "
using mk_disjoint_insert by force
thus "Sup {(f::'a ⇒ 'b::proto_near_quantale) y |f. f ∈ F} ≤ (SUP f∈F. f y)"
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 (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}"
also have "... = ⨆{⨆{f y ⋅ g z |f. f ∈ ℱ} |y z. R x y z}"
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
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}"
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}"
also have "... = ⨆{⨆{f y ⋅ g z |g. g ∈ 𝒢} |y z. R x y z}"
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))"
finally show ?thesis
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))"
finally show ?thesis
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 (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}"
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}"
also have "... = ⨆{f u ⋅ ⨆{g v ⋅ h z |v z. ρ y v z} |u y. ρ x u y}"
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 (rule antisym)
apply (rule Sup_least, safe)
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 (rule antisym)
apply (rule Sup_least, safe)
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 (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}"
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}"
also have "... = ⨆{f u ⋅ ⨆{g v ⋅ h z |v z. ρ y v z} |u y. ρ x u y}"
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"

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

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"

interpretation rel_fun2: quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup ⇒ 'b::quantale"

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 minus uminus inf less_eq less sup bot ‹top::'a::rel_semigroup ⇒ 'b::bool_quantale› Inf Sup 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 minus uminus inf less_eq less sup bot ‹top::'a::rel_monoid ⇒ 'b::bool_unital_quantale› Inf Sup 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"