# HG changeset patch
# User desharna
# Date 1742821148 -3600
# Node ID 8f3d03433917e9b09752975144fee63ec1b15e7d
# Parent  55e8b2a60dfabd03e2638d96afa04d5f5a518031
strengthened reflp_on_mono and renamed to reflp_on_mono_strong

diff -r 55e8b2a60dfa -r 8f3d03433917 NEWS
--- a/NEWS	Mon Mar 24 09:56:20 2025 +0100
+++ b/NEWS	Mon Mar 24 13:59:08 2025 +0100
@@ -54,6 +54,7 @@
       refl_on_empty[simp]
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
+      reflp_on_mono ~> reflp_on_mono_strong
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
       antisym_on_bot[simp]
diff -r 55e8b2a60dfa -r 8f3d03433917 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 09:56:20 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 13:59:08 2025 +0100
@@ -257,12 +257,12 @@
 lemma reflp_on_equality [simp]: "reflp_on A (=)"
   by (simp add: reflp_on_def)
 
-lemma reflp_on_mono:
-  "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
-  by (auto intro: reflp_onI dest: reflp_onD)
+lemma reflp_on_mono_strong:
+  "reflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
+  by (rule reflp_onI) (auto dest: reflp_onD)
 
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp Q"
-  by (rule reflp_on_mono[of UNIV R Q]) simp_all
+  using reflp_on_mono_strong[OF _ subset_UNIV] .
 
 lemma (in preorder) reflp_on_le[simp]: "reflp_on A (\<le>)"
   by (simp add: reflp_onI)