--- a/src/HOL/Relation.thy Mon Dec 19 15:33:13 2022 +0100
+++ b/src/HOL/Relation.thy Tue Dec 20 08:41:01 2022 +0100
@@ -663,8 +663,13 @@
lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))"
by (fact trans_INTER [to_pred])
-
-lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+
+lemma trans_on_join [code]:
+ "trans_on A r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. x \<in> A \<longrightarrow> y1 \<in> A \<longrightarrow>
+ (\<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> z \<in> A \<longrightarrow> (x, z) \<in> r))"
+ by (auto simp: trans_on_def)
+
+lemma trans_join: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
by (auto simp add: trans_def)
lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}"