Theory Derivative no longer depends on Path_Connected
authorpaulson <lp15@cam.ac.uk>
Wed, 04 Sep 2019 14:16:27 +0100
changeset 70831 0e2a065d6f31
parent 70830 5f4b8a505090
child 70832 de9c4ed2d5df
Theory Derivative no longer depends on Path_Connected
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Wed Sep 04 14:16:27 2019 +0100
@@ -7,7 +7,7 @@
 
 theory Derivative
   imports
-    Path_Connected
+    Starlike
     Operator_Norm
     Uniform_Limit
     Bounded_Linear_Function
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Sep 04 14:16:27 2019 +0100
@@ -2,7 +2,7 @@
 
 theory Ordered_Euclidean_Space
 imports
-  Cartesian_Euclidean_Space
+  Cartesian_Euclidean_Space Path_Connected
   "HOL-Library.Product_Order"
 begin
 
--- a/src/HOL/Analysis/Polytope.thy	Mon Sep 02 19:44:12 2019 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Wed Sep 04 14:16:27 2019 +0100
@@ -3,7 +3,7 @@
 text\<open>Ported from HOL Light by L C Paulson\<close>
 
 theory Polytope
-imports Cartesian_Euclidean_Space
+imports Cartesian_Euclidean_Space Path_Connected
 begin
 
 subsection \<open>Faces of a (usually convex) set\<close>
@@ -22,9 +22,7 @@
 proof -
   have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
     apply (simp add: face_of_def Ball_def, clarify)
-    apply (drule open_segment_translation_eq [THEN iffD1])
-    using inj_image_mem_iff inj_add_left apply metis
-    done
+    by (meson imageI open_segment_translation_eq)
   show ?thesis
     apply (rule iffI)
     apply (force simp: image_comp o_def dest: * [where a = "-a"])