--- a/NEWS Tue Oct 11 18:30:09 2022 +0200
+++ b/NEWS Tue Oct 11 18:52:01 2022 +0200
@@ -13,9 +13,15 @@
- 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]
+ reflp_le[simp]
totalp_on_singleton[simp]
--- a/src/HOL/Relation.thy Tue Oct 11 18:30:09 2022 +0200
+++ b/src/HOL/Relation.thy Tue Oct 11 18:52:01 2022 +0200
@@ -256,6 +256,12 @@
lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
by (rule reflp_on_mono[of UNIV R Q]) simp_all
+lemma (in preorder) reflp_le[simp]: "reflp (\<le>)"
+ by (simp add: reflpI)
+
+lemma (in preorder) reflp_ge[simp]: "reflp (\<ge>)"
+ by (simp add: reflpI)
+
subsubsection \<open>Irreflexivity\<close>
@@ -435,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>