src/HOL/Relation.thy

--- 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