Contractible sets. Also removal of obsolete theorems and refactoring
authorpaulson <lp15@cam.ac.uk>
Wed Mar 16 13:57:06 2016 +0000 (2016-03-16)
changeset 62626de25474ce728
parent 62623 dbc62f86a1a9
child 62627 20288ba55e85
Contractible sets. Also removal of obsolete theorems and refactoring
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/PolyRoots.thy
src/HOL/Real.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Mar 15 14:08:25 2016 +0000
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 16 13:57:06 2016 +0000
     1.3 @@ -686,4 +686,67 @@
     1.4      by (rule order_antisym)
     1.5  qed
     1.6  
     1.7 +lemma cSup_abs_le: 
     1.8 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
     1.9 +  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
    1.10 +  apply (auto simp add: abs_le_iff intro: cSup_least)
    1.11 +  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
    1.12 +
    1.13 +lemma cInf_abs_ge:
    1.14 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    1.15 +  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
    1.16 +  shows "\<bar>Inf S\<bar> \<le> a"
    1.17 +proof -
    1.18 +  have "Sup (uminus ` S) = - (Inf S)"
    1.19 +  proof (rule antisym)
    1.20 +    show "- (Inf S) \<le> Sup(uminus ` S)"
    1.21 +      apply (subst minus_le_iff)
    1.22 +      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
    1.23 +      apply (subst minus_le_iff)
    1.24 +      apply (rule cSup_upper, force)
    1.25 +      using bdd apply (force simp add: abs_le_iff bdd_above_def)
    1.26 +      done
    1.27 +  next
    1.28 +    show "Sup (uminus ` S) \<le> - Inf S"
    1.29 +      apply (rule cSup_least)
    1.30 +       using \<open>S \<noteq> {}\<close> apply (force simp add: )
    1.31 +      apply clarsimp  
    1.32 +      apply (rule cInf_lower)
    1.33 +      apply assumption
    1.34 +      using bdd apply (simp add: bdd_below_def)
    1.35 +      apply (rule_tac x="-a" in exI)
    1.36 +      apply force
    1.37 +      done
    1.38 +  qed
    1.39 +  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
    1.40 +qed
    1.41 +
    1.42 +lemma cSup_asclose:
    1.43 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    1.44 +  assumes S: "S \<noteq> {}"
    1.45 +    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
    1.46 +  shows "\<bar>Sup S - l\<bar> \<le> e"
    1.47 +proof -
    1.48 +  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    1.49 +    by arith
    1.50 +  have "bdd_above S"
    1.51 +    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
    1.52 +  with S b show ?thesis
    1.53 +    unfolding th by (auto intro!: cSup_upper2 cSup_least)
    1.54 +qed
    1.55 +
    1.56 +lemma cInf_asclose:
    1.57 +  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    1.58 +  assumes S: "S \<noteq> {}"
    1.59 +    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
    1.60 +  shows "\<bar>Inf S - l\<bar> \<le> e"
    1.61 +proof -
    1.62 +  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    1.63 +    by arith
    1.64 +  have "bdd_below S"
    1.65 +    using b by (auto intro!: bdd_belowI[of _ "l - e"])
    1.66 +  with S b show ?thesis
    1.67 +    unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
    1.68 +qed
    1.69 +
    1.70  end
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 15 14:08:25 2016 +0000
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 16 13:57:06 2016 +0000
     2.3 @@ -12,15 +12,8 @@
     2.4  imports Complex_Main Extended_Nat Liminf_Limsup
     2.5  begin
     2.6  
     2.7 -text \<open>
     2.8 -
     2.9 -This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    2.10 -AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.
    2.11 -
    2.12 -\<close>
    2.13 -
    2.14 -lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
    2.15 -  by auto
    2.16 +text \<open>This should be part of @{theory Extended_Nat} or @{theory Order_Continuity}, but then the
    2.17 +AFP-entry \<open>Jinja_Thread\<close> fails, as it does overload certain named from @{theory Complex_Main}.\<close>
    2.18  
    2.19  lemma incseq_setsumI2:
    2.20    fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::ordered_comm_monoid_add"
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Mar 15 14:08:25 2016 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Mar 16 13:57:06 2016 +0000
     3.3 @@ -6286,7 +6286,13 @@
     3.4    obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
     3.5      by (auto simp: dist_norm)
     3.6    def R \<equiv> "1 + \<bar>B\<bar> + norm z"
     3.7 -  have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero)
     3.8 +  have "R > 0" unfolding R_def 
     3.9 +  proof -
    3.10 +    have "0 \<le> cmod z + \<bar>B\<bar>"
    3.11 +      by (metis (full_types) add_nonneg_nonneg norm_ge_zero real_norm_def)
    3.12 +    then show "0 < 1 + \<bar>B\<bar> + cmod z"
    3.13 +      by linarith
    3.14 +  qed 
    3.15    have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
    3.16      apply (rule Cauchy_integral_circlepath)
    3.17      using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 15 14:08:25 2016 +0000
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Mar 16 13:57:06 2016 +0000
     4.3 @@ -6377,11 +6377,14 @@
     4.4  definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
     4.5    "open_segment a b \<equiv> closed_segment a b - {a,b}"
     4.6  
     4.7 +lemmas segment = open_segment_def closed_segment_def
     4.8 +
     4.9  definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
    4.10  
    4.11  definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
    4.12  
    4.13 -lemmas segment = open_segment_def closed_segment_def
    4.14 +lemma starlike_UNIV [simp]: "starlike UNIV"
    4.15 +  by (simp add: starlike_def)
    4.16  
    4.17  lemma midpoint_refl: "midpoint x x = x"
    4.18    unfolding midpoint_def
    4.19 @@ -6540,6 +6543,9 @@
    4.20  lemma open_segment_idem [simp]: "open_segment a a = {}"
    4.21    by (simp add: open_segment_def)
    4.22  
    4.23 +lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
    4.24 +  using open_segment_def by auto
    4.25 +  
    4.26  lemma closed_segment_eq_real_ivl:
    4.27    fixes a b::real
    4.28    shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
    4.29 @@ -7903,6 +7909,28 @@
    4.30  
    4.31  lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
    4.32  
    4.33 +lemma starlike_convex_tweak_boundary_points:
    4.34 +  fixes S :: "'a::euclidean_space set"
    4.35 +  assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
    4.36 +  shows "starlike T"
    4.37 +proof -
    4.38 +  have "rel_interior S \<noteq> {}"
    4.39 +    by (simp add: assms rel_interior_eq_empty)
    4.40 +  then obtain a where a: "a \<in> rel_interior S"  by blast 
    4.41 +  with ST have "a \<in> T"  by blast 
    4.42 +  have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
    4.43 +    apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    4.44 +    using assms by blast
    4.45 +  show ?thesis
    4.46 +    unfolding starlike_def
    4.47 +    apply (rule bexI [OF _ \<open>a \<in> T\<close>])
    4.48 +    apply (simp add: closed_segment_eq_open)
    4.49 +    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
    4.50 +    apply (simp add: order_trans [OF * ST])
    4.51 +    done
    4.52 +qed
    4.53 +
    4.54 +subsection\<open>The relative frontier of a set\<close>
    4.55  
    4.56  definition "rel_frontier S = closure S - rel_interior S"
    4.57  
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 15 14:08:25 2016 +0000
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 16 13:57:06 2016 +0000
     5.3 @@ -11,79 +11,10 @@
     5.4    "~~/src/HOL/Library/Indicator_Function"
     5.5  begin
     5.6  
     5.7 -lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
     5.8 -  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
     5.9 -  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
    5.10 -  apply (auto simp add: abs_le_iff intro: cSup_least)
    5.11 -  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
    5.12 -
    5.13 -lemma cInf_abs_ge:
    5.14 -  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    5.15 -  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
    5.16 -  shows "\<bar>Inf S\<bar> \<le> a"
    5.17 -proof -
    5.18 -  have "Sup (uminus ` S) = - (Inf S)"
    5.19 -  proof (rule antisym)
    5.20 -    show "- (Inf S) \<le> Sup(uminus ` S)"
    5.21 -      apply (subst minus_le_iff)
    5.22 -      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
    5.23 -      apply (subst minus_le_iff)
    5.24 -      apply (rule cSup_upper, force)
    5.25 -      using bdd apply (force simp add: abs_le_iff bdd_above_def)
    5.26 -      done
    5.27 -  next
    5.28 -    show "Sup (uminus ` S) \<le> - Inf S"
    5.29 -      apply (rule cSup_least)
    5.30 -       using \<open>S \<noteq> {}\<close> apply (force simp add: )
    5.31 -      apply clarsimp  
    5.32 -      apply (rule cInf_lower)
    5.33 -      apply assumption
    5.34 -      using bdd apply (simp add: bdd_below_def)
    5.35 -      apply (rule_tac x="-a" in exI)
    5.36 -      apply force
    5.37 -      done
    5.38 -  qed
    5.39 -  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
    5.40 -qed
    5.41 -
    5.42 -lemma cSup_asclose:
    5.43 -  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
    5.44 -  assumes S: "S \<noteq> {}"
    5.45 -    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
    5.46 -  shows "\<bar>Sup S - l\<bar> \<le> e"
    5.47 -proof -
    5.48 -  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    5.49 -    by arith
    5.50 -  have "bdd_above S"
    5.51 -    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
    5.52 -  with S b show ?thesis
    5.53 -    unfolding th by (auto intro!: cSup_upper2 cSup_least)
    5.54 -qed
    5.55 -
    5.56 -lemma cInf_asclose:
    5.57 -  fixes S :: "real set"
    5.58 -  assumes S: "S \<noteq> {}"
    5.59 -    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
    5.60 -  shows "\<bar>Inf S - l\<bar> \<le> e"
    5.61 -proof -
    5.62 -  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
    5.63 -    by auto
    5.64 -  also have "\<dots> \<le> e"
    5.65 -    apply (rule cSup_asclose)
    5.66 -    using abs_minus_add_cancel b by (auto simp add: S)
    5.67 -  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
    5.68 -  then show ?thesis
    5.69 -    by (simp add: Inf_real_def)
    5.70 -qed
    5.71 -
    5.72  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    5.73    scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
    5.74    scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    5.75  
    5.76 -lemma real_arch_invD:
    5.77 -  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
    5.78 -  by (subst(asm) real_arch_inverse)
    5.79 -
    5.80  
    5.81  subsection \<open>Sundries\<close>
    5.82  
    5.83 @@ -4595,6 +4526,10 @@
    5.84  
    5.85  subsection \<open>Uniform limit of integrable functions is integrable.\<close>
    5.86  
    5.87 +lemma real_arch_invD:
    5.88 +  "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
    5.89 +  by (subst(asm) real_arch_inverse)
    5.90 +
    5.91  lemma integrable_uniform_limit:
    5.92    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
    5.93    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"
     6.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Mar 15 14:08:25 2016 +0000
     6.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Mar 16 13:57:06 2016 +0000
     6.3 @@ -3128,9 +3128,9 @@
     6.4    done
     6.5  
     6.6  proposition homotopic_compose_continuous_left:
     6.7 -   "homotopic_with (\<lambda>f. True) X Y f g \<and>
     6.8 -        continuous_on Y h \<and> image h Y \<subseteq> Z
     6.9 -        \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
    6.10 +   "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
    6.11 +     continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
    6.12 +    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h o f) (h o g)"
    6.13    using homotopic_with_compose_continuous_left by fastforce
    6.14  
    6.15  proposition homotopic_with_Pair:
    6.16 @@ -4053,4 +4053,267 @@
    6.17      by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
    6.18  qed
    6.19  
    6.20 +subsection\<open>Contractible sets\<close>
    6.21 +
    6.22 +definition contractible where
    6.23 + "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
    6.24 +
    6.25 +proposition contractible_imp_simply_connected:
    6.26 +  fixes S :: "_::real_normed_vector set"
    6.27 +  assumes "contractible S" shows "simply_connected S"
    6.28 +proof (cases "S = {}")
    6.29 +  case True then show ?thesis by force
    6.30 +next
    6.31 +  case False
    6.32 +  obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
    6.33 +    using assms by (force simp add: contractible_def)
    6.34 +  then have "a \<in> S"
    6.35 +    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
    6.36 +  show ?thesis
    6.37 +    apply (simp add: simply_connected_eq_contractible_loop_all False)
    6.38 +    apply (rule bexI [OF _ \<open>a \<in> S\<close>])
    6.39 +    using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def)
    6.40 +    apply clarify
    6.41 +    apply (rule_tac x="(h o (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
    6.42 +    apply (intro conjI continuous_on_compose continuous_intros)
    6.43 +    apply (erule continuous_on_subset | force)+
    6.44 +    done
    6.45 +qed
    6.46 +
    6.47 +corollary contractible_imp_connected:
    6.48 +  fixes S :: "_::real_normed_vector set"
    6.49 +  shows "contractible S \<Longrightarrow> connected S"
    6.50 +by (simp add: contractible_imp_simply_connected simply_connected_imp_connected)
    6.51 +
    6.52 +lemma contractible_imp_path_connected:
    6.53 +  fixes S :: "_::real_normed_vector set"
    6.54 +  shows "contractible S \<Longrightarrow> path_connected S"
    6.55 +by (simp add: contractible_imp_simply_connected simply_connected_imp_path_connected)
    6.56 +
    6.57 +lemma nullhomotopic_through_contractible:
    6.58 +  fixes S :: "_::topological_space set"
    6.59 +  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
    6.60 +      and g: "continuous_on T g" "g ` T \<subseteq> U"
    6.61 +      and T: "contractible T"
    6.62 +    obtains c where "homotopic_with (\<lambda>h. True) S U (g o f) (\<lambda>x. c)"
    6.63 +proof -
    6.64 +  obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
    6.65 +    using assms by (force simp add: contractible_def)
    6.66 +  have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
    6.67 +    by (rule homotopic_compose_continuous_left [OF b g])
    6.68 +  then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
    6.69 +    by (rule homotopic_compose_continuous_right [OF _ f])
    6.70 +  then show ?thesis
    6.71 +    by (simp add: comp_def that)
    6.72 +qed
    6.73 +
    6.74 +lemma nullhomotopic_into_contractible:
    6.75 +  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
    6.76 +      and T: "contractible T"
    6.77 +    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
    6.78 +apply (rule nullhomotopic_through_contractible [OF f, of id T])
    6.79 +using assms
    6.80 +apply (auto simp: continuous_on_id)
    6.81 +done
    6.82 +
    6.83 +lemma nullhomotopic_from_contractible:
    6.84 +  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
    6.85 +      and S: "contractible S"
    6.86 +    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
    6.87 +apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
    6.88 +using assms
    6.89 +apply (auto simp: comp_def)
    6.90 +done
    6.91 +
    6.92 +lemma homotopic_through_contractible:
    6.93 +  fixes S :: "_::real_normed_vector set"
    6.94 +  assumes "continuous_on S f1" "f1 ` S \<subseteq> T"
    6.95 +          "continuous_on T g1" "g1 ` T \<subseteq> U"
    6.96 +          "continuous_on S f2" "f2 ` S \<subseteq> T"
    6.97 +          "continuous_on T g2" "g2 ` T \<subseteq> U"
    6.98 +          "contractible T" "path_connected U"
    6.99 +   shows "homotopic_with (\<lambda>h. True) S U (g1 o f1) (g2 o f2)"
   6.100 +proof -
   6.101 +  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 o f1) (\<lambda>x. c1)"
   6.102 +    apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
   6.103 +    using assms apply (auto simp: )
   6.104 +    done
   6.105 +  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 o f2) (\<lambda>x. c2)"
   6.106 +    apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
   6.107 +    using assms apply (auto simp: )
   6.108 +    done
   6.109 +  have *: "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
   6.110 +  proof (cases "S = {}")
   6.111 +    case True then show ?thesis by force
   6.112 +  next
   6.113 +    case False
   6.114 +    with c1 c2 have "c1 \<in> U" "c2 \<in> U"
   6.115 +      using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
   6.116 +    with \<open>path_connected U\<close> show ?thesis by blast
   6.117 +  qed
   6.118 +  show ?thesis
   6.119 +    apply (rule homotopic_with_trans [OF c1])
   6.120 +    apply (rule homotopic_with_symD)
   6.121 +    apply (rule homotopic_with_trans [OF c2])
   6.122 +    apply (simp add: path_component homotopic_constant_maps *)
   6.123 +    done
   6.124 +qed
   6.125 +
   6.126 +lemma homotopic_into_contractible:
   6.127 +  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   6.128 +  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   6.129 +      and g: "continuous_on S g" "g ` S \<subseteq> T"
   6.130 +      and T: "contractible T"
   6.131 +    shows "homotopic_with (\<lambda>h. True) S T f g"
   6.132 +using homotopic_through_contractible [of S f T id T g id]
   6.133 +by (simp add: assms contractible_imp_path_connected continuous_on_id)
   6.134 +
   6.135 +lemma homotopic_from_contractible:
   6.136 +  fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   6.137 +  assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   6.138 +      and g: "continuous_on S g" "g ` S \<subseteq> T"
   6.139 +      and "contractible S" "path_connected T"
   6.140 +    shows "homotopic_with (\<lambda>h. True) S T f g"
   6.141 +using homotopic_through_contractible [of S id S f T id g]
   6.142 +by (simp add: assms contractible_imp_path_connected continuous_on_id)
   6.143 +
   6.144 +lemma starlike_imp_contractible_gen:
   6.145 +  fixes S :: "'a::real_normed_vector set"
   6.146 +  assumes S: "starlike S"
   6.147 +      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)"
   6.148 +    obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
   6.149 +proof -
   6.150 +  obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
   6.151 +    using S by (auto simp add: starlike_def)
   6.152 +  have "(\<lambda>y. (1 - fst y) *\<^sub>R snd y + fst y *\<^sub>R a) ` ({0..1} \<times> S) \<subseteq> S"
   6.153 +    apply clarify
   6.154 +    apply (erule a [unfolded closed_segment_def, THEN subsetD])
   6.155 +    apply (simp add: )
   6.156 +    apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
   6.157 +    done
   6.158 +  then show ?thesis
   6.159 +    apply (rule_tac a="a" in that)
   6.160 +    using \<open>a \<in> S\<close>
   6.161 +    apply (simp add: homotopic_with_def)
   6.162 +    apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
   6.163 +    apply (intro conjI ballI continuous_on_compose continuous_intros)
   6.164 +    apply (simp_all add: P)
   6.165 +    done
   6.166 +qed
   6.167 +
   6.168 +lemma starlike_imp_contractible:
   6.169 +  fixes S :: "'a::real_normed_vector set"
   6.170 +  shows "starlike S \<Longrightarrow> contractible S"
   6.171 +using starlike_imp_contractible_gen contractible_def by (fastforce simp: id_def)
   6.172 +
   6.173 +lemma contractible_UNIV: "contractible (UNIV :: 'a::real_normed_vector set)"
   6.174 +  by (simp add: starlike_imp_contractible)
   6.175 +
   6.176 +lemma starlike_imp_simply_connected:
   6.177 +  fixes S :: "'a::real_normed_vector set"
   6.178 +  shows "starlike S \<Longrightarrow> simply_connected S"
   6.179 +by (simp add: contractible_imp_simply_connected starlike_imp_contractible)
   6.180 +
   6.181 +lemma convex_imp_simply_connected:
   6.182 +  fixes S :: "'a::real_normed_vector set"
   6.183 +  shows "convex S \<Longrightarrow> simply_connected S"
   6.184 +using convex_imp_starlike starlike_imp_simply_connected by blast
   6.185 +
   6.186 +lemma starlike_imp_path_connected:
   6.187 +  fixes S :: "'a::real_normed_vector set"
   6.188 +  shows "starlike S \<Longrightarrow> path_connected S"
   6.189 +by (simp add: simply_connected_imp_path_connected starlike_imp_simply_connected)
   6.190 +
   6.191 +lemma starlike_imp_connected:
   6.192 +  fixes S :: "'a::real_normed_vector set"
   6.193 +  shows "starlike S \<Longrightarrow> connected S"
   6.194 +by (simp add: path_connected_imp_connected starlike_imp_path_connected)
   6.195 +
   6.196 +lemma is_interval_simply_connected_1:
   6.197 +  fixes S :: "real set"
   6.198 +  shows "is_interval S \<longleftrightarrow> simply_connected S"
   6.199 +using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
   6.200 +
   6.201 +lemma contractible_empty: "contractible {}"
   6.202 +  by (simp add: continuous_on_empty contractible_def homotopic_with)
   6.203 +
   6.204 +lemma contractible_convex_tweak_boundary_points:
   6.205 +  fixes S :: "'a::euclidean_space set"
   6.206 +  assumes "convex S" and TS: "rel_interior S \<subseteq> T" "T \<subseteq> closure S"
   6.207 +  shows "contractible T"
   6.208 +proof (cases "S = {}")
   6.209 +  case True
   6.210 +  with assms show ?thesis
   6.211 +    by (simp add: contractible_empty subsetCE)
   6.212 +next
   6.213 +  case False
   6.214 +  show ?thesis
   6.215 +    apply (rule starlike_imp_contractible)
   6.216 +    apply (rule starlike_convex_tweak_boundary_points [OF \<open>convex S\<close> False TS])
   6.217 +    done
   6.218 +qed
   6.219 +
   6.220 +lemma convex_imp_contractible:
   6.221 +  fixes S :: "'a::real_normed_vector set"
   6.222 +  shows "convex S \<Longrightarrow> contractible S"
   6.223 +using contractible_empty convex_imp_starlike starlike_imp_contractible by auto
   6.224 +
   6.225 +lemma contractible_sing:
   6.226 +  fixes a :: "'a::real_normed_vector"
   6.227 +  shows "contractible {a}"
   6.228 +by (rule convex_imp_contractible [OF convex_singleton])
   6.229 +
   6.230 +lemma is_interval_contractible_1:
   6.231 +  fixes S :: "real set"
   6.232 +  shows  "is_interval S \<longleftrightarrow> contractible S"
   6.233 +using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1 
   6.234 +      is_interval_simply_connected_1 by auto
   6.235 +
   6.236 +lemma contractible_times:
   6.237 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.238 +  assumes S: "contractible S" and T: "contractible T"
   6.239 +  shows "contractible (S \<times> T)"
   6.240 +proof -
   6.241 +  obtain a h where conth: "continuous_on ({0..1} \<times> S) h" 
   6.242 +             and hsub: "h ` ({0..1} \<times> S) \<subseteq> S"
   6.243 +             and [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (0, x) = x" 
   6.244 +             and [simp]: "\<And>x. x \<in> S \<Longrightarrow>  h (1::real, x) = a"
   6.245 +    using S by (auto simp add: contractible_def homotopic_with)
   6.246 +  obtain b k where contk: "continuous_on ({0..1} \<times> T) k" 
   6.247 +             and ksub: "k ` ({0..1} \<times> T) \<subseteq> T"
   6.248 +             and [simp]: "\<And>x. x \<in> T \<Longrightarrow> k (0, x) = x" 
   6.249 +             and [simp]: "\<And>x. x \<in> T \<Longrightarrow>  k (1::real, x) = b"
   6.250 +    using T by (auto simp add: contractible_def homotopic_with)
   6.251 +  show ?thesis
   6.252 +    apply (simp add: contractible_def homotopic_with)
   6.253 +    apply (rule exI [where x=a])
   6.254 +    apply (rule exI [where x=b])
   6.255 +    apply (rule exI [where x = "\<lambda>z. (h (fst z, fst(snd z)), k (fst z, snd(snd z)))"])
   6.256 +    apply (intro conjI ballI continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF contk])
   6.257 +    using hsub ksub 
   6.258 +    apply (auto simp: )
   6.259 +    done
   6.260 +qed
   6.261 +
   6.262 +lemma homotopy_dominated_contractibility: 
   6.263 +  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   6.264 +  assumes S: "contractible S"
   6.265 +      and f: "continuous_on S f" "image f S \<subseteq> T" 
   6.266 +      and g: "continuous_on T g" "image g T \<subseteq> S" 
   6.267 +      and hom: "homotopic_with (\<lambda>x. True) T T (f o g) id"
   6.268 +    shows "contractible T"
   6.269 +proof -
   6.270 +  obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
   6.271 +    using nullhomotopic_from_contractible [OF f S] .
   6.272 +  then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
   6.273 +    by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
   6.274 +  show ?thesis
   6.275 +    apply (simp add: contractible_def)
   6.276 +    apply (rule exI [where x = b])
   6.277 +    apply (rule homotopic_with_symD)
   6.278 +    apply (rule homotopic_with_trans [OF _ hom])
   6.279 +    using homg apply (simp add: o_def)
   6.280 +    done
   6.281 +qed
   6.282 +
   6.283  end
     7.1 --- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Tue Mar 15 14:08:25 2016 +0000
     7.2 +++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Wed Mar 16 13:57:06 2016 +0000
     7.3 @@ -169,9 +169,13 @@
     7.4      qed
     7.5  qed
     7.6  
     7.7 -lemma norm_lemma_xy: "\<lbrakk>\<bar>b\<bar> + 1 \<le> norm(y) - a; norm(x) \<le> a\<rbrakk> \<Longrightarrow> b \<le> norm(x + y)"
     7.8 -  by (metis abs_add_one_not_less_self add.commute diff_le_eq dual_order.trans le_less_linear
     7.9 -         norm_diff_ineq)
    7.10 +lemma norm_lemma_xy: assumes "\<bar>b\<bar> + 1 \<le> norm(y) - a" "norm(x) \<le> a" shows "b \<le> norm(x + y)"
    7.11 +proof -
    7.12 +  have "b \<le> norm y - norm x"
    7.13 +    using assms by linarith
    7.14 +  then show ?thesis
    7.15 +    by (metis (no_types) add.commute norm_diff_ineq order_trans)
    7.16 +qed
    7.17  
    7.18  lemma polyfun_extremal:
    7.19    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
     8.1 --- a/src/HOL/Real.thy	Tue Mar 15 14:08:25 2016 +0000
     8.2 +++ b/src/HOL/Real.thy	Wed Mar 16 13:57:06 2016 +0000
     8.3 @@ -1404,21 +1404,6 @@
     8.4  lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
     8.5    by simp
     8.6  
     8.7 -subsection\<open>Absolute Value Function for the Reals\<close>
     8.8 -
     8.9 -lemma abs_minus_add_cancel: "\<bar>x + (- y)\<bar> = \<bar>y + (- (x::real))\<bar>"
    8.10 -  by (simp add: abs_if)
    8.11 -
    8.12 -lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>"
    8.13 -  by (simp add: abs_if)
    8.14 -
    8.15 -lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x"
    8.16 -  by simp
    8.17 -
    8.18 -lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (-l + -m)\<bar> \<le> \<bar>x + -l\<bar> + \<bar>y + -m\<bar>"
    8.19 -  by simp
    8.20 -
    8.21 -
    8.22  subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
    8.23  
    8.24  (* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)
    8.25 @@ -1564,7 +1549,7 @@
    8.26  proof -
    8.27    have "x ^ n = of_int (\<lfloor>x\<rfloor> ^ n)"
    8.28      using assms by (induct n arbitrary: x) simp_all
    8.29 -  then show ?thesis by (metis floor_of_int) 
    8.30 +  then show ?thesis by (metis floor_of_int)
    8.31  qed
    8.32  
    8.33  lemma floor_numeral_power[simp]:
     9.1 --- a/src/HOL/Rings.thy	Tue Mar 15 14:08:25 2016 +0000
     9.2 +++ b/src/HOL/Rings.thy	Wed Mar 16 13:57:06 2016 +0000
     9.3 @@ -2088,6 +2088,9 @@
     9.4     "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
     9.5    by (auto simp add: diff_le_eq ac_simps abs_le_iff)
     9.6  
     9.7 +lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>"
     9.8 +  by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans)
     9.9 +
    9.10  end
    9.11  
    9.12  subsection \<open>Dioids\<close>