# HG changeset patch
# User desharna
# Date 1671462737 -3600
# Node ID 66cae055ac7b0ba84ad4fd9102e906d98322c9b3
# Parent  66f17783913b2117b1b4724e23827205f88d2daa
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep

diff -r 66f17783913b -r 66cae055ac7b NEWS
--- a/NEWS	Mon Dec 19 16:07:44 2022 +0100
+++ b/NEWS	Mon Dec 19 16:12:17 2022 +0100
@@ -45,6 +45,7 @@
     for backward compatibility but their usage is discouraged.
     Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+      antisym_converse[simp] ~> antisym_on_converse[simp]
       order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
       order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
       preorder.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
@@ -56,9 +57,9 @@
       preorder.transp_le[simp] ~> preorder.transp_on_le[simp]
       preorder.transp_less[simp] ~> preorder.transp_on_less[simp]
       reflp_equality[simp] ~> reflp_on_equality[simp]
+      sym_converse[simp] ~> sym_on_converse[simp]
       total_on_singleton
-      sym_converse[simp] ~> sym_on_converse[simp]
-      antisym_converse[simp] ~> antisym_on_converse[simp]
+      trans_converse[simp] ~> trans_on_converse[simp]
   - Added lemmas.
       antisym_onD
       antisym_onI
@@ -119,6 +120,7 @@
       trans_on_subset
       transp_onD
       transp_onI
+      transp_on_conversep
       transp_on_subset
       transp_on_trans_on_eq[pred_set_conv]
 
diff -r 66f17783913b -r 66cae055ac7b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 16:07:44 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 16:12:17 2022 +0100
@@ -1179,8 +1179,11 @@
 lemma antisymp_on_conversep [simp]: "antisymp_on A R\<inverse>\<inverse> = antisymp_on A R"
   by (rule antisym_on_converse[to_pred])
 
-lemma trans_converse [simp]: "trans (converse r) = trans r"
-  unfolding trans_def by blast
+lemma trans_on_converse [simp]: "trans_on A (r\<inverse>) = trans_on A r"
+  by (auto intro: trans_onI dest: trans_onD)
+
+lemma transp_on_conversep [simp]: "transp_on A R\<inverse>\<inverse> = transp_on A R"
+  by (rule trans_on_converse[to_pred])
 
 lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r"
   unfolding sym_def by fast