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}"
    by (simp add: Setcompr_eq_image)
  hence "f ∈ F ⟹ f y ≤ ⨆{f y |f. f ∈ F}"
    by (simp add: Sup_upper)
  thus "(SUP f∈F. f y) ≤ ⨆{(f::'a ⇒ 'b::proto_near_quantale) y |f. f ∈ F}"
    by (simp add: Setcompr_eq_image)
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)"
    by (simp add: Setcompr_eq_image)
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 (simp add: bmod_comp_def)
  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}"
    by (simp add: bmod_comp_def SUP_is_Sup)
  also have "... = ⨆{⨆{f y ⋅ g z |f. f ∈ ℱ} |y z. R x y z}"
    by (simp add: Sup_distr bmod_auxl)
  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
    by (simp add: bmod_comp_def)
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}"
    by (simp add: bmod_comp_def SUP_is_Sup)
  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}"
    by (simp add:  bmod_comp_def SUP_is_Sup)
  also have "... = ⨆{⨆{f y ⋅ g z |g. g ∈ 𝒢} |y z. R x y z}"
    by (simp add: Sup_distl 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_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))"
    by (simp add: bres_galois)
  finally show ?thesis
    apply (simp add: fun_eq_iff bmod_bres_def)
    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))"
    by (simp add: fres_galois)
  finally show ?thesis
    apply (simp add: bmod_fres_def fun_eq_iff)
    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 (simp add: bmod_comp_def Sup_distr)
    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}"
    by (simp add: bmod_assoc_aux1)
  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}" 
    by (simp add: bmod_assoc_aux2)
  also have "... = ⨆{f u ⋅ ⨆{g v ⋅ h z |v z. ρ y v z} |u y. ρ x u y}" 
    apply (simp add: Sup_distl mult.assoc)
    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 (simp add: bmod_comp_def pid_def)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (simp add: bres_galois)
  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 (simp add: bmod_comp_def pid_def)
  apply (rule antisym)
  apply (rule Sup_least, safe)
  apply (simp add: fres_galois)
  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 (simp add: bmod_comp_def Sup_distr)
    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}"
    by (simp add: bmod_assoc_aux1)
  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}" 
    by (simp add: bmod_assoc_aux2)
  also have "... = ⨆{f u ⋅ ⨆{g v ⋅ h z |v z. ρ y v z} |u y. ρ x u y}"
    by (simp add: bmod_assoc_weak_aux) 
  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"
  by (simp add: times_rel_fun_def bmod_comm)

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
  by standard (simp add: rel_fun_Sup_distl)
    
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"
  by standard (simp_all add: rel_fun_assoc_weak) 

interpretation rel_fun2: quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_semigroup ⇒ 'b::quantale" 
  by standard (simp add: rel_fun_assoc)
    
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"
  by standard (simp add: rel_fun_comm)

interpretation rel_fun: ab_unital_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid ⇒ 'b::ab_unital_quantale" pid ..

interpretation rel_fun2: distrib_ab_unital_quantale Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid ⇒ 'b::distrib_ab_unital_quantale" times_rel_fun pid ..

interpretation rel_fun2: bool_ab_unital_quantale times_rel_fun Inf Sup inf less_eq less sup bot "top::'a::rel_ab_monoid ⇒ 'b::bool_ab_unital_quantale" minus uminus pid ..
    
end