src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 58953 2e19b392d9e3 parent 58889 5b7a9633cfa8 child 59009 348561aa3869
1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sat Nov 08 16:53:26 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Nov 09 10:03:17 2014 +0100
1.3 @@ -108,7 +108,7 @@
1.5  lemma ring_inv_is_inv1 [simp]:
1.6    "is_unit a \<Longrightarrow> a * ring_inv a = 1"
1.7 -  unfolding is_unit_def ring_inv_def by (simp add: dvd_mult_div_cancel)
1.8 +  unfolding is_unit_def ring_inv_def by simp
1.10  lemma ring_inv_is_inv2 [simp]:
1.11    "is_unit a \<Longrightarrow> ring_inv a * a = 1"
1.12 @@ -1034,19 +1034,19 @@
1.13  proof (cases "a * b = 0")
1.14    let ?nf = normalisation_factor
1.15    assume "a * b \<noteq> 0"
1.16 -  hence "gcd a b \<noteq> 0" by (auto simp add: gcd_zero)
1.17 +  hence "gcd a b \<noteq> 0" by simp
1.18    from lcm_gcd have "lcm a b * gcd a b = gcd a b * (a * b div (?nf (a*b) * gcd a b))"
1.19      by (simp add: mult_ac)
1.20    also from `a * b \<noteq> 0` have "... = a * b div ?nf (a*b)"
1.21 -    by (simp_all add: unit_ring_inv'1 dvd_mult_div_cancel unit_ring_inv)
1.22 +    by (simp_all add: unit_ring_inv'1 unit_ring_inv)
1.23    finally show ?thesis .
1.24 -qed (simp add: lcm_gcd)
1.25 +qed (auto simp add: lcm_gcd)
1.27  lemma lcm_dvd1 [iff]:
1.28    "x dvd lcm x y"
1.29  proof (cases "x*y = 0")
1.30    assume "x * y \<noteq> 0"
1.31 -  hence "gcd x y \<noteq> 0" by (auto simp: gcd_zero)
1.32 +  hence "gcd x y \<noteq> 0" by simp
1.33    let ?c = "ring_inv (normalisation_factor (x*y))"
1.34    from `x * y \<noteq> 0` have [simp]: "is_unit (normalisation_factor (x*y))" by simp
1.35    from lcm_gcd_prod[of x y] have "lcm x y * gcd x y = x * ?c * y"
1.36 @@ -1057,7 +1057,7 @@
1.37    also have "... = x * (?c * y div gcd x y)"
1.38      by (metis div_mult_swap gcd_dvd2 mult_assoc)
1.39    finally show ?thesis by (rule dvdI)
1.40 -qed (simp add: lcm_gcd)
1.41 +qed (auto simp add: lcm_gcd)
1.43  lemma lcm_least:
1.44    "\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
1.45 @@ -1067,17 +1067,17 @@
1.46    hence "is_unit (?nf k)" by simp
1.47    hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
1.48    assume A: "a dvd k" "b dvd k"
1.49 -  hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by (auto simp add: gcd_zero)
1.50 +  hence "gcd a b \<noteq> 0" using `k \<noteq> 0` by auto
1.51    from A obtain r s where ar: "k = a * r" and bs: "k = b * s"
1.52      unfolding dvd_def by blast
1.53 -  with `k \<noteq> 0` have "r * s \<noteq> 0"
1.54 -    by (intro notI) (drule divisors_zero, elim disjE, simp_all)
1.55 +  with `k \<noteq> 0` have "r * s \<noteq> 0"
1.56 +    by auto (drule sym [of 0], simp)
1.57    hence "is_unit (?nf (r * s))" by simp
1.58    let ?c = "?nf k div ?nf (r*s)"
1.59    from `is_unit (?nf k)` and `is_unit (?nf (r * s))` have "is_unit ?c" by (rule unit_div)
1.60    hence "?c \<noteq> 0" using not_is_unit_0 by fast
1.61    from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
1.62 -    by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps mult_assoc)
1.63 +    by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
1.64    also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
1.65      by (subst (3) `k = a * r`, subst (3) `k = b * s`, simp add: algebra_simps)
1.66    also have "... = ?c * r*s * k * gcd a b" using `r * s \<noteq> 0`
1.67 @@ -1138,7 +1138,7 @@
1.68    "normalisation_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
1.69  proof (cases "a = 0 \<or> b = 0")
1.70    case True then show ?thesis
1.71 -    by (simp add: lcm_gcd) (metis div_0 ac_simps mult_zero_left normalisation_factor_0)
1.72 +    by (auto simp add: lcm_gcd)
1.73  next
1.74    case False
1.75    let ?nf = normalisation_factor
1.76 @@ -1146,8 +1146,8 @@
1.77      have "?nf (lcm a b) * ?nf (gcd a b) = ?nf (a*b) div ?nf (a*b)"
1.78      by (metis div_by_0 div_self normalisation_correct normalisation_factor_0 normalisation_factor_mult)
1.79    also have "... = (if a*b = 0 then 0 else 1)"
1.80 -    by (cases "a*b = 0", simp, subst div_self, metis dvd_0_left normalisation_factor_dvd, simp)
1.81 -  finally show ?thesis using False by (simp add: no_zero_divisors)
1.82 +    by simp
1.83 +  finally show ?thesis using False by simp
1.84  qed
1.86  lemma lcm_dvd2 [iff]: "y dvd lcm x y"