src/HOL/Power.thy
changeset 14353 79f9fbef9106
parent 14348 744c868ee0b7
child 14438 6b41e98931f8
     1.1 --- a/src/HOL/Power.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/src/HOL/Power.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -153,6 +153,12 @@
     1.4  lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
     1.5  by force
     1.6  
     1.7 +lemma nonzero_power_inverse:
     1.8 +  "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
     1.9 +apply (induct_tac "n")
    1.10 +apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
    1.11 +done
    1.12 +
    1.13  text{*Perhaps these should be simprules.*}
    1.14  lemma power_inverse:
    1.15    "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
    1.16 @@ -160,11 +166,38 @@
    1.17  apply (auto simp add: power_Suc inverse_mult_distrib)
    1.18  done
    1.19  
    1.20 +lemma nonzero_power_divide: 
    1.21 +    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
    1.22 +by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
    1.23 +
    1.24 +lemma power_divide: 
    1.25 +    "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
    1.26 +apply (case_tac "b=0", simp add: power_0_left)
    1.27 +apply (rule nonzero_power_divide) 
    1.28 +apply assumption 
    1.29 +done
    1.30 +
    1.31  lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
    1.32  apply (induct_tac "n")
    1.33  apply (auto simp add: power_Suc abs_mult)
    1.34  done
    1.35  
    1.36 +lemma zero_less_power_abs_iff [simp]:
    1.37 +     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
    1.38 +proof (induct "n")
    1.39 +  case 0
    1.40 +    show ?case by (simp add: zero_less_one)
    1.41 +next
    1.42 +  case (Suc n)
    1.43 +    show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
    1.44 +qed
    1.45 +
    1.46 +lemma zero_le_power_abs [simp]:
    1.47 +     "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"
    1.48 +apply (induct_tac "n")
    1.49 +apply (auto simp add: zero_le_one zero_le_power)
    1.50 +done
    1.51 +
    1.52  lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
    1.53  proof -
    1.54    have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
    1.55 @@ -413,7 +446,11 @@
    1.56  val field_power_eq_0_iff = thm"field_power_eq_0_iff";
    1.57  val field_power_not_zero = thm"field_power_not_zero";
    1.58  val power_inverse = thm"power_inverse";
    1.59 +val nonzero_power_divide = thm"nonzero_power_divide";
    1.60 +val power_divide = thm"power_divide";
    1.61  val power_abs = thm"power_abs";
    1.62 +val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
    1.63 +val zero_le_power_abs = thm "zero_le_power_abs";
    1.64  val power_minus = thm"power_minus";
    1.65  val power_Suc_less = thm"power_Suc_less";
    1.66  val power_strict_decreasing = thm"power_strict_decreasing";