# HG changeset patch
# User huffman
# Date 1243998656 25200
# Node ID d9769f0931606b2b44c24c8da766057cd2c72bcb
# Parent  b67a3ac4882dd4cdfb8c4cf9adceb0bf44eb9204
generalize lemma norm_pastecart

diff -r b67a3ac4882d -r d9769f093160 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 19:42:44 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 20:10:56 2009 -0700
@@ -2746,17 +2746,19 @@
 lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
   by (simp add: dot_def setsum_UNIV_sum pastecart_def)
 
-lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ 'm::finite) + norm(y::real^'n::finite)"
-  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
-  apply (rule power2_le_imp_le)
-  apply (simp add: real_sqrt_pow2[OF add_nonneg_nonneg[OF dot_pos_le[of x] dot_pos_le[of y]]])
-  apply (auto simp add: power2_eq_square ring_simps)
-  apply (simp add: power2_eq_square[symmetric])
-  apply (rule mult_nonneg_nonneg)
-  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
-  apply (rule add_nonneg_nonneg)
-  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
-  done
+text {* TODO: move to NthRoot *}
+lemma sqrt_add_le_add_sqrt:
+  assumes x: "0 \<le> x" and y: "0 \<le> y"
+  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
+apply (rule power2_le_imp_le)
+apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
+apply (simp add: mult_nonneg_nonneg x y)
+apply (simp add: add_nonneg_nonneg x y)
+done
+
+lemma norm_pastecart: "norm (pastecart x y) <= norm x + norm y"
+  unfolding vector_norm_def setL2_def setsum_UNIV_sum
+  by (simp add: sqrt_add_le_add_sqrt setsum_nonneg)
 
 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}