# HG changeset patch
# User desharna
# Date 1742563304 -3600
# Node ID df99e867c63e39e131874b0941e6a1b8a2e22d9a
# Parent  a3b556a235410fdc49b03de4f746f0199a556934
added lemma trans_on_diff_Id

diff -r a3b556a23541 -r df99e867c63e NEWS
--- a/NEWS	Fri Mar 21 10:48:48 2025 +0000
+++ b/NEWS	Fri Mar 21 14:21:44 2025 +0100
@@ -55,6 +55,7 @@
       totalp_on_mono_stronger_alt
       totalp_on_top[simp]
       trans_on_bot[simp]
+      trans_on_diff_Id
       trans_on_top[simp]
       transp_on_bot[simp]
       transp_on_top[simp]
diff -r a3b556a23541 -r df99e867c63e src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Mar 21 10:48:48 2025 +0000
+++ b/src/HOL/Relation.thy	Fri Mar 21 14:21:44 2025 +0100
@@ -1013,8 +1013,11 @@
 lemma irrefl_diff_Id [simp]: "irrefl (r - Id)"
   by (simp add: irrefl_def)
 
-lemma trans_diff_Id: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)"
-  unfolding antisym_def trans_def by blast
+lemma trans_on_diff_Id: "trans_on A r \<Longrightarrow> antisym_on A r \<Longrightarrow> trans_on A (r - Id)"
+  by (blast intro: trans_onI dest: trans_onD antisym_onD)
+
+lemma trans_diff_Id[no_atp]: "trans r \<Longrightarrow> antisym r \<Longrightarrow> trans (r - Id)"
+  using trans_on_diff_Id .
 
 lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
   by (simp add: total_on_def)