# 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 \ '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