# HG changeset patch
# User huffman
# Date 1179421967 -7200
# Node ID b9e2a133e84e1606f02218465da57e57f093ef45
# Parent  775e9de3db48ec9e7a826d0613f66eabc49177ce
generalize class restrictions on some lemmas

diff -r 775e9de3db48 -r b9e2a133e84e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu May 17 18:32:17 2007 +0200
+++ b/src/HOL/Power.thy	Thu May 17 19:12:47 2007 +0200
@@ -141,32 +141,33 @@
 done
 
 lemma power_eq_0_iff [simp]:
-     "(a^n = 0) = (a = (0::'a::{ordered_idom,recpower}) & 0<n)"
+     "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)"
 apply (induct "n")
 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
 done
 
-lemma field_power_eq_0_iff [simp]:
+lemma field_power_eq_0_iff:
      "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
-apply (induct "n")
-apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
-done
+by simp (* TODO: delete *)
 
-lemma field_power_not_zero: "a \<noteq> (0::'a::{division_ring,recpower}) ==> a^n \<noteq> 0"
+lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0"
 by force
 
 lemma nonzero_power_inverse:
-  "a \<noteq> 0 ==> inverse ((a::'a::{division_ring,recpower}) ^ n) = (inverse a) ^ n"
+  fixes a :: "'a::{division_ring,recpower}"
+  shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n"
 apply (induct "n")
 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes)
-done
+done (* TODO: reorient or rename to nonzero_inverse_power *)
 
 text{*Perhaps these should be simprules.*}
 lemma power_inverse:
-  "inverse ((a::'a::{field,division_by_zero,recpower}) ^ n) = (inverse a) ^ n"
-apply (induct "n")
-apply (auto simp add: power_Suc inverse_mult_distrib)
-done
+  fixes a :: "'a::{division_ring,division_by_zero,recpower}"
+  shows "inverse (a ^ n) = (inverse a) ^ n"
+apply (cases "a = 0")
+apply (simp add: power_0_left)
+apply (simp add: nonzero_power_inverse)
+done (* TODO: reorient or rename to inverse_power *)
 
 lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = 
     (1 / a)^n"