# HG changeset patch
# User desharna
# Date 1709654121 -3600
# Node ID 1f94d92b0dc26746c013935b949ff44f1c88024c
# Parent  0e8620af9c9168fcb58d529c8459ef1d86fd54f4# Parent  817d33f8aa7fe9f356876e8fb17711cf811fb09e
merged

diff -r 817d33f8aa7f -r 1f94d92b0dc2 NEWS
--- a/NEWS	Tue Mar 05 14:32:50 2024 +0000
+++ b/NEWS	Tue Mar 05 16:55:21 2024 +0100
@@ -69,6 +69,8 @@
       relpowp_left_unique
       relpowp_right_unique
       relpowp_trans[trans]
+      rtranclp_ident_if_reflp_and_transp
+      tranclp_ident_if_and_transp
 
 * Theory "HOL-Library.Multiset":
   - Added lemmas.
diff -r 817d33f8aa7f -r 1f94d92b0dc2 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Mar 05 14:32:50 2024 +0000
+++ b/src/HOL/Transitive_Closure.thy	Tue Mar 05 16:55:21 2024 +0100
@@ -321,6 +321,27 @@
   then show ?thesis by auto
 qed
 
+lemma rtranclp_ident_if_reflp_and_transp:
+  assumes "reflp R" and "transp R"
+  shows "R\<^sup>*\<^sup>* = R"
+proof (intro ext iffI)
+  fix x y
+  show "R\<^sup>*\<^sup>* x y \<Longrightarrow> R x y"
+  proof (induction y rule: rtranclp_induct)
+    case base
+    show ?case
+      using \<open>reflp R\<close>[THEN reflpD] .
+  next
+    case (step y z)
+    thus ?case
+      using \<open>transp R\<close>[THEN transpD, of x y  z] by simp
+  qed
+next
+  fix x y
+  show "R x y \<Longrightarrow> R\<^sup>*\<^sup>* x y"
+    using r_into_rtranclp .
+qed
+
 
 subsection \<open>Transitive closure\<close>
 
@@ -735,6 +756,28 @@
 
 declare trancl_into_rtrancl [elim]
 
+lemma tranclp_ident_if_transp:
+  assumes "transp R"
+  shows "R\<^sup>+\<^sup>+ = R"
+proof (intro ext iffI)
+  fix x y
+  show "R\<^sup>+\<^sup>+ x y \<Longrightarrow> R x y"
+  proof (induction y rule: tranclp_induct)
+    case (base y)
+    thus ?case
+      by simp
+  next
+    case (step y z)
+    thus ?case
+      using \<open>transp R\<close>[THEN transpD, of x y  z] by simp
+  qed
+next
+  fix x y
+  show "R x y \<Longrightarrow> R\<^sup>+\<^sup>+ x y"
+    using tranclp.r_into_trancl .
+qed
+
+
 subsection \<open>Symmetric closure\<close>
 
 definition symclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"