# HG changeset patch
# User desharna
# Date 1671460605 -3600
# Node ID 201cbd9027fc0d2de89d3452c3bdb0fda18b9353
# Parent  44a3e883ccda5c1ea6811550d4cf3765b3d4c368
added lemma transp_on_trans_on_eq[pred_set_conv]

diff -r 44a3e883ccda -r 201cbd9027fc NEWS
--- a/NEWS	Tue Dec 20 08:41:01 2022 +0100
+++ b/NEWS	Mon Dec 19 15:36:45 2022 +0100
@@ -110,6 +110,7 @@
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]
+      transp_on_trans_on_eq[pred_set_conv]
 
 * Theory "HOL.Transitive_Closure":
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
diff -r 44a3e883ccda -r 201cbd9027fc src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Dec 20 08:41:01 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 15:36:45 2022 +0100
@@ -623,8 +623,10 @@
 
 text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close>
 
-lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
-  by (simp add: trans_def transp_def)
+lemma transp_on_trans_on_eq[pred_set_conv]: "transp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans_on A r"
+  by (simp add: trans_on_def transp_on_def)
+
+lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
 lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
   by (unfold trans_def) iprover