# HG changeset patch
# User desharna
# Date 1707981925 -3600
# Node ID 8836386d6e3f0cc67a03033ff3fc1193e110b3c0
# Parent  97612262718aadb099a62b5016b9248feb10a9f3# Parent  ad29777e8746b6422f582ff15936a36c383a4fba
merged

diff -r ad29777e8746 -r 8836386d6e3f NEWS
--- a/NEWS	Wed Feb 14 19:03:14 2024 +0000
+++ b/NEWS	Thu Feb 15 08:25:25 2024 +0100
@@ -46,6 +46,11 @@
 
 * Lemma even_succ_div_2 renamed to even_half_succ_eq.  Minor INCOMPATIBILITY.
 
+* Theory "HOL.Transitive_Closure":
+  - Added lemmas.
+      relpow_trans[trans]
+      relpowp_trans[trans]
+
 * Theory "HOL-Library.Multiset":
   - Added lemmas.
       trans_on_mult
diff -r ad29777e8746 -r 8836386d6e3f src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Feb 14 19:03:14 2024 +0000
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 15 08:25:25 2024 +0100
@@ -913,6 +913,29 @@
     (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (fact relpow_E2 [to_pred])
 
+lemma relpowp_trans[trans]: "(R ^^ i) x y \<Longrightarrow> (R ^^ j) y z \<Longrightarrow> (R ^^ (i + j)) x z"
+proof (induction i arbitrary: x)
+  case 0
+  thus ?case by simp
+next
+  case (Suc i)
+  obtain x' where "R x x'" and "(R ^^ i) x' y"
+    using \<open>(R ^^ Suc i) x y\<close>[THEN relpowp_Suc_D2] by auto
+
+  show "(R ^^ (Suc i + j)) x z"
+    unfolding add_Suc
+  proof (rule relpowp_Suc_I2)
+    show "R x x'"
+      using \<open>R x x'\<close> .
+  next
+    show "(R ^^ (i + j)) x' z"
+      using Suc.IH[OF \<open>(R ^^ i) x' y\<close> \<open>(R ^^ j) y z\<close>] .
+  qed
+qed
+
+lemma relpow_trans[trans]: "(x, y) \<in> R ^^ i \<Longrightarrow> (y, z) \<in> R ^^ j \<Longrightarrow> (x, z) \<in> R ^^ (i + j)"
+  using relpowp_trans[to_set] .
+
 lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
   by (induct n) auto