# Theory Quantales

```(* Title: Quantales
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 ‹Quantales›

text ‹This entry will be merged eventually with other quantale entries and become a standalone one.›

theory Quantales
imports Main

begin

notation sup (infixl "⊔" 60)
and inf (infixl "⊓" 55)
and top ("⊤")
and bot ("⊥")
and relcomp (infixl ";" 70)
and times (infixl "⋅" 70)
and Sup ("⨆_"  900)
and Inf ("⨅_"  900)

subsection ‹Properties of Complete Lattices›

lemma (in complete_lattice) Sup_sup_pred: "x ⊔ ⨆{y. P y} = ⨆{y. y = x ∨ P y}"
apply (rule order.antisym)
apply (simp add: Collect_mono Sup_subset_mono Sup_upper)
using Sup_least Sup_upper sup.coboundedI2 by force

lemma (in complete_lattice) sup_Sup: "x ⊔ y = ⨆{x,y}"
by simp

lemma (in complete_lattice) sup_Sup_var: "x ⊔ y = ⨆{z. z ∈ {x,y}}"
by (metis Collect_mem_eq sup_Sup)

lemma (in complete_boolean_algebra) shunt1: "x ⊓ y ≤ z ⟷ x ≤ -y ⊔ z"
proof standard
assume "x ⊓ y ≤ z"
hence  "-y ⊔ (x ⊓ y) ≤ -y ⊔ z"
using sup.mono by blast
hence "-y ⊔ x ≤ -y ⊔ z"
thus "x ≤ -y ⊔ z"
by simp
next
assume "x ≤ - y ⊔ z"
hence "x ⊓ y ≤ (-y ⊔ z) ⊓ y"
using inf_mono by auto
thus  "x ⊓ y ≤ z"
using inf.boundedE inf_sup_distrib2 by auto
qed

lemma (in complete_boolean_algebra) meet_shunt: "x ⊓ y = ⊥ ⟷ x ≤ -y"
by (metis bot_least inf_absorb2 inf_compl_bot_left2 shunt1 sup_absorb1)

lemma (in complete_boolean_algebra) join_shunt: "x ⊔ y = ⊤ ⟷ -x ≤ y"
by (metis compl_sup compl_top_eq double_compl meet_shunt)

subsection ‹ Familes of Proto-Quantales›

text ‹Proto-Quanales are complete lattices equipped with an operation of composition or multiplication
that need not be associative.›

class proto_near_quantale = complete_lattice + times +
assumes Sup_distr: "⨆X ⋅ y = ⨆{x ⋅ y |x. x ∈ X}"

begin

lemma mult_botl [simp]: "⊥ ⋅ x = ⊥"
using Sup_distr[where X="{}"] by auto

lemma sup_distr: "(x ⊔ y) ⋅ z = (x ⋅ z) ⊔ (y ⋅ z)"
using Sup_distr[where X="{x, y}"] by (fastforce intro!: Sup_eqI)

lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
by (metis sup.absorb_iff1 sup_distr)

definition bres :: "'a ⇒ 'a ⇒ 'a" (infixr "→" 60) where
"x → z = ⨆{y. x ⋅ y ≤ z}"

definition fres :: "'a ⇒ 'a ⇒ 'a" (infixl "←" 60) where
"z ← y = ⨆{x. x ⋅ y ≤ z}"

lemma bres_galois_imp: "x ⋅ y ≤ z ⟶ y ≤ x → z"

lemma fres_galois: "x ⋅ y ≤ z ⟷ x ≤ z ← y"
proof
show "x ⋅ y ≤ z ⟹ x ≤ z ← y"
next
assume "x ≤ z ← y"
hence "x ⋅ y ≤ ⨆{x. x ⋅ y ≤ z} ⋅ y"
also have "... = ⨆{x ⋅ y |x. x ⋅ y ≤ z}"
also have "... ≤ z"
by (rule Sup_least, auto)
finally show "x ⋅ y ≤ z" .
qed

end

class proto_pre_quantale = proto_near_quantale +
assumes Sup_subdistl: "⨆{x ⋅ y | y . y ∈ Y} ≤ x ⋅ ⨆Y"

begin

lemma sup_subdistl: "(x ⋅ y) ⊔ (x ⋅ z) ≤ x ⋅ (y ⊔ z)"
using Sup_subdistl[where Y="{y, z}"] Sup_le_iff by auto

lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
by (metis le_iff_sup le_sup_iff sup_subdistl)

end

class weak_proto_quantale = proto_near_quantale +
assumes weak_Sup_distl: "Y ≠ {} ⟹ x ⋅ ⨆Y = ⨆{x ⋅ y |y. y ∈ Y}"

begin

subclass proto_pre_quantale
proof standard
have a: "⋀x Y. Y = {} ⟹ ⨆{x ⋅ y |y. y ∈ Y} ≤ x ⋅ ⨆Y"
by simp
have b: "⋀x Y. Y ≠ {} ⟹ ⨆{x ⋅ y |y. y ∈ Y} ≤ x ⋅ ⨆Y"
show  "⋀x Y. ⨆{x ⋅ y |y. y ∈ Y} ≤ x ⋅ ⨆Y"
using a b by blast
qed

lemma  sup_distl: "x ⋅ (y ⊔ z) = (x ⋅ y) ⊔ (x ⋅ z)"
using weak_Sup_distl[where Y="{y, z}"] by (fastforce intro!: Sup_eqI)

lemma "y ≤ x → z ⟶ x ⋅ y ≤ z" (* nitpick [expect = genuine] *)
oops

end

class proto_quantale = proto_near_quantale +
assumes Sup_distl: "x ⋅ ⨆Y = ⨆{x ⋅ y |y. y ∈ Y}"

begin

subclass weak_proto_quantale

lemma bres_galois: "x ⋅ y ≤ z ⟷ y ≤ x → z"
proof
show "x ⋅ y ≤ z ⟹ y ≤ x → z"
next
assume "y ≤ x → z"
hence "x ⋅ y ≤ x ⋅ ⨆{y. x ⋅ y ≤ z}"
also have "... = ⨆{x ⋅ y |y. x ⋅ y ≤ z}"
also have "... ≤ z"
by (rule Sup_least, auto)
finally show "x ⋅ y ≤ z" .
qed

end

subsection ‹Families of Quantales›

class near_quantale = proto_near_quantale + semigroup_mult

class unital_near_quantale = near_quantale + monoid_mult

begin

definition iter :: "'a ⇒ 'a" where
"iter x ≡ ⨅{y. ∃i. y = x ^ i}"

lemma iter_ref [simp]: "iter x ≤ 1"
by (metis (mono_tags, lifting) Inf_lower local.power.power_0 mem_Collect_eq)

lemma le_top: "x ≤ ⊤ ⋅ x"
by (metis mult_isor mult.monoid_axioms top_greatest monoid.left_neutral)

end

class pre_quantale = proto_pre_quantale + semigroup_mult

subclass (in pre_quantale) near_quantale ..

class unital_pre_quantale = pre_quantale + monoid_mult

subclass (in unital_pre_quantale) unital_near_quantale ..

class weak_quantale = weak_proto_quantale + semigroup_mult

subclass (in weak_quantale) pre_quantale ..

text ‹The following counterexample shows an important consequence of weakness:
the absence of right annihilation.›

lemma (in weak_quantale) "x ⋅ ⊥ = ⊥" (*nitpick[expect=genuine]*)
oops

class unital_weak_quantale = weak_quantale + monoid_mult

lemma (in unital_weak_quantale) "x ⋅ ⊥ = ⊥" (*nitpick[expect=genuine]*)
oops

subclass (in unital_weak_quantale) unital_pre_quantale ..

class quantale = proto_quantale + semigroup_mult

begin

subclass weak_quantale ..

lemma mult_botr [simp]: "x ⋅ ⊥ = ⊥"
using Sup_distl[where Y="{}"] by auto

end

class unital_quantale = quantale + monoid_mult

subclass (in unital_quantale) unital_weak_quantale ..

class ab_quantale = quantale + ab_semigroup_mult

begin

lemma bres_fres_eq: "x → y = y ← x"
by (simp add: fres_def bres_def mult_commute)

end

class ab_unital_quantale = ab_quantale + unital_quantale

class distrib_quantale = quantale + complete_distrib_lattice

class bool_quantale = quantale + complete_boolean_algebra

class distrib_unital_quantale = unital_quantale + complete_distrib_lattice

class bool_unital_quantale = unital_quantale + complete_boolean_algebra

class distrib_ab_quantale = distrib_quantale + ab_quantale

class bool_ab_quantale = bool_quantale + ab_quantale

class distrib_ab_unital_quantale = distrib_quantale + unital_quantale

class bool_ab_unital_quantale = bool_ab_quantale + unital_quantale

subsection ‹Quantales of Booleans and Complete Boolean Algebras›

instantiation bool :: bool_ab_unital_quantale
begin

definition "one_bool = True"

definition "times_bool = (λx y. x ∧ y)"

instance
by standard (auto simp: times_bool_def one_bool_def)

end

context complete_distrib_lattice
begin

interpretation cdl_quantale: distrib_quantale _ _ _ _ _ _ _ _ inf
by standard (simp_all add: inf.assoc Setcompr_eq_image Sup_inf inf_Sup)

end

context complete_boolean_algebra
begin

interpretation cba_quantale: bool_ab_unital_quantale inf _ _ _ _ _ _ _ _ _ _ top
apply standard
by simp_all

text ‹In this setting, residuation can be translated like classical implication.›

lemma cba_bres1: "x ⊓ y ≤ z ⟷ x ≤ cba_quantale.bres y z"
using cba_quantale.bres_galois inf.commute by fastforce

lemma cba_bres2: "x ≤ -y ⊔ z ⟷ x ≤ cba_quantale.bres y z"
using cba_bres1 shunt1 by auto

lemma cba_bres_prop: "cba_quantale.bres x y = -x ⊔ y"
using cba_bres2 order.eq_iff by blast

end

text ‹Other models will follow.›

subsection ‹Products of Quantales›

definition "Inf_prod X = (⨅{fst x |x. x ∈ X}, ⨅{snd x |x.  x ∈ X})"

definition "inf_prod x y = (fst x ⊓ fst y, snd x ⊓ snd y)"

definition "bot_prod = (bot,bot)"

definition "Sup_prod X = (⨆{fst x |x. x ∈ X}, ⨆{snd x |x.  x ∈ X})"

definition "sup_prod x y = (fst x ⊔ fst y, snd x ⊔ snd y)"

definition "top_prod = (top,top)"

definition "less_eq_prod x y ≡ less_eq (fst x) (fst y) ∧ less_eq (snd x) (snd y)"

definition "less_prod x y ≡ less_eq (fst x) (fst y) ∧ less_eq (snd x) (snd y) ∧ x ≠ y"

definition "times_prod' x y = (fst x ⋅ fst y, snd x ⋅ snd y)"

definition "one_prod = (1,1)"

interpretation prod: complete_lattice Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::complete_lattice × 'b::complete_lattice)"
apply standard
apply (simp_all add: Inf_prod_def Sup_prod_def inf_prod_def sup_prod_def bot_prod_def top_prod_def less_eq_prod_def less_prod_def Sup_distl Sup_distr)
apply force+
apply (rule conjI, (rule Inf_lower, force)+)
apply (rule conjI, (rule Inf_greatest, force)+)
apply (rule conjI, (rule Sup_upper, force)+)
by (rule conjI, (rule Sup_least, force)+)

interpretation prod: proto_near_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_near_quantale × 'b::proto_near_quantale)" times_prod'
apply (standard, simp add: times_prod'_def Sup_prod_def)
by (rule conjI, (simp add: Sup_distr, clarify, metis)+)

interpretation prod: proto_quantale Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::proto_quantale × 'b::proto_quantale)" times_prod'
apply (standard, simp add: times_prod'_def Sup_prod_def less_eq_prod_def)
by (rule conjI, (simp add: Sup_distl, metis)+)

interpretation prod: unital_quantale one_prod times_prod' Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod "top_prod :: ('a::unital_quantale × 'b::unital_quantale)"
by standard (simp_all add: one_prod_def times_prod'_def mult.assoc)

subsection ‹Quantale Modules and Semidirect Products›

text ‹Quantale modules are extensions of semigroup actions in that a quantale acts on a complete lattice.›

locale unital_quantale_module =
fixes act :: "'a::unital_quantale ⇒ 'b::complete_lattice ⇒ 'b" ("α")
assumes act1: "α (x ⋅ y) p = α x (α y p)"
and act2 [simp]: "α 1 p = p"
and act3: "α (⨆X) p = ⨆{α x p |x. x ∈ X}"
and act4: "α x (⨆P) = ⨆{α x p |p. p ∈ P}"

context unital_quantale_module
begin

text ‹Actions are morphisms. The curried notation is particularly convenient for this.›

lemma act_morph1: "α (x ⋅ y) = (α x) ∘ (α y)"

lemma act_morph2: "α 1 = id"

lemma emp_act: "α (⨆{}) p = ⊥"
by (simp only: act3, force)

lemma emp_act_var: "α ⊥ p = ⊥"
using emp_act by auto

lemma act_emp: "α x (⨆{}) = ⊥"
by (simp only: act4, force)

lemma act_emp_var: "α x ⊥ = ⊥"
using act_emp by auto

lemma act_sup_distl: "α x (p ⊔ q) = (α x p) ⊔ (α x q)"
proof-
have "α x (p ⊔ q) = α x (⨆{p,q})"
by simp
also have "... = ⨆{α x y |y. y ∈ {p,q}}"
by (rule act4)
also have "... = ⨆{v. v = α x p ∨ v = α x q}"
by (metis empty_iff insert_iff)
finally show ?thesis
by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed

lemma act_sup_distr: "α (x ⊔ y) p = (α x p) ⊔ (α y p)"
proof-
have "α (x ⊔ y) p  = α (⨆{x,y}) p"
by simp
also have "... = ⨆{α v p |v. v ∈ {x,y}}"
by (rule act3)
also have "... = ⨆{v. v = α x p ∨ v = α y p}"
by (metis empty_iff insert_iff)
finally show ?thesis
by (metis Collect_disj_eq Sup_insert ccpo_Sup_singleton insert_def singleton_conv)
qed

lemma act_sup_distr_var: "α (x ⊔ y) = (α x) ⊔ (α y)"

text ‹Next we define the semidirect product of a  unital quantale and a complete lattice. ›

definition "sd_prod x y = (fst x ⋅ fst y, snd x ⊔ α (fst x) (snd y))"

lemma sd_distr_aux:
"⨆{snd x |x. x ∈ X} ⊔ ⨆{α (fst x) p |x. x ∈ X} = ⨆{snd x ⊔ α (fst x) p |x. x ∈ X}"
proof (rule antisym, rule sup_least)
show "⨆{snd x |x. x ∈ X} ≤ ⨆{snd x ⊔ α (fst x) p |x. x ∈ X}"
proof (rule Sup_least)
fix x :: 'b
assume "x ∈ {snd x |x. x ∈ X}"
hence "∃b pa. x ⊔ b = snd pa ⊔ α (fst pa) p ∧ pa ∈ X"
by blast
hence "∃b. x ⊔ b ∈ {snd pa ⊔ α (fst pa) p |pa. pa ∈ X}"
by blast
thus "x ≤ ⨆{snd pa ⊔ α (fst pa) p |pa. pa ∈ X}"
by (meson Sup_upper sup.bounded_iff)
qed
next
show "⨆{α (fst x) p |x. x ∈ X} ≤ ⨆{snd x ⊔ α (fst x) p |x. x ∈ X}"
proof (rule Sup_least)
fix x :: 'b
assume "x ∈ {α (fst x) p |x. x ∈ X}"
then have "∃b pa. b ⊔ x = snd pa ⊔ α (fst pa) p ∧ pa ∈ X"
by blast
then have "∃b. b ⊔ x ∈ {snd pa ⊔ α (fst pa) p |pa. pa ∈ X}"
by blast
then show "x ≤ ⨆{snd pa ⊔ α (fst pa) p |pa. pa ∈ X}"
by (meson Sup_upper le_supE)
qed
next
show "⨆{snd x ⊔ α (fst x) p |x. x ∈ X} ≤ ⨆{snd x |x. x ∈ X} ⊔ ⨆{α (fst x) p |x. x ∈ X}"
apply (rule Sup_least)
apply safe
apply (rule sup_least)
apply (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI1)
by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq sup.coboundedI2)
qed

lemma sd_distr: "sd_prod (Sup_prod X) y = Sup_prod {sd_prod x y |x. x ∈ X}"
proof -
have "sd_prod (Sup_prod X) y = sd_prod (⨆{fst x |x. x ∈ X}, ⨆{snd x |x. x ∈ X}) y"
also have
"... = ((⨆{fst x |x. x ∈ X}) ⋅ fst y, (⨆{snd x |x. x ∈ X}) ⊔ (α (⨆{fst x | x. x ∈ X})  (snd y)))"
also have
"... = (⨆{fst x ⋅ fst y|x. x ∈ X}, (⨆{snd x |x. x ∈ X}) ⊔ (α (⨆{fst x | x. x ∈ X})  (snd y)))"
also have
"... = (⨆{fst x ⋅ fst y|x. x ∈ X}, (⨆ {snd x |x. x ∈ X}) ⊔ (⨆{α (fst x) (snd y) | x. x ∈ X}))"
also have "... = (⨆{fst x ⋅ fst y|x. x ∈ X}, ⨆{snd x ⊔ (α (fst x) (snd y)) | x. x ∈ X})"
by (simp only: sd_distr_aux)
also have "... = Sup_prod {(fst x ⋅ fst y, snd x ⊔ (α (fst x) (snd y))) |x. x ∈ X}"
finally show ?thesis
qed

lemma sd_distl_aux: "Y ≠ {} ⟹ p ⊔ (⨆{α x (snd y) |y. y ∈ Y}) = ⨆{p ⊔ α x (snd y) |y. y ∈ Y}"
proof (rule antisym, rule sup_least)
show "Y ≠ {} ⟹ p ≤ ⨆{p ⊔ α x (snd y) |y. y ∈ Y}"
proof -
assume "Y ≠ {}"
hence "∃b. b ∈ {p ⊔ α x (snd pa) |pa. pa ∈ Y} ∧ p ≤ b"
by fastforce
thus "p ≤ ⨆{p ⊔ α x (snd pa) |pa. pa ∈ Y}"
by (meson Sup_upper2)
qed
next
show "Y ≠ {} ⟹ ⨆{α x (snd y) |y. y ∈ Y} ≤ ⨆{p ⊔ α x (snd y) |y. y ∈ Y}"
apply (rule Sup_least)
proof -
fix xa :: 'b
assume "xa ∈ {α x (snd y) |y. y ∈ Y}"
then have "∃b. (∃pa. b = p ⊔ α x (snd pa) ∧ pa ∈ Y) ∧ xa ≤ b"
by fastforce
then have "∃b. b ∈ {p ⊔ α x (snd pa) |pa. pa ∈ Y} ∧ xa ≤ b"
by blast
then show "xa ≤ ⨆{p ⊔ α x (snd pa) |pa. pa ∈ Y}"
by (meson Sup_upper2)
qed
next
show "Y ≠ {} ⟹ ⨆{p ⊔ α x (snd y) |y. y ∈ Y} ≤ p ⊔ ⨆{α x (snd y) |y. y ∈ Y}"
apply (rule Sup_least)
apply safe
by (metis (mono_tags, lifting) Sup_le_iff le_sup_iff mem_Collect_eq sup_ge1 sup_ge2)
qed

lemma sd_distl: "Y ≠ {} ⟹ sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y ∈ Y}"
proof -
assume a: "Y ≠ {}"
have "sd_prod x (Sup_prod Y) = sd_prod x (⨆{fst y |y. y ∈ Y}, ⨆{snd y |y. y ∈ Y})"
also have "... = ((fst x) ⋅ (⨆{fst y |y. y ∈ Y}), (snd x ⊔ (α (fst x) (⨆{snd y |y. y ∈ Y}))))"
also have "... = (⨆{fst x ⋅ fst y |y. y ∈ Y}, (snd x ⊔ (α (fst x) (⨆{snd y |y. y ∈ Y}))))"
also have "... = (⨆{fst x ⋅ fst y |y. y ∈ Y}, (snd x ⊔ (⨆{α (fst x) (snd y) |y. y ∈ Y})))"
also have "... = (⨆{fst x ⋅ fst y |y. y ∈ Y}, ⨆{snd x ⊔ (α (fst x) (snd y)) |y. y ∈ Y})"
using a sd_distl_aux by blast
also have "... = Sup_prod {(fst x ⋅ fst y, snd x ⊔ (α (fst x) (snd y))) |y. y ∈ Y}"
finally show ?thesis
qed

definition "sd_unit = (1,⊥)"

lemma sd_unitl [simp]: "sd_prod sd_unit x = x"

lemma sd_unitr [simp]: "sd_prod x sd_unit = x"
using act_emp by force

text ‹The following counterexamples rule out that semidirect products of quantales and complete lattices form quantales.
The reason is that the right annihilation law fails.›

lemma "sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y ∈ Y}" (*nitpick[show_all,expect=genuine]*)
oops

lemma "sd_prod x bot_prod = bot_prod" (*nitpick[show_all,expect=genuine]*)
oops

text ‹However we can show that semidirect products of (unital) quantales with complete lattices form weak (unital) quantales. ›

interpretation dp_quantale: weak_quantale sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
apply standard