# HG changeset patch
# User desharna
# Date 1709647351 -3600
# Node ID 0e8620af9c9168fcb58d529c8459ef1d86fd54f4
# Parent  48af00f6f110c325a681a2839464a9f7793569f5
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp

diff -r 48af00f6f110 -r 0e8620af9c91 NEWS
--- a/NEWS	Mon Mar 04 21:58:53 2024 +0100
+++ b/NEWS	Tue Mar 05 15:02:31 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 48af00f6f110 -r 0e8620af9c91 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Tue Mar 05 15:02:31 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"