Theory Quantales
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] 900)
and Inf (‹⨅_› [900] 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"
by (simp add: sup_inf_distrib1)
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"
by (simp add: Sup_upper bres_def)
lemma fres_galois: "x ⋅ y ≤ z ⟷ x ≤ z ← y"
proof
show "x ⋅ y ≤ z ⟹ x ≤ z ← y"
by (simp add: Sup_upper fres_def)
next
assume "x ≤ z ← y"
hence "x ⋅ y ≤ ⨆{x. x ⋅ y ≤ z} ⋅ y"
by (simp add: fres_def mult_isor)
also have "... = ⨆{x ⋅ y |x. x ⋅ y ≤ z}"
by (simp add: Sup_distr)
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"
by (simp add: weak_Sup_distl)
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"
oops
end
class proto_quantale = proto_near_quantale +
assumes Sup_distl: "x ⋅ ⨆Y = ⨆{x ⋅ y |y. y ∈ Y}"
begin
subclass weak_proto_quantale
by standard (simp add: Sup_distl)
lemma bres_galois: "x ⋅ y ≤ z ⟷ y ≤ x → z"
proof
show "x ⋅ y ≤ z ⟹ y ≤ x → z"
by (simp add: Sup_upper bres_def)
next
assume "y ≤ x → z"
hence "x ⋅ y ≤ x ⋅ ⨆{y. x ⋅ y ≤ z}"
by (simp add: bres_def mult_isol)
also have "... = ⨆{x ⋅ y |y. x ⋅ y ≤ z}"
by (simp add: Sup_distl)
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"
apply (simp add: iter_def)
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 ⋅ ⊥ = ⊥"
oops
class unital_weak_quantale = weak_quantale + monoid_mult
lemma (in unital_weak_quantale) "x ⋅ ⊥ = ⊥"
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
apply (simp add: inf.assoc)
apply (simp add: inf.commute)
apply (simp add: Setcompr_eq_image Sup_inf)
apply (simp add: Setcompr_eq_image inf_Sup)
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)+)