Theory Quantale_Left_Sided
section ‹Left-Sided Elements in Quantales›
theory Quantale_Left_Sided
imports Quantic_Nuclei_Conuclei
begin
context quantale
begin
subsection ‹Basic Definitions›
text ‹Left-sided elements are well investigated in quantale theory. They could be defined in weaker settings, for instance,
ord with a top element.›
definition "lsd x = (⊤ ⋅ x ≤ x)"
definition "rsd x = (x ⋅ ⊤ ≤ x)"
definition "twosd x = (lsd x ∧ rsd x)"
definition "slsd x = (⊤ ⋅ x = x)"
definition "srsd x = (x ⋅ ⊤ = x)"
definition "stwsd x = (slsd x ∧ srsd x)"
lemma lsided_bres: "(lsd x) = (x ≤ ⊤ → x)"
by (simp add: bres_galois lsd_def)
lemma lsided_fres: "(lsd x) = (⊤ ≤ x ← x)"
by (simp add: fres_galois lsd_def)
lemma lsided_fres_eq: "(lsd x) = (x ← x = ⊤)"
using fres_galois top_le lsd_def by force
lemma lsided_slsided: "lsd x ⟹ x ⋅ x = x ⟹ slsd x"
using fres_sol lsided_fres_eq slsd_def by force
lemma lsided_prop: "lsd x ⟹ y ⋅ x ≤ x"
by (simp add: fres_galois lsided_fres_eq)
lemma rsided_fres: "(rsd x) = (x ≤ x ← ⊤)"
by (simp add: fres_galois rsd_def)
lemma rsided_bres: "(rsd x) = (⊤ ≤ x → x)"
by (simp add: bres_galois rsd_def)
lemma rsided_bres_eq: "(rsd x) = (x → x = ⊤)"
using top_le rsided_bres by blast
lemma rsided_srsided: "rsd x ⟹ x ⋅ x = x ⟹ srsd x"
using bres_sol rsided_bres_eq srsd_def by auto
lemma rsided_prop: "rsd x ⟹ x ⋅ y ≤ x"
by (simp add: bres_galois rsided_bres_eq)
lemma lsided_top: "lsd ⊤"
by (simp add: lsd_def)
lemma lsided_bot: "lsd ⊥"
by (simp add: lsd_def)
lemma rsided_top: "rsd ⊤"
by (simp add: rsd_def)
lemma rsided_bot: "rsd ⊥"
by (simp add: rsd_def)
end
text ‹Right-sided elements are henceforth not considered. Their properties arise by opposition
duality, which is not formalised.›
text ‹The following functions have left-sided elements as fixpoints.›
definition lsl:: "'a::quantale ⇒ 'a" ("ν") where
"ν x = ⊤ ⋅ x"
definition lsu :: "'a::quantale ⇒ 'a" ("ν⇧♮") where
"ν⇧♮ x = ⊤ → x"
text ‹These functions are adjoints.›
lemma ls_galois: "ν ⊣ ν⇧♮"
by (simp add: adj_def bres_galois lsl_def lsu_def)
text ‹Due to this, the following properties hold.›
lemma lsl_iso: "mono ν"
using adj_iso1 ls_galois by blast
lemma lsl_iso_var: "x ≤ y ⟹ ν x ≤ ν y"
by (simp add: lsl_iso monoD)
lemma lsu_iso: "mono ν⇧♮"
using adj_iso2 ls_galois by blast
lemma lsu_iso_var: "x ≤ y ⟹ ν⇧♮ x ≤ ν⇧♮ y"
by (simp add: lsu_iso monoD)
lemma lsl_bot [simp]: "ν ⊥ = ⊥"
by (simp add: lsl_def)
lemma lsu_top [simp]: "ν⇧♮ ⊤ = ⊤"
by (simp add: lsu_def bres_galois_imp top_le)
lemma lsu_Inf_pres: "Inf_pres ν⇧♮"
unfolding fun_eq_iff by (metis ls_galois radj_Inf_pres)
lemma lsl_Sup_pres: "Sup_pres (ν::'a::quantale ⇒ 'a)"
by (simp add: fun_eq_iff, metis SUP_cong Sup_distl lsl_def)
lemma lsu_Inf_closed: "Inf_closed_set (range ν⇧♮)"
by (simp add: Inf_pres_Inf_closed lsu_Inf_pres)
lemma lsl_Sup_closed: "Sup_closed_set (range (ν::'a::quantale ⇒ 'a))"
by (simp add: Sup_pres_Sup_closed lsl_Sup_pres)
lemma lsl_lsu_canc1: "ν ∘ ν⇧♮ ≤ id"
by (simp add: adj_cancel1 ls_galois)
lemma lsl_lsu_canc2: "id ≤ ν⇧♮ ∘ ν"
by (simp add: adj_cancel2 ls_galois)
lemma clop_lsu_lsl: "clop (ν⇧♮ ∘ ν)"
by (simp add: clop_adj ls_galois)
lemma coclop_lsl_lsu: "coclop (ν ∘ ν⇧♮)"
by (simp add: coclop_adj ls_galois)
lemma dang1: "ν (ν x ⊓ y) ≤ ν x"
unfolding lsl_def by (metis bres_galois bres_interchange bres_top_top inf.coboundedI1)
lemma lsl_trans: "ν ∘ ν ≤ ν"
unfolding lsl_def fun_eq_iff comp_def
by (metis (no_types, lifting) bres_galois bres_interchange bres_top_top le_funI)
lemma lsl_lsu_prop: "ν ∘ ν⇧♮ ≤ ν⇧♮"
unfolding le_fun_def comp_def
by (metis adj_def dang1 dual_order.trans le_iff_inf ls_galois order_refl top_greatest)
lemma lsu_lsl_prop: "ν ≤ ν⇧♮ ∘ ν"
unfolding le_fun_def comp_def by (metis adj_def comp_def le_fun_def ls_galois lsl_trans)
context unital_quantale
begin
text ‹Left-sidedness and strict left-sidedness now coincide.›
lemma lsided_eq: "lsd = slsd"
unfolding fun_eq_iff by (simp add: order.eq_iff le_top lsd_def slsd_def)
lemma lsided_eq_var1: "(x ≤ ⊤ → x) = (x = ⊤ → x)"
using bres_galois dual_order.trans order.eq_iff le_top by blast
lemma lsided_eq_var2: "lsd x = (x = ⊤ → x)"
using bres_galois lsided_eq lsided_eq_var1 lsd_def by simp
end
lemma lsided_def3: "(ν (x::'a::unital_quantale) = x) = (ν⇧♮ x = x)"
unfolding lsl_def lsu_def by (metis lsided_eq lsided_eq_var2 slsd_def)
lemma Fix_lsl_lsu: "Fix (ν::'a::unital_quantale ⇒ 'a) = Fix ν⇧♮"
unfolding Fix_def by (simp add: lsided_def3)
lemma Fix_lsl_left_slsided: "Fix ν = {(x::'a::unital_quantale). lsd x}"
unfolding Fix_def lsl_def lsd_def using order.eq_iff le_top by blast
lemma Fix_lsl_iff [simp]: "(x ∈ Fix ν) = (ν x = x)"
by (simp add: Fix_def)
lemma Fix_lsu_iff [simp]: "(x ∈ Fix ν⇧♮) = (ν⇧♮ x = x)"
by (simp add: Fix_def)
lemma lsl_lsu_prop_eq [simp]: "(ν::'a::unital_quantale ⇒ 'a) ∘ ν⇧♮ = ν⇧♮"
by (smt antisym clop_extensive_var clop_lsu_lsl comp_apply le_fun_def lsided_eq_var1 lsl_lsu_prop lsu_def lsu_lsl_prop)
lemma lsu_lsl_prop_eq [simp]: "ν⇧♮ ∘ ν = (ν::'a::unital_quantale ⇒ 'a)"
by (metis adj_cancel_eq1 ls_galois lsl_lsu_prop_eq)
subsection ‹Connection with Closure and Coclosure Operators, Nuclei and Conuclei›
text ‹lsl is therefore a closure operator, lsu a cocolosure operator.›
lemma lsl_clop: "clop (ν::'a::unital_quantale ⇒ 'a)"
by (metis clop_lsu_lsl lsu_lsl_prop_eq)
lemma lsu_coclop: "coclop (ν⇧♮::'a::unital_quantale ⇒ 'a)"
by (metis coclop_lsl_lsu lsl_lsu_prop_eq)
lemma lsl_range_fix: "range (ν::'a::unital_quantale ⇒ 'a) = Fix ν"
by (simp add: clop_closure_set lsl_clop)
lemma lsu_range_fix: "range (ν⇧♮::'a::unital_quantale ⇒ 'a) = Fix ν⇧♮"
by (simp add: coclop_coclosure_set lsu_coclop)
lemma range_lsl_iff [simp]: "((x::'a::unital_quantale) ∈ range ν) = (ν x = x)"
by (simp add: lsl_range_fix)
lemma range_lsu_iff [simp]: "((x::'a::unital_quantale) ∈ range ν⇧♮) = (ν⇧♮ x = x)"
by (simp add: lsu_range_fix)
text ‹lsl and lsu are therefore both Sup and Inf closed.›
lemma lsu_Sup_closed: "Sup_closed_set (Fix (ν⇧♮::'a::unital_quantale ⇒ 'a))"
by (metis Fix_lsl_lsu lsl_Sup_closed lsl_range_fix)
lemma lsl_Inf_closed: "Inf_closed_set (Fix (ν::'a::unital_quantale ⇒ 'a))"
by (metis Fix_lsl_lsu lsu_Inf_closed lsu_range_fix)
text ‹lsl is even a quantic conucleus.›
lemma lsu_lax: "ν⇧♮ (x::'a::unital_quantale) ⋅ ν⇧♮ y ≤ ν⇧♮ (x ⋅ y)"
unfolding lsu_def by (meson bres_canc1 bres_galois bres_interchange le_top order_trans)
lemma lsu_one: "ν⇧♮ 1 ≤ (1::'a::unital_quantale)"
unfolding lsu_def using bres_canc1 dual_order.trans le_top by blast
lemma lsl_one: "1 ≤ ν (1::'a::unital_quantale)"
unfolding lsl_def by simp
lemma lsu_conuc: "conucleus (ν⇧♮::'a::unital_quantale ⇒ 'a)"
by (simp add: lsu_coclop conucleus_def lsu_lax)
text ‹It is therefore closed under composition.›
lemma lsu_comp_closed_var [simp]: "ν⇧♮ (ν⇧♮ x ⋅ ν⇧♮ y) = ν⇧♮ x ⋅ ν⇧♮ (y::'a::unital_quantale)"
by (simp add: conuc_comp_closed lsu_conuc)
lemma lsu_comp_closed: "comp_closed_set (Fix (ν⇧♮::'a::unital_quantale ⇒ 'a))"
by (simp add: conuc_Sup_qclosed lsu_conuc)
text ‹lsl is not a quantic nucleus unless composition is commutative.›
lemma "ν x ⋅ ν y ≤ ν (x ⋅ (y::'a::unital_quantale))"
oops
text ‹Yet it is closed under composition (because the set of fixpoints are the same).›
lemma lsl_comp_closed: "comp_closed_set (Fix (ν::'a::unital_quantale ⇒ 'a))"
by (simp add: Fix_lsl_lsu lsu_comp_closed)
lemma lsl_comp_closed_var [simp]: "ν (ν x ⋅ ν (y::'a::unital_quantale)) = ν x ⋅ ν y"
by (metis Fix_lsl_iff lsl_def lsl_range_fix mult.assoc rangeI)
text ‹The following simple properties go beyond nuclei and conuclei.›
lemma lsl_lsu_ran: "range ν⇧♮ = range (ν::'a::unital_quantale ⇒ 'a)"
by (simp add: Fix_lsl_lsu lsl_range_fix lsu_range_fix)
lemma lsl_top [simp]: "ν ⊤ = (⊤::'a::unital_quantale)"
by (simp add: clop_top lsl_clop)
lemma lsu_bot [simp]: "ν⇧♮ ⊥ = (⊥::'a::unital_quantale)"
using lsided_def3 lsl_bot by blast
lemma lsu_inj_on: "inj_on ν⇧♮ (Fix (ν⇧♮::'a::unital_quantale ⇒ 'a))"
by (metis coclop_coclosure inj_onI lsu_coclop lsu_range_fix)
lemma lsl_inj_on: "inj_on ν (Fix (ν::'a::unital_quantale ⇒ 'a))"
by (metis clop_closure inj_onI lsl_clop lsl_range_fix)
text ‹Additional preservation properties of lsl and lsu are useful in proofs.›
lemma lsl_Inf_closed_var [simp]: "ν (⨅x ∈ X. ν x) = (⨅x ∈ X. ν (x::'a::unital_quantale))"
by (metis (no_types, opaque_lifting) INF_image lsided_def3 lsu_Inf_pres lsu_lsl_prop_eq o_apply)
lemma lsl_Sup_closed_var [simp]: "ν (⨆x ∈ X. ν x) = (⨆x ∈ X. ν (x::'a::unital_quantale))"
unfolding lsl_def by (metis Sup_distl mult.assoc top_times_top)
lemma lsu_Inf_closed_var [simp]: "ν⇧♮ (⨅x ∈ X. ν⇧♮ x) = (⨅x ∈ X. ν⇧♮ (x::'a::unital_quantale))"
by (metis INF_image lsided_def3 lsl_Inf_closed_var lsl_lsu_prop_eq)
lemma lsu_Sup_closed_var [simp]: "ν⇧♮ (⨆x ∈ X. ν⇧♮ x) = (⨆x ∈ X. ν⇧♮ (x::'a::unital_quantale))"
by (metis SUP_image lsided_def3 lsl_Sup_closed_var lsl_lsu_prop_eq)
lemma lsl_inf_closed_var [simp]: "ν (ν x ⊓ ν y) = ν (x::'a::unital_quantale) ⊓ ν y"
by (smt antisym clop_extensive_var dang1 inf_sup_aci(1) le_inf_iff lsl_clop)
lemma lsl_sup_closed_var [simp]: "ν (ν x ⊔ ν y) = ν (x::'a::unital_quantale) ⊔ ν y"
by (meson Sup_sup_closed lsl_Sup_closed range_eqI range_lsl_iff sup_closed_set_def)
lemma lsu_inf_closed_var [simp]: "ν⇧♮ (ν⇧♮ x ⊓ ν⇧♮ y) = ν⇧♮ (x::'a::unital_quantale) ⊓ ν⇧♮ y"
by (metis (no_types, lifting) lsided_def3 lsl_inf_closed_var lsl_lsu_prop_eq o_apply)
lemma lsu_sup_closed_var [simp]: "ν⇧♮ (ν⇧♮ x ⊔ ν⇧♮ y) = ν⇧♮ (x::'a::unital_quantale) ⊔ ν⇧♮ y"
by (metis (no_types, lifting) lsided_def3 lsl_lsu_prop_eq lsl_sup_closed_var o_def)
lemma lsu_fres_closed [simp]: "ν⇧♮ (ν⇧♮ x ← ν⇧♮ y) = ν⇧♮ x ← ν⇧♮ (y::'a::unital_quantale)"
unfolding lsu_def by (simp add: bres_curry fres_bres)
lemma lsl_fres_closed [simp]: "ν (ν x ← ν y) = ν x ← ν (y::'a::unital_quantale)"
unfolding lsl_def by (metis fres_interchange lsd_def lsided_eq mult.assoc slsd_def top_times_top)
lemma lsl_almost_lax: "x ⋅ ν y ≤ ν (y::'a::unital_quantale)"
by (metis inf_top.right_neutral lsided_eq lsided_prop lsl_def lsl_inf_closed_var mult.right_neutral slsd_def)
text ‹Finally, here are two counterexamples.›
lemma "ν⇧♮ (ν⇧♮ x → ν⇧♮ y) = ν⇧♮ x → ν⇧♮ (y::'a::unital_quantale)"
oops
lemma "ν (ν x → ν y) = ν x → ν (y::'a::unital_quantale)"
oops
context ab_quantale
begin
lemma lsided_times_top: "lsd (⊤ ⋅ x)"
by (metis lsd_def mult_isor top_greatest mult_assoc)
lemma lsided_le2: "lsd x ⟹ x ⋅ y ≤ x ⊓ (y ⋅ ⊤)"
using lsided_prop psrpq.mult_isol mult_commute by auto
lemma lsided_le3: "lsd x ⟹ (x ⊓ y) ⋅ z ≤ x"
by (metis inf_le1 lsided_prop mult_isol order_trans mult_commute)
lemma lsided_le4: "lsd x ⟹ (x ⊓ y) ⋅ z ≤ x ⊓ (y ⋅ z)"
by (simp add: mult_isor lsided_le3)
lemma lsided_times_le_inf: "lsd x ⟹ lsd y ⟹ x ⋅ y ≤ x ⊓ y"
using lsided_prop lsided_le2 by force
end
text ‹Now lsl is a quantic nucleus.›
lemma lsl_lax: "ν x ⋅ ν y ≤ ν (x ⋅ (y::'aa::ab_unital_quantale))"
by (metis (no_types, opaque_lifting) lsl_almost_lax lsl_def mult.commute mult.left_commute)
lemma lsl_nuc: "nucleus (ν::'a::ab_unital_quantale ⇒ 'a)"
by (simp add: lsl_clop nucleus_def lsl_lax)
text ‹The following properties go beyond nuclei.›
lemma lsl_comp_pres: "ν (x ⋅ y) = ν x ⋅ ν (y::'a::ab_unital_quantale)"
by (metis (no_types, lifting) lsl_comp_closed_var lsl_nuc nuc_prop1 nuc_prop2)
lemma lsl_bres_closed [simp]: "ν (ν x → ν y) = ν x → ν (y::'a::ab_unital_quantale)"
by (simp add: lsl_nuc nuc_bres_closed)
lemma lsu_bres_pres [simp]: "ν⇧♮ (ν⇧♮ x → ν⇧♮ y) = ν⇧♮ x → ν⇧♮ (y::'a::ab_unital_quantale)"
by (simp add: bres_fres_eq)
lemma lsl_prelocalic_var: "ν x ⋅ y ≤ ν x ⊓ ν (y::'a::ab_unital_quantale)"
by (metis inf_top.right_neutral lsided_le4 lsided_times_top lsl_def)
lemma dang3: "(ν x ⊓ y) ⋅ z ≤ ν x ⊓ (y ⋅ (z::'a::ab_unital_quantale))"
by (metis lsided_le4 lsided_times_top lsl_def)
lemma lsl_prelocalic: "ν x ⋅ ν y ≤ ν x ⊓ ν (y::'a::ab_unital_quantale)"
by (metis lsided_times_le_inf lsided_times_top lsl_def)
lemma lsl_local: "x ⋅ ν y ≤ ν (x ⋅ (y::'a::ab_unital_quantale))"
by (simp add: lsl_def mult.left_commute)
lemma lsl_local_eq: "x ⋅ ν y = ν (x ⋅ (y::'a::ab_unital_quantale))"
by (simp add: lsl_def mult.left_commute)
text ‹Relative pseudocomplementation can be defined on the subquantale induced by lsu.›
definition "rpc x y = ν⇧♮ (-x ⊔ (y::'a::bool_unital_quantale))"
lemma lsl_rpc [simp]: "ν (rpc x y) = rpc x y"
by (metis lsl_lsu_prop_eq o_apply rpc_def)
lemma lsu_rpc [simp]: "ν⇧♮ (rpc x y) = rpc x y"
using lsided_def3 lsl_rpc by blast
lemma lsl_rpc_galois: "(x ⊓ ν z ≤ y) = (z ≤ rpc x (y::'a::bool_unital_quantale))"
unfolding rpc_def by (metis adj_def inf_commute ls_galois shunt1)
lemma lsl_rpc_galois_var: "x ⊓ ν z ≤ y ⟷ ν z ≤ rpc x y"
by (metis adj_def ls_galois lsl_rpc_galois lsu_rpc)
lemma rpc_expl_aux: "⨆{z. x ⊓ ν z ≤ y} = ⨆{z. x ⊓ z ≤ y ∧ ν z = (z::'a::bool_unital_quantale)}"
proof (rule antisym)
show "⨆{z. x ⊓ ν z ≤ y} ≤ ⨆{z. x ⊓ z ≤ y ∧ ν z = z}"
apply (rule Sup_mono, safe)
by (smt lsided_eq lsided_prop lsl_def lsl_lsu_prop_eq lsl_rpc_galois mem_Collect_eq o_apply rpc_def slsd_def)
show " ⨆{z. x ⊓ z ≤ y ∧ ν z = z} ≤ ⨆{z. x ⊓ ν z ≤ y}"
by (simp add: Collect_mono_iff Sup_subset_mono)
qed
lemma rpc_expl: "rpc x y = ⨆{z. x ⊓ z ≤ y ∧ ν z = (z::'a::bool_unital_quantale)}"
proof-
have "rpc x y = ⨆{z. z ≤ rpc x y}"
using Sup_atMost atMost_def by metis
also have "... = ⨆{z. x ⊓ ν z ≤ y}"
using lsl_rpc_galois by metis
finally show ?thesis
by (simp add: rpc_expl_aux)
qed
subsection ‹Non-Preservation and Lack of Closure›
context bool_ab_unital_quantale
begin
text ‹A few counterexamples deal in particular with lack of closure with respect to boolean complementation.›
lemma "ν⇧♮ (x ⋅ y) = ν⇧♮ x ⋅ ν⇧♮ y"
oops
lemma "ν 1 = 1"
oops
lemma "ν⇧♮ x = ν x"
oops
lemma "ν⇧♮ (⨆ P) = ⨆{ν⇧♮ p |p. p ∈ P}"
oops
lemma "rpc (ν⇧♮ x) (ν⇧♮ y) = -(ν⇧♮ x) ⊔ (ν⇧♮ y)"
oops
lemma "rpc (ν x) (ν y) = -(ν x) ⊔ (ν y)"
oops
lemma "ν (-(ν⇧♮ x) ⊔ (ν⇧♮ y)) = -(ν⇧♮ x) ⊔ (ν⇧♮ y)"
oops
lemma "ν (-(ν x) ⊔ (ν y)) = -(ν x) ⊔ (ν y)"
oops
lemma "ν x ⋅ ν y = ν x ⊓ ν y"
oops
lemma "ν (- (ν x)) = - (ν x)"
oops
lemma "ν⇧♮ (- (ν⇧♮ x)) = - (ν⇧♮ x)"
oops
lemma "ν (- (ν x) ⊔ (ν y)) = - (ν x) ⊔ (ν y)"
oops
lemma "ν⇧♮ (- (ν⇧♮ x) ⊔ (ν⇧♮ y)) = - (ν⇧♮ x) ⊔ (ν⇧♮ y)"
oops
end
subsection ‹Properties of Quotient Algebras and Subalgebras›
text ‹Finally I replay Rosenthal's quotient and subalgebra proofs for nuclei and conuclei in the concrete setting of left-sided elements. Ideally
it should be sufficient to show that lsl is a (quantale with) nucleus and then pick up the quotient algebra proof from the nucleus section. But there is no
way of achieving this, apart from creating a type class for quantales with the lsl operation. This seems bizarre, since lsl is just a definition.
On the other hand, an approach in which interpretations are used instead of instantiations might do the job.›
text ‹The first proof shows that lsu, as a conucleus, yields a subalgebra.›
typedef (overloaded) 'a lsu_set = "Fix (ν⇧♮::'a::unital_quantale ⇒ 'a)"
using Fix_lsu_iff lsu_bot by blast
setup_lifting type_definition_lsu_set
instantiation lsu_set :: (unital_quantale) quantale
begin
lift_definition times_lsu_set :: "'a lsu_set ⇒ 'a lsu_set ⇒ 'a lsu_set" is times
using comp_closed_set_def lsu_comp_closed by blast
lift_definition Inf_lsu_set :: "'a lsu_set set ⇒ 'a lsu_set" is Inf
by (metis Fix_lsl_lsu Inf_closed_set_def lsl_Inf_closed subset_eq)
lift_definition Sup_lsu_set :: "'a lsu_set set ⇒ 'a lsu_set" is Sup
using Sup_closed_set_def lsu_Sup_closed subsetI by blast
lift_definition bot_lsu_set :: "'a lsu_set" is "⊥"
by simp
lift_definition sup_lsu_set :: "'a lsu_set ⇒ 'a lsu_set ⇒ 'a lsu_set" is sup
by (metis Fix_lsu_iff lsu_sup_closed_var)
lift_definition top_lsu_set :: "'a lsu_set" is "⊤"
by simp
lift_definition inf_lsu_set :: "'a lsu_set ⇒ 'a lsu_set ⇒ 'a lsu_set" is inf
by (metis Fix_lsu_iff lsu_inf_closed_var)
lift_definition less_eq_lsu_set :: "'a lsu_set ⇒ 'a lsu_set ⇒ bool" is less_eq .
lift_definition less_lsu_set :: "'a lsu_set ⇒ 'a lsu_set ⇒ bool" is less .
instance
by (intro_classes; transfer, simp_all add: mult.assoc Inf_lower Inf_greatest Sup_upper Sup_least less_le_not_le Sup_distr Sup_distl)
end
text ‹This proof checks simply closure conditions, as one would expect for establishing a subalgebra.›
instance lsu_set :: (bool_ab_unital_quantale) distrib_ab_quantale
apply (intro_classes; transfer)
apply (simp add: mult.commute)
using sup_inf_distrib1 by blast
typedef (overloaded) 'a lsl_set = "range (ν::'a:: unital_quantale ⇒ 'a)"
by blast
setup_lifting type_definition_lsl_set
text ‹The final statement shows that lsu, as a nucleus, yields a quotient algebra.›
instantiation lsl_set :: (ab_unital_quantale) ab_unital_quantale
begin
lift_definition one_lsl_set :: "'a::ab_unital_quantale lsl_set" is "ν 1"
by blast
lift_definition Inf_lsl_set :: "'a lsl_set set ⇒ 'a lsl_set" is "λX. ν (⨅X)"
by blast
lift_definition Sup_lsl_set :: "'a lsl_set set ⇒ 'a lsl_set" is "λX. ν (⨆X)"
by blast
lift_definition bot_lsl_set :: "'a lsl_set" is "ν ⊥"
by blast
lift_definition sup_lsl_set :: "'a lsl_set ⇒ 'a lsl_set ⇒ 'a lsl_set" is "λx y. ν x ⊔ ν y"
by auto (metis lsl_sup_closed_var)
lift_definition top_lsl_set :: "'a lsl_set" is "ν ⊤"
by blast
lift_definition inf_lsl_set :: "'a lsl_set ⇒ 'a lsl_set ⇒ 'a lsl_set" is "λx y. ν x ⊓ ν y"
by (meson lsl_inf_closed_var range_lsl_iff)
lift_definition less_eq_lsl_set :: "'a lsl_set ⇒ 'a lsl_set ⇒ bool" is "λx y . ν x ≤ ν y" .
lift_definition less_lsl_set :: "'a lsl_set ⇒ 'a lsl_set ⇒ bool" is "λx y. ν x ≤ ν y ∧ x ≠ y" .
lift_definition times_lsl_set :: "'a lsl_set ⇒ 'a lsl_set ⇒ 'a lsl_set" is "λ x y. ν (x ⋅ y)"
by blast
instance
apply (standard; transfer)
apply (simp add: lsl_local_eq mult.commute mult.left_commute)
apply (simp add: mult.commute)
apply auto[1]
apply fastforce+
apply auto[1]
apply fastforce+
apply (metis Inf_lower lsl_iso_var range_lsl_iff)
apply (metis Inf_greatest lsl_iso_var range_lsl_iff)
apply (metis Sup_upper lsl_iso_var range_lsl_iff)
apply (metis Sup_least lsl_iso_var range_lsl_iff)
apply fastforce+
apply (smt Sup_distl image_cong lsl_local_eq mult.commute)
apply (smt Sup_distl image_cong lsl_local_eq mult.commute)
apply (simp add: lsl_def cong del: image_cong_simp)
apply (simp add: lsl_local_eq)
done
end
text ‹This proof checks preservation properties instead of closure ones.›
end