rationalised and generalised some theorems concerning abs and x^2.
authorpaulson <lp15@cam.ac.uk>
Tue Mar 31 16:48:48 2015 +0100 (2015-03-31)
changeset 598658a20dd967385
parent 59863 30519ff3dffb
child 59866 eebe69f31474
rationalised and generalised some theorems concerning abs and x^2.
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Power.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Tue Mar 31 15:01:06 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Tue Mar 31 16:48:48 2015 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4      hence "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2)
     1.5          \<le> (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
     1.6        by (auto intro!: setsum_mono
     1.7 -        simp add: clamp_def dist_real_def real_abs_le_square_iff[symmetric])
     1.8 +        simp add: clamp_def dist_real_def abs_le_square_iff[symmetric])
     1.9      thus ?thesis
    1.10        by (auto intro: real_sqrt_le_mono
    1.11          simp add: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 31 15:01:06 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Mar 31 16:48:48 2015 +0100
     2.3 @@ -68,25 +68,14 @@
     2.4  lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
     2.5    by (auto simp add: norm_eq_sqrt_inner)
     2.6  
     2.7 -lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)\<^sup>2 \<le> y\<^sup>2"
     2.8 -proof
     2.9 -  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    2.10 -  then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
    2.11 -  then show "x\<^sup>2 \<le> y\<^sup>2" by simp
    2.12 -next
    2.13 -  assume "x\<^sup>2 \<le> y\<^sup>2"
    2.14 -  then have "sqrt (x\<^sup>2) \<le> sqrt (y\<^sup>2)" by (rule real_sqrt_le_mono)
    2.15 -  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
    2.16 -qed
    2.17 -
    2.18  lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
    2.19 -  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
    2.20 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    2.21    using norm_ge_zero[of x]
    2.22    apply arith
    2.23    done
    2.24  
    2.25  lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
    2.26 -  apply (simp add: dot_square_norm real_abs_le_square_iff[symmetric])
    2.27 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    2.28    using norm_ge_zero[of x]
    2.29    apply arith
    2.30    done
     3.1 --- a/src/HOL/Power.thy	Tue Mar 31 15:01:06 2015 +0100
     3.2 +++ b/src/HOL/Power.thy	Tue Mar 31 16:48:48 2015 +0100
     3.3 @@ -645,6 +645,29 @@
     3.4    "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
     3.5    unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
     3.6  
     3.7 +lemma abs_le_square_iff:
     3.8 +   "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
     3.9 +proof
    3.10 +  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    3.11 +  then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
    3.12 +  then show "x\<^sup>2 \<le> y\<^sup>2" by simp
    3.13 +next
    3.14 +  assume "x\<^sup>2 \<le> y\<^sup>2"
    3.15 +  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    3.16 +    by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
    3.17 +qed
    3.18 +
    3.19 +lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
    3.20 +  using abs_le_square_iff [of x 1]
    3.21 +  by simp
    3.22 +
    3.23 +lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
    3.24 +  by (auto simp add: abs_if power2_eq_1_iff)
    3.25 +  
    3.26 +lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
    3.27 +  using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
    3.28 +  by (auto simp add: le_less)
    3.29 +
    3.30  end
    3.31  
    3.32  
     4.1 --- a/src/HOL/Rings.thy	Tue Mar 31 15:01:06 2015 +0100
     4.2 +++ b/src/HOL/Rings.thy	Tue Mar 31 16:48:48 2015 +0100
     4.3 @@ -1260,6 +1260,10 @@
     4.4    "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
     4.5    by (auto simp add: diff_less_eq ac_simps abs_less_iff)
     4.6  
     4.7 +lemma abs_diff_le_iff:
     4.8 +   "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r"
     4.9 +  by (auto simp add: diff_le_eq ac_simps abs_le_iff)
    4.10 +
    4.11  end
    4.12  
    4.13  hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib
     5.1 --- a/src/HOL/Transcendental.thy	Tue Mar 31 15:01:06 2015 +0100
     5.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 31 16:48:48 2015 +0100
     5.3 @@ -4542,16 +4542,6 @@
     5.4    (is "summable (?c x)")
     5.5    by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms])
     5.6  
     5.7 -lemma less_one_imp_sqr_less_one:
     5.8 -  fixes x :: real
     5.9 -  assumes "\<bar>x\<bar> < 1"
    5.10 -  shows "x\<^sup>2 < 1"
    5.11 -proof -
    5.12 -  have "\<bar>x\<^sup>2\<bar> < 1"
    5.13 -    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
    5.14 -  thus ?thesis using zero_le_power2 by auto
    5.15 -qed
    5.16 -
    5.17  lemma DERIV_arctan_series:
    5.18    assumes "\<bar> x \<bar> < 1"
    5.19    shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))"
    5.20 @@ -4568,7 +4558,7 @@
    5.21    {
    5.22      fix x :: real
    5.23      assume "\<bar>x\<bar> < 1"
    5.24 -    hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
    5.25 +    hence "x\<^sup>2 < 1" by (simp add: abs_square_less_1)
    5.26      have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
    5.27        by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
    5.28      hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
    5.29 @@ -4676,7 +4666,7 @@
    5.30              hence "\<bar>x\<bar> < r" by auto
    5.31              hence "\<bar>x\<bar> < 1" using `r < 1` by auto
    5.32              have "\<bar> - (x\<^sup>2) \<bar> < 1"
    5.33 -              using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto
    5.34 +              using abs_square_less_1 `\<bar>x\<bar> < 1` by auto
    5.35              hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))"
    5.36                unfolding real_norm_def[symmetric] by (rule geometric_sums)
    5.37              hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))"