diff -r ebd8c46d156b -r 0c0501cb6da6 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Mar 29 11:47:30 2012 +0200
+++ b/src/HOL/Num.thy	Thu Mar 29 14:09:10 2012 +0200
@@ -528,6 +528,12 @@
   by (induct n,
     simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1)
 
+lemma mult_2: "2 * z = z + z"
+  unfolding one_add_one [symmetric] left_distrib by simp
+
+lemma mult_2_right: "z * 2 = z + z"
+  unfolding one_add_one [symmetric] right_distrib by simp
+
 end
 
 lemma nat_of_num_numeral: "nat_of_num = numeral"
@@ -864,6 +870,12 @@
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   by (simp_all add: numeral.simps BitM_plus_one)
 
+lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
+  by (simp add: nat_number(2-4))
+
+lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
+  by (simp add: nat_number(2-4))
+
 
 subsection {* Numeral equations as default simplification rules *}