# HG changeset patch
# User desharna
# Date 1708339140 -3600
# Node ID 9f36a31fe7ae86fc3e6e42b252383325474b899f
# Parent  d4c077078497434feed6741b45503d0f1842b91c
added lemmas relpowp_left_unique and relpow_left_unique

diff -r d4c077078497 -r 9f36a31fe7ae NEWS
--- a/NEWS	Mon Feb 19 11:21:06 2024 +0100
+++ b/NEWS	Mon Feb 19 11:39:00 2024 +0100
@@ -48,8 +48,10 @@
 
 * Theory "HOL.Transitive_Closure":
   - Added lemmas.
+      relpow_left_unique
       relpow_right_unique
       relpow_trans[trans]
+      relpowp_left_unique
       relpowp_right_unique
       relpowp_trans[trans]
 
diff -r d4c077078497 -r 9f36a31fe7ae src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Feb 19 11:21:06 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Feb 19 11:39:00 2024 +0100
@@ -936,6 +936,41 @@
 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_left_unique:
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and n :: nat and x y z :: 'a
+  assumes lunique: "\<And>x y z. R x z \<Longrightarrow> R y z \<Longrightarrow> x = y"
+  shows "(R ^^ n) x z \<Longrightarrow> (R ^^ n) y z \<Longrightarrow> x = y"
+proof (induction n arbitrary: x y z)
+  case 0
+  thus ?case
+    by simp
+next
+  case (Suc n')
+  then obtain x' y' :: 'a where
+    "(R ^^ n') x x'" and "R x' z" and
+    "(R ^^ n') y y'" and "R y' z"
+    by auto
+
+  have "x' = y'"
+    using lunique[OF \<open>R x' z\<close> \<open>R y' z\<close>] .
+
+  show "x = y"
+  proof (rule Suc.IH)
+    show "(R ^^ n') x x'"
+      using \<open>(R ^^ n') x x'\<close> .
+  next
+    show "(R ^^ n') y x'"
+      using \<open>(R ^^ n') y y'\<close>
+      unfolding \<open>x' = y'\<close> .
+  qed
+qed
+
+lemma relpow_left_unique:
+  fixes R :: "('a \<times> 'a) set" and n :: nat and x y z :: 'a
+  shows "(\<And>x y z. (x, z) \<in> R \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> x = y) \<Longrightarrow>
+    (x, z) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> x = y"
+  using relpowp_left_unique[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"