# Theory Divides

(*  Title:      HOL/Divides.thy
*)

section ‹Misc lemmas on division, to be sorted out finally›

theory Divides
imports Parity
begin

class unique_euclidean_semiring_numeral = linordered_euclidean_semiring + discrete_linordered_semidom +
assumes div_less [no_atp]: "0  a  a < b  a div b = 0"
and mod_less [no_atp]: " 0  a  a < b  a mod b = a"
and div_positive [no_atp]: "0 < b  b  a  a div b > 0"
and mod_less_eq_dividend [no_atp]: "0  a  a mod b  a"
and pos_mod_bound [no_atp]: "0 < b  a mod b < b"
and pos_mod_sign [no_atp]: "0 < b  0  a mod b"
and mod_mult2_eq [no_atp]: "0  c  a mod (b * c) = b * (a div b mod c) + a mod b"
and div_mult2_eq [no_atp]: "0  c  a div (b * c) = a div b div c"

hide_fact (open) div_less mod_less div_positive mod_less_eq_dividend pos_mod_bound pos_mod_sign mod_mult2_eq div_mult2_eq

context unique_euclidean_semiring_numeral
begin

context
begin

qualified lemma discrete [no_atp]:
"a < b  a + 1  b"
by (fact less_iff_succ_less_eq)

qualified lemma divmod_digit_1 [no_atp]:
assumes "0  a" "0 < b" and "b  a mod (2 * b)"
shows "2 * (a div (2 * b)) + 1 = a div b" (is "?P")
and "a mod (2 * b) - b = a mod b" (is "?Q")
proof -
from assms mod_less_eq_dividend [of a "2 * b"] have "b  a"
by (auto intro: trans)
with 0 < b have "0 < a div b" by (auto intro: div_positive)
then have [simp]: "1  a div b" by (simp add: discrete)
with 0 < b have mod_less: "a mod b < b" by (simp add: pos_mod_bound)
define w where "w = a div b mod 2"
then have w_exhaust: "w = 0  w = 1" by auto
have mod_w: "a mod (2 * b) = a mod b + b * w"
by (simp add: w_def mod_mult2_eq ac_simps)
from assms w_exhaust have "w = 1"
using mod_less by (auto simp add: mod_w)
with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
have "2 * (a div (2 * b)) = a div b - w"
by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
with w = 1 have div: "2 * (a div (2 * b)) = a div b - 1" by simp
then show ?P and ?Q
qed

qualified lemma divmod_digit_0 [no_atp]:
assumes "0 < b" and "a mod (2 * b) < b"
shows "2 * (a div (2 * b)) = a div b" (is "?P")
and "a mod (2 * b) = a mod b" (is "?Q")
proof -
define w where "w = a div b mod 2"
then have w_exhaust: "w = 0  w = 1" by auto
have mod_w: "a mod (2 * b) = a mod b + b * w"
by (simp add: w_def mod_mult2_eq ac_simps)
moreover have "b  a mod b + b"
proof -
from 0 < b pos_mod_sign have "0  a mod b" by blast
then have "0 + b  a mod b + b" by (rule add_right_mono)
then show ?thesis by simp
qed
moreover note assms w_exhaust
ultimately have "w = 0" by auto
with mod_w have mod: "a mod (2 * b) = a mod b" by simp
have "2 * (a div (2 * b)) = a div b - w"
by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
with w = 0 have div: "2 * (a div (2 * b)) = a div b" by simp
then show ?P and ?Q
qed

qualified lemma mod_double_modulus [no_atp]:
assumes "m > 0" "x  0"
shows   "x mod (2 * m) = x mod m  x mod (2 * m) = x mod m + m"
proof (cases "x mod (2 * m) < m")
case True
thus ?thesis using assms using divmod_digit_0(2)[of m x] by auto
next
case False
hence *: "x mod (2 * m) - m = x mod m"
using assms by (intro divmod_digit_1) auto
hence "x mod (2 * m) = x mod m + m"
by (subst * [symmetric], subst le_add_diff_inverse2) (use False in auto)
thus ?thesis by simp
qed

end

end

instance nat :: unique_euclidean_semiring_numeral
by standard
(auto simp add: div_greater_zero_iff div_mult2_eq mod_mult2_eq)

instance int :: unique_euclidean_semiring_numeral
by standard (auto intro: zmod_le_nonneg_dividend simp add:
pos_imp_zdiv_pos_iff zmod_zmult2_eq zdiv_zmult2_eq)

context
begin

(* REVISIT: should this be generalized to all semiring_div types? *)
qualified lemma zmod_eq_0D [dest!]: "q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto

qualified lemma div_geq [no_atp]: "m div n = Suc ((m - n) div n)" if "0 < n" and " ¬ m < n" for m n :: nat
by (rule le_div_geq) (use that in simp_all add: not_less)

qualified lemma mod_geq [no_atp]: "m mod n = (m - n) mod n" if "¬ m < n" for m n :: nat
by (rule le_mod_geq) (use that in simp add: not_less)

qualified lemma mod_eq_0D [no_atp]: "q. m = d * q" if "m mod d = 0" for m d :: nat
using that by (auto simp add: mod_eq_0_iff_dvd)

qualified lemma pos_mod_conj [no_atp]: "0 < b  0  a mod b  a mod b < b" for a b :: int
by simp

qualified lemma neg_mod_conj [no_atp]: "b < 0  a mod b  0  b < a mod b" for a b :: int
by simp

qualified lemma zmod_eq_0_iff [no_atp]: "m mod d = 0  (q. m = d * q)" for m d :: int