# HG changeset patch # User haftmann # Date 1416232533 -3600 # Node ID 348561aa3869f0631522674f8f098871a046e9b5 # Parent f61482b0f240c28e81584cab72a11d63dc0e807b generalized lemmas (particularly concerning dvd) as far as appropriate diff -r f61482b0f240 -r 348561aa3869 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Nov 17 14:55:32 2014 +0100 +++ b/src/HOL/Divides.thy Mon Nov 17 14:55:33 2014 +0100 @@ -28,6 +28,14 @@ subclass semiring_no_zero_divisors .. +lemma power_not_zero: -- \FIXME cf. @{text field_power_not_zero}\ + "a \ 0 \ a ^ n \ 0" + by (induct n) (simp_all add: no_zero_divisors) + +lemma semiring_div_power_eq_0_iff: -- \FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\ + "n \ 0 \ a ^ n = 0 \ a = 0" + using power_not_zero [of a n] by (auto simp add: zero_power) + text {* @{const div} and @{const mod} *} lemma mod_div_equality2: "b * (a div b) + a mod b = a" @@ -390,6 +398,20 @@ lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" by (fact mod_mult_mult1 [symmetric]) +lemma dvd_times_left_cancel_iff [simp]: -- \FIXME generalize\ + assumes "c \ 0" + shows "c * a dvd c * b \ a dvd b" +proof - + have "(c * b) mod (c * a) = 0 \ b mod a = 0" (is "?P \ ?Q") + using assms by (simp add: mod_mult_mult1) + then show ?thesis by (simp add: mod_eq_0_iff_dvd) +qed + +lemma dvd_times_right_cancel_iff [simp]: -- \FIXME generalize\ + assumes "c \ 0" + shows "a * c dvd b * c \ a dvd b" + using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps) + lemma dvd_mod: "k dvd m \ k dvd n \ k dvd (m mod n)" unfolding dvd_def by (auto simp add: mod_mult_mult1) @@ -643,20 +665,6 @@ "a - 0 = a" by (rule diff_invert_add1 [symmetric]) simp -lemma dvd_times_left_cancel_iff [simp]: -- \FIXME generalize\ - assumes "c \ 0" - shows "c * a dvd c * b \ a dvd b" -proof - - have "(c * b) mod (c * a) = 0 \ b mod a = 0" (is "?P \ ?Q") - using assms by (simp add: mod_mult_mult1) - then show ?thesis by (simp add: mod_eq_0_iff_dvd) -qed - -lemma dvd_times_right_cancel_iff [simp]: -- \FIXME generalize\ - assumes "c \ 0" - shows "a * c dvd b * c \ a dvd b" - using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps) - subclass semiring_div_parity proof fix a diff -r f61482b0f240 -r 348561aa3869 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Nov 17 14:55:32 2014 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Nov 17 14:55:33 2014 +0100 @@ -6,33 +6,6 @@ imports Complex_Main begin -lemma finite_int_set_iff_bounded_le: - "finite (N::int set) = (\m\0. \n\N. abs n \ m)" -proof - assume "finite (N::int set)" - hence "finite (nat ` abs ` N)" by (intro finite_imageI) - hence "\m. \n\nat`abs`N. n \ m" by (simp add: finite_nat_set_iff_bounded_le) - then obtain m :: nat where "\n\N. nat (abs n) \ nat (int m)" by auto - then show "\m\0. \n\N. abs n \ m" by (intro exI[of _ "int m"]) (auto simp: nat_le_eq_zle) -next - assume "\m\0. \n\N. abs n \ m" - then obtain m where "m \ 0" and "\n\N. abs n \ m" by blast - hence "\n\N. nat (abs n) \ nat m" by (auto simp: nat_le_eq_zle) - hence "\n\nat`abs`N. n \ nat m" by (auto simp: nat_le_eq_zle) - hence A: "finite ((nat \ abs)`N)" unfolding o_def - by (subst finite_nat_set_iff_bounded_le) blast - { - assume "\finite N" - from pigeonhole_infinite[OF this A] obtain x - where "x \ N" and B: "~finite {a\N. nat (abs a) = nat (abs x)}" - unfolding o_def by blast - have "{a\N. nat (abs a) = nat (abs x)} \ {x, -x}" by auto - hence "finite {a\N. nat (abs a) = nat (abs x)}" by (rule finite_subset) simp - with B have False by contradiction - } - then show "finite N" by blast -qed - context semiring_div begin @@ -46,32 +19,6 @@ finally show "setprod f A = f x * setprod f (A - {x})" . qed -lemma dvd_mult_cancel_left: - assumes "a \ 0" and "a * b dvd a * c" - shows "b dvd c" -proof- - from assms(2) obtain k where "a * c = a * b * k" unfolding dvd_def by blast - hence "c * a = b * k * a" by (simp add: ac_simps) - hence "c * (a div a) = b * k * (a div a)" by (simp add: div_mult_swap) - also from `a \ 0` have "a div a = 1" by simp - finally show ?thesis by simp -qed - -lemma dvd_mult_cancel_right: - "a \ 0 \ b * a dvd c * a \ b dvd c" - by (subst (asm) (1 2) ac_simps, rule dvd_mult_cancel_left) - -lemma nonzero_pow_nonzero: - "a \ 0 \ a ^ n \ 0" - by (induct n) (simp_all add: no_zero_divisors) - -lemma zero_pow_zero: "n \ 0 \ 0 ^ n = 0" - by (cases n, simp_all) - -lemma pow_zero_iff: - "n \ 0 \ a^n = 0 \ a = 0" - using nonzero_pow_nonzero zero_pow_zero by auto - end context semiring_div @@ -260,9 +207,9 @@ hence [simp]: "x dvd y" "y dvd x" using `associated x y` unfolding associated_def by simp_all hence "1 = x div y * (y div x)" - by (simp add: div_mult_swap dvd_div_mult_self) + by (simp add: div_mult_swap) hence "is_unit (x div y)" unfolding is_unit_def by (rule dvdI) - moreover have "x = (x div y) * y" by (simp add: dvd_div_mult_self) + moreover have "x = (x div y) * y" by simp ultimately show ?thesis by blast qed next @@ -364,7 +311,7 @@ have "?nf (x div ?nf x) * ?nf (?nf x) = ?nf (x div ?nf x * ?nf x)" by (simp add: normalisation_factor_mult) also have "x div ?nf x * ?nf x = x" using `x \ 0` - by (simp add: dvd_div_mult_self) + by simp also have "?nf (?nf x) = ?nf x" using `x \ 0` normalisation_factor_is_unit normalisation_factor_unit by simp finally show ?thesis using `x \ 0` and `?nf x \ 0` @@ -653,7 +600,7 @@ also have "... = k * gcd x y div ?nf k" by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd) finally show ?thesis - by (simp add: ac_simps dvd_mult_div_cancel) + by simp qed lemma euclidean_size_gcd_le1 [simp]: @@ -711,7 +658,7 @@ apply (simp add: ac_simps) apply (rule gcd_dvd2) apply (rule gcd_greatest, erule (1) gcd_greatest, assumption) - apply (simp add: gcd_zero) + apply simp done lemma gcd_left_idem: "gcd p (gcd p q) = gcd p q" @@ -719,7 +666,7 @@ apply simp apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2) apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption) - apply (simp add: gcd_zero) + apply simp done lemma comp_fun_idem_gcd: "comp_fun_idem gcd" @@ -754,7 +701,7 @@ have "gcd c d dvd d" by simp with A show "gcd a b dvd d" by (rule dvd_trans) show "normalisation_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)" - by (simp add: gcd_zero) + by simp fix l assume "l dvd c" and "l dvd d" hence "l dvd gcd c d" by (rule gcd_greatest) from this and B show "l dvd gcd a b" by (rule dvd_trans) @@ -786,10 +733,10 @@ moreover from `?lhs` have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) hence "b dvd a" by (simp add: coprime_dvd_mult_iff) moreover from `?lhs` have "c dvd d * b" - unfolding associated_def by (metis dvd_mult_right ac_simps) + unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps) hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute) moreover from `?lhs` have "d dvd c * a" - unfolding associated_def by (metis dvd_mult_right ac_simps) + unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps) hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute) ultimately show ?rhs unfolding associated_def by simp qed @@ -819,17 +766,18 @@ proof (rule coprimeI) fix l assume "l dvd a'" "l dvd b'" then obtain s t where "a' = l * s" "b' = l * t" unfolding dvd_def by blast - moreover have "a = a' * d" "b = b' * d" by (simp_all add: dvd_div_mult_self) + moreover have "a = a' * d" "b = b' * d" by simp_all ultimately have "a = (l * d) * s" "b = (l * d) * t" - by (metis ac_simps)+ + by (simp_all only: ac_simps) hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left) hence "l*d dvd d" by (simp add: gcd_greatest) - then obtain u where "u * l * d = d" unfolding dvd_def - by (metis ac_simps mult_assoc) - moreover from nz have "d \ 0" by (simp add: gcd_zero) - ultimately have "u * l = 1" - by (metis div_mult_self1_is_id div_self ac_simps) - then show "l dvd 1" by force + then obtain u where "d = l * d * u" .. + then have "d * (l * u) = d" by (simp add: ac_simps) + moreover from nz have "d \ 0" by simp + with div_mult_self1_is_id have "d * (l * u) div d = l * u" . + ultimately have "1 = l * u" + using `d \ 0` by simp + then show "l dvd 1" .. qed lemma coprime_mult: @@ -866,7 +814,7 @@ assumes z: "gcd a b \ 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b" shows "gcd a' b' = 1" proof - - from z have "a \ 0 \ b \ 0" by (simp add: gcd_zero) + from z have "a \ 0 \ b \ 0" by simp with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" . also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+ also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+ @@ -886,7 +834,7 @@ shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ gcd a' b' = 1" apply (rule_tac x = "a div gcd a b" in exI) apply (rule_tac x = "b div gcd a b" in exI) - apply (insert nz, auto simp add: dvd_div_mult gcd_0_left gcd_zero intro: div_gcd_coprime) + apply (insert nz, auto intro: div_gcd_coprime) done lemma coprime_exp: @@ -934,7 +882,7 @@ shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" proof (cases "gcd a b = 0") assume "gcd a b = 0" - hence "a = 0 \ b = 0" by (simp add: gcd_zero) + hence "a = 0 \ b = 0" by simp hence "a = 0 * c \ 0 dvd b \ c dvd c" by simp then show ?thesis by blast next @@ -947,7 +895,7 @@ with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac) - with `?d \ 0` have "a' dvd b' * c" by (rule dvd_mult_cancel_left) + with `?d \ 0` have "a' dvd b' * c" by simp with coprime_dvd_mult[OF ab'(3)] have "a' dvd c" by (subst (asm) ac_simps, blast) with ab'(1) have "a = ?d * a' \ ?d dvd b \ a' dvd c" by (simp add: mult_ac) @@ -959,12 +907,12 @@ shows "a dvd b" proof (cases "gcd a b = 0") assume "gcd a b = 0" - then show ?thesis by (simp add: gcd_zero) + then show ?thesis by simp next let ?d = "gcd a b" assume "?d \ 0" from n obtain m where m: "n = Suc m" by (cases n, simp_all) - from `?d \ 0` have zn: "?d ^ n \ 0" by (rule nonzero_pow_nonzero) + from `?d \ 0` have zn: "?d ^ n \ 0" by (rule power_not_zero) from gcd_coprime_exists[OF `?d \ 0`] obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" by blast @@ -972,7 +920,7 @@ by (simp add: ab'(1,2)[symmetric]) hence "?d^n * a'^n dvd ?d^n * b'^n" by (simp only: power_mult_distrib ac_simps) - with zn have "a'^n dvd b'^n" by (rule dvd_mult_cancel_left) + with zn have "a'^n dvd b'^n" by simp hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m) hence "a' dvd b'^m * b'" by (simp add: m ac_simps) with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]] @@ -1022,8 +970,18 @@ qed lemma invertible_coprime: - "x * y mod m = 1 \ gcd x m = 1" - by (metis coprime_lmult gcd_1 ac_simps gcd_red) + assumes "x * y mod m = 1" + shows "coprime x m" +proof - + from assms have "coprime m (x * y mod m)" + by simp + then have "coprime m (x * y)" + by simp + then have "coprime m x" + by (rule coprime_lmult) + then show ?thesis + by (simp add: ac_simps) +qed lemma lcm_gcd: "lcm a b = a * b div (gcd a b * normalisation_factor (a*b))" @@ -1108,7 +1066,7 @@ { assume "a \ 0" "b \ 0" hence "a * b div ?nf (a * b) \ 0" by (simp add: no_zero_divisors) - moreover from `a \ 0` and `b \ 0` have "gcd a b \ 0" by (simp add: gcd_zero) + moreover from `a \ 0` and `b \ 0` have "gcd a b \ 0" by simp ultimately have "lcm a b \ 0" using lcm_gcd_prod[of a b] by (intro notI, simp) } moreover { assume "a = 0 \ b = 0" @@ -1123,7 +1081,7 @@ assumes "lcm a b \ 0" shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))" proof- - from assms have "gcd a b \ 0" by (simp add: gcd_zero lcm_zero) + from assms have "gcd a b \ 0" by (simp add: lcm_zero) let ?c = "normalisation_factor (a*b)" from `lcm a b \ 0` have "?c \ 0" by (intro notI, simp add: lcm_zero no_zero_divisors) hence "is_unit ?c" by simp @@ -1383,7 +1341,7 @@ { fix l' assume "\x\A. x dvd l'" with `\x\A. x dvd l` have "\x\A. x dvd gcd l l'" by (auto intro: gcd_greatest) - moreover from `l \ 0` have "gcd l l' \ 0" by (simp add: gcd_zero) + moreover from `l \ 0` have "gcd l l' \ 0" by simp ultimately have "\b. b \ 0 \ (\x\A. x dvd b) \ euclidean_size b = euclidean_size (gcd l l')" by (intro exI[of _ "gcd l l'"], auto) hence "euclidean_size (gcd l l') \ n" by (subst n_def) (rule Least_le) @@ -1585,7 +1543,7 @@ then show "g' dvd Gcd A" by (simp add: Gcd_Lcm) next show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" - by (simp add: Gcd_Lcm normalisation_factor_Lcm) + by (simp add: Gcd_Lcm) qed lemma GcdI: @@ -1619,7 +1577,7 @@ fix l assume "l dvd a" and "l dvd Gcd A" hence "\x\A. l dvd x" by (blast intro: dvd_trans Gcd_dvd) with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd) -qed (auto intro: Gcd_dvd dvd_Gcd simp: normalisation_factor_Gcd) +qed auto lemma Gcd_finite: assumes "finite A" @@ -1653,11 +1611,11 @@ lemma gcd_neg1 [simp]: "gcd (-x) y = gcd x y" - by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero) + by (rule sym, rule gcdI, simp_all add: gcd_greatest) lemma gcd_neg2 [simp]: "gcd x (-y) = gcd x y" - by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero) + by (rule sym, rule gcdI, simp_all add: gcd_greatest) lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) x = gcd (numeral n) x" diff -r f61482b0f240 -r 348561aa3869 src/HOL/Power.thy --- a/src/HOL/Power.thy Mon Nov 17 14:55:32 2014 +0100 +++ b/src/HOL/Power.thy Mon Nov 17 14:55:33 2014 +0100 @@ -149,7 +149,12 @@ "of_nat (m ^ n) = of_nat m ^ n" by (induct n) (simp_all add: of_nat_mult) -lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0" +lemma zero_power: + "0 < n \ 0 ^ n = 0" + by (cases n) simp_all + +lemma power_zero_numeral [simp]: + "0 ^ numeral k = 0" by (simp add: numeral_eq_Suc) lemma zero_power2: "0\<^sup>2 = 0" (* delete? *) diff -r f61482b0f240 -r 348561aa3869 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Nov 17 14:55:32 2014 +0100 +++ b/src/HOL/Rings.thy Mon Nov 17 14:55:33 2014 +0100 @@ -134,13 +134,13 @@ end -class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + dvd - (*previously almost_semiring*) +context comm_monoid_mult begin -subclass semiring_1 .. +subclass dvd . -lemma dvd_refl[simp]: "a dvd a" +lemma dvd_refl [simp]: + "a dvd a" proof show "a = a * 1" by simp qed @@ -155,30 +155,25 @@ then show ?thesis .. qed -lemma dvd_0_left_iff [simp]: "0 dvd a \ a = 0" -by (auto intro: dvd_refl elim!: dvdE) +lemma one_dvd [simp]: + "1 dvd a" + by (auto intro!: dvdI) -lemma dvd_0_right [iff]: "a dvd 0" -proof - show "0 = a * 0" by simp -qed - -lemma one_dvd [simp]: "1 dvd a" -by (auto intro!: dvdI) +lemma dvd_mult [simp]: + "a dvd c \ a dvd (b * c)" + by (auto intro!: mult.left_commute dvdI elim!: dvdE) -lemma dvd_mult[simp]: "a dvd c \ a dvd (b * c)" -by (auto intro!: mult.left_commute dvdI elim!: dvdE) +lemma dvd_mult2 [simp]: + "a dvd b \ a dvd (b * c)" + using dvd_mult [of a b c] by (simp add: ac_simps) -lemma dvd_mult2[simp]: "a dvd b \ a dvd (b * c)" - apply (subst mult.commute) - apply (erule dvd_mult) - done +lemma dvd_triv_right [simp]: + "a dvd b * a" + by (rule dvd_mult) (rule dvd_refl) -lemma dvd_triv_right [simp]: "a dvd b * a" -by (rule dvd_mult) (rule dvd_refl) - -lemma dvd_triv_left [simp]: "a dvd a * b" -by (rule dvd_mult2) (rule dvd_refl) +lemma dvd_triv_left [simp]: + "a dvd a * b" + by (rule dvd_mult2) (rule dvd_refl) lemma mult_dvd_mono: assumes "a dvd b" @@ -191,17 +186,39 @@ then show ?thesis .. qed -lemma dvd_mult_left: "a * b dvd c \ a dvd c" -by (simp add: dvd_def mult.assoc, blast) +lemma dvd_mult_left: + "a * b dvd c \ a dvd c" + by (simp add: dvd_def mult.assoc) blast -lemma dvd_mult_right: "a * b dvd c \ b dvd c" - unfolding mult.commute [of a] by (rule dvd_mult_left) +lemma dvd_mult_right: + "a * b dvd c \ b dvd c" + using dvd_mult_left [of b a c] by (simp add: ac_simps) + +end + +class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult + (*previously almost_semiring*) +begin + +subclass semiring_1 .. -lemma dvd_0_left: "0 dvd a \ a = 0" -by simp +lemma dvd_0_left_iff [simp]: + "0 dvd a \ a = 0" + by (auto intro: dvd_refl elim!: dvdE) -lemma dvd_add[simp]: - assumes "a dvd b" and "a dvd c" shows "a dvd (b + c)" +lemma dvd_0_right [iff]: + "a dvd 0" +proof + show "0 = a * 0" by simp +qed + +lemma dvd_0_left: + "0 dvd a \ a = 0" + by simp + +lemma dvd_add [simp]: + assumes "a dvd b" and "a dvd c" + shows "a dvd (b + c)" proof - from `a dvd b` obtain b' where "b = a * b'" .. moreover from `a dvd c` obtain c' where "c = a * c'" ..