haftmann@31060: (* Author: Florian Haftmann, TU Muenchen *)
haftmann@31060: 
haftmann@31060: header {* Preorders with explicit equivalence relation *}
haftmann@31060: 
haftmann@31060: theory Preorder
haftmann@31060: imports Orderings
haftmann@31060: begin
haftmann@31060: 
haftmann@31061: class preorder_equiv = preorder
haftmann@31060: begin
haftmann@31060: 
haftmann@31060: definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
haftmann@31060:   "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
haftmann@31060: 
haftmann@31060: notation
haftmann@31060:   equiv ("op ~~") and
haftmann@31060:   equiv ("(_/ ~~ _)" [51, 51] 50)
haftmann@31060:   
haftmann@31060: notation (xsymbols)
haftmann@31060:   equiv ("op \<approx>") and
haftmann@31060:   equiv ("(_/ \<approx> _)"  [51, 51] 50)
haftmann@31060: 
haftmann@31060: notation (HTML output)
haftmann@31060:   equiv ("op \<approx>") and
haftmann@31060:   equiv ("(_/ \<approx> _)"  [51, 51] 50)
haftmann@31060: 
haftmann@31060: lemma refl [iff]:
haftmann@31060:   "x \<approx> x"
haftmann@31060:   unfolding equiv_def by simp
haftmann@31060: 
haftmann@31060: lemma trans:
haftmann@31060:   "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
haftmann@31060:   unfolding equiv_def by (auto intro: order_trans)
haftmann@31060: 
haftmann@31060: lemma antisym:
haftmann@31060:   "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
haftmann@31060:   unfolding equiv_def ..
haftmann@31060: 
haftmann@31060: lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
haftmann@31060:   by (auto simp add: equiv_def less_le_not_le)
haftmann@31060: 
haftmann@31060: lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
haftmann@31060:   by (auto simp add: equiv_def less_le)
haftmann@31060: 
haftmann@31060: lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
haftmann@31060:   by (simp add: less_le)
haftmann@31060: 
haftmann@31060: lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
haftmann@31060:   by (simp add: less_le)
haftmann@31060: 
haftmann@31060: lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
haftmann@31060:   by (simp add: equiv_def less_le)
haftmann@31060: 
haftmann@31060: lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
haftmann@31060:   by (simp add: less_le)
haftmann@31060: 
haftmann@31060: lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
haftmann@31060:   by (simp add: less_le)
haftmann@31060: 
haftmann@31060: lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
haftmann@31060:   by (simp add: equiv_def)
haftmann@31060: 
haftmann@31060: end
haftmann@31060: 
haftmann@31060: end