# HG changeset patch
# User nipkow
# Date 1574969887 -3600
# Node ID a25b6f79043f29a93f050e76f99dde01881ea995
# Parent  df1d96114754df10f6169983e9852b6b412923c0# Parent  57bc95d2349106659892a04a617bfe6a445069e1
merged

diff -r 57bc95d23491 -r a25b6f79043f src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy	Thu Nov 28 18:40:39 2019 +0100
+++ b/src/HOL/Analysis/Line_Segment.thy	Thu Nov 28 20:38:07 2019 +0100
@@ -14,7 +14,7 @@
   Topology_Euclidean_Space
 begin
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets and Functions\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological Properties of Convex Sets, Metric Spaces and Functions\<close>
 
 lemma convex_supp_sum:
   assumes "convex S" and 1: "supp_sum u I = 1"
@@ -23,13 +23,11 @@
 proof -
   have fin: "finite {i \<in> I. u i \<noteq> 0}"
     using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
-  then have eq: "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+  then have "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
     by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
-  show ?thesis
-    apply (simp add: eq)
-    apply (rule convex_sum [OF fin \<open>convex S\<close>])
-    using 1 assms apply (auto simp: supp_sum_def support_on_def)
-    done
+  also have "... \<in> S"
+    using 1 assms by (force simp: supp_sum_def support_on_def intro: convex_sum [OF fin \<open>convex S\<close>])
+  finally show ?thesis .
 qed
 
 lemma closure_bounded_linear_image_subset:
@@ -135,7 +133,7 @@
 proposition clopen:
   fixes S :: "'a :: real_normed_vector set"
   shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
-    by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
+  by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
 
 corollary compact_open:
   fixes S :: "'a :: euclidean_space set"
@@ -143,8 +141,8 @@
   by (auto simp: compact_eq_bounded_closed clopen)
 
 corollary finite_imp_not_open:
-    fixes S :: "'a::{real_normed_vector, perfect_space} set"
-    shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
+  fixes S :: "'a::{real_normed_vector, perfect_space} set"
+  shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
   using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
 
 corollary empty_interior_finite:
@@ -246,11 +244,7 @@
   from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
     unfolding bounded_iff by auto
   show ?thesis
-    apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
-    unfolding subset_hull[of convex, OF convex_cball]
-    unfolding subset_eq mem_cball dist_norm using B
-    apply auto
-    done
+    by (simp add: bounded_subset[OF bounded_cball, of _ 0 B] B subsetI subset_hull)
 qed
 
 lemma finite_imp_bounded_convex_hull:
@@ -260,8 +254,6 @@
   by auto
 
 
-section \<open>Line Segments\<close>
-
 subsection \<open>Midpoint\<close>
 
 definition\<^marker>\<open>tag important\<close> midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -338,7 +330,7 @@
 by (simp add: linear_iff midpoint_def)
 
 
-subsection \<open>Line segments\<close>
+subsection \<open>Open and closed segments\<close>
 
 definition\<^marker>\<open>tag important\<close> closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
@@ -528,8 +520,7 @@
 lemma segment_bound:
   assumes "x \<in> closed_segment a b"
   shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
-apply (simp add: assms segment_bound1)
-by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)
+by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)+
 
 lemma open_segment_commute: "open_segment a b = open_segment b a"
 proof -
@@ -564,8 +555,11 @@
     by (auto intro!: mult_left_mono u assms)
   then show "x \<in> {a .. b}"
     unfolding x_def by (auto simp: algebra_simps)
-qed (auto simp: closed_segment_def divide_simps algebra_simps
-    intro!: exI[where x="(x - a) / (b - a)" for x])
+next
+  show "\<And>x. x \<in> {a..b} \<Longrightarrow> x \<in> closed_segment a b"
+    by (force simp: closed_segment_def divide_simps algebra_simps
+              intro: exI[where x="(x - a) / (b - a)" for x])
+qed 
 
 lemma closed_segment_eq_real_ivl:
   fixes a b::real