Theory Generated_Boolean_Algebra
theory Generated_Boolean_Algebra
imports Main
begin
section‹Generated Boolean Algebras of Sets›
subsection‹Definitions and Basic Lemmas›
lemma equalityI':
assumes "⋀x. x ∈ A ⟹ x ∈ B"
assumes "⋀x. x ∈ B ⟹ x ∈ A"
shows "A = B"
using assms by blast
lemma equalityI'':
assumes "⋀x. A x ⟹ B x"
assumes "⋀x. B x ⟹ A x"
shows "{x. A x} = {x. B x}"
using assms by blast
lemma SomeE:
assumes "a = (SOME x. P x)"
assumes "P c"
shows "P a"
using assms by (meson verit_sko_ex)
lemma SomeE':
assumes "a = (SOME x. P x)"
assumes "∃ x. P x"
shows "P a"
using assms by (meson verit_sko_ex)
section‹Basic notions about boolean algebras over a set ‹S›, generated by a set of generators ‹B››
text‹Note that the generators ‹B› need not be subsets of the set ‹S››
inductive_set gen_boolean_algebra
for S and B where
universe: "S ∈ gen_boolean_algebra S B"
| generator: "A ∈ B ⟹ A ∩ S ∈ gen_boolean_algebra S B"
| union: "⟦ A ∈ gen_boolean_algebra S B; C ∈ gen_boolean_algebra S B⟧ ⟹ A ∪ C ∈ gen_boolean_algebra S B"
| complement: "A ∈ gen_boolean_algebra S B ⟹ S - A ∈ gen_boolean_algebra S B"
lemma gen_boolean_algebra_subset:
shows "A ∈ gen_boolean_algebra S B ⟹ A ⊆ S"
apply(induction A rule: gen_boolean_algebra.induct)
apply blast
apply blast
apply blast
by blast
lemma gen_boolean_algebra_intersect:
assumes "A ∈ gen_boolean_algebra S B"
assumes "C ∈ gen_boolean_algebra S B"
shows "A ∩ C ∈ gen_boolean_algebra S B"
proof-
have 0: "S - A ∈ gen_boolean_algebra S B"
using assms(1) gen_boolean_algebra.complement by blast
have 1: "S - C ∈ gen_boolean_algebra S B"
using assms(2) gen_boolean_algebra.complement by blast
have 2: "(S - A) ∪ (S - C) ∈ gen_boolean_algebra S B"
using "0" "1" gen_boolean_algebra.union by blast
have "S - (A ∩ C) ∈ gen_boolean_algebra S B"
by (simp add: 2 Diff_Int)
then have 3: "S - (S - (A ∩ C)) ∈ gen_boolean_algebra S B"
using gen_boolean_algebra.complement
by blast
have "A ∩ C ⊆ S"
using assms(1) gen_boolean_algebra_subset
by blast
then show ?thesis
using 3
by (metis "0" Diff_partition Un_subset_iff assms(1) double_diff gen_boolean_algebra_subset)
qed
lemma gen_boolean_algebra_diff:
assumes "A ∈ gen_boolean_algebra S B"
assumes "C ∈ gen_boolean_algebra S B"
shows "A - C ∈ gen_boolean_algebra S B"
proof-
have "A - C = A ∩ (S - C)"
by (metis Int_Diff assms(1) gen_boolean_algebra_subset inf_absorb1)
then show ?thesis
by (metis assms(1) assms(2) gen_boolean_algebra.complement gen_boolean_algebra_intersect)
qed
lemma gen_boolean_algebra_diff_eq:
assumes "A ∈ gen_boolean_algebra S B"
assumes "C ∈ gen_boolean_algebra S B"
shows "A - C = A ∩ (S - C)"
by (metis Int_Diff assms(1) gen_boolean_algebra_subset inf_absorb1)
lemma gen_boolean_algebra_finite_union:
assumes "⋀a. a ∈ A ⟹ a ∈ gen_boolean_algebra S B"
assumes "finite A"
shows "⋃A ∈ gen_boolean_algebra S B"
proof-
have "(∀a ∈ A. a ∈ gen_boolean_algebra S B) ⟶ ⋃A ∈ gen_boolean_algebra S B"
apply(rule finite.induct[of A])
apply (simp add: assms(2); fail)
apply (metis DiffE Union_empty ex_in_conv gen_boolean_algebra.simps)
by (metis Union_insert gen_boolean_algebra.simps insert_iff)
then show ?thesis using assms by blast
qed
lemma gen_boolean_algebra_finite_intersection:
assumes "⋀a. a ∈ A ⟹ a ∈ gen_boolean_algebra S B"
assumes "finite A"
assumes "A ≠ {}"
shows "⋂A ∈ gen_boolean_algebra S B"
proof-
have "(∀a ∈ A. a ∈ gen_boolean_algebra S B) ∧ A ≠ {} ⟶ ⋂A ∈ gen_boolean_algebra S B"
apply(rule finite.induct[of A])
apply (simp add: assms(2))
apply force
using gen_boolean_algebra_intersect by auto
then show ?thesis using assms by blast
qed
lemma gen_boolean_algebra_generators:
assumes "⋀b. b ∈ B ⟹ b ⊆ S"
assumes "b ∈ B"
shows "b ∈ gen_boolean_algebra S B"
unfolding gen_boolean_algebra.simps[of b] using assms(1)[of b] assms(2) by blast
lemma gen_boolean_algebra_generator_subset:
assumes "A ∈ gen_boolean_algebra S As"
assumes "As ⊆ Bs"
shows "A ∈ gen_boolean_algebra S Bs"
apply(rule gen_boolean_algebra.induct[of A S As])
using assms(1) apply blast
apply (simp add: gen_boolean_algebra.intros(1); fail)
apply (meson Set.basic_monos(7) assms(2) gen_boolean_algebra.intros(2))
using gen_boolean_algebra.intros(3) apply blast
using gen_boolean_algebra.intros(4) by blast
lemma gen_boolean_algebra_generators_union:
assumes "A ∈ gen_boolean_algebra S As"
assumes "C ∈ gen_boolean_algebra S Cs"
shows "A ∪ C ∈ gen_boolean_algebra S (As ∪ Cs)"
apply(rule gen_boolean_algebra.induct[of C S Cs])
using assms apply blast
apply(rule gen_boolean_algebra.union)
apply(rule gen_boolean_algebra_generator_subset[of _ _ As], rule assms, blast)
apply(rule gen_boolean_algebra.universe)
apply(rule gen_boolean_algebra.union)
apply(rule gen_boolean_algebra_generator_subset[of _ _ As], rule assms, blast)
apply(rule gen_boolean_algebra.generator, blast)
apply(rule gen_boolean_algebra.union)
apply(rule gen_boolean_algebra_generator_subset[of _ _ As], rule assms, blast)
apply(rule gen_boolean_algebra.union)
apply(rule gen_boolean_algebra_generator_subset[of _ _ Cs], blast, blast)
apply(rule gen_boolean_algebra_generator_subset[of _ _ Cs], blast, blast)
apply(rule gen_boolean_algebra.union)
apply(rule gen_boolean_algebra_generator_subset[of _ _ As], rule assms, blast)
apply(rule gen_boolean_algebra_generator_subset[of _ _ Cs])
apply(rule gen_boolean_algebra_diff)
apply(rule gen_boolean_algebra.universe)
apply blast
by blast
lemma gen_boolean_algebra_finite_gen_wits:
assumes "A ∈ gen_boolean_algebra S B"
shows "∃ Bs. finite Bs ∧ Bs ⊆ B ∧ A ∈ gen_boolean_algebra S Bs"
proof(rule gen_boolean_algebra.induct[of A S B])
show " A ∈ gen_boolean_algebra S B"
using assms by blast
show "∃Bs. finite Bs ∧ Bs ⊆ B ∧ S ∈ gen_boolean_algebra S Bs"
using gen_boolean_algebra.universe[of S "{}"]
by blast
show "⋀A. A ∈ B ⟹ ∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∩ S ∈ gen_boolean_algebra S Bs"
proof- fix A assume A: "A ∈ B"
have 0: "{A} ⊆ B"
using A by blast
show "∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∩ S ∈ gen_boolean_algebra S Bs"
using gen_boolean_algebra.generator[of A "{A}" S] 0
by (meson finite.emptyI finite.insertI singletonI)
qed
show "⋀A C. A ∈ gen_boolean_algebra S B ⟹
∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∈ gen_boolean_algebra S Bs ⟹
C ∈ gen_boolean_algebra S B ⟹
∃Bs. finite Bs ∧ Bs ⊆ B ∧ C ∈ gen_boolean_algebra S Bs ⟹ ∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∪ C ∈ gen_boolean_algebra S Bs"
proof- fix A C
assume A: "A ∈ gen_boolean_algebra S B"
"∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∈ gen_boolean_algebra S Bs"
"C ∈ gen_boolean_algebra S B"
"∃Bs. finite Bs ∧ Bs ⊆ B ∧ C ∈ gen_boolean_algebra S Bs"
obtain As where As_def: "finite As ∧ As ⊆ B ∧ A ∈ gen_boolean_algebra S As"
using A by blast
obtain Cs where Cs_def: "finite Cs ∧ Cs ⊆ B ∧ C ∈ gen_boolean_algebra S Cs"
using A by blast
obtain Bs where Bs_def: "Bs = As ∪ Cs"
by blast
have Bs_sub: "Bs ⊆ B"
unfolding Bs_def using As_def Cs_def by blast
have 0: " A ∪ C ∈ gen_boolean_algebra S Bs"
unfolding Bs_def
apply(rule gen_boolean_algebra_generators_union)
using As_def apply blast
using Cs_def by blast
have 1: "finite Bs"
unfolding Bs_def using As_def Cs_def by blast
show " ∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∪ C ∈ gen_boolean_algebra S Bs"
using Bs_sub 0 1 by blast
qed
show "⋀A. A ∈ gen_boolean_algebra S B ⟹
∃Bs. finite Bs ∧ Bs ⊆ B ∧ A ∈ gen_boolean_algebra S Bs ⟹ ∃Bs. finite Bs ∧ Bs ⊆ B ∧ S - A ∈ gen_boolean_algebra S Bs"
using gen_boolean_algebra.complement by blast
qed
lemma gen_boolean_algebra_univ_mono:
assumes "A ∈ gen_boolean_algebra S B"
shows "gen_boolean_algebra A B ⊆ gen_boolean_algebra S B "
proof(rule subsetI) fix x assume A: "x ∈ gen_boolean_algebra A B"
obtain a where a_def: "a = A"
by blast
have 0: "a ∈ gen_boolean_algebra S B"
unfolding a_def using assms by blast
have 1: "a = A ∩ S"
using assms gen_boolean_algebra_subset unfolding a_def by blast
show "x ∈ gen_boolean_algebra S B "
apply(rule gen_boolean_algebra.induct[of x a B])
using A a_def apply blast apply(rule 0)
apply (metis 1 Int_left_commute assms gen_boolean_algebra.intros(2) gen_boolean_algebra_intersect)
apply(rule gen_boolean_algebra.union, blast, blast)
apply(rule gen_boolean_algebra_diff)
apply(rule 0)
by blast
qed
text‹
The boolean algebra generated by a collection of elements in another algebra is contained
in the original algebra:
›
lemma gen_boolean_algebra_subalgebra:
assumes "Xs ⊆ gen_boolean_algebra S B"
shows "gen_boolean_algebra S Xs ⊆ gen_boolean_algebra S B"
proof fix x assume A: "x ∈ gen_boolean_algebra S Xs"
show "x ∈ gen_boolean_algebra S B "
apply(rule gen_boolean_algebra.induct[of x S Xs])
apply (simp add: A; fail)
apply (simp add: gen_boolean_algebra.universe; fail)
using assms gen_boolean_algebra.universe gen_boolean_algebra_intersect apply blast
apply (simp add: gen_boolean_algebra.union; fail)
by (simp add: gen_boolean_algebra.complement)
qed
lemma gen_boolean_algebra_idempotent:
assumes "S = ⋃ Xs"
shows "gen_boolean_algebra S (gen_boolean_algebra S Xs) = (gen_boolean_algebra S Xs)"
apply(rule equalityI)
apply(rule subsetI)
apply (meson equalityD2 gen_boolean_algebra_subalgebra in_mono)
apply(rule subsetI)
by (metis gen_boolean_algebra.simps gen_boolean_algebra_subset inf.absorb1)
text‹We can always replace the set of generators ‹Xs› with their intersections with the universe
set ‹S›, and obtain the same algebra.›
lemma gen_boolean_algebra_restrict_generators:
"gen_boolean_algebra S Xs =gen_boolean_algebra S ((∩) S ` Xs)"
proof(rule equalityI')
fix x assume A: "x ∈ gen_boolean_algebra S Xs"
show "x ∈ gen_boolean_algebra S ((∩) S ` Xs)"
apply(rule gen_boolean_algebra.induct[of x S Xs], rule A, rule gen_boolean_algebra.universe)
apply (metis gen_boolean_algebra.generator image_eqI inf.right_idem inf_commute)
apply(rule gen_boolean_algebra.union, blast, blast)
by(rule gen_boolean_algebra_diff, rule gen_boolean_algebra.universe, blast)
next
fix x assume A: "x ∈ gen_boolean_algebra S ((∩) S ` Xs)"
show "x ∈ gen_boolean_algebra S Xs"
apply(rule gen_boolean_algebra.induct[of x S "(∩) S ` Xs"], rule A, rule gen_boolean_algebra.universe,
rule gen_boolean_algebra_intersect )
using gen_boolean_algebra.generator[of _ Xs S]
apply (metis (no_types, lifting) Int_commute image_iff)
apply(rule gen_boolean_algebra.universe)
apply(rule gen_boolean_algebra.union, blast, blast)
by(rule gen_boolean_algebra_diff, rule gen_boolean_algebra.universe, blast)
qed
text‹Adding a generator to a generated boolean algebra is redundant if the generator already
lies in the algebra.›
lemma add_generators:
assumes "A ∈ gen_boolean_algebra S Xs"
shows "gen_boolean_algebra S Xs = gen_boolean_algebra S (insert A Xs)"
proof(rule equalityI')
fix x assume A: "x ∈ gen_boolean_algebra S Xs"
show "x ∈ gen_boolean_algebra S (insert A Xs)"
apply(rule gen_boolean_algebra.induct[of x S Xs], rule A, rule gen_boolean_algebra.universe)
apply(rule gen_boolean_algebra.generator, blast)
apply(rule gen_boolean_algebra.union, blast,blast)
by(rule gen_boolean_algebra_diff, rule gen_boolean_algebra.universe, blast)
next
fix x assume A: "x ∈ gen_boolean_algebra S (insert A Xs)"
show "x ∈ gen_boolean_algebra S Xs"
apply(rule gen_boolean_algebra.induct[of x S "insert A Xs"], rule A, rule gen_boolean_algebra.universe)
using assms gen_boolean_algebra.generator[of _ Xs S]
using gen_boolean_algebra.universe gen_boolean_algebra_intersect apply blast
apply(rule gen_boolean_algebra.union, blast, blast)
by(rule gen_boolean_algebra_diff, rule gen_boolean_algebra.universe, blast)
qed
subsection‹Turning a Family of Sets into a Family of Disjoint Sets›
text‹
This section outlines the standard construction where sets $A_0, \dots, A_n$ are replaced by sets
$A_0, A_1 - A_0, A_2 - (A_0 \cup A_1), ..., A_n - (\bigcup \limits_{i = 0}^{n-1} A_i)$ to obtain
a disjoint family of the same cardinality.
›
fun rec_disjointify where
"rec_disjointify 0 f = {}"|
"rec_disjointify (Suc m) f = insert (f m - ⋃ (rec_disjointify m f)) (rec_disjointify m f)"
lemma card_of_rec_disjointify:
"card (rec_disjointify m f) ≤ m"
apply(induction m) unfolding rec_disjointify.simps
apply simp
by (metis Suc_le_mono card.infinite card_insert_disjoint finite_insert insert_absorb le_SucI)
lemma rec_disjointify_finite:
"finite (rec_disjointify m f)"
apply(induction m)
unfolding rec_disjointify.simps by auto
lemma rec_disjointify_in_gen_boolean_algebra:
assumes "f ` {..<m} ⊆ gen_boolean_algebra S B"
shows "rec_disjointify m f ⊆ gen_boolean_algebra S B"
proof-
have "⋀k. k ≤ m ⟶ rec_disjointify k f ⊆ gen_boolean_algebra S B"
proof- fix k show "k ≤ m ⟶ rec_disjointify k f ⊆ gen_boolean_algebra S B"
apply(induction k) unfolding rec_disjointify.simps(1) using assms apply blast
proof fix k
assume IH: " k ≤ m ⟶ rec_disjointify k f ⊆ gen_boolean_algebra S B"
"Suc k ≤ m"
then have 0: "rec_disjointify k f ⊆ gen_boolean_algebra S B"
by (simp add: IH(2))
have 1: "finite (rec_disjointify k f )"
using rec_disjointify_finite by blast
have 2: "f k ∈ gen_boolean_algebra S B"
using IH(2) assms
by (simp add: image_subset_iff)
show "rec_disjointify (Suc k) f ⊆ gen_boolean_algebra S B"
using 0 1 2 unfolding rec_disjointify.simps
by (simp add: gen_boolean_algebra_diff gen_boolean_algebra_finite_union subset_iff)
qed
qed
thus ?thesis by blast
qed
lemma rec_disjointify_union:
"⋃ (rec_disjointify m f) = (⋃ i ∈ {..<m}. f i)"
apply(induction m)
apply simp unfolding rec_disjointify.simps insert_def
apply(rule equalityI, rule subsetI)
apply (simp add: lessThan_Suc; fail)
apply(rule subsetI)
by (simp add: lessThan_Suc)
definition enum_rec_disjointify where
"enum_rec_disjointify f m = f m - ⋃ (rec_disjointify m f)"
lemma rec_disjointify_as_enum_rec_disjointify_image:
"rec_disjointify m f = enum_rec_disjointify f ` {..<m}"
apply(induction m)
unfolding rec_disjointify.simps
apply (simp; fail)
unfolding enum_rec_disjointify_def
using lessThan_Suc by auto
lemma enum_rec_disjointify_subset:
"enum_rec_disjointify f m ⊆ f m"
unfolding enum_rec_disjointify_def
by auto
lemma enum_rec_disjointify_disjoint:
assumes "k < m"
shows "enum_rec_disjointify f m ∩ enum_rec_disjointify f k = {}"
proof-
have "enum_rec_disjointify f k ⊆ ⋃ (rec_disjointify m f)"
unfolding rec_disjointify_union
using assms enum_rec_disjointify_subset by fastforce
thus ?thesis
unfolding enum_rec_disjointify_def
by auto
qed
lemma enum_rec_disjointify_disjoint':
assumes "k ≠ m"
shows "enum_rec_disjointify f m ∩ enum_rec_disjointify f k = {}"
apply(cases "k < m") using enum_rec_disjointify_disjoint[of k m f]
apply simp
using assms enum_rec_disjointify_disjoint[of m k f] by auto
lemma rec_disjointify_is_disjoint:
assumes "A ∈ rec_disjointify m f"
assumes "B ∈ rec_disjointify m f"
assumes "A ≠ B"
shows "A ∩ B = {}"
using rec_disjointify_as_enum_rec_disjointify_image enum_rec_disjointify_disjoint' assms
by (smt image_iff)
definition enumerates where
"enumerates A f ≡ finite A ∧ A = f ` {..< (card A)} ∧ inj_on f {..< (card A)}"
lemma finite_imp_exists_enumeration:
assumes "finite A"
shows "∃f. enumerates A f"
unfolding enumerates_def
using assms finite_imp_nat_seg_image_inj_on[of A]
by (metis card_Collect_less_nat card_image lessThan_def)
lemma enumeratesE:
assumes "enumerates A f"
shows "finite A" "A = f ` {..< card A}" "inj_on f {..< card A}"
using assms unfolding enumerates_def apply blast
using assms unfolding enumerates_def apply blast
using assms unfolding enumerates_def by blast
lemma rec_disjointify_finite_set:
assumes "enumerates A f"
shows "⋃ (rec_disjointify (card A) f) = ⋃ A"
unfolding rec_disjointify_union[of "card A" f]
using enumeratesE[of A f] assms by auto
definition enumerate where
"enumerate A = (SOME f. enumerates A f)"
lemma enumerate_enumerates:
assumes "finite A"
shows "enumerates A (enumerate A)"
unfolding enumerate_def using finite_imp_exists_enumeration assms
by (simp add: finite_imp_exists_enumeration some_eq_ex)
lemma enumerateE:
assumes "finite A"
assumes "a ∈ A"
shows "∃ i < card A. a = (enumerate A) i"
using enumerate_enumerates[of A] enumeratesE[of A] assms by blast
definition disjointify where
"disjointify As = rec_disjointify (card As) (enumerate As)"
lemma disjointify_is_disjoint:
assumes "finite As"
assumes "A ∈ disjointify As"
assumes "B ∈ disjointify As"
assumes "A ≠ B"
shows "A ∩ B = {}"
using assms rec_disjointify_is_disjoint[of A _ _ B] unfolding disjointify_def
by simp
lemma disjointify_union:
assumes "finite As"
shows "⋃ (disjointify As) = ⋃ As"
using assms
by (simp add: disjointify_def enumerate_enumerates rec_disjointify_finite_set)
lemma disjointify_gen_boolean_algebra:
assumes "finite As"
assumes "As ⊆ gen_boolean_algebra S B"
shows " disjointify As ⊆ gen_boolean_algebra S B"
using assms unfolding disjointify_def
by (metis enumerate_enumerates enumeratesE(2) rec_disjointify_in_gen_boolean_algebra)
lemma disjointify_finite:
assumes "finite As"
shows "finite (disjointify As)"
using assms unfolding disjointify_def
by (simp add: rec_disjointify_finite)
lemma disjointify_card:
assumes "finite As"
shows"card (disjointify As) ≤ card As"
by (simp add: card_of_rec_disjointify disjointify_def)
lemma disjointify_subset:
assumes "finite As"
assumes "A ∈ disjointify As"
shows "∃B ∈ As. A ⊆ B"
using assms enum_rec_disjointify_subset enumerate_enumerates enumeratesE
unfolding disjointify_def
by (smt image_iff rec_disjointify_as_enum_rec_disjointify_image)
subsection‹The Atoms Generated by Collections of Sets›
text‹
We can also turn a family of sets into a disjoint family by taking the atoms of the boolean
algebra generated by these sets. This will still yield a finite family if the initial family is
finite, but in general will be much larger in size.
›
subsubsection‹Defining the Atoms of a Family of Sets›
text‹
Here we intend that ‹As› is a subset of the collection of sets ‹Xs›. This function associate to each
subset ‹As ⊆ Xs› a set which is contained in each element of ‹As›, and is disjoint from
each element of ‹Xs - As›. Note that in general this may yield the empty set, but we will
ultimately be interested in the cases where the result is nonempty.›
definition subset_to_atom where
"subset_to_atom Xs As = ⋂ As - ⋃ (Xs - As)"
lemma subset_to_atom_memI:
assumes "⋀A. A ∈ As ⟹ x ∈ A"
assumes "⋀A. A ∈ Xs ⟹ A ∉ As ⟹ x ∉ A"
shows "x ∈ subset_to_atom Xs As"
using assms unfolding subset_to_atom_def
by blast
lemma subset_to_atom_memE:
assumes "x ∈ subset_to_atom Xs As"
shows "⋀A. A ∈ As ⟹ x ∈ A"
"⋀A. A ∈ Xs ⟹ A ∉ As ⟹ x ∉ A"
using assms unfolding subset_to_atom_def by auto
lemma subset_to_atom_closed:
assumes "As ≠ {}"
assumes "As ⊆ Xs"
shows "subset_to_atom Xs As ⊆ ⋃ Xs"
proof-
have 0: "⋂ As ⊆ ⋃ As "
apply(rule subsetI)
using assms(1) by blast
show ?thesis
apply(rule subsetI)
using assms 0 unfolding subset_to_atom_def
by (meson DiffD1 Union_mono subsetD)
qed
lemma subset_to_atom_as_intersection:
assumes "As ≠ {}"
assumes "As ⊆ Xs"
assumes "S = ⋃ Xs"
shows "subset_to_atom Xs As = ⋂ As ∩ (⋂ X ∈ Xs - As. S - X)"
unfolding assms subset_to_atom_def
apply(rule equalityI')
apply(rule IntI, blast)
apply(rule InterI)
using INT_I assms(1) assms(2) apply auto[1]
apply(rule DiffI, blast)
by blast
definition atoms_of where
"atoms_of Xs = (subset_to_atom Xs ` ((Pow Xs) - {{}})) - {{}}"
lemma atoms_nonempty:
assumes "A ∈ atoms_of Xs"
shows "A ≠ {}"
using assms unfolding atoms_of_def by blast
lemma atoms_of_disjoint:
assumes "A ∈ atoms_of Xs"
assumes "B ∈ atoms_of Xs"
assumes "A ≠ B"
shows "A ∩ B = {}"
proof-
obtain a where a_def: "a ⊆ Xs ∧ A = subset_to_atom Xs a"
using assms unfolding atoms_of_def by blast
obtain b where b_def: "b ⊆ Xs ∧ B = subset_to_atom Xs b"
using assms unfolding atoms_of_def by blast
have a_neq_b: "a ≠ b"
using assms a_def b_def by blast
have "A ∩ B ⊆ {}"
proof fix x assume A: "x ∈ A ∩ B"
show "x ∈ {}"
proof(cases "a ⊆ b")
case True
then obtain c where c_def: "c ∈ b - a"
using a_neq_b by blast
have c_in_Xs: "c ∈ Xs"
using c_def b_def by blast
have x_in_c: "x ∈ c"
using A b_def c_def subset_to_atom_memE[of x Xs b c] by blast
have x_notin_c: "x ∉ c"
using A a_def c_in_Xs c_def subset_to_atom_memE[of x Xs a c] by blast
then show ?thesis using x_in_c by blast
next
case False
then obtain c where c_def: "c ∈ a - b"
using a_neq_b by blast
have c_in_Xs: "c ∈ Xs"
using c_def a_def by blast
have x_in_c: "x ∈ c"
using A a_def c_def subset_to_atom_memE[of x Xs a c] by blast
have x_notin_c: "x ∉ c"
using A b_def c_in_Xs c_def subset_to_atom_memE[of x Xs b c] by blast
then show ?thesis using x_in_c by blast
qed
qed
thus "A ∩ B = {}"
by blast
qed
text ‹
The atoms of a family of sets ‹Xs› are minimal in the sense that they are either contained in or
disjoint from each element of ‹Xs›.
›
lemma atoms_are_minimal:
assumes "A ∈ atoms_of Xs"
assumes "X ∈ Xs"
shows "X ∩ A = {} ∨ A ⊆ X"
proof(cases "X ∩ A = {}")
case True
then show ?thesis by blast
next
case False
obtain As where As_def: "As ∈ Pow Xs - {{}} ∧ A = subset_to_atom Xs As"
using assms unfolding atoms_of_def by blast
have A_simp: "A = subset_to_atom Xs As"
using As_def by blast
then show ?thesis using assms unfolding atoms_of_def subset_to_atom_def A_simp
using DiffD1 subset_eq by auto
qed
subsubsection‹Atoms Induced by Types of Points›
text‹
The set of sets in ‹Xs› which contain some point ‹x›. In the case where ‹Xs› is some collection of
first order formulas, this is just the type of ‹x› over these formulas.›
definition point_to_type where
"point_to_type Xs x = {X ∈ Xs. x ∈ X}"
text ‹The type of a point ‹x› induces the unique atom of ‹Xs› which contains ‹x›.›
lemma point_in_atom_of_type:
assumes "x ∈ ⋃ Xs"
shows "x ∈ subset_to_atom Xs (point_to_type Xs x)"
using assms unfolding subset_to_atom_def point_to_type_def
by blast
lemma point_to_type_nonempty:
assumes "x ∈ ⋃ Xs"
shows "point_to_type Xs x ≠{}"
using assms unfolding point_to_type_def
by blast
lemma point_to_type_closed:
"point_to_type Xs x ⊆ Pow (⋃ Xs)"
unfolding point_to_type_def
by blast
lemma atoms_of_covers:
assumes "X = ⋃ Xs"
shows "⋃ (atoms_of Xs) = X"
proof
show " ⋃ (atoms_of Xs) ⊆ X"
proof fix x assume A: "x ∈ ⋃ (atoms_of Xs)"
then obtain As where As_def: "As ∈ Pow Xs - {{}} ∧ x ∈ subset_to_atom Xs As"
unfolding atoms_of_def by blast
have "subset_to_atom Xs As ⊆ ⋃ Xs"
using subset_to_atom_closed[of As Xs] As_def by blast
then show "x ∈ X" unfolding assms
using As_def by blast
qed
show "X ⊆ ⋃ (atoms_of Xs)" apply(rule subsetI)
using point_to_type_nonempty point_in_atom_of_type point_to_type_closed
unfolding assms point_to_type_def atoms_of_def
by fastforce
qed
lemma atoms_of_covers':
shows "⋃ (atoms_of Xs) = ⋃ Xs"
using atoms_of_covers[of "⋃ Xs"] by blast
text ‹Every atom of a collection ‹Xs› of sets is realized as the atom generated by the type of
an element in that atom.›
lemma nonemtpy_atom_from_point_to_type:
assumes "A ∈ atoms_of Xs"
assumes "a ∈ A"
shows "A = subset_to_atom Xs (point_to_type Xs a)"
proof-
obtain As where As_def: "As ∈ (Pow Xs) - {} ∧ A = subset_to_atom Xs As"
using assms unfolding atoms_of_def by blast
have A_simp: "A = subset_to_atom Xs As"
using As_def by blast
have 0: "As = point_to_type Xs a"
apply(rule equalityI)
apply(rule subsetI)
apply (smt As_def Diff_empty UnionI Union_Pow_eq assms point_in_atom_of_type subset_to_atom_memE(1) subset_to_atom_memE(2))
apply(rule subsetI)
using As_def assms subset_to_atom_memE(2)
by (metis (no_types, lifting) mem_Collect_eq point_to_type_def)
show ?thesis
using point_in_atom_of_type 0
atoms_of_covers'[of Xs] assms unfolding A_simp
by auto
qed
text ‹
In light of the previous theorem, a point a and a collection of sets ‹Xs› is enough to recover
the the unique atom of ‹Xs› which contains ‹a›.
›
definition point_to_atom where
"point_to_atom Xs a = subset_to_atom Xs (point_to_type Xs a)"
lemma point_to_atom_closed:
assumes "x ∈ ⋃ Xs"
shows "point_to_atom Xs x ∈ atoms_of Xs"
using assms unfolding atoms_of_def point_to_atom_def
by (metis (full_types) Union_iff atoms_of_covers atoms_of_def nonemtpy_atom_from_point_to_type)
text ‹All atoms of ‹Xs› are the atom induced by some point in the union of ‹Xs›.›
lemma atoms_induced_by_points:
"atoms_of Xs = point_to_atom Xs ` (⋃ Xs)"
apply(rule equalityI)
apply(rule subsetI)
using nonemtpy_atom_from_point_to_type atoms_nonempty atoms_of_covers'
unfolding point_to_atom_def
apply (smt DiffE Pow_empty Pow_iff atoms_of_def image_iff subsetD subsetI subset_to_atom_closed)
apply(rule subsetI)
by (metis (no_types, lifting) imageE point_to_atom_closed point_to_atom_def)
subsubsection‹Atoms of Generated Boolean Algebras›
lemma atoms_of_gen_boolean_algebra:
assumes "Xs ⊆ gen_boolean_algebra S B"
assumes "finite Xs"
shows "atoms_of Xs ⊆ gen_boolean_algebra S B"
proof
fix x assume A: "x ∈ atoms_of Xs"
then obtain As where As_def: "As ∈ ((Pow Xs) - {{}}) ∧ x = subset_to_atom Xs As"
unfolding atoms_of_def by blast
have x_simp: "x = subset_to_atom Xs As"
using As_def by blast
have 0: "finite As"
using As_def assms finite_subset by auto
have 1: "As ⊆ gen_boolean_algebra S B"
using As_def assms by blast
have 2: "⋂ As ∈ gen_boolean_algebra S B"
using 0 1 assms
by (metis As_def DiffE gen_boolean_algebra_finite_intersection singletonI subset_eq)
show "x ∈ gen_boolean_algebra S B"
using A 2 unfolding atoms_of_def subset_to_atom_def x_simp
by (metis (no_types, lifting) As_def DiffD1 Diff_partition Pow_iff Un_subset_iff assms(1) assms(2) finite_subset gen_boolean_algebra_diff gen_boolean_algebra_finite_union order_refl subsetD)
qed
text ‹If the generators of a boolean algebra are contained in the universe, the atoms induced by
the generators alone are minimal elements of the entire algebra.›
lemma finite_algebra_atoms_are_minimal:
assumes "finite Xs"
assumes "⋃ Xs ⊆ S"
assumes "A ∈ atoms_of Xs"
assumes "X ∈ gen_boolean_algebra S Xs"
shows "X ∩ A = {} ∨ A ⊆ X"
apply(rule gen_boolean_algebra.induct[of X S Xs])
apply (simp add: assms(4); fail)
apply (metis Union_upper assms(2) assms(3) atoms_of_covers dual_order.trans)
using assms(2) assms(3) atoms_are_minimal apply fastforce
apply blast
using assms
by (metis Diff_Int_distrib2 Diff_empty Diff_eq_empty_iff Sup_upper atoms_of_covers' equalityE inf.absorb_iff2 order_trans)
lemma finite_set_imp_finite_atoms:
assumes "finite Xs"
shows "finite (atoms_of Xs)"
using assms unfolding atoms_of_def
by blast
text ‹
Every element in the boolean algebra generated by ‹Xs› over ‹S› is a (disjoint) union
of atoms of generators:
›
lemma gen_boolean_algebra_elem_uni_of_atoms:
assumes "finite Xs"
assumes "S = ⋃ Xs"
assumes "X ∈ gen_boolean_algebra S Xs"
shows "X = ⋃ {a ∈ atoms_of Xs. a ⊆ X}"
proof
show "X ⊆ ⋃ {a ∈ atoms_of Xs. a ⊆ X}"
proof fix x assume A: "x ∈ X"
then have "point_to_atom Xs x ∈ atoms_of Xs"
using assms by (meson gen_boolean_algebra_subset point_to_atom_closed subsetD)
then show "x ∈ ⋃ {a ∈ atoms_of Xs. a ⊆ X}"
by (smt A IntI Union_iff assms(1) assms(2) assms(3) empty_iff finite_algebra_atoms_are_minimal gen_boolean_algebra.universe gen_boolean_algebra_subset mem_Collect_eq point_in_atom_of_type point_to_atom_def subsetD)
qed
show "⋃ {a ∈ atoms_of Xs. a ⊆ X} ⊆ X"
by blast
qed
text‹In fact, every generated boolean algebra is the power set of the atoms of its generators:›
lemma gen_boolean_algebra_generated_by_atoms:
assumes "finite Xs"
assumes "S = ⋃ Xs"
shows "gen_boolean_algebra S Xs = ⋃ ` (Pow (atoms_of Xs))"
proof
show "gen_boolean_algebra S Xs ⊆ ⋃ ` Pow (atoms_of Xs)"
apply(rule subsetI)
using gen_boolean_algebra_elem_uni_of_atoms[of Xs S] assms
by fastforce
show "⋃ ` Pow (atoms_of Xs) ⊆ gen_boolean_algebra S Xs"
apply(rule subsetI)
using atoms_of_gen_boolean_algebra[of Xs S Xs]
finite_subset[of _ "atoms_of Xs"] assms
finite_set_imp_finite_atoms[of Xs]
gen_boolean_algebra_finite_union[of _ S Xs]
by (smt Pow_iff Union_upper gen_boolean_algebra.intros(2) image_iff inf.absorb1 subsetD subsetI)
qed
text‹Finitely generated boolean algebras are finite›
lemma fin_gens_imp_fin_algebra:
assumes "finite Xs"
assumes "S = ⋃ Xs"
shows "finite (gen_boolean_algebra S Xs)"
using finite_set_imp_finite_atoms[of Xs] assms gen_boolean_algebra_generated_by_atoms[of Xs S]
by simp
lemma point_to_atom_equal:
assumes "finite Xs"
assumes "S = ⋃ Xs"
assumes "x ∈ S"
shows "point_to_atom Xs x = point_to_atom (gen_boolean_algebra S Xs) x"
proof
show P0: "point_to_atom Xs x ⊆ point_to_atom (gen_boolean_algebra S Xs) x"
proof-
have 0: "point_to_atom Xs x ∩ point_to_atom (gen_boolean_algebra S Xs) x ≠ {}"
using assms
by (metis IntI UnionI empty_iff gen_boolean_algebra.universe point_in_atom_of_type point_to_atom_def)
have 1: "point_to_atom (gen_boolean_algebra S Xs) x ∈ gen_boolean_algebra S Xs"
using assms fin_gens_imp_fin_algebra[of Xs S]
by (meson UnionI atoms_of_gen_boolean_algebra gen_boolean_algebra.simps point_to_atom_closed subset_eq subset_refl)
then show ?thesis
using 0 finite_algebra_atoms_are_minimal[of Xs S "point_to_atom Xs x" "point_to_atom (gen_boolean_algebra S Xs) x"]
assms(1) assms(2) assms(3) atoms_induced_by_points by auto
qed
show "point_to_atom (gen_boolean_algebra S Xs) x ⊆ point_to_atom Xs x"
proof-
have 0: "point_to_atom (gen_boolean_algebra S Xs) x ∩ point_to_atom Xs x ≠{}"
using assms P0 point_in_atom_of_type point_to_atom_def by fastforce
have 1: "point_to_atom (gen_boolean_algebra S Xs) x ∈ (gen_boolean_algebra S Xs)"
using assms gen_boolean_algebra_idempotent[of S Xs] atoms_of_gen_boolean_algebra
by (metis UnionI fin_gens_imp_fin_algebra gen_boolean_algebra.universe point_to_atom_closed subset_eq)
have 2: "⋃ (gen_boolean_algebra S Xs) ⊆ S"
using assms
by (simp add: Sup_le_iff gen_boolean_algebra_subset)
hence 3: "⋃ (gen_boolean_algebra S Xs) = S"
by (simp add: Union_upper gen_boolean_algebra.universe subset_antisym)
have 4: "gen_boolean_algebra S (gen_boolean_algebra S Xs) = gen_boolean_algebra S Xs"
using assms gen_boolean_algebra_idempotent[of S Xs] by blast
have 5: "point_to_atom Xs x ∈ gen_boolean_algebra S (gen_boolean_algebra S Xs)"
unfolding 4 using assms
by (metis (no_types, opaque_lifting) Int_absorb1 Int_commute Union_upper atoms_of_gen_boolean_algebra gen_boolean_algebra.generator point_to_atom_closed subsetD subsetI)
show ?thesis
using 2 5 finite_algebra_atoms_are_minimal[of "gen_boolean_algebra S Xs" S "point_to_atom (gen_boolean_algebra S Xs) x" "point_to_atom Xs x"] 0 1 2
unfolding 4
by (metis "3" Int_commute assms(1) assms(2) assms(3) fin_gens_imp_fin_algebra point_to_atom_closed)
qed
qed
text ‹
When the set ‹Xs› of generators covers the universe set ‹S›, the atoms of ‹Xs› in the above
sense are the same as the atoms of the boolean algebra they generate over ‹S›.
›
lemma atoms_of_sets_eq_atoms_of_algebra:
assumes "finite Xs"
assumes "S = ⋃ Xs"
shows "atoms_of Xs = atoms_of (gen_boolean_algebra S Xs)"
proof
show "atoms_of Xs ⊆ atoms_of (gen_boolean_algebra S Xs)"
proof fix A assume A: "A ∈ atoms_of Xs"
then obtain x where x_def: "x ∈ S ∧ A = point_to_atom Xs x"
using assms
by (metis atoms_induced_by_points image_iff)
have 0: "A = point_to_atom (gen_boolean_algebra S Xs) x"
using assms point_to_atom_equal x_def by fastforce
show "A ∈ atoms_of (gen_boolean_algebra S Xs)"
unfolding 0 using assms A
by (metis (full_types) "0" UnionI gen_boolean_algebra.universe point_to_atom_closed x_def)
qed
show "atoms_of (gen_boolean_algebra S Xs) ⊆ atoms_of Xs"
proof fix A assume A: "A ∈ atoms_of (gen_boolean_algebra S Xs)"
then obtain x where x_def: "x ∈ S ∧ A = point_to_atom (gen_boolean_algebra S Xs) x"
by (metis atoms_induced_by_points cSup_eq_maximum gen_boolean_algebra.universe gen_boolean_algebra_subset image_iff)
then show "A ∈ atoms_of Xs"
using assms(1) assms(2) point_to_atom_closed point_to_atom_equal by fastforce
qed
qed
lemma atoms_closed:
assumes "finite Xs"
assumes "A ∈ atoms_of (gen_boolean_algebra S Xs)"
assumes "S = ⋃ Xs"
shows "A ∈ (gen_boolean_algebra S Xs)"
proof-
have 1: "A = ⋃ {A}"
by blast
have 2: "A ∈ atoms_of Xs"
using assms atoms_of_sets_eq_atoms_of_algebra
by blast
show ?thesis
using gen_boolean_algebra_generated_by_atoms[of Xs S]
assms 1 2 unfolding Pow_def by blast
qed
lemma atoms_finite:
assumes "finite Xs"
shows "finite ((atoms_of (gen_boolean_algebra S Xs)))"
proof-
have 0: "gen_boolean_algebra S Xs =gen_boolean_algebra S ((∩) S ` Xs)"
using gen_boolean_algebra_restrict_generators by blast
have 1: "gen_boolean_algebra S Xs = gen_boolean_algebra S (insert S ((∩) S ` Xs))"
unfolding 0 by(rule add_generators, rule gen_boolean_algebra.universe)
obtain Ys where Ys_def: "Ys = (insert S ((∩) S ` Xs))"
by blast
have Ys_finite: "finite Ys"
unfolding Ys_def using assms by blast
have 2: "⋃ Ys = S"
unfolding Ys_def
by blast
have 3: "atoms_of Ys = atoms_of (gen_boolean_algebra S Xs) "
unfolding Ys_def 1
apply(rule atoms_of_sets_eq_atoms_of_algebra)
using Ys_finite unfolding Ys_def apply blast
by blast
have 4: "finite (atoms_of Ys)"
by(rule finite_set_imp_finite_atoms, rule Ys_finite)
show ?thesis using 4 unfolding 3 by blast
qed
text ‹
We can distinguish atoms of a set of generators ‹Cs› by finding some element of ‹Cs› which
includes one and excludes the other.
›
lemma distinct_atoms:
assumes "Cs ≠ {}"
assumes "a ∈ atoms_of Cs"
assumes "b ∈ atoms_of Cs"
assumes "a ≠ b"
shows "(∃B ∈ Cs. b ⊆ B ∧ a ∩ B = {}) ∨ (∃A ∈ Cs. a ⊆ A ∧ b ∩ A = {})"
proof-
obtain x where x_def: "x ∈ ⋃ Cs ∧ a = point_to_atom Cs x"
by (metis assms(2) atoms_induced_by_points imageE)
obtain y where y_def: "y ∈ ⋃ Cs ∧ b = point_to_atom Cs y"
by (metis assms(3) atoms_induced_by_points imageE)
have 0: "point_to_atom Cs x ≠ point_to_atom Cs y"
using x_def y_def assms by simp
hence 1: "point_to_type Cs x ≠ point_to_type Cs y"
unfolding point_to_atom_def subset_to_atom_def by blast
then obtain B where B_def: "B ∈ Cs ∧ (B ∈ point_to_type Cs x - point_to_type Cs y ∨ B ∈ point_to_type Cs y - point_to_type Cs x)"
unfolding point_to_type_def by blast
have 2: "B ∈ point_to_type Cs x - point_to_type Cs y ⟹ a ⊆ B"
using x_def point_to_atom_def subset_to_atom_memE(1) by fastforce
have 3: "B ∈ point_to_type Cs y - point_to_type Cs y ⟹ b ⊆ B"
using y_def by blast
show ?thesis using B_def 2 3
by (smt Diff_iff disjoint_iff_not_equal point_to_atom_def subset_eq subset_to_atom_memE(1) subset_to_atom_memE(2) x_def y_def)
qed
subsection‹Partitions of a Set›
definition disjoint :: "'a set set ⇒ bool" where
"disjoint Ss = (∀ A ∈ Ss. ∀B ∈ Ss. A ≠B ⟶ A ∩ B = {})"
lemma disjointE:
assumes "disjoint Ss"
assumes "A ∈ Ss"
assumes "B ∈ Ss"
assumes "A ≠B"
shows "A ∩ B = {}"
by (meson assms(1) assms(2) assms(3) assms(4) disjoint_def)
lemma disjointI:
assumes "⋀A B. A ∈ Ss ⟹ B ∈ Ss ⟹ A ≠ B ⟹ A ∩ B = {}"
shows "disjoint Ss"
by (meson assms disjoint_def)
definition is_partition :: "'a set set ⇒ 'a set ⇒ bool" (infixl "partitions" 75) where
"S partitions A = (disjoint S ∧ ⋃ S = A)"
lemma is_partitionE:
assumes "S partitions A"
shows "disjoint S"
"⋃ S = A"
using assms is_partition_def apply blast
using assms
by (simp add: is_partition_def)
lemma is_partitionI:
assumes "disjoint S"
assumes "⋃ S = A"
shows "S partitions A"
using assms is_partition_def by blast
text ‹
If we start with a finite partition of a set ‹A›, and each element in that partition has a
finite partition with some property ‹P›, then ‹A› itself has a finite partition where each
element has property ‹P›.›
lemma iter_partition:
assumes "As partitions A"
assumes "finite As"
assumes "⋀a. a ∈ As ⟹ ∃Bs. finite Bs ∧ Bs partitions a ∧ (∀b ∈ Bs. P b)"
shows "∃Bs. finite Bs ∧ Bs partitions A ∧ (∀b ∈ Bs. P b)"
proof-
obtain F where F_def: "F = (λa. (SOME Bs. finite Bs ∧ Bs partitions a ∧ (∀b ∈ Bs. P b)))"
by blast
have FE: "⋀a. a ∈ As ⟹ finite (F a) ∧ (F a) partitions a ∧ (∀b ∈ (F a). P b)"
proof- fix a assume A: "a ∈ As"
show "finite (F a) ∧ (F a) partitions a ∧ (∀b ∈ (F a). P b)"
apply(rule SomeE'[of _ "λBs. finite Bs ∧ Bs partitions a ∧ (∀b ∈ Bs. P b)"])
unfolding F_def apply blast
using assms by (simp add: A)
qed
obtain Bs where Bs_def: "Bs = (⋃ a ∈ As. F a)"
by blast
have 0: "finite Bs"
unfolding Bs_def using FE assms by blast
have 1: "disjoint Bs"
proof(rule disjointI)
fix a b assume A: "a ∈ Bs" "b ∈ Bs" "a ≠ b"
obtain c where c_def: "c ∈ As ∧ a ∈ F c"
using Bs_def A by blast
obtain d where d_def: "d ∈ As ∧ b ∈ F d"
using Bs_def A by blast
have 0: "a ⊆ c"
using c_def FE[of c] is_partitionE(2)[of "F c" c] by blast
have 1: "b ⊆ d"
using d_def FE[of d] is_partitionE(2)[of "F d" d] by blast
show "a ∩ b = {}"
proof(cases "c = d")
case True
show ?thesis apply(rule disjointE[of "F c"])
unfolding True using FE is_partitionE d_def apply blast
using c_def unfolding True apply blast
using d_def apply blast
by(rule A)
next
case False
have "c ∩ d = {}"
apply(rule disjointE[of As])
using assms is_partitionE apply blast
using c_def apply blast
using d_def apply blast
using False by blast
then show ?thesis using 0 1 by blast
qed
qed
have 2: "(∀b ∈ Bs. P b)"
apply(rule )
unfolding Bs_def using FE
by blast
have FE': "⋀a. a ∈ As ⟹ (⋃ (F a)) = a "
apply(rule is_partitionE)
using FE by blast
have 3: "Bs partitions A"
apply(rule is_partitionI, rule 1)
apply(rule equalityI')
unfolding Bs_def using assms is_partitionE(2)[of As A]
FE' is_partitionE(2) apply blast
proof-
fix x assume A: "x ∈ A"
then obtain a where a_def: "a ∈ As ∧ x ∈ a"
using assms is_partitionE by blast
then have "x ∈ (⋃ (F a))"
using a_def FE' by blast
thus " x ∈ ⋃ (⋃ (F ` As))"
using a_def A by blast
qed
show "∃Bs. finite Bs ∧ Bs partitions A ∧ (∀b∈Bs. P b)"
using 0 2 3 by blast
qed
subsection‹Intersections of Families of Sets›
definition pairwise_intersect where
"pairwise_intersect As Bs = {c. ∃a ∈ As. ∃b ∈ Bs. c = a ∩ b}"
lemma partition_intersection:
assumes "As partitions A"
assumes "Bs partitions B"
shows "(pairwise_intersect As Bs) partitions (A ∩ B)"
proof(rule is_partitionI, rule disjointI)
fix a b assume a0: "a ∈ pairwise_intersect As Bs" "b ∈ pairwise_intersect As Bs" "a ≠ b"
obtain a1 b1 where def1: "a1 ∈ As ∧ b1 ∈ Bs ∧ a = a1 ∩ b1"
using a0 unfolding pairwise_intersect_def by blast
obtain a2 b2 where def2: "a2 ∈ As ∧ b2 ∈ Bs ∧ b = a2 ∩ b2"
using a0 unfolding pairwise_intersect_def by blast
have 0: "a ∩ b = (a1 ∩ a2) ∩ (b1 ∩ b2)"
using def1 def2 by blast
show " a ∩ b= {}"
proof(cases "a1 ≠ a2")
case True
have T0: "a1 ∩ a2 = {}"
apply(rule disjointE[of As a1 a2] )
using def1 def2 assms(1) True is_partitionE(1)[of As A] apply blast
using def1 apply blast using def2 apply blast by(rule True)
thus ?thesis unfolding 0 by blast
next
case False
then have F0: "b1 ≠ b2"
using a0 def1 def2 by blast
have F1: "b1 ∩ b2 = {}"
apply(rule disjointE[of Bs b1 b2])
using def1 def2 assms(2) F0 is_partitionE(1)[of Bs B] apply blast
using def1 apply blast using def2 apply blast by(rule F0)
thus ?thesis unfolding 0 by blast
qed
next
show "⋃ (pairwise_intersect As Bs) = A ∩ B"
proof(rule equalityI')
fix x assume A: "x ∈ ⋃ (pairwise_intersect As Bs)"
then obtain a b where def1: "a ∈ As ∧ b ∈ Bs ∧ x ∈ a ∩ b"
unfolding pairwise_intersect_def by blast
have 0: "a ⊆ A"
using def1 assms is_partitionE by blast
have 1: "b ⊆ B"
using def1 assms is_partitionE by blast
show " x ∈ A ∩ B"
using 0 1 def1 by blast
next
fix x assume A: "x ∈ A ∩ B"
obtain a where a_def: "a ∈ As ∧ x ∈ a"
using A assms is_partitionE by blast
obtain b where b_def: "b ∈ Bs ∧ x ∈ b"
using A assms is_partitionE by blast
have 0: "x ∈ a ∩ b"
using a_def b_def by blast
show "x ∈ ⋃ (pairwise_intersect As Bs)"
using a_def b_def 0 unfolding pairwise_intersect_def
by blast
qed
qed
lemma pairwise_intersect_finite:
assumes "finite As"
assumes "finite Bs"
shows "finite (pairwise_intersect As Bs)"
proof-
have 0: "(pairwise_intersect As Bs) = (⋃ a ∈ As. (∩) a ` Bs)"
unfolding pairwise_intersect_def
apply(rule equalityI')
unfolding mem_Collect_eq apply blast
by blast
have 1: "⋀a. a ∈ As ⟹ finite ((∩) a ` Bs)"
using assms by blast
show ?thesis unfolding 0 using assms(1) 1 by blast
qed
definition family_intersect where
"family_intersect parts = atoms_of (⋃ parts)"
lemma family_intersect_partitions:
assumes "⋀Ps. Ps ∈ parts ⟹ Ps partitions A"
assumes "⋀Ps. Ps ∈ parts ⟹ finite Ps"
assumes "finite parts"
assumes "parts ≠ {}"
shows "family_intersect parts partitions A"
proof(rule is_partitionI)
show "disjoint (family_intersect parts)"
apply(rule disjointI)
unfolding family_intersect_def apply(rule atoms_of_disjoint)
apply blast
apply blast
by blast
show " ⋃ (family_intersect parts) = A"
proof-
have 0: "⋃ (family_intersect parts) = ⋃ (⋃ parts)"
unfolding family_intersect_def
apply(rule atoms_of_covers)
by blast
have 1: "⋀Ps. Ps ∈ parts ⟹ ⋃Ps = A"
by(rule is_partitionE, rule assms, blast)
show ?thesis unfolding 0
using 1 assms by blast
qed
qed
lemma family_intersect_memE:
assumes "⋀Ps. Ps ∈ parts ⟹ Ps partitions A"
assumes "⋀Ps. Ps ∈ parts ⟹ finite Ps"
assumes "finite parts"
assumes "parts ≠ {}"
shows "⋀Ps a. a ∈ family_intersect parts ⟹ Ps ∈ parts ⟹ ∃P ∈ Ps. a ⊆ P"
proof-
fix Ps a assume A: "a ∈ family_intersect parts" "Ps ∈ parts"
have 0: "⋃ Ps = A"
apply(rule is_partitionE)
using A assms by blast
have 1: "⋃ (family_intersect parts) = A"
apply(rule is_partitionE)
using family_intersect_partitions assms by blast
have 2: "a ≠ {}"
using A unfolding family_intersect_def atoms_of_def by blast
obtain P where P_def: "P ∈ Ps ∧ a ∩ P ≠ {}"
using 0 1 A 2 by blast
have P_in: "P ∈ (⋃ parts)"
using P_def A by blast
have a_sub: "a ⊆ P"
using atoms_are_minimal P_def A P_in unfolding family_intersect_def by blast
show "∃P ∈ Ps. a ⊆ P"
using a_sub P_def by blast
qed
lemma family_intersect_mem_inter:
assumes "⋀Ps. Ps ∈ (parts:: 'a set set set) ⟹ Ps partitions A"
assumes "⋀Ps. Ps ∈ parts ⟹ finite Ps"
assumes "finite parts"
assumes "parts ≠ {}"
assumes "a ∈ family_intersect parts"
shows "∃f. ∀ Ps ∈ parts. f Ps ∈ Ps ∧ a = (⋂ Ps ∈ parts. f Ps)"
proof-
obtain f where f_def: "f = (λPs:: 'a set set. (SOME P. P ∈ Ps ∧ a ⊆ P))"
by blast
have f_eval: "⋀Ps. Ps ∈ parts ⟹ f Ps ∈ Ps ∧ a ⊆ (f Ps)"
proof-
fix Ps assume A: "Ps ∈ parts"
obtain P where P_def: "P ∈ Ps ∧ a ⊆ P"
using assms family_intersect_memE A by blast
show " f Ps ∈ Ps ∧ a ⊆ f Ps"
apply(rule SomeE[of "f Ps" _ P])
unfolding f_def using A apply simp
by(rule P_def)
qed
have 0: "a ≠ {}"
using assms unfolding family_intersect_def
using atoms_nonempty by blast
have 1: "a = (⋂ Ps ∈ parts. f Ps)"
proof(rule equalityI)
show 10: "a ⊆ ⋂ (f ` parts)"
using f_eval by blast
show "⋂ (f ` parts) ⊆ a"
proof
fix x assume A: "x ∈ ⋂ (f ` parts)"
obtain b where b_def: "b = point_to_atom (⋃ parts) x"
by blast
have b_atom: "b ∈ atoms_of (⋃ parts)"
unfolding b_def apply(rule point_to_atom_closed)
using A f_eval assms by blast
show x_in_a: "x ∈ a"
proof(rule ccontr)
assume "x ∉ a"
then have "¬ b ⊆ a"
using b_def unfolding point_to_atom_def point_to_type_def subset_to_atom_def by blast
hence p0: "a ≠ b"
by blast
have p1: "b ∩ a = {}"
apply(rule atoms_of_disjoint[of _ "(⋃ parts)"] )
apply(rule b_atom)
using assms unfolding family_intersect_def apply blast
using p0 by blast
have p2: " (∃B∈⋃ parts. b ⊆ B ∧ a ∩ B = {}) ∨ (∃A∈⋃ parts. a ⊆ A ∧ b ∩ A = {})"
using distinct_atoms[of "⋃ parts" a b] assms
by (metis Sup_bot_conv(1) b_atom equalityI' f_eval family_intersect_def mem_simps(2) p0)
show False
proof(cases "(∃B∈⋃ parts. b ⊆ B ∧ a ∩ B = {})")
case True
then obtain B where B_def: "B∈⋃ parts ∧ b ⊆ B ∧ a ∩ B = {}"
by blast
obtain Ps where Ps_def: "B ∈ Ps ∧ Ps ∈ parts"
using B_def by blast
have B_neq: "B ≠ f Ps"
using Ps_def B_def 10 0 by blast
have B_cap: "B ∩ f Ps = {}"
apply(rule disjointE[of Ps])
apply(rule is_partitionE[of Ps A])
using Ps_def assms apply blast
using Ps_def apply blast
using f_eval Ps_def apply blast
by(rule B_neq)
have b_cap: "b ∩ f Ps = {}"
using B_cap B_def by blast
have x_in_b: "x ∈ b"
using b_def unfolding point_to_atom_def point_to_type_def subset_to_atom_def
by blast
show False using x_in_b b_cap Ps_def A by blast
next
case False
then obtain B where B_def: "B∈⋃ parts ∧ a ⊆ B ∧ b ∩ B = {}"
using p2 by blast
obtain Ps where Ps_def: "B ∈ Ps ∧ Ps ∈ parts"
using B_def by blast
have F0: "B = f Ps"
proof(rule ccontr)
assume not: "B ≠ f Ps"
have F0: "B ∩ f Ps = {}"
apply(rule disjointE[of Ps])
apply(rule is_partitionE[of Ps A])
using Ps_def assms apply blast
using Ps_def apply blast
using f_eval Ps_def apply blast
by(rule not)
have a_sub: "a ⊆ f Ps"
using 10 Ps_def by blast
show False using F0 B_def a_sub 0 by blast
qed
have x_in_B: "x ∈ B"
unfolding F0 using A Ps_def by blast
have x_in_b: "x ∈ b"
using b_def unfolding point_to_atom_def point_to_type_def subset_to_atom_def
by blast
show False using x_in_b x_in_B B_def by blast
qed
qed
qed
qed
show ?thesis using f_eval 1 by blast
qed
text ‹
If we take a finite family of partitions in a particular generated boolean algebra, where each
partition itself is finite, then their induced partition is also in the algebra.›
lemma family_intersect_in_gen_boolean_algebra:
assumes "A ∈ gen_boolean_algebra S B"
assumes "⋀Ps. Ps ∈ parts ⟹ Ps partitions A"
assumes "⋀Ps. Ps ∈ parts ⟹ finite Ps"
assumes "⋀Ps P. Ps ∈ parts ⟹ P ∈ Ps ⟹ P ∈ gen_boolean_algebra S B"
assumes "finite parts"
assumes "parts ≠ {}"
shows "⋀P. P ∈ family_intersect parts ⟹ P ∈ gen_boolean_algebra S B"
proof-
fix P assume A: "P ∈ family_intersect parts"
have 0: "P ∈ atoms_of (⋃ parts)"
using A unfolding family_intersect_def by blast
have 1: "finite (⋃ parts)"
using assms by blast
have 2: "⋃ parts ⊆ gen_boolean_algebra S B"
using assms by blast
obtain Ps where Ps_def: "Ps ∈ parts"
using assms by blast
have 3: "⋃ (⋃ parts) = A"
apply(rule equalityI')
using assms is_partitionE(2)[of _ A] apply blast
using assms is_partitionE(2)[of Ps A] Ps_def by blast
have 4: "atoms_of (⋃ parts) = atoms_of (gen_boolean_algebra A (⋃ parts))"
apply(rule atoms_of_sets_eq_atoms_of_algebra[of "⋃ parts" A])
apply(rule 1)
unfolding 3 by blast
have 5: "atoms_of (⋃ parts) ⊆ (gen_boolean_algebra A (⋃ parts))"
apply(rule atoms_of_gen_boolean_algebra)
using 3 gen_boolean_algebra.generator[of _ "⋃ parts" A]
apply (meson Sup_upper gen_boolean_algebra_generators subsetI)
by(rule 1)
have 6: "A ⊆ S"
using assms gen_boolean_algebra_subset by blast
have 7: "(gen_boolean_algebra A (⋃ parts)) ⊆ gen_boolean_algebra (S) (⋃ parts)"
apply(rule gen_boolean_algebra_univ_mono)
using 3 gen_boolean_algebra_finite_union[of "⋃ parts" "S" "⋃ parts"]
gen_boolean_algebra.generator[of _ "⋃ parts" "S" ] 6 1
by (meson Sup_le_iff gen_boolean_algebra_generators)
have 8: "gen_boolean_algebra (S) (⋃ parts) ⊆ gen_boolean_algebra S B"
apply(rule gen_boolean_algebra_subalgebra)
using 2 by blast
show "P ∈ gen_boolean_algebra S B"
using 0 5 6 7 8 by blast
qed
end