# HG changeset patch
# User desharna
# Date 1671462464 -3600
# Node ID 66f17783913b2117b1b4724e23827205f88d2daa
# Parent  f70a7ff13b1051e5eab61fbac27934ba0e978e0a
strengthened and renamed trans_reflclI

diff -r f70a7ff13b10 -r 66f17783913b NEWS
--- a/NEWS	Mon Dec 19 16:05:57 2022 +0100
+++ b/NEWS	Mon Dec 19 16:07:44 2022 +0100
@@ -127,6 +127,7 @@
       antisym_reflcl[simp] ~> antisym_on_reflcl[simp]
       reflp_rtranclp[simp] ~> reflp_on_rtranclp[simp]
       symp_symclp[simp] ~> symp_on_symclp[simp]
+      trans_reflclI[simp] ~> trans_on_reflcl[simp]
   - Added lemmas.
       antisymp_on_reflcp[simp]
       reflclp_ident_if_reflp[simp]
diff -r f70a7ff13b10 -r 66f17783913b src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Dec 19 16:05:57 2022 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Dec 19 16:07:44 2022 +0100
@@ -82,11 +82,11 @@
 lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
   by (rule antisym_on_reflcl[to_pred])
 
-lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)"
-  unfolding trans_def by blast
+lemma trans_on_reflcl[simp]: "trans_on A r \<Longrightarrow> trans_on A (r\<^sup>=)"
+  by (auto intro: trans_onI dest: trans_onD)
 
 lemma transp_on_reflclp[simp]: "transp_on A R \<Longrightarrow> transp_on A R\<^sup>=\<^sup>="
-  by (auto intro: transp_onI dest: transp_onD)
+  by (rule trans_on_reflcl[to_pred])
 
 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast