src/HOL/Old_Number_Theory/Legacy_GCD.thy
changeset 58834 773b378d9313
parent 58623 2db1df2c8467
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -207,7 +207,8 @@
     1.4    from dvdg dvdg' obtain ka kb ka' kb' where
     1.5        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     1.6      unfolding dvd_def by blast
     1.7 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
     1.8 +  from this(3-4) [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
     1.9 +    by (simp_all only: ac_simps mult.left_commute [of _ "gcd a b"])
    1.10    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.11      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    1.12        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    1.13 @@ -351,7 +352,7 @@
    1.14            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" 
    1.15              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
    1.16            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
    1.17 -            by (simp only: diff_mult_distrib2 add.commute ac_simps)
    1.18 +            by (simp only: diff_mult_distrib2 ac_simps)
    1.19            hence ?thesis using H(1,2)
    1.20              apply -
    1.21              apply (rule exI[where x=d], simp)
    1.22 @@ -641,7 +642,8 @@
    1.23    from dvdg dvdg' obtain ka kb ka' kb' where
    1.24     kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
    1.25      unfolding dvd_def by blast
    1.26 -  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
    1.27 +  from this(3-4) [symmetric] have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'"
    1.28 +    by (simp_all only: ac_simps mult.left_commute [of _ "zgcd a b"])
    1.29    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.30      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    1.31        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)