Theory Cardinality

theory Cardinality

imports "List-Infinite.InfiniteSet2" Representation

begin

unbundle (in uminus) no uminus_syntax


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