diff -r d33fc5228aae -r 44a3e883ccda src/HOL/Relation.thy
--- 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}"