src/HOL/GCD.thy
 changeset 44821 a92f65e174cf parent 44766 d4d33a4d7548 child 44845 5e51075cbd97
```     1.1 --- a/src/HOL/GCD.thy	Wed Sep 07 14:58:40 2011 +0200
1.2 +++ b/src/HOL/GCD.thy	Wed Sep 07 09:02:58 2011 -0700
1.3 @@ -485,16 +485,16 @@
1.4  done
1.5
1.6  lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
1.9
1.10  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
1.13
1.14  lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
1.15  by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
1.16
1.17  lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
1.18 -by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
1.19 +by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)
1.20
1.21
1.22  (* to do: differences, and all variations of addition rules
1.23 @@ -1030,8 +1030,7 @@
1.24        apply (subst mod_div_equality [of m n, symmetric])
1.25        (* applying simp here undoes the last substitution!
1.26           what is procedure cancel_div_mod? *)
1.27 -      apply (simp only: field_simps zadd_int [symmetric]
1.28 -        zmult_int [symmetric])
1.29 +      apply (simp only: field_simps of_nat_add of_nat_mult)
1.30        done
1.31  qed
1.32
1.33 @@ -1237,7 +1236,7 @@
1.34
1.35  lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1.36    by (simp add: lcm_int_def lcm_nat_def zdiv_int
1.37 -    zmult_int [symmetric] gcd_int_def)
1.38 +    of_nat_mult gcd_int_def)
1.39
1.40  lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
1.41    unfolding lcm_nat_def
```