Theory Antichain

section‹Antichains›

(*<*)
theory Antichain
  imports
    Auxiliary
begin
(*>*)

definition incomparable where
  "incomparable A = (∀x ∈ A. ∀y ∈ A. x ≠ y ⟶ ¬ x < y ∧ ¬ y < x)"

lemma incomparable_empty[simp, intro]: "incomparable {}"
  unfolding incomparable_def by auto

typedef (overloaded) 'a :: order antichain =
  "{A :: 'a set. finite A ∧ incomparable A}"
  morphisms set_antichain antichain
  by auto

setup_lifting type_definition_antichain

lift_definition member_antichain :: "'a :: order ⇒ 'a antichain ⇒ bool" ("(_/ ∈⇩A _)" [51, 51] 50) is "Set.member" .

abbreviation not_member_antichain :: "'a :: order ⇒ 'a antichain ⇒ bool" ("(_/ ∉⇩A _)" [51, 51] 50) where
  "x ∉⇩A A ≡ ¬ x ∈⇩A A"

lift_definition empty_antichain :: "'a :: order antichain" ("{}⇩A") is "{}" by simp

lemma mem_antichain_nonempty[simp]: "s ∈⇩A A ⟹ A ≠ {}⇩A"
  by transfer auto

definition "minimal_antichain A = {x ∈ A. ¬(∃y ∈ A. y < x)}"

lemma in_minimal_antichain: "x ∈ minimal_antichain A ⟷ x ∈ A ∧ ¬(∃y ∈ A. y < x)"
  unfolding minimal_antichain_def by auto

lemma in_antichain_minimal_antichain[simp]: "finite M ⟹ x ∈⇩A antichain (minimal_antichain M) ⟷ x ∈ minimal_antichain M"
  apply (clarsimp simp: minimal_antichain_def member_antichain.rep_eq)
  apply (intro conjI iffI)
    apply (subst (asm) antichain_inverse)
     apply (simp add: incomparable_def)
    apply simp
   apply (subst (asm) antichain_inverse)
    apply (simp add: incomparable_def)
   apply simp
  apply (subst antichain_inverse)
   apply (simp add: incomparable_def)
  apply simp
  done

lemma incomparable_minimal_antichain[simp]: "incomparable (minimal_antichain A)"
  unfolding incomparable_def minimal_antichain_def
  by auto

lemma finite_minimal_antichain[simp]: "finite A ⟹ finite (minimal_antichain A)"
  unfolding minimal_antichain_def by auto

lemma finite_set_antichain[simp, intro]: "finite (set_antichain A)"
  by transfer auto

lemma minimal_antichain_subset: "minimal_antichain A ⊆ A"
  unfolding minimal_antichain_def by auto

lift_definition frontier :: "'t :: order zmultiset ⇒ 't antichain" is
  "λM. minimal_antichain {t. zcount M t > 0}"
  by (auto simp: finite_subset[OF minimal_antichain_subset finite_zcount_pos])

lemma member_frontier_pos_zmset: "t ∈⇩A frontier M ⟹ 0 < zcount M t"
  by (simp add: frontier_def in_minimal_antichain)

lemma frontier_comparable_False[simp]: "x ∈⇩A frontier M ⟹ y ∈⇩A frontier M ⟹ x < y ⟹ False"
  by transfer (auto simp: minimal_antichain_def)

lemma minimal_antichain_idempotent[simp]: "minimal_antichain (minimal_antichain A) = minimal_antichain A"
  by (auto simp: minimal_antichain_def)

instantiation antichain :: (order) minus begin
lift_definition minus_antichain :: "'a antichain ⇒ 'a antichain ⇒ 'a antichain" is "(-)"
  by (auto simp: incomparable_def)
instance ..
end

instantiation antichain :: (order) plus begin
lift_definition plus_antichain :: "'a antichain ⇒ 'a antichain ⇒ 'a antichain" is "λM N. minimal_antichain (M ∪ N)"
  by (auto simp: incomparable_def minimal_antichain_def)
instance ..
end

lemma antichain_add_commute: "(M :: 'a :: order antichain) + N = N + M"
  by transfer (auto simp: incomparable_def sup_commute)


lift_definition filter_antichain :: "('a :: order ⇒ bool) ⇒ 'a antichain ⇒ 'a antichain" is "Set.filter"
  by (auto simp: incomparable_def)

syntax (ASCII)
  "_ACCollect" :: "pttrn ⇒ 'a :: order antichain ⇒ bool ⇒ 'a antichain" ("(1{_ :⇩A _./ _})")
syntax
  "_ACCollect" :: "pttrn ⇒ 'a :: order antichain ⇒ bool ⇒ 'a antichain" ("(1{_ ∈⇩A _./ _})")
translations
  "{x ∈⇩A M. P}" == "CONST filter_antichain (λx. P) M"


declare empty_antichain.rep_eq[simp]

lemma minimal_antichain_empty[simp]: "minimal_antichain {} = {}"
  by (simp add: minimal_antichain_def)

lemma minimal_antichain_singleton[simp]: "minimal_antichain {x::_ ::order} = {x}"
  by (auto simp: minimal_antichain_def)

lemma minimal_antichain_nonempty:
  "finite A ⟹ (t::_::order) ∈ A ⟹ minimal_antichain A ≠ {}"
  by (auto simp: minimal_antichain_def dest: order_finite_set_exists_foundation[of _ t])

lemma minimal_antichain_member:
  "finite A ⟹ (t::_::order) ∈ A ⟹ ∃t'. t' ∈ minimal_antichain A ∧ t' ≤ t"
  by (auto simp: minimal_antichain_def dest: order_finite_set_exists_foundation[of _ t])

lemma minimal_antichain_union: "minimal_antichain ((A::(_ :: order) set) ∪ B) ⊆ minimal_antichain (minimal_antichain A ∪ minimal_antichain B)"
  by (auto simp: minimal_antichain_def)

lemma ac_Diff_iff: "c ∈⇩A A - B ⟷ c ∈⇩A A ∧ c ∉⇩A B"
  by transfer simp

lemma ac_DiffD2: "c ∈⇩A A - B ⟹ c ∈⇩A B ⟹ P"
  by transfer simp

lemma ac_notin_Diff: "¬ x ∈⇩A A - B ⟹ ¬ x ∈⇩A A ∨ x ∈⇩A B"
  by transfer simp

lemma ac_eq_iff: "A = B ⟷ (∀x. x ∈⇩A A ⟷ x ∈⇩A B)"
  by transfer auto

lemma antichain_obtain_foundation:
  assumes   "t ∈⇩A M"
  obtains s where "s ∈⇩A M ∧ s ≤ t ∧ (∀u. u∈⇩AM ⟶ ¬ u < s)"
  using assms unfolding member_antichain.rep_eq
  by - (rule order_finite_set_obtain_foundation[of "set_antichain M" t]; auto)

lemma set_antichain1[simp]: "x ∈ set_antichain X ⟹ x ∈⇩A X"
  by transfer simp

lemma set_antichain2[simp]: "x ∈⇩A X ⟹ x ∈ set_antichain X"
  by transfer simp

(*<*)
end
(*>*)