Theory Mono_Atomic

section ‹Mono-Atomic Elements›

theory Mono_Atomic

imports Stone_Relation_Algebras.Relation_Algebras

begin

text ‹
This theory defines mono-atomic elements in a bounded semilattice and shows that they correspond to join-irreducible elements under the divisibility axioms A1--A17 of \cite{Cegielski1989}.
In the model of natural numbers both types of elements correspond to prime powers.
›

subsection ‹Mono-atomic›

context order_bot
begin

text ‹
Divisibility axioms A1 (reflexivity), A2 (antisymmetry), A3 (transitivity) and A6 (least element) are the axioms of class ‹order_bot›, so not mentioned explicitly.
›

text ‹
An ‹atom› in a partial order is an element that is strictly above only the least element ‹bot›.
›

definition "atom a                       ≡ a ≠ bot ∧ (∀x . x ≤ a ⟶ x = bot ∨ x = a)"
abbreviation "atom_below a x             ≡ atom a ∧ a ≤ x"

text ‹
A mono-atomic element has exactly one atom below it.
›

definition "mono_atomic x                ≡ (∃!a . atom_below a x)"
definition "mono_atomic_with x a         ≡ atom_below a x ∧ (∀b . atom_below b x ⟶ b = a)"
abbreviation "mono_atomic_below x y      ≡ mono_atomic x ∧ x ≤ y"
abbreviation "mono_atomic_above x y      ≡ mono_atomic x ∧ y ≤ x"
definition "mono_atomic_above_or_bot x y ≡ x = bot ∨ mono_atomic_above x y"

text ‹
Divisibility axiom A11 (atomicity) states that every element except ‹bot› is above some atom.
›

abbreviation A11_atomic            :: "'a ⇒ bool" where "A11_atomic _            ≡ (∀x . x ≠ bot ⟶ (∃a . atom_below a x))"

lemma mono_atomic_above:
  "mono_atomic x ⟷ (∃a . mono_atomic_with x a)"
  by (metis mono_atomic_with_def mono_atomic_def)

text ‹
Among others, the following divisibility axioms are considered in \cite{Cegielski1989}.
In the model of natural numbers,
\begin{itemize}
\item A7 (pre-f-decomposability) expresses that every number $x$ is the least upper bound of the prime powers below $x$;
\item A8 (fibered) expresses that the prime powers can be partitioned into chains;
\item A9 (f-decomposability) expresses that for every number $x$ above an atom $a$ there is a maximal prime power of $a$ below $x$;
\item A14 (truncability) express that the prime powers contained in a number $y$ can be restricted to those whose atoms are not below a number $x$.
\end{itemize}
Their definitions are based on join-irreducible elements and given in class ‹bounded_semilattice_sup_bot› below.
Here we introduce corresponding axioms B7, B8, B9 and B14 based on mono-atomic elements.
›

abbreviation B7_pre_f_decomposable :: "'a ⇒ bool" where "B7_pre_f_decomposable _ ≡ (∀x y . (∀z . mono_atomic_below z x ⟶ z ≤ y) ⟶ x ≤ y)"
abbreviation B8_fibered            :: "'a ⇒ bool" where "B8_fibered _            ≡ (∀x y z . mono_atomic x ∧ mono_atomic y ∧ mono_atomic z ∧ ((x ≤ z ∧ y ≤ z) ∨ (z ≤ x ∧ z ≤ y)) ⟶ x ≤ y ∨ y ≤ x)"
abbreviation B9_f_decomposable     :: "'a ⇒ bool" where "B9_f_decomposable _     ≡ (∀x a . atom a ⟶ (∃z . mono_atomic_above_or_bot z a ∧ z ≤ x ∧ (∀w . mono_atomic_above_or_bot w a ∧ w ≤ x ⟶ w ≤ z)))"

text ‹
Function ‹mval› returns the value whose existence is asserted by axiom B9.
›

definition "mval a x ≡ SOME z . mono_atomic_above_or_bot z a ∧ z ≤ x ∧ (∀w . mono_atomic_above_or_bot w a ∧ w ≤ x ⟶ w ≤ z)"

lemma mval_char:
  assumes "B9_f_decomposable _"
      and "atom a"
    shows "mono_atomic_above_or_bot (mval a x) a ∧ mval a x ≤ x ∧ (∀w . mono_atomic_above_or_bot w a ∧ w ≤ x ⟶ w ≤ mval a x)"
proof -
  obtain z where "mono_atomic_above_or_bot z a ∧ z ≤ x ∧ (∀w . mono_atomic_above_or_bot w a ∧ w ≤ x ⟶ w ≤ z)"
    using assms by blast
  thus ?thesis
    using mval_def someI by simp
qed

lemma mval_unique:
  assumes "B9_f_decomposable _"
      and "atom a"
      and "mono_atomic_above_or_bot z a ∧ z ≤ x ∧ (∀w . mono_atomic_above_or_bot w a ∧ w ≤ x ⟶ w ≤ z)"
    shows "z = mval a x"
  by (simp add: assms dual_order.antisym mval_char)

lemma atom_below_mval:
  assumes "B9_f_decomposable _"
      and "atom a"
      and "a ≤ x"
    shows "a ≤ mval a x"
proof -
  have "mono_atomic_above_or_bot a a"
    using assms(2) atom_def mono_atomic_above_or_bot_def mono_atomic_def by auto
  thus ?thesis
    by (simp add: assms mval_char)
qed

abbreviation B14_truncability      :: "'a ⇒ bool" where "B14_truncability _      ≡ (∀x y . ∃ z . ∀a . atom a ⟶ (if a ≤ x then mval a z = bot else mval a z = mval a y))"

text ‹
Function ‹mtrunc› returns the value whose existence is asserted by axiom B14.
›

definition "mtrunc x y ≡ SOME z . ∀a . atom a ⟶ (if a ≤ x then mval a z = bot else mval a z = mval a y)"

lemma mtrunc_char:
  assumes "B14_truncability _"
    shows "∀a . atom a ⟶ (if a ≤ x then mval a (mtrunc x y) = bot else mval a (mtrunc x y) = mval a y)"
proof -
  obtain z where "∀a . atom a ⟶ (if a ≤ x then mval a z = bot else mval a z = mval a y)"
    using assms by blast
  thus ?thesis
    by (smt mtrunc_def someI)
qed

lemma mtrunc_char_1:
  assumes "B14_truncability _"
      and "atom a"
      and "a ≤ x"
    shows "mval a (mtrunc x y) = bot"
  by (simp add: assms mtrunc_char)

lemma mtrunc_char_2:
  assumes "B14_truncability _"
      and "atom a"
      and "¬ a ≤ x"
    shows "mval a (mtrunc x y) = mval a y"
  by (simp add: assms mtrunc_char)

lemma mtrunc_unique:
  assumes "B14_truncability _"
      and "∀a . atom a ⟶ (if a ≤ x then mval a z = bot else mval a z = mval a y)"
      and "atom a"
    shows "mval a z = mval a (mtrunc x y)"
  by (smt (z3) assms mtrunc_char)

lemma lesseq_iff_mval_below:
  assumes "B7_pre_f_decomposable _"
      and "B9_f_decomposable _"
      and "atom a"
    shows "x ≤ y ⟷ (∀a . atom a ⟶ mval a x ≤ y)"
proof (rule iffI)
  assume 1: "x ≤ y"
  show "∀a . atom a ⟶ mval a x ≤ y"
  proof (rule allI, rule impI)
    fix a
    assume "atom a"
    thus "mval a x ≤ y"
      using 1 assms(2) dual_order.trans mval_char by blast
  qed
next
  assume 2: "∀a . atom a ⟶ mval a x ≤ y"
  have "∀z . mono_atomic_below z x ⟶ z ≤ y"
  proof (rule allI, rule impI)
    fix z
    assume 3: "mono_atomic_below z x"
    from this obtain a where 4: "atom_below a z"
      using mono_atomic_def by blast
    hence "z ≤ mval a x"
      using 3 assms(2) mono_atomic_above_or_bot_def mval_char by auto
    thus "z ≤ y"
      using 2 4 by auto
  qed
  thus "x ≤ y"
    using assms(1) by blast
qed

end

subsection ‹Join-irreducible›

context bounded_semilattice_sup_bot
begin

text ‹
Divisibility axioms A1 (reflexivity), A2 (antisymmetry), A3 (transitivity), A5 (least upper bound) and A6 (least element) are the axioms of class ‹bounded_semilattice_sup_bot›, so not mentioned explicitly.
›

text ‹
A join-irreducible element cannot be expressed as the join of two incomparable elements.
›

definition "join_irreducible x                ≡ x ≠ bot ∧ (∀y z . x = y ⊔ z ⟶ x = y ∨ x = z)"
abbreviation "join_irreducible_below x y      ≡ join_irreducible x ∧ x ≤ y"
abbreviation "join_irreducible_above x y      ≡ join_irreducible x ∧ y ≤ x"
definition "join_irreducible_above_or_bot x y ≡ x = bot ∨ join_irreducible_above x y"

text ‹
Divisibility axioms A7, A8 and A9 based on join-irreducible elements are introduced here; axiom A14 is not needed for this development.
›

abbreviation A7_pre_f_decomposable :: "'a ⇒ bool" where "A7_pre_f_decomposable _ ≡ (∀x y . (∀z . join_irreducible_below z x ⟶ z ≤ y) ⟶ x ≤ y)"
abbreviation A8_fibered            :: "'a ⇒ bool" where "A8_fibered _            ≡ (∀x y z . join_irreducible x ∧ join_irreducible y ∧ join_irreducible z ∧ ((x ≤ z ∧ y ≤ z) ∨ (z ≤ x ∧ z ≤ y)) ⟶ x ≤ y ∨ y ≤ x)"
abbreviation A9_f_decomposable     :: "'a ⇒ bool" where "A9_f_decomposable _     ≡ (∀x a . atom a ⟶ (∃z . join_irreducible_above_or_bot z a ∧ z ≤ x ∧ (∀w . join_irreducible_above_or_bot w a ∧ w ≤ x ⟶ w ≤ z)))"

lemma atom_join_irreducible:
  assumes "atom a"
    shows "join_irreducible a"
  by (metis assms join_irreducible_def atom_def sup.cobounded1 sup_bot_left)

lemma mono_atomic_with_downclosed:
  assumes "A11_atomic _"
      and "mono_atomic_with x a"
      and "y ≠ bot"
      and "y ≤ x"
    shows "mono_atomic_with y a"
  using assms mono_atomic_with_def[of y a] mono_atomic_with_def[of x a] order_lesseq_imp[of y] by blast

subsection ‹Equivalence›

text ‹
The following result shows that under divisibility axioms A1--A3, A5--A9 and A11, join-irreducible elements coincide with mono-atomic elements.
›

lemma join_irreducible_iff_mono_atomic:
  assumes "A7_pre_f_decomposable _"
      and "A8_fibered _"
      and "A9_f_decomposable _"
      and "A11_atomic _"
    shows "join_irreducible x ⟷ mono_atomic x"
proof (rule iffI)
  assume 1: "join_irreducible x"
  from this obtain a where 2: "atom_below a x"
    using assms(4) join_irreducible_def by blast
  have "∀b . atom_below b x ⟶ b = a"
  proof (rule allI, rule impI)
    fix b
    assume 3: "atom_below b x"
    hence "join_irreducible a ∧ join_irreducible b"
      using 2 atom_join_irreducible by auto
    hence "a ≤ b ∨ b ≤ a"
      using 1 2 3 assms(2) by blast
    thus "b = a"
      using 2 3 atom_def by auto
  qed
  thus "mono_atomic x"
    using 2 mono_atomic_def by auto
next
  assume "mono_atomic x"
  from this obtain a where 4: "mono_atomic_with x a"
    using mono_atomic_above by blast
  hence 5: "x ≠ bot"
    using atom_def le_bot mono_atomic_with_def by blast
  have "∀y z . x = y ⊔ z ⟶ x = y ∨ x = z"
  proof (intro allI, rule impI)
    fix y z
    assume 6: "x = y ⊔ z"
    show "x = y ∨ x = z"
    proof (cases "y = bot ∨ z = bot")
      case True
      thus "x = y ∨ x = z"
        using 6 by auto
    next
      case False
      hence 7: "mono_atomic_with y a ∧ mono_atomic_with z a"
        using 4 6 assms(4) sup.cobounded1 sup.cobounded2 mono_atomic_with_downclosed by blast
      from this obtain u where 8: "join_irreducible_above_or_bot u a ∧ u ≤ y ∧ (∀w . join_irreducible_above_or_bot w a ∧ w ≤ y ⟶ w ≤ u)"
        using assms(3) mono_atomic_with_def by blast
      from 7 obtain v where 9: "join_irreducible_above_or_bot v a ∧ v ≤ z ∧ (∀w . join_irreducible_above_or_bot w a ∧ w ≤ z ⟶ w ≤ v)"
        using assms(3) mono_atomic_with_def by blast
      have "join_irreducible a"
        using 4 atom_join_irreducible mono_atomic_with_def by blast
      hence 10: "u ≤ v ∨ v ≤ u"
        using 8 9 assms(2) join_irreducible_above_or_bot_def by auto
      have 11: "u ≤ v ⟹ y ≤ z"
      proof -
        assume 12: "u ≤ v"
        have "∀w . join_irreducible_below w y ⟶ w ≤ z"
        proof (rule allI, rule impI)
          fix w
          assume 13: "join_irreducible_below w y"
          hence "mono_atomic_with w a"
            using 7 by (metis assms(4) join_irreducible_def mono_atomic_with_downclosed)
          hence "w ≤ u"
            using 8 13 by (simp add: join_irreducible_above_or_bot_def mono_atomic_with_def)
          thus "w ≤ z"
            using 9 12 by force
        qed
        thus "y ≤ z"
          using assms(1) by blast
      qed
      have "v ≤ u ⟹ z ≤ y"
      proof -
        assume 14: "v ≤ u"
        have "∀w . join_irreducible_below w z ⟶ w ≤ y"
        proof (rule allI, rule impI)
          fix w
          assume 15: "join_irreducible_below w z"
          hence "mono_atomic_with w a"
            using 7 by (metis assms(4) join_irreducible_def mono_atomic_with_downclosed)
          hence "w ≤ v"
            using 9 15 by (simp add: join_irreducible_above_or_bot_def mono_atomic_with_def)
          thus "w ≤ y"
            using 8 14 by force
        qed
        thus "z ≤ y"
          using assms(1) by blast
      qed
      thus ?thesis
        using 6 10 11 sup.order_iff sup_monoid.add_commute by force
    qed
  qed
  thus "join_irreducible x"
    using 5 join_irreducible_def by blast
qed

text ‹
The following result shows that under divisibility axioms A1--A3, A5--A6, B7--B9, A11 and B14, join-irreducible elements coincide with mono-atomic elements.
›

lemma mono_atomic_iff_join_irreducible:
  assumes "B7_pre_f_decomposable _"
      and "B8_fibered _"
      and "B9_f_decomposable _"
      and "A11_atomic _"
      and "B14_truncability _"
    shows "mono_atomic x ⟷ join_irreducible x"
proof (rule iffI)
  assume 1: "mono_atomic x"
  from this obtain a where "mono_atomic_below a x"
    by blast
  hence 2: "x ≠ bot"
    using atom_def bot_unique mono_atomic_def by force
  have "∀y z . x = y ⊔ z ⟶ x = y ∨ x = z"
  proof (intro allI, rule impI)
    fix y z
    assume 3: "x = y ⊔ z"
    show "x = y ∨ x = z"
    proof (cases "y = bot ∨ z = bot")
      case True
      thus ?thesis
        using 3 by fastforce
    next
      case False
      hence "mono_atomic y ∧ mono_atomic z"
        using 1 3 by (metis assms(4) mono_atomic_above sup.cobounded1 sup_right_divisibility mono_atomic_with_downclosed)
      hence "y ≤ z ∨ z ≤ y"
        using 1 3 assms(2) by force
      thus ?thesis
        using 3 sup.order_iff sup_monoid.add_commute by force
    qed
  qed
  thus "join_irreducible x"
    using 2 join_irreducible_def by blast
next
  assume "join_irreducible x"
  from this obtain a where 4: "atom a ∧ join_irreducible_above x a"
    using assms(4) join_irreducible_def by blast
  let ?y = "mval a x"
  let ?z = "mtrunc ?y x"
  have 5: "mval a ?z = bot"
    using 4 by (smt (z3) assms(3,5) mono_atomic_above_or_bot_def mtrunc_char mval_char)
  have 6: "mono_atomic_above_or_bot ?y a"
    using 4 assms(3) mval_char by simp
  hence "∀b . atom b ∧ b ≠ a ⟶ ¬ b ≤ ?y"
    using 4 by (metis atom_def bot_unique mono_atomic_above_or_bot_def mono_atomic_def)
  hence 7: "∀b . atom b ∧ b ≠ a ⟶ mval b ?z = mval b x"
    by (simp add: assms(5) mtrunc_char)
  have 8: "?y ≤ x"
    using 4 assms(3) mval_char by blast
  have "∀b . atom b ⟶ mval b ?z ≤ x"
  proof (rule allI, rule impI)
    fix b
    assume 9: "atom b"
    show "mval b ?z ≤ x"
    proof (cases "b = a")
      case True
      thus ?thesis
        using 5 by auto
    next
      case False
      thus ?thesis
        using 7 9 by (simp add:  assms(3) mval_char)
    qed
  qed
  hence 10: "?z ≤ x"
    using 4 assms(1,3) lesseq_iff_mval_below by blast
  have "∀w . ?y ≤ w ∧ ?z ≤ w ⟶ x ≤ w"
  proof (rule allI, rule impI)
    fix w
    assume 11: "?y ≤ w ∧ ?z ≤ w"
    have "∀c . atom c ⟶ mval c x ≤ w"
    proof (rule allI, rule impI)
      fix c
      assume 12: "atom c"
      show "mval c x ≤ w"
      proof (cases "c = a")
        case True
        thus ?thesis
          using 11 by blast
      next
        case False
        thus ?thesis
          using 7 11 12 by (smt (z3) assms(3) dual_order.trans mval_char)
      qed
    qed
    thus "x ≤ w"
      using 4 assms(1,3) lesseq_iff_mval_below by blast
  qed
  hence 13: "x = ?y ⊔ ?z"
    using 8 10 order.ordering_axioms ordering.antisym by force
  have "x ≠ ?z"
  proof (rule notI)
    assume "x = ?z"
    hence "?y = bot"
      using 5 by force
    hence "a = bot"
      using 4 assms(3) atom_below_mval bot_unique by fastforce
    thus False
      using 4 atom_def by blast
  qed
  hence "x = ?y"
    using 4 13 join_irreducible_def by force
  thus "mono_atomic x"
    using 4 6 join_irreducible_def mono_atomic_above_or_bot_def by auto
qed

end

end