summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Fri, 01 Jul 2016 08:35:15 +0200 | |

changeset 63359 | 99b51ba8da1c |

parent 63358 | a500677d4cec |

child 63360 | 65a9eb946ff2 |

More lemmas on Gcd/Lcm

src/HOL/GCD.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Rings.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/GCD.thy Fri Jul 01 08:19:53 2016 +0200 +++ b/src/HOL/GCD.thy Fri Jul 01 08:35:15 2016 +0200 @@ -1188,6 +1188,35 @@ shows "Gcd A = a" using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd) +lemma dvd_GcdD: + assumes "x dvd Gcd A" "y \<in> A" + shows "x dvd y" + using assms Gcd_dvd dvd_trans by blast + +lemma dvd_Gcd_iff: + "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)" + by (blast dest: dvd_GcdD intro: Gcd_greatest) + +lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A" +proof (cases "c = 0") + case [simp]: False + have "Gcd (op * c ` A) div c dvd Gcd A" + by (intro Gcd_greatest, subst div_dvd_iff_mult) + (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c]) + hence "Gcd (op * c ` A) dvd c * Gcd A" + by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac) + also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c" + by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac) + also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A" + by (simp add: dvd_mult_unit_iff) + finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" . + moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)" + by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd) + ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)" + by (rule associatedI) + thus ?thesis by (simp add: normalize_mult) +qed auto + lemma Lcm_eqI: assumes "normalize a = a" assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a" @@ -1195,6 +1224,46 @@ shows "Lcm A = a" using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm) +lemma Lcm_dvdD: + assumes "Lcm A dvd x" "y \<in> A" + shows "y dvd x" + using assms dvd_Lcm dvd_trans by blast + +lemma Lcm_dvd_iff: + "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)" + by (blast dest: Lcm_dvdD intro: Lcm_least) + +lemma Lcm_mult: + assumes "A \<noteq> {}" + shows "Lcm (op * c ` A) = normalize c * Lcm A" +proof (cases "c = 0") + case True + moreover from assms this have "op * c ` A = {0}" by auto + ultimately show ?thesis by auto +next + case [simp]: False + from assms obtain x where x: "x \<in> A" by blast + have "c dvd c * x" by simp + also from x have "c * x dvd Lcm (op * c ` A)" by (intro dvd_Lcm) auto + finally have dvd: "c dvd Lcm (op * c ` A)" . + + have "Lcm A dvd Lcm (op * c ` A) div c" + by (intro Lcm_least dvd_mult_imp_div) + (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c]) + hence "c * Lcm A dvd Lcm (op * c ` A)" + by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd) + also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c" + by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac) + also have "\<dots> dvd Lcm (op * c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (op * c ` A)" + by (simp add: mult_unit_dvd_iff) + finally have "normalize c * Lcm A dvd Lcm (op * c ` A)" . + moreover have "Lcm (op * c ` A) dvd normalize c * Lcm A" + by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm) + ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))" + by (rule associatedI) + thus ?thesis by (simp add: normalize_mult) +qed + lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"

--- a/src/HOL/Rings.thy Fri Jul 01 08:19:53 2016 +0200 +++ b/src/HOL/Rings.thy Fri Jul 01 08:35:15 2016 +0200 @@ -757,6 +757,17 @@ finally show ?thesis . qed +lemma dvd_mult_imp_div: + assumes "a * c dvd b" + shows "a dvd b div c" +proof (cases "c = 0") + case True then show ?thesis by simp +next + case False + from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" .. + with False show ?thesis by (simp add: mult.commute [of a] mult.assoc) +qed + text \<open>Units: invertible elements in a ring\<close>