# HG changeset patch
# User desharna
# Date 1671447615 -3600
# Node ID e19a3dbbf5de67f8b2923053bd5b36edcb8e5ca4
# Parent  b6b7f3caa74af8d98c7cd238d600d5a4ac780b5c
added lemmas reflI and reflD

diff -r b6b7f3caa74a -r e19a3dbbf5de NEWS
--- a/NEWS	Mon Dec 19 11:26:56 2022 +0100
+++ b/NEWS	Mon Dec 19 12:00:15 2022 +0100
@@ -92,6 +92,8 @@
       preorder.antisymp_on_less[simp]
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
+      reflD
+      reflI
       reflp_on_conversp[simp]
       sym_onD
       sym_onI
diff -r b6b7f3caa74a -r e19a3dbbf5de src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 11:26:56 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 12:00:15 2022 +0100
@@ -173,6 +173,9 @@
 lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
   unfolding refl_on_def by (iprover intro!: ballI)
 
+lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
+  by (auto intro: refl_onI)
+
 lemma reflp_onI:
   "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
   by (simp add: reflp_on_def)
@@ -189,6 +192,9 @@
 lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
   unfolding refl_on_def by blast
 
+lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
+  unfolding refl_on_def by blast
+
 lemma reflp_onD:
   "reflp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> R x x"
   by (simp add: reflp_on_def)