add lemma real_sqrt_sum_squares_triangle_ineq
authorhuffman
Tue May 08 04:56:28 2007 +0200 (2007-05-08)
changeset 228585ca5d1cce388
parent 22857 cb84e886cc90
child 22859 c03c076d9dca
add lemma real_sqrt_sum_squares_triangle_ineq
src/HOL/Hyperreal/NthRoot.thy
     1.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue May 08 04:55:19 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue May 08 04:56:28 2007 +0200
     1.3 @@ -487,4 +487,32 @@
     1.4  apply (rule real_sqrt_eq_iff, auto)
     1.5  done
     1.6  
     1.7 +lemma power2_sum:
     1.8 +  fixes x y :: "'a::{number_ring,recpower}"
     1.9 +  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
    1.10 +by (simp add: left_distrib right_distrib power2_eq_square)
    1.11 +
    1.12 +lemma power2_diff:
    1.13 +  fixes x y :: "'a::{number_ring,recpower}"
    1.14 +  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
    1.15 +by (simp add: left_diff_distrib right_diff_distrib power2_eq_square)
    1.16 +
    1.17 +lemma real_sqrt_sum_squares_triangle_ineq:
    1.18 +  "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
    1.19 +apply (rule power2_le_imp_le, simp)
    1.20 +apply (simp add: power2_sum)
    1.21 +apply (simp only: mult_assoc right_distrib [symmetric])
    1.22 +apply (rule mult_left_mono)
    1.23 +apply (rule power2_le_imp_le)
    1.24 +apply (simp add: power2_sum power_mult_distrib)
    1.25 +apply (simp add: ring_distrib)
    1.26 +apply (subgoal_tac "0 \<le> b\<twosuperior> * c\<twosuperior> + a\<twosuperior> * d\<twosuperior> - 2 * (a * c) * (b * d)", simp)
    1.27 +apply (rule_tac b="(a * d - b * c)\<twosuperior>" in ord_le_eq_trans)
    1.28 +apply (rule zero_le_power2)
    1.29 +apply (simp add: power2_diff power_mult_distrib)
    1.30 +apply (simp add: mult_nonneg_nonneg)
    1.31 +apply simp
    1.32 +apply (simp add: add_increasing)
    1.33 +done
    1.34 +
    1.35  end