836 done |
836 done |
837 |
837 |
838 |
838 |
839 subsubsection \<open>More Algebraic Laws for div and mod\<close> |
839 subsubsection \<open>More Algebraic Laws for div and mod\<close> |
840 |
840 |
841 text\<open>proving (a*b) div c = a * (b div c) + a * (b mod c)\<close> |
|
842 |
|
843 lemma zmult1_lemma: |
|
844 "[| eucl_rel_int b c (q, r) |] |
|
845 ==> eucl_rel_int (a * b) c (a*q + a*r div c, a*r mod c)" |
|
846 by (auto simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left ac_simps) |
|
847 |
|
848 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
841 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)" |
849 apply (case_tac "c = 0", simp) |
842 by (fact div_mult1_eq) |
850 apply (blast intro: eucl_rel_int [THEN zmult1_lemma, THEN div_int_unique]) |
|
851 done |
|
852 |
|
853 text\<open>proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c)\<close> |
|
854 |
|
855 lemma zadd1_lemma: |
|
856 "[| eucl_rel_int a c (aq, ar); eucl_rel_int b c (bq, br) |] |
|
857 ==> eucl_rel_int (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)" |
|
858 by (force simp add: split_ifs eucl_rel_int_iff linorder_neq_iff distrib_left) |
|
859 |
843 |
860 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
844 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
861 lemma zdiv_zadd1_eq: |
845 lemma zdiv_zadd1_eq: |
862 "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" |
846 "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)" |
863 apply (case_tac "c = 0", simp) |
847 by (fact div_add1_eq) |
864 apply (blast intro: zadd1_lemma [OF eucl_rel_int eucl_rel_int] div_int_unique) |
|
865 done |
|
866 |
848 |
867 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
849 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" |
868 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) |
850 by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) |
869 |
851 |
870 (* REVISIT: should this be generalized to all semiring_div types? *) |
852 (* REVISIT: should this be generalized to all semiring_div types? *) |