equal
deleted
inserted
replaced
526 |
526 |
527 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
527 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
528 by (induct n, |
528 by (induct n, |
529 simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
529 simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
530 |
530 |
|
531 lemma mult_2: "2 * z = z + z" |
|
532 unfolding one_add_one [symmetric] left_distrib by simp |
|
533 |
|
534 lemma mult_2_right: "z * 2 = z + z" |
|
535 unfolding one_add_one [symmetric] right_distrib by simp |
|
536 |
531 end |
537 end |
532 |
538 |
533 lemma nat_of_num_numeral: "nat_of_num = numeral" |
539 lemma nat_of_num_numeral: "nat_of_num = numeral" |
534 proof |
540 proof |
535 fix n |
541 fix n |
862 "numeral One = Suc 0" |
868 "numeral One = Suc 0" |
863 "numeral (Bit0 n) = Suc (numeral (BitM n))" |
869 "numeral (Bit0 n) = Suc (numeral (BitM n))" |
864 "numeral (Bit1 n) = Suc (numeral (Bit0 n))" |
870 "numeral (Bit1 n) = Suc (numeral (Bit0 n))" |
865 by (simp_all add: numeral.simps BitM_plus_one) |
871 by (simp_all add: numeral.simps BitM_plus_one) |
866 |
872 |
|
873 lemma numeral_2_eq_2: "2 = Suc (Suc 0)" |
|
874 by (simp add: nat_number(2-4)) |
|
875 |
|
876 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))" |
|
877 by (simp add: nat_number(2-4)) |
|
878 |
867 |
879 |
868 subsection {* Numeral equations as default simplification rules *} |
880 subsection {* Numeral equations as default simplification rules *} |
869 |
881 |
870 declare (in numeral) numeral_One [simp] |
882 declare (in numeral) numeral_One [simp] |
871 declare (in numeral) numeral_plus_numeral [simp] |
883 declare (in numeral) numeral_plus_numeral [simp] |