# 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 @@ (\y m. n = Suc m \ P x y \ (P ^^ m) y z \ Q) \ Q" by (fact relpow_E2 [to_pred]) +lemma relpowp_trans[trans]: "(R ^^ i) x y \ (R ^^ j) y z \ (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 \(R ^^ Suc i) x y\[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 \R x x'\ . + next + show "(R ^^ (i + j)) x' z" + using Suc.IH[OF \(R ^^ i) x' y\ \(R ^^ j) y z\] . + qed +qed + +lemma relpow_trans[trans]: "(x, y) \ R ^^ i \ (y, z) \ R ^^ j \ (x, z) \ R ^^ (i + j)" + using relpowp_trans[to_set] . + lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" by (induct n) auto