introduced predicate reflp_on and redefined reflp to be an abbreviation

--- a/NEWS	Tue May 31 20:56:09 2022 +0200
+++ b/NEWS	Sat Jun 04 15:43:34 2022 +0200
@@ -40,8 +40,12 @@
 * Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
 longer. INCOMPATIBILITY.
 
-* Theory "HOL.Relation": Added lemmas asymp_less and asymp_greater to
-  type class preorder.
+* Theory "HOL.Relation":
+  - Added lemmas asymp_less and asymp_greater to type class preorder.
+  - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+    Lemma reflp_def is explicitly provided for backward compatibility
+    but its usage is discouraged. Minor INCOMPATIBILITY.
+  - Added lemmas reflp_onI and reflp_onD.
 
 * Theory "HOL-Library.Multiset":
   - Consolidated operation and fact names.

--- a/src/HOL/Relation.thy	Tue May 31 20:56:09 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 15:43:34 2022 +0200
@@ -155,8 +155,16 @@
 abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
   where "refl \<equiv> refl_on UNIV"
 
-definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "reflp r \<longleftrightarrow> (\<forall>x. r x x)"
+definition reflp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "reflp_on A R \<longleftrightarrow> (\<forall>x\<in>A. R x x)"
+
+abbreviation reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "reflp \<equiv> reflp_on UNIV"
+
+lemma reflp_def[no_atp]: "reflp R \<longleftrightarrow> (\<forall>x. R x x)"
+  by (simp add: reflp_on_def)
+
+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)
@@ -164,6 +172,13 @@
 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 reflp_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> reflp_on A R"
+  by (simp add: reflp_on_def)
+
+lemma reflpI[intro?]: "(\<And>x. R x x) \<Longrightarrow> reflp R"
+  by (rule reflp_onI)
+
 lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
   unfolding refl_on_def by blast
 
@@ -173,19 +188,18 @@
 lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
   unfolding refl_on_def by blast
 
-lemma reflpI [intro?]: "(\<And>x. r x x) \<Longrightarrow> reflp r"
-  by (auto intro: refl_onI simp add: reflp_def)
+lemma reflp_onD:
+  "reflp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> R x x"
+  by (simp add: reflp_on_def)
+
+lemma reflpD[dest?]: "reflp R \<Longrightarrow> R x x"
+  by (simp add: reflp_onD)
 
 lemma reflpE:
   assumes "reflp r"
   obtains "r x x"
   using assms by (auto dest: refl_onD simp add: reflp_def)
 
-lemma reflpD [dest?]:
-  assumes "reflp r"
-  shows "r x x"
-  using assms by (auto elim: reflpE)
-
 lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)"
   unfolding refl_on_def by blast
 

--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue May 31 20:56:09 2022 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Sat Jun 04 15:43:34 2022 +0200
@@ -389,7 +389,7 @@
 
 fun mk_pred name R =
   Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
-val mk_reflp = mk_pred \<^const_name>\<open>reflp\<close>;
+val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
 val mk_symp = mk_pred \<^const_name>\<open>symp\<close>;
 val mk_transp =  mk_pred \<^const_name>\<open>transp\<close>;
 

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue May 31 20:56:09 2022 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Jun 04 15:43:34 2022 +0200
@@ -758,7 +758,7 @@
           handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
       in
         case reflp_tm of
-          Const (\<^const_name>\<open>reflp\<close>, _) $ _ => ()
+          \<^Const_>\<open>reflp_on _ for \<^Const>\<open>top_class.top _\<close> _\<close> => ()
           | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
       end