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