# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1458136626 0
# Node ID de25474ce728ef8e4824b87c9f6dbf39973725da
# Parent  dbc62f86a1a9b95b7094d00f7581bd16a6cd03f8
Contractible sets. Also removal of obsolete theorems and refactoring

diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -686,4 +686,67 @@
     by (rule order_antisym)
 qed
 
+lemma cSup_abs_le: 
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+  apply (auto simp add: abs_le_iff intro: cSup_least)
+  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
+
+lemma cInf_abs_ge:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
+  shows "\<bar>Inf S\<bar> \<le> a"
+proof -
+  have "Sup (uminus ` S) = - (Inf S)"
+  proof (rule antisym)
+    show "- (Inf S) \<le> Sup(uminus ` S)"
+      apply (subst minus_le_iff)
+      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
+      apply (subst minus_le_iff)
+      apply (rule cSup_upper, force)
+      using bdd apply (force simp add: abs_le_iff bdd_above_def)
+      done
+  next
+    show "Sup (uminus ` S) \<le> - Inf S"
+      apply (rule cSup_least)
+       using \<open>S \<noteq> {}\<close> apply (force simp add: )
+      apply clarsimp  
+      apply (rule cInf_lower)
+      apply assumption
+      using bdd apply (simp add: bdd_below_def)
+      apply (rule_tac x="-a" in exI)
+      apply force
+      done
+  qed
+  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
+qed
+
+lemma cSup_asclose:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes S: "S \<noteq> {}"
+    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+  shows "\<bar>Sup S - l\<bar> \<le> e"
+proof -
+  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+    by arith
+  have "bdd_above S"
+    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
+  with S b show ?thesis
+    unfolding th by (auto intro!: cSup_upper2 cSup_least)
+qed
+
+lemma cInf_asclose:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes S: "S \<noteq> {}"
+    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+  shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+    by arith
+  have "bdd_below S"
+    using b by (auto intro!: bdd_belowI[of _ "l - e"])
+  with S b show ?thesis
+    unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
+qed
+
 end
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -12,15 +12,8 @@
 imports Complex_Main Extended_Nat Liminf_Limsup
 begin
 
-text \<open>
-
-This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
-AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
-
-\<close>
-
-lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
-  by auto
+text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
+AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close>
 
 lemma incseq_setsumI2:
   fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -6286,7 +6286,13 @@
   obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
     by (auto simp: dist_norm)
   def R \<equiv> "1 + \<bar>B\<bar> + norm z"
-  have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero)
+  have "R > 0" unfolding R_def 
+  proof -
+    have "0 \<le> cmod z + \<bar>B\<bar>"
+      by (metis (full_types) add_nonneg_nonneg norm_ge_zero real_norm_def)
+    then show "0 < 1 + \<bar>B\<bar> + cmod z"
+      by linarith
+  qed 
   have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
     apply (rule Cauchy_integral_circlepath)
     using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -6377,11 +6377,14 @@
 definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
   "open_segment a b \<equiv> closed_segment a b - {a,b}"
 
+lemmas segment = open_segment_def closed_segment_def
+
 definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
 
 definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
 
-lemmas segment = open_segment_def closed_segment_def
+lemma starlike_UNIV [simp]: "starlike UNIV"
+  by (simp add: starlike_def)
 
 lemma midpoint_refl: "midpoint x x = x"
   unfolding midpoint_def
@@ -6540,6 +6543,9 @@
 lemma open_segment_idem [simp]: "open_segment a a = {}"
   by (simp add: open_segment_def)
 
+lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
+  using open_segment_def by auto
+  
 lemma closed_segment_eq_real_ivl:
   fixes a b::real
   shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
@@ -7903,6 +7909,28 @@
 
 lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
 
+lemma starlike_convex_tweak_boundary_points:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
+  shows "starlike T"
+proof -
+  have "rel_interior S \<noteq> {}"
+    by (simp add: assms rel_interior_eq_empty)
+  then obtain a where a: "a \<in> rel_interior S"  by blast 
+  with ST have "a \<in> T"  by blast 
+  have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
+    apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
+    using assms by blast
+  show ?thesis
+    unfolding starlike_def
+    apply (rule bexI [OF _ \<open>a \<in> T\<close>])
+    apply (simp add: closed_segment_eq_open)
+    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
+    apply (simp add: order_trans [OF * ST])
+    done
+qed
+
+subsection\<open>The relative frontier of a set\<close>
 
 definition "rel_frontier S = closure S - rel_interior S"
 
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -11,79 +11,10 @@
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
-lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
-  apply (auto simp add: abs_le_iff intro: cSup_least)
-  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
-
-lemma cInf_abs_ge:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
-  shows "\<bar>Inf S\<bar> \<le> a"
-proof -
-  have "Sup (uminus ` S) = - (Inf S)"
-  proof (rule antisym)
-    show "- (Inf S) \<le> Sup(uminus ` S)"
-      apply (subst minus_le_iff)
-      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
-      apply (subst minus_le_iff)
-      apply (rule cSup_upper, force)
-      using bdd apply (force simp add: abs_le_iff bdd_above_def)
-      done
-  next
-    show "Sup (uminus ` S) \<le> - Inf S"
-      apply (rule cSup_least)
-       using \<open>S \<noteq> {}\<close> apply (force simp add: )
-      apply clarsimp  
-      apply (rule cInf_lower)
-      apply assumption
-      using bdd apply (simp add: bdd_below_def)
-      apply (rule_tac x="-a" in exI)
-      apply force
-      done
-  qed
-  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
-qed
-
-lemma cSup_asclose:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes S: "S \<noteq> {}"
-    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
-  shows "\<bar>Sup S - l\<bar> \<le> e"
-proof -
-  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
-    by arith
-  have "bdd_above S"
-    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
-  with S b show ?thesis
-    unfolding th by (auto intro!: cSup_upper2 cSup_least)
-qed
-
-lemma cInf_asclose:
-  fixes S :: "real set"
-  assumes S: "S \<noteq> {}"
-    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
-  shows "\<bar>Inf S - l\<bar> \<le> e"
-proof -
-  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
-    by auto
-  also have "\<dots> \<le> e"
-    apply (rule cSup_asclose)
-    using abs_minus_add_cancel b by (auto simp add: S)
-  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
-  then show ?thesis
-    by (simp add: Inf_real_def)
-qed
-
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
 
-lemma real_arch_invD:
-  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
-  by (subst(asm) real_arch_inverse)
-
 
 subsection \<open>Sundries\<close>
 
@@ -4595,6 +4526,10 @@
 
 subsection \<open>Uniform limit of integrable functions is integrable.\<close>
 
+lemma real_arch_invD:
+  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
+  by (subst(asm) real_arch_inverse)
+
 lemma integrable_uniform_limit:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
   assumes "\<forall>e>0. \<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -3128,9 +3128,9 @@
   done
 
 proposition homotopic_compose_continuous_left:
-   "homotopic_with (\<lambda>f. True) X Y f g \<and>
-        continuous_on Y h \<and> image h Y \<subseteq> Z
-        \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
+   "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
+     continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
+    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
   using homotopic_with_compose_continuous_left by fastforce
 
 proposition homotopic_with_Pair:
@@ -4053,4 +4053,267 @@
     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)"
+
+proposition contractible_imp_simply_connected:
+  fixes S :: "_::real_normed_vector set"
+  assumes "contractible S" shows "simply_connected S"
+proof (cases "S = {}")
+  case True then show ?thesis by force
+next
+  case False
+  obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+    using assms by (force simp add: contractible_def)
+  then have "a \<in> S"
+    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
+  show ?thesis
+    apply (simp add: simply_connected_eq_contractible_loop_all False)
+    apply (rule bexI [OF _ \<open>a \<in> S\<close>])
+    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def)
+    apply clarify
+    apply (rule_tac x="(h o (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
+    apply (intro conjI continuous_on_compose continuous_intros)
+    apply (erule continuous_on_subset | force)+
+    done
+qed
+
+corollary contractible_imp_connected:
+  fixes S :: "_::real_normed_vector set"
+  shows "contractible S \<Longrightarrow> connected S"
+by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)
+
+lemma contractible_imp_path_connected:
+  fixes S :: "_::real_normed_vector set"
+  shows "contractible S \<Longrightarrow> path_connected S"
+by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)
+
+lemma nullhomotopic_through_contractible:
+  fixes S :: "_::topological_space set"
+  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+      and g: "continuous_on T g" "g ` T \<subseteq> U"
+      and T: "contractible T"
+    obtains c where "homotopic_with (\<lambda>h. True) S U (g o f) (\<lambda>x. c)"
+proof -
+  obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
+    using assms by (force simp add: contractible_def)
+  have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
+    by (rule homotopic_compose_continuous_left [OF b g])
+  then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
+    by (rule homotopic_compose_continuous_right [OF _ f])
+  then show ?thesis
+    by (simp add: comp_def that)
+qed
+
+lemma nullhomotopic_into_contractible:
+  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+      and T: "contractible T"
+    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+apply (rule nullhomotopic_through_contractible [OF f, of id T])
+using assms
+apply (auto simp: continuous_on_id)
+done
+
+lemma nullhomotopic_from_contractible:
+  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+      and S: "contractible S"
+    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
+using assms
+apply (auto simp: comp_def)
+done
+
+lemma homotopic_through_contractible:
+  fixes S :: "_::real_normed_vector set"
+  assumes "continuous_on S f1" "f1 ` S \<subseteq> T"
+          "continuous_on T g1" "g1 ` T \<subseteq> U"
+          "continuous_on S f2" "f2 ` S \<subseteq> T"
+          "continuous_on T g2" "g2 ` T \<subseteq> U"
+          "contractible T" "path_connected U"
+   shows "homotopic_with (\<lambda>h. True) S U (g1 o f1) (g2 o f2)"
+proof -
+  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 o f1) (\<lambda>x. c1)"
+    apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
+    using assms apply (auto simp: )
+    done
+  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 o f2) (\<lambda>x. c2)"
+    apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
+    using assms apply (auto simp: )
+    done
+  have *: "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
+  proof (cases "S = {}")
+    case True then show ?thesis by force
+  next
+    case False
+    with c1 c2 have "c1 \<in> U" "c2 \<in> U"
+      using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
+    with \<open>path_connected U\<close> show ?thesis by blast
+  qed
+  show ?thesis
+    apply (rule homotopic_with_trans [OF c1])
+    apply (rule homotopic_with_symD)
+    apply (rule homotopic_with_trans [OF c2])
+    apply (simp add: path_component homotopic_constant_maps *)
+    done
+qed
+
+lemma homotopic_into_contractible:
+  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
+  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+      and g: "continuous_on S g" "g ` S \<subseteq> T"
+      and T: "contractible T"
+    shows "homotopic_with (\<lambda>h. True) S T f g"
+using homotopic_through_contractible [of S f T id T g id]
+by (simp add: assms contractible_imp_path_connected continuous_on_id)
+
+lemma homotopic_from_contractible:
+  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
+  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
+      and g: "continuous_on S g" "g ` S \<subseteq> T"
+      and "contractible S" "path_connected T"
+    shows "homotopic_with (\<lambda>h. True) S T f g"
+using homotopic_through_contractible [of S id S f T id g]
+by (simp add: assms contractible_imp_path_connected continuous_on_id)
+
+lemma starlike_imp_contractible_gen:
+  fixes S :: "'a::real_normed_vector set"
+  assumes S: "starlike S"
+      and P: "\<And>a T. \<lbrakk>a \<in> S; 0 \<le> T; T \<le> 1\<rbrakk> \<Longrightarrow> P(\<lambda>x. (1 - T) *\<^sub>R x + T *\<^sub>R a)"
+    obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
+proof -
+  obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
+    using S by (auto simp add: starlike_def)
+  have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
+    apply clarify
+    apply (erule a [unfolded closed_segment_def, THEN subsetD])
+    apply (simp add: )
+    apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
+    done
+  then show ?thesis
+    apply (rule_tac a="a" in that)
+    using \<open>a \<in> S\<close>
+    apply (simp add: homotopic_with_def)
+    apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
+    apply (intro conjI ballI continuous_on_compose continuous_intros)
+    apply (simp_all add: P)
+    done
+qed
+
+lemma starlike_imp_contractible:
+  fixes S :: "'a::real_normed_vector set"
+  shows "starlike S \<Longrightarrow> contractible S"
+using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
+
+lemma contractible_UNIV: "contractible (UNIV :: 'a::real_normed_vector set)"
+  by (simp add: starlike_imp_contractible)
+
+lemma starlike_imp_simply_connected:
+  fixes S :: "'a::real_normed_vector set"
+  shows "starlike S \<Longrightarrow> simply_connected S"
+by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
+
+lemma convex_imp_simply_connected:
+  fixes S :: "'a::real_normed_vector set"
+  shows "convex S \<Longrightarrow> simply_connected S"
+using convex_imp_starlike starlike_imp_simply_connected by blast
+
+lemma starlike_imp_path_connected:
+  fixes S :: "'a::real_normed_vector set"
+  shows "starlike S \<Longrightarrow> path_connected S"
+by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
+
+lemma starlike_imp_connected:
+  fixes S :: "'a::real_normed_vector set"
+  shows "starlike S \<Longrightarrow> connected S"
+by (simp add: path_connected_imp_connected starlike_imp_path_connected)
+
+lemma is_interval_simply_connected_1:
+  fixes S :: "real set"
+  shows "is_interval S \<longleftrightarrow> simply_connected S"
+using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
+
+lemma contractible_empty: "contractible {}"
+  by (simp add: continuous_on_empty contractible_def homotopic_with)
+
+lemma contractible_convex_tweak_boundary_points:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" and TS: "rel_interior S \<subseteq> T" "T \<subseteq> closure S"
+  shows "contractible T"
+proof (cases "S = {}")
+  case True
+  with assms show ?thesis
+    by (simp add: contractible_empty subsetCE)
+next
+  case False
+  show ?thesis
+    apply (rule starlike_imp_contractible)
+    apply (rule starlike_convex_tweak_boundary_points [OF \<open>convex S\<close> False TS])
+    done
+qed
+
+lemma convex_imp_contractible:
+  fixes S :: "'a::real_normed_vector set"
+  shows "convex S \<Longrightarrow> contractible S"
+using contractible_empty convex_imp_starlike starlike_imp_contractible by auto
+
+lemma contractible_sing:
+  fixes a :: "'a::real_normed_vector"
+  shows "contractible {a}"
+by (rule convex_imp_contractible [OF convex_singleton])
+
+lemma is_interval_contractible_1:
+  fixes S :: "real set"
+  shows  "is_interval S \<longleftrightarrow> contractible S"
+using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1 
+      is_interval_simply_connected_1 by auto
+
+lemma contractible_times:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes S: "contractible S" and T: "contractible T"
+  shows "contractible (S \<times> T)"
+proof -
+  obtain a h where conth: "continuous_on ({0..1} \<times> S) h" 
+             and hsub: "h ` ({0..1} \<times> S) \<subseteq> S"
+             and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (0, x) = x" 
+             and [simp]: "\<And>x. x \<in> S \<Longrightarrow>  h (1::real, x) = a"
+    using S by (auto simp add: contractible_def homotopic_with)
+  obtain b k where contk: "continuous_on ({0..1} \<times> T) k" 
+             and ksub: "k ` ({0..1} \<times> T) \<subseteq> T"
+             and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (0, x) = x" 
+             and [simp]: "\<And>x. x \<in> T \<Longrightarrow>  k (1::real, x) = b"
+    using T by (auto simp add: contractible_def homotopic_with)
+  show ?thesis
+    apply (simp add: contractible_def homotopic_with)
+    apply (rule exI [where x=a])
+    apply (rule exI [where x=b])
+    apply (rule exI [where x = "\<lambda>z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
+    apply (intro conjI ballI continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
+    using hsub ksub 
+    apply (auto simp: )
+    done
+qed
+
+lemma homotopy_dominated_contractibility: 
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  assumes S: "contractible S"
+      and f: "continuous_on S f" "image f S \<subseteq> T" 
+      and g: "continuous_on T g" "image g T \<subseteq> S" 
+      and hom: "homotopic_with (\<lambda>x. True) T T (f o g) id"
+    shows "contractible T"
+proof -
+  obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
+    using nullhomotopic_from_contractible [OF f S] .
+  then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
+    by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
+  show ?thesis
+    apply (simp add: contractible_def)
+    apply (rule exI [where x = b])
+    apply (rule homotopic_with_symD)
+    apply (rule homotopic_with_trans [OF _ hom])
+    using homg apply (simp add: o_def)
+    done
+qed
+
 end
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -169,9 +169,13 @@
     qed
 qed
 
-lemma norm_lemma_xy: "\<lbrakk>\<bar>b\<bar> + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
-  by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear
-         norm_diff_ineq)
+lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
+proof -
+  have "b \<le> norm y - norm x"
+    using assms by linarith
+  then show ?thesis
+    by (metis (no_types) add.commute norm_diff_ineq order_trans)
+qed
 
 lemma polyfun_extremal:
   fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Real.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -1404,21 +1404,6 @@
 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
   by simp
 
-subsection\<open>Absolute Value Function for the Reals\<close>
-
-lemma abs_minus_add_cancel: "\<bar>x + (- y)\<bar> = \<bar>y + (- (x::real))\<bar>"
-  by (simp add: abs_if)
-
-lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>"
-  by (simp add: abs_if)
-
-lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x"
-  by simp
-
-lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (-l + -m)\<bar> \<le> \<bar>x + -l\<bar> + \<bar>y + -m\<bar>"
-  by simp
-
-
 subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
 
 (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)
@@ -1564,7 +1549,7 @@
 proof -
   have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)"
     using assms by (induct n arbitrary: x) simp_all
-  then show ?thesis by (metis floor_of_int) 
+  then show ?thesis by (metis floor_of_int)
 qed
 
 lemma floor_numeral_power[simp]:
diff -r dbc62f86a1a9 -r de25474ce728 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Mar 15 14:08:25 2016 +0000
+++ b/src/HOL/Rings.thy	Wed Mar 16 13:57:06 2016 +0000
@@ -2088,6 +2088,9 @@
    "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
   by (auto simp add: diff_le_eq ac_simps abs_le_iff)
 
+lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
+  by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
+
 end
 
 subsection \<open>Dioids\<close>