# HG changeset patch
# User desharna
# Date 1671461643 -3600
# Node ID b35ffbe82031f139694e3d5192a0b2594cd02e0b
# Parent  53e40173cae5f0b6977464804077a970fd94ae15
added lemmas trans_on_subset and transp_on_subset

diff -r 53e40173cae5 -r b35ffbe82031 NEWS
--- 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":
diff -r 53e40173cae5 -r b35ffbe82031 src/HOL/Relation.thy
--- 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)