More lemmas on Gcd/Lcm
authorManuel Eberl <eberlm@in.tum.de>
Fri Jul 01 08:35:15 2016 +0200 (2016-07-01)
changeset 6335999b51ba8da1c
parent 63358 a500677d4cec
child 63360 65a9eb946ff2
More lemmas on Gcd/Lcm
src/HOL/GCD.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/GCD.thy	Fri Jul 01 08:19:53 2016 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Jul 01 08:35:15 2016 +0200
     1.3 @@ -1188,6 +1188,35 @@
     1.4    shows "Gcd A = a"
     1.5    using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
     1.6  
     1.7 +lemma dvd_GcdD:
     1.8 +  assumes "x dvd Gcd A" "y \<in> A"
     1.9 +  shows   "x dvd y"
    1.10 +  using assms Gcd_dvd dvd_trans by blast
    1.11 +
    1.12 +lemma dvd_Gcd_iff:
    1.13 +  "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
    1.14 +  by (blast dest: dvd_GcdD intro: Gcd_greatest)
    1.15 +
    1.16 +lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A"
    1.17 +proof (cases "c = 0")
    1.18 +  case [simp]: False
    1.19 +  have "Gcd (op * c ` A) div c dvd Gcd A"
    1.20 +    by (intro Gcd_greatest, subst div_dvd_iff_mult)
    1.21 +       (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
    1.22 +  hence "Gcd (op * c ` A) dvd c * Gcd A"
    1.23 +    by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
    1.24 +  also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
    1.25 +    by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
    1.26 +  also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A"
    1.27 +    by (simp add: dvd_mult_unit_iff)
    1.28 +  finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" .
    1.29 +  moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)"
    1.30 +    by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
    1.31 +  ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)"
    1.32 +    by (rule associatedI)
    1.33 +  thus ?thesis by (simp add: normalize_mult)
    1.34 +qed auto
    1.35 +
    1.36  lemma Lcm_eqI:
    1.37    assumes "normalize a = a"
    1.38    assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
    1.39 @@ -1195,6 +1224,46 @@
    1.40    shows "Lcm A = a"
    1.41    using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
    1.42  
    1.43 +lemma Lcm_dvdD:
    1.44 +  assumes "Lcm A dvd x" "y \<in> A"
    1.45 +  shows   "y dvd x"
    1.46 +  using assms dvd_Lcm dvd_trans by blast
    1.47 +
    1.48 +lemma Lcm_dvd_iff:
    1.49 +  "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
    1.50 +  by (blast dest: Lcm_dvdD intro: Lcm_least)
    1.51 +
    1.52 +lemma Lcm_mult: 
    1.53 +  assumes "A \<noteq> {}"
    1.54 +  shows   "Lcm (op * c ` A) = normalize c * Lcm A"
    1.55 +proof (cases "c = 0")
    1.56 +  case True
    1.57 +  moreover from assms this have "op * c ` A = {0}" by auto
    1.58 +  ultimately show ?thesis by auto
    1.59 +next
    1.60 +  case [simp]: False
    1.61 +  from assms obtain x where x: "x \<in> A" by blast
    1.62 +  have "c dvd c * x" by simp
    1.63 +  also from x have "c * x dvd Lcm (op * c ` A)" by (intro dvd_Lcm) auto
    1.64 +  finally have dvd: "c dvd Lcm (op * c ` A)" .
    1.65 +
    1.66 +  have "Lcm A dvd Lcm (op * c ` A) div c"
    1.67 +    by (intro Lcm_least dvd_mult_imp_div)
    1.68 +       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
    1.69 +  hence "c * Lcm A dvd Lcm (op * c ` A)"
    1.70 +    by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
    1.71 +  also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
    1.72 +    by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
    1.73 +  also have "\<dots> dvd Lcm (op * c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (op * c ` A)"
    1.74 +    by (simp add: mult_unit_dvd_iff)
    1.75 +  finally have "normalize c * Lcm A dvd Lcm (op * c ` A)" .
    1.76 +  moreover have "Lcm (op * c ` A) dvd normalize c * Lcm A"
    1.77 +    by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
    1.78 +  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))"
    1.79 +    by (rule associatedI)
    1.80 +  thus ?thesis by (simp add: normalize_mult)
    1.81 +qed
    1.82 +
    1.83  
    1.84  lemma Lcm_no_units:
    1.85    "Lcm A = Lcm (A - {a. is_unit a})"
     2.1 --- a/src/HOL/Rings.thy	Fri Jul 01 08:19:53 2016 +0200
     2.2 +++ b/src/HOL/Rings.thy	Fri Jul 01 08:35:15 2016 +0200
     2.3 @@ -757,6 +757,17 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 +lemma dvd_mult_imp_div:
     2.8 +  assumes "a * c dvd b"
     2.9 +  shows "a dvd b div c"
    2.10 +proof (cases "c = 0")
    2.11 +  case True then show ?thesis by simp
    2.12 +next
    2.13 +  case False
    2.14 +  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
    2.15 +  with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
    2.16 +qed
    2.17 +
    2.18  
    2.19  text \<open>Units: invertible elements in a ring\<close>
    2.20