merged

--- a/NEWS	Mon Feb 19 14:12:20 2024 +0000
+++ b/NEWS	Mon Feb 19 14:12:29 2024 +0000
@@ -48,7 +48,11 @@
 
 * Theory "HOL.Transitive_Closure":
   - Added lemmas.
+      relpow_left_unique
+      relpow_right_unique
       relpow_trans[trans]
+      relpowp_left_unique
+      relpowp_right_unique
       relpowp_trans[trans]
 
 * Theory "HOL-Library.Multiset":

--- a/src/HOL/Analysis/Retracts.thy	Mon Feb 19 14:12:20 2024 +0000
+++ b/src/HOL/Analysis/Retracts.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -1178,7 +1178,7 @@
       if "openin (top_of_set U) V" "T retract_of V" "U \<noteq> {}" for V
     using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
   obtain Ta where "(openin (top_of_set U) Ta \<and> T retract_of Ta)"
-    using ANR_def UT \<open>S homeomorphic T\<close> assms by moura
+    using ANR_def UT \<open>S homeomorphic T\<close> assms by atomize_elim (auto simp: choice)
   then show ?thesis
     using S \<open>U \<noteq> {}\<close> by blast
 qed

--- a/src/HOL/Library/Multiset_Order.thy	Mon Feb 19 14:12:20 2024 +0000
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -652,7 +652,7 @@
       by (metis image_mset_Diff image_mset_union)
   next
     obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
-      using ex_y by moura
+      using ex_y by metis
 
     show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
     proof (intro allI impI)

--- a/src/HOL/Transitive_Closure.thy	Mon Feb 19 14:12:20 2024 +0000
+++ b/src/HOL/Transitive_Closure.thy	Mon Feb 19 14:12:29 2024 +0000
@@ -936,6 +936,64 @@
 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"
+  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