# HG changeset patch
# User desharna
# Date 1665402134 -7200
# Node ID b3ff4f171edaa847525ac40e864e9169fbe4bf9a
# Parent  7ae89ee919a7ca33287c8f97986c2863eb5e6a89
added lemmas irreflD and irreflpD

diff -r 7ae89ee919a7 -r b3ff4f171eda NEWS
--- 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]
 
 
diff -r 7ae89ee919a7 -r b3ff4f171eda src/HOL/Relation.thy
--- 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)