# HG changeset patch
# User huffman
# Date 1308783535 25200
# Node ID 2b92a6943915c3d63ae94520b7e0ca3e08d8c061
# Parent  8f28a91ea135f0f7581450094b4c565251d6dfd0
generalize lemmas power_number_of_even and power_number_of_odd

diff -r 8f28a91ea135 -r 2b92a6943915 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Wed Jun 22 13:45:32 2011 -0700
+++ b/src/HOL/Nat_Numeral.thy	Wed Jun 22 15:58:55 2011 -0700
@@ -647,13 +647,13 @@
 text{*For arbitrary rings*}
 
 lemma power_number_of_even:
-  fixes z :: "'a::number_ring"
+  fixes z :: "'a::monoid_mult"
   shows "z ^ number_of (Int.Bit0 w) = (let w = z ^ (number_of w) in w * w)"
 by (cases "w \<ge> 0") (auto simp add: Let_def Bit0_def nat_number_of_def number_of_is_id
   nat_add_distrib power_add simp del: nat_number_of)
 
 lemma power_number_of_odd:
-  fixes z :: "'a::number_ring"
+  fixes z :: "'a::monoid_mult"
   shows "z ^ number_of (Int.Bit1 w) = (if (0::int) <= number_of w
      then (let w = z ^ (number_of w) in z * w * w) else 1)"
 unfolding Let_def Bit1_def nat_number_of_def number_of_is_id