# HG changeset patch # User desharna # Date 1708338066 -3600 # Node ID d4c077078497434feed6741b45503d0f1842b91c # Parent 65223730d7e1a704c81fbb86e667446a911daae5 added lemmas relpowp_right_unique and relpow_right_unique diff -r 65223730d7e1 -r d4c077078497 NEWS --- a/NEWS Mon Feb 19 08:23:23 2024 +0100 +++ b/NEWS Mon Feb 19 11:21:06 2024 +0100 @@ -48,7 +48,9 @@ * Theory "HOL.Transitive_Closure": - Added lemmas. + relpow_right_unique relpow_trans[trans] + relpowp_right_unique relpowp_trans[trans] * Theory "HOL-Library.Multiset": diff -r 65223730d7e1 -r d4c077078497 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Mon Feb 19 08:23:23 2024 +0100 +++ b/src/HOL/Transitive_Closure.thy Mon Feb 19 11:21:06 2024 +0100 @@ -936,6 +936,29 @@ lemma relpow_trans[trans]: "(x, y) \ R ^^ i \ (y, z) \ R ^^ j \ (x, z) \ R ^^ (i + j)" using relpowp_trans[to_set] . +lemma relpowp_right_unique: + fixes R :: "'a \ 'a \ bool" and n :: nat and x y z :: 'a + assumes runique: "\x y z. R x y \ R x z \ y = z" + shows "(R ^^ n) x y \ (R ^^ n) x z \ y = z" +proof (induction n arbitrary: x y z) + case 0 + thus ?case + by simp +next + case (Suc n') + then obtain x' :: 'a where + "(R ^^ n') x x'" and "R x' y" and "R x' z" + by auto + thus "y = z" + using runique by simp +qed + +lemma relpow_right_unique: + fixes R :: "('a \ 'a) set" and n :: nat and x y z :: 'a + shows "(\x y z. (x, y) \ R \ (x, z) \ R \ y = z) \ + (x, y) \ (R ^^ n) \ (x, z) \ (R ^^ n) \ y = z" + using relpowp_right_unique[to_set] . + lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" by (induct n) auto