src/HOL/Num.thy
changeset 47220 52426c62b5d0
parent 47218 2b652cbadde1
child 47226 ea712316fc87
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 12:02:23 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 12:32:35 2012 +0200
     1.3 @@ -869,8 +869,7 @@
     1.4  lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
     1.5    unfolding pred_numeral_def by simp
     1.6  
     1.7 -lemma nat_number:
     1.8 -  "1 = Suc 0"
     1.9 +lemma eval_nat_numeral:
    1.10    "numeral One = Suc 0"
    1.11    "numeral (Bit0 n) = Suc (numeral (BitM n))"
    1.12    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    1.13 @@ -880,14 +879,14 @@
    1.14    "pred_numeral Num.One = 0"
    1.15    "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
    1.16    "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
    1.17 -  unfolding pred_numeral_def nat_number
    1.18 +  unfolding pred_numeral_def eval_nat_numeral
    1.19    by (simp_all only: diff_Suc_Suc diff_0)
    1.20  
    1.21  lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    1.22 -  by (simp add: nat_number(2-4))
    1.23 +  by (simp add: eval_nat_numeral)
    1.24  
    1.25  lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    1.26 -  by (simp add: nat_number(2-4))
    1.27 +  by (simp add: eval_nat_numeral)
    1.28  
    1.29  lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    1.30    by (simp only: numeral_One One_nat_def)