equal
deleted
inserted
replaced
710 apply (rule zdiv_mono2_neg_lemma) |
710 apply (rule zdiv_mono2_neg_lemma) |
711 apply (erule subst) |
711 apply (erule subst) |
712 apply (erule subst, simp_all) |
712 apply (erule subst, simp_all) |
713 done |
713 done |
714 |
714 |
|
715 |
715 subsection{*More Algebraic Laws for div and mod*} |
716 subsection{*More Algebraic Laws for div and mod*} |
716 |
717 |
717 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} |
718 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *} |
718 |
719 |
719 lemma zmult1_lemma: |
720 lemma zmult1_lemma: |
743 apply (rule zmod_zmult1_eq) |
744 apply (rule zmod_zmult1_eq) |
744 done |
745 done |
745 |
746 |
746 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" |
747 by (simp add: zdiv_zmult1_eq) |
748 by (simp add: zdiv_zmult1_eq) |
|
749 |
|
750 instance int :: semiring_div |
|
751 by intro_classes auto |
748 |
752 |
749 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a" |
753 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a" |
750 by (subst mult_commute, erule zdiv_zmult_self1) |
754 by (subst mult_commute, erule zdiv_zmult_self1) |
751 |
755 |
752 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" |
756 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)" |
1051 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
1055 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") |
1052 apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], |
1056 apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric], |
1053 simp) |
1057 simp) |
1054 done |
1058 done |
1055 |
1059 |
1056 |
|
1057 (*Not clear why this must be proved separately; probably number_of causes |
1060 (*Not clear why this must be proved separately; probably number_of causes |
1058 simplification problems*) |
1061 simplification problems*) |
1059 lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)" |
1062 lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)" |
1060 by auto |
1063 by auto |
1061 |
1064 |
1149 |
1152 |
1150 subsection {* The Divides Relation *} |
1153 subsection {* The Divides Relation *} |
1151 |
1154 |
1152 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1155 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
1153 by (simp add: dvd_def zmod_eq_0_iff) |
1156 by (simp add: dvd_def zmod_eq_0_iff) |
1154 |
|
1155 instance int :: dvd_mod |
|
1156 by default (simp add: zdvd_iff_zmod_eq_0) |
|
1157 |
1157 |
1158 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1158 lemmas zdvd_iff_zmod_eq_0_number_of [simp] = |
1159 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1159 zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] |
1160 |
1160 |
1161 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |
1161 lemma zdvd_0_right [iff]: "(m::int) dvd 0" |