Theory Quantales
section ‹Quantales›
theory Quantales
imports
"Order_Lattice_Props.Closure_Operators"
Kleene_Algebra.Dioid
begin
subsection ‹Families of Proto-Quantales›
text ‹Proto-Quanales are complete lattices equipped with an operation of composition or multiplication
that need not be associative. The notation in this component differs from Rosenthal's \<^cite>‹"Rosenthal90"›, but is consistent with the one we use
for semirings and Kleene algebras.›
class proto_near_quantale = complete_lattice + times +
assumes Sup_distr: "⨆X ⋅ y = (⨆x ∈ X. x ⋅ y)"
lemma Sup_pres_multr: "Sup_pres (λ(z::'a::proto_near_quantale). z ⋅ y)"
unfolding fun_eq_iff comp_def Sup_distr by simp
lemma sup_pres_multr: "sup_pres (λ(z::'a::proto_near_quantale). z ⋅ y)"
using Sup_pres_multr Sup_sup_pres by fastforce
lemma bot_pres_multr: "bot_pres (λ(z::'a::proto_near_quantale). z ⋅ y)"
by (metis SUP_empty Sup_distr Sup_empty)
context proto_near_quantale
begin
lemma mult_botl [simp]: "⊥ ⋅ x = ⊥"
proof -
have "⊥ ⋅ x = (⨆a∈{}. a ⋅ x)"
using Sup_distr Sup_empty by blast
thus ?thesis
by simp
qed
lemma sup_distr: "(x ⊔ y) ⋅ z = (x ⋅ z) ⊔ (y ⋅ z)"
by (smt SUP_empty SUP_insert Sup_distr sup_Sup sup_bot.right_neutral)
lemma mult_isor: "x ≤ y ⟹ x ⋅ z ≤ y ⋅ z"
by (metis sup.absorb_iff1 sup_distr)
text ‹Left and right residuals can be defined in every proto-nearquantale.›
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}"
text ‹The left one is a right adjoint to composition. For the right one, additional assumptions are needed›
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 setcompr_eq_image)
also have "... ≤ z"
by (rule Sup_least, auto)
finally show "x ⋅ y ≤ z" .
qed
end
lemma fres_adj: "(λ(x::'a::proto_near_quantale). x ⋅ y) ⊣ (λx. x ← y)"
by (simp add: adj_def fres_galois)
context proto_near_quantale
begin
lemma fres_canc1: "(y ← x) ⋅ x ≤ y"
by (simp add: fres_galois)
lemma fres_canc2: "y ≤ (y ⋅ x) ← x"
using fres_galois by force
lemma inf_fres: "y ⋅ x = ⨅{z. y ≤ z ← x}"
by (metis (mono_tags, lifting) fres_canc2 Inf_eqI fres_galois mem_Collect_eq)
lemma bres_iso: "x ≤ y ⟹ z → x ≤ z → y"
using Sup_le_iff bres_def bres_galois_imp by force
lemma bres_anti: "x ≤ y ⟹ y → z ≤ x → z"
by (smt Sup_le_iff bres_def bres_galois_imp fres_galois order_trans mem_Collect_eq)
lemma fres_iso: "x ≤ y ⟹ x ← z ≤ y ← z"
using fres_galois dual_order.trans by blast
lemma bres_top_top [simp]: "⊤ → ⊤ = ⊤"
by (simp add: bres_galois_imp dual_order.antisym)
lemma fres_top_top [simp]: "⊤ ← ⊤ = ⊤"
using fres_galois top_greatest top_le by blast
lemma bres_bot_bot [simp]: "⊥ → ⊥ = ⊤"
by (simp add: bres_galois_imp top_le)
lemma left_sided_localp: "⊤ ⋅ y = y ⟹ x ⋅ y ≤ y"
by (metis mult_isor top_greatest)
lemma fres_sol: "((y ← x) ⋅ x = y) = (∃z. z ⋅ x = y)"
using dual_order.antisym fres_canc1 fres_canc2 mult_isor by fastforce
lemma sol_fres: "((y ⋅ x) ← x = y) = (∃z. y = z ← x)"
by (metis fres_canc1 fres_canc2 fres_sol order.eq_iff fres_galois)
end
class proto_pre_quantale = proto_near_quantale +
assumes Sup_subdistl: "(⨆y ∈ Y. x ⋅ y) ≤ x ⋅ ⨆Y"
begin
lemma sup_subdistl: "(x ⋅ y) ⊔ (x ⋅ z) ≤ x ⋅ (y ⊔ z)"
by (smt SUP_empty SUP_insert Sup_subdistl sup_Sup sup_bot_right)
lemma mult_isol: "x ≤ y ⟹ z ⋅ x ≤ z ⋅ y"
by (metis le_iff_sup le_sup_iff sup_subdistl)
lemma fres_anti: "x ≤ y ⟹ z ← y ≤ z ← x"
using dual_order.trans fres_galois mult_isol by blast
end
class weak_proto_quantale = proto_near_quantale +
assumes weak_Sup_distl: "Y ≠ {} ⟹ x ⋅ ⨆Y = (⨆y ∈ Y. x ⋅ y)"
begin
subclass proto_pre_quantale
proof unfold_locales
have a: "⋀x Y. Y = {} ⟹ (⨆y ∈ Y. x ⋅ y) ≤ x ⋅ ⨆Y"
by simp
have b: "⋀x Y. Y ≠ {} ⟹ (⨆y ∈ Y. x ⋅ y) ≤ x ⋅ ⨆Y"
by (simp add: weak_Sup_distl)
show "⋀x Y. (⨆y ∈ Y. x ⋅ 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 = (⨆y ∈ Y. x ⋅ y)"
lemma Sup_pres_multl: "Sup_pres (λ(z::'a::proto_quantale). x ⋅ z)"
unfolding fun_eq_iff comp_def Sup_distl by simp
lemma sup_pres_multl: "sup_pres (λ(z::'a::proto_quantale). x ⋅ z)"
by (metis (no_types, lifting) SUP_insert Sup_distl Sup_empty Sup_insert sup_bot_right)
lemma bot_pres_multl: "bot_pres (λ(z::'a::proto_quantale). x ⋅ z)"
by (metis SUP_empty Sup_distl Sup_empty)
context proto_quantale
begin
subclass weak_proto_quantale
by standard (simp add: Sup_distl)
lemma mult_botr [simp]: "x ⋅ ⊥ = ⊥"
by (smt image_empty Sup_distl Sup_empty)
text ‹Now there is also an adjunction for the other residual.›
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 setcompr_eq_image)
also have "... ≤ z"
by (rule Sup_least, safe)
finally show "x ⋅ y ≤ z" .
qed
end
lemma bres_adj: "(λ(y::'a::proto_quantale). x ⋅ y) ⊣ (λy. x → y)"
by (simp add: adj_def bres_galois)
context proto_quantale
begin
lemma bres_canc1: "x ⋅ (x → y) ≤ y"
by (simp add: bres_galois)
lemma bres_canc2: "y ≤ x → (x ⋅ y)"
by (simp add: bres_galois_imp)
lemma inf_bres: "x ⋅ y = ⨅{z. y ≤ x → z}"
using bres_galois fres_galois inf_fres by force
lemma bres_sol: "(x ⋅ (x → y) = y) = (∃z. x ⋅ z = y)"
using bres_galois order.antisym mult_isol by force
lemma sol_bres: "(x → (x ⋅ y) = y) = (∃z. y = x → z)"
by (metis bres_canc1 bres_canc2 bres_iso order.eq_iff)
end
lemma bres_fres_clop: "clop (λx::'a::proto_quantale. y ← (x → y))"
unfolding clop_def comp_def mono_def le_fun_def
by (metis bres_anti bres_canc1 bres_galois_imp fres_anti fres_galois id_apply)
lemma fres_bres_clop: "clop (λx::'a::proto_quantale. (y ← x) → y)"
unfolding clop_def comp_def mono_def le_fun_def
by (metis bres_anti bres_canc1 bres_galois_imp fres_anti fres_canc1 fres_galois id_apply)
subsection ‹Families of Quantales›
class near_quantale = proto_near_quantale + semigroup_mult
sublocale near_quantale ⊆ nsrnq: near_dioid "(⊔)" "(⋅)" "(≤)" "(<)"
apply unfold_locales
apply (simp add: sup_assoc)
apply (simp add: sup_commute)
apply (simp_all add: sup_distr)
apply (simp add: le_iff_sup)
by auto
context near_quantale
begin
lemma fres_curry: "(z ← y) ← x = z ← (x ⋅ y)"
by (metis order.eq_iff fres_canc1 fres_galois mult_assoc)
end
class unital_near_quantale = near_quantale + monoid_mult
sublocale unital_near_quantale ⊆ nsrnqo: near_dioid_one "(⊔)" "(⋅)" "1""(≤)" "(<)"
by (unfold_locales, simp_all)
context unital_near_quantale
begin
definition iter :: "'a ⇒ 'a" where
"iter x ≡ ⨅i. x ^ i"
lemma iter_ref [simp]: "iter x ≤ 1"
by (metis iter_def Inf_lower power.power_0 rangeI)
lemma le_top: "x ≤ ⊤ ⋅ x"
by (metis mult.left_neutral mult_isor top_greatest)
lemma top_times_top [simp]: "⊤ ⋅ ⊤ = ⊤"
by (simp add: le_top top_le)
lemma bres_one: "1 ≤ x → x"
by (simp add: bres_galois_imp)
lemma fres_one: "1 ≤ x ← x"
using fres_galois by fastforce
end
class pre_quantale = proto_pre_quantale + semigroup_mult
begin
subclass near_quantale ..
lemma fres_interchange: "z ⋅ (x ← y) ≤ (z ⋅ x) ← y"
using Sup_upper fres_canc1 fres_def mult_isol mult_assoc by fastforce
end
sublocale pre_quantale ⊆ psrpq: pre_dioid "(⊔)" "(⋅)" "(≤)" "(<)"
by (unfold_locales, simp add: mult_isol)
class unital_pre_quantale = pre_quantale + monoid_mult
begin
subclass unital_near_quantale ..
text ‹Abstract rules of Hoare logic without the star can be derived.›
lemma h_w1: "x ≤ x' ⟹ x' ⋅ y ≤ z ⟹ x ⋅ y ≤ z"
by (simp add: fres_galois)
lemma h_w2: "x ⋅ y ≤ z' ⟹ z' ≤ z ⟹ x ⋅ y ≤ z"
using order_trans by blast
lemma h_seq: "x ⋅ v ≤ z ⟹ y ⋅ w ≤ v ⟹ x ⋅ y ⋅ w ≤ z"
using dual_order.trans mult_isol mult_assoc by presburger
lemma h_sup: "x ⋅ w ≤ z ⟹ y ⋅ w ≤ z ⟹ (x ⊔ y) ⋅ w ≤ z"
by (simp add: fres_galois)
lemma h_Sup: "∀x ∈ X. x ⋅ w ≤ z ⟹ ⨆X ⋅ w ≤ z"
by (simp add: Sup_least fres_galois)
end
sublocale unital_pre_quantale ⊆ psrpqo: pre_dioid_one "(⊔)" "(⋅)" "1" "(≤)" "(<)"..
class weak_quantale = weak_proto_quantale + semigroup_mult
begin
subclass pre_quantale ..
text ‹The following counterexample shows an important consequence of weakness:
the absence of right annihilation.›
lemma "x ⋅ ⊥ = ⊥"
oops
end
class unital_weak_quantale = weak_quantale + monoid_mult
lemma (in unital_weak_quantale) "x ⋅ ⊥ = ⊥"
oops
subclass (in unital_weak_quantale) unital_pre_quantale ..