equal
deleted
inserted
replaced
1662 by (subst posDivAlg.simps, auto) |
1662 by (subst posDivAlg.simps, auto) |
1663 |
1663 |
1664 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)" |
1664 lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)" |
1665 by (subst posDivAlg.simps, auto) |
1665 by (subst posDivAlg.simps, auto) |
1666 |
1666 |
1667 lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)" |
1667 lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)" |
1668 by (subst negDivAlg.simps, auto) |
1668 by (subst negDivAlg.simps, auto) |
1669 |
1669 |
1670 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)" |
1670 lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)" |
1671 by (auto simp add: divmod_int_rel_def) |
1671 by (auto simp add: divmod_int_rel_def) |
1672 |
1672 |