Theory HOL-Library.Preorder

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Preorders with explicit equivalence relation›

theory Preorder
imports Main
begin

class preorder_equiv = preorder
begin

definition equiv :: "'a  'a  bool"
  where "equiv x y  x  y  y  x"

notation
  equiv ("'(≈')") and
  equiv ("(_/  _)"  [51, 51] 50)

lemma equivD1: "x  y" if "x  y"
  using that by (simp add: equiv_def)

lemma equivD2: "y  x" if "x  y"
  using that by (simp add: equiv_def)

lemma equiv_refl [iff]: "x  x"
  by (simp add: equiv_def)

lemma equiv_sym: "x  y  y  x"
  by (auto simp add: equiv_def)

lemma equiv_trans: "x  y  y  z  x  z"
  by (auto simp: equiv_def intro: order_trans)

lemma equiv_antisym: "x  y  y  x  x  y"
  by (simp only: equiv_def)

lemma less_le: "x < y  x  y  ¬ x  y"
  by (auto simp add: equiv_def less_le_not_le)

lemma le_less: "x  y  x < y  x  y"
  by (auto simp add: equiv_def less_le)

lemma le_imp_less_or_equiv: "x  y  x < y  x  y"
  by (simp add: less_le)

lemma less_imp_not_equiv: "x < y  ¬ x  y"
  by (simp add: less_le)

lemma not_equiv_le_trans: "¬ a  b  a  b  a < b"
  by (simp add: less_le)

lemma le_not_equiv_trans: "a  b  ¬ a  b  a < b"
  by (rule not_equiv_le_trans)

lemma antisym_conv: "y  x  x  y  x  y"
  by (simp add: equiv_def)

end

ML_file ‹~~/src/Provers/preorder.ML›

ML structure Quasi = Quasi_Tac(
struct

val le_trans = @{thm order_trans};
val le_refl = @{thm order_refl};
val eqD1 = @{thm equivD1};
val eqD2 = @{thm equivD2};
val less_reflE = @{thm less_irrefl};
val less_imp_le = @{thm less_imp_le};
val le_neq_trans = @{thm le_not_equiv_trans};
val neq_le_trans = @{thm not_equiv_le_trans};
val less_imp_neq = @{thm less_imp_not_equiv};

fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2)
  | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2)
  | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2)
  | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2)
  | decomp_quasi thy _ = NONE;

fun decomp_trans thy t = case decomp_quasi thy t of
    x as SOME (t1, "<=", t2) => x
  | _ => NONE;

end
);

end