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