src/HOL/Library/Preorder.thy
changeset 31060 75d7c7cc8bdb
child 31061 1d117af9f9f3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Preorder.thy	Thu May 07 12:17:17 2009 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* Preorders with explicit equivalence relation *}
     1.7 +
     1.8 +theory Preorder
     1.9 +imports Orderings
    1.10 +begin
    1.11 +
    1.12 +context preorder
    1.13 +begin
    1.14 +
    1.15 +definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.16 +  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    1.17 +
    1.18 +notation
    1.19 +  equiv ("op ~~") and
    1.20 +  equiv ("(_/ ~~ _)" [51, 51] 50)
    1.21 +  
    1.22 +notation (xsymbols)
    1.23 +  equiv ("op \<approx>") and
    1.24 +  equiv ("(_/ \<approx> _)"  [51, 51] 50)
    1.25 +
    1.26 +notation (HTML output)
    1.27 +  equiv ("op \<approx>") and
    1.28 +  equiv ("(_/ \<approx> _)"  [51, 51] 50)
    1.29 +
    1.30 +lemma refl [iff]:
    1.31 +  "x \<approx> x"
    1.32 +  unfolding equiv_def by simp
    1.33 +
    1.34 +lemma trans:
    1.35 +  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
    1.36 +  unfolding equiv_def by (auto intro: order_trans)
    1.37 +
    1.38 +lemma antisym:
    1.39 +  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
    1.40 +  unfolding equiv_def ..
    1.41 +
    1.42 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
    1.43 +  by (auto simp add: equiv_def less_le_not_le)
    1.44 +
    1.45 +lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
    1.46 +  by (auto simp add: equiv_def less_le)
    1.47 +
    1.48 +lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
    1.49 +  by (simp add: less_le)
    1.50 +
    1.51 +lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
    1.52 +  by (simp add: less_le)
    1.53 +
    1.54 +lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
    1.55 +  by (simp add: equiv_def less_le)
    1.56 +
    1.57 +lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    1.58 +  by (simp add: less_le)
    1.59 +
    1.60 +lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
    1.61 +  by (simp add: less_le)
    1.62 +
    1.63 +lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
    1.64 +  by (simp add: equiv_def)
    1.65 +
    1.66 +end
    1.67 +
    1.68 +end