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.4  
     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.9  
    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.26  
    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.42  
    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.85  
    1.86  lemma lcm_dvd2 [iff]: "y dvd lcm x y"