src/HOL/Num.thy
changeset 47192 0c0501cb6da6
parent 47191 ebd8c46d156b
child 47207 9368aa814518
     1.1 --- a/src/HOL/Num.thy	Thu Mar 29 11:47:30 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Thu Mar 29 14:09:10 2012 +0200
     1.3 @@ -528,6 +528,12 @@
     1.4    by (induct n,
     1.5      simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
     1.6  
     1.7 +lemma mult_2: "2 * z = z + z"
     1.8 +  unfolding one_add_one [symmetric] left_distrib by simp
     1.9 +
    1.10 +lemma mult_2_right: "z * 2 = z + z"
    1.11 +  unfolding one_add_one [symmetric] right_distrib by simp
    1.12 +
    1.13  end
    1.14  
    1.15  lemma nat_of_num_numeral: "nat_of_num = numeral"
    1.16 @@ -864,6 +870,12 @@
    1.17    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    1.18    by (simp_all add: numeral.simps BitM_plus_one)
    1.19  
    1.20 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    1.21 +  by (simp add: nat_number(2-4))
    1.22 +
    1.23 +lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
    1.24 +  by (simp add: nat_number(2-4))
    1.25 +
    1.26  
    1.27  subsection {* Numeral equations as default simplification rules *}
    1.28