--- 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
--- 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