src/HOL/Power.thy
changeset 59865 8a20dd967385
parent 59741 5b762cd73a8e
child 59867 58043346ca64
     1.1 --- a/src/HOL/Power.thy	Tue Mar 31 15:01:06 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Mar 31 16:48:48 2015 +0100
     1.3 @@ -645,6 +645,29 @@
     1.4    "0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
     1.5    unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff)
     1.6  
     1.7 +lemma abs_le_square_iff:
     1.8 +   "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2"
     1.9 +proof
    1.10 +  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    1.11 +  then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp)
    1.12 +  then show "x\<^sup>2 \<le> y\<^sup>2" by simp
    1.13 +next
    1.14 +  assume "x\<^sup>2 \<le> y\<^sup>2"
    1.15 +  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>"
    1.16 +    by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
    1.17 +qed
    1.18 +
    1.19 +lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
    1.20 +  using abs_le_square_iff [of x 1]
    1.21 +  by simp
    1.22 +
    1.23 +lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
    1.24 +  by (auto simp add: abs_if power2_eq_1_iff)
    1.25 +  
    1.26 +lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
    1.27 +  using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
    1.28 +  by (auto simp add: le_less)
    1.29 +
    1.30  end
    1.31  
    1.32