Theory Preorder

theory Preorder
imports Orderings
(* Author: Florian Haftmann, TU Muenchen *)

section ‹Preorders with explicit equivalence relation›

theory Preorder
imports Orderings
begin

class preorder_equiv = preorder
begin

definition equiv :: "'a ⇒ 'a ⇒ bool"
  where "equiv x y ⟷ x ≤ y ∧ y ≤ x"

notation
  equiv ("op ≈") and
  equiv ("(_/ ≈ _)"  [51, 51] 50)

lemma refl [iff]: "x ≈ x"
  by (simp add: equiv_def)

lemma trans: "x ≈ y ⟹ y ≈ z ⟹ x ≈ z"
  by (auto simp: equiv_def intro: order_trans)

lemma antisym: "x ≤ y ⟹ y ≤ x ⟹ x ≈ y"
  by (simp only: equiv_def)

lemma less_le: "x < y ⟷ x ≤ y ∧ ¬ x ≈ y"
  by (auto simp add: equiv_def less_le_not_le)

lemma le_less: "x ≤ y ⟷ x < y ∨ x ≈ y"
  by (auto simp add: equiv_def less_le)

lemma le_imp_less_or_eq: "x ≤ y ⟹ x < y ∨ x ≈ y"
  by (simp add: less_le)

lemma less_imp_not_eq: "x < y ⟹ x ≈ y ⟷ False"
  by (simp add: less_le)

lemma less_imp_not_eq2: "x < y ⟹ y ≈ x ⟷ False"
  by (simp add: equiv_def less_le)

lemma neq_le_trans: "¬ a ≈ b ⟹ a ≤ b ⟹ a < b"
  by (simp add: less_le)

lemma le_neq_trans: "a ≤ b ⟹ ¬ a ≈ b ⟹ a < b"
  by (simp add: less_le)

lemma antisym_conv: "y ≤ x ⟹ x ≤ y ⟷ x ≈ y"
  by (simp add: equiv_def)

end

end