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
```