# HG changeset patch
# User huffman
# Date 1181265867 -7200
# Node ID 9302a50a5bc9f3917a09f1903ccdf8f9177ac5ac
# Parent  77577fc2f14108b272b25b5b8c6c28b65b276f4e
generalize zpower_number_of_{even,odd} lemmas

diff -r 77577fc2f141 -r 9302a50a5bc9 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Jun 07 17:21:43 2007 +0200
+++ b/src/HOL/NatBin.thy	Fri Jun 08 03:24:27 2007 +0200
@@ -617,34 +617,36 @@
 
 
 
-text{*For the integers*}
+text{*For arbitrary rings*}
 
-lemma zpower_number_of_even:
-  "(z::int) ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
+lemma power_number_of_even:
+  fixes z :: "'a::{number_ring,recpower}"
+  shows "z ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
 unfolding Let_def nat_number_of_def number_of_BIT bit.cases
 apply (rule_tac x = "number_of w" in spec, clarify)
 apply (case_tac " (0::int) <= x")
 apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
 done
 
-lemma zpower_number_of_odd:
-  "(z::int) ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w                    
+lemma power_number_of_odd:
+  fixes z :: "'a::{number_ring,recpower}"
+  shows "z ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w
      then (let w = z ^ (number_of w) in z * w * w) else 1)"
 unfolding Let_def nat_number_of_def number_of_BIT bit.cases
 apply (rule_tac x = "number_of w" in spec, auto)
 apply (simp only: nat_add_distrib nat_mult_distrib)
 apply simp
-apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
+apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat power_Suc)
 done
 
-lemmas zpower_number_of_even_number_of =
-    zpower_number_of_even [of "number_of v", standard]
-declare zpower_number_of_even_number_of [simp]
+lemmas zpower_number_of_even = power_number_of_even [where 'a=int]
+lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
 
-lemmas zpower_number_of_odd_number_of =
-    zpower_number_of_odd [of "number_of v", standard]
-declare zpower_number_of_odd_number_of [simp]
+lemmas power_number_of_even_number_of [simp] =
+    power_number_of_even [of "number_of v", standard]
 
+lemmas power_number_of_odd_number_of [simp] =
+    power_number_of_odd [of "number_of v", standard]
 
 
 
@@ -709,7 +711,7 @@
   by (simp add: Let_def)
 
 lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
-by (simp add: power_mult); 
+by (simp add: power_mult power_Suc); 
 
 lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
 by (simp add: power_mult power_Suc);