# HG changeset patch
# User desharna
# Date 1665481684 -7200
# Node ID 2f10e7a2ff01e9ba4037168be8f6e0608c08a7fb
# Parent  61a5b5ad3a6e3ef33dbe9c04aa416431b765afe9
added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]

diff -r 61a5b5ad3a6e -r 2f10e7a2ff01 NEWS
--- a/NEWS	Tue Oct 11 11:07:07 2022 +0200
+++ b/NEWS	Tue Oct 11 11:48:04 2022 +0200
@@ -13,7 +13,11 @@
   - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
   - Added lemmas.
       antisym_if_asymp
+      antisymp_ge[simp]
+      antisymp_greater[simp]
       antisymp_if_asymp
+      antisymp_le[simp]
+      antisymp_less[simp]
       irreflD
       irreflpD
       reflp_ge[simp]
diff -r 61a5b5ad3a6e -r 2f10e7a2ff01 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Oct 11 11:07:07 2022 +0200
+++ b/src/HOL/Relation.thy	Tue Oct 11 11:48:04 2022 +0200
@@ -441,6 +441,18 @@
 lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
   by (rule antisym_if_asym[to_pred])
 
+lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
+  by (rule antisymp_if_asymp[OF asymp_less])
+
+lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
+  by (rule antisymp_if_asymp[OF asymp_greater])
+
+lemma (in order) antisymp_le[simp]: "antisymp (\<le>)"
+  by (simp add: antisympI)
+
+lemma (in order) antisymp_ge[simp]: "antisymp (\<ge>)"
+  by (simp add: antisympI)
+
 
 subsubsection \<open>Transitivity\<close>