author huffman Wed Aug 31 13:51:22 2011 -0700 (2011-08-31 ago) changeset 44629 1cd782f3458b parent 44628 bd17b7543af1 child 44630 d08cb39b628a
remove redundant lemma card_enum
```     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.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.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)"
```