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
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"
--- 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>