src/HOL/GCD.thy
 changeset 63359 99b51ba8da1c parent 63145 703edebd1d92 child 63489 cd540c8031a4
```     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})"
```