Theory Cardinality
theory Cardinality
imports "List-Infinite.InfiniteSet2" Representation
begin
context uminus
begin
no_notation uminus ("- _" [81] 80)
end
section ‹Atoms Below an Element in Partial Orders›
text ‹
We define the set and the number of atoms below an element in a partial order.
To handle infinitely many atoms we use ‹enat›, which are natural numbers with infinity, and ‹icard›, which modifies ‹card› by giving a separate option of being infinite.
We include general results about ‹enat›, ‹icard›, sets functions and atoms.
›
lemma enat_mult_strict_mono:
assumes "a < b" "c < d" "(0::enat) < b" "0 ≤ c"
shows "a * c < b * d"
proof -
have "a ≠ ∞ ∧ c ≠ ∞"
using assms(1,2) linorder_not_le by fastforce
thus ?thesis
using assms by (smt (verit, del_insts) enat_0_less_mult_iff idiff_eq_conv_enat ileI1 imult_ile_mono imult_is_infinity_enat less_eq_idiff_eq_sum less_le_not_le mult_eSuc_right order.strict_trans1 order_le_neq_trans zero_enat_def)
qed
lemma enat_mult_strict_mono':
assumes "a < b" and "c < d" and "(0::enat) ≤ a" and "0 ≤ c"
shows "a * c < b * d"
using assms by (auto simp add: enat_mult_strict_mono)
lemma finite_icard_card:
"finite A ⟹ icard A = icard B ⟹ card A = card B"
by (metis icard_def icard_eq_enat_imp_card)
lemma icard_eq_sum:
"finite A ⟹ icard A = sum (λx. 1) A"
by (simp add: icard_def of_nat_eq_enat)
lemma icard_sum_constant_function:
assumes "∀x∈A . f x = c"
and "finite A"
shows "sum f A = (icard A) * c"
by (metis assms icard_finite_conv of_nat_eq_enat sum.cong sum_constant)
lemma icard_le_finite:
assumes "icard A ≤ icard B"
and "finite B"
shows "finite A"
by (metis assms enat_ord_simps(5) icard_infinite_conv)
lemma bij_betw_same_icard:
"bij_betw f A B ⟹ icard A = icard B"
by (simp add: bij_betw_finite bij_betw_same_card icard_def)
lemma surj_icard_le: "B ⊆ f ` A ⟹ icard B ≤ icard A"
by (meson icard_image_le icard_mono preorder_class.order_trans)
lemma icard_image_part_le:
assumes "∀x∈A . f x ⊆ B"
and "∀x∈A . f x ≠ {}"
and "∀x∈A . ∀y∈A . x ≠ y ⟶ f x ∩ f y = {}"
shows "icard A ≤ icard B"
proof -
have "∀x∈A . ∃y . y ∈ f x ∩ B"
using assms(1,2) by fastforce
hence "∃g . ∀x∈A . g x ∈ f x ∩ B"
using bchoice by simp
from this obtain g where 1: "∀x∈A . g x ∈ f x ∩ B"
by auto
hence "inj_on g A"
by (metis Int_iff assms(3) empty_iff inj_onI)
thus "icard A ≤ icard B"
using 1 icard_inj_on_le by fastforce
qed
lemma finite_image_part_le:
assumes "∀x∈A . f x ⊆ B"
and "∀x∈A . f x ≠ {}"
and "∀x∈A . ∀y∈A . x ≠ y ⟶ f x ∩ f y = {}"
and "finite B"
shows "finite A"
by (metis assms icard_image_part_le icard_le_finite)
context semiring_1
begin
lemma sum_constant_function:
assumes "∀x∈A . f x = c"
shows "sum f A = of_nat (card A) * c"
proof (cases "finite A")
case True
show ?thesis
proof (rule finite_subset_induct)
show "finite A"
using True by simp
show "A ⊆ A"
by simp
show "sum f {} = of_nat (card {}) * c"
by simp
fix a F
assume "finite F" "a ∈ A" "a ∉ F" "sum f F = of_nat (card F) * c"
thus "sum f (insert a F) = of_nat (card (insert a F)) * c"
using assms by (metis sum.insert sum_constant)
qed
next
case False
thus ?thesis
by simp
qed
end
context order
begin
lemma ne_finite_has_minimal:
assumes "finite S"
and "S ≠ {}"
shows "∃m∈S . ∀x∈S . x ≤ m ⟶ x = m"
proof (rule finite_ne_induct)
show "finite S"
using assms(1) by simp
show "S ≠ {}"
using assms(2) by simp
show "⋀x . ∃m∈{x}. ∀y∈{x}. y ≤ m ⟶ y = m"
by auto
show "⋀x F . finite F ⟹ F ≠ {} ⟹ x ∉ F ⟹ (∃m∈F . ∀y∈F . y ≤ m ⟶ y = m) ⟹ (∃m∈insert x F . ∀y∈insert x F . y ≤ m ⟶ y = m)"
by (metis finite_insert insert_not_empty finite_has_minimal)
qed
end
context order_bot
begin
abbreviation atoms_below :: "'a ⇒ 'a set" ("AB")
where "atoms_below x ≡ { a . atom a ∧ a ≤ x }"
definition num_atoms_below :: "'a ⇒ enat" ("nAB")
where "num_atoms_below x ≡ icard (atoms_below x)"
lemma AB_iso:
"x ≤ y ⟹ AB x ⊆ AB y"
by (simp add: Collect_mono dual_order.trans)
lemma AB_bot:
"AB bot = {}"
by (simp add: bot_unique)
lemma nAB_bot:
"nAB bot = 0"
proof -
have "nAB bot = icard (AB bot)"
by (simp add: num_atoms_below_def)
also have "... = 0"
by (metis (mono_tags, lifting) AB_bot icard_empty)
finally show ?thesis
.
qed
lemma AB_atom:
"atom a ⟷ AB a = {a}"
by blast
lemma nAB_atom:
"atom a ⟹ nAB a = 1"
proof -
assume "atom a"
hence "AB a = {a}"
using AB_atom by meson
thus "nAB a = 1"
by (simp add: num_atoms_below_def one_eSuc)
qed
lemma nAB_iso:
"x ≤ y ⟹ nAB x ≤ nAB y"
using icard_mono AB_iso num_atoms_below_def by auto
end
context bounded_semilattice_sup_bot
begin
lemma nAB_iso_sup:
"nAB x ≤ nAB (x ⊔ y)"
by (simp add: nAB_iso)
end
context bounded_lattice
begin
lemma different_atoms_disjoint:
"atom x ⟹ atom y ⟹ x ≠ y ⟹ x ⊓ y = bot"
using inf_le1 le_iff_inf by auto
lemma AB_dist_inf:
"AB (x ⊓ y) = AB x ∩ AB y"
by auto
lemma AB_iso_inf:
"AB (x ⊓ y) ⊆ AB x"
by (simp add: Collect_mono)
lemma AB_iso_sup:
"AB x ⊆ AB (x ⊔ y)"
by (simp add: Collect_mono le_supI1)
lemma AB_disjoint:
assumes "x ⊓ y = bot"
shows "AB x ∩ AB y = {}"
proof (rule Int_emptyI)
fix a
assume "a ∈ AB x" "a ∈ AB y"
hence "atom a ∧ a ≤ x ∧ a ≤ y"
by simp
thus False
using assms bot_unique by fastforce
qed
lemma nAB_iso_inf:
"nAB (x ⊓ y) ≤ nAB x"
by (simp add: nAB_iso)
end
context distrib_lattice_bot
begin
lemma atom_in_sup:
assumes "atom a"
and "a ≤ x ⊔ y"
shows "a ≤ x ∨ a ≤ y"
proof -
have 1: "a = (a ⊓ x) ⊔ (a ⊓ y)"
using assms(2) inf_sup_distrib1 le_iff_inf by force
have "a ⊓ x = bot ∨ a ⊓ x = a"
using assms(1) by fastforce
thus ?thesis
using 1 le_iff_inf sup_bot_left by fastforce
qed
lemma atom_in_sup_iff:
assumes "atom a"
shows "a ≤ x ⊔ y ⟷ a ≤ x ∨ a ≤ y"
using assms atom_in_sup le_supI1 le_supI2 by blast
lemma atom_in_sup_xor:
"atom a ⟹ a ≤ x ⊔ y ⟹ x ⊓ y = bot ⟹ (a ≤ x ∧ ¬ a ≤ y) ∨ (¬ a ≤ x ∧ a ≤ y)"
using atom_in_sup bot_unique le_inf_iff by blast
lemma atom_in_sup_xor_iff:
assumes "atom a"
and "x ⊓ y = bot"
shows "a ≤ x ⊔ y ⟷ (a ≤ x ∧ ¬ a ≤ y) ∨ (¬ a ≤ x ∧ a ≤ y)"
using assms atom_in_sup_xor le_supI1 le_supI2 by auto
lemma AB_dist_sup:
"AB (x ⊔ y) = AB x ∪ AB y"
proof
show "AB (x ⊔ y) ⊆ AB x ∪ AB y"
using atom_in_sup by fastforce
next
show "AB x ∪ AB y ⊆ AB (x ⊔ y)"
using le_supI1 le_supI2 by fastforce
qed
end
context bounded_distrib_lattice
begin
lemma nAB_add:
"nAB x + nAB y = nAB (x ⊔ y) + nAB (x ⊓ y)"
proof -
have "nAB x + nAB y = icard (AB x ∪ AB y) + icard (AB x ∩ AB y)"
using num_atoms_below_def icard_Un_Int by auto
also have "... = nAB (x ⊔ y) + nAB (x ⊓ y)"
using num_atoms_below_def AB_dist_inf AB_dist_sup by auto
finally show ?thesis
.
qed
lemma nAB_split_disjoint:
assumes "x ⊓ y = bot"
shows "nAB (x ⊔ y) = nAB x + nAB y"
by (simp add: assms nAB_add nAB_bot)
end
context p_algebra
begin
lemma atom_in_p:
"atom a ⟹ a ≤ x ∨ a ≤ -x"
using inf.orderI pseudo_complement by force
lemma atom_in_p_xor:
"atom a ⟹ (a ≤ x ∧ ¬ a ≤ -x) ∨ (¬ a ≤ x ∧ a ≤ -x)"
by (metis atom_in_p le_iff_inf pseudo_complement)
text ‹
The following two lemmas also hold in distributive lattices with a least element (see above).
However, p-algebras are not necessarily distributive, so the following results are indepenent.
›
lemma atom_in_sup':
"atom a ⟹ a ≤ x ⊔ y ⟹ a ≤ x ∨ a ≤ y"
by (metis inf.absorb_iff2 inf.sup_ge2 pseudo_complement sup_least)
lemma AB_dist_sup':
"AB (x ⊔ y) = AB x ∪ AB y"
proof
show "AB (x ⊔ y) ⊆ AB x ∪ AB y"
using atom_in_sup' by fastforce
next
show "AB x ∪ AB y ⊆ AB (x ⊔ y)"
using le_supI1 le_supI2 by fastforce
qed
lemma AB_split_1:
"AB x = AB ((x ⊓ y) ⊔ (x ⊓ -y))"
proof
show "AB x ⊆ AB ((x ⊓ y) ⊔ (x ⊓ -y))"
proof
fix a
assume "a ∈ AB x"
hence "atom a ∧ a ≤ x"
by simp
hence "atom a ∧ a ≤ (x ⊓ y) ⊔ (x ⊓ -y)"
by (metis atom_in_p_xor inf.boundedI le_supI1 le_supI2)
thus "a ∈ AB ((x ⊓ y) ⊔ (x ⊓ -y))"
by simp
qed
next
show "AB ((x ⊓ y) ⊔ (x ⊓ -y)) ⊆ AB x"
using atom_in_sup' inf.boundedE by blast
qed
lemma AB_split_2:
"AB x = AB (x ⊓ y) ∪ AB (x ⊓ -y)"
using AB_dist_sup' AB_split_1 by auto
lemma AB_split_2_disjoint:
"AB (x ⊓ y) ∩ AB (x ⊓ -y) = {}"
using atom_in_p_xor by fastforce
lemma AB_pp:
"AB (--x) = AB x"
by (metis (opaque_lifting) atom_in_p_xor)
lemma nAB_pp:
"nAB (--x) = nAB x"
using AB_pp num_atoms_below_def by auto
lemma nAB_split_1:
"nAB x = nAB ((x ⊓ y) ⊔ (x ⊓ - y))"
using AB_split_1 num_atoms_below_def by simp
lemma nAB_split_2:
"nAB x = nAB (x ⊓ y) + nAB (x ⊓ -y)"
proof -
have "icard (AB (x ⊓ y)) + icard (AB (x ⊓ -y)) = icard (AB (x ⊓ y) ∪ AB (x ⊓ -y)) + icard (AB (x ⊓ y) ∩ AB (x ⊓ -y))"
using icard_Un_Int by auto
also have "... = icard (AB x)"
using AB_split_2 AB_split_2_disjoint by auto
finally show ?thesis
using num_atoms_below_def by auto
qed
end
section ‹Atoms Below an Element in Stone Relation Algebras›
text ‹
We extend our study of atoms below an element to Stone relation algebras.
We consider combinations of the following five assumptions: the Stone relation algebra is atomic, atom-rectangular, atom-simple, a relation algebra, or has finitely many atoms.
We include general properties of atoms, rectangles and simple elements.
›
context stone_relation_algebra
begin
abbreviation rectangle :: "'a ⇒ bool" where "rectangle x ≡ x * top * x ≤ x"
abbreviation simple :: "'a ⇒ bool" where "simple x ≡ top * x * top = top"
lemma rectangle_eq:
"rectangle x ⟷ x * top * x = x"
by (simp add: order.eq_iff ex231d)
lemma arc_univalent_injective_rectangle_simple:
"arc a ⟷ univalent a ∧ injective a ∧ rectangle a ∧ simple a"
by (smt (z3) arc_top_arc comp_associative conv_dist_comp conv_involutive ideal_top_closed surjective_vector_top rectangle_eq)
lemma conv_atom:
"atom x ⟹ atom (x⇧T)"
by (metis conv_involutive conv_isotone symmetric_bot_closed)
lemma conv_atom_iff:
"atom x ⟷ atom (x⇧T)"
by (metis conv_atom conv_involutive)
lemma counterexample_different_atoms_top_disjoint:
"atom x ⟹ atom y ⟹ x ≠ y ⟹ x * top ⊓ y = bot"
nitpick[expect=genuine,card=4]
oops
lemma counterexample_different_univalent_atoms_top_disjoint:
"atom x ⟹ univalent x ⟹ atom y ⟹ univalent y ⟹ x ≠ y ⟹ x * top ⊓ y = bot"
nitpick[expect=genuine,card=4]
oops
lemma AB_card_4_1:
"a ≤ x ∧ a ≤ y ⟷ a ≤ x ⊔ y ∧ a ≤ x ⊓ y"
using le_supI1 by auto
lemma AB_card_4_2:
assumes "atom a"
shows "(a ≤ x ∧ ¬ a ≤ y) ∨ (¬ a ≤ x ∧ a ≤ y) ⟷ a ≤ x ⊔ y ∧ ¬ a ≤ x ⊓ y"
using assms atom_in_sup le_supI1 le_supI2 by auto
lemma AB_card_4_3:
assumes "atom a"
shows "¬ a ≤ x ∧ ¬ a ≤ y ⟷ ¬ a ≤ x ⊔ y ∧ ¬ a ≤ x ⊓ y"
using assms AB_card_4_2 by auto
lemma AB_card_5_1:
assumes "atom a"
and "a ≤ x⇧T * y ⊓ z"
shows "x * a ⊓ y ≤ x * z ⊓ y"
and "x * a ⊓ y ≠ bot"
proof -
show "x * a ⊓ y ≤ x * z ⊓ y"
using assms(2) comp_inf.mult_left_isotone mult_right_isotone by auto
show "x * a ⊓ y ≠ bot"
by (smt assms inf.left_commute inf.left_idem inf_absorb1 schroeder_1)
qed
lemma AB_card_5_2:
assumes "univalent x"
and "atom a"
and "atom b"
and "b ≤ x⇧T * y ⊓ z"
and "a ≠ b"
shows "(x * a ⊓ y) ⊓ (x * b ⊓ y) = bot"
and "x * a ⊓ y ≠ x * b ⊓ y"
proof -
show "(x * a ⊓ y) ⊓ (x * b ⊓ y) = bot"
by (metis assms(1-3,5) comp_inf.semiring.mult_zero_left inf.cobounded1 inf.left_commute inf.sup_monoid.add_commute semiring.mult_not_zero univalent_comp_left_dist_inf)
thus "x * a ⊓ y ≠ x * b ⊓ y"
using AB_card_5_1(2) assms(3,4) by fastforce
qed
lemma AB_card_6_0:
assumes "univalent x"
and "atom a"
and "a ≤ x"
and "atom b"
and "b ≤ x"
and "a ≠ b"
shows "a * top ⊓ b * top = bot"
proof -
have "a⇧T * b ≤ 1"
by (meson assms(1,3,5) comp_isotone conv_isotone dual_order.trans)
hence "a * top ⊓ b = bot"
by (metis assms(2,4,6) comp_inf.semiring.mult_zero_left comp_right_one inf.cobounded1 inf.cobounded2 inf.orderE schroeder_1)
thus ?thesis
using vector_bot_closed vector_export_comp by force
qed
lemma AB_card_6_1:
assumes "atom a"
and "a ≤ x ⊓ y * z⇧T"
shows "a * z ⊓ y ≤ x * z ⊓ y"
and "a * z ⊓ y ≠ bot"
proof -
show "a * z ⊓ y ≤ x * z ⊓ y"
using assms(2) inf.sup_left_isotone mult_left_isotone by auto
show "a * z ⊓ y ≠ bot"
by (metis assms inf.absorb2 inf.boundedE schroeder_2)
qed
lemma AB_card_6_2:
assumes "univalent x"
and "atom a"
and "a ≤ x ⊓ y * z⇧T"
and "atom b"
and "b ≤ x ⊓ y * z⇧T"
and "a ≠ b"
shows "(a * z ⊓ y) ⊓ (b * z ⊓ y) = bot"
and "a * z ⊓ y ≠ b * z ⊓ y"
proof -
have "(a * z ⊓ y) ⊓ (b * z ⊓ y) ≤ a * top ⊓ b * top"
by (meson comp_inf.comp_isotone comp_inf.ex231d inf.boundedE mult_right_isotone)
also have "... = bot"
using AB_card_6_0 assms by force
finally show "(a * z ⊓ y) ⊓ (b * z ⊓ y) = bot"
using le_bot by blast
thus "a * z ⊓ y ≠ b * z ⊓ y"
using AB_card_6_1(2) assms(4,5) by fastforce
qed
lemma nAB_conv:
"nAB x = nAB (x⇧T)"
proof (unfold num_atoms_below_def, rule bij_betw_same_icard)
show "bij_betw conv (AB x) (AB (x⇧T))"
proof (unfold bij_betw_def, rule conjI)
show "inj_on conv (AB x)"
by (metis (mono_tags, lifting) inj_onI conv_involutive)
show "conv ` AB x = AB (x⇧T)"
proof
show "conv ` AB x ⊆ AB (x⇧T)"
using conv_atom_iff conv_isotone by force
show "AB (x⇧T) ⊆ conv ` AB x"
proof
fix y
assume "y ∈ AB (x⇧T)"
hence "atom y ∧ y ≤ x⇧T"
by auto
hence "atom (y⇧T) ∧ y⇧T ≤ x"
using conv_atom_iff conv_order by force
hence "y⇧T ∈ AB x"
by auto
thus "y ∈ conv ` AB x"
by (metis (no_types, lifting) image_iff conv_involutive)
qed
qed
qed
qed
lemma domain_atom:
assumes "atom a"
shows "atom (a * top ⊓ 1)"
proof
show "a * top ⊓ 1 ≠ bot"
by (metis assms domain_vector_conv ex231a inf_vector_comp mult_left_zero vector_export_comp_unit)
next
show "∀y. y ≠ bot ∧ y ≤ a * top ⊓ 1 ⟶ y = a * top ⊓ 1"
proof (rule allI, rule impI)
fix y
assume 1: "y ≠ bot ∧ y ≤ a * top ⊓ 1"
hence 2: "y = 1 ⊓ y * a * top"
using dedekind_injective comp_associative coreflexive_idempotent coreflexive_symmetric inf.absorb2 inf.sup_monoid.add_commute by auto
hence "y * a ≠ bot"
using 1 comp_inf.semiring.mult_zero_right vector_bot_closed by force
hence "a = y * a"
using 1 by (metis assms comp_right_one coreflexive_comp_top_inf inf.boundedE mult_sub_right_one)
thus "y = a * top ⊓ 1"
using 2 inf.sup_monoid.add_commute by auto
qed
qed
lemma codomain_atom:
assumes "atom a"
shows "atom (top * a ⊓ 1)"
proof -
have "top * a ⊓ 1 = a⇧T * top ⊓ 1"
by (simp add: domain_vector_covector inf.sup_monoid.add_commute)
thus ?thesis
using domain_atom conv_atom assms by auto
qed
lemma atom_rectangle_atom_one_rep:
"(∀a . atom a ⟶ a * top * a ≤ a) ⟷ (∀a . atom a ∧ a ≤ 1 ⟶ a * top * a ≤ 1)"
proof
assume "∀a . atom a ⟶ a * top * a ≤ a"
thus "∀a . atom a ∧ a ≤ 1 ⟶ a * top * a ≤ 1"
by auto
next
assume 1: "∀a . atom a ∧ a ≤ 1 ⟶ a * top * a ≤ 1"
show "∀a . atom a ⟶ a * top * a ≤ a"
proof (rule allI, rule impI)
fix a
assume "atom a"
hence "atom (a * top ⊓ 1)"
by (simp add: domain_atom)
hence "(a * top ⊓ 1) * top * (a * top ⊓ 1) ≤ 1"
using 1 by simp
hence "a * top * a⇧T ≤ 1"
by (smt comp_associative conv_dist_comp coreflexive_symmetric ex231e inf_top.right_neutral symmetric_top_closed vector_export_comp_unit)
thus "a * top * a ≤ a"
by (smt comp_associative conv_dist_comp domain_vector_conv order.eq_iff ex231e inf.absorb2 inf.sup_monoid.add_commute mapping_one_closed symmetric_top_closed top_right_mult_increasing vector_export_comp_unit)
qed
qed
lemma AB_card_2_1:
assumes "a * top * a ≤ a"
shows "(a * top ⊓ 1) * top * (top * a ⊓ 1) = a"
by (metis assms comp_inf.vector_top_closed covector_comp_inf ex231d order.antisym inf_commute surjective_one_closed vector_export_comp_unit vector_top_closed mult_assoc)
lemma atomsimple_atom1simple:
"(∀a . atom a ⟶ top * a * top = top) ⟷ (∀a . atom a ∧ a ≤ 1 ⟶ top * a * top = top)"
proof
assume "∀a . atom a ⟶ top * a * top = top"
thus "∀a . atom a ∧ a ≤ 1 ⟶ top * a * top = top"
by simp
next
assume 1: "∀a . atom a ∧ a ≤ 1 ⟶ top * a * top = top"
show "∀a . atom a ⟶ top * a * top = top"
proof (rule allI, rule impI)
fix a
assume "atom a"
hence 2: "atom (a * top ⊓ 1)"
by (simp add: domain_atom)
have "top * (a * top ⊓ 1) * top = top * a * top"
using comp_associative vector_export_comp_unit by auto
thus "top * a * top = top"
using 1 2 by auto
qed
qed
lemma AB_card_2_2:
assumes "atom a"
and "a ≤ 1"
and "atom b"
and "b ≤ 1"
and "∀a . atom a ⟶ top * a * top = top"
shows "a * top * b * top ⊓ 1 = a" and "top * a * top * b ⊓ 1 = b"
proof -
show "a * top * b * top ⊓ 1 = a"
using assms(2,3,5) comp_associative coreflexive_comp_top_inf_one by auto
show "top * a * top * b ⊓ 1 = b"
using assms(1,4,5) epm_3 inf.sup_monoid.add_commute by auto
qed
abbreviation dom_cod :: "'a ⇒ 'a × 'a"
where "dom_cod a ≡ (a * top ⊓ 1, top * a ⊓ 1)"
lemma dom_cod_atoms_1:
"dom_cod ` AB top ⊆ AB 1 × AB 1"
proof
fix x
assume "x ∈ dom_cod ` AB top"
from this obtain a where 1: "atom a ∧ x = dom_cod a"
by auto
hence "a * top ⊓ 1 ∈ AB 1 ∧ top * a ⊓ 1 ∈ AB 1"
using domain_atom codomain_atom by auto
thus "x ∈ AB 1 × AB 1"
using 1 by auto
qed
end
class stone_relation_algebra_simple = stone_relation_algebra +
assumes simple: "x ≠ bot ⟶ simple x"
begin
lemma point_ideal_point:
"point x ⟷ ideal_point x"
using simple by fastforce
end
subsection ‹Atomic›
class stone_relation_algebra_atomic = stone_relation_algebra +
assumes atomic: "x ≠ bot ⟶ (∃a . atom a ∧ a ≤ x)"
begin
lemma AB_nonempty:
"x ≠ bot ⟹ AB x ≠ {}"
using atomic by fastforce
lemma AB_nonempty_iff:
"x ≠ bot ⟷ AB x ≠ {}"
using AB_nonempty AB_bot by blast
lemma atomsimple_simple:
"(∀a . a ≠ bot ⟶ top * a * top = top) ⟷ (∀a . atom a ⟶ top * a * top = top)"
proof
assume "∀a . a ≠ bot ⟶ top * a * top = top"
thus "∀a . atom a ⟶ top * a * top = top"
by simp
next
assume 1: "∀a . atom a ⟶ top * a * top = top"
show "∀a . a ≠ bot ⟶ top * a * top = top"
proof (rule allI, rule impI)
fix a
assume "a ≠ bot"
from this atomic obtain b where 2: "atom b ∧ b ≤ a"
by auto
hence "top * b * top = top"
using 1 by auto
thus "top * a * top = top"
using 2 by (metis order.antisym mult_left_isotone mult_right_isotone top.extremum)
qed
qed
lemma AB_card_2_3:
assumes "a ≠ bot"
and "a ≤ 1"
and "b ≠ bot"
and "b ≤ 1"
and "∀a . a ≠ bot ⟶ top * a * top = top"
shows "a * top * b * top ⊓ 1 = a" and "top * a * top * b ⊓ 1 = b"
proof -
show "a * top * b * top ⊓ 1 = a"
using assms(2,3,5) comp_associative coreflexive_comp_top_inf_one by auto
show "top * a * top * b ⊓ 1 = b"
using assms(1,4,5) epm_3 inf.sup_monoid.add_commute by auto
qed
lemma injective_down_closed:
"x ≤ y ⟹ injective y ⟹ injective x"
using conv_isotone mult_isotone by fastforce
lemma univalent_down_closed:
"x ≤ y ⟹ univalent y ⟹ univalent x"
using conv_isotone mult_isotone by fastforce
lemma nAB_bot_iff:
"x = bot ⟷ nAB x = 0"
by (smt (verit, best) icard_0_eq AB_nonempty_iff num_atoms_below_def)
text ‹
It is unclear if ‹atomic› is necessary for the following two results, but it seems likely.
›
lemma nAB_univ_comp_meet:
assumes "univalent x"
shows "nAB (x⇧T * y ⊓ z) ≤ nAB (x * z ⊓ y)"
proof (unfold num_atoms_below_def, rule icard_image_part_le)
show "∀a ∈ AB (x⇧T * y ⊓ z) . AB (x * a ⊓ y) ⊆ AB (x * z ⊓ y)"
proof
fix a
assume "a ∈ AB (x⇧T * y ⊓ z)"
hence "x * a ⊓ y ≤ x * z ⊓ y"
using AB_card_5_1(1) by auto
thus "AB (x * a ⊓ y) ⊆ AB (x * z ⊓ y)"
using AB_iso by blast
qed
next
show "∀a ∈ AB (x⇧T * y ⊓ z) . AB (x * a ⊓ y) ≠ {}"
proof
fix a
assume "a ∈ AB (x⇧T * y ⊓ z)"
hence "x * a ⊓ y ≠ bot"
using AB_card_5_1(2) by auto
thus "AB (x * a ⊓ y) ≠ {}"
using atomic by fastforce
qed
next
show "∀a ∈ AB (x⇧T * y ⊓ z) . ∀b ∈ AB (x⇧T * y ⊓ z) . a ≠ b ⟶ AB (x * a ⊓ y) ∩ AB (x * b ⊓ y) = {}"
proof (intro ballI, rule impI)
fix a b
assume "a ∈ AB (x⇧T * y ⊓ z)" "b ∈ AB (x⇧T * y ⊓ z)" "a ≠ b"
hence "(x * a ⊓ y) ⊓ (x * b ⊓ y) = bot"
using assms AB_card_5_2(1) by auto
thus "AB (x * a ⊓ y) ∩ AB (x * b ⊓ y) = {}"
using AB_bot AB_dist_inf by blast
qed
qed
lemma nAB_univ_meet_comp:
assumes "univalent x"
shows "nAB (x ⊓ y * z⇧T) ≤ nAB (x * z ⊓ y)"
proof (unfold num_atoms_below_def, rule icard_image_part_le)
show "∀a ∈ AB (x ⊓ y * z⇧T) . AB (a * z ⊓ y) ⊆ AB (x * z ⊓ y)"
proof
fix a
assume "a ∈ AB (x ⊓ y * z⇧T)"
hence "a * z ⊓ y ≤ x * z ⊓ y"
using AB_card_6_1(1) by auto
thus "AB (a * z ⊓ y) ⊆ AB (x * z ⊓ y)"
using AB_iso by blast
qed
next
show "∀a ∈ AB (x ⊓ y * z⇧T) . AB (a * z ⊓ y) ≠ {}"
proof
fix a
assume "a ∈ AB (x ⊓ y * z⇧T)"
hence "a * z ⊓ y ≠ bot"
using AB_card_6_1(2) by auto
thus "AB (a * z ⊓ y) ≠ {}"
using atomic by fastforce
qed
next
show "∀a ∈ AB (x ⊓ y * z⇧T) . ∀b ∈ AB (x ⊓ y * z⇧T) . a ≠ b ⟶ AB (a * z ⊓ y) ∩ AB (b * z ⊓ y) = {}"
proof (intro ballI, rule impI)
fix a b
assume "a ∈ AB (x ⊓ y * z⇧T)" "b ∈ AB (x ⊓ y * z⇧T)" "a ≠ b"
hence "(a * z ⊓ y) ⊓ (b * z ⊓ y) = bot"
using assms AB_card_6_2(1) by auto
thus "AB (a * z ⊓ y) ∩ AB (b * z ⊓ y) = {}"
using AB_bot AB_dist_inf by blast
qed
qed
end
subsection ‹Atom-rectangular›
class stone_relation_algebra_atomrect = stone_relation_algebra +
assumes atomrect: "atom a ⟶ rectangle a"
begin
lemma atomrect_eq:
"atom a ⟹ a * top * a = a"
by (simp add: order.antisym ex231d atomrect)
lemma AB_card_2_4:
assumes "atom a"
shows "(a * top ⊓ 1) * top * (top * a ⊓ 1) = a"
by (simp add: assms AB_card_2_1 atomrect)
lemma simple_atom_2:
assumes "atom a"
and "a ≤ 1"
and "atom b"
and "b ≤ 1"
and "x ≠ bot"
and "x ≤ a * top * b"
shows "x = a * top * b"
proof -
have 1: "x * top ⊓ 1 ≠ bot"
by (metis assms(5) inf_top_right le_bot top_right_mult_increasing vector_bot_closed vector_export_comp_unit)
have "x * top ⊓ 1 ≤ a * top * b * top ⊓ 1"
using assms(6) comp_inf.comp_isotone comp_isotone by blast
also have "... ≤ a * top ⊓ 1"
by (metis comp_associative comp_inf.mult_right_isotone inf.sup_monoid.add_commute mult_right_isotone top.extremum)
also have "... = a"
by (simp add: assms(2) coreflexive_comp_top_inf_one)
finally have 2: "x * top ⊓ 1 = a"
using 1 by (simp add: assms(1) domain_atom)
have 3: "top * x ⊓ 1 ≠ bot"
using 1 by (metis schroeder_1 schroeder_2 surjective_one_closed symmetric_top_closed total_one_closed)
have "top * x ⊓ 1 ≤ top * a * top * b ⊓ 1"
by (metis assms(6) comp_associative comp_inf.comp_isotone mult_right_isotone reflexive_one_closed)
also have "... ≤ top * b ⊓ 1"
using inf.sup_mono mult_left_isotone top_greatest by blast
also have "... = b"
using assms(4) epm_3 inf.sup_monoid.add_commute by auto
finally have "top * x ⊓ 1 = b"
using 3 by (simp add: assms(3) codomain_atom)
hence "a * top * b = x * top * x"
using 2 by (smt abel_semigroup.commute covector_comp_inf inf.abel_semigroup_axioms inf_top_right surjective_one_closed vector_export_comp_unit vector_top_closed mult_assoc)
also have "... = a * top * b * top * (x ⊓ a * top * b)"
using assms(6) calculation inf_absorb1 by auto
also have "... ≤ a * top * (x ⊓ a * top * b)"
by (metis comp_associative comp_inf_covector inf.idem inf.order_iff mult_right_isotone)
also have "... ≤ a * top * (x ⊓ a * top)"
using comp_associative comp_inf.mult_right_isotone mult_right_isotone by auto
also have "... = a * top * a⇧T * x"
by (metis comp_associative comp_inf_vector inf_top.left_neutral)
also have "... = a * top * a * x"
by (simp add: assms(2) coreflexive_symmetric)
also have "... = a * x"
by (simp add: assms(1) atomrect_eq)
also have "... ≤ x"
using assms(2) mult_left_isotone by fastforce
finally show ?thesis
using assms(6) order.antisym by blast
qed
lemma dom_cod_inj_atoms:
"inj_on dom_cod (AB top)"
proof
fix a b
assume 1: "a ∈ AB top" "b ∈ AB top" "dom_cod a = dom_cod b"
have "a = a * top * a"
using 1 atomrect_eq by auto
also have "... = (a * top ⊓ 1) * top * (top * a ⊓ 1)"
using calculation AB_card_2_1 by auto
also have "... = (b * top ⊓ 1) * top * (top * b ⊓ 1)"
using 1 by simp
also have "... = b * top * b"
using abel_semigroup.commute comp_inf_covector inf.abel_semigroup_axioms vector_export_comp_unit mult_assoc by fastforce
also have "... = b"
using 1 atomrect_eq by auto
finally show "a = b"
.
qed
lemma finite_AB_iff:
"finite (AB top) ⟷ finite (AB 1)"
proof
have "AB 1 ⊆ AB top"
by auto
thus "finite (AB top) ⟹ finite (AB 1)"
by (meson finite_subset)
next
assume 1: "finite (AB 1)"
show "finite (AB top)"
proof (rule inj_on_finite)
show "inj_on dom_cod (AB top)"
using dom_cod_inj_atoms by blast
show "dom_cod ` AB top ⊆ AB 1 × AB 1"
using dom_cod_atoms_1 by blast
show "finite (AB 1 × AB 1)"
using 1 by blast
qed
qed
lemma nAB_top_1:
"nAB top ≤ nAB 1 * nAB 1"
proof (unfold num_atoms_below_def icard_cartesian_product[THEN sym], rule icard_inj_on_le)
show "inj_on dom_cod (AB top)"
using dom_cod_inj_atoms by blast
show "dom_cod ` AB top ⊆ AB 1 × AB 1"
using dom_cod_atoms_1 by blast
qed
lemma atom_vector_injective:
assumes "atom x"
shows "injective (x * top)"
proof -
have "atom (x * top ⊓ 1)"
by (simp add: assms domain_atom)
hence "(x * top ⊓ 1) * top * (x * top ⊓ 1) ≤ 1"
using atom_rectangle_atom_one_rep atomrect by auto
hence "x * top * x⇧T ≤ 1"
by (smt comp_associative conv_dist_comp coreflexive_symmetric ex231e inf_top.right_neutral symmetric_top_closed vector_export_comp_unit)
thus "injective (x * top)"
by (metis comp_associative conv_dist_comp symmetric_top_closed vector_top_closed)
qed
lemma atom_injective:
"atom x ⟹ injective x"
by (metis atom_vector_injective comp_associative conv_dist_comp dual_order.trans mult_right_isotone symmetric_top_closed top_left_mult_increasing)
lemma atom_covector_univalent:
"atom x ⟹ univalent (top * x)"
by (metis comp_associative conv_involutive atom_vector_injective conv_atom_iff conv_dist_comp symmetric_top_closed)
lemma atom_univalent:
"atom x ⟹ univalent x"
using atom_injective conv_atom_iff univalent_conv_injective by blast
lemma counterexample_atom_simple:
"atom x ⟹ simple x"
nitpick[expect=genuine,card=3]
oops
lemma symmetric_atom_below_1:
assumes "atom x"
and "x = x⇧T"
shows "x ≤ 1"
proof -
have "x = x * top * x⇧T"
using assms atomrect_eq by auto
also have "... ≤ 1"
by (metis assms(1) atom_vector_injective conv_dist_comp equivalence_top_closed ideal_top_closed mult_assoc)
finally show ?thesis
.
qed
end
subsection ‹Atomic and Atom-Rectangular›
class stone_relation_algebra_atomic_atomrect = stone_relation_algebra_atomic + stone_relation_algebra_atomrect
begin
lemma point_dense:
assumes "x ≠ bot"
and "x ≤ 1"
shows "∃a . a ≠ bot ∧ a * top * a ≤ 1 ∧ a ≤ x"
proof -
from atomic obtain a where 1: "atom a ∧ a ≤ x"
using assms(1) by auto
hence "a * top * a ≤ a"
by (simp add: atomrect)
also have "... ≤ 1"
using 1 assms(2) order_trans by blast
finally show ?thesis
using 1 by blast
qed
end
subsection ‹Atom-simple›
class stone_relation_algebra_atomsimple = stone_relation_algebra +
assumes atomsimple: "atom a ⟶ simple a"
begin
lemma AB_card_2_5:
assumes "atom a"
and "a ≤ 1"
and "atom b"
and "b ≤ 1"
shows "a * top * b * top ⊓ 1 = a" and "top * a * top * b ⊓ 1 = b"
using assms AB_card_2_2 atomsimple by auto
lemma simple_atom_1:
"atom a ⟹ atom b ⟹ a * top * b ≠ bot"
by (metis order.antisym atomsimple bot_least comp_associative mult_left_zero top_right_mult_increasing)
end
subsection ‹Atomic and Atom-simple›
class stone_relation_algebra_atomic_atomsimple = stone_relation_algebra_atomic + stone_relation_algebra_atomsimple
begin
subclass stone_relation_algebra_simple
apply unfold_locales
using atomsimple atomsimple_simple by blast
lemma AB_card_2_6:
assumes "a ≠ bot"
and "a ≤ 1"
and "b ≠ bot"
and "b ≤ 1"
shows "a * top * b * top ⊓ 1 = a" and "top * a * top * b ⊓ 1 = b"
using assms AB_card_2_3 simple atomsimple_simple by auto
lemma dom_cod_atoms_2:
"AB 1 × AB 1 ⊆ dom_cod ` AB top"
proof
fix x
assume "x ∈ AB 1 × AB 1"
from this obtain a b where 1: "atom a ∧ a ≤ 1 ∧ atom b ∧ b ≤ 1 ∧ x = (a,b)"
by auto
hence "a * top * b ≠ bot"
by (simp add: simple_atom_1)
from this obtain c where 2: "atom c ∧ c ≤ a * top * b"
using atomic by blast
hence "c * top ⊓ 1 ≤ a * top ⊓ 1"
by (smt comp_inf.comp_isotone inf.boundedE inf.orderE inf_vector_comp reflexive_one_closed top_right_mult_increasing)
also have "... = a"
using 1 by (simp add: coreflexive_comp_top_inf_one)
finally have 3: "c * top ⊓ 1 = a"
using 1 2 domain_atom by simp
have "top * c ≤ top * b"
using 2 3 by (smt comp_associative comp_inf.reflexive_top_closed comp_inf.vector_top_closed comp_inf_covector comp_isotone simple vector_export_comp_unit)
hence "top * c ⊓ 1 ≤ b"
using 1 by (smt epm_3 inf.cobounded1 inf.left_commute inf.orderE injective_one_closed reflexive_one_closed)
hence "top * c ⊓ 1 = b"
using 1 2 codomain_atom by simp
hence "dom_cod c = x"
using 1 3 by simp
thus "x ∈ dom_cod ` AB top"
using 2 by auto
qed
lemma dom_cod_atoms:
"AB 1 × AB 1 = dom_cod ` AB top"
using dom_cod_atoms_2 dom_cod_atoms_1 by blast
end
subsection ‹Atom-rectangular and Atom-simple›
class stone_relation_algebra_atomrect_atomsimple = stone_relation_algebra_atomrect + stone_relation_algebra_atomsimple
begin
lemma simple_atom:
assumes "atom a"
and "a ≤ 1"
and "atom b"
and "b ≤ 1"
shows "atom (a * top * b)"
using assms simple_atom_1 simple_atom_2 by auto
lemma nAB_top_2:
"nAB 1 * nAB 1 ≤ nAB top"
proof (unfold num_atoms_below_def icard_cartesian_product[THEN sym], rule icard_inj_on_le)
let ?f = "λ(a,b) . a * top * b"
show "inj_on ?f (AB 1 × AB 1)"
proof
fix x y
assume "x ∈ AB 1 × AB 1" "y ∈ AB 1 × AB 1"
from this obtain a b c d where 1: "atom a ∧ a ≤ 1 ∧ atom b ∧ b ≤ 1 ∧ x = (a,b) ∧ atom c ∧ c ≤ 1 ∧ atom d ∧ d ≤ 1 ∧ y = (c,d)"
by auto
assume "?f x = ?f y"
hence 2: "a * top * b = c * top * d"
using 1 by auto
hence 3: "a = c"
using 1 by (smt atomsimple comp_associative coreflexive_comp_top_inf_one)
have "b = d"
using 1 2 by (smt atomsimple comp_associative epm_3 injective_one_closed)
thus "x = y"
using 1 3 by simp
qed
show "?f ` (AB 1 × AB 1) ⊆ AB top"
proof
fix x
assume "x ∈ ?f ` (AB 1 × AB 1)"
from this obtain a b where 4: "atom a ∧ a ≤ 1 ∧ atom b ∧ b ≤ 1 ∧ x = a * top * b"
by auto
hence "a * top * b ∈ AB top"
using simple_atom by simp
thus "x ∈ AB top"
using 4 by simp
qed
qed
lemma nAB_top:
"nAB 1 * nAB 1 = nAB top"
using nAB_top_1 nAB_top_2 by auto
lemma atom_covector_mapping:
"atom a ⟹ mapping (top * a)"
using atom_covector_univalent atomsimple by blast
lemma atom_covector_regular:
"atom a ⟹ regular (top * a)"
by (simp add: atom_covector_mapping mapping_regular)
lemma atom_vector_bijective:
"atom a ⟹ bijective (a * top)"
using atom_vector_injective comp_associative atomsimple by auto
lemma atom_vector_regular:
"atom a ⟹ regular (a * top)"
by (simp add: atom_vector_bijective bijective_regular)
lemma atom_rectangle_regular:
"atom a ⟹ regular (a * top * a)"
by (smt atom_covector_regular atom_vector_regular comp_associative pp_dist_comp regular_closed_top)
lemma atom_regular:
"atom a ⟹ regular a"
using atom_rectangle_regular atomrect_eq by auto
end
subsection ‹Atomic, Atom-rectangular and Atom-simple›
class stone_relation_algebra_atomic_atomrect_atomsimple = stone_relation_algebra_atomic + stone_relation_algebra_atomrect + stone_relation_algebra_atomsimple
begin
subclass stone_relation_algebra_atomic_atomrect ..
subclass stone_relation_algebra_atomic_atomsimple ..
subclass stone_relation_algebra_atomrect_atomsimple ..
lemma nAB_atom_iff:
"atom a ⟷ nAB a = 1"
proof
assume "atom a"
thus "nAB a = 1"
by (simp add: nAB_atom)
next
assume "nAB a = 1"
from this obtain b where 1: "AB a = {b}"
using icard_1_imp_singleton num_atoms_below_def one_eSuc by fastforce
hence 2: "atom b ∧ b ≤ a"
by auto
hence 3: "AB (a ⊓ b) = {b}"
by fastforce
have "AB (a ⊓ b) ∪ AB (a ⊓ -b) = AB a ∧ AB (a ⊓ b) ∩ AB (a ⊓ -b) = {}"
using AB_split_2 AB_split_2_disjoint by simp
hence "{b} ∪ AB (a ⊓ -b) = {b} ∧ {b} ∩ AB (a ⊓ -b) = {}"
using 1 3 by simp
hence "AB (a ⊓ -b) = {}"
by auto
hence "a ⊓ -b = bot"
using AB_nonempty_iff by blast
hence "a ≤ b"
using 2 atom_regular pseudo_complement by auto
thus "atom a"
using 2 by auto
qed
end
subsection ‹Finitely Many Atoms›
class stone_relation_algebra_finiteatoms = stone_relation_algebra +
assumes finiteatoms: "finite { a . atom a }"
begin
lemma finite_AB:
"finite (AB x)"
using finite_Collect_conjI finiteatoms by force
lemma nAB_top_finite:
"nAB top ≠ ∞"
by (smt (verit, best) finite_AB icard_infinite_conv num_atoms_below_def)
end
subsection ‹Atomic and Finitely Many Atoms›
class stone_relation_algebra_atomic_finiteatoms = stone_relation_algebra_atomic + stone_relation_algebra_finiteatoms
begin
lemma finite_ideal_points:
"finite { p . ideal_point p }"
proof (cases "bot = top")
case True
hence "⋀p . ideal_point p ⟹ p = bot"
using le_bot top.extremum by blast
hence "{ p . ideal_point p } ⊆ {bot}"
by auto
thus ?thesis
using finite_subset by auto
next
case False
let ?p = "{ p . ideal_point p }"
show 0: "finite ?p"
proof (rule finite_image_part_le)
show "∀x∈?p . AB x ⊆ AB top"
using top.extremum by auto
have "∀x∈?p . x ≠ bot"
using False by auto
thus "∀x∈?p . AB x ≠ {}"
using AB_nonempty by auto
show "∀x∈?p . ∀y∈?p . x ≠ y ⟶ AB x ∩ AB y = {}"
proof (intro ballI, rule impI, rule ccontr)
fix x y
assume "x ∈ ?p" "y ∈ ?p" "x ≠ y"
hence 1: "x ⊓ y = bot"
by (simp add: different_ideal_points_disjoint)
assume "AB x ∩ AB y ≠ {}"
from this obtain a where "atom a ∧ a ≤ x ∧ a ≤ y"
by auto
thus False
using 1 by (metis comp_inf.semiring.mult_zero_left inf.absorb2 inf.sup_monoid.add_assoc)
qed
show "finite (AB top)"
using finite_AB by blast
qed
qed
end
subsection ‹Atom-rectangular and Finitely Many Atoms›
class stone_relation_algebra_atomrect_finiteatoms = stone_relation_algebra_atomrect + stone_relation_algebra_finiteatoms
subsection ‹Atomic, Atom-rectangular and Finitely Many Atoms›
class stone_relation_algebra_atomic_atomrect_finiteatoms = stone_relation_algebra_atomic + stone_relation_algebra_atomrect + stone_relation_algebra_finiteatoms
begin
subclass stone_relation_algebra_atomic_atomrect ..
subclass stone_relation_algebra_atomic_finiteatoms ..
subclass stone_relation_algebra_atomrect_finiteatoms ..
lemma counterexample_nAB_atom_iff:
"atom x ⟷ nAB x = 1"
nitpick[expect=genuine,card=3]
oops
lemma counterexample_nAB_top_iff_eq:
"nAB x = nAB top ⟷ x = top"
nitpick[expect=genuine,card=3]
oops
lemma counterexample_nAB_top_iff_leq:
"nAB top ≤ nAB x ⟷ x = top"
nitpick[expect=genuine,card=3]
oops
end
subsection ‹Atom-simple and Finitely Many Atoms›
class stone_relation_algebra_atomsimple_finiteatoms = stone_relation_algebra_atomsimple + stone_relation_algebra_finiteatoms
subsection ‹Atomic, Atom-simple and Finitely Many Atoms›
class stone_relation_algebra_atomic_atomsimple_finiteatoms = stone_relation_algebra_atomic + stone_relation_algebra_atomsimple + stone_relation_algebra_finiteatoms
begin
subclass stone_relation_algebra_atomic_atomsimple ..
subclass stone_relation_algebra_atomic_finiteatoms ..
subclass stone_relation_algebra_atomsimple_finiteatoms ..
lemma nAB_top_2:
"nAB 1 * nAB 1 ≤ nAB top"
proof (unfold num_atoms_below_def icard_cartesian_product[THEN sym], rule surj_icard_le)
show "AB 1 × AB 1 ⊆ dom_cod ` AB top"
using dom_cod_atoms_2 by blast
qed
lemma counterexample_nAB_atom_iff_2:
"atom x ⟷ nAB x = 1"
nitpick[expect=genuine,card=6]
oops
lemma counterexample_nAB_top_iff_eq_2:
"nAB x = nAB top ⟷ x = top"
nitpick[expect=genuine,card=6]
oops
lemma counterexample_nAB_top_iff_leq_2:
"nAB top ≤ nAB x ⟷ x = top"
nitpick[expect=genuine,card=6]
oops
lemma counterexample_nAB_atom_top_iff_leq_2:
"(atom x ⟷ nAB x = 1) ∨ (nAB y = nAB top ⟷ y = top) ∨ (nAB top ≤ nAB y ⟷ y = top)"
nitpick[expect=genuine,card=6]
oops
end
subsection ‹Atom-rectangular, Atom-simple and Finitely Many Atoms›
class stone_relation_algebra_atomrect_atomsimple_finiteatoms = stone_relation_algebra_atomrect + stone_relation_algebra_atomsimple + stone_relation_algebra_finiteatoms
begin
subclass stone_relation_algebra_atomrect_atomsimple ..
subclass stone_relation_algebra_atomrect_finiteatoms ..
subclass stone_relation_algebra_atomsimple_finiteatoms ..
end
subsection ‹Atomic, Atom-rectangular, Atom-simple and Finitely Many Atoms›
class stone_relation_algebra_atomic_atomrect_atomsimple_finiteatoms = stone_relation_algebra_atomic + stone_relation_algebra_atomrect + stone_relation_algebra_atomsimple + stone_relation_algebra_finiteatoms
begin
subclass stone_relation_algebra_atomic_atomrect_atomsimple ..
subclass stone_relation_algebra_atomic_atomrect_finiteatoms ..
subclass stone_relation_algebra_atomic_atomsimple_finiteatoms ..
subclass stone_relation_algebra_atomrect_atomsimple_finiteatoms ..
lemma all_regular:
"regular x"
proof (cases "x = bot")
case True
thus ?thesis
by simp
next
case False
hence 1: "AB x ≠ {}"
using AB_nonempty by blast
have 2: "finite (AB x)"
using finite_AB by blast
have 3: "regular (Sup_fin (AB x))"
proof (rule finite_ne_subset_induct')
show "finite (AB x)"
using 2 by simp
show "AB x ≠ {}"
using 1 by simp
show "AB x ⊆ AB top"
by auto
show "⋀a . a ∈ AB top ⟹ Sup_fin {a} = --Sup_fin {a}"
using atom_regular by auto
show "⋀a F . finite F ⟹ F ≠ {} ⟹ F ⊆ AB top ⟹ a ∈ AB top ⟹ a ∉ F ⟹ Sup_fin F = --Sup_fin F ⟹ Sup_fin (insert a F) = --Sup_fin (insert a F)"
using atom_regular by auto
qed
have "x ⊓ -Sup_fin (AB x) = bot"
proof (rule ccontr)
assume "x ⊓ -Sup_fin (AB x) ≠ bot"
from this obtain b where 4: "atom b ∧ b ≤ x ⊓ -Sup_fin (AB x)"
using atomic by blast
hence "b ≤ Sup_fin (AB x)"
using Sup_fin.coboundedI 2 by force
thus "False"
using 4 atom_in_p_xor by auto
qed
hence 5: "x ≤ Sup_fin (AB x)"
using 3 by (simp add: pseudo_complement)
have "Sup_fin (AB x) ≤ x"
using 1 2 Sup_fin.boundedI by fastforce
thus ?thesis
using 3 5 order.antisym by force
qed