src/HOL/Library/Euclidean_Space.thy
 changeset 32456 341c83339aeb parent 32412 8d1263a00392 child 32685 29e4e567b5f4
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Aug 29 14:31:39 2009 +0200
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Aug 31 14:09:42 2009 +0200
1.3 @@ -1055,28 +1055,6 @@
1.4  lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"
1.5    by (metis basic_trans_rules(21) norm_triangle_ineq)
1.6
1.7 -lemma setsum_delta:
1.8 -  assumes fS: "finite S"
1.9 -  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
1.10 -proof-
1.11 -  let ?f = "(\<lambda>k. if k=a then b k else 0)"
1.12 -  {assume a: "a \<notin> S"
1.13 -    hence "\<forall> k\<in> S. ?f k = 0" by simp
1.14 -    hence ?thesis  using a by simp}
1.15 -  moreover
1.16 -  {assume a: "a \<in> S"
1.17 -    let ?A = "S - {a}"
1.18 -    let ?B = "{a}"
1.19 -    have eq: "S = ?A \<union> ?B" using a by blast
1.20 -    have dj: "?A \<inter> ?B = {}" by simp
1.21 -    from fS have fAB: "finite ?A" "finite ?B" by auto
1.22 -    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
1.23 -      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
1.24 -      by simp
1.25 -    then have ?thesis  using a by simp}
1.26 -  ultimately show ?thesis by blast
1.27 -qed
1.28 -
1.29  lemma component_le_norm: "\<bar>x\$i\<bar> <= norm (x::real ^ 'n::finite)"
1.31    apply (rule member_le_setL2, simp_all)
1.32 @@ -2079,13 +2057,6 @@
1.33  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
1.34    by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
1.35
1.36 -lemma setsum_delta':
1.37 -  assumes fS: "finite S" shows
1.38 -  "setsum (\<lambda>k. if a = k then b k else 0) S =
1.39 -     (if a\<in> S then b a else 0)"
1.40 -  using setsum_delta[OF fS, of a b, symmetric]
1.41 -  by (auto intro: setsum_cong)
1.42 -
1.43  lemma matrix_mul_lid:
1.44    fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite"
1.45    shows "mat 1 ** A = A"
```