src/HOL/Library/Preorder.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63465 d7610beb98bc
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
tuned proofs;
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     3
section \<open>Preorders with explicit equivalence relation\<close>
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
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    12
definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    13
  where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
31060
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 \<approx>") and
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    17
  equiv ("(_/ \<approx> _)"  [51, 51] 50)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    18
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    19
lemma refl [iff]: "x \<approx> x"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    20
  by (simp add: equiv_def)
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    21
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    22
lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    23
  by (auto simp: equiv_def intro: order_trans)
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    24
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    25
lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 61384
diff changeset
    26
  by (simp only: equiv_def)
31060
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    27
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    28
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
    29
  by (auto simp add: equiv_def less_le_not_le)
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 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
    32
  by (auto simp add: equiv_def less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    33
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    34
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
    35
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    36
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    37
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
    38
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    39
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    40
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
    41
  by (simp add: equiv_def less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    42
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    43
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
    44
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    45
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    46
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
    47
  by (simp add: less_le)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    48
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    49
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
    50
  by (simp add: equiv_def)
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    51
75d7c7cc8bdb added theory for explicit equivalence relation in preorders
haftmann
parents:
diff changeset
    52
end
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
end