Theory Order_Lattice_Props
section ‹Properties of Orderings and Lattices›
theory Order_Lattice_Props
imports Order_Duality
begin
subsection ‹Basic Definitions for Orderings and Lattices›
text ‹The first definition is for order morphisms --- isotone (order-preserving, monotone) functions.
An order isomorphism is an order-preserving bijection. This should be defined in the class ord, but mono requires order.›
definition ord_homset :: "('a::order ⇒ 'b::order) set" where
"ord_homset = {f::'a::order ⇒ 'b::order. mono f}"
definition ord_embed :: "('a::order ⇒ 'b::order) ⇒ bool" where
"ord_embed f = (∀x y. f x ≤ f y ⟷ x ≤ y)"
definition ord_iso :: "('a::order ⇒ 'b::order) ⇒ bool" where
"ord_iso = bij ⊓ mono ⊓ (mono ∘ the_inv)"
lemma ord_embed_alt: "ord_embed f = (mono f ∧ (∀x y. f x ≤ f y ⟶ x ≤ y))"
using mono_def ord_embed_def by auto
lemma ord_embed_homset: "ord_embed f ⟹ f ∈ ord_homset"
by (simp add: mono_def ord_embed_def ord_homset_def)
lemma ord_embed_inj: "ord_embed f ⟹ inj f"
unfolding ord_embed_def inj_def by (simp add: eq_iff)
lemma ord_iso_ord_embed: "ord_iso f ⟹ ord_embed f"
unfolding ord_iso_def ord_embed_def bij_def inj_def mono_def
by (clarsimp, metis inj_def the_inv_f_f)
lemma ord_iso_alt: "ord_iso f = (ord_embed f ∧ surj f)"
unfolding ord_iso_def ord_embed_def surj_def bij_def inj_def mono_def
apply safe
by simp_all (metis eq_iff inj_def the_inv_f_f)+
lemma ord_iso_the_inv: "ord_iso f ⟹ mono (the_inv f)"
by (simp add: ord_iso_def)
lemma ord_iso_inv1: "ord_iso f ⟹ (the_inv f) ∘ f = id"
using ord_embed_inj ord_iso_ord_embed the_inv_into_f_f by fastforce
lemma ord_iso_inv2: "ord_iso f ⟹ f ∘ (the_inv f) = id"
using f_the_inv_into_f ord_embed_inj ord_iso_alt by fastforce
typedef (overloaded) ('a,'b) ord_homset = "ord_homset::('a::order ⇒ 'b::order) set"
by (force simp: ord_homset_def mono_def)
setup_lifting type_definition_ord_homset
text ‹The next definition is for the set of fixpoints of a given function. It is important in the context of orders,
for instance for proving Tarski's fixpoint theorem, but does not really belong here.›
definition Fix :: "('a ⇒ 'a) ⇒ 'a set" where
"Fix f = {x. f x = x}"
lemma retraction_prop: "f ∘ f = f ⟹ f x = x ⟷ x ∈ range f"
by (metis comp_apply f_inv_into_f rangeI)
lemma retraction_prop_fix: "f ∘ f = f ⟹ range f = Fix f"
unfolding Fix_def using retraction_prop by fastforce
lemma Fix_map_dual: "Fix ∘ ∂⇩F = (`) ∂ ∘ Fix"
unfolding Fix_def map_dual_def comp_def fun_eq_iff
by (smt (verit) Collect_cong invol_dual pointfree_idE setcompr_eq_image)
lemma Fix_map_dual_var: "Fix (∂⇩F f) = ∂ ` (Fix f)"
by (metis Fix_map_dual o_def)
lemma gfp_dual: "(∂::'a::complete_lattice_with_dual ⇒ 'a) ∘ gfp = lfp ∘ ∂⇩F"
proof-
{fix f:: "'a ⇒ 'a"
have "∂ (gfp f) = ∂ (⨆{u. u ≤ f u})"
by (simp add: gfp_def)
also have "... = ⨅(∂ ` {u. u ≤ f u})"
by (simp add: Sup_dual_def_var)
also have "... = ⨅{∂ u |u. u ≤ f u}"
by (simp add: setcompr_eq_image)
also have "... = ⨅{u |u. (∂⇩F f) u ≤ u}"
by (metis (no_types, opaque_lifting) dual_dual_ord dual_iff map_dual_def o_def)
finally have "∂ (gfp f) = lfp (∂⇩F f)"
by (metis lfp_def)}
thus ?thesis
by auto
qed
lemma gfp_dual_var:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
shows "∂ (gfp f) = lfp (∂⇩F f)"
using comp_eq_elim gfp_dual by blast
lemma gfp_to_lfp: "gfp = (∂::'a::complete_lattice_with_dual ⇒ 'a) ∘ lfp ∘ ∂⇩F"
by (simp add: comp_assoc fun_dual2 gfp_dual)
lemma gfp_to_lfp_var:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
shows "gfp f = ∂ (lfp (∂⇩F f))"
by (metis gfp_dual_var invol_dual_var)
lemma lfp_dual: "(∂::'a::complete_lattice_with_dual ⇒ 'a) ∘ lfp = gfp ∘ ∂⇩F"
by (simp add: comp_assoc gfp_to_lfp map_dual_invol)
lemma lfp_dual_var:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
shows "∂ (lfp f) = gfp (map_dual f)"
using comp_eq_dest_lhs lfp_dual by fastforce
lemma lfp_to_gfp: "lfp = (∂::'a::complete_lattice_with_dual ⇒ 'a) ∘ gfp ∘ ∂⇩F"
by (simp add: comp_assoc gfp_dual map_dual_invol)
lemma lfp_to_gfp_var:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'a"
shows "lfp f = ∂ (gfp (∂⇩F f))"
by (metis invol_dual_var lfp_dual_var)
lemma lfp_in_Fix:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ lfp f ∈ Fix f"
by (metis (mono_tags, lifting) Fix_def lfp_unfold mem_Collect_eq)
lemma gfp_in_Fix:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ gfp f ∈ Fix f"
by (metis (mono_tags, lifting) Fix_def gfp_unfold mem_Collect_eq)
lemma nonempty_Fix:
fixes f :: "'a::complete_lattice ⇒ 'a"
shows "mono f ⟹ Fix f ≠ {}"
using lfp_in_Fix by fastforce
text ‹Next the minimal and maximal elements of an ordering are defined.›
context ord
begin
definition min_set :: "'a set ⇒ 'a set" where
"min_set X = {y ∈ X. ∀x ∈ X. x ≤ y ⟶ x = y}"
definition max_set :: "'a set ⇒ 'a set" where
"max_set X = {x ∈ X. ∀y ∈ X. x ≤ y ⟶ x = y}"
end
context ord_with_dual
begin
lemma min_max_set_dual: "(`) ∂ ∘ min_set = max_set ∘ (`) ∂"
unfolding max_set_def min_set_def fun_eq_iff comp_def
apply safe
using dual_dual_ord inj_dual_iff by auto
lemma min_max_set_dual_var: "∂ ` (min_set X) = max_set (∂ ` X)"
using comp_eq_dest min_max_set_dual by fastforce
lemma max_min_set_dual: "(`) ∂ ∘ max_set = min_set ∘ (`) ∂"
by (metis (no_types, opaque_lifting) comp_id fun.map_comp id_comp image_dual min_max_set_dual)
lemma min_to_max_set: "min_set = (`) ∂ ∘ max_set ∘ (`) ∂"
by (metis comp_id image_dual max_min_set_dual o_assoc)
lemma max_min_set_dual_var: "∂ ` (max_set X) = min_set (∂ ` X)"
using comp_eq_dest max_min_set_dual by fastforce
lemma min_to_max_set_var: "min_set X = ∂ ` (max_set (∂ ` X))"
by (simp add: max_min_set_dual_var pointfree_idE)
end
text ‹Next, directed and filtered sets, upsets, downsets, filters and ideals in posets are defined.›
context ord
begin
definition directed :: "'a set ⇒ bool" where
"directed X = (∀Y. finite Y ∧ Y ⊆ X ⟶ (∃x ∈ X. ∀y ∈ Y. y ≤ x))"
definition filtered :: "'a set ⇒ bool" where
"filtered X = (∀Y. finite Y ∧ Y ⊆ X ⟶ (∃x ∈ X. ∀y ∈ Y. x ≤ y))"
definition downset_set :: "'a set ⇒ 'a set" (‹⇓›) where
"⇓X = {y. ∃x ∈ X. y ≤ x}"
definition upset_set :: "'a set ⇒ 'a set" (‹⇑›) where
"⇑X = {y. ∃x ∈ X. x ≤ y}"
definition downset :: "'a ⇒ 'a set" (‹↓›) where
"↓ = ⇓ ∘ η"
definition upset :: "'a ⇒ 'a set" (‹↑›) where
"↑ = ⇑ ∘ η"
definition downsets :: "'a set set" where
"downsets = Fix ⇓"
definition upsets :: "'a set set" where
"upsets = Fix ⇑"
definition "downclosed_set X = (X ∈ downsets)"
definition "upclosed_set X = (X ∈ upsets)"
definition ideals :: "'a set set" where
"ideals = {X. X ≠ {} ∧ downclosed_set X ∧ directed X}"
definition filters :: "'a set set" where
"filters = {X. X ≠ {} ∧ upclosed_set X ∧ filtered X}"
abbreviation "idealp X ≡ X ∈ ideals"
abbreviation "filterp X ≡ X ∈ filters"
end
text ‹These notions are pair-wise dual.›
text ‹Filtered and directed sets are dual.›
context ord_with_dual
begin
lemma filtered_directed_dual: "filtered ∘ (`) ∂ = directed"
unfolding filtered_def directed_def fun_eq_iff comp_def
apply clarsimp
apply safe
apply (meson finite_imageI imageI image_mono dual_dual_ord)
by (smt (verit, ccfv_threshold) finite_subset_image imageE ord_dual)
lemma directed_filtered_dual: "directed ∘ (`) ∂ = filtered"
using filtered_directed_dual by (metis comp_id image_dual o_assoc)
lemma filtered_to_directed: "filtered X = directed (∂ ` X)"
by (metis comp_apply directed_filtered_dual)
text ‹Upsets and downsets are dual.›
lemma downset_set_upset_set_dual: "(`) ∂ ∘ ⇓ = ⇑ ∘ (`) ∂"
unfolding downset_set_def upset_set_def fun_eq_iff comp_def
apply safe
apply (meson image_eqI ord_dual)
by (clarsimp, metis (mono_tags, lifting) dual_iff image_iff mem_Collect_eq ord_dual)
lemma upset_set_downset_set_dual: "(`) ∂ ∘ ⇑ = ⇓ ∘ (`) ∂"
using downset_set_upset_set_dual by (metis (no_types, opaque_lifting) comp_id id_comp image_dual o_assoc)
lemma upset_set_to_downset_set: "⇑ = (`) ∂ ∘ ⇓ ∘ (`) ∂"
by (simp add: comp_assoc downset_set_upset_set_dual)
lemma upset_set_to_downset_set2: "⇑ X = ∂ ` (⇓ (∂ ` X))"
by (simp add: upset_set_to_downset_set)
lemma downset_upset_dual: "(`) ∂ ∘ ↓ = ↑ ∘ ∂"
using downset_def upset_def upset_set_to_downset_set by fastforce
lemma upset_to_downset: "(`) ∂ ∘ ↑ = ↓ ∘ ∂"
by (metis comp_assoc id_apply ord.downset_def ord.upset_def power_set_func_nat_trans upset_set_downset_set_dual)
lemma upset_to_downset2: "↑ = (`) ∂ ∘ ↓ ∘ ∂"
by (simp add: comp_assoc downset_upset_dual)
lemma upset_to_downset3: "↑ x = ∂ ` (↓ (∂ x))"
by (simp add: upset_to_downset2)
lemma downsets_upsets_dual: "(X ∈ downsets) = (∂ ` X ∈ upsets)"
unfolding downsets_def upsets_def Fix_def
by (smt (verit) comp_eq_dest downset_set_upset_set_dual image_inv_f_f inj_dual mem_Collect_eq)
lemma downset_setp_upset_setp_dual: "upclosed_set ∘ (`) ∂ = downclosed_set"
unfolding downclosed_set_def upclosed_set_def using downsets_upsets_dual by fastforce
lemma upsets_to_downsets: "(X ∈ upsets) = (∂ ` X ∈ downsets)"
by (simp add: downsets_upsets_dual image_comp)
lemma upset_setp_downset_setp_dual: "downclosed_set ∘ (`) ∂ = upclosed_set"
by (metis comp_id downset_setp_upset_setp_dual image_dual o_assoc)
text ‹Filters and ideals are dual.›
lemma ideals_filters_dual: "(X ∈ ideals) = ((∂ ` X) ∈ filters)"
by (smt (verit) comp_eq_dest_lhs directed_filtered_dual image_inv_f_f image_is_empty inv_unique_comp filters_def ideals_def inj_dual invol_dual mem_Collect_eq upset_setp_downset_setp_dual)
lemma idealp_filterp_dual: "idealp = filterp ∘ (`) ∂"
unfolding fun_eq_iff by (simp add: ideals_filters_dual)
lemma filters_to_ideals: "(X ∈ filters) = ((∂ ` X) ∈ ideals)"
by (simp add: ideals_filters_dual image_comp)
lemma filterp_idealp_dual: "filterp = idealp ∘ (`) ∂"
unfolding fun_eq_iff by (simp add: filters_to_ideals)
end
subsection ‹Properties of Orderings›
context ord
begin
lemma directed_nonempty: "directed X ⟹ X ≠ {}"
unfolding directed_def by fastforce
lemma directed_ub: "directed X ⟹ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. x ≤ z ∧ y ≤ z)"
by (meson empty_subsetI directed_def finite.emptyI finite_insert insert_subset order_refl)
lemma downset_set_prop: "⇓ = Union ∘ (`) ↓"
unfolding downset_set_def downset_def fun_eq_iff by fastforce
lemma downset_set_prop_var: "⇓X = (⋃x ∈ X. ↓x)"
by (simp add: downset_set_prop)
lemma downset_prop: "↓x = {y. y ≤ x}"
unfolding downset_def downset_set_def fun_eq_iff by fastforce
lemma downset_prop2: "y ≤ x ⟹ y ∈ ↓x"
by (simp add: downset_prop)
lemma ideals_downsets: "X ∈ ideals ⟹ X ∈ downsets"
by (simp add: downclosed_set_def ideals_def)
lemma ideals_directed: "X ∈ ideals ⟹ directed X"
by (simp add: ideals_def)
end
context preorder
begin
lemma directed_prop: "X ≠ {} ⟹ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. x ≤ z ∧ y ≤ z) ⟹ directed X"
proof-
assume h1: "X ≠ {}"
and h2: "∀x ∈ X. ∀y ∈ X. ∃z ∈ X. x ≤ z ∧ y ≤ z"
{fix Y
have "finite Y ⟹ Y ⊆ X ⟹ (∃x ∈ X. ∀y ∈ Y. y ≤ x)"
proof (induct rule: finite_induct)
case empty
then show ?case
using h1 by blast
next
case (insert x F)
then show ?case
by (metis h2 insert_iff insert_subset order_trans)
qed}
thus ?thesis
by (simp add: directed_def)
qed
lemma directed_alt: "directed X = (X ≠ {} ∧ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. x ≤ z ∧ y ≤ z))"
by (metis directed_prop directed_nonempty directed_ub)
lemma downset_set_prop_var2: "x ∈ ⇓X ⟹ y ≤ x ⟹ y ∈ ⇓X"
unfolding downset_set_def using order_trans by blast
lemma downclosed_set_iff: "downclosed_set X = (∀x ∈ X. ∀y. y ≤ x ⟶ y ∈ X)"
unfolding downclosed_set_def downsets_def Fix_def downset_set_def by auto
lemma downclosed_downset_set: "downclosed_set (⇓X)"
by (simp add: downclosed_set_iff downset_set_prop_var2 downset_def)
lemma downclosed_downset: "downclosed_set (↓x)"
by (simp add: downclosed_downset_set downset_def)
lemma downset_set_ext: "id ≤ ⇓"
unfolding le_fun_def id_def downset_set_def by auto
lemma downset_set_iso: "mono ⇓"
unfolding mono_def downset_set_def by blast
lemma downset_set_idem [simp]: "⇓ ∘ ⇓ = ⇓"
unfolding fun_eq_iff downset_set_def using order_trans by auto
lemma downset_faithful: "↓x ⊆ ↓y ⟹ x ≤ y"
by (simp add: downset_prop subset_eq)
lemma downset_iso_iff: "(↓x ⊆ ↓y) = (x ≤ y)"
using atMost_iff downset_prop order_trans by blast
text ‹The following proof uses the Axiom of Choice.›
lemma downset_directed_downset_var [simp]: "directed (⇓X) = directed X"
proof
assume h1: "directed X"
{fix Y
assume h2: "finite Y" and h3: "Y ⊆ ⇓X"
hence "∀y. ∃x. y ∈ Y ⟶ x ∈ X ∧ y ≤ x"
by (force simp: downset_set_def)
hence "∃f. ∀y. y ∈ Y ⟶ f y ∈ X ∧ y ≤ f y"
by (rule choice)
hence "∃f. finite (f ` Y) ∧ f ` Y ⊆ X ∧ (∀y ∈ Y. y ≤ f y)"
by (metis finite_imageI h2 image_subsetI)
hence "∃Z. finite Z ∧ Z ⊆ X ∧ (∀y ∈ Y. ∃ z ∈ Z. y ≤ z)"
by fastforce
hence "∃Z. finite Z ∧ Z ⊆ X ∧ (∀y ∈ Y. ∃ z ∈ Z. y ≤ z) ∧ (∃x ∈ X. ∀ z ∈ Z. z ≤ x)"
by (metis directed_def h1)
hence "∃x ∈ X. ∀y ∈ Y. y ≤ x"
by (meson order_trans)}
thus "directed (⇓X)"
unfolding directed_def downset_set_def by fastforce
next
assume "directed (⇓X)"
thus "directed X"
unfolding directed_def downset_set_def
apply clarsimp
by (smt (verit) Ball_Collect order_refl order_trans subsetCE)
qed
lemma downset_directed_downset [simp]: "directed ∘ ⇓ = directed"
unfolding fun_eq_iff by simp
lemma directed_downset_ideals: "directed (⇓X) = (⇓X ∈ ideals)"
by (metis (mono_tags, lifting) CollectI Fix_def directed_alt downset_set_idem downclosed_set_def downsets_def ideals_def o_def ord.ideals_directed)
lemma downclosed_Fix: "downclosed_set X = (⇓X = X)"
by (metis (mono_tags, lifting) CollectD Fix_def downclosed_downset_set downclosed_set_def downsets_def)
end
lemma downset_iso: "mono (↓::'a::order ⇒ 'a set)"
by (simp add: downset_iso_iff mono_def)
lemma mono_downclosed:
fixes f :: "'a::order ⇒ 'b::order"
assumes "mono f"
shows "∀Y. downclosed_set Y ⟶ downclosed_set (f -` Y)"
by (simp add: assms downclosed_set_iff monoD)
lemma
fixes f :: "'a::order ⇒ 'b::order"
assumes "mono f"
shows "∀Y. downclosed_set X ⟶ downclosed_set (f ` X)"
oops
lemma downclosed_mono:
fixes f :: "'a::order ⇒ 'b::order"
assumes "∀Y. downclosed_set Y ⟶ downclosed_set (f -` Y)"
shows "mono f"
proof-
{fix x y :: "'a::order"
assume h: "x ≤ y"
have "downclosed_set (↓ (f y))"
unfolding downclosed_set_def downsets_def Fix_def downset_set_def downset_def by auto
hence "downclosed_set (f -` (↓ (f y)))"
by (simp add: assms)
hence "downclosed_set {z. f z ≤ f y}"
unfolding vimage_def downset_def downset_set_def by auto
hence "∀z w. (f z ≤ f y ∧ w ≤ z) ⟶ f w ≤ f y"
unfolding downclosed_set_def downclosed_set_def downsets_def Fix_def downset_set_def by force
hence "f x ≤ f y"
using h by blast}
thus ?thesis..
qed
lemma mono_downclosed_iff: "mono f = (∀Y. downclosed_set Y ⟶ downclosed_set (f -` Y))"
using mono_downclosed downclosed_mono by auto
context order
begin
lemma downset_inj: "inj ↓"
by (metis injI downset_iso_iff order.eq_iff)
lemma "(X ⊆ Y) = (⇓X ⊆ ⇓Y)"
oops
end
context lattice
begin
lemma lat_ideals: "X ∈ ideals = (X ≠ {} ∧ X ∈ downsets ∧ (∀x ∈ X. ∀ y ∈ X. x ⊔ y ∈ X))"
unfolding ideals_def directed_alt downsets_def Fix_def downset_set_def downclosed_set_def
using local.sup.bounded_iff local.sup_ge2 by blast
end
context bounded_lattice
begin
lemma bot_ideal: "X ∈ ideals ⟹ ⊥ ∈ X"
unfolding ideals_def downclosed_set_def downsets_def Fix_def downset_set_def by fastforce
end
context complete_lattice
begin
lemma Sup_downset_id [simp]: "Sup ∘ ↓ = id"
using Sup_atMost atMost_def downset_prop by fastforce
lemma downset_Sup_id: "id ≤ ↓ ∘ Sup"
by (simp add: Sup_upper downset_prop le_funI subsetI)
lemma Inf_Sup_var: "⨆(⋂x ∈ X. ↓x) = ⨅X"
unfolding downset_prop by (simp add: Collect_ball_eq Inf_eq_Sup)
lemma Inf_pres_downset_var: "(⋂x ∈ X. ↓x) = ↓(⨅X)"
unfolding downset_prop by (safe, simp_all add: le_Inf_iff)
end
subsection ‹Dual Properties of Orderings›
context ord_with_dual
begin
lemma filtered_nonempty: "filtered X ⟹ X ≠ {}"
using filtered_to_directed ord.directed_nonempty by auto
lemma filtered_lb: "filtered X ⟹ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. z ≤ x ∧ z ≤ y)"
using filtered_to_directed directed_ub dual_dual_ord by fastforce
lemma upset_set_prop_var: "⇑X = (⋃x ∈ X. ↑x)"
by (simp add: image_Union downset_set_prop_var upset_set_to_downset_set2 upset_to_downset2)
lemma upset_set_prop: "⇑ = Union ∘ (`) ↑"
unfolding fun_eq_iff by (simp add: upset_set_prop_var)
lemma upset_prop: "↑x = {y. x ≤ y}"
unfolding upset_to_downset3 downset_prop image_def using dual_dual_ord by fastforce
lemma upset_prop2: "x ≤ y ⟹ y ∈ ↑x"
by (simp add: upset_prop)
lemma filters_upsets: "X ∈ filters ⟹ X ∈ upsets"
by (simp add: upclosed_set_def filters_def)
lemma filters_filtered: "X ∈ filters ⟹ filtered X"
by (simp add: filters_def)
end
context preorder_with_dual
begin
lemma filtered_prop: "X ≠ {} ⟹ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. z ≤ x ∧ z ≤ y) ⟹ filtered X"
unfolding filtered_to_directed
by (rule directed_prop, blast, metis (full_types) image_iff ord_dual)
lemma filtered_alt: "filtered X = (X ≠ {} ∧ (∀x ∈ X. ∀y ∈ X. ∃z ∈ X. z ≤ x ∧ z ≤ y))"
by (metis image_empty directed_alt filtered_to_directed filtered_lb filtered_prop)
lemma up_set_prop_var2: "x ∈ ⇑X ⟹ x ≤ y ⟹ y ∈ ⇑X"
using downset_set_prop_var2 dual_iff ord_dual upset_set_to_downset_set2 by fastforce
lemma upclosed_set_iff: "upclosed_set X = (∀x ∈ X. ∀y. x ≤ y ⟶ y ∈ X)"
unfolding upclosed_set_def upsets_def Fix_def upset_set_def by auto
lemma upclosed_upset_set: "upclosed_set (⇑X)"
using up_set_prop_var2 upclosed_set_iff by blast
lemma upclosed_upset: "upclosed_set (↑x)"
by (simp add: upset_def upclosed_upset_set)
lemma upset_set_ext: "id ≤ ⇑"
by (smt (verit) comp_def comp_id image_mono le_fun_def downset_set_ext image_dual upset_set_to_downset_set2)
lemma upset_set_anti: "mono ⇑"
by (metis image_mono downset_set_iso upset_set_to_downset_set2 mono_def)
lemma up_set_idem [simp]: "⇑ ∘ ⇑ = ⇑"
by (metis comp_assoc downset_set_idem upset_set_downset_set_dual upset_set_to_downset_set)
lemma upset_faithful: "↑x ⊆ ↑y ⟹ y ≤ x"
by (metis inj_image_subset_iff downset_faithful dual_dual_ord inj_dual upset_to_downset3)
lemma upset_anti_iff: "(↑y ⊆ ↑x) = (x ≤ y)"
by (metis downset_iso_iff ord_dual upset_to_downset3 subset_image_iff upset_faithful)
lemma upset_filtered_upset [simp]: "filtered ∘ ⇑ = filtered"
by (metis comp_assoc directed_filtered_dual downset_directed_downset upset_set_downset_set_dual)
lemma filtered_upset_filters: "filtered (⇑X) = (⇑X ∈ filters)"
by (metis comp_apply directed_downset_ideals filtered_to_directed filterp_idealp_dual upset_set_downset_set_dual)
lemma upclosed_Fix: "upclosed_set X = (⇑X = X)"
by (simp add: Fix_def upclosed_set_def upsets_def)
end
lemma upset_anti: "antimono (↑::'a::order_with_dual ⇒ 'a set)"
by (simp add: antimono_def upset_anti_iff)
lemma mono_upclosed:
fixes f :: "'a::order_with_dual ⇒ 'b::order_with_dual"
assumes "mono f"
shows "∀Y. upclosed_set Y ⟶ upclosed_set (f -` Y)"
by (simp add: assms monoD upclosed_set_iff)
lemma mono_upclosed:
fixes f :: "'a::order_with_dual ⇒ 'b::order_with_dual"
assumes "mono f"
shows "∀Y. upclosed_set X ⟶ upclosed_set (f ` X)"
oops
lemma upclosed_mono:
fixes f :: "'a::order_with_dual ⇒ 'b::order_with_dual"
assumes "∀Y. upclosed_set Y ⟶ upclosed_set (f -` Y)"
shows "mono f"
by (metis (mono_tags, lifting) assms dual_order.refl mem_Collect_eq monoI order.trans upclosed_set_iff vimageE vimageI2)
lemma mono_upclosed_iff:
fixes f :: "'a::order_with_dual ⇒ 'b::order_with_dual"
shows "mono f = (∀Y. upclosed_set Y ⟶ upclosed_set (f -` Y))"
using mono_upclosed upclosed_mono by auto
context order_with_dual
begin
lemma upset_inj: "inj ↑"
by (metis inj_compose inj_on_imageI2 downset_inj inj_dual upset_to_downset)
lemma "(X ⊆ Y) = (⇑Y ⊆ ⇑X)"
oops
end
context lattice_with_dual
begin
lemma lat_filters: "X ∈ filters = (X ≠ {} ∧ X ∈ upsets ∧ (∀x ∈ X. ∀ y ∈ X. x ⊓ y ∈ X))"
unfolding filters_to_ideals upsets_to_downsets inf_to_sup lat_ideals
by (smt (verit) image_iff image_inv_f_f image_is_empty inj_image_mem_iff inv_unique_comp inj_dual invol_dual)
end
context bounded_lattice_with_dual
begin
lemma top_filter: "X ∈ filters ⟹ ⊤ ∈ X"
using bot_ideal inj_image_mem_iff inj_dual filters_to_ideals top_dual by fastforce
end
context complete_lattice_with_dual
begin
lemma Inf_upset_id [simp]: "Inf ∘ ↑ = id"
by (metis comp_assoc comp_id Sup_downset_id Sups_dual_def downset_upset_dual invol_dual)
lemma upset_Inf_id: "id ≤ ↑ ∘ Inf"
by (simp add: Inf_lower le_funI subsetI upset_prop)
lemma Sup_Inf_var: " ⨅(⋂x ∈ X. ↑x) = ⨆X"
unfolding upset_prop by (simp add: Collect_ball_eq Sup_eq_Inf)
lemma Sup_dual_upset_var: "(⋂x ∈ X. ↑x) = ↑(⨆X)"
unfolding upset_prop by (safe, simp_all add: Sup_le_iff)
end
subsection ‹Properties of Complete Lattices›
definition "Inf_closed_set X = (∀Y ⊆ X. ⨅Y ∈ X)"
definition "Sup_closed_set X = (∀Y ⊆ X. ⨆Y ∈ X)"
definition "inf_closed_set X = (∀x ∈ X. ∀y ∈ X. x ⊓ y ∈ X)"
definition "sup_closed_set X = (∀x ∈ X. ∀y ∈ X. x ⊔ y ∈ X)"
text ‹The following facts about complete lattices add to those in the Isabelle libraries.›
context complete_lattice
begin
text ‹The translation between sup and Sup could be improved. The sup-theorems should be direct
consequences of Sup-ones. In addition, duality between sup and inf is currently not exploited.›
lemma sup_Sup: "x ⊔ y = ⨆{x,y}"
by simp
lemma inf_Inf: "x ⊓ y = ⨅{x,y}"
by simp
text ‹The next two lemmas are about Sups and Infs of indexed families. These are interesting for
iterations and fixpoints.›
lemma fSup_unfold: "(f::nat ⇒ 'a) 0 ⊔ (⨆n. f (Suc n)) = (⨆n. f n)"
apply (intro order.antisym sup_least)
apply (rule Sup_upper, force)
apply (rule Sup_mono, force)
apply (safe intro!: Sup_least)
by (case_tac n, simp_all add: Sup_upper le_supI2)
lemma fInf_unfold: "(f::nat ⇒ 'a) 0 ⊓ (⨅n. f (Suc n)) = (⨅n. f n)"
apply (intro order.antisym inf_greatest)
apply (rule Inf_greatest, safe)
apply (case_tac n)
apply simp_all
using Inf_lower inf.coboundedI2 apply force
apply (simp add: Inf_lower)
by (auto intro: Inf_mono)
end
lemma Sup_sup_closed: "Sup_closed_set (X::'a::complete_lattice set) ⟹ sup_closed_set X"
by (metis Sup_closed_set_def empty_subsetI insert_subsetI sup_Sup sup_closed_set_def)
lemma Inf_inf_closed: "Inf_closed_set (X::'a::complete_lattice set) ⟹ inf_closed_set X"
by (metis Inf_closed_set_def empty_subsetI inf_Inf inf_closed_set_def insert_subset)
subsection ‹Sup- and Inf-Preservation›
text ‹Next, important notation for morphism between posets and lattices is introduced:
sup-preservation, inf-preservation and related properties.›
abbreviation Sup_pres :: "('a::Sup ⇒ 'b::Sup) ⇒ bool" where
"Sup_pres f ≡ f ∘ Sup = Sup ∘ (`) f"
abbreviation Inf_pres :: "('a::Inf ⇒ 'b::Inf) ⇒ bool" where
"Inf_pres f ≡ f ∘ Inf = Inf ∘ (`) f"
abbreviation sup_pres :: "('a::sup ⇒ 'b::sup) ⇒ bool" where
"sup_pres f ≡ (∀x y. f (x ⊔ y) = f x ⊔ f y)"
abbreviation inf_pres :: "('a::inf ⇒ 'b::inf) ⇒ bool" where
"inf_pres f ≡ (∀x y. f (x ⊓ y) = f x ⊓ f y)"
abbreviation bot_pres :: "('a::bot ⇒ 'b::bot) ⇒ bool" where
"bot_pres f ≡ f ⊥ = ⊥"
abbreviation top_pres :: "('a::top ⇒ 'b::top) ⇒ bool" where
"top_pres f ≡ f ⊤ = ⊤"
abbreviation Sup_dual :: "('a::Sup ⇒ 'b::Inf) ⇒ bool" where
"Sup_dual f ≡ f ∘ Sup = Inf ∘ (`) f"
abbreviation Inf_dual :: "('a::Inf ⇒ 'b::Sup) ⇒ bool" where
"Inf_dual f ≡ f ∘ Inf = Sup ∘ (`) f"
abbreviation sup_dual :: "('a::sup ⇒ 'b::inf) ⇒ bool" where
"sup_dual f ≡ (∀x y. f (x ⊔ y) = f x ⊓ f y)"
abbreviation inf_dual :: "('a::inf ⇒ 'b::sup) ⇒ bool" where
"inf_dual f ≡ (∀x y. f (x ⊓ y) = f x ⊔ f y)"
abbreviation bot_dual :: "('a::bot ⇒ 'b::top) ⇒ bool" where
"bot_dual f ≡ f ⊥ = ⊤"
abbreviation top_dual :: "('a::top ⇒ 'b::bot) ⇒ bool" where
"top_dual f ≡ f ⊤ = ⊥"
text ‹Inf-preservation and sup-preservation relate with duality.›
lemma Inf_pres_map_dual_var:
"Inf_pres f = Sup_pres (∂⇩F f)"
for f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
proof -
{ fix x :: "'a set"
assume "∂ (f (⨅ (∂ ` x))) = (⨆y∈x. ∂ (f (∂ y)))" for x
then have "⨅ (f ` ∂ ` A) = f (∂ (⨆ A))" for A
by (metis (no_types) Sup_dual_def_var image_image invol_dual_var subset_dual)
then have "⨅ (f ` x) = f (⨅ x)"
by (metis Sup_dual_def_var subset_dual) }
then show ?thesis
by (auto simp add: map_dual_def fun_eq_iff Inf_dual_var Sup_dual_def_var image_comp)
qed
lemma Inf_pres_map_dual: "Inf_pres = Sup_pres ∘ (∂⇩F::('a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual) ⇒ 'a ⇒ 'b)"
proof-
{fix f::"'a ⇒ 'b"
have "Inf_pres f = (Sup_pres ∘ ∂⇩F) f"
by (simp add: Inf_pres_map_dual_var)}
thus ?thesis
by force
qed
lemma Sup_pres_map_dual_var:
fixes f :: "'a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual"
shows "Sup_pres f = Inf_pres (∂⇩F f)"
by (metis Inf_pres_map_dual_var fun_dual5 map_dual_def)
lemma Sup_pres_map_dual: "Sup_pres = Inf_pres ∘ (∂⇩F::('a::complete_lattice_with_dual ⇒ 'b::complete_lattice_with_dual) ⇒ 'a ⇒ 'b)"
by (simp add: Inf_pres_map_dual comp_assoc map_dual_invol)
text ‹The following lemmas relate isotonicity of functions between complete lattices
with weak (left) preservation properties of sups and infs.›
lemma fun_isol: "mono f ⟹ mono ((∘) f)"
by (simp add: le_fun_def mono_def)
lemma fun_isor: "mono f ⟹ mono (λx. x ∘ f)"
by (simp add: le_fun_def mono_def)
lemma Sup_sup_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_pres f ⟹ sup_pres f"
by (metis (no_types, opaque_lifting) Sup_empty Sup_insert comp_apply image_insert sup_bot.right_neutral)
lemma Inf_inf_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows"Inf_pres f ⟹ inf_pres f"
by (smt (verit) INF_insert Inf_empty Inf_insert comp_eq_elim inf_top.right_neutral)
lemma Sup_bot_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_pres f ⟹ bot_pres f"
by (metis SUP_empty Sup_empty comp_eq_elim)
lemma Inf_top_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_pres f ⟹ top_pres f"
by (metis INF_empty Inf_empty comp_eq_elim)
lemma Sup_sup_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_dual f ⟹ sup_dual f"
by (smt (verit) comp_eq_elim image_empty image_insert inf_Inf sup_Sup)
lemma Inf_inf_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_dual f ⟹ inf_dual f"
by (smt (verit) comp_eq_elim image_empty image_insert inf_Inf sup_Sup)
lemma Sup_bot_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_dual f ⟹ bot_dual f"
by (metis INF_empty Sup_empty comp_eq_elim)
lemma Inf_top_dual:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_dual f ⟹ top_dual f"
by (metis Inf_empty SUP_empty comp_eq_elim)
text ‹However, Inf-preservation does not imply top-preservation and
Sup-preservation does not imply bottom-preservation.›
lemma
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Sup_pres f ⟹ top_pres f"
oops
lemma
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "Inf_pres f ⟹ bot_pres f"
oops
context complete_lattice
begin
lemma iso_Inf_subdistl:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "mono f ⟹f ∘ Inf ≤ Inf ∘ (`) f"
by (simp add: complete_lattice_class.le_Inf_iff le_funI Inf_lower monoD)
lemma iso_Sup_supdistl:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "mono f ⟹ Sup ∘ (`) f ≤ f ∘ Sup"
by (simp add: complete_lattice_class.Sup_le_iff le_funI Sup_upper monoD)
lemma Inf_subdistl_iso:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "f ∘ Inf ≤ Inf ∘ (`) f ⟹ mono f"
unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.le_INF_iff Inf_atLeast atLeast_iff)
lemma Sup_supdistl_iso:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "Sup ∘ (`) f ≤ f ∘ Sup ⟹ mono f"
unfolding mono_def le_fun_def comp_def by (metis complete_lattice_class.SUP_le_iff Sup_atMost atMost_iff)
lemma supdistl_iso:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "(Sup ∘ (`) f ≤ f ∘ Sup) = mono f"
using Sup_supdistl_iso iso_Sup_supdistl by force
lemma subdistl_iso:
fixes f :: "'a ⇒ 'b::complete_lattice"
shows "(f ∘ Inf ≤ Inf ∘ (`) f) = mono f"
using Inf_subdistl_iso iso_Inf_subdistl by force
end
lemma ord_iso_Inf_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "ord_iso f ⟹ Inf ∘ (`) f = f ∘ Inf"
proof-
let ?g = "the_inv f"
assume h: "ord_iso f"
hence a: "mono ?g"
by (simp add: ord_iso_the_inv)
{fix X :: "'a::complete_lattice set"
{fix y :: "'b::complete_lattice"
have "(y ≤ f (⨅X)) = (?g y ≤ ⨅X)"
by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
also have "... = (∀x ∈ X. ?g y ≤ x)"
by (simp add: le_Inf_iff)
also have "... = (∀x ∈ X. y ≤ f x)"
by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
also have "... = (y ≤ ⨅ (f ` X))"
by (simp add: le_INF_iff)
finally have "(y ≤ f (⨅X)) = (y ≤ ⨅ (f ` X))".}
hence "f (⨅X) = ⨅ (f ` X)"
by (meson dual_order.antisym order_refl)}
thus ?thesis
unfolding fun_eq_iff by simp
qed
lemma ord_iso_Sup_pres:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "ord_iso f ⟹ Sup ∘ (`) f = f ∘ Sup"
proof-
let ?g = "the_inv f"
assume h: "ord_iso f"
hence a: "mono ?g"
by (simp add: ord_iso_the_inv)
{fix X :: "'a::complete_lattice set"
{fix y :: "'b::complete_lattice"
have "(f (⨆X) ≤ y) = (⨆X ≤ ?g y)"
by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
also have "... = (∀x ∈ X. x ≤ ?g y)"
by (simp add: Sup_le_iff)
also have "... = (∀x ∈ X. f x ≤ y)"
by (metis (mono_tags, lifting) UNIV_I f_the_inv_into_f h monoD ord_embed_alt ord_embed_inj ord_iso_alt)
also have "... = (⨆ (f ` X) ≤ y)"
by (simp add: SUP_le_iff)
finally have "(f (⨆X) ≤ y) = (⨆ (f ` X) ≤ y)".}
hence "f (⨆X) = ⨆ (f ` X)"
by (meson dual_order.antisym order_refl)}
thus ?thesis
unfolding fun_eq_iff by simp
qed
text ‹Right preservation of sups and infs is trivial.›
lemma fSup_distr: "Sup_pres (λx. x ∘ f)"
unfolding fun_eq_iff by (simp add: image_comp)
lemma fSup_distr_var: "⨆F ∘ g = (⨆f ∈ F. f ∘ g)"
unfolding fun_eq_iff by (simp add: image_comp)
lemma fInf_distr: "Inf_pres (λx. x ∘ f)"
unfolding fun_eq_iff comp_def
by (smt (verit) INF_apply Inf_fun_def Sup.SUP_cong)
lemma fInf_distr_var: "⨅F ∘ g = (⨅f ∈ F. f ∘ g)"
unfolding fun_eq_iff comp_def
by (smt (verit) INF_apply INF_cong INF_image Inf_apply image_comp image_def image_image)
text ‹The next set of lemma revisits the preservation properties in the function space.›
lemma fSup_subdistl:
assumes "mono (f::'a::complete_lattice ⇒ 'b::complete_lattice)"
shows "Sup ∘ (`) ((∘) f) ≤ (∘) f ∘ Sup"
using assms by (simp add: fun_isol supdistl_iso)
lemma fSup_subdistl_var:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "mono f ⟹ (⨆g ∈ G. f ∘ g) ≤ f ∘ ⨆G"
by (simp add: fun_isol mono_Sup)
lemma fInf_subdistl:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "mono f ⟹ (∘) f ∘ Inf ≤ Inf ∘ (`) ((∘) f)"
by (simp add: fun_isol subdistl_iso)
lemma fInf_subdistl_var:
fixes f :: "'a::complete_lattice ⇒ 'b::complete_lattice"
shows "mono f ⟹ f ∘ ⨅G ≤ (⨅g ∈ G. f ∘ g)"
by (simp add: fun_isol mono_Inf)
lemma fSup_distl: "Sup_pres f ⟹ Sup_pres ((∘) f)"
unfolding fun_eq_iff by (simp add: image_comp)
lemma fSup_distl_var: "Sup_pres f ⟹ f ∘ ⨆G = (⨆g ∈ G. f ∘ g)"
unfolding fun_eq_iff by (simp add: image_comp)
lemma fInf_distl: "Inf_pres f ⟹ Inf_pres ((∘) f)"
unfolding fun_eq_iff by (simp add: image_comp)
lemma fInf_distl_var: "Inf_pres f ⟹ f ∘ ⨅G = (⨅g ∈ G. f ∘ g)"
unfolding fun_eq_iff by (simp add: image_comp)
text ‹Downsets preserve infs whereas upsets preserve sups.›
lemma Inf_pres_downset: "Inf_pres (↓::'a::complete_lattice_with_dual ⇒ 'a set)"
unfolding downset_prop fun_eq_iff
by (safe, simp_all add: le_Inf_iff)
lemma Sup_dual_upset: "Sup_dual (↑::'a::complete_lattice_with_dual ⇒ 'a set)"
unfolding upset_prop fun_eq_iff
by (safe, simp_all add: Sup_le_iff)
text ‹Images of Sup-morphisms are closed under Sups and images of Inf-morphisms are closed under Infs.›
lemma Sup_pres_Sup_closed: "Sup_pres f ⟹ Sup_closed_set (range f)"
by (metis (mono_tags, lifting) Sup_closed_set_def comp_eq_elim range_eqI subset_image_iff)
lemma Inf_pres_Inf_closed: "Inf_pres f ⟹ Inf_closed_set (range f)"
by (metis (mono_tags, lifting) Inf_closed_set_def comp_eq_elim range_eqI subset_image_iff)
text ‹It is well known that functions into complete lattices form complete lattices. Here, such results are shown for
the subclasses of isotone functions, where additional closure conditions must be respected.›
typedef (overloaded) 'a iso = "{f::'a::order ⇒ 'a::order. mono f}"
by (metis Abs_ord_homset_cases ord_homset_def)
setup_lifting type_definition_iso
instantiation iso :: (complete_lattice) complete_lattice
begin
lift_definition Inf_iso :: "'a::complete_lattice iso set ⇒ 'a iso" is Sup
by (metis (mono_tags, lifting) SUP_subset_mono Sup_apply mono_def subsetI)
lift_definition Sup_iso :: "'a::complete_lattice iso set ⇒ 'a iso" is Inf
by (smt (verit) INF_lower2 Inf_apply le_INF_iff mono_def)
lift_definition bot_iso :: "'a::complete_lattice iso" is "⊤"
by (simp add: monoI)
lift_definition sup_iso :: "'a::complete_lattice iso ⇒ 'a iso ⇒ 'a iso" is inf
by (smt (verit) inf_apply inf_mono monoD monoI)
lift_definition top_iso :: "'a::complete_lattice iso" is "⊥"
by (simp add: mono_def)
lift_definition inf_iso :: "'a::complete_lattice iso ⇒ 'a iso ⇒ 'a iso" is sup
by (smt (verit) mono_def sup.mono sup_apply)
lift_definition less_eq_iso :: "'a::complete_lattice iso ⇒ 'a iso ⇒ bool" is "(≥)".
lift_definition less_iso :: "'a::complete_lattice iso ⇒ 'a iso ⇒ bool" is "(>)".
instance
by (intro_classes; transfer, simp_all add: less_fun_def Sup_upper Sup_least Inf_lower Inf_greatest)
end
text ‹Duality has been baked into this result because of its relevance for predicate transformers. A proof
where Sups are mapped to Sups and Infs to Infs is certainly possible, but two instantiation of the same type
and the same classes are unfortunately impossible. Interpretations could be used instead.
A corresponding result for Inf-preseving functions and Sup-lattices, is proved in components on transformers,
as more advanced properties about Inf-preserving functions are needed.›
subsection ‹Alternative Definitions for Complete Boolean Algebras›
text ‹The current definitions of complete boolean algebras deviates from that in most textbooks in that
a distributive law with infinite sups and infinite infs is used. There are interesting applications, for instance
in topology, where weaker laws are needed --- for instance for frames and locales.›
class complete_heyting_algebra = complete_lattice +
assumes ch_dist: "x ⊓ ⨆Y = (⨆y ∈ Y. x ⊓ y)"
text ‹Complete Heyting algebras are also known as frames or locales (they differ with respect to their morphisms).›
class complete_co_heyting_algebra = complete_lattice +
assumes co_ch_dist: "x ⊔ ⨅Y = (⨅y ∈ Y. x ⊔ y)"
class complete_boolean_algebra_alt = complete_lattice + boolean_algebra
instance set :: (type) complete_boolean_algebra_alt..
context complete_boolean_algebra_alt
begin
subclass complete_heyting_algebra
proof
fix x Y
{fix t
have "(x ⊓ ⨆Y ≤ t) = (⨆Y ≤ -x ⊔ t)"
by (simp add: inf.commute shunt1[symmetric])
also have "... = (∀y ∈ Y. y ≤ -x ⊔ t)"
using Sup_le_iff by blast
also have "... = (∀y ∈ Y. x ⊓ y ≤ t)"
by (simp add: inf.commute shunt1)
finally have "(x ⊓ ⨆Y ≤ t) = ((⨆y∈Y. x ⊓ y) ≤ t)"
by (simp add: local.SUP_le_iff)}
thus "x ⊓ ⨆Y = (⨆y∈Y. x ⊓ y)"
using order.eq_iff by blast
qed
subclass complete_co_heyting_algebra
apply unfold_locales
apply (rule order.antisym)
apply (simp add: INF_greatest Inf_lower2)
by (meson eq_refl le_INF_iff le_Inf_iff shunt2)
lemma de_morgan1: "-(⨆X) = (⨅x ∈ X. -x)"
proof-
{fix y
have "(y ≤ -(⨆X)) = (⨆X ≤ -y)"
using compl_le_swap1 by blast
also have "... = (∀x ∈ X. x ≤ -y)"
by (simp add: Sup_le_iff)
also have "... = (∀x ∈ X. y ≤ -x)"
using compl_le_swap1 by blast
also have "... = (y ≤ (⨅x ∈ X. -x))"
using le_INF_iff by force
finally have "(y ≤ -(⨆X)) = (y ≤(⨅x ∈ X. -x))".}
thus ?thesis
using order.antisym by blast
qed
lemma de_morgan2: "-(⨅X) = (⨆x ∈ X. -x)"
by (metis de_morgan1 ba_dual.dual_iff ba_dual.image_dual pointfree_idE)
end
class complete_boolean_algebra_alt_with_dual = complete_lattice_with_dual + complete_boolean_algebra_alt
instantiation set :: (type) complete_boolean_algebra_alt_with_dual
begin
definition dual_set :: "'a set ⇒ 'a set" where
"dual_set = uminus"
instance
by intro_classes (simp_all add: ba_dual.inj_dual dual_set_def comp_def uminus_Sup id_def)
end
context complete_boolean_algebra_alt
begin
sublocale cba_dual: complete_boolean_algebra_alt_with_dual _ _ _ _ _ _ _ _ uminus _ _
by unfold_locales (auto simp: de_morgan2 de_morgan1)
end
subsection ‹Atomic Boolean Algebras›
text ‹Next, atomic boolean algebras are defined.›
context bounded_lattice
begin
text ‹Atoms are covers of bottom.›
definition "atom x = (x ≠ ⊥ ∧ ¬(∃y. ⊥ < y ∧ y < x))"
definition "atom_map x = {y. atom y ∧ y ≤ x}"
lemma atom_map_def_var: "atom_map x = ↓x ∩ Collect atom"
unfolding atom_map_def downset_def downset_set_def comp_def atom_def by fastforce
lemma atom_map_atoms: "⋃(range atom_map) = Collect atom"
unfolding atom_map_def atom_def by auto
end
typedef (overloaded) 'a atoms = "range (atom_map::'a::bounded_lattice ⇒ 'a set)"
by blast
setup_lifting type_definition_atoms
definition at_map :: "'a::bounded_lattice ⇒ 'a atoms" where
"at_map = Abs_atoms ∘ atom_map"
class atomic_boolean_algebra = boolean_algebra +
assumes atomicity: "x ≠ ⊥ ⟹ (∃y. atom y ∧ y ≤ x)"
class complete_atomic_boolean_algebra = complete_lattice + atomic_boolean_algebra
begin
subclass complete_boolean_algebra_alt..
end
text ‹Here are two equivalent definitions for atoms; first in boolean algebras, and then in complete
boolean algebras.›
context boolean_algebra
begin
text ‹The following two conditions are taken from Koppelberg's book~\<^cite>‹"Koppelberg89"›.›
lemma atom_neg: "atom x ⟹ x ≠ ⊥ ∧ (∀y z. x ≤ y ∨ x ≤ -y)"
by (auto simp add: atom_def) (metis local.dual_order.not_eq_order_implies_strict local.inf.cobounded1 local.inf.cobounded2 local.inf_shunt)
lemma atom_sup: "(∀y. x ≤ y ∨ x ≤ -y) ⟹ (∀y z. (x ≤ y ∨ x ≤ z) = (x ≤ y ⊔ z))"
by (metis inf.orderE le_supI1 shunt2)
lemma sup_atom: "x ≠ ⊥ ⟹ (∀y z. (x ≤ y ∨ x ≤ z) = (x ≤ y ⊔ z)) ⟹ atom x"
by (auto simp add: atom_def) (metis (full_types) local.inf.boundedI local.inf.cobounded2 local.inf_shunt local.inf_sup_ord(4) local.le_iff_sup local.shunt1 local.sup.absorb1 local.sup.strict_order_iff)
lemma atom_sup_iff: "atom x = (x ≠ ⊥ ∧ (∀y z. (x ≤ y ∨ x ≤ z) = (x ≤ y ⊔ z)))"
by rule (auto simp add: atom_neg atom_sup sup_atom)
lemma atom_neg_iff: "atom x = (x ≠ ⊥ ∧ (∀y z. x ≤ y ∨ x ≤ -y))"
by rule (auto simp add: atom_neg atom_sup sup_atom)
lemma atom_map_bot_pres: "atom_map ⊥ = {}"
using atom_def atom_map_def le_bot by auto
lemma atom_map_top_pres: "atom_map ⊤ = Collect atom"
using atom_map_def by auto
end
context complete_boolean_algebra_alt
begin
lemma atom_Sup: "⋀Y. x ≠ ⊥ ⟹ (∀y. x ≤ y ∨ x ≤ -y) ⟹ ((∃y ∈ Y. x ≤ y) = (x ≤ ⨆Y))"
by (metis Sup_least Sup_upper2 compl_le_swap1 le_iff_inf inf_shunt)
lemma Sup_atom: "x ≠ ⊥ ⟹ (∀Y. (∃y ∈ Y. x ≤ y) = (x ≤ ⨆Y)) ⟹ atom x"
proof-
assume h1: "x ≠ ⊥"
and h2: "∀Y. (∃y ∈ Y. x ≤ y) = (x ≤ ⨆Y)"
hence "∀y z. (x ≤ y ∨ x ≤ z) = (x ≤ y ⊔ z)"
by (smt (verit) insert_iff sup_Sup sup_bot.right_neutral)
thus "atom x"
by (simp add: h1 sup_atom)
qed
lemma atom_Sup_iff: "atom x = (x ≠ ⊥ ∧ (∀Y. (∃y ∈ Y. x ≤ y) = (x ≤ ⨆Y)))"
by standard (auto simp: atom_neg atom_Sup Sup_atom)
end
end