# HG changeset patch # User huffman # Date 1178741666 -7200 # Node ID 38ae2815989f0c3b3ae2193e6d8c039e6eaa561f # Parent c714f6d0a8d72541ca75ce19c5bd82296630f92e add lemma norm_diff_ineq; shorten other proofs diff -r c714f6d0a8d7 -r 38ae2815989f src/HOL/Real/RealVector.thy --- a/src/HOL/Real/RealVector.thy Wed May 09 19:37:22 2007 +0200 +++ b/src/HOL/Real/RealVector.thy Wed May 09 22:14:26 2007 +0200 @@ -437,10 +437,9 @@ fixes a b :: "'a::real_normed_vector" shows "norm (a - b) = norm (b - a)" proof - - have "norm (a - b) = norm (- (a - b))" - by (simp only: norm_minus_cancel) - also have "\ = norm (b - a)" by simp - finally show ?thesis . + have "norm (- (b - a)) = norm (b - a)" + by (rule norm_minus_cancel) + thus ?thesis by simp qed lemma norm_triangle_ineq2: @@ -449,10 +448,7 @@ proof - have "norm (a - b + b) \ norm (a - b) + norm b" by (rule norm_triangle_ineq) - also have "(a - b + b) = a" - by simp - finally show ?thesis - by (simp add: compare_rls) + thus ?thesis by simp qed lemma norm_triangle_ineq3: @@ -469,12 +465,19 @@ fixes a b :: "'a::real_normed_vector" shows "norm (a - b) \ norm a + norm b" proof - - have "norm (a - b) = norm (a + - b)" - by (simp only: diff_minus) - also have "\ \ norm a + norm (- b)" + have "norm (a + - b) \ norm a + norm (- b)" by (rule norm_triangle_ineq) - finally show ?thesis - by simp + thus ?thesis + by (simp only: diff_minus norm_minus_cancel) +qed + +lemma norm_diff_ineq: + fixes a b :: "'a::real_normed_vector" + shows "norm a - norm b \ norm (a + b)" +proof - + have "norm a - norm (- b) \ norm (a - - b)" + by (rule norm_triangle_ineq2) + thus ?thesis by simp qed lemma norm_diff_triangle_ineq: