# HG changeset patch
# User desharna
# Date 1741971736 -3600
# Node ID 4355a2afa7a3132d18b3d6057b95c87b0f488ec9
# Parent  72e641e3b7cd19acbd6eaebf315f2acea09cfcc5
added lemma reflp_on_refl_on_eq [pred_set_conv]

diff -r 72e641e3b7cd -r 4355a2afa7a3 NEWS
--- a/NEWS	Thu Mar 13 16:00:48 2025 +0100
+++ b/NEWS	Fri Mar 14 18:02:16 2025 +0100
@@ -20,6 +20,8 @@
   - Changed definition of predicate refl_on to not constrain the domain
     and range of the relation. To get the old semantics, explicitely use
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
+  - Added lemmas.
+      reflp_on_refl_on_eq[pred_set_conv]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
diff -r 72e641e3b7cd -r 4355a2afa7a3 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Mar 13 16:00:48 2025 +0100
+++ b/src/HOL/Relation.thy	Fri Mar 14 18:02:16 2025 +0100
@@ -167,8 +167,10 @@
 
 text \<open>@{thm [source] reflp_def} is for backward compatibility.\<close>
 
-lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
-  by (simp add: refl_on_def reflp_def)
+lemma reflp_on_refl_on_eq[pred_set_conv]: "reflp_on A (\<lambda>a b. (a, b) \<in> r) \<longleftrightarrow> refl_on A r"
+  by (simp add: refl_on_def reflp_on_def)
+
+lemmas reflp_refl_eq = reflp_on_refl_on_eq[of UNIV]
 
 lemma refl_onI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
   unfolding refl_on_def by (iprover intro!: ballI)