src/HOL/Library/Preorder.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69821 8432b771f12e
permissions -rw-r--r--
improved code equations taken over from AFP
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
haftmann@69815
    19
lemma equivD1: "x \<le> y" if "x \<approx> y"
haftmann@69815
    20
  using that by (simp add: equiv_def)
haftmann@69815
    21
haftmann@69815
    22
lemma equivD2: "y \<le> x" if "x \<approx> y"
haftmann@69815
    23
  using that by (simp add: equiv_def)
haftmann@69815
    24
haftmann@69815
    25
lemma equiv_refl [iff]: "x \<approx> x"
wenzelm@63465
    26
  by (simp add: equiv_def)
haftmann@31060
    27
haftmann@69815
    28
lemma equiv_sym: "x \<approx> y \<longleftrightarrow> y \<approx> x"
haftmann@69815
    29
  by (auto simp add: equiv_def)
haftmann@69815
    30
haftmann@69815
    31
lemma equiv_trans: "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
wenzelm@63465
    32
  by (auto simp: equiv_def intro: order_trans)
haftmann@31060
    33
haftmann@69815
    34
lemma equiv_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
wenzelm@63465
    35
  by (simp only: equiv_def)
haftmann@31060
    36
haftmann@31060
    37
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
haftmann@31060
    38
  by (auto simp add: equiv_def less_le_not_le)
haftmann@31060
    39
haftmann@31060
    40
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
haftmann@31060
    41
  by (auto simp add: equiv_def less_le)
haftmann@31060
    42
haftmann@69815
    43
lemma le_imp_less_or_equiv: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
haftmann@31060
    44
  by (simp add: less_le)
haftmann@31060
    45
haftmann@69815
    46
lemma less_imp_not_equiv: "x < y \<Longrightarrow> \<not> x \<approx> y"
haftmann@31060
    47
  by (simp add: less_le)
haftmann@31060
    48
haftmann@69815
    49
lemma not_equiv_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
haftmann@31060
    50
  by (simp add: less_le)
haftmann@31060
    51
haftmann@69815
    52
lemma le_not_equiv_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
haftmann@69815
    53
  by (rule not_equiv_le_trans)
haftmann@31060
    54
haftmann@31060
    55
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
haftmann@31060
    56
  by (simp add: equiv_def)
haftmann@31060
    57
haftmann@31060
    58
end
haftmann@31060
    59
haftmann@69815
    60
ML_file \<open>~~/src/Provers/preorder.ML\<close>
haftmann@69815
    61
haftmann@69815
    62
ML \<open>
haftmann@69815
    63
structure Quasi = Quasi_Tac(
haftmann@69815
    64
struct
haftmann@69815
    65
haftmann@69815
    66
val le_trans = @{thm order_trans};
haftmann@69815
    67
val le_refl = @{thm order_refl};
haftmann@69815
    68
val eqD1 = @{thm equivD1};
haftmann@69815
    69
val eqD2 = @{thm equivD2};
haftmann@69815
    70
val less_reflE = @{thm less_irrefl};
haftmann@69815
    71
val less_imp_le = @{thm less_imp_le};
haftmann@69815
    72
val le_neq_trans = @{thm le_not_equiv_trans};
haftmann@69815
    73
val neq_le_trans = @{thm not_equiv_le_trans};
haftmann@69815
    74
val less_imp_neq = @{thm less_imp_not_equiv};
haftmann@69815
    75
haftmann@69815
    76
fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2)
haftmann@69815
    77
  | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2)
haftmann@69815
    78
  | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2)
haftmann@69815
    79
  | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2)
haftmann@69815
    80
  | decomp_quasi thy _ = NONE;
haftmann@69815
    81
haftmann@69815
    82
fun decomp_trans thy t = case decomp_quasi thy t of
haftmann@69815
    83
    x as SOME (t1, "<=", t2) => x
haftmann@69815
    84
  | _ => NONE;
haftmann@69815
    85
haftmann@31060
    86
end
haftmann@69815
    87
);
haftmann@69815
    88
\<close>
haftmann@69815
    89
haftmann@69815
    90
end