--- a/src/HOL/Analysis/Retracts.thy Mon Dec 02 14:22:03 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy Mon Dec 02 14:22:28 2019 +0100
@@ -2592,50 +2592,4 @@
using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
-lemma path_connected_arc_complement:
- fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "arc \<gamma>" "2 \<le> DIM('a)"
- shows "path_connected(- path_image \<gamma>)"
-proof -
- have "path_image \<gamma> homeomorphic {0..1::real}"
- by (simp add: assms homeomorphic_arc_image_interval)
- then
- show ?thesis
- apply (rule path_connected_complement_homeomorphic_convex_compact)
- apply (auto simp: assms)
- done
-qed
-
-lemma connected_arc_complement:
- fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "arc \<gamma>" "2 \<le> DIM('a)"
- shows "connected(- path_image \<gamma>)"
- by (simp add: assms path_connected_arc_complement path_connected_imp_connected)
-
-lemma inside_arc_empty:
- fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "arc \<gamma>"
- shows "inside(path_image \<gamma>) = {}"
-proof (cases "DIM('a) = 1")
- case True
- then show ?thesis
- using assms connected_arc_image connected_convex_1_gen inside_convex by blast
-next
- case False
- show ?thesis
- proof (rule inside_bounded_complement_connected_empty)
- show "connected (- path_image \<gamma>)"
- apply (rule connected_arc_complement [OF assms])
- using False
- by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
- show "bounded (path_image \<gamma>)"
- by (simp add: assms bounded_arc_image)
- qed
-qed
-
-lemma inside_simple_curve_imp_closed:
- fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
- shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
- using arc_simple_path inside_arc_empty by blast
-
end
--- a/src/HOL/Analysis/Smooth_Paths.thy Mon Dec 02 14:22:03 2019 +0100
+++ b/src/HOL/Analysis/Smooth_Paths.thy Mon Dec 02 14:22:28 2019 +0100
@@ -9,36 +9,6 @@
subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
-lemma homeomorphism_arc:
- fixes g :: "real \<Rightarrow> 'a::t2_space"
- assumes "arc g"
- obtains h where "homeomorphism {0..1} (path_image g) g h"
-using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)
-
-lemma homeomorphic_arc_image_interval:
- fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
- assumes "arc g" "a < b"
- shows "(path_image g) homeomorphic {a..b}"
-proof -
- have "(path_image g) homeomorphic {0..1::real}"
- by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
- also have "\<dots> homeomorphic {a..b}"
- using assms by (force intro: homeomorphic_closed_intervals_real)
- finally show ?thesis .
-qed
-
-lemma homeomorphic_arc_images:
- fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
- assumes "arc g" "arc h"
- shows "(path_image g) homeomorphic (path_image h)"
-proof -
- have "(path_image g) homeomorphic {0..1::real}"
- by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
- also have "\<dots> homeomorphic (path_image h)"
- by (meson assms homeomorphic_def homeomorphism_arc)
- finally show ?thesis .
-qed
-
lemma path_connected_arc_complement:
fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
assumes "arc \<gamma>" "2 \<le> DIM('a)"
@@ -487,4 +457,4 @@
lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
by (simp add: Let_def rectpath_def)
-end
\ No newline at end of file
+end