src/HOL/Library/Preorder.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 67398 5eb932e604a2
child 69815 56d5bb8c102e
permissions -rw-r--r--
tuned equation
haftmann@31060
     1
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@31060
     2
wenzelm@60500
     3
section \<open>Preorders with explicit equivalence relation\<close>
haftmann@31060
     4
haftmann@31060
     5
theory Preorder
wenzelm@67006
     6
imports Main
haftmann@31060
     7
begin
haftmann@31060
     8
haftmann@31061
     9
class preorder_equiv = preorder
haftmann@31060
    10
begin
haftmann@31060
    11
wenzelm@63465
    12
definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@63465
    13
  where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
haftmann@31060
    14
haftmann@31060
    15
notation
nipkow@67398
    16
  equiv ("'(\<approx>')") and
haftmann@31060
    17
  equiv ("(_/ \<approx> _)"  [51, 51] 50)
haftmann@31060
    18
wenzelm@63465
    19
lemma refl [iff]: "x \<approx> x"
wenzelm@63465
    20
  by (simp add: equiv_def)
haftmann@31060
    21
wenzelm@63465
    22
lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
wenzelm@63465
    23
  by (auto simp: equiv_def intro: order_trans)
haftmann@31060
    24
wenzelm@63465
    25
lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
wenzelm@63465
    26
  by (simp only: equiv_def)
haftmann@31060
    27
haftmann@31060
    28
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
haftmann@31060
    29
  by (auto simp add: equiv_def less_le_not_le)
haftmann@31060
    30
haftmann@31060
    31
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
haftmann@31060
    32
  by (auto simp add: equiv_def less_le)
haftmann@31060
    33
haftmann@31060
    34
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
haftmann@31060
    35
  by (simp add: less_le)
haftmann@31060
    36
haftmann@31060
    37
lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
haftmann@31060
    38
  by (simp add: less_le)
haftmann@31060
    39
haftmann@31060
    40
lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
haftmann@31060
    41
  by (simp add: equiv_def less_le)
haftmann@31060
    42
haftmann@31060
    43
lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
haftmann@31060
    44
  by (simp add: less_le)
haftmann@31060
    45
haftmann@31060
    46
lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
haftmann@31060
    47
  by (simp add: less_le)
haftmann@31060
    48
haftmann@31060
    49
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
haftmann@31060
    50
  by (simp add: equiv_def)
haftmann@31060
    51
haftmann@31060
    52
end
haftmann@31060
    53
haftmann@31060
    54
end