# HG changeset patch
# User immler
# Date 1460452709 -7200
# Node ID c355b3223cbdda9d7cabad782139228b00db598f
# Parent  f36a54da47a4d544ac3ed7e449e9c3f599186500
generalized

diff -r f36a54da47a4 -r c355b3223cbd src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 12 11:18:29 2016 +0200
@@ -6623,17 +6623,27 @@
     done
 qed
 
+lemma compact_segment [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "compact (closed_segment a b)"
+  by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)
+
+lemma closed_segment [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "closed (closed_segment a b)"
+  by (simp add: compact_imp_closed)
+
+lemma closure_closed_segment [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "closure(closed_segment a b) = closed_segment a b"
+  by simp
+
 lemma open_segment_bound:
   assumes "x \<in> open_segment a b"
   shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
 apply (simp add: assms open_segment_bound1)
 by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
 
-lemma closure_closed_segment [simp]:
-    fixes a :: "'a::euclidean_space"
-    shows "closure(closed_segment a b) = closed_segment a b"
-  by (simp add: closure_eq compact_imp_closed segment_convex_hull compact_convex_hull)
-
 lemma closure_open_segment [simp]:
     fixes a :: "'a::euclidean_space"
     shows "closure(open_segment a b) = (if a = b then {} else closed_segment a b)"
@@ -6647,18 +6657,10 @@
          closure_translation image_comp [symmetric] del: closure_greaterThanLessThan)
 qed
 
-lemma closed_segment [simp]:
-    fixes a :: "'a::euclidean_space"  shows "closed (closed_segment a b)"
-  using closure_subset_eq by fastforce
-
 lemma closed_open_segment_iff [simp]:
     fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) \<longleftrightarrow> a = b"
   by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
 
-lemma compact_segment [simp]:
-    fixes a :: "'a::euclidean_space"  shows "compact (closed_segment a b)"
-  by (simp add: compact_convex_hull segment_convex_hull)
-
 lemma compact_open_segment_iff [simp]:
     fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) \<longleftrightarrow> a = b"
   by (simp add: bounded_open_segment compact_eq_bounded_closed)