src/HOL/Power.thy
 changeset 25134 3d4953e88449 parent 25062 af5ef0d4d655 child 25162 ad4d5365d9d8
```--- a/src/HOL/Power.thy	Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Power.thy	Sun Oct 21 14:53:44 2007 +0200
@@ -140,16 +140,13 @@
done

lemma power_eq_0_iff [simp]:
-     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
+  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
apply (induct "n")
apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
done

-lemma field_power_eq_0_iff:
-     "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
-by simp (* TODO: delete *)
-
-lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
+lemma field_power_not_zero:
+  "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
by force

lemma nonzero_power_inverse:
@@ -279,26 +276,26 @@
order_less_imp_le)
done

-lemma power_increasing_iff [simp]:
-     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
-  by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)
+lemma power_increasing_iff [simp]:
+  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
+by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)

lemma power_strict_increasing_iff [simp]:
-     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
-  by (blast intro: power_less_imp_less_exp power_strict_increasing)
+  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
+by (blast intro: power_less_imp_less_exp power_strict_increasing)

lemma power_le_imp_le_base:
-  assumes le: "a ^ Suc n \<le> b ^ Suc n"
-      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
-  shows "a \<le> b"
- proof (rule ccontr)
-   assume "~ a \<le> b"
-   then have "b < a" by (simp only: linorder_not_le)
-   then have "b ^ Suc n < a ^ Suc n"
-     by (simp only: prems power_strict_mono)
-   from le and this show "False"
-      by (simp add: linorder_not_less [symmetric])
- qed
+assumes le: "a ^ Suc n \<le> b ^ Suc n"
+    and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
+shows "a \<le> b"
+proof (rule ccontr)
+  assume "~ a \<le> b"
+  then have "b < a" by (simp only: linorder_not_le)
+  then have "b ^ Suc n < a ^ Suc n"
+    by (simp only: prems power_strict_mono)
+  from le and this show "False"
+    by (simp add: linorder_not_less [symmetric])
+qed

lemma power_less_imp_less_base:
fixes a b :: "'a::{ordered_semidom,recpower}"
@@ -345,7 +342,7 @@
lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
by (insert one_le_power [of i n], simp)

-lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
by (induct "n", auto)

text{*Valid for the naturals, but what if @{text"0<i<1"}?
@@ -393,7 +390,7 @@
val power_mono = thm"power_mono";
val power_strict_mono = thm"power_strict_mono";
val power_eq_0_iff = thm"power_eq_0_iff";
-val field_power_eq_0_iff = thm"field_power_eq_0_iff";
+val field_power_eq_0_iff = thm"power_eq_0_iff";
val field_power_not_zero = thm"field_power_not_zero";
val power_inverse = thm"power_inverse";
val nonzero_power_divide = thm"nonzero_power_divide";```