author paulson Wed Mar 16 13:57:06 2016 +0000 (2016-03-16) changeset 62626 de25474ce728 parent 62623 dbc62f86a1a9 child 62627 20288ba55e85
Contractible sets. Also removal of obsolete theorems and refactoring
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.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.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.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.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.11  definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
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.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.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.31  lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
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.56  definition "rel_frontier S = closure S - rel_interior S"
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.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.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.81  subsection \<open>Sundries\<close>
5.83 @@ -4595,6 +4526,10 @@
5.85  subsection \<open>Uniform limit of integrable functions is integrable.\<close>
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.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.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.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.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.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.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.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.173 +lemma contractible_UNIV: "contractible (UNIV :: 'a::real_normed_vector set)"
6.174 +  by (simp add: starlike_imp_contractible)
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.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.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.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.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.201 +lemma contractible_empty: "contractible {}"
6.202 +  by (simp add: continuous_on_empty contractible_def homotopic_with)
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.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.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.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.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.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.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.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.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.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.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.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.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.12  subsection \<open>Dioids\<close>