Theory Filters
section ‹Filters›
text ‹
This theory develops filters based on orders, semilattices, lattices and distributive lattices.
We prove the ultrafilter lemma for orders with a least element.
We show the following structure theorems:
\begin{itemize}
\item The set of filters over a directed semilattice forms a lattice with a greatest element.
\item The set of filters over a bounded semilattice forms a bounded lattice.
\item The set of filters over a distributive lattice with a greatest element forms a bounded distributive lattice.
\end{itemize}
Another result is that in a distributive lattice ultrafilters are prime filters.
We also prove a lemma of Gr\"atzer and Schmidt about principal filters.
We apply these results in proving the construction theorem for Stone algebras (described in a separate theory).
See, for example, \<^cite>‹"BalbesDwinger1974" and "Birkhoff1967" and "Blyth2005" and "DaveyPriestley2002" and "Graetzer1971"› for further results about filters.
›
theory Filters
imports Lattice_Basics
begin
subsection ‹Orders›
text ‹
This section gives the basic definitions related to filters in terms of orders.
The main result is the ultrafilter lemma.
›
context ord
begin
abbreviation down :: "'a ⇒ 'a set" ("↓_" [81] 80)
where "↓x ≡ { y . y ≤ x }"
abbreviation down_set :: "'a set ⇒ 'a set" ("⇓_" [81] 80)
where "⇓X ≡ { y . ∃x∈X . y ≤ x }"
abbreviation is_down_set :: "'a set ⇒ bool"
where "is_down_set X ≡ ∀x∈X . ∀y . y ≤ x ⟶ y∈X"
abbreviation is_principal_down :: "'a set ⇒ bool"
where "is_principal_down X ≡ ∃x . X = ↓x"
abbreviation up :: "'a ⇒ 'a set" ("↑_" [81] 80)
where "↑x ≡ { y . x ≤ y }"
abbreviation up_set :: "'a set ⇒ 'a set" ("⇑_" [81] 80)
where "⇑X ≡ { y . ∃x∈X . x ≤ y }"
abbreviation is_up_set :: "'a set ⇒ bool"
where "is_up_set X ≡ ∀x∈X . ∀y . x ≤ y ⟶ y∈X"
abbreviation is_principal_up :: "'a set ⇒ bool"
where "is_principal_up X ≡ ∃x . X = ↑x"
text ‹
A filter is a non-empty, downward directed, up-closed set.
›
definition filter :: "'a set ⇒ bool"
where "filter F ≡ (F ≠ {}) ∧ (∀x∈F . ∀y∈F . ∃z∈F . z ≤ x ∧ z ≤ y) ∧ is_up_set F"
abbreviation proper_filter :: "'a set ⇒ bool"
where "proper_filter F ≡ filter F ∧ F ≠ UNIV"
abbreviation ultra_filter :: "'a set ⇒ bool"
where "ultra_filter F ≡ proper_filter F ∧ (∀G . proper_filter G ∧ F ⊆ G ⟶ F = G)"
abbreviation filters :: "'a set set"
where "filters ≡ { F::'a set . filter F }"
lemma filter_map_filter:
assumes "filter F"
and "mono f"
and "∀x y . f x ≤ y ⟶ (∃z . x ≤ z ∧ y = f z)"
shows "filter (f ` F)"
proof (unfold ord_class.filter_def, intro conjI)
show "f ` F ≠ {}"
using assms(1) ord_class.filter_def by auto
next
show "∀x∈f ` F . ∀y∈f ` F . ∃z∈f ` F . z ≤ x ∧ z ≤ y"
proof (intro ballI)
fix x y
assume "x ∈ f ` F" and "y ∈ f ` F"
then obtain u v where 1: "x = f u ∧ u ∈ F ∧ y = f v ∧ v ∈ F"
by auto
then obtain w where "w ≤ u ∧ w ≤ v ∧ w ∈ F"
by (meson assms(1) ord_class.filter_def)
thus "∃z∈f ` F . z ≤ x ∧ z ≤ y"
using 1 assms(2) mono_def image_eqI by blast
qed
next
show "is_up_set (f ` F)"
proof
fix x
assume "x ∈ f ` F"
then obtain u where 1: "x = f u ∧ u ∈ F"
by auto
show "∀y . x ≤ y ⟶ y ∈ f ` F"
proof (rule allI, rule impI)
fix y
assume "x ≤ y"
hence "f u ≤ y"
using 1 by simp
then obtain z where "u ≤ z ∧ y = f z"
using assms(3) by auto
thus "y ∈ f ` F"
by (meson 1 assms(1) image_iff ord_class.filter_def)
qed
qed
qed
end
context order
begin
lemma self_in_downset [simp]:
"x ∈ ↓x"
by simp
lemma self_in_upset [simp]:
"x ∈ ↑x"
by simp
lemma up_filter [simp]:
"filter (↑x)"
using filter_def order_lesseq_imp by auto
lemma up_set_up_set [simp]:
"is_up_set (⇑X)"
using order.trans by fastforce
lemma up_injective:
"↑x = ↑y ⟹ x = y"
using order.antisym by auto
lemma up_antitone:
"x ≤ y ⟷ ↑y ⊆ ↑x"
by auto
end
context order_bot
begin
lemma bot_in_downset [simp]:
"bot ∈ ↓x"
by simp
lemma down_bot [simp]:
"↓bot = {bot}"
by (simp add: bot_unique)
lemma up_bot [simp]:
"↑bot = UNIV"
by simp
text ‹
The following result is the ultrafilter lemma, generalised from \<^cite>‹‹10.17› in "DaveyPriestley2002"› to orders with a least element.
Its proof uses Isabelle/HOL's ‹Zorn_Lemma›, which requires closure under union of arbitrary (possibly empty) chains.
Actually, the proof does not use any of the underlying order properties except ‹bot_least›.
›
lemma ultra_filter:
assumes "proper_filter F"
shows "∃G . ultra_filter G ∧ F ⊆ G"
proof -
let ?A = "{ G . (proper_filter G ∧ F ⊆ G) ∨ G = {} }"
have "∀C ∈ chains ?A . ⋃C ∈ ?A"
proof
fix C :: "'a set set"
let ?D = "C - {{}}"
assume 1: "C ∈ chains ?A"
hence 2: "∀x∈⋃?D . ∃H∈?D . x ∈ H ∧ proper_filter H"
using chainsD2 by fastforce
have 3: "⋃?D = ⋃C"
by blast
have "⋃?D ∈ ?A"
proof (cases "?D = {}")
assume "?D = {}"
thus ?thesis
by auto
next
assume 4: "?D ≠ {}"
then obtain G where "G ∈ ?D"
by auto
hence 5: "F ⊆ ⋃?D"
using 1 chainsD2 by blast
have 6: "is_up_set (⋃?D)"
proof
fix x
assume "x ∈ ⋃?D"
then obtain H where "x ∈ H ∧ H ∈ ?D ∧ filter H"
using 2 by auto
thus "∀y . x ≤ y ⟶ y∈⋃?D"
using filter_def UnionI by fastforce
qed
have 7: "⋃?D ≠ UNIV"
proof (rule ccontr)
assume "¬ ⋃?D ≠ UNIV"
then obtain H where "bot ∈ H ∧ proper_filter H"
using 2 by blast
thus False
by (meson UNIV_I bot_least filter_def subsetI subset_antisym)
qed
{
fix x y
assume "x∈⋃?D ∧ y∈⋃?D"
then obtain H I where 8: "x ∈ H ∧ H ∈ ?D ∧ filter H ∧ y ∈ I ∧ I ∈ ?D ∧ filter I"
using 2 by metis
have "∃z∈⋃?D . z ≤ x ∧ z ≤ y"
proof (cases "H ⊆ I")
assume "H ⊆ I"
hence "∃z∈I . z ≤ x ∧ z ≤ y"
using 8 by (metis subsetCE filter_def)
thus ?thesis
using 8 by (metis UnionI)
next
assume "¬ (H ⊆ I)"
hence "I ⊆ H"
using 1 8 by (meson DiffE chainsD)
hence "∃z∈H . z ≤ x ∧ z ≤ y"
using 8 by (metis subsetCE filter_def)
thus ?thesis
using 8 by (metis UnionI)
qed
}
thus ?thesis
using 4 5 6 7 filter_def by auto
qed
thus "⋃C ∈ ?A"
using 3 by simp
qed
hence "∃M∈?A . ∀X∈?A . M ⊆ X ⟶ X = M"
by (rule Zorn_Lemma)
then obtain M where 9: "M ∈ ?A ∧ (∀X∈?A . M ⊆ X ⟶ X = M)"
by auto
hence 10: "M ≠ {}"
using assms filter_def by auto
{
fix G
assume 11: "proper_filter G ∧ M ⊆ G"
hence "F ⊆ G"
using 9 10 by blast
hence "M = G"
using 9 11 by auto
}
thus ?thesis
using 9 10 by blast
qed
end
context order_top
begin
lemma down_top [simp]:
"↓top = UNIV"
by simp
lemma top_in_upset [simp]:
"top ∈ ↑x"
by simp
lemma up_top [simp]:
"↑top = {top}"
by (simp add: top_unique)
lemma filter_top [simp]:
"filter {top}"
using filter_def top_unique by auto
lemma top_in_filter [simp]:
"filter F ⟹ top ∈ F"
using filter_def by fastforce
end
text ‹
The existence of proper filters and ultrafilters requires that the underlying order contains at least two elements.
›
context non_trivial_order
begin
lemma proper_filter_exists:
"∃F . proper_filter F"
proof -
from consistent obtain x y :: 'a where "x ≠ y"
by auto
hence "↑x ≠ UNIV ∨ ↑y ≠ UNIV"
using order.antisym by blast
hence "proper_filter (↑x) ∨ proper_filter (↑y)"
by simp
thus ?thesis
by blast
qed
end
context non_trivial_order_bot
begin
lemma ultra_filter_exists:
"∃F . ultra_filter F"
using ultra_filter proper_filter_exists by blast
end
context non_trivial_bounded_order
begin
lemma proper_filter_top:
"proper_filter {top}"
using bot_not_top filter_top by blast
lemma ultra_filter_top:
"∃G . ultra_filter G ∧ top ∈ G"
using ultra_filter proper_filter_top by fastforce
end
subsection ‹Lattices›
text ‹
This section develops the lattice structure of filters based on a semilattice structure of the underlying order.
The main results are that filters over a directed semilattice form a lattice with a greatest element and that filters over a bounded semilattice form a bounded lattice.
›
context semilattice_sup
begin
abbreviation prime_filter :: "'a set ⇒ bool"
where "prime_filter F ≡ proper_filter F ∧ (∀x y . x ⊔ y ∈ F ⟶ x ∈ F ∨ y ∈ F)"
end
context semilattice_inf
begin
lemma filter_inf_closed:
"filter F ⟹ x ∈ F ⟹ y ∈ F ⟹ x ⊓ y ∈ F"
by (meson filter_def inf.boundedI)
lemma filter_univ:
"filter UNIV"
by (meson UNIV_I UNIV_not_empty filter_def inf.cobounded1 inf.cobounded2)
text ‹
The operation ‹filter_sup› is the join operation in the lattice of filters.
›
definition "filter_sup F G ≡ { z . ∃x∈F . ∃y∈G . x ⊓ y ≤ z }"
lemma filter_sup:
assumes "filter F"
and "filter G"
shows "filter (filter_sup F G)"
proof -
have "F ≠ {} ∧ G ≠ {}"
using assms filter_def by blast
hence 1: "filter_sup F G ≠ {}"
using filter_sup_def by blast
have 2: "∀x∈filter_sup F G . ∀y∈filter_sup F G . ∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
proof
fix x
assume "x∈filter_sup F G"
then obtain t u where 3: "t ∈ F ∧ u ∈ G ∧ t ⊓ u ≤ x"
using filter_sup_def by auto
show "∀y∈filter_sup F G . ∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
proof
fix y
assume "y∈filter_sup F G"
then obtain v w where 4: "v ∈ F ∧ w ∈ G ∧ v ⊓ w ≤ y"
using filter_sup_def by auto
let ?z = "(t ⊓ v) ⊓ (u ⊓ w)"
have 5: "?z ≤ x ∧ ?z ≤ y"
using 3 4 by (meson order.trans inf.cobounded1 inf.cobounded2 inf_mono)
have "?z ∈ filter_sup F G"
unfolding filter_sup_def using assms 3 4 filter_inf_closed by blast
thus "∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
using 5 by blast
qed
qed
have "∀x∈filter_sup F G . ∀y . x ≤ y ⟶ y ∈ filter_sup F G"
unfolding filter_sup_def using order_trans by blast
thus ?thesis
using 1 2 filter_def by presburger
qed
lemma filter_sup_left_upper_bound:
assumes "filter G"
shows "F ⊆ filter_sup F G"
proof -
from assms obtain y where "y∈G"
using all_not_in_conv filter_def by auto
thus ?thesis
unfolding filter_sup_def using inf.cobounded1 by blast
qed
lemma filter_sup_symmetric:
"filter_sup F G = filter_sup G F"
unfolding filter_sup_def using inf.commute by fastforce
lemma filter_sup_right_upper_bound:
"filter F ⟹ G ⊆ filter_sup F G"
using filter_sup_symmetric filter_sup_left_upper_bound by simp
lemma filter_sup_least_upper_bound:
assumes "filter H"
and "F ⊆ H"
and "G ⊆ H"
shows "filter_sup F G ⊆ H"
proof
fix x
assume "x ∈ filter_sup F G"
then obtain y z where 1: "y ∈ F ∧ z ∈ G ∧ y ⊓ z ≤ x"
using filter_sup_def by auto
hence "y ∈ H ∧ z ∈ H"
using assms(2-3) by auto
hence "y ⊓ z ∈ H"
by (simp add: assms(1) filter_inf_closed)
thus "x ∈ H"
using 1 assms(1) filter_def by auto
qed
lemma filter_sup_left_isotone:
"G ⊆ H ⟹ filter_sup G F ⊆ filter_sup H F"
unfolding filter_sup_def by blast
lemma filter_sup_right_isotone:
"G ⊆ H ⟹ filter_sup F G ⊆ filter_sup F H"
unfolding filter_sup_def by blast
lemma filter_sup_right_isotone_var:
"filter_sup F (G ∩ H) ⊆ filter_sup F H"
unfolding filter_sup_def by blast
lemma up_dist_inf:
"↑(x ⊓ y) = filter_sup (↑x) (↑y)"
proof
show "↑(x ⊓ y) ⊆ filter_sup (↑x) (↑y)"
unfolding filter_sup_def by blast
next
show "filter_sup (↑x) (↑y) ⊆ ↑(x ⊓ y)"
proof
fix z
assume "z ∈ filter_sup (↑x) (↑y)"
then obtain u v where "u∈↑x ∧ v∈↑y ∧ u ⊓ v ≤ z"
using filter_sup_def by auto
hence "x ⊓ y ≤ z"
using order.trans inf_mono by blast
thus "z ∈ ↑(x ⊓ y)"
by blast
qed
qed
text ‹
The following result is part of \<^cite>‹‹Exercise 2.23› in "DaveyPriestley2002"›.
›
lemma filter_inf_filter [simp]:
assumes "filter F"
shows "filter (⇑{ y . ∃z∈F . x ⊓ z = y})"
proof -
let ?G = "⇑{ y . ∃z∈F . x ⊓ z = y}"
have "F ≠ {}"
using assms filter_def by simp
hence 1: "?G ≠ {}"
by blast
have 2: "is_up_set ?G"
by auto
{
fix y z
assume "y ∈ ?G ∧ z ∈ ?G"
then obtain v w where "v ∈ F ∧ w ∈ F ∧ x ⊓ v ≤ y ∧ x ⊓ w ≤ z"
by auto
hence "v ⊓ w ∈ F ∧ x ⊓ (v ⊓ w) ≤ y ⊓ z"
by (meson assms filter_inf_closed order.trans inf.boundedI inf.cobounded1 inf.cobounded2)
hence "∃u∈?G . u ≤ y ∧ u ≤ z"
by auto
}
hence "∀x∈?G . ∀y∈?G . ∃z∈?G . z ≤ x ∧ z ≤ y"
by auto
thus ?thesis
using 1 2 filter_def by presburger
qed
end
context directed_semilattice_inf
begin
text ‹
Set intersection is the meet operation in the lattice of filters.
›
lemma filter_inf:
assumes "filter F"
and "filter G"
shows "filter (F ∩ G)"
proof (unfold filter_def, intro conjI)
from assms obtain x y where 1: "x∈F ∧ y∈G"
using all_not_in_conv filter_def by auto
from ub obtain z where "x ≤ z ∧ y ≤ z"
by auto
hence "z ∈ F ∩ G"
using 1 by (meson assms Int_iff filter_def)
thus "F ∩ G ≠ {}"
by blast
next
show "is_up_set (F ∩ G)"
by (meson assms Int_iff filter_def)
next
show "∀x∈F ∩ G . ∀y∈F ∩ G . ∃z∈F ∩ G . z ≤ x ∧ z ≤ y"
by (metis assms Int_iff filter_inf_closed inf.cobounded2 inf.commute)
qed
end
text ‹
We introduce the following type of filters to instantiate the lattice classes and thereby inherit the results shown about lattices.
›
typedef (overloaded) 'a filter = "{ F::'a::order set . filter F }"
by (meson mem_Collect_eq up_filter)
lemma simp_filter [simp]:
"filter (Rep_filter x)"
using Rep_filter by simp
setup_lifting type_definition_filter
text ‹
The set of filters over a directed semilattice forms a lattice with a greatest element.
›
instantiation filter :: (directed_semilattice_inf) bounded_lattice_top
begin
lift_definition top_filter :: "'a filter" is UNIV
by (simp add: filter_univ)
lift_definition sup_filter :: "'a filter ⇒ 'a filter ⇒ 'a filter" is filter_sup
by (simp add: filter_sup)
lift_definition inf_filter :: "'a filter ⇒ 'a filter ⇒ 'a filter" is inter
by (simp add: filter_inf)
lift_definition less_eq_filter :: "'a filter ⇒ 'a filter ⇒ bool" is subset_eq .
lift_definition less_filter :: "'a filter ⇒ 'a filter ⇒ bool" is subset .
instance
apply intro_classes
subgoal apply transfer by (simp add: less_le_not_le)
subgoal apply transfer by simp
subgoal apply transfer by simp
subgoal apply transfer by simp
subgoal apply transfer by simp
subgoal apply transfer by simp
subgoal apply transfer by simp
subgoal apply transfer by (simp add: filter_sup_left_upper_bound)
subgoal apply transfer by (simp add: filter_sup_right_upper_bound)
subgoal apply transfer by (simp add: filter_sup_least_upper_bound)
subgoal apply transfer by simp
done
end
context bounded_semilattice_inf_top
begin
abbreviation "filter_complements F G ≡ filter F ∧ filter G ∧ filter_sup F G = UNIV ∧ F ∩ G = {top}"
end
text ‹
The set of filters over a bounded semilattice forms a bounded lattice.
›
instantiation filter :: (bounded_semilattice_inf_top) bounded_lattice
begin
lift_definition bot_filter :: "'a filter" is "{top}"
by simp
instance
apply intro_classes
apply transfer
by simp
end
context lattice
begin
lemma up_dist_sup:
"↑(x ⊔ y) = ↑x ∩ ↑y"
by auto
end
text ‹
For convenience, the following function injects principal filters into the filter type.
We cannot define it in the ‹order› class since the type filter requires the sort constraint ‹order› that is not available in the class.
The result of the function is a filter by lemma ‹up_filter›.
›
abbreviation up_filter :: "'a::order ⇒ 'a filter"
where "up_filter x ≡ Abs_filter (↑x)"
lemma up_filter_dist_inf:
"up_filter ((x::'a::lattice) ⊓ y) = up_filter x ⊔ up_filter y"
by (simp add: eq_onp_def sup_filter.abs_eq up_dist_inf)
lemma up_filter_dist_sup:
"up_filter ((x::'a::lattice) ⊔ y) = up_filter x ⊓ up_filter y"
by (metis eq_onp_def inf_filter.abs_eq up_dist_sup up_filter)
lemma up_filter_injective:
"up_filter x = up_filter y ⟹ x = y"
by (metis Abs_filter_inject mem_Collect_eq up_filter up_injective)
lemma up_filter_antitone:
"x ≤ y ⟷ up_filter y ≤ up_filter x"
by (metis eq_onp_same_args less_eq_filter.abs_eq up_antitone up_filter)
text ‹
The following definition applies a function to each element of a filter.
The subsequent lemma gives conditions under which the result of this application is a filter.
›
abbreviation filter_map :: "('a::order ⇒ 'b::order) ⇒ 'a filter ⇒ 'b filter"
where "filter_map f F ≡ Abs_filter (f ` Rep_filter F)"
lemma filter_map_filter:
assumes "mono f"
and "∀x y . f x ≤ y ⟶ (∃z . x ≤ z ∧ y = f z)"
shows "filter (f ` Rep_filter F)"
by (simp add: assms inf.filter_map_filter)
subsection ‹Distributive Lattices›
text ‹
In this section we additionally assume that the underlying order forms a distributive lattice.
Then filters form a bounded distributive lattice if the underlying order has a greatest element.
Moreover ultrafilters are prime filters.
We also prove a lemma of Gr\"atzer and Schmidt about principal filters.
›
context distrib_lattice
begin
lemma filter_sup_left_dist_inf:
assumes "filter F"
and "filter G"
and "filter H"
shows "filter_sup F (G ∩ H) = filter_sup F G ∩ filter_sup F H"
proof
show "filter_sup F (G ∩ H) ⊆ filter_sup F G ∩ filter_sup F H"
unfolding filter_sup_def using filter_sup_right_isotone_var by blast
next
show "filter_sup F G ∩ filter_sup F H ⊆ filter_sup F (G ∩ H)"
proof
fix x
assume "x ∈ filter_sup F G ∩ filter_sup F H"
then obtain t u v w where 1: "t ∈ F ∧ u ∈ G ∧ v ∈ F ∧ w ∈ H ∧ t ⊓ u ≤ x ∧ v ⊓ w ≤ x"
using filter_sup_def by auto
let ?y = "t ⊓ v"
let ?z = "u ⊔ w"
have 2: "?y ∈ F"
using 1 by (simp add: assms(1) filter_inf_closed)
have 3: "?z ∈ G ∩ H"
using 1 by (meson assms(2-3) Int_iff filter_def sup_ge1 sup_ge2)
have "?y ⊓ ?z = (t ⊓ v ⊓ u) ⊔ (t ⊓ v ⊓ w)"
by (simp add: inf_sup_distrib1)
also have "... ≤ (t ⊓ u) ⊔ (v ⊓ w)"
by (metis inf.cobounded1 inf.cobounded2 inf.left_idem inf_mono sup.mono)
also have "... ≤ x"
using 1 by (simp add: le_supI)
finally show "x ∈ filter_sup F (G ∩ H)"
unfolding filter_sup_def using 2 3 by blast
qed
qed
lemma filter_inf_principal_rep:
"F ∩ G = ↑z ⟹ (∃x∈F . ∃y∈G . z = x ⊔ y)"
by force
lemma filter_sup_principal_rep:
assumes "filter F"
and "filter G"
and "filter_sup F G = ↑z"
shows "∃x∈F . ∃y∈G . z = x ⊓ y"
proof -
from assms(3) obtain x y where 1: "x∈F ∧ y∈G ∧ x ⊓ y ≤ z"
unfolding filter_sup_def using order_refl by blast
hence 2: "x ⊔ z ∈ F ∧ y ⊔ z ∈ G"
by (meson assms(1-2) sup_ge1 filter_def)
have "(x ⊔ z) ⊓ (y ⊔ z) = z"
using 1 sup_absorb2 sup_inf_distrib2 by fastforce
thus ?thesis
using 2 by force
qed
lemma inf_sup_principal_aux:
assumes "filter F"
and "filter G"
and "is_principal_up (filter_sup F G)"
and "is_principal_up (F ∩ G)"
shows "is_principal_up F"
proof -
from assms(3-4) obtain x y where 1: "filter_sup F G = ↑x ∧ F ∩ G = ↑y"
by blast
from filter_inf_principal_rep obtain t u where 2: "t∈F ∧ u∈G ∧ y = t ⊔ u"
using 1 by meson
from filter_sup_principal_rep obtain v w where 3: "v∈F ∧ w∈G ∧ x = v ⊓ w"
using 1 by (meson assms(1-2))
have "t ∈ filter_sup F G ∧ u ∈ filter_sup F G"
unfolding filter_sup_def using 2 inf.cobounded1 inf.cobounded2 by blast
hence "x ≤ t ∧ x ≤ u"
using 1 by blast
hence 4: "(t ⊓ v) ⊓ (u ⊓ w) = x"
using 3 by (simp add: inf.absorb2 inf.assoc inf.left_commute)
have "(t ⊓ v) ⊔ (u ⊓ w) ∈ F ∧ (t ⊓ v) ⊔ (u ⊓ w) ∈ G"
using 2 3 by (metis (no_types, lifting) assms(1-2) filter_inf_closed sup.cobounded1 sup.cobounded2 filter_def)
hence "y ≤ (t ⊓ v) ⊔ (u ⊓ w)"
using 1 Int_iff by blast
hence 5: "(t ⊓ v) ⊔ (u ⊓ w) = y"
using 2 by (simp add: order.antisym inf.coboundedI1)
have "F = ↑(t ⊓ v)"
proof
show "F ⊆ ↑(t ⊓ v)"
proof
fix z
assume 6: "z ∈ F"
hence "z ∈ filter_sup F G"
unfolding filter_sup_def using 2 inf.cobounded1 by blast
hence "x ≤ z"
using 1 by simp
hence 7: "(t ⊓ v ⊓ z) ⊓ (u ⊓ w) = x"
using 4 by (metis inf.absorb1 inf.assoc inf.commute)
have "z ⊔ u ∈ F ∧ z ⊔ u ∈ G ∧ z ⊔ w ∈ F ∧ z ⊔ w ∈ G"
using 2 3 6 by (meson assms(1-2) filter_def sup_ge1 sup_ge2)
hence "y ≤ (z ⊔ u) ⊓ (z ⊔ w)"
using 1 Int_iff filter_inf_closed by auto
hence 8: "(t ⊓ v ⊓ z) ⊔ (u ⊓ w) = y"
using 5 by (metis inf.absorb1 sup.commute sup_inf_distrib2)
have "t ⊓ v ⊓ z = t ⊓ v"
using 4 5 7 8 relative_equality by blast
thus "z ∈ ↑(t ⊓ v)"
by (simp add: inf.orderI)
qed
next
show "↑(t ⊓ v) ⊆ F"
proof
fix z
have 9: "t ⊓ v ∈ F"
using 2 3 by (simp add: assms(1) filter_inf_closed)
assume "z ∈ ↑(t ⊓ v)"
hence "t ⊓ v ≤ z" by simp
thus "z ∈ F"
using assms(1) 9 filter_def by auto
qed
qed
thus ?thesis
by blast
qed
text ‹
The following result is \<^cite>‹‹Lemma II› in "GraetzerSchmidt1958"›.
If both join and meet of two filters are principal filters, both filters are principal filters.
›
lemma inf_sup_principal:
assumes "filter F"
and "filter G"
and "is_principal_up (filter_sup F G)"
and "is_principal_up (F ∩ G)"
shows "is_principal_up F ∧ is_principal_up G"
proof -
have "filter G ∧ filter F ∧ is_principal_up (filter_sup G F) ∧ is_principal_up (G ∩ F)"
by (simp add: assms Int_commute filter_sup_symmetric)
thus ?thesis
using assms(3) inf_sup_principal_aux by blast
qed
lemma filter_sup_absorb_inf: "filter F ⟹ filter G ⟹ filter_sup (F ∩ G) G = G"
by (simp add: filter_inf filter_sup_least_upper_bound filter_sup_left_upper_bound filter_sup_symmetric subset_antisym)
lemma filter_inf_absorb_sup: "filter F ⟹ filter G ⟹ filter_sup F G ∩ G = G"
apply (rule subset_antisym)
apply simp
by (simp add: filter_sup_right_upper_bound)
lemma filter_inf_right_dist_sup:
assumes "filter F"
and "filter G"
and "filter H"
shows "filter_sup F G ∩ H = filter_sup (F ∩ H) (G ∩ H)"
proof -
have "filter_sup (F ∩ H) (G ∩ H) = filter_sup (F ∩ H) G ∩ filter_sup (F ∩ H) H"
by (simp add: assms filter_sup_left_dist_inf filter_inf)
also have "... = filter_sup (F ∩ H) G ∩ H"
using assms(1,3) filter_sup_absorb_inf by simp
also have "... = filter_sup F G ∩ filter_sup G H ∩ H"
using assms filter_sup_left_dist_inf filter_sup_symmetric by simp
also have "... = filter_sup F G ∩ H"
by (simp add: assms(2-3) filter_inf_absorb_sup semilattice_inf_class.inf_assoc)
finally show ?thesis
by simp
qed
text ‹
The following result generalises \<^cite>‹‹10.11› in "DaveyPriestley2002"› to distributive lattices as remarked after that section.
›
lemma ultra_filter_prime:
assumes "ultra_filter F"
shows "prime_filter F"
proof -
{
fix x y
assume 1: "x ⊔ y ∈ F ∧ x ∉ F"
let ?G = "⇑{ z . ∃w∈F . x ⊓ w = z }"
have 2: "filter ?G"
using assms filter_inf_filter by simp
have "x ∈ ?G"
using 1 by auto
hence 3: "F ≠ ?G"
using 1 by auto
have "F ⊆ ?G"
using inf_le2 order_trans by blast
hence "?G = UNIV"
using 2 3 assms by blast
then obtain z where 4: "z ∈ F ∧ x ⊓ z ≤ y"
by blast
hence "y ⊓ z = (x ⊔ y) ⊓ z"
by (simp add: inf_sup_distrib2 sup_absorb2)
also have "... ∈ F"
using 1 4 assms filter_inf_closed by auto
finally have "y ∈ F"
using assms by (simp add: filter_def)
}
thus ?thesis
using assms by blast
qed
lemma up_dist_inf_inter:
assumes "is_up_set S"
shows "↑(x ⊓ y) ∩ S = filter_sup (↑x ∩ S) (↑y ∩ S) ∩ S"
proof
show "↑(x ⊓ y) ∩ S ⊆ filter_sup (↑x ∩ S) (↑y ∩ S) ∩ S"
proof
fix z
let ?x = "x ⊔ z"
let ?y = "y ⊔ z"
assume "z ∈ ↑(x ⊓ y) ∩ S"
hence 1: "x ⊓ y ≤ z ∧ z ∈ S"
by auto
hence "?x ∈ (↑x ∩ S) ∧ ?y ∈ (↑y ∩ S) ∧ ?x ⊓ ?y ≤ z"
using assms sup_absorb2 sup_inf_distrib2 by fastforce
thus "z ∈ filter_sup (↑x ∩ S) (↑y ∩ S) ∩ S"
using filter_sup_def 1 by fastforce
qed
next
show "filter_sup (↑x ∩ S) (↑y ∩ S) ∩ S ⊆ ↑(x ⊓ y) ∩ S"
proof
fix z
assume "z ∈ filter_sup (↑x ∩ S) (↑y ∩ S) ∩ S"
then obtain u v where 2: "u∈↑x ∧ v∈↑y ∧ u ⊓ v ≤ z ∧ z ∈ S"
using filter_sup_def by auto
hence "x ⊓ y ≤ z"
using order.trans inf_mono by blast
thus "z ∈ ↑(x ⊓ y) ∩ S"
using 2 by blast
qed
qed
end
context distrib_lattice_bot
begin
lemma prime_filter:
"proper_filter F ⟹ ∃G . prime_filter G ∧ F ⊆ G"
by (metis ultra_filter ultra_filter_prime)
end
context distrib_lattice_top
begin
lemma complemented_filter_inf_principal:
assumes "filter_complements F G"
shows "is_principal_up (F ∩ ↑x)"
proof -
have 1: "filter F ∧ filter G"
by (simp add: assms)
hence 2: "filter (F ∩ ↑x) ∧ filter (G ∩ ↑x)"
by (simp add: filter_inf)
have "(F ∩ ↑x) ∩ (G ∩ ↑x) = {top}"
using assms Int_assoc Int_insert_left_if1 inf_bot_left inf_sup_aci(3) top_in_upset inf.idem by auto
hence 3: "is_principal_up ((F ∩ ↑x) ∩ (G ∩ ↑x))"
using up_top by blast
have "filter_sup (F ∩ ↑x) (G ∩ ↑x) = filter_sup F G ∩ ↑x"
using 1 filter_inf_right_dist_sup up_filter by auto
also have "... = ↑x"
by (simp add: assms)
finally have "is_principal_up (filter_sup (F ∩ ↑x) (G ∩ ↑x))"
by auto
thus ?thesis
using 1 2 3 inf_sup_principal_aux by blast
qed
end
text ‹
The set of filters over a distributive lattice with a greatest element forms a bounded distributive lattice.
›
instantiation filter :: (distrib_lattice_top) bounded_distrib_lattice
begin
instance
apply intro_classes
apply transfer
by (simp add: filter_sup_left_dist_inf)
end
end