--- a/NEWS Sun Oct 09 16:24:50 2022 +0200
+++ b/NEWS Mon Oct 10 13:42:14 2022 +0200
@@ -10,10 +10,12 @@
*** HOL ***
* Theory "HOL.Relation":
- - Strengthened total_on_singleton. Minor INCOMPATIBILITY.
+ - Strengthened lemma total_on_singleton. Minor INCOMPATIBILITY.
- Added lemmas.
antisym_if_asymp
antisymp_if_asymp
+ irreflD
+ irreflpD
totalp_on_singleton[simp]
--- 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)