# HG changeset patch
# User desharna
# Date 1671461535 -3600
# Node ID 53e40173cae5f0b6977464804077a970fd94ae15
# Parent  76f93e2620fef55b99627162830e995fb82d3d08
added lemmas trans_onD and transp_onD

diff -r 76f93e2620fe -r 53e40173cae5 NEWS
--- a/NEWS	Mon Dec 19 15:41:52 2022 +0100
+++ b/NEWS	Mon Dec 19 15:52:15 2022 +0100
@@ -110,7 +110,9 @@
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]
+      trans_onD
       trans_onI
+      transp_onD
       transp_onI
       transp_on_trans_on_eq[pred_set_conv]
 
diff -r 76f93e2620fe -r 53e40173cae5 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 15:41:52 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 15:52:15 2022 +0100
@@ -654,15 +654,19 @@
   obtains "r x z"
   using assms by (rule transE [to_pred])
 
-lemma transD [dest?]:
-  assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
-  shows "(x, z) \<in> r"
-  using assms by (rule transE)
+lemma trans_onD:
+  "trans_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
+  unfolding trans_on_def
+  by (elim ballE) iprover+
 
-lemma transpD [dest?]:
-  assumes "transp r" and "r x y" and "r y z"
-  shows "r x z"
-  using assms by (rule transD [to_pred])
+lemma transD[dest?]: "trans r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
+  by (simp add: trans_onD[of UNIV r x y z])
+
+lemma transp_onD: "transp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+  by (rule trans_onD[to_pred])
+
+lemma transpD[dest?]: "transp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+  by (rule transD[to_pred])
 
 lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
   by (fast intro: transI elim: transE)