# HG changeset patch
# User haftmann
# Date 1241691437 -7200
# Node ID 75d7c7cc8bdb2092d61b42472195bcde3db7f8f7
# Parent  45c085c7efc643a30d08e8286b70d681208492bf
added theory for explicit equivalence relation in preorders

diff -r 45c085c7efc6 -r 75d7c7cc8bdb src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 07 12:02:16 2009 +0200
+++ b/src/HOL/IsaMakefile	Thu May 07 12:17:17 2009 +0200
@@ -342,6 +342,7 @@
   Library/Random.thy Library/Quickcheck.thy	\
   Library/Poly_Deriv.thy \
   Library/Polynomial.thy \
+  Library/Preorder.thy \
   Library/Product_plus.thy \
   Library/Product_Vector.thy \
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
diff -r 45c085c7efc6 -r 75d7c7cc8bdb src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu May 07 12:02:16 2009 +0200
+++ b/src/HOL/Library/Library.thy	Thu May 07 12:17:17 2009 +0200
@@ -42,6 +42,7 @@
   Pocklington
   Poly_Deriv
   Polynomial
+  Preorder
   Primes
   Product_Vector
   Quickcheck
diff -r 45c085c7efc6 -r 75d7c7cc8bdb src/HOL/Library/Preorder.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Preorder.thy	Thu May 07 12:17:17 2009 +0200
@@ -0,0 +1,65 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Preorders with explicit equivalence relation *}
+
+theory Preorder
+imports Orderings
+begin
+
+context preorder
+begin
+
+definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
+
+notation
+  equiv ("op ~~") and
+  equiv ("(_/ ~~ _)" [51, 51] 50)
+  
+notation (xsymbols)
+  equiv ("op \<approx>") and
+  equiv ("(_/ \<approx> _)"  [51, 51] 50)
+
+notation (HTML output)
+  equiv ("op \<approx>") and
+  equiv ("(_/ \<approx> _)"  [51, 51] 50)
+
+lemma refl [iff]:
+  "x \<approx> x"
+  unfolding equiv_def by simp
+
+lemma trans:
+  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+  unfolding equiv_def by (auto intro: order_trans)
+
+lemma antisym:
+  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+  unfolding equiv_def ..
+
+lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
+  by (auto simp add: equiv_def less_le_not_le)
+
+lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
+  by (auto simp add: equiv_def less_le)
+
+lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
+  by (simp add: less_le)
+
+lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
+  by (simp add: less_le)
+
+lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
+  by (simp add: equiv_def less_le)
+
+lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
+  by (simp add: less_le)
+
+lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
+  by (simp add: less_le)
+
+lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
+  by (simp add: equiv_def)
+
+end
+
+end