src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

   "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
   by(auto simp add:vector_component_simps all_1 Cart_eq)
 
 lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
 
-lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
+lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
 
 lemma setsum_delta_notmem: assumes "x\<notin>s"
   shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
         "setsum (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
         "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"

 lemma mem_interval_1: fixes x :: "real^1" shows
  "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
 by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1)
 
-lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =
+lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
   (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   using image_affinity_interval[of m 0 a b] by auto
 
 lemma dest_vec1_inverval:
   "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"

 proof- have *:"x - y + (y - z) = x - z" by auto
   show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded smult_conv_scaleR *]
     by(auto simp add:norm_minus_commute) qed
 
 lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto 
-lemma norm_minus_eqI:"(x::real^'n::finite) = - y \<Longrightarrow> norm x = norm y" by auto
+lemma norm_minus_eqI:"(x::real^'n) = - y \<Longrightarrow> norm x = norm y" by auto
 
 lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
   unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
 
 lemma dimindex_ge_1:"CARD(_::finite) \<ge> 1"

   by(auto simp add: real_convex_bound_lt inner_add)
 
 lemma convex_halfspace_gt: "convex {x. inner a x > b}"
    using convex_halfspace_lt[of "-a" "-b"] by auto
 
-lemma convex_positive_orthant: "convex {x::real^'n::finite. (\<forall>i. 0 \<le> x$i)}"
+lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
   unfolding convex_def apply auto apply(erule_tac x=i in allE)+
   apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)
 
 subsection {* Explicit expressions for convexity in terms of arbitrary sums. *}
 

       apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
       apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
   thus ?thesis unfolding convex_def cone_def by auto
 qed
 
-lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
+lemma affine_dependent_biggerset: fixes s::"(real^'n) set"
   assumes "finite s" "card s \<ge> CARD('n) + 2"
   shows "affine_dependent s"
 proof-
   have "s\<noteq>{}" using assms by auto then obtain a where "a\<in>s" by auto
   have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto

   finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
     apply(rule dependent_imp_affine_dependent)
     apply(rule dependent_biggerset) by auto qed
 
 lemma affine_dependent_biggerset_general:
-  assumes "finite (s::(real^'n::finite) set)" "card s \<ge> dim s + 2"
+  assumes "finite (s::(real^'n) set)" "card s \<ge> dim s + 2"
   shows "affine_dependent s"
 proof-
   from assms(2) have "s \<noteq> {}" by auto
   then obtain a where "a\<in>s" by auto
   have *:"{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})" by auto

   finally show ?thesis apply(subst insert_Diff[OF `a\<in>s`, THEN sym])
     apply(rule dependent_imp_affine_dependent) apply(rule dependent_biggerset_general) unfolding ** by auto qed
 
 subsection {* Caratheodory's theorem. *}
 
-lemma convex_hull_caratheodory: fixes p::"(real^'n::finite) set"
+lemma convex_hull_caratheodory: fixes p::"(real^'n) set"
   shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1 \<and>
   (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
 proof(rule,rule)
   fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"

   thus "\<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1
     \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y" using obt by auto
 qed auto
 
 lemma caratheodory:
- "convex hull p = {x::real^'n::finite. \<exists>s. finite s \<and> s \<subseteq> p \<and>
+ "convex hull p = {x::real^'n. \<exists>s. finite s \<and> s \<subseteq> p \<and>
       card s \<le> CARD('n) + 1 \<and> x \<in> convex hull s}"
   unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
   fix x assume "x \<in> convex hull p"
   then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> CARD('n) + 1"
      "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto

     apply (rule compact_continuous_image)
     apply (intro compact_Times compact_real_interval assms)
     done
 qed
 
-lemma compact_convex_hull: fixes s::"(real^'n::finite) set"
+lemma compact_convex_hull: fixes s::"(real^'n) set"
   assumes "compact s"  shows "compact(convex hull s)"
 proof(cases "s={}")
   case True thus ?thesis using compact_empty by simp
 next
   case False then obtain w where "w\<in>s" by auto

   using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
 
 subsection {* Closest point of a convex set is unique, with a continuous projection. *}
 
 definition
-  closest_point :: "(real ^ 'n::finite) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
+  closest_point :: "(real ^ 'n) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
  "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
   assumes "closed s" "s \<noteq> {}"
   shows  "closest_point s a \<in> s" "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"

 
 (* TODO: move *)
 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
   unfolding norm_eq_sqrt_inner by simp
 
-lemma closer_points_lemma: fixes y::"real^'n::finite"
+lemma closer_points_lemma: fixes y::"real^'n"
   assumes "inner y z > 0"
   shows "\<exists>u>0. \<forall>v>0. v \<le> u \<longrightarrow> norm(v *\<^sub>R z - y) < norm y"
 proof- have z:"inner z z > 0" unfolding inner_gt_zero_iff using assms by auto
   thus ?thesis using assms apply(rule_tac x="inner y z / inner z z" in exI) apply(rule) defer proof(rule+)
     fix v assume "0<v" "v \<le> inner y z / inner z z"
     thus "norm (v *\<^sub>R z - y) < norm y" unfolding norm_lt using z and assms
       by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ `0<v`])
   qed(rule divide_pos_pos, auto) qed
 
 lemma closer_point_lemma:
-  fixes x y z :: "real ^ 'n::finite"
+  fixes x y z :: "real ^ 'n"
   assumes "inner (y - x) (z - x) > 0"
   shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *\<^sub>R (z - x)) y < dist x y"
 proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)"
     using closer_points_lemma[OF assms] by auto
   show ?thesis apply(rule_tac x="min u 1" in exI) using u[THEN spec[where x="min u 1"]] and `u>0`

       unfolding power2_norm_eq_inner and not_less by (auto simp add: field_simps inner_commute inner_diff)
   qed(insert `y\<in>s` `z\<notin>s`, auto)
 qed
 
 lemma separating_hyperplane_closed_0:
-  assumes "convex (s::(real^'n::finite) set)" "closed s" "0 \<notin> s"
+  assumes "convex (s::(real^'n) set)" "closed s" "0 \<notin> s"
   shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. inner a x > b)"
   proof(cases "s={}") guess a using UNIV_witness[where 'a='n] ..
-  case True have "norm ((basis a)::real^'n::finite) = 1" 
+  case True have "norm ((basis a)::real^'n) = 1" 
     using norm_basis and dimindex_ge_1 by auto
   thus ?thesis apply(rule_tac x="basis a" in exI, rule_tac x=1 in exI) using True by auto
 next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
     apply - apply(erule exE)+ unfolding dot_rzero apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
 
 subsection {* Now set-to-set for closed/compact sets. *}
 
 lemma separating_hyperplane_closed_compact:
-  assumes "convex (s::(real^'n::finite) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
+  assumes "convex (s::(real^'n) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
   shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
 proof(cases "s={}")
   case True
   obtain b where b:"b>0" "\<forall>x\<in>t. norm x \<le> b" using compact_imp_bounded[OF assms(4)] unfolding bounded_pos by auto
   obtain z::"real^'n" where z:"norm z = b + 1" using vector_choose_size[of "b + 1"] and b(1) by auto

   thus ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-b" in exI) by auto qed
 
 subsection {* General case without assuming closure and getting non-strict separation. *}
 
 lemma separating_hyperplane_set_0:
-  assumes "convex s" "(0::real^'n::finite) \<notin> s"
+  assumes "convex s" "(0::real^'n) \<notin> s"
   shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
 proof- let ?k = "\<lambda>c. {x::real^'n. 0 \<le> inner c x}"
   have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
     apply(rule compact_imp_fip) apply(rule compact_frontier[OF compact_cball])
     defer apply(rule,rule,erule conjE) proof-

   qed(insert closed_halfspace_ge, auto)
   then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
   thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: inner_commute) qed
 
 lemma separating_hyperplane_sets:
-  assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
+  assumes "convex s" "convex (t::(real^'n) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
   shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
 proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
   obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" 
     using assms(3-5) by auto 
   hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"

   from radon_partition[OF *] guess m .. then guess p ..
   thus ?thesis apply(rule_tac that[of p m]) using s by auto qed
 
 subsection {* Helly's theorem. *}
 
-lemma helly_induct: fixes f::"(real^'n::finite) set set"
+lemma helly_induct: fixes f::"(real^'n) set set"
   assumes "card f = n" "n \<ge> CARD('n) + 1"
   "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   shows "\<Inter> f \<noteq> {}"
 using assms proof(induct n arbitrary: f)
 case (Suc n)

       thus "x\<in>\<Inter>g" using X[THEN bspec[where x=y]] using * f by auto
     qed(auto)
     thus ?thesis unfolding f using mp(3)[unfolded gh] by blast qed
 qed(insert dimindex_ge_1, auto) qed(auto)
 
-lemma helly: fixes f::"(real^'n::finite) set set"
+lemma helly: fixes f::"(real^'n) set set"
   assumes "card f \<ge> CARD('n) + 1" "\<forall>s\<in>f. convex s"
           "\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   shows "\<Inter> f \<noteq>{}"
   apply(rule helly_induct) using assms by auto
 

   qed(insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3))
   thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
     apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
 
 lemma starlike_compact_projective:
-  assumes "compact s" "cball (0::real^'n::finite) 1 \<subseteq> s "
+  assumes "compact s" "cball (0::real^'n) 1 \<subseteq> s "
   "\<forall>x\<in>s. \<forall>u. 0 \<le> u \<and> u < 1 \<longrightarrow> (u *\<^sub>R x) \<in> (s - frontier s )"
-  shows "s homeomorphic (cball (0::real^'n::finite) 1)"
+  shows "s homeomorphic (cball (0::real^'n) 1)"
 proof-
   have fs:"frontier s \<subseteq> s" apply(rule frontier_subset_closed) using compact_imp_closed[OF assms(1)] by simp
   def pi \<equiv> "\<lambda>x::real^'n. inverse (norm x) *\<^sub>R x"
   have "0 \<notin> frontier s" unfolding frontier_straddle apply(rule ccontr) unfolding not_not apply(erule_tac x=1 in allE)
     using assms(2)[unfolded subset_eq Ball_def mem_cball] by auto

         ultimately have *:"pi x = pi y" using surf(4)[THEN bspec[where x="pi x"]] surf(4)[THEN bspec[where x="pi y"]] by auto 
         moreover have "norm x = norm y" using as(3)[unfolded *] using False by(auto dest:surf_0)
         ultimately show ?thesis using injpi by auto qed qed
   qed auto qed
 
-lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n::finite) set"
+lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n) set"
   assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
   shows "s homeomorphic (cball (0::real^'n) 1)"
   apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
   fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
   hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq

       unfolding class_semiring.mul_a using `u<1` by auto
     thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
       using as unfolding scaleR_scaleR by auto qed auto
   thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
 
-lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n::finite) set"
+lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n) set"
   assumes "convex s" "compact s" "interior s \<noteq> {}" "0 < e"
-  shows "s homeomorphic (cball (b::real^'n::finite) e)"
+  shows "s homeomorphic (cball (b::real^'n) e)"
 proof- obtain a where "a\<in>interior s" using assms(3) by auto
   then obtain d where "d>0" and d:"cball a d \<subseteq> s" unfolding mem_interior_cball by auto
   let ?d = "inverse d" and ?n = "0::real^'n"
   have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
     apply(rule, rule_tac x="d *\<^sub>R x + a" in image_eqI) defer

     using assms(1,2) by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
   thus ?thesis apply(rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
     apply(rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
     using `d>0` `e>0` by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib) qed
 
-lemma homeomorphic_convex_compact: fixes s::"(real^'n::finite) set" and t::"(real^'n) set"
+lemma homeomorphic_convex_compact: fixes s::"(real^'n) set" and t::"(real^'n) set"
   assumes "convex s" "compact s" "interior s \<noteq> {}"
           "convex t" "compact t" "interior t \<noteq> {}"
   shows "s homeomorphic t"
   using assms by(meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
 
 subsection {* Epigraphs of convex functions. *}
 
-definition "epigraph s (f::real^'n::finite \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
+definition "epigraph s (f::real^'n \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
 
 lemma mem_epigraph: "(pastecart x (vec1 y)) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
 
 lemma convex_epigraph: 
   "convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"

 lemma is_interval_connected:
   fixes s :: "(real ^ _) set"
   shows "is_interval s \<Longrightarrow> connected s"
   using is_interval_convex convex_connected by auto
 
-lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
+lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n}"
   apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
 subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
 
 lemma is_interval_1:

   "connected s \<longleftrightarrow> convex (s::(real^1) set)" 
   using is_interval_convex convex_connected is_interval_connected_1 by auto
 
 subsection {* Another intermediate value theorem formulation. *}
 
-lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
   assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
 proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI) 
     using assms(1) by(auto simp add: vector_le_def dest_vec1_def)
   thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
     using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
     using assms by(auto intro!: imageI) qed
 
-lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
   assumes "dest_vec1 a \<le> dest_vec1 b"
   "\<forall>x\<in>{a .. b}. continuous (at x) f" "f a$k \<le> y" "y \<le> f b$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
   apply(rule ivt_increasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto
 
-lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
   assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
   apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
   apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
   by(auto simp add:vector_uminus_component)
 
-lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
   assumes "dest_vec1 a \<le> dest_vec1 b" "\<forall>x\<in>{a .. b}. continuous (at x) f" "f b$k \<le> y" "y \<le> f a$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
   apply(rule ivt_decreasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto
 
 subsection {* A bound within a convex hull, and so an interval. *}

     using assms(2) obt(1) by auto
   thus "f x \<le> b" using assms(1)[unfolded convex_on[OF convex_convex_hull], rule_format, of k u v]
     unfolding obt(2-3) using obt(1) and hull_subset[unfolded subset_eq, rule_format, of _ s] by auto qed
 
 lemma unit_interval_convex_hull:
-  "{0::real^'n::finite .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
+  "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
 proof- have 01:"{0,1} \<subseteq> convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto
   { fix n x assume "x\<in>{0::real^'n .. 1}" "n \<le> CARD('n)" "card {i. x$i \<noteq> 0} \<le> n" 
   hence "x\<in>convex hull ?points" proof(induct n arbitrary: x)
     case 0 hence "x = 0" apply(subst Cart_eq) apply rule by auto
     thus "x\<in>convex hull ?points" using 01 by auto

         { fix j have "x$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $ j - x $ i) / (1 - x $ i)" "(x $ j - x $ i) / (1 - x $ i) \<le> 1"
             apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
             using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta) 
           hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
         moreover have "i\<in>{j. x$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" using i01 by(auto simp add: Cart_lambda_beta)
-        hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n::finite) $ j \<noteq> 0}" by auto
-        hence **:"{j. ((\<chi> j. ?y j)::real^'n::finite) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta)  
+        hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" by auto
+        hence **:"{j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta)  
         have "card {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<le> n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
         ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
           apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1))
           unfolding mem_interval using i01 Suc(3) by (auto simp add: Cart_lambda_beta)
       qed qed qed } note * = this

     unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
     by(auto simp add: vector_le_def mem_def[of _ convex]) qed
 
 subsection {* And this is a finite set of vertices. *}
 
-lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n::finite} = convex hull s"
-  apply(rule that[of "{x::real^'n::finite. \<forall>i. x$i=0 \<or> x$i=1}"])
-  apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n::finite) ` UNIV"])
+lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n} = convex hull s"
+  apply(rule that[of "{x::real^'n. \<forall>i. x$i=0 \<or> x$i=1}"])
+  apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n) ` UNIV"])
   prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof-
   fix x::"real^'n" assume as:"\<forall>i. x $ i = 0 \<or> x $ i = 1"
   show "x \<in> (\<lambda>s. \<chi> i. if i \<in> s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x$i = 1}"])
     unfolding Cart_eq using as by(auto simp add:Cart_lambda_beta) qed auto
 
 subsection {* Hence any cube (could do any nonempty interval). *}
 
 lemma cube_convex_hull:
-  assumes "0 < d" obtains s::"(real^'n::finite) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof-
+  assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof-
   let ?d = "(\<chi> i. d)::real^'n"
   have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. 1}" apply(rule set_ext, rule)
     unfolding image_iff defer apply(erule bexE) proof-
     fix y assume as:"y\<in>{x - ?d .. x + ?d}"
     { fix i::'n have "x $ i \<le> d + y $ i" "y $ i \<le> d + x $ i" using as[unfolded mem_interval, THEN spec[where x=i]]

   thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
 
 subsection {* Hence a convex function on an open set is continuous. *}
 
 lemma convex_on_continuous:
-  assumes "open (s::(real^'n::finite) set)" "convex_on s f" 
+  assumes "open (s::(real^'n) set)" "convex_on s f" 
   shows "continuous_on s f"
   unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
   note dimge1 = dimindex_ge_1[where 'a='n]
   fix x assume "x\<in>s"
   then obtain e where e:"cball x e \<subseteq> s" "e>0" using assms(1) unfolding open_contains_cball by auto

 
 (* Use the same overloading tricks as for intervals, so that 
    segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
 
 definition
-  midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
+  midpoint :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
   "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
 definition
-  open_segment :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+  open_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
   "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real.  0 < u \<and> u < 1}"
 
 definition
-  closed_segment :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+  closed_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
   "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
 definition "between = (\<lambda> (a,b). closed_segment a b)"
 
 lemmas segment = open_segment_def closed_segment_def

   "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
   "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
   "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
   "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
 proof-
-  have *: "\<And>x y::real^'n::finite. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
-  have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2" by auto
+  have *: "\<And>x y::real^'n. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
+  have **:"\<And>x y::real^'n. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2" by auto
   note scaleR_right_distrib [simp]
   show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
   show ?t2 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
   show ?t3 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
   show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed
 
 lemma midpoint_eq_endpoint:
-  "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
+  "midpoint a b = a \<longleftrightarrow> a = (b::real^'n)"
   "midpoint a b = b \<longleftrightarrow> a = b"
   unfolding dist_eq_0_iff[where 'a="real^'n", THEN sym] dist_midpoint by auto
 
 lemma convex_contains_segment:
   "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"

 lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
 
 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   unfolding between_def mem_def by auto
 
-lemma between:"between (a,b) (x::real^'n::finite) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
+lemma between:"between (a,b) (x::real^'n) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
 proof(cases "a = b")
   case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
     by(auto simp add:segment_refl dist_commute) next
   case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto 
   have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)

             unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
             by(auto simp add:field_simps vector_component_simps)
           finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i" by auto
         qed(insert Fal2, auto) qed qed
 
-lemma between_midpoint: fixes a::"real^'n::finite" shows
+lemma between_midpoint: fixes a::"real^'n" shows
   "between (a,b) (midpoint a b)" (is ?t1) 
   "between (b,a) (midpoint a b)" (is ?t2)
 proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
   show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
     by(auto simp add:field_simps Cart_eq vector_component_simps) qed

   apply(rule_tac x=u in exI) defer apply(rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2)
   unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto
 
 lemma std_simplex:
   "convex hull (insert 0 { basis i | i. i\<in>UNIV}) =
-        {x::real^'n::finite . (\<forall>i. 0 \<le> x$i) \<and> setsum (\<lambda>i. x$i) UNIV \<le> 1 }" (is "convex hull (insert 0 ?p) = ?s")
+        {x::real^'n . (\<forall>i. 0 \<le> x$i) \<and> setsum (\<lambda>i. x$i) UNIV \<le> 1 }" (is "convex hull (insert 0 ?p) = ?s")
 proof- let ?D = "UNIV::'n set"
   have "0\<notin>?p" by(auto simp add: basis_nonzero)
   have "{(basis i)::real^'n |i. i \<in> ?D} = basis ` ?D" by auto
   note sumbas = this  setsum_reindex[OF basis_inj, unfolded o_def]
   show ?thesis unfolding simplex[OF finite_stdbasis `0\<notin>?p`] apply(rule set_ext) unfolding mem_Collect_eq apply rule

       apply(rule_tac x="\<lambda>y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE) using as(1) apply(erule_tac x=i in allE) 
       unfolding sumbas using as(2) and basis_expansion_unique [where 'a=real, unfolded smult_conv_scaleR] by(auto simp add:inner_basis) qed qed 
 
 lemma interior_std_simplex:
   "interior (convex hull (insert 0 { basis i| i. i\<in>UNIV})) =
-  {x::real^'n::finite. (\<forall>i. 0 < x$i) \<and> setsum (\<lambda>i. x$i) UNIV < 1 }"
+  {x::real^'n. (\<forall>i. 0 < x$i) \<and> setsum (\<lambda>i. x$i) UNIV < 1 }"
   apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball
   unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof-
   fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1"
   show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
     fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`

     have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf
       using `0<e` dimindex_ge_1 by(auto simp add: setsum_delta')
     also have "\<dots> \<le> 1" using ** apply(drule_tac as[rule_format]) by auto
     finally show "setsum (op $ x) UNIV < 1" by auto qed
 next
-  fix x::"real^'n::finite" assume as:"\<forall>i. 0 < x $ i" "setsum (op $ x) UNIV < 1"
+  fix x::"real^'n" assume as:"\<forall>i. 0 < x $ i" "setsum (op $ x) UNIV < 1"
   guess a using UNIV_witness[where 'a='b] ..
   let ?d = "(1 - setsum (op $ x) UNIV) / real (CARD('n))"
   have "Min ((op $ x) ` UNIV) > 0" apply(rule Min_grI) using as(1) dimindex_ge_1 by auto
   moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) using dimindex_ge_1 by(auto simp add: Suc_le_eq)
   ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1"

       fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
         using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto
       thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps)
     qed auto qed auto qed
 
-lemma interior_std_simplex_nonempty: obtains a::"real^'n::finite" where
+lemma interior_std_simplex_nonempty: obtains a::"real^'n" where
   "a \<in> interior(convex hull (insert 0 {basis i | i . i \<in> UNIV}))" proof-
   let ?D = "UNIV::'n set" let ?a = "setsum (\<lambda>b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
   have *:"{basis i :: real ^ 'n | i. i \<in> ?D} = basis ` ?D" by auto
   { fix i have "?a $ i = inverse (2 * real CARD('n))"
     unfolding setsum_component vector_smult_component and * and setsum_reindex[OF basis_inj] and o_def

     also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] by (auto simp add:field_simps)
     finally show "setsum (op $ ?a) ?D < 1" by auto qed qed
 
 subsection {* Paths. *}
 
-definition "path (g::real^1 \<Rightarrow> real^'n::finite) \<longleftrightarrow> continuous_on {0 .. 1} g"
+definition "path (g::real^1 \<Rightarrow> real^'n) \<longleftrightarrow> continuous_on {0 .. 1} g"
 
 definition "pathstart (g::real^1 \<Rightarrow> real^'n) = g 0"
 
 definition "pathfinish (g::real^1 \<Rightarrow> real^'n) = g 1"
 

     by(auto simp add:vector_component_simps image_iff) qed
 
 subsection {* Special case of straight-line paths. *}
 
 definition
-  linepath :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
+  linepath :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
   "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *\<^sub>R a + dest_vec1 x *\<^sub>R b)"
 
 lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
   unfolding pathstart_def linepath_def by auto
 

     by(auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) qed
 
 subsection {* sphere is path-connected. *}
 
 lemma path_connected_punctured_universe:
- assumes "2 \<le> CARD('n::finite)" shows "path_connected((UNIV::(real^'n::finite) set) - {a})" proof-
+ assumes "2 \<le> CARD('n::finite)" shows "path_connected((UNIV::(real^'n) set) - {a})" proof-
   obtain \<psi> where \<psi>:"bij_betw \<psi> {1..CARD('n)} (UNIV::'n set)" using ex_bij_betw_nat_finite_1[OF finite_UNIV] by auto
   let ?U = "UNIV::(real^'n) set" let ?u = "?U - {0}"
   let ?basis = "\<lambda>k. basis (\<psi> k)"
   let ?A = "\<lambda>k. {x::real^'n. \<exists>i\<in>{1..k}. inner (basis (\<psi> i)) x \<noteq> 0}"
   have "\<forall>k\<in>{2..CARD('n)}. path_connected (?A k)" proof

     apply rule apply(rule_tac x="x - a" in bexI) by auto
   have **:"\<And>x::real^'n. x\<noteq>0 \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)" unfolding Cart_eq by(auto simp add: inner_basis)
   show ?thesis unfolding * apply(rule path_connected_continuous_image) apply(rule continuous_on_intros)+ 
     unfolding ** apply(rule lem[THEN bspec[where x="CARD('n)"], unfolded ***]) using assms by auto qed
 
-lemma path_connected_sphere: assumes "2 \<le> CARD('n::finite)" shows "path_connected {x::real^'n::finite. norm(x - a) = r}" proof(cases "r\<le>0")
+lemma path_connected_sphere: assumes "2 \<le> CARD('n::finite)" shows "path_connected {x::real^'n. norm(x - a) = r}" proof(cases "r\<le>0")
   case True thus ?thesis proof(cases "r=0") 
     case False hence "{x::real^'n. norm(x - a) = r} = {}" using True by auto
     thus ?thesis using path_connected_empty by auto
   qed(auto intro!:path_connected_singleton) next
   case False hence *:"{x::real^'n. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule)

     apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
     apply(rule continuous_at_norm[unfolded o_def]) by auto
   thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
     by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
 
-lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n::finite. norm(x - a) = r}"
+lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}"
   using path_connected_sphere path_connected_imp_connected by auto
- 
+
 end