author huffman Tue Jun 02 20:10:56 2009 -0700 (2009-06-02) changeset 31399 d9769f093160 parent 31398 b67a3ac4882d child 31400 d671d74b2d1d
generalize lemma norm_pastecart
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 19:42:44 2009 -0700
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 20:10:56 2009 -0700
1.3 @@ -2746,17 +2746,19 @@
1.4  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"
1.5    by (simp add: dot_def setsum_UNIV_sum pastecart_def)
1.6
1.7 -lemma norm_pastecart: "norm(pastecart x y) <= norm(x :: real ^ 'm::finite) + norm(y::real^'n::finite)"
1.8 -  unfolding real_vector_norm_def dot_pastecart real_sqrt_le_iff id_def
1.9 -  apply (rule power2_le_imp_le)
1.11 -  apply (auto simp add: power2_eq_square ring_simps)
1.12 -  apply (simp add: power2_eq_square[symmetric])
1.13 -  apply (rule mult_nonneg_nonneg)
1.14 -  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
1.16 -  apply (simp_all add: real_sqrt_pow2[OF dot_pos_le])
1.17 -  done
1.18 +text {* TODO: move to NthRoot *}
1.20 +  assumes x: "0 \<le> x" and y: "0 \<le> y"
1.21 +  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
1.22 +apply (rule power2_le_imp_le)