src/HOL/GCD.thy
changeset 57512 cc97b347b301
parent 56218 1c3f1f2431f9
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/GCD.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4    apply (rule_tac n = k in coprime_dvd_mult_nat)
     1.5    apply (simp add: gcd_assoc_nat)
     1.6    apply (simp add: gcd_commute_nat)
     1.7 -  apply (simp_all add: mult_commute)
     1.8 +  apply (simp_all add: mult.commute)
     1.9  done
    1.10  
    1.11  lemma gcd_mult_cancel_int:
    1.12 @@ -432,9 +432,9 @@
    1.13    with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
    1.14    from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
    1.15    with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
    1.16 -  from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute)
    1.17 +  from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
    1.18    with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
    1.19 -  from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute)
    1.20 +  from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
    1.21    with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
    1.22    from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
    1.23    moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
    1.24 @@ -456,7 +456,7 @@
    1.25  
    1.26  lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
    1.27    apply (subst (1 2) gcd_commute_nat)
    1.28 -  apply (subst add_commute)
    1.29 +  apply (subst add.commute)
    1.30    apply simp
    1.31  done
    1.32  
    1.33 @@ -496,16 +496,16 @@
    1.34  done
    1.35  
    1.36  lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
    1.37 -by (metis gcd_red_int mod_add_self1 add_commute)
    1.38 +by (metis gcd_red_int mod_add_self1 add.commute)
    1.39  
    1.40  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
    1.41 -by (metis gcd_add1_int gcd_commute_int add_commute)
    1.42 +by (metis gcd_add1_int gcd_commute_int add.commute)
    1.43  
    1.44  lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
    1.45  by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
    1.46  
    1.47  lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
    1.48 -by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)
    1.49 +by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute)
    1.50  
    1.51  
    1.52  (* to do: differences, and all variations of addition rules
    1.53 @@ -778,7 +778,7 @@
    1.54      by (auto simp:div_gcd_coprime_nat)
    1.55    hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
    1.56        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
    1.57 -    apply (subst (1 2) mult_commute)
    1.58 +    apply (subst (1 2) mult.commute)
    1.59      apply (subst gcd_mult_distrib_nat [symmetric])
    1.60      apply simp
    1.61      done
    1.62 @@ -820,10 +820,10 @@
    1.63      from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
    1.64      with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
    1.65      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
    1.66 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
    1.67 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
    1.68      with z have th_1: "a' dvd b' * c" by auto
    1.69      from coprime_dvd_mult_nat[OF ab'(3)] th_1
    1.70 -    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
    1.71 +    have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
    1.72      from ab' have "a = ?g*a'" by algebra
    1.73      with thb thc have ?thesis by blast }
    1.74    ultimately show ?thesis by blast
    1.75 @@ -844,10 +844,10 @@
    1.76      with dc have th0: "a' dvd b*c"
    1.77        using dvd_trans[of a' a "b*c"] by simp
    1.78      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
    1.79 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
    1.80 +    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
    1.81      with z have th_1: "a' dvd b' * c" by auto
    1.82      from coprime_dvd_mult_int[OF ab'(3)] th_1
    1.83 -    have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
    1.84 +    have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
    1.85      from ab' have "a = ?g*a'" by algebra
    1.86      with thb thc have ?thesis by blast }
    1.87    ultimately show ?thesis by blast
    1.88 @@ -869,13 +869,13 @@
    1.89      from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
    1.90        by (simp add: ab'(1,2)[symmetric])
    1.91      hence "?g^n*a'^n dvd ?g^n *b'^n"
    1.92 -      by (simp only: power_mult_distrib mult_commute)
    1.93 +      by (simp only: power_mult_distrib mult.commute)
    1.94      with zn z n have th0:"a'^n dvd b'^n" by auto
    1.95      have "a' dvd a'^n" by (simp add: m)
    1.96      with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
    1.97 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
    1.98 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
    1.99      from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   1.100 -    have "a' dvd b'" by (subst (asm) mult_commute, blast)
   1.101 +    have "a' dvd b'" by (subst (asm) mult.commute, blast)
   1.102      hence "a'*?g dvd b'*?g" by simp
   1.103      with ab'(1,2)  have ?thesis by simp }
   1.104    ultimately show ?thesis by blast
   1.105 @@ -897,14 +897,14 @@
   1.106      from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
   1.107        by (simp add: ab'(1,2)[symmetric])
   1.108      hence "?g^n*a'^n dvd ?g^n *b'^n"
   1.109 -      by (simp only: power_mult_distrib mult_commute)
   1.110 +      by (simp only: power_mult_distrib mult.commute)
   1.111      with zn z n have th0:"a'^n dvd b'^n" by auto
   1.112      have "a' dvd a'^n" by (simp add: m)
   1.113      with th0 have "a' dvd b'^n"
   1.114        using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.115 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
   1.116 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   1.117      from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   1.118 -    have "a' dvd b'" by (subst (asm) mult_commute, blast)
   1.119 +    have "a' dvd b'" by (subst (asm) mult.commute, blast)
   1.120      hence "a'*?g dvd b'*?g" by simp
   1.121      with ab'(1,2)  have ?thesis by simp }
   1.122    ultimately show ?thesis by blast
   1.123 @@ -922,7 +922,7 @@
   1.124  proof-
   1.125    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.126      unfolding dvd_def by blast
   1.127 -  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   1.128 +  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.129    hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   1.130    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.131    from n' k show ?thesis unfolding dvd_def by auto
   1.132 @@ -934,7 +934,7 @@
   1.133  proof-
   1.134    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.135      unfolding dvd_def by blast
   1.136 -  from mr n' have "m dvd n'*n" by (simp add: mult_commute)
   1.137 +  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.138    hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   1.139    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.140    from n' k show ?thesis unfolding dvd_def by auto
   1.141 @@ -1218,14 +1218,14 @@
   1.142            from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
   1.143              by simp
   1.144            hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
   1.145 -            by (simp only: mult_assoc distrib_left)
   1.146 +            by (simp only: mult.assoc distrib_left)
   1.147            hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
   1.148              by algebra
   1.149            hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
   1.150            hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
   1.151              by (simp only: diff_add_assoc[OF dble, of d, symmetric])
   1.152            hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
   1.153 -            by (simp only: diff_mult_distrib2 add_commute mult_ac)
   1.154 +            by (simp only: diff_mult_distrib2 add.commute mult_ac)
   1.155            hence ?thesis using H(1,2)
   1.156              apply -
   1.157              apply (rule exI[where x=d], simp)
   1.158 @@ -1674,7 +1674,7 @@
   1.159  apply(auto simp add:inj_on_def)
   1.160  apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
   1.161  apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
   1.162 -             dvd.neq_le_trans dvd_triv_right mult_commute)
   1.163 +             dvd.neq_le_trans dvd_triv_right mult.commute)
   1.164  done
   1.165  
   1.166  text{* Nitpick: *}