# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1575292948 -3600
# Node ID 777d673fa672f57ce2b852d32a22886f59c78ac6
# Parent  a8ccea88b7250a9b4624a8ea9e892448f1ce3c02
Removed duplicate theorems from HOL-Analysis

diff -r a8ccea88b725 -r 777d673fa672 src/HOL/Analysis/Retracts.thy
--- 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
diff -r a8ccea88b725 -r 777d673fa672 src/HOL/Analysis/Smooth_Paths.thy
--- 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