Theory Birkhoff_Finite_Distributive_Lattices
theory Birkhoff_Finite_Distributive_Lattices
imports
"HOL-Library.Finite_Lattice"
"HOL.Transcendental"
begin
unbundle lattice_syntax
text ‹ The proof of Birkhoff's representation theorem for finite
distributive lattices @{cite birkhoffRingsSets1937} presented
here follows Davey and Priestley @{cite daveyChapterRepresentationFinite2002}. ›
section ‹ Atoms, Join Primes and Join Irreducibles \label{sec:join-irreducibles} ›
text ‹ Atomic elements are defined as follows. ›
definition (in bounded_lattice_bot) atomic :: "'a ⇒ bool" where
"atomic x ≡ x ≠ ⊥ ∧ (∀ y. y ≤ x ⟶ y = ⊥ ∨ y = x)"
text ‹ Two related concepts are ∗‹join-prime› elements and ∗‹join-irreducible›
elements. ›
definition (in bounded_lattice_bot) join_prime :: "'a ⇒ bool" where
"join_prime x ≡ x ≠ ⊥ ∧ (∀ y z . x ≤ y ⊔ z ⟶ x ≤ y ∨ x ≤ z)"
definition (in bounded_lattice_bot) join_irreducible :: "'a ⇒ bool" where
"join_irreducible x ≡ x ≠ ⊥ ∧ (∀ y z . y < x ⟶ z < x ⟶ y ⊔ z < x)"
lemma (in bounded_lattice_bot) join_irreducible_def':
"join_irreducible x = (x ≠ ⊥ ∧ (∀ y z . x = y ⊔ z ⟶ x = y ∨ x = z))"
unfolding join_irreducible_def
by (metis
nless_le
sup.bounded_iff
sup.cobounded1
sup_ge2)
text ‹ Every join-prime is also join-irreducible. ›
lemma (in bounded_lattice_bot) join_prime_implies_join_irreducible:
assumes "join_prime x"
shows "join_irreducible x"
using assms
unfolding
join_irreducible_def'
join_prime_def
by (simp add: dual_order.eq_iff)
text ‹ In the special case when the underlying lattice is
distributive, the join-prime elements and join-irreducible
elements coincide. ›
class bounded_distrib_lattice_bot = bounded_lattice_bot +
assumes sup_inf_distrib1: "x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
begin
subclass distrib_lattice
by (unfold_locales, metis (full_types) sup_inf_distrib1)
end
context complete_distrib_lattice
begin
subclass bounded_distrib_lattice_bot
by (unfold_locales,
metis (full_types)
sup_inf_distrib1)
end
lemma (in bounded_distrib_lattice_bot) join_irreducible_is_join_prime:
"join_irreducible x = join_prime x"
proof
assume "join_prime x"
thus "join_irreducible x"
by (simp add: join_prime_implies_join_irreducible)
next
assume "join_irreducible x"
{
fix y z
assume "x ≤ y ⊔ z"
hence "x = x ⊓ (y ⊔ z)"
by (metis local.inf.orderE)
hence "x = (x ⊓ y) ⊔ (x ⊓ z)"
using inf_sup_distrib1 by auto
hence "(x = x ⊓ y) ∨ (x = x ⊓ z)"
using ‹join_irreducible x›
unfolding join_irreducible_def'
by metis
hence "(x ≤ y) ∨ (x ≤ z)"
by (metis (full_types) local.inf.cobounded2)
}
thus "join_prime x"
by (metis
‹join_irreducible x›
join_irreducible_def'
join_prime_def)
qed
text ‹ Every atomic element is join-irreducible. ›
lemma (in bounded_lattice_bot) atomic_implies_join_prime:
assumes "atomic x"
shows "join_irreducible x"
using assms
unfolding
atomic_def
join_irreducible_def'
by (metis (no_types, opaque_lifting)
sup.cobounded2
sup_bot.right_neutral)
text ‹ In the case of Boolean algebras, atomic elements and
join-prime elements are one-in-the-same. ›
lemma (in boolean_algebra) join_prime_is_atomic:
"atomic x = join_prime x"
proof
assume "atomic x"
{
fix y z
assume "x ≤ y ⊔ z"
hence "x = (x ⊓ y) ⊔ (x ⊓ z)"
using inf.absorb1 inf_sup_distrib1 by fastforce
moreover
have "x ≤ y ∨ (x ⊓ y) = ⊥"
"x ≤ z ∨ (x ⊓ z) = ⊥"
using ‹atomic x› inf.cobounded1 inf.cobounded2
unfolding atomic_def
by fastforce+
ultimately have "x ≤ y ∨ x ≤ z"
using ‹atomic x› atomic_def by auto
}
thus "join_prime x"
using ‹atomic x› join_prime_def atomic_def
by auto
next
assume "join_prime x"
{
fix y
assume "y ≤ x" "y ≠ x"
hence "x = x ⊔ y"
using sup.orderE by blast
also have "… = (x ⊔ y) ⊓ (y ⊔ -y)"
by simp
finally have "x = (x ⊓ -y) ⊔ y"
by (simp add: sup_inf_distrib2)
hence "x ≤ -y"
using
‹join_prime x›
‹y ≠ x›
‹y ≤ x›
antisym_conv
inf_le2
sup_neg_inf
unfolding join_prime_def
by blast
hence "y ≤ y ⊓ -y"
by (metis
‹x = x ⊔ y›
inf.orderE
inf_compl_bot_right
inf_sup_absorb
order_refl
sup.commute)
hence "y = ⊥"
using sup_absorb2 by fastforce
}
thus "atomic x"
using ‹join_prime x›
unfolding
atomic_def
join_prime_def
by auto
qed
text ‹ All atomic elements are disjoint. ›
lemma (in bounded_lattice_bot) atomic_disjoint:
assumes "atomic α"
and "atomic β"
shows "(α = β) ⟷ (α ⊓ β ≠ ⊥)"
proof
assume "α = β"
hence "α ⊓ β = α"
by simp
thus "α ⊓ β ≠ ⊥"
using ‹atomic α›
unfolding atomic_def
by auto
next
assume "α ⊓ β ≠ ⊥"
hence "β ≤ α ∧ α ≤ β"
by (metis
assms
atomic_def
inf_absorb2
inf_le1
inf_le2)
thus "α = β" by auto
qed
definition (in bounded_lattice_bot) atomic_elements (‹𝒜›) where
"𝒜 ≡ {a . atomic a}"
definition (in bounded_lattice_bot) join_irreducible_elements (‹𝒥›) where
"𝒥 ≡ {a . join_irreducible a}"
section ‹ Birkhoff's Representation Theorem For Finite Distributive Lattices \label{section:birkhoffs-theorem} ›
text ‹ Birkhoff's representation theorem for finite distributive
lattices follows from the fact that every non-‹⊥› element
can be represented by the join-irreducible elements beneath it. ›
text ‹ In this section we merely demonstrate the representation aspect of
Birkhoff's theorem. In \S\ref{section:isomorphism} we show this
representation is a lattice homomorphism. ›
text ‹ The fist step to representing elements is to show that there ∗‹exist›
join-irreducible elements beneath them. This is done by showing if there is
no join-irreducible element, we can make a descending chain with more elements
than the finite Boolean algebra under consideration. ›
fun (in order) descending_chain_list :: "'a list ⇒ bool" where
"descending_chain_list [] = True"
| "descending_chain_list [x] = True"
| "descending_chain_list (x # x' # xs)
= (x < x' ∧ descending_chain_list (x' # xs))"
lemma (in order) descending_chain_list_tail:
assumes "descending_chain_list (s # S)"
shows "descending_chain_list S"
using assms
by (induct S, auto)
lemma (in order) descending_chain_list_drop_penultimate:
assumes "descending_chain_list (s # s' # S)"
shows "descending_chain_list (s # S)"
using assms
by (induct S, simp, auto)
lemma (in order) descending_chain_list_less_than_others:
assumes "descending_chain_list (s # S)"
shows "∀s' ∈ set S. s < s'"
using assms
by (induct S,
auto,
simp add: descending_chain_list_drop_penultimate)
lemma (in order) descending_chain_list_distinct:
assumes "descending_chain_list S"
shows "distinct S"
using assms
by (induct S,
simp,
meson
descending_chain_list_less_than_others
descending_chain_list_tail
distinct.simps(2)
less_irrefl)
lemma (in finite_distrib_lattice) join_irreducible_lower_bound_exists:
assumes "¬ (x ≤ y)"
shows "∃ z ∈ 𝒥. z ≤ x ∧ ¬ (z ≤ y)"
proof (rule ccontr)
assume ⋆: "¬ (∃ z ∈ 𝒥. z ≤ x ∧ ¬ (z ≤ y))"
{
fix z :: 'a
assume
"z ≤ x"
"¬ (z ≤ y)"
with ⋆ obtain p q where
"p < z"
"q < z"
"p ⊔ q = z"
by (metis (full_types)
bot_least
dual_order.not_eq_order_implies_strict
join_irreducible_def'
join_irreducible_elements_def
sup_ge1
sup_ge2
mem_Collect_eq)
hence "¬ (p ≤ y) ∨ ¬ (q ≤ y)"
by (metis (full_types) ‹¬ z ≤ y› sup_least)
hence "∃ p < z. ¬ (p ≤ y)"
by (metis ‹p < z› ‹q < z›)
}
note fresh = this
{
fix n :: nat
have "∃ S . descending_chain_list S
∧ length S = n
∧ (∀s ∈ set S. s ≤ x ∧ ¬ (s ≤ y))"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case proof (cases "n = 0")
case True
hence "descending_chain_list [x]
∧ length [x] = Suc n
∧ (∀s ∈ set [x]. s ≤ x ∧ ¬ (s ≤ y))"
by (metis
Suc
assms
length_0_conv
length_Suc_conv
descending_chain_list.simps(2)
le_less set_ConsD)
then show ?thesis
by blast
next
case False
from this obtain s S where
"descending_chain_list (s # S)"
"length (s # S) = n"
"∀s ∈ set (s # S). s ≤ x ∧ ¬ (s ≤ y)"
using
Suc.hyps
length_0_conv
descending_chain_list.elims(2)
by metis
note A = this
hence "s ≤ x" "¬ (s ≤ y)" by auto
obtain s' :: 'a where
"s' < s"
"¬ (s' ≤ y)"
using
fresh [OF ‹s ≤ x› ‹¬ (s ≤ y)›]
by auto
note B = this
let ?S' = "s' # s # S"
from A and B have
"descending_chain_list ?S'"
"length ?S' = Suc n"
"∀s ∈ set ?S'. s ≤ x ∧ ¬ (s ≤ y)"
by auto
then show ?thesis by blast
qed
qed
}
from this obtain S :: "'a list" where
"descending_chain_list S"
"length S = 1 + (card (UNIV::'a set))"
by auto
hence "card (set S) = 1 + (card (UNIV::'a set))"
using descending_chain_list_distinct
distinct_card
by fastforce
hence "¬ card (set S) ≤ card (UNIV::'a set)"
by presburger
thus "False"
using card_mono finite_UNIV by blast
qed
definition (in bounded_lattice_bot)
join_irreducibles_embedding :: "'a ⇒ 'a set" (‹⦃ _ ⦄› [50]) where
"⦃ x ⦄ ≡ {a ∈ 𝒥. a ≤ x}"
text ‹ We can now show every element is exactly the suprema of the
join-irreducible elements beneath them in any distributive lattice. ›
theorem (in finite_distrib_lattice) sup_join_prime_embedding_ident:
"x = ⨆ ⦃ x ⦄"
proof -
have "∀ a ∈ ⦃ x ⦄. a ≤ x"
by (metis (no_types, lifting)
join_irreducibles_embedding_def
mem_Collect_eq)
hence "⨆ ⦃ x ⦄ ≤ x"
by (simp add: Sup_least)
moreover
{
fix y :: 'a
assume "⨆ ⦃ x ⦄ ≤ y"
have "x ≤ y"
proof (rule ccontr)
assume "¬ x ≤ y"
from this obtain a where
"a ∈ 𝒥"
"a ≤ x"
"¬ a ≤ y"
using join_irreducible_lower_bound_exists [OF ‹¬ x ≤ y›]
by metis
hence "a ∈ ⦃ x ⦄"
by (metis (no_types, lifting)
join_irreducibles_embedding_def
mem_Collect_eq)
hence "a ≤ y"
using ‹⨆⦃ x ⦄ ≤ y›
Sup_upper
order.trans
by blast
thus "False"
by (metis (full_types) ‹¬ a ≤ y›)
qed
}
ultimately show ?thesis
using antisym_conv by blast
qed
text ‹ Just as ‹x = ⨆ ⦃ x ⦄›, the reverse is also true; ‹λ x. ⦃ x ⦄›
and ‹λ S. ⨆ S› are inverses where ‹S ∈ 𝒪𝒥›, the set of downsets
in ‹Pow 𝒥›. ›
definition (in bounded_lattice_bot) down_irreducibles (‹𝒪𝒥›) where
"𝒪𝒥 ≡ { S ∈ Pow 𝒥 . (∃ x . S = ⦃ x ⦄) }"
lemma (in finite_distrib_lattice) join_irreducible_embedding_sup_ident:
assumes "S ∈ 𝒪𝒥"
shows "S = ⦃ ⨆ S ⦄"
proof -
obtain x where
"S = ⦃ x ⦄"
using
‹S ∈ 𝒪𝒥›
unfolding
down_irreducibles_def
by auto
with ‹S ∈ 𝒪𝒥› have "∀ s ∈ S. s ∈ 𝒥 ∧ s ≤ ⨆ S"
unfolding
down_irreducibles_def
Pow_def
using Sup_upper
by fastforce
hence "S ⊆ ⦃ ⨆ S ⦄"
unfolding join_irreducibles_embedding_def
by blast
moreover
{
fix y
assume
"y ∈ 𝒥"
"y ≤ ⨆ S"
have "finite S" by auto
from ‹finite S› and ‹y ≤ ⨆ S› have "∃ s ∈ S. y ≤ s"
proof (induct S rule: finite_induct)
case empty
hence "y ≤ ⊥"
by (metis Sup_empty)
then show ?case
using
‹y ∈ 𝒥›
unfolding
join_irreducible_elements_def
join_irreducible_def
by (metis (mono_tags, lifting)
le_bot
mem_Collect_eq)
next
case (insert s S)
hence "y ≤ s ∨ y ≤ ⨆ S"
using
‹y ∈ 𝒥›
unfolding
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by auto
then show ?case
by (metis (full_types)
insert.hyps(3)
insertCI)
qed
hence "y ≤ x"
by (metis (no_types, lifting)
‹S = ⦃ x ⦄›
join_irreducibles_embedding_def
order_trans
mem_Collect_eq)
hence "y ∈ S"
by (metis (no_types, lifting)
‹S = ⦃ x ⦄›
‹y ∈ 𝒥›
join_irreducibles_embedding_def
mem_Collect_eq)
}
hence "⦃ ⨆ S ⦄ ⊆ S"
unfolding
join_irreducibles_embedding_def
by blast
ultimately show ?thesis by auto
qed
text ‹ Given that ‹λ x. ⦃ x ⦄› has a left and right inverse, we can show
it is a ∗‹bijection›. ›
text ‹ The bijection below is recognizable as a form of ∗‹Birkhoff's Representation Theorem›
for finite distributive lattices. ›
theorem (in finite_distrib_lattice) birkhoffs_theorem:
"bij_betw (λ x. ⦃ x ⦄) UNIV 𝒪𝒥"
unfolding bij_betw_def
proof
{
fix x y
assume "⦃ x ⦄ = ⦃ y ⦄"
hence "⨆ ⦃ x ⦄ = ⨆ ⦃ y ⦄"
by simp
hence "x = y"
using sup_join_prime_embedding_ident
by auto
}
thus "inj (λ x. ⦃ x ⦄)"
unfolding inj_def
by auto
next
show "range (λ x. ⦃ x ⦄) = 𝒪𝒥"
unfolding
down_irreducibles_def
join_irreducibles_embedding_def
by auto
qed
section ‹ Finite Ditributive Lattice Isomorphism \label{section:isomorphism} ›
text ‹ The form of Birkhoff's theorem presented in \S\ref{section:birkhoffs-theorem}
simply gave a bijection between a finite distributive lattice and the
downsets of its join-irreducible elements. This relationship can be
extended to a full-blown ∗‹lattice homomorphism›. In particular
we have the following properties:
▪ ‹⊥› and ‹⊤› are preserved; specifically ‹⦃ ⊥ ⦄ = {}› and
‹⦃ ⊤ ⦄ = 𝒥›.
▪ Order is preserved: ‹x ≤ y = (⦃ x ⦄ ⊆ ⦃ y ⦄)›.
▪ ‹λ x . ⦃ x ⦄› is a lower complete semi-lattice homomorphism, mapping
‹⦃ ⨆ X ⦄ = (⋃ x ∈ X . ⦃ x ⦄)›.
▪ In addition to preserving arbitrary joins, ‹λ x . ⦃ x ⦄› is a
lattice homomorphism, since it also preserves finitary meets with
‹ ⦃ x ⊓ y ⦄ = ⦃ x ⦄ ∩ ⦃ y ⦄ ›. Arbitrary meets are also preserved,
but relative to a top element ‹𝒥›, or in other words
‹ ⦃ ⨅ X ⦄ = 𝒥 ∩ (⋂ x ∈ X. ⦃ x ⦄) ›.
▪ In the case of a Boolean algebra, complementation corresponds to
relative set complementation via ‹⦃ - x ⦄ = 𝒥 - ⦃ x ⦄›.
›
lemma (in finite_distrib_lattice) join_irreducibles_bot:
"⦃ ⊥ ⦄ = {}"
unfolding
join_irreducibles_embedding_def
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by (simp add: bot_unique)
lemma (in finite_distrib_lattice) join_irreducibles_top:
"⦃ ⊤ ⦄ = 𝒥"
unfolding
join_irreducibles_embedding_def
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by auto
lemma (in finite_distrib_lattice) join_irreducibles_order_isomorphism:
"x ≤ y = (⦃ x ⦄ ⊆ ⦃ y ⦄)"
by (rule iffI,
metis (mono_tags, lifting)
join_irreducibles_embedding_def
order_trans
mem_Collect_eq
subsetI,
metis (full_types)
Sup_subset_mono
sup_join_prime_embedding_ident)
lemma (in finite_distrib_lattice) join_irreducibles_join_homomorphism:
"⦃ x ⊔ y ⦄ = ⦃ x ⦄ ∪ ⦃ y ⦄"
proof
show "⦃ x ⊔ y ⦄ ⊆ ⦃ x ⦄ ∪ ⦃ y ⦄"
unfolding
join_irreducibles_embedding_def
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by blast
next
show "⦃ x ⦄ ∪ ⦃ y ⦄ ⊆ ⦃ x ⊔ y ⦄"
unfolding
join_irreducibles_embedding_def
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
using
le_supI1
sup.absorb_iff1
sup.assoc
by force
qed
lemma (in finite_distrib_lattice) join_irreducibles_sup_homomorphism:
"⦃ ⨆ X ⦄ = (⋃ x ∈ X . ⦃ x ⦄)"
proof -
have "finite X"
by simp
thus ?thesis
proof (induct X rule: finite_induct)
case empty
then show ?case by (simp add: join_irreducibles_bot)
next
case (insert x X)
then show ?case by (simp add: join_irreducibles_join_homomorphism)
qed
qed
lemma (in finite_distrib_lattice) join_irreducibles_meet_homomorphism:
"⦃ x ⊓ y ⦄ = ⦃ x ⦄ ∩ ⦃ y ⦄"
unfolding
join_irreducibles_embedding_def
by auto
text ‹ Arbitrary meets are also preserved, but relative to a top element ‹𝒥›. ›
lemma (in finite_distrib_lattice) join_irreducibles_inf_homomorphism:
"⦃ ⨅ X ⦄ = 𝒥 ∩ (⋂ x ∈ X. ⦃ x ⦄)"
proof -
have "finite X"
by simp
thus ?thesis
proof (induct X rule: finite_induct)
case empty
then show ?case by (simp add: join_irreducibles_top)
next
case (insert x X)
then show ?case by (simp add: join_irreducibles_meet_homomorphism, blast)
qed
qed
text ‹ Finally, we show that complementation is preserved. ›
text ‹ To begin, we define the class of finite Boolean algebras.
This class is simply an extension of @{class boolean_algebra},
extended with \<^term>‹finite UNIV› as per the axiom class @{class finite}. We also
also extend the language of the class with ∗‹infima› and ∗‹suprema›
(i.e. ‹⨅ A› and ‹⨆ A› respectively). ›
class finite_boolean_algebra = boolean_algebra + finite + Inf + Sup +
assumes Inf_def: "⨅ A = Finite_Set.fold (⊓) ⊤ A"
assumes Sup_def: "⨆ A = Finite_Set.fold (⊔) ⊥ A"
begin
text ‹ Finite Boolean algebras are trivially a subclass of finite
distributive lattices, which are necessarily ∗‹complete›. ›
subclass finite_distrib_lattice_complete
using
Inf_fin.coboundedI
Sup_fin.coboundedI
finite_UNIV
le_bot
top_unique
Inf_def
Sup_def
by (unfold_locales, blast, fastforce+)
subclass bounded_distrib_lattice_bot
by (unfold_locales, metis sup_inf_distrib1)
end
lemma (in finite_boolean_algebra) join_irreducibles_complement_homomorphism:
"⦃ - x ⦄ = 𝒥 - ⦃ x ⦄"
proof
show "⦃ - x ⦄ ⊆ 𝒥 - ⦃ x ⦄"
proof
fix j
assume "j ∈ ⦃ - x ⦄"
hence "j ∉ ⦃ x ⦄"
unfolding
join_irreducibles_embedding_def
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by (metis
(mono_tags, lifting)
CollectD
bot_unique
inf.boundedI
inf_compl_bot)
thus "j ∈ 𝒥 - ⦃ x ⦄"
using ‹j ∈ ⦃ - x ⦄›
unfolding
join_irreducibles_embedding_def
by blast
qed
next
show "𝒥 - ⦃ x ⦄ ⊆ ⦃ - x ⦄"
proof
fix j
assume "j ∈ 𝒥 - ⦃ x ⦄"
hence "j ∈ 𝒥" and "¬ j ≤ x"
unfolding join_irreducibles_embedding_def
by blast+
moreover have "j ≤ x ⊔ -x"
by auto
ultimately have "j ≤ -x"
unfolding
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by blast
thus "j ∈ ⦃ - x ⦄"
unfolding join_irreducibles_embedding_def
using ‹j ∈ 𝒥›
by auto
qed
qed
section ‹ Cardinality ›
text ‹ Another consequence of Birkhoff's theorem from \S\ref{section:birkhoffs-theorem}
is that every finite Boolean algebra has a cardinality which is
a power of two. This gives a bound on the number of
atoms/join-prime/irreducible elements, which must be logarithmic in
the size of the finite Boolean algebra they belong to. ›
text ‹ We first show that ‹𝒪𝒥›, the downsets of the join-irreducible elements
‹𝒥›, are the same as the powerset of ‹𝒥› in any finite Boolean algebra. ›
lemma (in finite_boolean_algebra) 𝒪𝒥_is_Pow_𝒥:
"𝒪𝒥 = Pow 𝒥"
proof
show "𝒪𝒥 ⊆ Pow 𝒥"
unfolding down_irreducibles_def
by auto
next
show "Pow 𝒥 ⊆ 𝒪𝒥"
proof (rule ccontr)
assume "¬ Pow 𝒥 ⊆ 𝒪𝒥"
from this obtain S where
"S ⊆ 𝒥"
"∀ x. S ≠ {a ∈ 𝒥. a ≤ x}"
unfolding
down_irreducibles_def
join_irreducibles_embedding_def
by auto
hence "S ≠ {a ∈ 𝒥. a ≤ ⨆ S}"
by auto
moreover
have "∀ s ∈ S . s ∈ 𝒥 ∧ s ≤ ⨆ S"
by (metis (no_types, lifting)
‹S ⊆ 𝒥›
Sup_upper subsetD)
hence "S ⊆ {a ∈ 𝒥. a ≤ ⨆ S}"
by (metis (mono_tags, lifting) Ball_Collect)
ultimately have "∃ y ∈ 𝒥 . y ≤ ⨆ S ∧ y ∉ S"
by (metis (mono_tags, lifting)
mem_Collect_eq
subsetI
subset_antisym)
moreover
{
fix y
assume
"y ∈ 𝒥"
"y ≤ ⨆ S"
from
finite [of S]
‹y ≤ ⨆ S›
‹S ⊆ 𝒥›
have "y ∈ S"
proof (induct S rule: finite_induct)
case empty
hence "y ≤ ⊥"
by (metis (full_types) local.Sup_empty)
then show ?case
using ‹y ∈ 𝒥›
unfolding
join_irreducible_elements_def
join_irreducible_def
by (metis (mono_tags, lifting)
le_bot
mem_Collect_eq)
next
case (insert s S)
hence "y ≤ s ∨ y ≤ ⨆ S"
using ‹y ∈ 𝒥›
unfolding
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by simp
moreover
{
assume "y ≤ s"
have "atomic s"
by (metis in_mono
insert.prems(2)
insertCI
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_is_atomic
mem_Collect_eq)
hence "y = s"
by (metis (no_types, lifting)
‹y ∈ 𝒥›
‹y ≤ s›
atomic_def
join_irreducible_def
join_irreducible_elements_def
mem_Collect_eq)
}
ultimately show ?case
by (metis
insert.prems(2)
insert_iff
insert_subset
insert(3))
qed
}
ultimately show False by auto
qed
qed
lemma (in finite_boolean_algebra) UNIV_card:
"card (UNIV::'a set) = card (Pow 𝒥)"
using
bij_betw_same_card [where f="λx. ⦃ x ⦄"]
birkhoffs_theorem
unfolding
𝒪𝒥_is_Pow_𝒥
by blast
lemma finite_Pow_card:
assumes "finite X"
shows "card (Pow X) = 2 powr (card X)"
using assms
proof (induct X rule: finite_induct)
case empty
then show ?case by fastforce
next
case (insert x X)
have "0 ≤ (2 :: real)" by auto
hence two_powr_one: "(2 :: real) = 2 powr 1" by fastforce
have "bij_betw (λ x. fst x ∪ snd x) ({{},{x}} × Pow X) (Pow (insert x X))"
unfolding bij_betw_def
proof
{
fix y z
assume
"y ∈ {{}, {x}} × Pow X"
"z ∈ {{}, {x}} × Pow X"
"fst y ∪ snd y = fst z ∪ snd z"
(is "?Uy = ?Uz")
hence
"x ∉ snd y"
"x ∉ snd z"
"fst y = {x} ∨ fst y = {}"
"fst z = {x} ∨ fst z = {}"
using insert.hyps(2) by auto
hence
"x ∈ ?Uy ⟷ fst y = {x}"
"x ∈ ?Uz ⟷ fst z = {x}"
"x ∉ ?Uy ⟷ fst y = {}"
"x ∉ ?Uz ⟷ fst z = {}"
"snd y = ?Uy - {x}"
"snd z = ?Uz - {x}"
by auto
hence
"x ∈ ?Uy ⟷ y = ({x}, ?Uy - {x})"
"x ∈ ?Uz ⟷ z = ({x}, ?Uz - {x})"
"x ∉ ?Uy ⟷ y = ({}, ?Uy - {x})"
"x ∉ ?Uz ⟷ z = ({}, ?Uz - {x})"
by (metis fst_conv prod.collapse)+
hence "y = z"
using ‹?Uy = ?Uz›
by metis
}
thus "inj_on (λx. fst x ∪ snd x) ({{}, {x}} × Pow X)"
unfolding inj_on_def
by auto
next
show "(λx. fst x ∪ snd x) ` ({{}, {x}} × Pow X) = Pow (insert x X)"
proof (intro equalityI subsetI)
fix y
assume "y ∈ (λx. fst x ∪ snd x) ` ({{}, {x}} × Pow X)"
from this obtain z where
"z ∈ ({{}, {x}} × Pow X)"
"y = fst z ∪ snd z"
by auto
hence
"snd z ⊆ X"
"fst z ⊆ insert x X"
using SigmaE by auto
thus "y ∈ Pow (insert x X)"
using ‹y = fst z ∪ snd z› by blast
next
fix y
assume "y ∈ Pow (insert x X)"
let ?z = "(if x ∈ y then {x} else {}, y - {x})"
have "?z ∈ ({{}, {x}} × Pow X)"
using ‹y ∈ Pow (insert x X)› by auto
moreover have "(λx. fst x ∪ snd x) ?z = y"
by auto
ultimately show "y ∈ (λx. fst x ∪ snd x) ` ({{}, {x}} × Pow X)"
by blast
qed
qed
hence "card (Pow (insert x X)) = card ({{},{x}} × Pow X)"
using bij_betw_same_card by fastforce
also have "… = 2 * card (Pow X)"
by (simp add: insert.hyps(1))
also have "… = 2 * (2 powr (card X))"
by (simp add: insert.hyps(3))
also have "… = (2 powr 1) * 2 powr (card X)"
using two_powr_one
by fastforce
also have "… = 2 powr (1 + card X)"
by (simp add: powr_add)
also have "… = 2 powr (card (insert x X))"
by (simp add: insert.hyps(1) insert.hyps(2))
finally show ?case .
qed
lemma (in finite_boolean_algebra) UNIV_card_powr_2:
"card (UNIV::'a set) = 2 powr (card 𝒥)"
using
finite [of 𝒥]
finite_Pow_card [of 𝒥]
UNIV_card
by linarith
lemma (in finite_boolean_algebra) join_irreducibles_card_log_2:
"card 𝒥 = log 2 (card (UNIV :: 'a set))"
proof (cases "card (UNIV :: 'a set) = 1")
case True
hence "∃ x :: 'a. UNIV = {x}"
using card_1_singletonE by blast
hence "∀ x y :: 'a. x ∈ UNIV ⟶ y ∈ UNIV ⟶ x = y"
by (metis (mono_tags) singletonD)
hence "∀ x y :: 'a. x = y"
by blast
hence "∀ x. x = ⊥"
by blast
hence "𝒥 = {}"
unfolding
join_irreducible_elements_def
join_irreducible_is_join_prime
join_prime_def
by blast
hence "card 𝒥 = (0 :: real)"
by simp
moreover
have "log 2 (card (UNIV :: 'a set)) = 0"
by (simp add: True)
ultimately show ?thesis by auto
next
case False
hence "0 < 2 powr (card 𝒥)" "2 powr (card 𝒥) ≠ 1"
using finite_UNIV_card_ge_0 finite UNIV_card_powr_2
by (simp, linarith)
hence "log 2 (2 powr (card 𝒥)) = card 𝒥"
by simp
then show ?thesis
using UNIV_card_powr_2
by simp
qed
end