# 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) \<in> R ^^ i \<Longrightarrow> (y, z) \<in> R ^^ j \<Longrightarrow> (x, z) \<in> R ^^ (i + j)"
   using relpowp_trans[to_set] .
 
+lemma relpowp_right_unique:
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and n :: nat and x y z :: 'a
+  assumes runique: "\<And>x y z. R x y \<Longrightarrow> R x z \<Longrightarrow> y = z"
+  shows "(R ^^ n) x y \<Longrightarrow> (R ^^ n) x z \<Longrightarrow> 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 \<times> 'a) set" and n :: nat and x y z :: 'a
+  shows "(\<And>x y z. (x, y) \<in> R \<Longrightarrow> (x, z) \<in> R \<Longrightarrow> y = z) \<Longrightarrow>
+    (x, y) \<in> (R ^^ n) \<Longrightarrow> (x, z) \<in> (R ^^ n) \<Longrightarrow> y = z"
+  using relpowp_right_unique[to_set] .
+
 lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
   by (induct n) auto