author paulson Wed, 16 Mar 2016 13:57:06 +0000 changeset 62626 de25474ce728 parent 62623 dbc62f86a1a9 child 62627 20288ba55e85
Contractible sets. Also removal of obsolete theorems and refactoring
```--- 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```
```--- 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"```
```--- 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)+```
```--- 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"
```
```--- 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

-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"```
```--- 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```
```--- 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"```
```--- 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]:```
```--- 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>```