generalize class restrictions on some lemmas
authorhuffman
Thu May 17 19:12:47 2007 +0200 (2007-05-17)
changeset 22991b9e2a133e84e
parent 22990 775e9de3db48
child 22992 fc54d5fc4a7a
generalize class restrictions on some lemmas
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Thu May 17 18:32:17 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu May 17 19:12:47 2007 +0200
     1.3 @@ -141,32 +141,33 @@
     1.4  done
     1.5  
     1.6  lemma power_eq_0_iff [simp]:
     1.7 -     "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
     1.8 +     "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)"
     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 [simp]:
    1.14 +lemma field_power_eq_0_iff:
    1.15       "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
    1.16 -apply (induct "n")
    1.17 -apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
    1.18 -done
    1.19 +by simp (* TODO: delete *)
    1.20  
    1.21 -lemma field_power_not_zero: "a \<noteq> (0::'a::{division_ring,recpower}) ==> a^n \<noteq> 0"
    1.22 +lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0"
    1.23  by force
    1.24  
    1.25  lemma nonzero_power_inverse:
    1.26 -  "a \<noteq> 0 ==> inverse ((a::'a::{division_ring,recpower}) ^ n) = (inverse a) ^ n"
    1.27 +  fixes a :: "'a::{division_ring,recpower}"
    1.28 +  shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n"
    1.29  apply (induct "n")
    1.30  apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes)
    1.31 -done
    1.32 +done (* TODO: reorient or rename to nonzero_inverse_power *)
    1.33  
    1.34  text{*Perhaps these should be simprules.*}
    1.35  lemma power_inverse:
    1.36 -  "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
    1.37 -apply (induct "n")
    1.38 -apply (auto simp add: power_Suc inverse_mult_distrib)
    1.39 -done
    1.40 +  fixes a :: "'a::{division_ring,division_by_zero,recpower}"
    1.41 +  shows "inverse (a ^ n) = (inverse a) ^ n"
    1.42 +apply (cases "a = 0")
    1.43 +apply (simp add: power_0_left)
    1.44 +apply (simp add: nonzero_power_inverse)
    1.45 +done (* TODO: reorient or rename to inverse_power *)
    1.46  
    1.47  lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = 
    1.48      (1 / a)^n"