src/HOL/Analysis/Path_Connected.thy

 lemma simple_path_linepath[intro]: "a \<noteq> b \<Longrightarrow> simple_path (linepath a b)"
   by (simp add: arc_imp_simple_path arc_linepath)
 
 lemma linepath_trivial [simp]: "linepath a a x = a"
   by (simp add: linepath_def real_vector.scale_left_diff_distrib)
+
+lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
+  by auto
 
 lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
   by (simp add: subpath_def linepath_def algebra_simps)
 
 lemma linepath_of_real: "(linepath (of_real a) (of_real b) x) = of_real ((1 - x)*a + x*b)"

       done
   qed
   with assms show ?thesis
     by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
 qed
+
 
 subsection\<open>Contractible sets\<close>
 
 definition contractible where
  "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"