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.7 -by (metis gcd_red_int mod_add_self1 zadd_commute)
     1.8 +by (metis gcd_red_int mod_add_self1 add_commute)
     1.9  
    1.10  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
    1.11 -by (metis gcd_add1_int gcd_commute_int zadd_commute)
    1.12 +by (metis gcd_add1_int gcd_commute_int add_commute)
    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