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