# HG changeset patch
# User huffman
# Date 1277923895 25200
# Node ID a5400b94d2dd4e7eca2c1f6f84b3b32240ef8838
# Parent  dbdbebec57dfcda66ae91524a9632dc11f415009
minimize dependencies on Numeral_Type

diff -r dbdbebec57df -r a5400b94d2dd src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jun 30 10:42:38 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jun 30 11:51:35 2010 -0700
@@ -59,9 +59,6 @@
 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
 
@@ -1648,7 +1645,7 @@
       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"
@@ -2227,8 +2224,6 @@
   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}"
@@ -2238,7 +2233,7 @@
       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
@@ -2519,7 +2514,7 @@
   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"
@@ -2528,7 +2523,7 @@
         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) 
diff -r dbdbebec57df -r a5400b94d2dd src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 10:42:38 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jun 30 11:51:35 2010 -0700
@@ -7,7 +7,7 @@
 theory Euclidean_Space
 imports
   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-  Infinite_Set Numeral_Type
+  Infinite_Set
   Inner_Product L2_Norm Convex
 uses "positivstellensatz.ML" ("normarith.ML")
 begin