equal
deleted
inserted
replaced
640 Goal "(b*a) mod b = (#0::int)"; |
640 Goal "(b*a) mod b = (#0::int)"; |
641 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
641 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
642 qed "zmod_zmult_self2"; |
642 qed "zmod_zmult_self2"; |
643 |
643 |
644 Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
644 Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
|
645 |
|
646 Goal "(m mod d = #0) = (EX q::int. m = d*q)"; |
|
647 by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1); |
|
648 by Auto_tac; |
|
649 qed "zmod_eq_0_iff"; |
|
650 AddSDs [zmod_eq_0_iff RS iffD1]; |
645 |
651 |
646 |
652 |
647 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
653 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
648 |
654 |
649 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= #0 |] \ |
655 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= #0 |] \ |