661 apply (auto simp add: zcong_def) |
661 apply (auto simp add: zcong_def) |
662 done |
662 done |
663 |
663 |
664 lemma "[a = b] (mod m) = (a mod m = b mod m)" |
664 lemma "[a = b] (mod m) = (a mod m = b mod m)" |
665 apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO) |
665 apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO) |
666 apply (case_tac "0 < m") |
666 apply (simp add: linorder_neq_iff) |
667 apply (simp add: zcong_zmod_eq) |
667 apply (erule disjE) |
|
668 prefer 2 apply (simp add: zcong_zmod_eq) |
|
669 txt{*Remainding case: @{term "m<0"}*} |
668 apply (rule_tac t = m in zminus_zminus [THEN subst]) |
670 apply (rule_tac t = m in zminus_zminus [THEN subst]) |
669 apply (subst zcong_zminus) |
671 apply (subst zcong_zminus) |
670 apply (subst zcong_zmod_eq) |
672 apply (subst zcong_zmod_eq) |
671 apply arith |
673 apply arith |
672 oops -- {* FIXME: finish this proof? *} |
674 apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) |
673 |
675 apply (simp add: zmod_zminus2_eq_if) |
|
676 done |
674 |
677 |
675 subsection {* Modulo *} |
678 subsection {* Modulo *} |
676 |
679 |
677 lemma zmod_zdvd_zmod: |
680 lemma zmod_zdvd_zmod: |
678 "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" |
681 "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" |