# HG changeset patch # User huffman # Date 1333024745 -7200 # Node ID 6e53f2a718c21358b3053e68a8aeeb9a427e0cf6 # Parent 9ae03b37b4f647c201121d987acb1147a90bb59d remove unneeded rewrite rules for powers of numerals diff -r 9ae03b37b4f6 -r 6e53f2a718c2 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu Mar 29 14:29:36 2012 +0200 +++ b/src/HOL/Nat_Numeral.thy Thu Mar 29 14:39:05 2012 +0200 @@ -159,15 +159,6 @@ subsection{*Literal arithmetic involving powers*} -(* TODO: replace with more generic rule for powers of numerals *) -lemma power_nat_numeral: - "(numeral v :: nat) ^ n = nat ((numeral v :: int) ^ n)" - by (simp only: nat_power_eq zero_le_numeral nat_numeral) - -lemmas power_nat_numeral_numeral = power_nat_numeral [of _ "numeral w"] for w -declare power_nat_numeral_numeral [simp] - - text{*For arbitrary rings*} lemma power_numeral_even: @@ -184,12 +175,6 @@ lemmas zpower_numeral_even = power_numeral_even [where 'a=int] lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int] -lemmas power_numeral_even_numeral [simp] = - power_numeral_even [of "numeral v"] for v - -lemmas power_numeral_odd_numeral [simp] = - power_numeral_odd [of "numeral v"] for v - lemma nat_numeral_Bit0: "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)" unfolding numeral_Bit0 Let_def ..