1401 next |
1401 next |
1402 fix a :: int show "0 div a = 0" |
1402 fix a :: int show "0 div a = 0" |
1403 by (rule div_int_unique, auto simp add: divmod_int_rel_def) |
1403 by (rule div_int_unique, auto simp add: divmod_int_rel_def) |
1404 qed |
1404 qed |
1405 |
1405 |
1406 text{*Arbitrary definitions for division by zero. Useful to simplify |
|
1407 certain equations.*} |
|
1408 |
|
1409 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a" |
|
1410 by simp (* FIXME: delete *) |
|
1411 |
|
1412 text{*Basic laws about division and remainder*} |
1406 text{*Basic laws about division and remainder*} |
1413 |
1407 |
1414 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
1408 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" |
1415 by (fact mod_div_equality2 [symmetric]) |
1409 by (fact mod_div_equality2 [symmetric]) |
1416 |
1410 |
1550 fixes k l :: int |
1544 fixes k l :: int |
1551 shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" |
1545 shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0" |
1552 unfolding zmod_zminus2_eq_if by auto |
1546 unfolding zmod_zminus2_eq_if by auto |
1553 |
1547 |
1554 |
1548 |
1555 subsubsection {* Division of a Number by Itself *} |
|
1556 |
|
1557 lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q" |
|
1558 apply (subgoal_tac "0 < a*q") |
|
1559 apply (simp add: zero_less_mult_iff, arith) |
|
1560 done |
|
1561 |
|
1562 lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1" |
|
1563 apply (subgoal_tac "0 \<le> a* (1-q) ") |
|
1564 apply (simp add: zero_le_mult_iff) |
|
1565 apply (simp add: right_diff_distrib) |
|
1566 done |
|
1567 |
|
1568 lemma self_quotient: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> q = 1" |
|
1569 apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff) |
|
1570 apply (rule order_antisym, safe, simp_all) |
|
1571 apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) |
|
1572 apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2) |
|
1573 apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ |
|
1574 done |
|
1575 |
|
1576 lemma self_remainder: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> r = 0" |
|
1577 apply (frule (1) self_quotient) |
|
1578 apply (simp add: divmod_int_rel_def) |
|
1579 done |
|
1580 |
|
1581 lemma zdiv_self [simp]: "a \<noteq> 0 ==> a div a = (1::int)" |
|
1582 by (fact div_self) (* FIXME: delete *) |
|
1583 |
|
1584 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
|
1585 lemma zmod_self [simp]: "a mod a = (0::int)" |
|
1586 by (fact mod_self) (* FIXME: delete *) |
|
1587 |
|
1588 |
|
1589 subsubsection {* Computation of Division and Remainder *} |
1549 subsubsection {* Computation of Division and Remainder *} |
1590 |
|
1591 lemma zdiv_zero [simp]: "(0::int) div b = 0" |
|
1592 by (fact div_0) (* FIXME: delete *) |
|
1593 |
1550 |
1594 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
1551 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1" |
1595 by (simp add: div_int_def divmod_int_def) |
1552 by (simp add: div_int_def divmod_int_def) |
1596 |
|
1597 lemma zmod_zero [simp]: "(0::int) mod b = 0" |
|
1598 by (fact mod_0) (* FIXME: delete *) |
|
1599 |
1553 |
1600 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
1554 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" |
1601 by (simp add: mod_int_def divmod_int_def) |
1555 by (simp add: mod_int_def divmod_int_def) |
1602 |
1556 |
1603 text{*a positive, b positive *} |
1557 text{*a positive, b positive *} |
1839 done |
1793 done |
1840 |
1794 |
1841 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
1795 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)" |
1842 by (fact mod_mult_right_eq) (* FIXME: delete *) |
1796 by (fact mod_mult_right_eq) (* FIXME: delete *) |
1843 |
1797 |
1844 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)" |
|
1845 by (fact mod_div_trivial) (* FIXME: delete *) |
|
1846 |
|
1847 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
1798 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
1848 |
1799 |
1849 lemma zadd1_lemma: |
1800 lemma zadd1_lemma: |
1850 "[| divmod_int_rel a c (aq, ar); divmod_int_rel b c (bq, br) |] |
1801 "[| divmod_int_rel a c (aq, ar); divmod_int_rel b c (bq, br) |] |
1851 ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" |
1802 ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" |
2233 |
2184 |
2234 subsubsection {* Further properties *} |
2185 subsubsection {* Further properties *} |
2235 |
2186 |
2236 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)" |
2187 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)" |
2237 using zmod_zdiv_equality[where a="m" and b="n"] |
2188 using zmod_zdiv_equality[where a="m" and b="n"] |
2238 by (simp add: algebra_simps) |
2189 by (simp add: algebra_simps) (* FIXME: generalize *) |
2239 |
2190 |
2240 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
2191 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m" |
2241 apply (induct "y", auto) |
2192 apply (induct "y", auto) |
2242 apply (rule zmod_zmult1_eq [THEN trans]) |
2193 apply (rule mod_mult_right_eq [THEN trans]) |
2243 apply (simp (no_asm_simp)) |
2194 apply (simp (no_asm_simp)) |
2244 apply (rule mod_mult_eq [symmetric]) |
2195 apply (rule mod_mult_eq [symmetric]) |
2245 done |
2196 done (* FIXME: generalize *) |
2246 |
2197 |
2247 lemma zdiv_int: "int (a div b) = (int a) div (int b)" |
2198 lemma zdiv_int: "int (a div b) = (int a) div (int b)" |
2248 apply (subst split_div, auto) |
2199 apply (subst split_div, auto) |
2249 apply (subst split_zdiv, auto) |
2200 apply (subst split_zdiv, auto) |
2250 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient) |
2201 apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in unique_quotient) |
2288 by (rule mod_diff_right_eq [symmetric]) |
2239 by (rule mod_diff_right_eq [symmetric]) |
2289 |
2240 |
2290 lemmas zmod_simps = |
2241 lemmas zmod_simps = |
2291 mod_add_left_eq [symmetric] |
2242 mod_add_left_eq [symmetric] |
2292 mod_add_right_eq [symmetric] |
2243 mod_add_right_eq [symmetric] |
2293 zmod_zmult1_eq [symmetric] |
2244 mod_mult_right_eq[symmetric] |
2294 mod_mult_left_eq [symmetric] |
2245 mod_mult_left_eq [symmetric] |
2295 zpower_zmod |
2246 zpower_zmod |
2296 zminus_zmod zdiff_zmod_left zdiff_zmod_right |
2247 zminus_zmod zdiff_zmod_left zdiff_zmod_right |
2297 |
2248 |
2298 text {* Distributive laws for function @{text nat}. *} |
2249 text {* Distributive laws for function @{text nat}. *} |