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.30    apply (simp add: norm_vector_def)
    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"