src/HOL/Power.thy
changeset 63417 c184ec919c70
parent 63040 eb4ddd18d635
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Power.thy	Fri Jul 08 23:43:11 2016 +0200
     1.2 +++ b/src/HOL/Power.thy	Sat Jul 09 13:26:16 2016 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  
     1.5  lemma of_nat_power [simp]:
     1.6    "of_nat (m ^ n) = of_nat m ^ n"
     1.7 -  by (induct n) (simp_all add: of_nat_mult)
     1.8 +  by (induct n) simp_all
     1.9  
    1.10  lemma zero_power:
    1.11    "0 < n \<Longrightarrow> 0 ^ n = 0"
    1.12 @@ -645,10 +645,10 @@
    1.13    by (simp add: le_less)
    1.14  
    1.15  lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
    1.16 -  by (simp add: power2_eq_square abs_mult abs_mult_self)
    1.17 +  by (simp add: power2_eq_square)
    1.18  
    1.19  lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
    1.20 -  by (simp add: power2_eq_square abs_mult_self)
    1.21 +  by (simp add: power2_eq_square)
    1.22  
    1.23  lemma odd_power_less_zero:
    1.24    "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
    1.25 @@ -749,6 +749,18 @@
    1.26    "(x - y)\<^sup>2 = (y - x)\<^sup>2"
    1.27    by (simp add: algebra_simps power2_eq_square)
    1.28  
    1.29 +lemma (in comm_ring_1) minus_power_mult_self:
    1.30 +  "(- a) ^ n * (- a) ^ n = a ^ (2 * n)"
    1.31 +  by (simp add: power_mult_distrib [symmetric]) (simp add: power2_eq_square [symmetric] power_mult [symmetric])
    1.32 +  
    1.33 +lemma (in comm_ring_1) minus_one_mult_self [simp]:
    1.34 +  "(- 1) ^ n * (- 1) ^ n = 1"
    1.35 +  using minus_power_mult_self [of 1 n] by simp
    1.36 +
    1.37 +lemma (in comm_ring_1) left_minus_one_mult_self [simp]:
    1.38 +  "(- 1) ^ n * ((- 1) ^ n * a) = a"
    1.39 +  by (simp add: mult.assoc [symmetric])
    1.40 +
    1.41  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
    1.42  
    1.43  lemmas zero_compare_simps =