--- 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 \<Rightarrow> int) = Lcm" ..
-
+
+lemma [code, code del]:
+ "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
+
+lemma [code, code del]:
+ "(Lcm :: _ poly set \<Rightarrow> _) = 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: ...',
--- 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: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> 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 \<and> d dvd b \<and>
+ normalize d = d \<and>
+ (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<Longrightarrow> gcd a b = normalize b"
+ by (rule gcdI [symmetric]) simp_all
+
+lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a"
+ by (rule gcdI [symmetric]) simp_all
+
+lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
+proof
+ assume A: "gcd m n = normalize m"
+ show "m dvd n"
+ proof (cases "m = 0")
+ assume [simp]: "m \<noteq> 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 \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> 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 \<open>coprime a b\<close> mult_gcd_left [of c a b]
+ have "gcd (c * a) (c * b) * unit_factor c = c"
+ by (simp add: ac_simps)
+ moreover from \<open>a dvd c * b\<close> 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 \<longleftrightarrow> a dvd b"
+ using assms by (auto intro: coprime_dvd_mult)
+
+lemma gcd_mult_cancel:
+ "coprime c b \<Longrightarrow> 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
+ \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume ?rhs then show ?lhs by simp
+next
+ assume ?lhs
+ from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
+ by (auto intro: dvdI dest: sym)
+ with \<open>coprime a d\<close> have "a dvd b"
+ by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
+ by (auto intro: dvdI dest: sym)
+ with \<open>coprime b c\<close> have "b dvd a"
+ by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
+ by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime b c\<close> have "c dvd d"
+ by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
+ by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime a d\<close> have "d dvd c"
+ by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
+ from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
+ by (rule associatedI)
+ moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> 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: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
+ by (rule sym, rule gcdI, simp_all)
+
+lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
+ by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
+
+lemma div_gcd_coprime:
+ assumes nz: "a \<noteq> 0 \<or> b \<noteq> 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 \<noteq> 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 \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
+ with \<open>a dvd c\<close> have "a dvd b' * b"
+ by (simp add: ac_simps)
+ with \<open>coprime a b\<close> have "a dvd b'"
+ by (simp add: coprime_dvd_mult_iff)
+ then obtain a' where "b' = a * a'" ..
+ with \<open>c = b * b'\<close> 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 \<open>l dvd d\<close> 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 \<open>l dvd d\<close> 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 \<longleftrightarrow> gcd d a = 1 \<and> 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 \<noteq> 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 \<noteq> 0 \<or> b \<noteq> 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 \<longleftrightarrow> 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 \<noteq> 0"
+ shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<Longrightarrow> 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 \<and> 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 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof (cases "gcd a b = 0")
+ assume "gcd a b = 0"
+ hence "a = 0 \<and> b = 0" by simp
+ hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
+ then show ?thesis by blast
+next
+ let ?d = "gcd a b"
+ assume "?d \<noteq> 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 \<open>?d \<noteq> 0\<close> 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' \<and> ?d dvd b \<and> 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 \<noteq> 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 \<noteq> 0"
+ from n obtain m where m: "n = Suc m" by (cases n, simp_all)
+ from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
+ from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
+ 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 \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> 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]:
+ "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
+ apply (cases "finite A")
+ apply (induct set: finite)
+ apply (auto simp add: gcd_mult_cancel)
+ done
+
+lemma listprod_coprime:
+ "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> 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 "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> 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 \<and> b dvd d \<and>
+ normalize d = d \<and>
+ (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
+ by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
+
+lemma lcm_coprime:
+ "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
+ by (subst lcm_gcd) simp
+
+lemma lcm_proj1_if_dvd:
+ "b dvd a \<Longrightarrow> lcm a b = normalize a"
+ by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
+
+lemma lcm_proj2_if_dvd:
+ "a dvd b \<Longrightarrow> 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 \<longleftrightarrow> n dvd m"
+proof
+ assume A: "lcm m n = normalize m"
+ show "n dvd m"
+ proof (cases "m = 0")
+ assume [simp]: "m \<noteq> 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 \<longleftrightarrow> 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 \<in> A \<Longrightarrow> Gcd A dvd a"
@@ -471,6 +1010,27 @@
by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
qed
+lemma LcmI:
+ assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> 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 \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
+ by (blast intro: Lcm_least dvd_Lcm)
+
+lemma Lcm_Un:
+ "Lcm (A \<union> 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 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
proof
@@ -518,20 +1078,6 @@
by simp
qed
-lemma unit_factor_Gcd:
- "unit_factor (Gcd A) = (if \<forall>a\<in>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 "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> 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 \<in> 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 \<open>finite A\<close>])
+ (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 \<open>finite A\<close>])
+ (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}) \<union> {a\<in>A. is_unit a} = A" by blast
+ hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
+ by (simp add: Lcm_Un [symmetric])
+ also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
+ finally show ?thesis by simp
+qed
+
+lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
+ by (metis Lcm_least dvd_0_left dvd_Lcm)
+
+lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> 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 \<noteq> {}"
+ assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
+ shows "Lcm A = normalize (\<Prod>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 (\<Prod>A)" by blast
+ also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
+ also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
+ with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
+ by (simp add: lcm_coprime)
+ finally show ?case .
+qed simp
+
+lemma Lcm_coprime':
+ "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
+ \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
+ by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
+
+lemma Gcd_1:
+ "1 \<in> A \<Longrightarrow> 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 = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
+
+lemma pairwise_coprimeI [intro?]:
+ "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
+ by (simp add: pairwise_coprime_def)
+
+lemma pairwise_coprimeD:
+ "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
+ by (simp add: pairwise_coprime_def)
+
+lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
+ by (force simp: pairwise_coprime_def)
+
end
subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
@@ -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 \<open>coprime a b\<close> mult_gcd_left [of c a b]
- have "gcd (c * a) (c * b) * unit_factor c = c"
- by (simp add: ac_simps)
- moreover from \<open>a dvd c * b\<close> 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 \<longleftrightarrow> a dvd b"
- using assms by (auto intro: coprime_dvd_mult)
-
-lemma gcd_mult_cancel:
- "coprime c b \<Longrightarrow> 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
- \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?rhs then show ?lhs by simp
-next
- assume ?lhs
- from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
- by (auto intro: dvdI dest: sym)
- with \<open>coprime a d\<close> have "a dvd b"
- by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
- by (auto intro: dvdI dest: sym)
- with \<open>coprime b c\<close> have "b dvd a"
- by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
- by (auto intro: dvdI dest: sym simp add: mult.commute)
- with \<open>coprime b c\<close> have "c dvd d"
- by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
- by (auto intro: dvdI dest: sym simp add: mult.commute)
- with \<open>coprime a d\<close> have "d dvd c"
- by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
- from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
- by (rule associatedI)
- moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> 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 \<open>\medskip Addition laws\<close>
-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 \<Longrightarrow> 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 \<Longrightarrow> 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]: -- \<open>FIXME move\<close>
@@ -1104,49 +1651,6 @@
subsection \<open>Coprimality\<close>
-context semiring_gcd
-begin
-
-lemma div_gcd_coprime:
- assumes nz: "a \<noteq> 0 \<or> b \<noteq> 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 \<noteq> 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 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
-proof
- assume ?P then show ?Q by auto
-next
- assume ?Q
- then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> 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 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> 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 \<noteq> 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 \<noteq> 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) \<longleftrightarrow>
- coprime d a \<and> 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) \<longleftrightarrow>
- coprime d a \<and> 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) \<longleftrightarrow> 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 \<noteq> 0"
- shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<noteq> 0"
- shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<Longrightarrow> coprime d (a^n)"
- by (induct n) (simp_all add: coprime_mult)
-
-lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> 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 \<and> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof-
- let ?g = "gcd a b"
- {assume "?g = 0" with dc have ?thesis by auto}
- moreover
- {assume z: "?g \<noteq> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof-
- let ?g = "gcd a b"
- {assume "?g = 0" with dc have ?thesis by auto}
- moreover
- {assume z: "?g \<noteq> 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 \<noteq> 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 \<noteq> 0"
- hence zn: "?g ^ n \<noteq> 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 \<noteq> 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 \<noteq> 0"
- hence zn: "?g ^ n \<noteq> 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 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
- by (auto intro: pow_divides_pow_nat dvd_power_same)
-
-lemma pow_divides_eq_int [simp]:
- "n ~= 0 \<Longrightarrow> (a::int) ^ n dvd b ^ n \<longleftrightarrow> 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 \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
- with \<open>a dvd c\<close> have "a dvd b' * b"
- by (simp add: ac_simps)
- with \<open>coprime a b\<close> have "a dvd b'"
- by (simp add: coprime_dvd_mult_iff)
- then obtain a' where "b' = a * a'" ..
- with \<open>c = b * b'\<close> 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) \<noteq> 0 \<Longrightarrow> 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 "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>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 "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>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 \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
@@ -1505,15 +1687,11 @@
"coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
using gcd_greatest_iff [of x a b] by auto
-lemma coprime_divisors_nat:
- "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<open>Bezout's theorem\<close>
@@ -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: "\<bar>m::int\<bar> * \<bar>n\<bar> = 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 = \<bar>n::int\<bar> \<longleftrightarrow> 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 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
using lcm_eq_1_iff [of m n] by simp
@@ -2069,21 +2239,11 @@
text \<open>Some code equations\<close>
-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 \<open>Fact aliasses\<close>
--- 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 "\<dots> = fib (n + 2) + fib (n + 1)"
by simp
also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
- by (rule gcd_add2_nat)
+ by (rule gcd_add2)
also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd.commute)
also assume "\<dots> = 1"
--- 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 \<Longrightarrow> 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) \<Longrightarrow> 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 \<Longrightarrow> coprime a m =
@@ -568,7 +568,7 @@
[x = y] (mod (\<Prod>i\<in>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 \<Longrightarrow>
@@ -577,7 +577,7 @@
[x = y] (mod (\<Prod>i\<in>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 (\<Prod>j \<in> A - {i}. m j) (m i)"
- by (intro setprod_coprime_nat, auto)
+ by (intro setprod_coprime, auto)
then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
by (elim cong_solve_coprime_nat)
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
@@ -824,7 +824,7 @@
[x = y] (mod (\<Prod>i\<in>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:
--- 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 \<open>Abstract euclidean algorithm\<close>
theory Euclidean_Algorithm
-imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
+imports "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
begin
text \<open>
@@ -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 \<noteq> 0 \<Longrightarrow> 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: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> 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 \<and> d dvd b \<and>
- normalize d = d \<and>
- (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> gcd a b = normalize a"
- by (subst gcd.commute, simp add: gcd_proj2_if_dvd)
-
-lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
-proof
- assume A: "gcd m n = normalize m"
- show "m dvd n"
- proof (cases "m = 0")
- assume [simp]: "m \<noteq> 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 \<longleftrightarrow> 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 \<noteq> 0"
shows "euclidean_size (gcd a b) \<le> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<circ> gcd b = gcd b \<circ> gcd a"
- by (simp add: fun_eq_iff ac_simps)
-next
- fix a show "gcd a \<circ> 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 \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> 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) \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d"
- (is "?lhs \<longleftrightarrow> ?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: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
- by (rule sym, rule gcdI, simp_all)
-
-lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
- by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
-
-lemma div_gcd_coprime:
- assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
- defines [simp]: "d \<equiv> gcd a b"
- defines [simp]: "a' \<equiv> a div d" and [simp]: "b' \<equiv> 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 \<noteq> 0" by simp
- with div_mult_self1_is_id have "d * (l * u) div d = l * u" .
- ultimately have "1 = l * u"
- using \<open>d \<noteq> 0\<close> 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 \<open>l dvd d\<close> 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 \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> 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 \<noteq> 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 \<noteq> 0 \<or> b \<noteq> 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 \<longleftrightarrow> 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 \<noteq> 0"
- shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> 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 \<Longrightarrow> 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 \<and> 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 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> 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 "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof (cases "gcd a b = 0")
- assume "gcd a b = 0"
- hence "a = 0 \<and> b = 0" by simp
- hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
- then show ?thesis by blast
-next
- let ?d = "gcd a b"
- assume "?d \<noteq> 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 \<open>?d \<noteq> 0\<close> 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' \<and> ?d dvd b \<and> 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 \<noteq> 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 \<noteq> 0"
- from n obtain m where m: "n = Suc m" by (cases n, simp_all)
- from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
- from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
- 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 \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> 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]:
- "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
- apply (cases "finite A")
- apply (induct set: finite)
- apply (auto simp add: gcd_mult_cancel)
- done
-
-lemma listprod_coprime:
- "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> 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 \<longleftrightarrow> a = 0 \<or> b = 0"
- by (fact lcm_eq_0_iff)
-
-lemmas lcm_0_iff = lcm_zero
-
-lemma gcd_lcm:
- assumes "lcm a b \<noteq> 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 "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> 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 \<and> b dvd d \<and>
- normalize d = d \<and>
- (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
- by rule (auto intro: lcmI simp: lcm_least lcm_zero)
-
-lemma lcm_coprime:
- "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
- by (subst lcm_gcd) simp
-
-lemma lcm_proj1_if_dvd:
- "b dvd a \<Longrightarrow> lcm a b = normalize a"
- by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
-
-lemma lcm_proj2_if_dvd:
- "a dvd b \<Longrightarrow> 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 \<longleftrightarrow> n dvd m"
-proof
- assume A: "lcm m n = normalize m"
- show "n dvd m"
- proof (cases "m = 0")
- assume [simp]: "m \<noteq> 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 \<longleftrightarrow> m dvd n"
- using lcm_proj1_iff [of n m] by (simp add: ac_simps)
-
lemma euclidean_size_lcm_le1:
assumes "a \<noteq> 0" and "b \<noteq> 0"
shows "euclidean_size a \<le> 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 \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
+ with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff)
then show ?thesis by (subst A, intro size_mult_mono)
qed
@@ -849,7 +379,7 @@
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> 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 \<open>\<not>b dvd a\<close> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> 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 \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
- by (blast intro: Lcm_least dvd_Lcm)
-
-lemma Lcm_Un:
- "Lcm (A \<union> 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}) \<union> {a\<in>A. is_unit a} = A" by blast
- hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
- by (simp add: Lcm_Un [symmetric])
- also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
- finally show ?thesis by simp
-qed
-
-lemma Lcm_0_iff':
- "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
-proof
- assume "Lcm A = 0"
- show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
- proof
- assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)"
- then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
- def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
- def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
- have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> 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 \<noteq> 0" unfolding l_def by simp_all
- hence "normalize l \<noteq> 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 \<open>Lcm A = 0\<close> by contradiction
- qed
-qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
-
-lemma Lcm_no_multiple:
- "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
-proof -
- assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)"
- hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>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 \<open>finite A\<close>])
- (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 \<noteq> {}"
- assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
- shows "Lcm A = normalize (\<Prod>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 (\<Prod>A)" by blast
- also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
- also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
- with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
- by (simp add: lcm_coprime)
- finally show ?case .
-qed simp
-
-lemma Lcm_coprime':
- "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
- \<Longrightarrow> Lcm A = normalize (\<Prod>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 "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> 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 \<in> A \<Longrightarrow> 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 \<open>finite A\<close>])
- (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 = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
-
-lemma pairwise_coprimeI [intro?]:
- "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
- by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprimeD:
- "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
- by (simp add: pairwise_coprime_def)
-
-lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
- by (force simp: pairwise_coprime_def)
-
end
text \<open>
@@ -1084,48 +431,6 @@
lemma bezout: "\<exists>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 "\<dots> = gcd ((n - 1) + 1) (n - 1)" by simp
- also have "\<dots> = 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
--- 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 \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
--- 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 \<open>Relationships Between Gauss Sets\<close>
--- 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: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [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)" "\<forall>k <m. \<not>?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 "\<dots> = (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) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
using c by simp
also have "\<dots> \<longleftrightarrow> [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"
--- 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 \<Longrightarrow> ~ p dvd a \<Longrightarrow> 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 \<Longrightarrow> ~ p dvd a \<Longrightarrow> 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 \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> 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 "\<exists>x y. a * x - b * y = gcd a b \<or> 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:
--- 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) (\<Prod>i \<in> (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