# HG changeset patch
# User desharna
# Date 1707924341 -3600
# Node ID 97612262718aadb099a62b5016b9248feb10a9f3
# Parent  1b3770369ee7b3c2c38d07aeac6988be16963fea
added lemmas relpow_trans[trans] and relpowp_trans[trans]

diff -r 1b3770369ee7 -r 97612262718a NEWS
--- a/NEWS	Wed Feb 14 08:31:24 2024 +0100
+++ b/NEWS	Wed Feb 14 16:25:41 2024 +0100
@@ -43,6 +43,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 1b3770369ee7 -r 97612262718a src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Feb 14 08:31:24 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Feb 14 16:25:41 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