added theory for explicit equivalence relation in preorders
authorhaftmann
Thu May 07 12:17:17 2009 +0200 (2009-05-07)
changeset 3106075d7c7cc8bdb
parent 31059 45c085c7efc6
child 31061 1d117af9f9f3
added theory for explicit equivalence relation in preorders
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Preorder.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu May 07 12:02:16 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 07 12:17:17 2009 +0200
     1.3 @@ -342,6 +342,7 @@
     1.4    Library/Random.thy Library/Quickcheck.thy	\
     1.5    Library/Poly_Deriv.thy \
     1.6    Library/Polynomial.thy \
     1.7 +  Library/Preorder.thy \
     1.8    Library/Product_plus.thy \
     1.9    Library/Product_Vector.thy \
    1.10    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
     2.1 --- a/src/HOL/Library/Library.thy	Thu May 07 12:02:16 2009 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Thu May 07 12:17:17 2009 +0200
     2.3 @@ -42,6 +42,7 @@
     2.4    Pocklington
     2.5    Poly_Deriv
     2.6    Polynomial
     2.7 +  Preorder
     2.8    Primes
     2.9    Product_Vector
    2.10    Quickcheck
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Preorder.thy	Thu May 07 12:17:17 2009 +0200
     3.3 @@ -0,0 +1,65 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Preorders with explicit equivalence relation *}
     3.7 +
     3.8 +theory Preorder
     3.9 +imports Orderings
    3.10 +begin
    3.11 +
    3.12 +context preorder
    3.13 +begin
    3.14 +
    3.15 +definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    3.16 +  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    3.17 +
    3.18 +notation
    3.19 +  equiv ("op ~~") and
    3.20 +  equiv ("(_/ ~~ _)" [51, 51] 50)
    3.21 +  
    3.22 +notation (xsymbols)
    3.23 +  equiv ("op \<approx>") and
    3.24 +  equiv ("(_/ \<approx> _)"  [51, 51] 50)
    3.25 +
    3.26 +notation (HTML output)
    3.27 +  equiv ("op \<approx>") and
    3.28 +  equiv ("(_/ \<approx> _)"  [51, 51] 50)
    3.29 +
    3.30 +lemma refl [iff]:
    3.31 +  "x \<approx> x"
    3.32 +  unfolding equiv_def by simp
    3.33 +
    3.34 +lemma trans:
    3.35 +  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
    3.36 +  unfolding equiv_def by (auto intro: order_trans)
    3.37 +
    3.38 +lemma antisym:
    3.39 +  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
    3.40 +  unfolding equiv_def ..
    3.41 +
    3.42 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
    3.43 +  by (auto simp add: equiv_def less_le_not_le)
    3.44 +
    3.45 +lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
    3.46 +  by (auto simp add: equiv_def less_le)
    3.47 +
    3.48 +lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
    3.49 +  by (simp add: less_le)
    3.50 +
    3.51 +lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
    3.52 +  by (simp add: less_le)
    3.53 +
    3.54 +lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
    3.55 +  by (simp add: equiv_def less_le)
    3.56 +
    3.57 +lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    3.58 +  by (simp add: less_le)
    3.59 +
    3.60 +lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
    3.61 +  by (simp add: less_le)
    3.62 +
    3.63 +lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
    3.64 +  by (simp add: equiv_def)
    3.65 +
    3.66 +end
    3.67 +
    3.68 +end