--- a/src/HOL/Power.thy Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Power.thy Mon Dec 28 01:26:34 2015 +0100
@@ -622,24 +622,20 @@
context linordered_idom
begin
-lemma power_abs:
- "abs (a ^ n) = abs a ^ n"
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
by (induct n) (auto simp add: abs_mult)
-lemma abs_power_minus [simp]:
- "abs ((-a) ^ n) = abs (a ^ n)"
+lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
by (simp add: power_abs)
-lemma zero_less_power_abs_iff [simp]:
- "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
+lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff)
qed
-lemma zero_le_power_abs [simp]:
- "0 \<le> abs a ^ n"
+lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
by (rule zero_le_power [OF abs_ge_zero])
lemma zero_le_power2 [simp]:
@@ -658,12 +654,10 @@
"a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
by (simp add: le_less)
-lemma abs_power2 [simp]:
- "abs (a\<^sup>2) = a\<^sup>2"
+lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
by (simp add: power2_eq_square abs_mult abs_mult_self)
-lemma power2_abs [simp]:
- "(abs a)\<^sup>2 = a\<^sup>2"
+lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
by (simp add: power2_eq_square abs_mult_self)
lemma odd_power_less_zero:
@@ -729,14 +723,14 @@
by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
qed
-lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
+lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
using abs_le_square_iff [of x 1]
by simp
-lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
+lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
by (auto simp add: abs_if power2_eq_1_iff)
-lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
+lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
using abs_square_eq_1 [of x] abs_square_le_1 [of x]
by (auto simp add: le_less)