diff -r 179ff9cb160b -r 5b25fee0362c src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Mar 04 10:43:39 2009 +0100 +++ b/src/HOL/IntDiv.thy Wed Mar 04 10:45:52 2009 +0100 @@ -547,34 +547,6 @@ simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *} -(* The following 8 lemmas are made unnecessary by the above simprocs: *) - -lemmas div_pos_pos_number_of = - div_pos_pos [of "number_of v" "number_of w", standard] - -lemmas div_neg_pos_number_of = - div_neg_pos [of "number_of v" "number_of w", standard] - -lemmas div_pos_neg_number_of = - div_pos_neg [of "number_of v" "number_of w", standard] - -lemmas div_neg_neg_number_of = - div_neg_neg [of "number_of v" "number_of w", standard] - - -lemmas mod_pos_pos_number_of = - mod_pos_pos [of "number_of v" "number_of w", standard] - -lemmas mod_neg_pos_number_of = - mod_neg_pos [of "number_of v" "number_of w", standard] - -lemmas mod_pos_neg_number_of = - mod_pos_neg [of "number_of v" "number_of w", standard] - -lemmas mod_neg_neg_number_of = - mod_neg_neg [of "number_of v" "number_of w", standard] - - lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w", standard] @@ -584,15 +556,6 @@ text{*Special-case simplification *} -lemma zmod_1 [simp]: "a mod (1::int) = 0" -apply (cut_tac a = a and b = 1 in pos_mod_sign) -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) -apply (auto simp del:pos_mod_bound pos_mod_sign) -done - -lemma zdiv_1 [simp]: "a div (1::int) = a" -by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) - lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" apply (cut_tac a = a and b = "-1" in neg_mod_sign) apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound) @@ -726,9 +689,6 @@ apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod]) done -lemma zdiv_zmult_self1 [simp]: "b \ (0::int) ==> (a*b) div b = a" -by (simp add: zdiv_zmult1_eq) - lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)" apply (case_tac "b = 0", simp) apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) @@ -754,7 +714,7 @@ assume not0: "b \ 0" show "(a + c * b) div b = c + a div b" unfolding zdiv_zadd1_eq [of a "c * b"] using not0 - by (simp add: zmod_zmult1_eq zmod_zdiv_trivial) + by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq) qed auto lemma posDivAlg_div_mod: @@ -784,41 +744,12 @@ show ?thesis by simp qed -lemma zdiv_zadd_self1: "a \ (0::int) ==> (a+b) div a = b div a + 1" -by (rule div_add_self1) (* already declared [simp] *) - -lemma zdiv_zadd_self2: "a \ (0::int) ==> (b+a) div a = b div a + 1" -by (rule div_add_self2) (* already declared [simp] *) - -lemma zdiv_zmult_self2: "b \ (0::int) ==> (b*a) div b = a" -by (rule div_mult_self1_is_id) (* already declared [simp] *) - -lemma zmod_zmult_self1: "(a*b) mod b = (0::int)" -by (rule mod_mult_self2_is_0) (* already declared [simp] *) - -lemma zmod_zmult_self2: "(b*a) mod b = (0::int)" -by (rule mod_mult_self1_is_0) (* already declared [simp] *) - lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) (* REVISIT: should this be generalized to all semiring_div types? *) lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] -lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" -by (rule mod_add_left_eq) - -lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" -by (rule mod_add_right_eq) - -lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)" -by (rule mod_add_self1) (* already declared [simp] *) - -lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)" -by (rule mod_add_self2) (* already declared [simp] *) - -lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)" -by (rule mod_diff_eq) subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} @@ -902,13 +833,6 @@ "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)" by (simp add:zdiv_zmult_zmult1) -(* -lemma zdiv_zmult_zmult2: "c \ (0::int) ==> (a*c) div (b*c) = a div b" -apply (drule zdiv_zmult_zmult1) -apply (auto simp add: mult_commute) -done -*) - subsection{*Distribution of Factors over mod*} @@ -933,9 +857,6 @@ apply (auto simp add: mult_commute) done -lemma zmod_zmod_cancel: "n dvd m \ (k::int) mod m mod n = k mod n" -by (rule mod_mod_cancel) - subsection {*Splitting Rules for div and mod*} @@ -1070,7 +991,7 @@ apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) = 1 + 2* ((-b - 1) mod (-a))") apply (rule_tac [2] pos_zmod_mult_2) -apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib) +apply (auto simp add: right_diff_distrib) apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))") prefer 2 apply simp apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric]) @@ -1132,38 +1053,8 @@ subsection {* The Divides Relation *} -lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" - by (rule dvd_eq_mod_eq_0) - lemmas zdvd_iff_zmod_eq_0_number_of [simp] = - zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] - -lemma zdvd_0_right: "(m::int) dvd 0" - by (rule dvd_0_right) (* already declared [iff] *) - -lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)" - by (rule dvd_0_left_iff) (* already declared [noatp,simp] *) - -lemma zdvd_1_left: "1 dvd (m::int)" - by (rule one_dvd) (* already declared [simp] *) - -lemma zdvd_refl: "m dvd (m::int)" - by (rule dvd_refl) (* already declared [simp] *) - -lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" - by (rule dvd_trans) - -lemma zdvd_zminus_iff: "m dvd -n \ m dvd (n::int)" - by (rule dvd_minus_iff) (* already declared [simp] *) - -lemma zdvd_zminus2_iff: "-m dvd n \ m dvd (n::int)" - by (rule minus_dvd_iff) (* already declared [simp] *) - -lemma zdvd_abs1: "( \i::int\ dvd j) = (i dvd j)" - by (rule abs_dvd_iff) (* already declared [simp] *) - -lemma zdvd_abs2: "( (i::int) dvd \j\) = (i dvd j)" - by (rule dvd_abs_iff) (* already declared [simp] *) + dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard] lemma zdvd_anti_sym: "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" @@ -1171,58 +1062,32 @@ apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff) done -lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" - by (rule dvd_add) - -lemma zdvd_dvd_eq: assumes anz:"a \ 0" and ab: "(a::int) dvd b" and ba:"b dvd a" +lemma zdvd_dvd_eq: assumes "a \ 0" and "(a::int) dvd b" and "b dvd a" shows "\a\ = \b\" proof- - from ab obtain k where k:"b = a*k" unfolding dvd_def by blast - from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast + from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast + from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast from k k' have "a = a*k*k'" by simp with mult_cancel_left1[where c="a" and b="k*k'"] - have kk':"k*k' = 1" using anz by (simp add: mult_assoc) + have kk':"k*k' = 1" using `a\0` by (simp add: mult_assoc) hence "k = 1 \ k' = 1 \ k = -1 \ k' = -1" by (simp add: zmult_eq_1_iff) thus ?thesis using k k' by auto qed -lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)" - by (rule Ring_and_Field.dvd_diff) - lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" apply (subgoal_tac "m = n + (m - n)") apply (erule ssubst) - apply (blast intro: zdvd_zadd, simp) + apply (blast intro: dvd_add, simp) done -lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" - by (rule dvd_mult) - -lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" - by (rule dvd_mult2) - -lemma zdvd_triv_right: "(k::int) dvd m * k" - by (rule dvd_triv_right) (* already declared [simp] *) - -lemma zdvd_triv_left: "(k::int) dvd k * m" - by (rule dvd_triv_left) (* already declared [simp] *) - -lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" - by (rule dvd_mult_left) - -lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" - by (rule dvd_mult_right) - -lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" - by (rule mult_dvd_mono) - lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" - apply (rule iffI) - apply (erule_tac [2] zdvd_zadd) - apply (subgoal_tac "n = (n + k * m) - k * m") - apply (erule ssubst) - apply (erule zdvd_zdiff, simp_all) - done +apply (rule iffI) + apply (erule_tac [2] dvd_add) + apply (subgoal_tac "n = (n + k * m) - k * m") + apply (erule ssubst) + apply (erule dvd_diff) + apply(simp_all) +done lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" apply (simp add: dvd_def) @@ -1232,7 +1097,7 @@ lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" apply (subgoal_tac "k dvd n * (m div n) + m mod n") apply (simp add: zmod_zdiv_equality [symmetric]) - apply (simp only: zdvd_zadd zdvd_zmult2) + apply (simp only: dvd_add dvd_mult2) done lemma zdvd_not_zless: "0 < m ==> m < n ==> \ n dvd (m::int)" @@ -1252,7 +1117,7 @@ lemma zdvd_mult_div_cancel:"(n::int) dvd m \ n * (m div n) = m" apply (subgoal_tac "m mod n = 0") apply (simp add: zmult_div_cancel) -apply (simp only: zdvd_iff_zmod_eq_0) +apply (simp only: dvd_eq_mod_eq_0) done lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \ (0::int)" @@ -1265,10 +1130,6 @@ thus ?thesis by simp qed -lemma zdvd_zmult_cancel_disj[simp]: - "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))" -by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel) - theorem ex_nat: "(\x::nat. P x) = (\x::int. 0 <= x \ P (nat x))" apply (simp split add: split_nat) @@ -1300,44 +1161,38 @@ then show ?thesis by (simp only: negative_eq_positive) auto qed qed - then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult) + then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult) qed lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \x\ = 1)" proof - assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by (simp add: zdvd_abs1) + assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by simp hence "nat \x\ dvd 1" by (simp add: zdvd_int) hence "nat \x\ = 1" by simp thus "\x\ = 1" by (cases "x < 0", auto) next assume "\x\=1" thus "x dvd 1" - by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0) + by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0) qed lemma zdvd_mult_cancel1: assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" proof assume n1: "\n\ = 1" thus "m * n dvd m" - by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff) + by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff) next assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq) qed lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" - unfolding zdvd_int by (cases "z \ 0") (simp_all add: zdvd_zminus_iff) + unfolding zdvd_int by (cases "z \ 0") simp_all lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" - unfolding zdvd_int by (cases "z \ 0") (simp_all add: zdvd_zminus2_iff) + unfolding zdvd_int by (cases "z \ 0") simp_all lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)" by (auto simp add: dvd_int_iff) -lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))" - by (rule minus_dvd_iff) - -lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))" - by (rule dvd_minus_iff) - lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \ (n::int)" apply (rule_tac z=n in int_cases) apply (auto simp add: dvd_int_iff) @@ -1367,10 +1222,13 @@ apply (auto simp add: IntDiv.divmod_rel_def of_nat_mult) done +lemma abs_div: "(y::int) dvd x \ abs (x div y) = abs x div abs y" +by (unfold dvd_def, cases "y=0", auto simp add: abs_mult) + text{*Suggested by Matthias Daum*} lemma int_power_div_base: "\0 < m; 0 < k\ \ k ^ m div k = (k::int) ^ (m - Suc 0)" -apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)") +apply (subgoal_tac "k ^ m = k ^ ((m - Suc 0) + Suc 0)") apply (erule ssubst) apply (simp only: power_add) apply simp_all @@ -1387,8 +1245,8 @@ by (rule mod_diff_right_eq [symmetric]) lemmas zmod_simps = - IntDiv.zmod_zadd_left_eq [symmetric] - IntDiv.zmod_zadd_right_eq [symmetric] + mod_add_left_eq [symmetric] + mod_add_right_eq [symmetric] IntDiv.zmod_zmult1_eq [symmetric] mod_mult_left_eq [symmetric] IntDiv.zpower_zmod @@ -1463,14 +1321,14 @@ assume H: "x mod n = y mod n" hence "x mod n - y mod n = 0" by simp hence "(x mod n - y mod n) mod n = 0" by simp - hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric]) - thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0) + hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric]) + thus "n dvd x - y" by (simp add: dvd_eq_mod_eq_0) next assume H: "n dvd x - y" then obtain k where k: "x-y = n*k" unfolding dvd_def by blast hence "x = n*k + y" by simp hence "x mod n = (n*k + y) mod n" by simp - thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq) + thus "x mod n = y mod n" by (simp add: mod_add_left_eq) qed lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \ x"