replace lemmas eval_nat_numeral with a simpler reformulation
authorhuffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 4722052426c62b5d0
parent 47219 172c031ad743
child 47221 7205eb4a0a05
replace lemmas eval_nat_numeral with a simpler reformulation
src/HOL/Nat_Numeral.thy
src/HOL/Num.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 12:02:23 2012 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 12:32:35 2012 +0200
     1.3 @@ -61,17 +61,6 @@
     1.4  lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
     1.5  lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
     1.6  
     1.7 -lemma nat_numeral_Bit0:
     1.8 -  "numeral (Num.Bit0 w) = (let n::nat = numeral w in n + n)"
     1.9 -  unfolding numeral_Bit0 Let_def ..
    1.10 -
    1.11 -lemma nat_numeral_Bit1:
    1.12 -  "numeral (Num.Bit1 w) = (let n = numeral w in Suc (n + n))"
    1.13 -  unfolding numeral_Bit1 Let_def by simp
    1.14 -
    1.15 -lemmas eval_nat_numeral =
    1.16 -  nat_numeral_Bit0 nat_numeral_Bit1
    1.17 -
    1.18  lemmas nat_arith =
    1.19    diff_nat_numeral
    1.20  
     2.1 --- a/src/HOL/Num.thy	Fri Mar 30 12:02:23 2012 +0200
     2.2 +++ b/src/HOL/Num.thy	Fri Mar 30 12:32:35 2012 +0200
     2.3 @@ -869,8 +869,7 @@
     2.4  lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
     2.5    unfolding pred_numeral_def by simp
     2.6  
     2.7 -lemma nat_number:
     2.8 -  "1 = Suc 0"
     2.9 +lemma eval_nat_numeral:
    2.10    "numeral One = Suc 0"
    2.11    "numeral (Bit0 n) = Suc (numeral (BitM n))"
    2.12    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    2.13 @@ -880,14 +879,14 @@
    2.14    "pred_numeral Num.One = 0"
    2.15    "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
    2.16    "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
    2.17 -  unfolding pred_numeral_def nat_number
    2.18 +  unfolding pred_numeral_def eval_nat_numeral
    2.19    by (simp_all only: diff_Suc_Suc diff_0)
    2.20  
    2.21  lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    2.22 -  by (simp add: nat_number(2-4))
    2.23 +  by (simp add: eval_nat_numeral)
    2.24  
    2.25  lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    2.26 -  by (simp add: nat_number(2-4))
    2.27 +  by (simp add: eval_nat_numeral)
    2.28  
    2.29  lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    2.30    by (simp only: numeral_One One_nat_def)
     3.1 --- a/src/HOL/Power.thy	Fri Mar 30 12:02:23 2012 +0200
     3.2 +++ b/src/HOL/Power.thy	Fri Mar 30 12:32:35 2012 +0200
     3.3 @@ -185,7 +185,7 @@
     3.4  
     3.5  lemma power_minus_Bit1:
     3.6    "(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))"
     3.7 -  by (simp only: nat_number(4) power_Suc power_minus_Bit0 mult_minus_left)
     3.8 +  by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left)
     3.9  
    3.10  lemma power_neg_numeral_Bit0 [simp]:
    3.11    "neg_numeral k ^ numeral (Num.Bit0 l) = numeral (Num.pow k (Num.Bit0 l))"