--- a/src/HOL/Relation.thy Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Relation.thy Tue Mar 11 10:20:44 2025 +0100
@@ -151,7 +151,7 @@
subsubsection \<open>Reflexivity\<close>
definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
- where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
+ where "refl_on A r \<longleftrightarrow> (\<forall>x\<in>A. (x, x) \<in> r)"
abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
where "refl \<equiv> refl_on UNIV"
@@ -170,7 +170,7 @@
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 refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
+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)
lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
@@ -186,12 +186,6 @@
lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
unfolding refl_on_def by blast
-lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A"
- unfolding refl_on_def by blast
-
-lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
- unfolding refl_on_def by blast
-
lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
unfolding refl_on_def by blast
@@ -252,10 +246,6 @@
lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
by (blast intro: refl_onI)
-lemma refl_on_def' [nitpick_unfold, code]:
- "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
- by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
-
lemma reflp_on_equality [simp]: "reflp_on A (=)"
by (simp add: reflp_on_def)
@@ -952,7 +942,7 @@
by blast
lemma refl_on_Id_on: "refl_on A (Id_on A)"
- by (rule refl_onI [OF Id_on_subset_Times Id_onI])
+ by (rule refl_onI[OF Id_onI])
lemma antisym_Id_on [simp]: "antisym (Id_on A)"
unfolding antisym_def by blast