src/HOL/Library/Preorder.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 31061 1d117af9f9f3
child 58881 b9556a055632
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Preorders with explicit equivalence relation *}
     4 
     5 theory Preorder
     6 imports Orderings
     7 begin
     8 
     9 class preorder_equiv = preorder
    10 begin
    11 
    12 definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    13   "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    14 
    15 notation
    16   equiv ("op ~~") and
    17   equiv ("(_/ ~~ _)" [51, 51] 50)
    18   
    19 notation (xsymbols)
    20   equiv ("op \<approx>") and
    21   equiv ("(_/ \<approx> _)"  [51, 51] 50)
    22 
    23 notation (HTML output)
    24   equiv ("op \<approx>") and
    25   equiv ("(_/ \<approx> _)"  [51, 51] 50)
    26 
    27 lemma refl [iff]:
    28   "x \<approx> x"
    29   unfolding equiv_def by simp
    30 
    31 lemma trans:
    32   "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
    33   unfolding equiv_def by (auto intro: order_trans)
    34 
    35 lemma antisym:
    36   "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
    37   unfolding equiv_def ..
    38 
    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)
    41 
    42 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
    43   by (auto simp add: equiv_def less_le)
    44 
    45 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
    46   by (simp add: less_le)
    47 
    48 lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
    49   by (simp add: less_le)
    50 
    51 lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
    52   by (simp add: equiv_def less_le)
    53 
    54 lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    55   by (simp add: less_le)
    56 
    57 lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
    58   by (simp add: less_le)
    59 
    60 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
    61   by (simp add: equiv_def)
    62 
    63 end
    64 
    65 end