745 done |
745 done |
746 |
746 |
747 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a" |
747 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a" |
748 by (simp add: zdiv_zmult1_eq) |
748 by (simp add: zdiv_zmult1_eq) |
749 |
749 |
750 lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)" |
750 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)" |
751 apply (case_tac "b = 0", simp) |
751 apply (case_tac "b = 0", simp) |
752 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) |
752 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) |
753 done |
753 done |
754 |
754 |
755 lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)" |
755 lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)" |
756 apply (case_tac "b = 0", simp) |
756 apply (case_tac "b = 0", simp) |
757 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) |
757 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) |
758 done |
758 done |
759 |
759 |
760 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
760 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} |
773 |
773 |
774 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" |
774 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" |
775 apply (case_tac "c = 0", simp) |
775 apply (case_tac "c = 0", simp) |
776 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) |
776 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod) |
777 done |
777 done |
778 |
|
779 lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1" |
|
780 by (simp add: zdiv_zadd1_eq) |
|
781 |
|
782 lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1" |
|
783 by (simp add: zdiv_zadd1_eq) |
|
784 |
778 |
785 instance int :: semiring_div |
779 instance int :: semiring_div |
786 proof |
780 proof |
787 fix a b c :: int |
781 fix a b c :: int |
788 assume not0: "b \<noteq> 0" |
782 assume not0: "b \<noteq> 0" |
789 show "(a + c * b) div b = c + a div b" |
783 show "(a + c * b) div b = c + a div b" |
790 unfolding zdiv_zadd1_eq [of a "c * b"] using not0 |
784 unfolding zdiv_zadd1_eq [of a "c * b"] using not0 |
791 by (simp add: zmod_zmult1_eq) |
785 by (simp add: zmod_zmult1_eq zmod_zdiv_trivial) |
792 qed auto |
786 qed auto |
793 |
787 |
794 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a" |
788 lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1" |
795 by (subst mult_commute, erule zdiv_zmult_self1) |
789 by (rule div_add_self1) (* already declared [simp] *) |
796 |
790 |
797 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" |
791 lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1" |
798 by (simp add: zmod_zmult1_eq) |
792 by (rule div_add_self2) (* already declared [simp] *) |
799 |
793 |
800 lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)" |
794 lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a" |
801 by (simp add: mult_commute zmod_zmult1_eq) |
795 by (rule div_mult_self1_is_id) (* already declared [simp] *) |
|
796 |
|
797 lemma zmod_zmult_self1: "(a*b) mod b = (0::int)" |
|
798 by (rule mod_mult_self2_is_0) (* already declared [simp] *) |
|
799 |
|
800 lemma zmod_zmult_self2: "(b*a) mod b = (0::int)" |
|
801 by (rule mod_mult_self1_is_0) (* already declared [simp] *) |
802 |
802 |
803 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
803 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
804 proof |
804 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) |
805 assume "m mod d = 0" |
805 |
806 with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto |
806 (* REVISIT: should this be generalized to all semiring_div types? *) |
807 next |
|
808 assume "EX q::int. m = d*q" |
|
809 thus "m mod d = 0" by auto |
|
810 qed |
|
811 |
|
812 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] |
807 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] |
813 |
808 |
814 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" |
809 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" |
815 apply (rule trans [symmetric]) |
810 by (rule mod_add_left_eq) |
816 apply (rule zmod_zadd1_eq, simp) |
|
817 apply (rule zmod_zadd1_eq [symmetric]) |
|
818 done |
|
819 |
811 |
820 lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" |
812 lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" |
821 apply (rule trans [symmetric]) |
813 by (rule mod_add_right_eq) |
822 apply (rule zmod_zadd1_eq, simp) |
814 |
823 apply (rule zmod_zadd1_eq [symmetric]) |
815 lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)" |
824 done |
816 by (rule mod_add_self1) (* already declared [simp] *) |
825 |
817 |
826 lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)" |
818 lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)" |
827 apply (case_tac "a = 0", simp) |
819 by (rule mod_add_self2) (* already declared [simp] *) |
828 apply (simp add: zmod_zadd1_eq) |
|
829 done |
|
830 |
|
831 lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)" |
|
832 apply (case_tac "a = 0", simp) |
|
833 apply (simp add: zmod_zadd1_eq) |
|
834 done |
|
835 |
|
836 |
820 |
837 lemma zmod_zdiff1_eq: fixes a::int |
821 lemma zmod_zdiff1_eq: fixes a::int |
838 shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r") |
822 shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r") |
839 proof - |
823 proof - |
840 have "?l = (c + (a mod c - b mod c)) mod c" |
824 have "?l = (c + (a mod c - b mod c)) mod c" |