# 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);