Theory Preorder

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

header {* 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)

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

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

lemma refl [iff]:
"x ≈ x"
unfolding equiv_def by simp

lemma trans:
"x ≈ y ==> y ≈ z ==> x ≈ z"
unfolding equiv_def by (auto intro: order_trans)

lemma antisym:
"x ≤ y ==> y ≤ x ==> x ≈ y"
unfolding 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