Theory Posets

section‹Some order tools: posets with explicit universe›

theory Posets
imports Main "HOL-Library.LaTeXsugar"

begin

locale poset_on =
  fixes P :: "'b set"
  fixes P_lesseq :: "'b ⇒ 'b ⇒ bool" (infix ‹≤⇧^P› 60) 
  fixes P_less :: "'b ⇒ 'b ⇒ bool" (infix ‹<⇧^P› 60)
  assumes not_empty [simp]: "P ≠ ∅"
  and reflex: "reflp_on P (≤⇧^P)"
  and antisymm: "antisymp_on P (≤⇧^P)"
  and trans: "transp_on P (≤⇧^P)"
  and strict_iff_order: "x ∈ P ⟹ y ∈ P ⟹ x <⇧^P y = (x ≤⇧^P y ∧ x ≠ y)"
begin

lemma strict_trans:
  assumes "a ∈ P" "b ∈ P" "c ∈ P" "a <⇧^P b" "b <⇧^P c"
  shows "a <⇧^P c"
  using antisymm antisymp_onD assms trans strict_iff_order transp_onD
  by (smt (verit, ccfv_SIG))

end

locale bot_poset_on = poset_on +
  fixes bot :: "'b" (‹0⇧^P›)
  assumes bot_closed: "0⇧^P ∈ P"
  and bot_first: "x ∈ P ⟹ 0⇧^P ≤⇧^P x"

locale top_poset_on = poset_on +
  fixes top :: "'b" (‹1⇧^P›)
  assumes top_closed: "1⇧^P ∈ P"
  and top_last: "x ∈ P ⟹ x ≤⇧^P 1⇧^P"

locale bounded_poset_on  = bot_poset_on + top_poset_on

locale total_poset_on = poset_on +
  assumes total: "totalp_on P (≤⇧^P)"
begin

lemma trichotomy:
  assumes "a ∈ P" "b ∈ P"
  shows "(a <⇧^P b ∧ ¬(a = b ∨ b <⇧^P a)) ∨
         (a = b ∧ ¬(a <⇧^P b ∨ b <⇧^P a)) ∨
         (b <⇧^P a ∧ ¬(a = b ∨ a <⇧^P b))"
  using  antisymm antisymp_onD assms strict_iff_order total totalp_onD by metis

lemma strict_order_equiv_not_converse: 
  assumes "a ∈ P" "b ∈ P"
  shows "a <⇧^P b ⟷ ¬(b ≤⇧^P a)"
  using assms strict_iff_order reflex reflp_onD strict_trans trichotomy by metis

end
     
end