src/HOL/Library/Preorder.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 31061 1d117af9f9f3 child 58881 b9556a055632 permissions -rw-r--r--
cleaned up some proofs
```     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
```