--- a/src/HOL/Relation.thy Sun Oct 09 16:24:50 2022 +0200
+++ b/src/HOL/Relation.thy Mon Oct 10 13:42:14 2022 +0200
@@ -274,6 +274,12 @@
lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R"
by (fact irreflI [to_pred])
+lemma irreflD: "irrefl r \<Longrightarrow> (x, x) \<notin> r"
+ unfolding irrefl_def by simp
+
+lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
+ unfolding irreflp_def by simp
+
lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)"
by (auto simp add: irrefl_def)