added lemmas trans_on_subset and transp_on_subset

--- a/NEWS	Mon Dec 19 15:52:15 2022 +0100
+++ b/NEWS	Mon Dec 19 15:54:03 2022 +0100
@@ -112,8 +112,10 @@
       totalp_on_singleton[simp]
       trans_onD
       trans_onI
+      trans_on_subset
       transp_onD
       transp_onI
+      transp_on_subset
       transp_on_trans_on_eq[pred_set_conv]
 
 * Theory "HOL.Transitive_Closure":

--- a/src/HOL/Relation.thy	Mon Dec 19 15:52:15 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 15:54:03 2022 +0100
@@ -668,6 +668,12 @@
 lemma transpD[dest?]: "transp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   by (rule transD[to_pred])
 
+lemma trans_on_subset: "trans_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> trans_on B r"
+  by (auto simp: trans_on_def)
+
+lemma transp_on_subset: "transp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> transp_on B R"
+  by (auto simp: transp_on_def)
+
 lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
   by (fast intro: transI elim: transE)