diff -r 19cc354ba625 -r 35b2143aeec6 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Mar 28 08:30:42 2024 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Mar 28 13:32:57 2024 +0000
@@ -121,6 +121,20 @@
   using assms
   by (simp add: loop_free_linear_image_eq path_linear_image_eq simple_path_def)
 
+lemma simple_pathI [intro?]:
+  assumes "path p"
+  assumes "\<And>x y. 0 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> p x = p y \<Longrightarrow> x = 0 \<and> y = 1"
+  shows   "simple_path p"
+  unfolding simple_path_def loop_free_def
+proof (intro ballI conjI impI)
+  fix x y assume "x \<in> {0..1}" "y \<in> {0..1}" "p x = p y"
+  thus "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+    by (metis assms(2) atLeastAtMost_iff linorder_less_linear)
+qed fact+
+
+lemma arcD: "arc p \<Longrightarrow> p x = p y \<Longrightarrow> x \<in> {0..1} \<Longrightarrow> y \<in> {0..1} \<Longrightarrow> x = y"
+  by (auto simp: arc_def inj_on_def)
+
 lemma arc_translation_eq:
   fixes g :: "real \<Rightarrow> 'a::euclidean_space"
   shows "arc((\<lambda>x. a + x) \<circ> g) \<longleftrightarrow> arc g"
@@ -670,6 +684,38 @@
   using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
 
 
+subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Symmetry and loops\<close>
+
+lemma path_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
+  by auto
+
+lemma simple_path_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
+  by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
+
+lemma path_image_sym:
+  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
+     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
+  by (simp add: path_image_join sup_commute)
+
+lemma simple_path_joinI:
+  assumes "arc p1" "arc p2" "pathfinish p1 = pathstart p2"
+  assumes "path_image p1 \<inter> path_image p2 
+        \<subseteq> insert (pathstart p2) (if pathstart p1 = pathfinish p2 then {pathstart p1} else {})"
+  shows   "simple_path (p1 +++ p2)"
+  by (smt (verit, best) Int_commute arc_imp_simple_path arc_join assms insert_commute simple_path_join_loop simple_path_sym)
+
+lemma simple_path_join3I:
+  assumes "arc p1" "arc p2" "arc p3"
+  assumes "path_image p1 \<inter> path_image p2 \<subseteq> {pathstart p2}"
+  assumes "path_image p2 \<inter> path_image p3 \<subseteq> {pathstart p3}"
+  assumes "path_image p1 \<inter> path_image p3 \<subseteq> {pathstart p1} \<inter> {pathfinish p3}"
+  assumes "pathfinish p1 = pathstart p2" "pathfinish p2 = pathstart p3"
+  shows   "simple_path (p1 +++ p2 +++ p3)"
+  using assms by (intro simple_path_joinI arc_join) (auto simp: path_image_join)
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>The joining of paths is associative\<close>
 
 lemma path_assoc:
@@ -720,22 +766,6 @@
       \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
 by (simp add: arc_simple_path simple_path_assoc)
 
-subsubsection\<^marker>\<open>tag unimportant\<close>\<open>Symmetry and loops\<close>
-
-lemma path_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
-  by auto
-
-lemma simple_path_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
-     \<Longrightarrow> simple_path(p +++ q) \<longleftrightarrow> simple_path(q +++ p)"
-  by (metis (full_types) inf_commute insert_commute simple_path_joinE simple_path_join_loop)
-
-lemma path_image_sym:
-  "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk>
-     \<Longrightarrow> path_image(p +++ q) = path_image(q +++ p)"
-  by (simp add: path_image_join sup_commute)
-
 
 subsection\<open>Subpath\<close>