# HG changeset patch # User Manuel Eberl # Date 1456521309 -3600 # Node ID 25271ff79171c7a51182bf99f19decf241fed9fa # Parent 4d5fbec92bb191fa5d10eb3a13ad5422764bb992 Tuned Euclidean Rings/GCD rings diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Fri Feb 26 22:15:09 2016 +0100 @@ -60,7 +60,19 @@ lemma [code, code del]: "(Lcm :: int set \ int) = Lcm" .. - + +lemma [code, code del]: + "(Gcd :: _ poly set \ _) = Gcd" .. + +lemma [code, code del]: + "(Lcm :: _ poly set \ _) = Lcm" .. + +lemma [code, code del]: + "Gcd_eucl = Gcd_eucl" .. + +lemma [code, code del]: + "Lcm_eucl = Lcm_eucl" .. + (* If the code generation ends with an exception with the following message: '"List.set" is not a constructor, on left hand side of equation: ...', diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/GCD.thy Fri Feb 26 22:15:09 2016 +0100 @@ -395,10 +395,549 @@ lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c" using mult_lcm_left [of c a b] by (simp add: ac_simps) + +lemma gcdI: + assumes "c dvd a" and "c dvd b" and greatest: "\d. d dvd a \ d dvd b \ d dvd c" + and "normalize c = c" + shows "c = gcd a b" + by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) + +lemma gcd_unique: "d dvd a \ d dvd b \ + normalize d = d \ + (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" + by rule (auto intro: gcdI simp: gcd_greatest) + +lemma gcd_dvd_prod: "gcd a b dvd k * b" + using mult_dvd_mono [of 1] by auto + +lemma gcd_proj2_if_dvd: "b dvd a \ gcd a b = normalize b" + by (rule gcdI [symmetric]) simp_all + +lemma gcd_proj1_if_dvd: "a dvd b \ gcd a b = normalize a" + by (rule gcdI [symmetric]) simp_all + +lemma gcd_proj1_iff: "gcd m n = normalize m \ m dvd n" +proof + assume A: "gcd m n = normalize m" + show "m dvd n" + proof (cases "m = 0") + assume [simp]: "m \ 0" + from A have B: "m = gcd m n * unit_factor m" + by (simp add: unit_eq_div2) + show ?thesis by (subst B, simp add: mult_unit_dvd_iff) + qed (insert A, simp) +next + assume "m dvd n" + then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd) +qed +lemma gcd_proj2_iff: "gcd m n = normalize n \ n dvd m" + using gcd_proj1_iff [of n m] by (simp add: ac_simps) + +lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)" + by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric]) + +lemma gcd_mult_distrib: + "k * gcd a b = gcd (k * a) (k * b) * unit_factor k" +proof- + have "normalize k * gcd a b = gcd (k * a) (k * b)" + by (simp add: gcd_mult_distrib') + then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k" + by simp + then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k" + by (simp only: ac_simps) + then show ?thesis + by simp +qed + +lemma lcm_mult_unit1: + "is_unit a \ lcm (b * a) c = lcm b c" + by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1) + +lemma lcm_mult_unit2: + "is_unit a \ lcm b (c * a) = lcm b c" + using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) + +lemma lcm_div_unit1: + "is_unit a \ lcm (b div a) c = lcm b c" + by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) + +lemma lcm_div_unit2: + "is_unit a \ lcm b (c div a) = lcm b c" + by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) + +lemma normalize_lcm_left [simp]: + "lcm (normalize a) b = lcm a b" +proof (cases "a = 0") + case True then show ?thesis + by simp +next + case False then have "is_unit (unit_factor a)" + by simp + moreover have "normalize a = a div unit_factor a" + by simp + ultimately show ?thesis + by (simp only: lcm_div_unit1) +qed + +lemma normalize_lcm_right [simp]: + "lcm a (normalize b) = lcm a b" + using normalize_lcm_left [of b a] by (simp add: ac_simps) + +lemma gcd_mult_unit1: "is_unit a \ gcd (b * a) c = gcd b c" + apply (rule gcdI) + apply simp_all + apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) + done + +lemma gcd_mult_unit2: "is_unit a \ gcd b (c * a) = gcd b c" + by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute) + +lemma gcd_div_unit1: "is_unit a \ gcd (b div a) c = gcd b c" + by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) + +lemma gcd_div_unit2: "is_unit a \ gcd b (c div a) = gcd b c" + by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) + +lemma normalize_gcd_left [simp]: + "gcd (normalize a) b = gcd a b" +proof (cases "a = 0") + case True then show ?thesis + by simp +next + case False then have "is_unit (unit_factor a)" + by simp + moreover have "normalize a = a div unit_factor a" + by simp + ultimately show ?thesis + by (simp only: gcd_div_unit1) +qed + +lemma normalize_gcd_right [simp]: + "gcd a (normalize b) = gcd a b" + using normalize_gcd_left [of b a] by (simp add: ac_simps) + +lemma comp_fun_idem_gcd: "comp_fun_idem gcd" + by standard (simp_all add: fun_eq_iff ac_simps) + +lemma comp_fun_idem_lcm: "comp_fun_idem lcm" + by standard (simp_all add: fun_eq_iff ac_simps) + +lemma gcd_dvd_antisym: + "gcd a b dvd gcd c d \ gcd c d dvd gcd a b \ gcd a b = gcd c d" +proof (rule gcdI) + assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b" + have "gcd c d dvd c" by simp + with A show "gcd a b dvd c" by (rule dvd_trans) + have "gcd c d dvd d" by simp + with A show "gcd a b dvd d" by (rule dvd_trans) + show "normalize (gcd a b) = gcd a b" + 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) +qed + +lemma coprime_dvd_mult: + assumes "coprime a b" and "a dvd c * b" + shows "a dvd c" +proof (cases "c = 0") + case True then show ?thesis by simp +next + case False + then have unit: "is_unit (unit_factor c)" by simp + from \coprime a b\ mult_gcd_left [of c a b] + have "gcd (c * a) (c * b) * unit_factor c = c" + by (simp add: ac_simps) + moreover from \a dvd c * b\ have "a dvd gcd (c * a) (c * b) * unit_factor c" + by (simp add: dvd_mult_unit_iff unit) + ultimately show ?thesis by simp +qed + +lemma coprime_dvd_mult_iff: + assumes "coprime a c" + shows "a dvd b * c \ a dvd b" + using assms by (auto intro: coprime_dvd_mult) + +lemma gcd_mult_cancel: + "coprime c b \ gcd (c * a) b = gcd a b" + apply (rule associated_eqI) + apply (rule gcd_greatest) + apply (rule_tac b = c in coprime_dvd_mult) + apply (simp add: gcd.assoc) + apply (simp_all add: ac_simps) + done + +lemma coprime_crossproduct: + fixes a b c d + assumes "coprime a d" and "coprime b c" + shows "normalize a * normalize c = normalize b * normalize d + \ normalize a = normalize b \ normalize c = normalize d" (is "?lhs \ ?rhs") +proof + assume ?rhs then show ?lhs by simp +next + assume ?lhs + from \?lhs\ have "normalize a dvd normalize b * normalize d" + by (auto intro: dvdI dest: sym) + with \coprime a d\ have "a dvd b" + by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) + from \?lhs\ have "normalize b dvd normalize a * normalize c" + by (auto intro: dvdI dest: sym) + with \coprime b c\ have "b dvd a" + by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) + from \?lhs\ have "normalize c dvd normalize d * normalize b" + by (auto intro: dvdI dest: sym simp add: mult.commute) + with \coprime b c\ have "c dvd d" + by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) + from \?lhs\ have "normalize d dvd normalize c * normalize a" + by (auto intro: dvdI dest: sym simp add: mult.commute) + with \coprime a d\ have "d dvd c" + by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) + from \a dvd b\ \b dvd a\ have "normalize a = normalize b" + by (rule associatedI) + moreover from \c dvd d\ \d dvd c\ have "normalize c = normalize d" + by (rule associatedI) + ultimately show ?rhs .. +qed + +lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n" + by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff) + +lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n" + using gcd_add1 [of n m] by (simp add: ac_simps) + +lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n" + by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff) + +lemma coprimeI: "(\l. \l dvd a; l dvd b\ \ l dvd 1) \ gcd a b = 1" + by (rule sym, rule gcdI, simp_all) + +lemma coprime: "gcd a b = 1 \ (\d. d dvd a \ d dvd b \ is_unit d)" + by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2) + +lemma div_gcd_coprime: + assumes nz: "a \ 0 \ b \ 0" + shows "coprime (a div gcd a b) (b div gcd a b)" +proof - + let ?g = "gcd a b" + let ?a' = "a div ?g" + let ?b' = "b div ?g" + let ?g' = "gcd ?a' ?b'" + have dvdg: "?g dvd a" "?g dvd b" by simp_all + have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all + from dvdg dvdg' obtain ka kb ka' kb' where + kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" + unfolding dvd_def by blast + from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" + by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) + then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" + by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] + dvd_mult_div_cancel [OF dvdg(2)] dvd_def) + have "?g \ 0" using nz by simp + moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . + thm dvd_mult_cancel_left + ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp +qed + + +lemma divides_mult: + assumes "a dvd c" and nr: "b dvd c" and "coprime a b" + shows "a * b dvd c" +proof- + from \b dvd c\ obtain b' where"c = b * b'" .. + with \a dvd c\ have "a dvd b' * b" + by (simp add: ac_simps) + with \coprime a b\ have "a dvd b'" + by (simp add: coprime_dvd_mult_iff) + then obtain a' where "b' = a * a'" .. + with \c = b * b'\ have "c = (a * b) * a'" + by (simp add: ac_simps) + then show ?thesis .. +qed + +lemma coprime_lmult: + assumes dab: "gcd d (a * b) = 1" + shows "gcd d a = 1" +proof (rule coprimeI) + fix l assume "l dvd d" and "l dvd a" + hence "l dvd a * b" by simp + with \l dvd d\ and dab show "l dvd 1" by (auto intro: gcd_greatest) +qed + +lemma coprime_rmult: + assumes dab: "gcd d (a * b) = 1" + shows "gcd d b = 1" +proof (rule coprimeI) + fix l assume "l dvd d" and "l dvd b" + hence "l dvd a * b" by simp + with \l dvd d\ and dab show "l dvd 1" by (auto intro: gcd_greatest) +qed + +lemma coprime_mult: + assumes da: "coprime d a" and db: "coprime d b" + shows "coprime d (a * b)" + apply (subst gcd.commute) + using da apply (subst gcd_mult_cancel) + apply (subst gcd.commute, assumption) + apply (subst gcd.commute, rule db) + done + +lemma coprime_mul_eq: "gcd d (a * b) = 1 \ gcd d a = 1 \ gcd d b = 1" + using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast + +lemma gcd_coprime: + assumes c: "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 c 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'" using dvd_div_eq_mult local.gcd_dvd1 by blast + also from assms have "b div gcd a b = b'" using dvd_div_eq_mult local.gcd_dvd1 by blast + finally show ?thesis . +qed + +lemma coprime_power: + assumes "0 < n" + shows "gcd a (b ^ n) = 1 \ gcd a b = 1" +using assms proof (induct n) + case (Suc n) then show ?case + by (cases n) (simp_all add: coprime_mul_eq) +qed simp + +lemma gcd_coprime_exists: + assumes nz: "gcd a b \ 0" + 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 intro: div_gcd_coprime) + done + +lemma coprime_exp: + "gcd d a = 1 \ gcd d (a^n) = 1" + by (induct n, simp_all add: coprime_mult) + +lemma coprime_exp_left: + assumes "coprime a b" + shows "coprime (a ^ n) b" + using assms by (induct n) (simp_all add: gcd_mult_cancel) + +lemma coprime_exp2: + assumes "coprime a b" + shows "coprime (a ^ n) (b ^ m)" +proof (rule coprime_exp_left) + from assms show "coprime a (b ^ m)" + by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a]) +qed + +lemma gcd_exp: + "gcd (a ^ n) (b ^ n) = gcd a b ^ n" +proof (cases "a = 0 \ b = 0") + case True + then show ?thesis by (cases n) simp_all +next + case False + then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" + using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp + then have "gcd a b ^ n = gcd a b ^ n * ..." by simp + also note gcd_mult_distrib + also have "unit_factor (gcd a b ^ n) = 1" + using False by (auto simp add: unit_factor_power unit_factor_gcd) + also have "(gcd a b)^n * (a div gcd a b)^n = a^n" + by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) + also have "(gcd a b)^n * (b div gcd a b)^n = b^n" + by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) + finally show ?thesis by simp +qed + +lemma coprime_common_divisor: + "gcd a b = 1 \ a dvd a \ a dvd b \ is_unit a" + apply (subgoal_tac "a dvd gcd a b") + apply simp + apply (erule (1) gcd_greatest) + done + +lemma division_decomp: + assumes dc: "a dvd b * c" + 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 + hence "a = 0 * c \ 0 dvd b \ c dvd c" by simp + then show ?thesis by blast +next + let ?d = "gcd a b" + assume "?d \ 0" + from gcd_coprime_exists[OF this] + obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" + by blast + from ab'(1) have "a' dvd a" unfolding dvd_def by blast + 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 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) + then show ?thesis by blast +qed + +lemma pow_divs_pow: + assumes ab: "a ^ n dvd b ^ n" and n: "n \ 0" + shows "a dvd b" +proof (cases "gcd a b = 0") + assume "gcd a b = 0" + 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 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 + from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n" + 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 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]] + have "a' dvd b'" by (subst (asm) ac_simps, blast) + hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp) + with ab'(1,2) show ?thesis by simp +qed + +lemma pow_divs_eq [simp]: + "n \ 0 \ a ^ n dvd b ^ n \ a dvd b" + by (auto intro: pow_divs_pow dvd_power_same) + +lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1" + by (subst add_commute, simp) + +lemma setprod_coprime [rule_format]: + "(\i\A. gcd (f i) a = 1) \ gcd (\i\A. f i) a = 1" + apply (cases "finite A") + apply (induct set: finite) + apply (auto simp add: gcd_mult_cancel) + done + +lemma listprod_coprime: + "(\x. x \ set xs \ coprime x y) \ coprime (listprod xs) y" + by (induction xs) (simp_all add: gcd_mult_cancel) + +lemma coprime_divisors: + assumes "d dvd a" "e dvd b" "gcd a b = 1" + shows "gcd d e = 1" +proof - + from assms obtain k l where "a = d * k" "b = e * l" + unfolding dvd_def by blast + with assms have "gcd (d * k) (e * l) = 1" by simp + hence "gcd (d * k) e = 1" by (rule coprime_lmult) + also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps) + finally have "gcd e d = 1" by (rule coprime_lmult) + then show ?thesis by (simp add: ac_simps) +qed + +lemma lcm_gcd_prod: + "lcm a b * gcd a b = normalize (a * b)" + by (simp add: lcm_gcd) + +declare unit_factor_lcm [simp] + +lemma lcmI: + assumes "a dvd c" and "b dvd c" and "\d. a dvd d \ b dvd d \ c dvd d" + and "normalize c = c" + shows "c = lcm a b" + by (rule associated_eqI) (auto simp: assms intro: lcm_least) + +lemma gcd_dvd_lcm [simp]: + "gcd a b dvd lcm a b" + using gcd_dvd2 by (rule dvd_lcmI2) + +lemmas lcm_0 = lcm_0_right + +lemma lcm_unique: + "a dvd d \ b dvd d \ + normalize d = d \ + (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" + by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff) + +lemma lcm_coprime: + "gcd a b = 1 \ lcm a b = normalize (a * b)" + by (subst lcm_gcd) simp + +lemma lcm_proj1_if_dvd: + "b dvd a \ lcm a b = normalize a" + by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) + +lemma lcm_proj2_if_dvd: + "a dvd b \ lcm a b = normalize b" + using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) + +lemma lcm_proj1_iff: + "lcm m n = normalize m \ n dvd m" +proof + assume A: "lcm m n = normalize m" + show "n dvd m" + proof (cases "m = 0") + assume [simp]: "m \ 0" + from A have B: "m = lcm m n * unit_factor m" + by (simp add: unit_eq_div2) + show ?thesis by (subst B, simp) + qed simp +next + assume "n dvd m" + then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd) +qed + +lemma lcm_proj2_iff: + "lcm m n = normalize n \ m dvd n" + using lcm_proj1_iff [of n m] by (simp add: ac_simps) + end class ring_gcd = comm_ring_1 + semiring_gcd +begin + +lemma coprime_minus_one: "coprime (n - 1) n" + using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute) + +lemma gcd_neg1 [simp]: + "gcd (-a) b = gcd a b" + by (rule sym, rule gcdI, simp_all add: gcd_greatest) + +lemma gcd_neg2 [simp]: + "gcd a (-b) = gcd a b" + by (rule sym, rule gcdI, simp_all add: gcd_greatest) + +lemma gcd_neg_numeral_1 [simp]: + "gcd (- numeral n) a = gcd (numeral n) a" + by (fact gcd_neg1) + +lemma gcd_neg_numeral_2 [simp]: + "gcd a (- numeral n) = gcd a (numeral n)" + by (fact gcd_neg2) + +lemma gcd_diff1: "gcd (m - n) n = gcd m n" + by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) + +lemma gcd_diff2: "gcd (n - m) n = gcd m n" + by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1) + +lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b" + by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff) + +lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b" + by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff) + +lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a" + by (fact lcm_neg1) + +lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)" + by (fact lcm_neg2) + +end class semiring_Gcd = semiring_gcd + Gcd + assumes Gcd_dvd: "a \ A \ Gcd A dvd a" @@ -471,6 +1010,27 @@ by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) qed +lemma LcmI: + assumes "\a. a \ A \ a dvd b" and "\c. (\a. a \ A \ a dvd c) \ b dvd c" + and "normalize b = b" shows "b = Lcm A" + by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least) + +lemma Lcm_subset: + "A \ B \ Lcm A dvd Lcm B" + by (blast intro: Lcm_least dvd_Lcm) + +lemma Lcm_Un: + "Lcm (A \ B) = lcm (Lcm A) (Lcm B)" + apply (rule lcmI) + apply (blast intro: Lcm_subset) + apply (blast intro: Lcm_subset) + apply (intro Lcm_least ballI, elim UnE) + apply (rule dvd_trans, erule dvd_Lcm, assumption) + apply (rule dvd_trans, erule dvd_Lcm, assumption) + apply simp + done + + lemma Gcd_0_iff [simp]: "Gcd A = 0 \ A \ {0}" (is "?P \ ?Q") proof @@ -518,20 +1078,6 @@ by simp qed -lemma unit_factor_Gcd: - "unit_factor (Gcd A) = (if \a\A. a = 0 then 0 else 1)" -proof (cases "Gcd A = 0") - case True then show ?thesis by auto -next - case False - from unit_factor_mult_normalize - have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" . - then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp - then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp - with False have "unit_factor (Gcd A) = 1" by simp - with False show ?thesis by auto -qed - lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" proof (cases "Lcm A = 0") @@ -544,6 +1090,18 @@ by simp qed +lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" +proof - + show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" + by (simp add: Gcd_Lcm unit_factor_Lcm) +qed + +lemma GcdI: + assumes "\a. a \ A \ b dvd a" and "\c. (\a. a \ A \ c dvd a) \ c dvd b" + and "normalize b = b" + shows "b = Gcd A" + by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) + lemma Gcd_eq_1_I: assumes "is_unit a" and "a \ A" shows "Gcd A = 1" @@ -585,13 +1143,26 @@ (auto simp add: lcm_eq_0_iff) qed -lemma Gcd_set [code_unfold]: - "Gcd (set as) = foldr gcd as 0" - by (induct as) simp_all +lemma Gcd_finite: + assumes "finite A" + shows "Gcd A = Finite_Set.fold gcd 0 A" + by (induct rule: finite.induct[OF \finite A\]) + (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) + +lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as" + by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] + foldl_conv_fold gcd.commute) + +lemma Lcm_finite: + assumes "finite A" + shows "Lcm A = Finite_Set.fold lcm 1 A" + by (induct rule: finite.induct[OF \finite A\]) + (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) lemma Lcm_set [code_unfold]: - "Lcm (set as) = foldr lcm as 1" - by (induct as) simp_all + "Lcm (set as) = foldl lcm 1 as" + by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] + foldl_conv_fold lcm.commute) lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A" @@ -624,6 +1195,76 @@ shows "Lcm A = a" using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm) + +lemma Lcm_no_units: + "Lcm A = Lcm (A - {a. is_unit a})" +proof - + have "(A - {a. is_unit a}) \ {a\A. is_unit a} = A" by blast + hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\A. is_unit a})" + by (simp add: Lcm_Un [symmetric]) + also have "Lcm {a\A. is_unit a} = 1" by (simp add: Lcm_1_iff) + finally show ?thesis by simp +qed + +lemma Lcm_0_iff': "Lcm A = 0 \ \(\l. l \ 0 \ (\a\A. a dvd l))" + by (metis Lcm_least dvd_0_left dvd_Lcm) + +lemma Lcm_no_multiple: "(\m. m \ 0 \ (\a\A. \a dvd m)) \ Lcm A = 0" + by (auto simp: Lcm_0_iff') + +lemma Lcm_singleton [simp]: + "Lcm {a} = normalize a" + by simp + +lemma Lcm_2 [simp]: + "Lcm {a,b} = lcm a b" + by simp + +lemma Lcm_coprime: + assumes "finite A" and "A \ {}" + assumes "\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1" + shows "Lcm A = normalize (\A)" +using assms proof (induct rule: finite_ne_induct) + case (insert a A) + have "Lcm (insert a A) = lcm a (Lcm A)" by simp + also from insert have "Lcm A = normalize (\A)" by blast + also have "lcm a \ = lcm a (\A)" by (cases "\A = 0") (simp_all add: lcm_div_unit2) + also from insert have "gcd a (\A) = 1" by (subst gcd.commute, intro setprod_coprime) auto + with insert have "lcm a (\A) = normalize (\(insert a A))" + by (simp add: lcm_coprime) + finally show ?case . +qed simp + +lemma Lcm_coprime': + "card A \ 0 \ (\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1) + \ Lcm A = normalize (\A)" + by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) + +lemma Gcd_1: + "1 \ A \ Gcd A = 1" + by (auto intro!: Gcd_eq_1_I) + +lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" + by simp + +lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" + by simp + + +definition pairwise_coprime where + "pairwise_coprime A = (\x y. x \ A \ y \ A \ x \ y \ coprime x y)" + +lemma pairwise_coprimeI [intro?]: + "(\x y. x \ A \ y \ A \ x \ y \ coprime x y) \ pairwise_coprime A" + by (simp add: pairwise_coprime_def) + +lemma pairwise_coprimeD: + "pairwise_coprime A \ x \ A \ y \ A \ x \ y \ coprime x y" + by (simp add: pairwise_coprime_def) + +lemma pairwise_coprime_subset: "pairwise_coprime A \ B \ A \ pairwise_coprime B" + by (force simp: pairwise_coprime_def) + end subsection \GCD and LCM on @{typ nat} and @{typ int}\ @@ -895,73 +1536,6 @@ apply auto done -context semiring_gcd -begin - -lemma coprime_dvd_mult: - assumes "coprime a b" and "a dvd c * b" - shows "a dvd c" -proof (cases "c = 0") - case True then show ?thesis by simp -next - case False - then have unit: "is_unit (unit_factor c)" by simp - from \coprime a b\ mult_gcd_left [of c a b] - have "gcd (c * a) (c * b) * unit_factor c = c" - by (simp add: ac_simps) - moreover from \a dvd c * b\ have "a dvd gcd (c * a) (c * b) * unit_factor c" - by (simp add: dvd_mult_unit_iff unit) - ultimately show ?thesis by simp -qed - -lemma coprime_dvd_mult_iff: - assumes "coprime a c" - shows "a dvd b * c \ a dvd b" - using assms by (auto intro: coprime_dvd_mult) - -lemma gcd_mult_cancel: - "coprime c b \ gcd (c * a) b = gcd a b" - apply (rule associated_eqI) - apply (rule gcd_greatest) - apply (rule_tac b = c in coprime_dvd_mult) - apply (simp add: gcd.assoc) - apply (simp_all add: ac_simps) - done - -lemma coprime_crossproduct: - fixes a b c d - assumes "coprime a d" and "coprime b c" - shows "normalize a * normalize c = normalize b * normalize d - \ normalize a = normalize b \ normalize c = normalize d" (is "?lhs \ ?rhs") -proof - assume ?rhs then show ?lhs by simp -next - assume ?lhs - from \?lhs\ have "normalize a dvd normalize b * normalize d" - by (auto intro: dvdI dest: sym) - with \coprime a d\ have "a dvd b" - by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) - from \?lhs\ have "normalize b dvd normalize a * normalize c" - by (auto intro: dvdI dest: sym) - with \coprime b c\ have "b dvd a" - by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric]) - from \?lhs\ have "normalize c dvd normalize d * normalize b" - by (auto intro: dvdI dest: sym simp add: mult.commute) - with \coprime b c\ have "c dvd d" - by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) - from \?lhs\ have "normalize d dvd normalize c * normalize a" - by (auto intro: dvdI dest: sym simp add: mult.commute) - with \coprime a d\ have "d dvd c" - by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric]) - from \a dvd b\ \b dvd a\ have "normalize a = normalize b" - by (rule associatedI) - moreover from \c dvd d\ \d dvd c\ have "normalize c = normalize d" - by (rule associatedI) - ultimately show ?rhs .. -qed - -end - lemma coprime_crossproduct_nat: fixes a b c d :: nat assumes "coprime a d" and "coprime b c" @@ -976,21 +1550,10 @@ text \\medskip Addition laws\ -lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" - apply (case_tac "n = 0") - apply (simp_all add: gcd_non_0_nat) - done - -lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n" - apply (subst (1 2) gcd.commute) - apply (subst add.commute) - apply simp - done - (* to do: add the other variations? *) lemma gcd_diff1_nat: "(m::nat) >= n \ gcd (m - n) n = gcd m n" - by (subst gcd_add1_nat [symmetric]) auto + by (subst gcd_add1 [symmetric]) auto lemma gcd_diff2_nat: "(n::nat) >= m \ gcd (n - m) n = gcd m n" apply (subst gcd.commute) @@ -1022,25 +1585,9 @@ apply auto done -lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" -by (metis gcd_red_int mod_add_self1 add.commute) - -lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" -by (metis gcd_add1_int gcd.commute add.commute) - -lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" -by (metis mod_mult_self3 gcd.commute gcd_red_nat) - -lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" -by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute) - - (* to do: differences, and all variations of addition rules as simplification rules for nat and int *) -lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n" - using mult_dvd_mono [of 1] by auto - (* to do: add the three variations of these, and for ints? *) lemma finite_divisors_nat [simp]: -- \FIXME move\ @@ -1104,49 +1651,6 @@ subsection \Coprimality\ -context semiring_gcd -begin - -lemma div_gcd_coprime: - assumes nz: "a \ 0 \ b \ 0" - shows "coprime (a div gcd a b) (b div gcd a b)" -proof - - let ?g = "gcd a b" - let ?a' = "a div ?g" - let ?b' = "b div ?g" - let ?g' = "gcd ?a' ?b'" - have dvdg: "?g dvd a" "?g dvd b" by simp_all - have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all - from dvdg dvdg' obtain ka kb ka' kb' where - kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" - unfolding dvd_def by blast - from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" - by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) - then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" - by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] - dvd_mult_div_cancel [OF dvdg(2)] dvd_def) - have "?g \ 0" using nz by simp - moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . - thm dvd_mult_cancel_left - ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp -qed - -lemma coprime: - "coprime a b \ (\d. d dvd a \ d dvd b \ is_unit d)" (is "?P \ ?Q") -proof - assume ?P then show ?Q by auto -next - assume ?Q - then have "is_unit (gcd a b) \ gcd a b dvd a \ gcd a b dvd b" - by blast - then have "is_unit (gcd a b)" - by simp - then show ?P - by simp -qed - -end - lemma coprime_nat: "coprime (a::nat) b \ (\d. d dvd a \ d dvd b \ d = 1)" using coprime [of a b] by simp @@ -1165,337 +1669,15 @@ using abs_dvd_iff abs_ge_zero apply blast done -lemma gcd_coprime_nat: - assumes z: "gcd (a::nat) b \ 0" and a: "a = a' * gcd a b" and - b: "b = b' * gcd a b" - shows "coprime a' b'" - - apply (subgoal_tac "a' = a div gcd a b") - apply (erule ssubst) - apply (subgoal_tac "b' = b div gcd a b") - apply (erule ssubst) - apply (rule div_gcd_coprime) - using z apply force - apply (subst (1) b) - using z apply force - apply (subst (1) a) - using z apply force - done - -lemma gcd_coprime_int: - assumes z: "gcd (a::int) b \ 0" and a: "a = a' * gcd a b" and - b: "b = b' * gcd a b" - shows "coprime a' b'" - apply (subgoal_tac "a' = a div gcd a b") - apply (erule ssubst) - apply (subgoal_tac "b' = b div gcd a b") - apply (erule ssubst) - apply (rule div_gcd_coprime) - using z apply force - apply (subst (1) b) - using z apply force - apply (subst (1) a) - using z apply force - done - -context semiring_gcd -begin - -lemma coprime_mult: - assumes da: "coprime d a" and db: "coprime d b" - shows "coprime d (a * b)" - apply (subst gcd.commute) - using da apply (subst gcd_mult_cancel) - apply (subst gcd.commute, assumption) - apply (subst gcd.commute, rule db) - done - -end - -lemma coprime_lmult_nat: - assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a" -proof - - have "gcd d a dvd gcd d (a * b)" - by (rule gcd_greatest, auto) - with dab show ?thesis - by auto -qed - -lemma coprime_lmult_int: - assumes "coprime (d::int) (a * b)" shows "coprime d a" -proof - - have "gcd d a dvd gcd d (a * b)" - by (rule gcd_greatest, auto) - with assms show ?thesis - by auto -qed - -lemma coprime_rmult_nat: - assumes "coprime (d::nat) (a * b)" shows "coprime d b" -proof - - have "gcd d b dvd gcd d (a * b)" - by (rule gcd_greatest, auto intro: dvd_mult) - with assms show ?thesis - by auto -qed - -lemma coprime_rmult_int: - assumes dab: "coprime (d::int) (a * b)" shows "coprime d b" -proof - - have "gcd d b dvd gcd d (a * b)" - by (rule gcd_greatest, auto intro: dvd_mult) - with dab show ?thesis - by auto -qed - -lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \ - coprime d a \ coprime d b" - using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b] - coprime_mult [of d a b] - by blast - -lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \ - coprime d a \ coprime d b" - using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b] - coprime_mult [of d a b] - by blast - -lemma coprime_power_int: - assumes "0 < n" shows "coprime (a :: int) (b ^ n) \ coprime a b" - using assms -proof (induct n) - case (Suc n) then show ?case - by (cases n) (simp_all add: coprime_mul_eq_int) -qed simp - -lemma gcd_coprime_exists_nat: - assumes nz: "gcd (a::nat) b \ 0" - shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ coprime a' b'" - apply (rule_tac x = "a div gcd a b" in exI) - apply (rule_tac x = "b div gcd a b" in exI) - using nz apply (auto simp add: div_gcd_coprime dvd_div_mult) -done - -lemma gcd_coprime_exists_int: - assumes nz: "gcd (a::int) b \ 0" - shows "\a' b'. a = a' * gcd a b \ b = b' * gcd a b \ coprime a' b'" - apply (rule_tac x = "a div gcd a b" in exI) - apply (rule_tac x = "b div gcd a b" in exI) - using nz apply (auto simp add: div_gcd_coprime) -done - -lemma coprime_exp_nat: "coprime (d::nat) a \ coprime d (a^n)" - by (induct n) (simp_all add: coprime_mult) - -lemma coprime_exp_int: "coprime (d::int) a \ coprime d (a^n)" - by (induct n) (simp_all add: coprime_mult) - -context semiring_gcd -begin - -lemma coprime_exp_left: - assumes "coprime a b" - shows "coprime (a ^ n) b" - using assms by (induct n) (simp_all add: gcd_mult_cancel) - -lemma coprime_exp2: - assumes "coprime a b" - shows "coprime (a ^ n) (b ^ m)" -proof (rule coprime_exp_left) - from assms show "coprime a (b ^ m)" - by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a]) -qed - -end - -lemma gcd_exp_nat: - "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n" -proof (cases "a = 0 \ b = 0") - case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power) -next - case False - then have "coprime (a div gcd a b) (b div gcd a b)" - by (auto simp: div_gcd_coprime) - then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" - by (simp add: coprime_exp2) - then have "gcd ((a div gcd a b)^n * (gcd a b)^n) - ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n" - by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral) - also have "(a div gcd a b)^n * (gcd a b)^n = a^n" - by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) - also have "(b div gcd a b)^n * (gcd a b)^n = b^n" - by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib) - finally show ?thesis . -qed - -lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n" - apply (subst (1 2) gcd_abs_int) - apply (subst (1 2) power_abs) - apply (rule gcd_exp_nat [where n = n, transferred]) - apply auto -done - -lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c" - shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" -proof- - let ?g = "gcd a b" - {assume "?g = 0" with dc have ?thesis by auto} - moreover - {assume z: "?g \ 0" - from gcd_coprime_exists_nat[OF z] - obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" - by blast - have thb: "?g dvd b" by auto - from ab'(1) have "a' dvd a" unfolding dvd_def by blast - with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp - from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto - hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc) - with z have th_1: "a' dvd b' * c" by auto - from coprime_dvd_mult [OF ab'(3)] th_1 - have thc: "a' dvd c" by (subst (asm) mult.commute, blast) - from ab' have "a = ?g*a'" by algebra - with thb thc have ?thesis by blast } - ultimately show ?thesis by blast -qed - -lemma division_decomp_int: assumes dc: "(a::int) dvd b * c" - shows "\b' c'. a = b' * c' \ b' dvd b \ c' dvd c" -proof- - let ?g = "gcd a b" - {assume "?g = 0" with dc have ?thesis by auto} - moreover - {assume z: "?g \ 0" - from gcd_coprime_exists_int[OF z] - obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" - by blast - have thb: "?g dvd b" by auto - from ab'(1) have "a' dvd a" unfolding dvd_def by blast - with dc have th0: "a' dvd b*c" - using dvd_trans[of a' a "b*c"] by simp - from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto - hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps) - with z have th_1: "a' dvd b' * c" by auto - from coprime_dvd_mult [OF ab'(3)] th_1 - have thc: "a' dvd c" by (subst (asm) mult.commute, blast) - from ab' have "a = ?g*a'" by algebra - with thb thc have ?thesis by blast } - ultimately show ?thesis by blast -qed - -lemma pow_divides_pow_nat: - assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \ 0" - shows "a dvd b" -proof- - let ?g = "gcd a b" - from n obtain m where m: "n = Suc m" by (cases n, simp_all) - {assume "?g = 0" with ab n have ?thesis by auto } - moreover - {assume z: "?g \ 0" - hence zn: "?g ^ n \ 0" using n by simp - from gcd_coprime_exists_nat[OF z] - obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" - by blast - from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" - by (simp add: ab'(1,2)[symmetric]) - hence "?g^n*a'^n dvd ?g^n *b'^n" - by (simp only: power_mult_distrib mult.commute) - then have th0: "a'^n dvd b'^n" - using zn by auto - have "a' dvd a'^n" by (simp add: m) - with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp - hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute) - from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1 - have "a' dvd b'" by (subst (asm) mult.commute, blast) - hence "a'*?g dvd b'*?g" by simp - with ab'(1,2) have ?thesis by simp } - ultimately show ?thesis by blast -qed - -lemma pow_divides_pow_int: - assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \ 0" - shows "a dvd b" -proof- - let ?g = "gcd a b" - from n obtain m where m: "n = Suc m" by (cases n, simp_all) - {assume "?g = 0" with ab n have ?thesis by auto } - moreover - {assume z: "?g \ 0" - hence zn: "?g ^ n \ 0" using n by simp - from gcd_coprime_exists_int[OF z] - obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" - by blast - from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" - by (simp add: ab'(1,2)[symmetric]) - hence "?g^n*a'^n dvd ?g^n *b'^n" - by (simp only: power_mult_distrib mult.commute) - with zn z n have th0:"a'^n dvd b'^n" by auto - have "a' dvd a'^n" by (simp add: m) - with th0 have "a' dvd b'^n" - using dvd_trans[of a' "a'^n" "b'^n"] by simp - hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute) - from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1 - have "a' dvd b'" by (subst (asm) mult.commute, blast) - hence "a'*?g dvd b'*?g" by simp - with ab'(1,2) have ?thesis by simp } - ultimately show ?thesis by blast -qed - lemma pow_divides_eq_nat [simp]: "n > 0 \ (a::nat) ^ n dvd b ^ n \ a dvd b" - by (auto intro: pow_divides_pow_nat dvd_power_same) - -lemma pow_divides_eq_int [simp]: - "n ~= 0 \ (a::int) ^ n dvd b ^ n \ a dvd b" - by (auto intro: pow_divides_pow_int dvd_power_same) - -context semiring_gcd -begin - -lemma divides_mult: - assumes "a dvd c" and nr: "b dvd c" and "coprime a b" - shows "a * b dvd c" -proof- - from \b dvd c\ obtain b' where"c = b * b'" .. - with \a dvd c\ have "a dvd b' * b" - by (simp add: ac_simps) - with \coprime a b\ have "a dvd b'" - by (simp add: coprime_dvd_mult_iff) - then obtain a' where "b' = a * a'" .. - with \c = b * b'\ have "c = (a * b) * a'" - by (simp add: ac_simps) - then show ?thesis .. -qed - -end - -lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n" - by (simp add: gcd.commute del: One_nat_def) + using pow_divs_eq[of n] by simp lemma coprime_Suc_nat [simp]: "coprime (Suc n) n" - using coprime_plus_one_nat by simp - -lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n" - by (simp add: gcd.commute) + using coprime_plus_one[of n] by simp lemma coprime_minus_one_nat: "(n::nat) \ 0 \ coprime (n - 1) n" - using coprime_plus_one_nat [of "n - 1"] - gcd.commute [of "n - 1" n] by auto - -lemma coprime_minus_one_int: "coprime ((n::int) - 1) n" - using coprime_plus_one_int [of "n - 1"] - gcd.commute [of "n - 1" n] by auto - -lemma setprod_coprime_nat: - fixes x :: nat - shows "(\i. i \ A \ coprime (f i) x) \ coprime (\i\A. f i) x" - by (induct A rule: infinite_finite_induct) - (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def) - -lemma setprod_coprime_int: - fixes x :: int - shows "(\i. i \ A \ coprime (f i) x) \ coprime (\i\A. f i) x" - by (induct A rule: infinite_finite_induct) - (auto simp add: gcd_mult_cancel) + using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto lemma coprime_common_divisor_nat: "coprime (a::nat) b \ x dvd a \ x dvd b \ x = 1" @@ -1505,15 +1687,11 @@ "coprime (a::int) b \ x dvd a \ x dvd b \ \x\ = 1" using gcd_greatest_iff [of x a b] by auto -lemma coprime_divisors_nat: - "(d::int) dvd a \ e dvd b \ coprime a b \ coprime d e" - by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int) - lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \ coprime x m" -by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat) +by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat) lemma invertible_coprime_int: "(x::int) * y mod m = 1 \ coprime x m" -by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int) +by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int) subsection \Bezout's theorem\ @@ -1763,7 +1941,7 @@ lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n" unfolding lcm_nat_def - by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat]) + by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod]) lemma prod_gcd_lcm_int: "\m::int\ * \n\ = gcd m n * lcm m n" unfolding lcm_int_def gcd_int_def @@ -1828,14 +2006,6 @@ lemma lcm_proj2_iff_int [simp]: "lcm m n = \n::int\ \ m dvd n" by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int) -lemma (in semiring_gcd) comp_fun_idem_gcd: - "comp_fun_idem gcd" - by standard (simp_all add: fun_eq_iff ac_simps) - -lemma (in semiring_gcd) comp_fun_idem_lcm: - "comp_fun_idem lcm" - by standard (simp_all add: fun_eq_iff ac_simps) - lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = Suc 0 \ m = Suc 0 \ n = Suc 0" using lcm_eq_1_iff [of m n] by simp @@ -2069,21 +2239,11 @@ text \Some code equations\ -lemma Lcm_set_nat [code, code_unfold]: - "Lcm (set ns) = fold lcm ns (1::nat)" - using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric]) - -lemma Gcd_set_nat [code]: - "Gcd (set ns) = fold gcd ns (0::nat)" - using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric]) +lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat] +lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat] +lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int] +lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int] -lemma Lcm_set_int [code, code_unfold]: - "Lcm (set xs) = fold lcm xs (1::int)" - using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric]) - -lemma Gcd_set_int [code]: - "Gcd (set xs) = fold gcd xs (0::int)" - using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric]) text \Fact aliasses\ diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Isar_Examples/Fibonacci.thy --- a/src/HOL/Isar_Examples/Fibonacci.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Isar_Examples/Fibonacci.thy Fri Feb 26 22:15:09 2016 +0100 @@ -80,7 +80,7 @@ also have "\ = fib (n + 2) + fib (n + 1)" by simp also have "gcd (fib (n + 2)) \ = gcd (fib (n + 2)) (fib (n + 1))" - by (rule gcd_add2_nat) + by (rule gcd_add2) also have "\ = gcd (fib (n + 1)) (fib (n + 1 + 1))" by (simp add: gcd.commute) also assume "\ = 1" diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Cong.thy Fri Feb 26 22:15:09 2016 +0100 @@ -529,11 +529,11 @@ lemma coprime_iff_invertible_nat: "m > 0 \ coprime a m = (EX x. [a * x = Suc 0] (mod m))" - by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult_nat gcd.commute gcd_Suc_0) + by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0) lemma coprime_iff_invertible_int: "m > (0::int) \ coprime a m = (EX x. [a * x = 1] (mod m))" apply (auto intro: cong_solve_coprime_int) - apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int) + apply (metis cong_int_def coprime_mul_eq gcd_1_int gcd.commute gcd_red_int) done lemma coprime_iff_invertible'_nat: "m > 0 \ coprime a m = @@ -568,7 +568,7 @@ [x = y] (mod (\i\A. m i))" apply (induct set: finite) apply auto - apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat) + apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime) done lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \ @@ -577,7 +577,7 @@ [x = y] (mod (\i\A. m i))" apply (induct set: finite) apply auto - apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int) + apply (metis coprime_cong_mult_int gcd.commute setprod_coprime) done lemma binary_chinese_remainder_aux_nat: @@ -760,7 +760,7 @@ fix i assume "i : A" with cop have "coprime (\j \ A - {i}. m j) (m i)" - by (intro setprod_coprime_nat, auto) + by (intro setprod_coprime, auto) then have "EX x. [(\j \ A - {i}. m j) * x = 1] (mod m i)" by (elim cong_solve_coprime_nat) then obtain x where "[(\j \ A - {i}. m j) * x = 1] (mod m i)" @@ -824,7 +824,7 @@ [x = y] (mod (\i\A. m i))" apply (induct set: finite) apply auto - apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat) + apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime) done lemma chinese_remainder_unique_nat: diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Fri Feb 26 22:15:09 2016 +0100 @@ -3,7 +3,7 @@ section \Abstract euclidean algorithm\ theory Euclidean_Algorithm -imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial" +imports "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial" begin text \ @@ -309,56 +309,14 @@ subclass semiring_Gcd by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least) - lemma gcd_non_0: "b \ 0 \ gcd a b = gcd b (a mod b)" unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0) lemmas gcd_0 = gcd_0_right lemmas dvd_gcd_iff = gcd_greatest_iff - lemmas gcd_greatest_iff = dvd_gcd_iff -lemma gcdI: - assumes "c dvd a" and "c dvd b" and greatest: "\d. d dvd a \ d dvd b \ d dvd c" - and "normalize c = c" - shows "c = gcd a b" - by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) - -lemma gcd_unique: "d dvd a \ d dvd b \ - normalize d = d \ - (\e. e dvd a \ e dvd b \ e dvd d) \ d = gcd a b" - by rule (auto intro: gcdI simp: gcd_greatest) - -lemma gcd_dvd_prod: "gcd a b dvd k * b" - using mult_dvd_mono [of 1] by auto - -lemma gcd_proj2_if_dvd: - "b dvd a \ gcd a b = normalize b" - by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0) - -lemma gcd_proj1_if_dvd: - "a dvd b \ gcd a b = normalize a" - by (subst gcd.commute, simp add: gcd_proj2_if_dvd) - -lemma gcd_proj1_iff: "gcd m n = normalize m \ m dvd n" -proof - assume A: "gcd m n = normalize m" - show "m dvd n" - proof (cases "m = 0") - assume [simp]: "m \ 0" - from A have B: "m = gcd m n * unit_factor m" - by (simp add: unit_eq_div2) - show ?thesis by (subst B, simp add: mult_unit_dvd_iff) - qed (insert A, simp) -next - assume "m dvd n" - then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd) -qed - -lemma gcd_proj2_iff: "gcd m n = normalize n \ n dvd m" - using gcd_proj1_iff [of n m] by (simp add: ac_simps) - lemma gcd_mod1 [simp]: "gcd (a mod b) b = gcd a b" by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) @@ -367,39 +325,6 @@ "gcd a (b mod a) = gcd a b" by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff) -lemma gcd_mult_distrib': - "normalize c * gcd a b = gcd (c * a) (c * b)" -proof (cases "c = 0") - case True then show ?thesis by simp_all -next - case False then have [simp]: "is_unit (unit_factor c)" by simp - show ?thesis - proof (induct a b rule: gcd_eucl_induct) - case (zero a) show ?case - proof (cases "a = 0") - case True then show ?thesis by simp - next - case False - then show ?thesis by (simp add: normalize_mult) - qed - case (mod a b) - then show ?case by (simp add: mult_mod_right gcd.commute) - qed -qed - -lemma gcd_mult_distrib: - "k * gcd a b = gcd (k * a) (k * b) * unit_factor k" -proof- - have "normalize k * gcd a b = gcd (k * a) (k * b)" - by (simp add: gcd_mult_distrib') - then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k" - by simp - then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k" - by (simp only: ac_simps) - then show ?thesis - by simp -qed - lemma euclidean_size_gcd_le1 [simp]: assumes "a \ 0" shows "euclidean_size (gcd a b) \ euclidean_size a" @@ -431,408 +356,13 @@ shows "euclidean_size (gcd a b) < euclidean_size b" using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) -lemma gcd_mult_unit1: "is_unit a \ gcd (b * a) c = gcd b c" - apply (rule gcdI) - apply simp_all - apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps) - done - -lemma gcd_mult_unit2: "is_unit a \ gcd b (c * a) = gcd b c" - by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute) - -lemma gcd_div_unit1: "is_unit a \ gcd (b div a) c = gcd b c" - by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) - -lemma gcd_div_unit2: "is_unit a \ gcd b (c div a) = gcd b c" - by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) - -lemma normalize_gcd_left [simp]: - "gcd (normalize a) b = gcd a b" -proof (cases "a = 0") - case True then show ?thesis - by simp -next - case False then have "is_unit (unit_factor a)" - by simp - moreover have "normalize a = a div unit_factor a" - by simp - ultimately show ?thesis - by (simp only: gcd_div_unit1) -qed - -lemma normalize_gcd_right [simp]: - "gcd a (normalize b) = gcd a b" - using normalize_gcd_left [of b a] by (simp add: ac_simps) - -lemma gcd_idem: "gcd a a = normalize a" - by (cases "a = 0") (simp, rule sym, rule gcdI, simp_all) - -lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b" - apply (rule gcdI) - apply (simp add: ac_simps) - apply (rule gcd_dvd2) - apply (rule gcd_greatest, erule (1) gcd_greatest, assumption) - apply simp - done - -lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b" - apply (rule gcdI) - apply simp - apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2) - apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption) - apply simp - done - -lemma comp_fun_idem_gcd: "comp_fun_idem gcd" -proof - fix a b show "gcd a \ gcd b = gcd b \ gcd a" - by (simp add: fun_eq_iff ac_simps) -next - fix a show "gcd a \ gcd a = gcd a" - by (simp add: fun_eq_iff gcd_left_idem) -qed - -lemma gcd_dvd_antisym: - "gcd a b dvd gcd c d \ gcd c d dvd gcd a b \ gcd a b = gcd c d" -proof (rule gcdI) - assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b" - have "gcd c d dvd c" by simp - with A show "gcd a b dvd c" by (rule dvd_trans) - have "gcd c d dvd d" by simp - with A show "gcd a b dvd d" by (rule dvd_trans) - show "normalize (gcd a b) = gcd a b" - 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) -qed - -lemma coprime_crossproduct: - assumes [simp]: "gcd a d = 1" "gcd b c = 1" - shows "normalize (a * c) = normalize (b * d) \ normalize a = normalize b \ normalize c = normalize d" - (is "?lhs \ ?rhs") -proof - assume ?rhs - then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd) - then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+ - then show ?lhs by (simp add: associated_iff_dvd) -next - assume ?lhs - then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd) - then have "a dvd b * d" by (metis dvd_mult_left) - hence "a dvd b" by (simp add: coprime_dvd_mult_iff) - moreover from dvd have "b dvd a * c" by (metis dvd_mult_left) - hence "b dvd a" by (simp add: coprime_dvd_mult_iff) - moreover from dvd have "c dvd d * b" - 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 dvd have "d dvd c * a" - 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 by (simp add: associated_iff_dvd) -qed - -lemma gcd_add1 [simp]: - "gcd (m + n) n = gcd m n" - by (cases "n = 0", simp_all add: gcd_non_0) - -lemma gcd_add2 [simp]: - "gcd m (m + n) = gcd m n" - using gcd_add1 [of n m] by (simp add: ac_simps) - -lemma gcd_add_mult: - "gcd m (k * m + n) = gcd m n" -proof - - have "gcd m ((k * m + n) mod m) = gcd m (k * m + n)" - by (fact gcd_mod2) - then show ?thesis by simp -qed - -lemma coprimeI: "(\l. \l dvd a; l dvd b\ \ l dvd 1) \ gcd a b = 1" - by (rule sym, rule gcdI, simp_all) - -lemma coprime: "gcd a b = 1 \ (\d. d dvd a \ d dvd b \ is_unit d)" - by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2) - -lemma div_gcd_coprime: - assumes nz: "a \ 0 \ b \ 0" - defines [simp]: "d \ gcd a b" - defines [simp]: "a' \ a div d" and [simp]: "b' \ b div d" - shows "gcd a' b' = 1" -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 - ultimately have "a = (l * d) * s" "b = (l * d) * t" - 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 "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_lmult: - assumes dab: "gcd d (a * b) = 1" - shows "gcd d a = 1" -proof (rule coprimeI) - fix l assume "l dvd d" and "l dvd a" - hence "l dvd a * b" by simp - with \l dvd d\ and dab show "l dvd 1" by (auto intro: gcd_greatest) -qed - -lemma coprime_rmult: - assumes dab: "gcd d (a * b) = 1" - shows "gcd d b = 1" -proof (rule coprimeI) - fix l assume "l dvd d" and "l dvd b" - hence "l dvd a * b" by simp - with \l dvd d\ and dab show "l dvd 1" by (auto intro: gcd_greatest) -qed - -lemma coprime_mul_eq: "gcd d (a * b) = 1 \ gcd d a = 1 \ gcd d b = 1" - using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast - -lemma gcd_coprime: - assumes c: "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 c 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)+ - finally show ?thesis . -qed - -lemma coprime_power: - assumes "0 < n" - shows "gcd a (b ^ n) = 1 \ gcd a b = 1" -using assms proof (induct n) - case (Suc n) then show ?case - by (cases n) (simp_all add: coprime_mul_eq) -qed simp - -lemma gcd_coprime_exists: - assumes nz: "gcd a b \ 0" - 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 intro: div_gcd_coprime) - done - -lemma coprime_exp: - "gcd d a = 1 \ gcd d (a^n) = 1" - by (induct n, simp_all add: coprime_mult) - -lemma gcd_exp: - "gcd (a ^ n) (b ^ n) = gcd a b ^ n" -proof (cases "a = 0 \ b = 0") - case True - then show ?thesis by (cases n) simp_all -next - case False - then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" - using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp - then have "gcd a b ^ n = gcd a b ^ n * ..." by simp - also note gcd_mult_distrib - also have "unit_factor (gcd a b ^ n) = 1" - using False by (auto simp add: unit_factor_power unit_factor_gcd) - also have "(gcd a b)^n * (a div gcd a b)^n = a^n" - by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) - also have "(gcd a b)^n * (b div gcd a b)^n = b^n" - by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp) - finally show ?thesis by simp -qed - -lemma coprime_common_divisor: - "gcd a b = 1 \ a dvd a \ a dvd b \ is_unit a" - apply (subgoal_tac "a dvd gcd a b") - apply simp - apply (erule (1) gcd_greatest) - done - -lemma division_decomp: - assumes dc: "a dvd b * c" - 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 - hence "a = 0 * c \ 0 dvd b \ c dvd c" by simp - then show ?thesis by blast -next - let ?d = "gcd a b" - assume "?d \ 0" - from gcd_coprime_exists[OF this] - obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1" - by blast - from ab'(1) have "a' dvd a" unfolding dvd_def by blast - 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 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) - then show ?thesis by blast -qed - -lemma pow_divs_pow: - assumes ab: "a ^ n dvd b ^ n" and n: "n \ 0" - shows "a dvd b" -proof (cases "gcd a b = 0") - assume "gcd a b = 0" - 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 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 - from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n" - 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 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]] - have "a' dvd b'" by (subst (asm) ac_simps, blast) - hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp) - with ab'(1,2) show ?thesis by simp -qed - -lemma pow_divs_eq [simp]: - "n \ 0 \ a ^ n dvd b ^ n \ a dvd b" - by (auto intro: pow_divs_pow dvd_power_same) - -lemmas divs_mult = divides_mult - -lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1" - by (subst add_commute, simp) - -lemma setprod_coprime [rule_format]: - "(\i\A. gcd (f i) a = 1) \ gcd (\i\A. f i) a = 1" - apply (cases "finite A") - apply (induct set: finite) - apply (auto simp add: gcd_mult_cancel) - done - -lemma listprod_coprime: - "(\x. x \ set xs \ coprime x y) \ coprime (listprod xs) y" - by (induction xs) (simp_all add: gcd_mult_cancel) - -lemma coprime_divisors: - assumes "d dvd a" "e dvd b" "gcd a b = 1" - shows "gcd d e = 1" -proof - - from assms obtain k l where "a = d * k" "b = e * l" - unfolding dvd_def by blast - with assms have "gcd (d * k) (e * l) = 1" by simp - hence "gcd (d * k) e = 1" by (rule coprime_lmult) - also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps) - finally have "gcd e d = 1" by (rule coprime_lmult) - then show ?thesis by (simp add: ac_simps) -qed - -lemma invertible_coprime: - assumes "a * b mod m = 1" - shows "coprime a m" -proof - - from assms have "coprime m (a * b mod m)" - by simp - then have "coprime m (a * b)" - by simp - then have "coprime m a" - by (rule coprime_lmult) - then show ?thesis - by (simp add: ac_simps) -qed - -lemma lcm_gcd_prod: - "lcm a b * gcd a b = normalize (a * b)" - by (simp add: lcm_gcd) - -lemma lcm_zero: - "lcm a b = 0 \ a = 0 \ b = 0" - by (fact lcm_eq_0_iff) - -lemmas lcm_0_iff = lcm_zero - -lemma gcd_lcm: - assumes "lcm a b \ 0" - shows "gcd a b = normalize (a * b) div lcm a b" -proof - - have "lcm a b * gcd a b = normalize (a * b)" - by (fact lcm_gcd_prod) - with assms show ?thesis - by (metis nonzero_mult_divide_cancel_left) -qed - -declare unit_factor_lcm [simp] - -lemma lcmI: - assumes "a dvd c" and "b dvd c" and "\d. a dvd d \ b dvd d \ c dvd d" - and "normalize c = c" - shows "c = lcm a b" - by (rule associated_eqI) (auto simp: assms intro: lcm_least) - -lemma gcd_dvd_lcm [simp]: - "gcd a b dvd lcm a b" - using gcd_dvd2 by (rule dvd_lcmI2) - -lemmas lcm_0 = lcm_0_right - -lemma lcm_unique: - "a dvd d \ b dvd d \ - normalize d = d \ - (\e. a dvd e \ b dvd e \ d dvd e) \ d = lcm a b" - by rule (auto intro: lcmI simp: lcm_least lcm_zero) - -lemma lcm_coprime: - "gcd a b = 1 \ lcm a b = normalize (a * b)" - by (subst lcm_gcd) simp - -lemma lcm_proj1_if_dvd: - "b dvd a \ lcm a b = normalize a" - by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all) - -lemma lcm_proj2_if_dvd: - "a dvd b \ lcm a b = normalize b" - using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) - -lemma lcm_proj1_iff: - "lcm m n = normalize m \ n dvd m" -proof - assume A: "lcm m n = normalize m" - show "n dvd m" - proof (cases "m = 0") - assume [simp]: "m \ 0" - from A have B: "m = lcm m n * unit_factor m" - by (simp add: unit_eq_div2) - show ?thesis by (subst B, simp) - qed simp -next - assume "n dvd m" - then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd) -qed - -lemma lcm_proj2_iff: - "lcm m n = normalize n \ m dvd n" - using lcm_proj1_iff [of n m] by (simp add: ac_simps) - lemma euclidean_size_lcm_le1: assumes "a \ 0" and "b \ 0" shows "euclidean_size a \ euclidean_size (lcm a b)" proof - have "a dvd lcm a b" by (rule dvd_lcm1) then obtain c where A: "lcm a b = a * c" .. - with \a \ 0\ and \b \ 0\ have "c \ 0" by (auto simp: lcm_zero) + with \a \ 0\ and \b \ 0\ have "c \ 0" by (auto simp: lcm_eq_0_iff) then show ?thesis by (subst A, intro size_mult_mono) qed @@ -849,7 +379,7 @@ with \a \ 0\ and \b \ 0\ have "euclidean_size (lcm a b) = euclidean_size a" by (intro le_antisym, simp, intro euclidean_size_lcm_le1) with assms have "lcm a b dvd a" - by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero) + by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff) hence "b dvd a" by (rule lcm_dvdD2) with \\b dvd a\ show False by contradiction qed @@ -859,197 +389,14 @@ shows "euclidean_size b < euclidean_size (lcm a b)" using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) -lemma lcm_mult_unit1: - "is_unit a \ lcm (b * a) c = lcm b c" - by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1) - -lemma lcm_mult_unit2: - "is_unit a \ lcm b (c * a) = lcm b c" - using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) - -lemma lcm_div_unit1: - "is_unit a \ lcm (b div a) c = lcm b c" - by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) - -lemma lcm_div_unit2: - "is_unit a \ lcm b (c div a) = lcm b c" - by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) - -lemma normalize_lcm_left [simp]: - "lcm (normalize a) b = lcm a b" -proof (cases "a = 0") - case True then show ?thesis - by simp -next - case False then have "is_unit (unit_factor a)" - by simp - moreover have "normalize a = a div unit_factor a" - by simp - ultimately show ?thesis - by (simp only: lcm_div_unit1) -qed - -lemma normalize_lcm_right [simp]: - "lcm a (normalize b) = lcm a b" - using normalize_lcm_left [of b a] by (simp add: ac_simps) - -lemma LcmI: - assumes "\a. a \ A \ a dvd b" and "\c. (\a. a \ A \ a dvd c) \ b dvd c" - and "normalize b = b" shows "b = Lcm A" - by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least) - -lemma Lcm_subset: - "A \ B \ Lcm A dvd Lcm B" - by (blast intro: Lcm_least dvd_Lcm) - -lemma Lcm_Un: - "Lcm (A \ B) = lcm (Lcm A) (Lcm B)" - apply (rule lcmI) - apply (blast intro: Lcm_subset) - apply (blast intro: Lcm_subset) - apply (intro Lcm_least ballI, elim UnE) - apply (rule dvd_trans, erule dvd_Lcm, assumption) - apply (rule dvd_trans, erule dvd_Lcm, assumption) - apply simp - done - -lemma Lcm_no_units: - "Lcm A = Lcm (A - {a. is_unit a})" -proof - - have "(A - {a. is_unit a}) \ {a\A. is_unit a} = A" by blast - hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\A. is_unit a})" - by (simp add: Lcm_Un [symmetric]) - also have "Lcm {a\A. is_unit a} = 1" by (simp add: Lcm_1_iff) - finally show ?thesis by simp -qed - -lemma Lcm_0_iff': - "Lcm A = 0 \ \(\l. l \ 0 \ (\a\A. a dvd l))" -proof - assume "Lcm A = 0" - show "\(\l. l \ 0 \ (\a\A. a dvd l))" - proof - assume ex: "\l. l \ 0 \ (\a\A. a dvd l)" - then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\a\A. a dvd l\<^sub>0)" by blast - def n \ "LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" - def l \ "SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" - have "\l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" - apply (subst n_def) - apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) - apply (rule exI[of _ l\<^sub>0]) - apply (simp add: l\<^sub>0_props) - done - from someI_ex[OF this] have "l \ 0" unfolding l_def by simp_all - hence "normalize l \ 0" by simp - also from ex have "normalize l = Lcm A" - by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def) - finally show False using \Lcm A = 0\ by contradiction - qed -qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) - -lemma Lcm_no_multiple: - "(\m. m \ 0 \ (\a\A. \a dvd m)) \ Lcm A = 0" -proof - - assume "\m. m \ 0 \ (\a\A. \a dvd m)" - hence "\(\l. l \ 0 \ (\a\A. a dvd l))" by blast - then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False) -qed - -lemma Lcm_finite: - assumes "finite A" - shows "Lcm A = Finite_Set.fold lcm 1 A" - by (induct rule: finite.induct[OF \finite A\]) - (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm]) - -lemma Lcm_set: - "Lcm (set xs) = foldl lcm 1 xs" - using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite - by (simp add: foldl_conv_fold lcm.commute) - lemma Lcm_eucl_set [code]: "Lcm_eucl (set xs) = foldl lcm_eucl 1 xs" by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set) -lemma Lcm_singleton [simp]: - "Lcm {a} = normalize a" - by simp - -lemma Lcm_2 [simp]: - "Lcm {a,b} = lcm a b" - by simp - -lemma Lcm_coprime: - assumes "finite A" and "A \ {}" - assumes "\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1" - shows "Lcm A = normalize (\A)" -using assms proof (induct rule: finite_ne_induct) - case (insert a A) - have "Lcm (insert a A) = lcm a (Lcm A)" by simp - also from insert have "Lcm A = normalize (\A)" by blast - also have "lcm a \ = lcm a (\A)" by (cases "\A = 0") (simp_all add: lcm_div_unit2) - also from insert have "gcd a (\A) = 1" by (subst gcd.commute, intro setprod_coprime) auto - with insert have "lcm a (\A) = normalize (\(insert a A))" - by (simp add: lcm_coprime) - finally show ?case . -qed simp - -lemma Lcm_coprime': - "card A \ 0 \ (\a b. a \ A \ b \ A \ a \ b \ gcd a b = 1) - \ Lcm A = normalize (\A)" - by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) - -lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" -proof - - show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" - by (simp add: Gcd_Lcm unit_factor_Lcm) -qed - -lemma GcdI: - assumes "\a. a \ A \ b dvd a" and "\c. (\a. a \ A \ c dvd a) \ c dvd b" - and "normalize b = b" - shows "b = Gcd A" - by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) - -lemma Gcd_1: - "1 \ A \ Gcd A = 1" - by (auto intro!: Gcd_eq_1_I) - -lemma Gcd_finite: - assumes "finite A" - shows "Gcd A = Finite_Set.fold gcd 0 A" - by (induct rule: finite.induct[OF \finite A\]) - (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd]) - -lemma Gcd_set: - "Gcd (set xs) = foldl gcd 0 xs" - using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite - by (simp add: foldl_conv_fold gcd.commute) - lemma Gcd_eucl_set [code]: "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs" by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set) -lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" - by simp - -lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b" - by simp - - -definition pairwise_coprime where - "pairwise_coprime A = (\x y. x \ A \ y \ A \ x \ y \ coprime x y)" - -lemma pairwise_coprimeI [intro?]: - "(\x y. x \ A \ y \ A \ x \ y \ coprime x y) \ pairwise_coprime A" - by (simp add: pairwise_coprime_def) - -lemma pairwise_coprimeD: - "pairwise_coprime A \ x \ A \ y \ A \ x \ y \ coprime x y" - by (simp add: pairwise_coprime_def) - -lemma pairwise_coprime_subset: "pairwise_coprime A \ B \ A \ pairwise_coprime B" - by (force simp: pairwise_coprime_def) - end text \ @@ -1084,48 +431,6 @@ lemma bezout: "\s t. s * a + t * b = gcd a b" using euclid_ext'_correct by blast -lemma gcd_neg1 [simp]: - "gcd (-a) b = gcd a b" - by (rule sym, rule gcdI, simp_all add: gcd_greatest) - -lemma gcd_neg2 [simp]: - "gcd a (-b) = gcd a b" - by (rule sym, rule gcdI, simp_all add: gcd_greatest) - -lemma gcd_neg_numeral_1 [simp]: - "gcd (- numeral n) a = gcd (numeral n) a" - by (fact gcd_neg1) - -lemma gcd_neg_numeral_2 [simp]: - "gcd a (- numeral n) = gcd a (numeral n)" - by (fact gcd_neg2) - -lemma gcd_diff1: "gcd (m - n) n = gcd m n" - by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) - -lemma gcd_diff2: "gcd (n - m) n = gcd m n" - by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1) - -lemma coprime_minus_one [simp]: "gcd (n - 1) n = 1" -proof - - have "gcd (n - 1) n = gcd n (n - 1)" by (fact gcd.commute) - also have "\ = gcd ((n - 1) + 1) (n - 1)" by simp - also have "\ = 1" by (rule coprime_plus_one) - finally show ?thesis . -qed - -lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b" - by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) - -lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b" - by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero) - -lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a" - by (fact lcm_neg1) - -lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)" - by (fact lcm_neg2) - end diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Fib.thy --- a/src/HOL/Number_Theory/Fib.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Fib.thy Fri Feb 26 22:15:09 2016 +0100 @@ -59,7 +59,7 @@ lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))" apply (induct n rule: fib.induct) apply auto - apply (metis gcd_add1_nat add.commute) + apply (metis gcd_add1 add.commute) done lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)" @@ -67,7 +67,7 @@ apply (cases m) apply (auto simp add: fib_add) apply (metis gcd.commute mult.commute coprime_fib_Suc_nat - gcd_add_mult_nat gcd_mult_cancel gcd.commute) + gcd_add_mult gcd_mult_cancel gcd.commute) done lemma gcd_fib_diff: "m \ n \ gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)" diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Gauss.thy --- a/src/HOL/Number_Theory/Gauss.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Gauss.thy Fri Feb 26 22:15:09 2016 +0100 @@ -205,7 +205,7 @@ by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int) lemma A_prod_relprime: "gcd (setprod id A) p = 1" - by (metis id_def all_A_relprime setprod_coprime_int) + by (metis id_def all_A_relprime setprod_coprime) subsection \Relationships Between Gauss Sets\ diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Pocklington.thy --- a/src/HOL/Number_Theory/Pocklington.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Pocklington.thy Fri Feb 26 22:15:09 2016 +0100 @@ -130,7 +130,7 @@ have "coprime x a" "coprime x b" by (metis cong_gcd_eq_nat)+ then have "coprime x (a*b)" - by (metis coprime_mul_eq_nat) + by (metis coprime_mul_eq) with x show ?thesis by blast qed @@ -242,7 +242,7 @@ from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1" by simp from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1 have an: "coprime a n" "coprime (a^(n - 1)) n" - by (auto simp add: coprime_exp_nat gcd.commute) + by (auto simp add: coprime_exp gcd.commute) {assume H0: "\m. 0 < m \ m < n - 1 \ [a ^ m = 1] (mod n)" (is "EX m. ?P m") from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\k ?P k" by blast @@ -251,7 +251,7 @@ let ?y = "a^ ((n - 1) div m * m)" note mdeq = mod_div_equality[of "(n - 1)" m] have yn: "coprime ?y n" - by (metis an(1) coprime_exp_nat gcd.commute) + by (metis an(1) coprime_exp gcd.commute) have "?y mod n = (a^m)^((n - 1) div m) mod n" by (simp add: algebra_simps power_mult) also have "\ = (a^m mod n)^((n - 1) div m) mod n" @@ -417,9 +417,9 @@ from na have an: "coprime a n" by (metis gcd.commute) have aen: "coprime (a^e) n" - by (metis coprime_exp_nat gcd.commute na) + by (metis coprime_exp gcd.commute na) have acn: "coprime (a^c) n" - by (metis coprime_exp_nat gcd.commute na) + by (metis coprime_exp gcd.commute na) have "[a^d = a^e] (mod n) \ [a^(e + c) = a^(e + 0)] (mod n)" using c by simp also have "\ \ [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add) @@ -587,7 +587,7 @@ by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} hence cpa: "coprime p a" by auto have arp: "coprime (a^r) p" - by (metis coprime_exp_nat cpa gcd.commute) + by (metis coprime_exp cpa gcd.commute) from euler_theorem_nat[OF arp, simplified ord_divides] o phip have "q dvd (p - 1)" by simp then obtain d where d:"p - 1 = q * d" diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/Primes.thy Fri Feb 26 22:15:09 2016 +0100 @@ -152,11 +152,11 @@ lemma prime_imp_power_coprime_nat: "prime p \ ~ p dvd a \ coprime a (p^m)" - by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat) + by (metis coprime_exp gcd.commute prime_imp_coprime_nat) lemma prime_imp_power_coprime_int: fixes a::int shows "prime p \ ~ p dvd a \ coprime a (p^m)" - by (metis coprime_exp_int gcd.commute prime_imp_coprime_int) + by (metis coprime_exp gcd.commute prime_imp_coprime_int) lemma primes_coprime_nat: "prime p \ prime q \ p \ q \ coprime p q" by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat) @@ -203,7 +203,7 @@ with p have "coprime b p" by (subst gcd.commute, intro prime_imp_coprime_nat) then have pnb: "coprime (p^n) b" - by (subst gcd.commute, rule coprime_exp_nat) + by (subst gcd.commute, rule coprime_exp) from coprime_dvd_mult[OF pnb pab] have ?thesis by blast } moreover { assume pb: "p dvd b" @@ -213,7 +213,7 @@ with p have "coprime a p" by (subst gcd.commute, intro prime_imp_coprime_nat) then have pna: "coprime (p^n) a" - by (subst gcd.commute, rule coprime_exp_nat) + by (subst gcd.commute, rule coprime_exp) from coprime_dvd_mult[OF pna pnba] have ?thesis by blast } ultimately have ?thesis by blast } ultimately show ?thesis by blast @@ -374,7 +374,7 @@ lemma bezout_gcd_nat: fixes a::nat shows "\x y. a * x - b * y = gcd a b \ b * x - a * y = gcd a b" using bezout_nat[of a b] -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute +by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute gcd_nat.right_neutral mult_0) lemma gcd_bezout_sum_nat: diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Fri Feb 26 18:33:01 2016 +0100 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Feb 26 22:15:09 2016 +0100 @@ -99,7 +99,7 @@ moreover have "coprime (a ^ count M a) (\i \ (set_mset N - {a}). i ^ count N i)" apply (subst gcd.commute) - apply (rule setprod_coprime_nat) + apply (rule setprod_coprime) apply (rule primes_imp_powers_coprime_nat) using assms True apply auto