626 next |
626 next |
627 case False then have "a * 0 div a = 0" |
627 case False then have "a * 0 div a = 0" |
628 by (rule nonzero_mult_divide_cancel_left) |
628 by (rule nonzero_mult_divide_cancel_left) |
629 then show ?thesis by simp |
629 then show ?thesis by simp |
630 qed |
630 qed |
|
631 |
|
632 lemma divide_1 [simp]: |
|
633 "a div 1 = a" |
|
634 using nonzero_mult_divide_cancel_left [of 1 a] by simp |
|
635 |
|
636 lemma dvd_times_left_cancel_iff [simp]: |
|
637 assumes "a \<noteq> 0" |
|
638 shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") |
|
639 proof |
|
640 assume ?P then obtain d where "a * c = a * b * d" .. |
|
641 with assms have "c = b * d" by (simp add: ac_simps) |
|
642 then show ?Q .. |
|
643 next |
|
644 assume ?Q then obtain d where "c = b * d" .. |
|
645 then have "a * c = a * b * d" by (simp add: ac_simps) |
|
646 then show ?P .. |
|
647 qed |
|
648 |
|
649 lemma dvd_times_right_cancel_iff [simp]: |
|
650 assumes "a \<noteq> 0" |
|
651 shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q") |
|
652 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) |
|
653 |
|
654 lemma div_dvd_iff_mult: |
|
655 assumes "b \<noteq> 0" and "b dvd a" |
|
656 shows "a div b dvd c \<longleftrightarrow> a dvd c * b" |
|
657 proof - |
|
658 from \<open>b dvd a\<close> obtain d where "a = b * d" .. |
|
659 with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps) |
|
660 qed |
|
661 |
|
662 lemma dvd_div_iff_mult: |
|
663 assumes "c \<noteq> 0" and "c dvd b" |
|
664 shows "a dvd b div c \<longleftrightarrow> a * c dvd b" |
|
665 proof - |
|
666 from \<open>c dvd b\<close> obtain d where "b = c * d" .. |
|
667 with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a]) |
|
668 qed |
631 |
669 |
632 end |
670 end |
633 |
671 |
634 class idom_divide = idom + semidom_divide |
672 class idom_divide = idom + semidom_divide |
635 |
673 |