equal
deleted
inserted
replaced
460 lemma div_minus_right: "a div (-b) = (-a) div b" |
460 lemma div_minus_right: "a div (-b) = (-a) div b" |
461 using div_minus_minus [of "-a" b] by simp |
461 using div_minus_minus [of "-a" b] by simp |
462 |
462 |
463 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)" |
463 lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)" |
464 using mod_minus_minus [of "-a" b] by simp |
464 using mod_minus_minus [of "-a" b] by simp |
|
465 |
|
466 lemma div_minus1_right [simp]: "a div (-1) = -a" |
|
467 using div_minus_right [of a 1] by simp |
|
468 |
|
469 lemma mod_minus1_right [simp]: "a mod (-1) = 0" |
|
470 using mod_minus_right [of a 1] by simp |
465 |
471 |
466 end |
472 end |
467 |
473 |
468 |
474 |
469 subsection {* Division on @{typ nat} *} |
475 subsection {* Division on @{typ nat} *} |
1659 negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w |
1665 negDivAlg_eqn [of "numeral v" "neg_numeral w", OF zero_less_numeral] for v w |
1660 |
1666 |
1661 |
1667 |
1662 text{*Special-case simplification *} |
1668 text{*Special-case simplification *} |
1663 |
1669 |
1664 lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" |
|
1665 apply (cut_tac a = a and b = "-1" in neg_mod_sign) |
|
1666 apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound) |
|
1667 apply (auto simp del: neg_mod_sign neg_mod_bound) |
|
1668 done (* FIXME: generalize *) |
|
1669 |
|
1670 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a" |
|
1671 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto) |
|
1672 (* FIXME: generalize *) |
|
1673 |
|
1674 (** The last remaining special cases for constant arithmetic: |
1670 (** The last remaining special cases for constant arithmetic: |
1675 1 div z and 1 mod z **) |
1671 1 div z and 1 mod z **) |
1676 |
1672 |
1677 lemmas div_pos_pos_1_numeral [simp] = |
1673 lemmas div_pos_pos_1_numeral [simp] = |
1678 div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w |
1674 div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w |