src/HOL/Power.thy
changeset 64715 33d5fa0ce6e5
parent 64065 40d440b75b00
child 64964 a0c985a57f7e
     1.1 --- a/src/HOL/Power.thy	Fri Dec 30 18:02:27 2016 +0100
     1.2 +++ b/src/HOL/Power.thy	Sat Dec 31 08:12:31 2016 +0100
     1.3 @@ -582,10 +582,22 @@
     1.4  context linordered_idom
     1.5  begin
     1.6  
     1.7 -lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
     1.8 -  by (induct n) (auto simp add: abs_mult)
     1.9 +lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
    1.10 +  by (simp add: power2_eq_square)
    1.11 +
    1.12 +lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
    1.13 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
    1.14  
    1.15 -lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
    1.16 +lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
    1.17 +  by (force simp add: power2_eq_square mult_less_0_iff)
    1.18 +
    1.19 +lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
    1.20 +  by (induct n) (simp_all add: abs_mult)
    1.21 +
    1.22 +lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
    1.23 +  by (induct n) (simp_all add: sgn_mult)
    1.24 +    
    1.25 +lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
    1.26    by (simp add: power_abs)
    1.27  
    1.28  lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
    1.29 @@ -600,15 +612,6 @@
    1.30  lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
    1.31    by (rule zero_le_power [OF abs_ge_zero])
    1.32  
    1.33 -lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
    1.34 -  by (simp add: power2_eq_square)
    1.35 -
    1.36 -lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
    1.37 -  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
    1.38 -
    1.39 -lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
    1.40 -  by (force simp add: power2_eq_square mult_less_0_iff)
    1.41 -
    1.42  lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
    1.43    by (simp add: le_less)
    1.44  
    1.45 @@ -618,7 +621,7 @@
    1.46  lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
    1.47    by (simp add: power2_eq_square)
    1.48  
    1.49 -lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
    1.50 +lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
    1.51  proof (induct n)
    1.52    case 0
    1.53    then show ?case by simp
    1.54 @@ -630,11 +633,11 @@
    1.55      by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
    1.56  qed
    1.57  
    1.58 -lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
    1.59 +lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
    1.60    using odd_power_less_zero [of a n]
    1.61    by (force simp add: linorder_not_less [symmetric])
    1.62  
    1.63 -lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2*n)"
    1.64 +lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
    1.65  proof (induct n)
    1.66    case 0
    1.67    show ?case by simp