1791 unfolding divmod_int_rel_def by (auto simp: algebra_simps) |
1791 unfolding divmod_int_rel_def by (auto simp: algebra_simps) |
1792 thus "(a + c * b) div b = c + a div b" |
1792 thus "(a + c * b) div b = c + a div b" |
1793 by (rule div_int_unique) |
1793 by (rule div_int_unique) |
1794 next |
1794 next |
1795 fix a b c :: int |
1795 fix a b c :: int |
1796 assume "c \<noteq> 0" |
1796 assume c: "c \<noteq> 0" |
1797 hence "\<And>q r. divmod_int_rel a b (q, r) |
1797 have "\<And>q r. divmod_int_rel a b (q, r) |
1798 \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)" |
1798 \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)" |
1799 unfolding divmod_int_rel_def |
1799 unfolding divmod_int_rel_def |
1800 by - (rule linorder_cases [of 0 b], auto simp: algebra_simps |
1800 by (rule linorder_cases [of 0 b]) |
|
1801 (use c in \<open>auto simp: algebra_simps |
1801 mult_less_0_iff zero_less_mult_iff mult_strict_right_mono |
1802 mult_less_0_iff zero_less_mult_iff mult_strict_right_mono |
1802 mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff) |
1803 mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>) |
1803 hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))" |
1804 hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))" |
1804 using divmod_int_rel [of a b] . |
1805 using divmod_int_rel [of a b] . |
1805 thus "(c * a) div (c * b) = a div b" |
1806 thus "(c * a) div (c * b) = a div b" |
1806 by (rule div_int_unique) |
1807 by (rule div_int_unique) |
1807 next |
1808 next |