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)
```