--- a/src/HOL/Power.thy Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Power.thy Sun Oct 26 19:11:16 2014 +0100
@@ -244,9 +244,18 @@
end
+lemma power_eq_0_nat_iff [simp]:
+ fixes m n :: nat
+ shows "m ^ n = 0 \<longleftrightarrow> m = 0 \<and> n > 0"
+ by (induct n) auto
+
context ring_1_no_zero_divisors
begin
+lemma power_eq_0_iff [simp]:
+ "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
+ by (induct n) auto
+
lemma field_power_not_zero:
"a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
by (induct n) auto
@@ -559,6 +568,10 @@
"\<not> a\<^sup>2 < 0"
by (force simp add: power2_eq_square mult_less_0_iff)
+lemma power2_less_eq_zero_iff [simp]:
+ "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
+ by (simp add: le_less)
+
lemma abs_power2 [simp]:
"abs (a\<^sup>2) = a\<^sup>2"
by (simp add: power2_eq_square abs_mult abs_mult_self)
@@ -631,15 +644,13 @@
lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
unfolding One_nat_def by (cases m) simp_all
-lemma power2_sum:
- fixes x y :: "'a::comm_semiring_1"
- shows "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
+lemma (in comm_semiring_1) power2_sum:
+ "(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y"
by (simp add: algebra_simps power2_eq_square mult_2_right)
-lemma power2_diff:
- fixes x y :: "'a::comm_ring_1"
- shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
- by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute)
+lemma (in comm_ring_1) power2_diff:
+ "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
+ by (simp add: algebra_simps power2_eq_square mult_2_right)
lemma power_0_Suc [simp]:
"(0::'a::{power, semiring_0}) ^ Suc n = 0"
@@ -650,12 +661,6 @@
"0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
by (induct n) simp_all
-lemma power_eq_0_iff [simp]:
- "a ^ n = 0 \<longleftrightarrow>
- a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \<and> n \<noteq> 0"
- by (induct n)
- (auto simp add: no_zero_divisors elim: contrapos_pp)
-
lemma (in field) power_diff:
assumes nz: "a \<noteq> 0"
shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"