remove redundant lemma card_enum
authorhuffman
Wed Aug 31 13:51:22 2011 -0700 (2011-08-31 ago)
changeset 446291cd782f3458b
parent 44628 bd17b7543af1
child 44630 d08cb39b628a
remove redundant lemma card_enum
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 31 08:11:47 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 31 13:51:22 2011 -0700
     1.3 @@ -524,7 +524,7 @@
     1.4    show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
     1.5      unfolding * apply auto
     1.6      apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
     1.7 -    apply(rule_tac x=u in exI) by(auto intro!: exI)
     1.8 +    apply(rule_tac x=u in exI) by force
     1.9  qed
    1.10  
    1.11  lemma mem_affine:
    1.12 @@ -3028,7 +3028,7 @@
    1.13      hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
    1.14         using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
    1.15         apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
    1.16 -       by(auto simp add: inner_commute elim!: ballE)
    1.17 +       by(auto simp add: inner_commute del: ballE elim!: ballE)
    1.18      thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
    1.19    qed(insert closed_halfspace_ge, auto)
    1.20    then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
    1.21 @@ -3062,7 +3062,7 @@
    1.22    apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
    1.23    apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
    1.24    apply(rule assms[unfolded convex_def, rule_format]) prefer 6
    1.25 -  by (auto intro!: tendsto_intros)
    1.26 +  by (auto del: tendsto_const intro!: tendsto_intros)
    1.27  
    1.28  lemma convex_interior:
    1.29    fixes s :: "'a::real_normed_vector set"
    1.30 @@ -4156,7 +4156,7 @@
    1.31          using component_le_norm[of "y - x" i]
    1.32          using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
    1.33        thus "y $$ i \<le> x $$ i + ?d" by auto qed
    1.34 -    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat by(auto simp add: Suc_le_eq)
    1.35 +    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat by(auto simp add: Suc_le_eq)
    1.36      finally show "(\<forall>i<DIM('a). 0 \<le> y $$ i) \<and> setsum (op $$ y) {..<DIM('a)} \<le> 1" 
    1.37      proof safe fix i assume i:"i<DIM('a)"
    1.38        have "norm (x - y) < x$$i" apply(rule less_le_trans) 
    1.39 @@ -4176,7 +4176,7 @@
    1.40    show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof safe
    1.41      fix i assume i:"i<DIM('a)" show "0 < ?a $$ i" unfolding **[OF i] by(auto simp add: Suc_le_eq)
    1.42    next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real DIM('a))) ?D" apply(rule setsum_cong2, rule **) by auto
    1.43 -    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
    1.44 +    also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
    1.45      finally show "setsum (op $$ ?a) ?D < 1" by auto qed qed
    1.46  
    1.47  lemma rel_interior_substd_simplex: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
    1.48 @@ -4251,7 +4251,7 @@
    1.49          using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2]
    1.50          by(auto simp add: norm_minus_commute)
    1.51        thus "y $$ i \<le> x $$ i + ?d" by auto qed
    1.52 -    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat
    1.53 +    also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant real_eq_of_nat
    1.54        using `0 < card d` by auto
    1.55      finally show "setsum (op $$ y) d \<le> 1" .
    1.56       
    1.57 @@ -4294,7 +4294,7 @@
    1.58      finally show "0 < ?a $$ i" by auto
    1.59    next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D" 
    1.60        by(rule setsum_cong2, rule **) 
    1.61 -    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym]
    1.62 +    also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat real_divide_def[THEN sym]
    1.63        by (auto simp add:field_simps)
    1.64      finally show "setsum (op $$ ?a) ?D < 1" by auto
    1.65    next fix i assume "i<DIM('a)" and "i~:d"
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 31 08:11:47 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 31 13:51:22 2011 -0700
     2.3 @@ -2534,8 +2534,6 @@
     2.4    unfolding infnorm_set_image  ball_simps
     2.5    by (metis component_le_norm)
     2.6  
     2.7 -lemma card_enum: "card {1 .. n} = n" by auto
     2.8 -
     2.9  lemma norm_le_infnorm: "norm(x) <= sqrt(real DIM('a)) * infnorm(x::'a::euclidean_space)"
    2.10  proof-
    2.11    let ?d = "DIM('a)"