src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy

 
 lemma norm_minus_eqI:"x = - 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"
-  using one_le_card_finite by auto
 
 lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
   unfolding norm_eq_sqrt_inner by simp
 
 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"

       thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
       fix x assume "x\<in>X ` h" then guess y unfolding image_iff ..
       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)
+qed(auto) qed(auto)
 
 lemma helly: fixes f::"('a::euclidean_space) set set"
   assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
           "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   shows "\<Inter> f \<noteq>{}"

   let ?d = "(\<chi>\<chi> i. d)::'a"
   obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
   have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:euclidean_simps)
   hence "c\<noteq>{}" using c by auto
   def k \<equiv> "Max (f ` c)"
-  have real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1" 
-    by(metis dimindex_ge_1 real_eq_of_nat real_of_nat_1 real_of_nat_le_iff) 
   have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
     apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof 
     fix z assume z:"z\<in>{x - ?d..x + ?d}"
     have e:"e = setsum (\<lambda>i. d) {..<DIM('a)}" unfolding setsum_constant d_def using dimge1
       unfolding real_eq_of_nat by auto
     show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
       using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:euclidean_simps) qed
   hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
     unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
-  have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto
+  have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 by auto
   hence dsube:"cball x d \<subseteq> cball x e" unfolding subset_eq Ball_def mem_cball by auto
   have conv:"convex_on (cball x d) f" apply(rule convex_on_subset, rule convex_on_subset[OF assms(2)]) apply(rule e(1)) using dsube by auto
   hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
     fix y assume y:"y\<in>cball x d"
     { fix i assume "i<DIM('a)" hence "x $$ i - d \<le> y $$ i"  "y $$ i \<le> x $$ i + d" 

     finally show "setsum (op $$ x) {..<DIM('a)} < 1" by auto qed
 next fix x::"'a" assume as:"\<forall>i<DIM('a). 0 < x $$ i" "setsum (op $$ x) {..<DIM('a)} < 1"
   guess a using UNIV_witness[where 'a='b] ..
   let ?d = "(1 - setsum (op $$ x) {..<DIM('a)}) / real (DIM('a))"
   have "Min ((op $$ x) ` {..<DIM('a)}) > 0" apply(rule Min_grI) using as(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)
+  moreover have"?d > 0" apply(rule divide_pos_pos) using as(2) by(auto simp add: Suc_le_eq)
   ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1"
     apply(rule_tac x="min (Min ((op $$ x) ` {..<DIM('a)})) ?D" in exI) apply rule defer apply(rule,rule) proof-
     fix y assume y:"dist x y < min (Min (op $$ x ` {..<DIM('a)})) ?d"
     have "setsum (op $$ y) {..<DIM('a)} \<le> setsum (\<lambda>i. x$$i + ?d) {..<DIM('a)}" proof(rule setsum_mono)
       fix i assume "i\<in>{..<DIM('a)}" hence "abs (y$$i - x$$i) < ?d" apply-apply(rule le_less_trans)
         using component_le_norm[of "y - x" i]
         using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
       thus "y $$ i \<le> x $$ i + ?d" by auto qed
-    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
+    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat by(auto simp add: Suc_le_eq)
     finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1" 
     proof safe fix i assume i:"i<DIM('a)"
       have "norm (x - y) < x$$i" apply(rule less_le_trans) 
         apply(rule y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]) using i by auto
       thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto