src/HOL/Real_Vector_Spaces.thy
changeset 54230 b1d955791529
parent 53600 8fda7ad57466
child 54263 c4159fe6fa46
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  qed
     1.5  
     1.6  lemma diff: "f (x - y) = f x - f y"
     1.7 -by (simp add: add minus diff_minus)
     1.8 +  using add [of x "- y"] by (simp add: minus)
     1.9  
    1.10  lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
    1.11  apply (cases "finite A")
    1.12 @@ -553,8 +553,7 @@
    1.13  proof -
    1.14    have "norm (a + - b) \<le> norm a + norm (- b)"
    1.15      by (rule norm_triangle_ineq)
    1.16 -  thus ?thesis
    1.17 -    by (simp only: diff_minus norm_minus_cancel)
    1.18 +  then show ?thesis by simp
    1.19  qed
    1.20  
    1.21  lemma norm_diff_ineq:
    1.22 @@ -571,7 +570,7 @@
    1.23    shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
    1.24  proof -
    1.25    have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
    1.26 -    by (simp add: diff_minus add_ac)
    1.27 +    by (simp add: algebra_simps)
    1.28    also have "\<dots> \<le> norm (a - c) + norm (b - d)"
    1.29      by (rule norm_triangle_ineq)
    1.30    finally show ?thesis .