# HG changeset patch
# User huffman
# Date 1333103555 -7200
# Node ID 52426c62b5d0a1eb8ee0f4a0f2680759636d0a65
# Parent  172c031ad743c93baebf3433a148707f6a7f2f80
replace lemmas eval_nat_numeral with a simpler reformulation

diff -r 172c031ad743 -r 52426c62b5d0 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 12:02:23 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 12:32:35 2012 +0200
@@ -61,17 +61,6 @@
 lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
 lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
 
-lemma nat_numeral_Bit0:
-  "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)"
-  unfolding numeral_Bit0 Let_def ..
-
-lemma nat_numeral_Bit1:
-  "numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))"
-  unfolding numeral_Bit1 Let_def by simp
-
-lemmas eval_nat_numeral =
-  nat_numeral_Bit0 nat_numeral_Bit1
-
 lemmas nat_arith =
   diff_nat_numeral
 
diff -r 172c031ad743 -r 52426c62b5d0 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 30 12:02:23 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 12:32:35 2012 +0200
@@ -869,8 +869,7 @@
 lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
   unfolding pred_numeral_def by simp
 
-lemma nat_number:
-  "1 = Suc 0"
+lemma eval_nat_numeral:
   "numeral One = Suc 0"
   "numeral (Bit0 n) = Suc (numeral (BitM n))"
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
@@ -880,14 +879,14 @@
   "pred_numeral Num.One = 0"
   "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
   "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
-  unfolding pred_numeral_def nat_number
+  unfolding pred_numeral_def eval_nat_numeral
   by (simp_all only: diff_Suc_Suc diff_0)
 
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
-  by (simp add: nat_number(2-4))
+  by (simp add: eval_nat_numeral)
 
 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
-  by (simp add: nat_number(2-4))
+  by (simp add: eval_nat_numeral)
 
 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
   by (simp only: numeral_One One_nat_def)
diff -r 172c031ad743 -r 52426c62b5d0 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Mar 30 12:02:23 2012 +0200
+++ b/src/HOL/Power.thy	Fri Mar 30 12:32:35 2012 +0200
@@ -185,7 +185,7 @@
 
 lemma power_minus_Bit1:
   "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
-  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
+  by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
 
 lemma power_neg_numeral_Bit0 [simp]:
   "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"