# HG changeset patch
# User huffman
# Date 1314143268 25200
# Node ID 0e5c27f0752995f0cf3d0d1a712ccbc0b0149e24
# Parent  fa56622bb7bc32ee7fd26563fb402c5772a93849
remove unnecessary lemma card_ge1

diff -r fa56622bb7bc -r 0e5c27f07529 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 23 16:17:22 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 23 16:47:48 2011 -0700
@@ -40,9 +40,6 @@
 using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
 using add_divide_distrib[of u v "u+v"] by auto
 
-lemma card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1"
-by (metis Suc_eq_plus1 assms(1) assms(2) card_eq_0_iff fact_ge_one_nat fact_num_eq_if_nat one_le_mult_iff plus_nat.add_0)
-
 lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)" 
 by (blast dest: inj_onD)
 
@@ -4217,9 +4214,9 @@
     unfolding substd_simplex[OF assms] by fastsimp 
   obtain a where a:"a:d" using `d ~= {}` by auto
   let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
-  have "card d >= 1" using `d ~={}` card_ge1[of d] using `finite d` by auto
-  have "Min ((op $$ x) ` d) > 0" apply(rule Min_grI) using as `card d >= 1` `finite d` by auto
-  moreover have "?d > 0" apply(rule divide_pos_pos) using as using `card d >= 1` by(auto simp add: Suc_le_eq)
+  have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff)
+  have "Min ((op $$ x) ` d) > 0" using as `d \<noteq> {}` `finite d` by (simp add: Min_grI)
+  moreover have "?d > 0" apply(rule divide_pos_pos) using as using `0 < card d` by auto
   ultimately have h3: "min (Min ((op $$ x) ` d)) ?d > 0" by auto
 
   have "x : rel_interior (convex hull (insert 0 ?p))"
@@ -4234,14 +4231,14 @@
         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 `card d >= 1` by(auto simp add: Suc_le_eq)
+      using `0 < card d` by auto
     finally show "setsum (op $$ y) d \<le> 1" .
      
     fix i assume "i<DIM('a)" thus "0 \<le> y$$i" 
     proof(cases "i\<in>d") case True
       have "norm (x - y) < x$$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
-        using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `card d >= 1` `i:d`
-        apply auto by (metis Suc_n_not_le_n True card_eq_0_iff finite_imageI)
+        using Min_gr_iff[of "op $$ x ` d" "norm (x - y)"] `0 < card d` `i:d`
+        by (simp add: card_gt_0_iff)
       thus "0 \<le> y$$i" using component_le_norm[of "x - y" i] and as(1)[rule_format] by auto
     qed(insert y2, auto)
   qed
@@ -4260,7 +4257,7 @@
   let ?D = d let ?a = "setsum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card d)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
   have *:"{basis i :: 'a | i. i \<in> ?D} = basis ` ?D" by auto
   have "finite d" apply(rule finite_subset) using assms(2) by auto
-  hence d1: "real(card d) >= 1" using `d ~={}` card_ge1[of d] by auto
+  hence d1: "0 < real(card d)" using `d ~={}` by auto
   { fix i assume "i:d" have "?a $$ i = inverse (2 * real (card d))"
       unfolding * setsum_reindex[OF basis_inj_on, OF assms(2)] o_def
       apply(rule trans[of _ "setsum (\<lambda>j. if i = j then inverse (2 * real (card d)) else 0) ?D"]) 
@@ -4271,7 +4268,7 @@
   note ** = this
   show ?thesis apply(rule that[of ?a]) unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
   proof safe fix i assume "i:d" 
-    have "0 < inverse (2 * real (card d))" using d1 by(auto simp add: Suc_le_eq)
+    have "0 < inverse (2 * real (card d))" using d1 by auto
     also have "...=?a $$ i" using **[of i] `i:d` by auto
     finally show "0 < ?a $$ i" by auto
   next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"