src/HOL/Power.thy
changeset 14353 79f9fbef9106
parent 14348 744c868ee0b7
child 14438 6b41e98931f8
equal deleted inserted replaced
14352:a8b1a44d8264 14353:79f9fbef9106
   151 done
   151 done
   152 
   152 
   153 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
   153 lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
   154 by force
   154 by force
   155 
   155 
       
   156 lemma nonzero_power_inverse:
       
   157   "a \<noteq> 0 ==> inverse ((a::'a::{field,ringpower}) ^ n) = (inverse a) ^ n"
       
   158 apply (induct_tac "n")
       
   159 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib mult_commute)
       
   160 done
       
   161 
   156 text{*Perhaps these should be simprules.*}
   162 text{*Perhaps these should be simprules.*}
   157 lemma power_inverse:
   163 lemma power_inverse:
   158   "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
   164   "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
   159 apply (induct_tac "n")
   165 apply (induct_tac "n")
   160 apply (auto simp add: power_Suc inverse_mult_distrib)
   166 apply (auto simp add: power_Suc inverse_mult_distrib)
   161 done
   167 done
   162 
   168 
       
   169 lemma nonzero_power_divide: 
       
   170     "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
       
   171 by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
       
   172 
       
   173 lemma power_divide: 
       
   174     "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n/ b ^ n)"
       
   175 apply (case_tac "b=0", simp add: power_0_left)
       
   176 apply (rule nonzero_power_divide) 
       
   177 apply assumption 
       
   178 done
       
   179 
   163 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
   180 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
   164 apply (induct_tac "n")
   181 apply (induct_tac "n")
   165 apply (auto simp add: power_Suc abs_mult)
   182 apply (auto simp add: power_Suc abs_mult)
       
   183 done
       
   184 
       
   185 lemma zero_less_power_abs_iff [simp]:
       
   186      "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
       
   187 proof (induct "n")
       
   188   case 0
       
   189     show ?case by (simp add: zero_less_one)
       
   190 next
       
   191   case (Suc n)
       
   192     show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
       
   193 qed
       
   194 
       
   195 lemma zero_le_power_abs [simp]:
       
   196      "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n"
       
   197 apply (induct_tac "n")
       
   198 apply (auto simp add: zero_le_one zero_le_power)
   166 done
   199 done
   167 
   200 
   168 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
   201 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
   169 proof -
   202 proof -
   170   have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
   203   have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
   411 val power_strict_mono = thm"power_strict_mono";
   444 val power_strict_mono = thm"power_strict_mono";
   412 val power_eq_0_iff = thm"power_eq_0_iff";
   445 val power_eq_0_iff = thm"power_eq_0_iff";
   413 val field_power_eq_0_iff = thm"field_power_eq_0_iff";
   446 val field_power_eq_0_iff = thm"field_power_eq_0_iff";
   414 val field_power_not_zero = thm"field_power_not_zero";
   447 val field_power_not_zero = thm"field_power_not_zero";
   415 val power_inverse = thm"power_inverse";
   448 val power_inverse = thm"power_inverse";
       
   449 val nonzero_power_divide = thm"nonzero_power_divide";
       
   450 val power_divide = thm"power_divide";
   416 val power_abs = thm"power_abs";
   451 val power_abs = thm"power_abs";
       
   452 val zero_less_power_abs_iff = thm"zero_less_power_abs_iff";
       
   453 val zero_le_power_abs = thm "zero_le_power_abs";
   417 val power_minus = thm"power_minus";
   454 val power_minus = thm"power_minus";
   418 val power_Suc_less = thm"power_Suc_less";
   455 val power_Suc_less = thm"power_Suc_less";
   419 val power_strict_decreasing = thm"power_strict_decreasing";
   456 val power_strict_decreasing = thm"power_strict_decreasing";
   420 val power_decreasing = thm"power_decreasing";
   457 val power_decreasing = thm"power_decreasing";
   421 val power_Suc_less_one = thm"power_Suc_less_one";
   458 val power_Suc_less_one = thm"power_Suc_less_one";