Quelle  Posets.thy

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 ‹<\<^sup>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