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