src/HOL/Num.thy
changeset 47207 9368aa814518
parent 47192 0c0501cb6da6
child 47209 4893907fe872
     1.1 --- a/src/HOL/Num.thy	Thu Mar 29 14:47:31 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 08:10:28 2012 +0200
     1.3 @@ -876,6 +876,16 @@
     1.4  lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
     1.5    by (simp add: nat_number(2-4))
     1.6  
     1.7 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
     1.8 +  by (simp only: numeral_One One_nat_def)
     1.9 +
    1.10 +lemma Suc_nat_number_of_add:
    1.11 +  "Suc (numeral v + n) = numeral (v + Num.One) + n"
    1.12 +  by simp
    1.13 +
    1.14 +(*Maps #n to n for n = 1, 2*)
    1.15 +lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
    1.16 +
    1.17  
    1.18  subsection {* Numeral equations as default simplification rules *}
    1.19