(* 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 (
‹(
‹notation=
‹infix ≈››_/
≈ _)
› [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
