diff -r b933700f0384 -r 3d4953e88449 src/HOL/Power.thy --- 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}) & 00)" 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 (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \ 0" +lemma field_power_not_zero: + "a \ (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \ 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 \ b ^ y) = (x \ 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 \ b ^ y) = (x \ 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 \ b ^ Suc n" - and ynonneg: "(0::'a::{ordered_semidom,recpower}) \ b" - shows "a \ b" - proof (rule ccontr) - assume "~ a \ 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 \ b ^ Suc n" + and ynonneg: "(0::'a::{ordered_semidom,recpower}) \ b" +shows "a \ b" +proof (rule ccontr) + assume "~ a \ 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 \ i ==> Suc 0 \ i^n" by (insert one_le_power [of i n], simp) -lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \ (0::nat) | n=0)" +lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\0)" by (induct "n", auto) text{*Valid for the naturals, but what if @{text"0