src/HOL/Relation.thy
changeset 76255 b3ff4f171eda
parent 76254 7ae89ee919a7
child 76256 207b6fcfc47d
--- 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)