equal
deleted
inserted
replaced
527 done |
527 done |
528 |
528 |
529 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)" |
529 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)" |
530 by (rule numeral_mult [symmetric]) |
530 by (rule numeral_mult [symmetric]) |
531 |
531 |
|
532 lemma mult_2: "2 * z = z + z" |
|
533 unfolding one_add_one [symmetric] distrib_right by simp |
|
534 |
|
535 lemma mult_2_right: "z * 2 = z + z" |
|
536 unfolding one_add_one [symmetric] distrib_left by simp |
|
537 |
532 end |
538 end |
533 |
539 |
534 subsubsection {* |
540 subsubsection {* |
535 Structures with a zero: class @{text semiring_1} |
541 Structures with a zero: class @{text semiring_1} |
536 *} |
542 *} |
541 subclass semiring_numeral .. |
547 subclass semiring_numeral .. |
542 |
548 |
543 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
549 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
544 by (induct n, |
550 by (induct n, |
545 simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
551 simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
546 |
|
547 lemma mult_2: "2 * z = z + z" |
|
548 unfolding one_add_one [symmetric] distrib_right by simp |
|
549 |
|
550 lemma mult_2_right: "z * 2 = z + z" |
|
551 unfolding one_add_one [symmetric] distrib_left by simp |
|
552 |
552 |
553 end |
553 end |
554 |
554 |
555 lemma nat_of_num_numeral [code_abbrev]: |
555 lemma nat_of_num_numeral [code_abbrev]: |
556 "nat_of_num = numeral" |
556 "nat_of_num = numeral" |