src/HOL/Power.thy
changeset 36409 d323e7773aa8
parent 36349 39be26d1bc28
child 39438 c5ece2a7a86e
     1.1 --- a/src/HOL/Power.thy	Mon Apr 26 11:34:19 2010 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Apr 26 15:37:50 2010 +0200
     1.3 @@ -392,27 +392,26 @@
     1.4    by (induct n)
     1.5      (auto simp add: no_zero_divisors elim: contrapos_pp)
     1.6  
     1.7 -lemma power_diff:
     1.8 -  fixes a :: "'a::field"
     1.9 +lemma (in field) power_diff:
    1.10    assumes nz: "a \<noteq> 0"
    1.11    shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
    1.12 -  by (induct m n rule: diff_induct) (simp_all add: nz)
    1.13 +  by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
    1.14  
    1.15  text{*Perhaps these should be simprules.*}
    1.16  lemma power_inverse:
    1.17 -  fixes a :: "'a::{division_ring,division_ring_inverse_zero,power}"
    1.18 -  shows "inverse (a ^ n) = (inverse a) ^ n"
    1.19 +  fixes a :: "'a::division_ring_inverse_zero"
    1.20 +  shows "inverse (a ^ n) = inverse a ^ n"
    1.21  apply (cases "a = 0")
    1.22  apply (simp add: power_0_left)
    1.23  apply (simp add: nonzero_power_inverse)
    1.24  done (* TODO: reorient or rename to inverse_power *)
    1.25  
    1.26  lemma power_one_over:
    1.27 -  "1 / (a::'a::{field,division_ring_inverse_zero, power}) ^ n =  (1 / a) ^ n"
    1.28 +  "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
    1.29    by (simp add: divide_inverse) (rule power_inverse)
    1.30  
    1.31  lemma power_divide:
    1.32 -  "(a / b) ^ n = (a::'a::{field,division_ring_inverse_zero}) ^ n / b ^ n"
    1.33 +  "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
    1.34  apply (cases "b = 0")
    1.35  apply (simp add: power_0_left)
    1.36  apply (rule nonzero_power_divide)