src/HOL/Library/Preorder.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 31061 1d117af9f9f3 child 58881 b9556a055632 permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Preorders with explicit equivalence relation *}
5 theory Preorder
6 imports Orderings
7 begin
9 class preorder_equiv = preorder
10 begin
12 definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
13   "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
15 notation
16   equiv ("op ~~") and
17   equiv ("(_/ ~~ _)" [51, 51] 50)
19 notation (xsymbols)
20   equiv ("op \<approx>") and
21   equiv ("(_/ \<approx> _)"  [51, 51] 50)
23 notation (HTML output)
24   equiv ("op \<approx>") and
25   equiv ("(_/ \<approx> _)"  [51, 51] 50)
27 lemma refl [iff]:
28   "x \<approx> x"
29   unfolding equiv_def by simp
31 lemma trans:
32   "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
33   unfolding equiv_def by (auto intro: order_trans)
35 lemma antisym:
36   "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
37   unfolding equiv_def ..
39 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
40   by (auto simp add: equiv_def less_le_not_le)
42 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
43   by (auto simp add: equiv_def less_le)
45 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"