src/HOL/Library/Preorder.thy
author wenzelm
Tue Jul 12 20:03:18 2016 +0200 (2016-07-12)
changeset 63465 d7610beb98bc
parent 61384 9f5145281888
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
misc tuning and modernization;
     1 (* Author: Florian Haftmann, TU Muenchen *)
     2 
     3 section \<open>Preorders with explicit equivalence relation\<close>
     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"
    13   where "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    14 
    15 notation
    16   equiv ("op \<approx>") and
    17   equiv ("(_/ \<approx> _)"  [51, 51] 50)
    18 
    19 lemma refl [iff]: "x \<approx> x"
    20   by (simp add: equiv_def)
    21 
    22 lemma trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
    23   by (auto simp: equiv_def intro: order_trans)
    24 
    25 lemma antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
    26   by (simp only: equiv_def)
    27 
    28 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
    29   by (auto simp add: equiv_def less_le_not_le)
    30 
    31 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
    32   by (auto simp add: equiv_def less_le)
    33 
    34 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
    35   by (simp add: less_le)
    36 
    37 lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
    38   by (simp add: less_le)
    39 
    40 lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
    41   by (simp add: equiv_def less_le)
    42 
    43 lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    44   by (simp add: less_le)
    45 
    46 lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
    47   by (simp add: less_le)
    48 
    49 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
    50   by (simp add: equiv_def)
    51 
    52 end
    53 
    54 end