src/HOL/Library/Preorder.thy
author wenzelm
Sun, 02 Nov 2014 17:20:45 +0100
changeset 58881 b9556a055632
parent 31061 1d117af9f9f3
child 60500 903bb1495239
permissions -rw-r--r--
modernized header;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     1
(* Author: Florian Haftmann, TU Muenchen *)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     2
58881
b9556a055632 modernized header;
wenzelm
parents: 31061
diff changeset
     3
section {* Preorders with explicit equivalence relation *}
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     4
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     5
theory Preorder
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     6
imports Orderings
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     7
begin
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
     8
31061
1d117af9f9f3 better to have distinguished class for preorders
haftmann
parents: 31060
diff changeset
     9
class preorder_equiv = preorder
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    10
begin
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    11
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    12
definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    13
  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    14
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    15
notation
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    16
  equiv ("op ~~") and
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    17
  equiv ("(_/ ~~ _)" [51, 51] 50)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    18
  
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    19
notation (xsymbols)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    20
  equiv ("op \<approx>") and
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    21
  equiv ("(_/ \<approx> _)"  [51, 51] 50)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    22
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    23
notation (HTML output)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    24
  equiv ("op \<approx>") and
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    25
  equiv ("(_/ \<approx> _)"  [51, 51] 50)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    26
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    27
lemma refl [iff]:
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    28
  "x \<approx> x"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    29
  unfolding equiv_def by simp
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    30
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    31
lemma trans:
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    32
  "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    33
  unfolding equiv_def by (auto intro: order_trans)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    34
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    35
lemma antisym:
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    36
  "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    37
  unfolding equiv_def ..
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    38
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    39
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    40
  by (auto simp add: equiv_def less_le_not_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    41
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    42
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    43
  by (auto simp add: equiv_def less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    44
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    45
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    46
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    47
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    48
lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    49
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    50
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    51
lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    52
  by (simp add: equiv_def less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    53
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    54
lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    55
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    56
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    57
lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    58
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    59
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    60
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    61
  by (simp add: equiv_def)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    62
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    63
end
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    64
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    65
end