src/HOL/Power.thy
changeset 25134 3d4953e88449
parent 25062 af5ef0d4d655
child 25162 ad4d5365d9d8
     1.1 --- a/src/HOL/Power.thy	Sun Oct 21 14:21:54 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Oct 21 14:53:44 2007 +0200
     1.3 @@ -140,16 +140,13 @@
     1.4  done
     1.5  
     1.6  lemma power_eq_0_iff [simp]:
     1.7 -     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
     1.8 +  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n\<noteq>0)"
     1.9  apply (induct "n")
    1.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.11  done
    1.12  
    1.13 -lemma field_power_eq_0_iff:
    1.14 -     "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
    1.15 -by simp (* TODO: delete *)
    1.16 -
    1.17 -lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    1.18 +lemma field_power_not_zero:
    1.19 +  "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    1.20  by force
    1.21  
    1.22  lemma nonzero_power_inverse:
    1.23 @@ -279,26 +276,26 @@
    1.24                   order_less_imp_le)
    1.25  done
    1.26  
    1.27 -lemma power_increasing_iff [simp]: 
    1.28 -     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
    1.29 -  by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
    1.30 +lemma power_increasing_iff [simp]:
    1.31 +  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
    1.32 +by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le) 
    1.33  
    1.34  lemma power_strict_increasing_iff [simp]:
    1.35 -     "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
    1.36 -  by (blast intro: power_less_imp_less_exp power_strict_increasing) 
    1.37 +  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
    1.38 +by (blast intro: power_less_imp_less_exp power_strict_increasing) 
    1.39  
    1.40  lemma power_le_imp_le_base:
    1.41 -  assumes le: "a ^ Suc n \<le> b ^ Suc n"
    1.42 -      and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
    1.43 -  shows "a \<le> b"
    1.44 - proof (rule ccontr)
    1.45 -   assume "~ a \<le> b"
    1.46 -   then have "b < a" by (simp only: linorder_not_le)
    1.47 -   then have "b ^ Suc n < a ^ Suc n"
    1.48 -     by (simp only: prems power_strict_mono)
    1.49 -   from le and this show "False"
    1.50 -      by (simp add: linorder_not_less [symmetric])
    1.51 - qed
    1.52 +assumes le: "a ^ Suc n \<le> b ^ Suc n"
    1.53 +    and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
    1.54 +shows "a \<le> b"
    1.55 +proof (rule ccontr)
    1.56 +  assume "~ a \<le> b"
    1.57 +  then have "b < a" by (simp only: linorder_not_le)
    1.58 +  then have "b ^ Suc n < a ^ Suc n"
    1.59 +    by (simp only: prems power_strict_mono)
    1.60 +  from le and this show "False"
    1.61 +    by (simp add: linorder_not_less [symmetric])
    1.62 +qed
    1.63  
    1.64  lemma power_less_imp_less_base:
    1.65    fixes a b :: "'a::{ordered_semidom,recpower}"
    1.66 @@ -345,7 +342,7 @@
    1.67  lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.68  by (insert one_le_power [of i n], simp)
    1.69  
    1.70 -lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
    1.71 +lemma nat_zero_less_power_iff [simp]: "(x^n = 0) = (x = (0::nat) & n\<noteq>0)"
    1.72  by (induct "n", auto)
    1.73  
    1.74  text{*Valid for the naturals, but what if @{text"0<i<1"}?
    1.75 @@ -393,7 +390,7 @@
    1.76  val power_mono = thm"power_mono";
    1.77  val power_strict_mono = thm"power_strict_mono";
    1.78  val power_eq_0_iff = thm"power_eq_0_iff";
    1.79 -val field_power_eq_0_iff = thm"field_power_eq_0_iff";
    1.80 +val field_power_eq_0_iff = thm"power_eq_0_iff";
    1.81  val field_power_not_zero = thm"field_power_not_zero";
    1.82  val power_inverse = thm"power_inverse";
    1.83  val nonzero_power_divide = thm"nonzero_power_divide";