src/HOL/Number_Theory/Gauss.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 58288 87b59745dd6d
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -260,11 +260,11 @@
     1.4    fix y::int and z::int
     1.5    assume "p - (y*a) mod p = (z*a) mod p"
     1.6    then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
     1.7 -    by (metis add_commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
     1.8 +    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
     1.9    moreover have "[y * a = (y*a) mod p] (mod p)"
    1.10      by (metis cong_int_def mod_mod_trivial)
    1.11    ultimately have "[a * (y + z) = 0] (mod p)"
    1.12 -    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult_commute ring_class.ring_distribs(1))
    1.13 +    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
    1.14    with p_prime a_nonzero p_a_relprime
    1.15    have a: "[y + z = 0] (mod p)"
    1.16      by (metis cong_prime_prod_zero_int)
    1.17 @@ -319,19 +319,19 @@
    1.18  subsection {* Gauss' Lemma *}
    1.19  
    1.20  lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
    1.21 -by (metis (no_types) minus_minus mult_commute mult_left_commute power_minus power_one)
    1.22 +by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
    1.23  
    1.24  theorem pre_gauss_lemma:
    1.25    "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
    1.26  proof -
    1.27    have "[setprod id A = setprod id F * setprod id D](mod p)"
    1.28 -    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong)
    1.29 +    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong)
    1.30    then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
    1.31      apply (rule cong_trans_int)
    1.32      apply (metis cong_scalar_int prod_F_zcong)
    1.33      done
    1.34    then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
    1.35 -    by (metis C_prod_eq_D_times_E mult_commute mult_left_commute)
    1.36 +    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
    1.37    then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
    1.38      by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
    1.39    then have "[setprod id A = ((-1)^(card E) *
    1.40 @@ -349,7 +349,7 @@
    1.41    then have "[setprod id A = ((-1)^(card E) * a^(card A) *
    1.42        setprod id A)](mod p)"
    1.43      apply (rule cong_trans_int)
    1.44 -    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult_assoc)
    1.45 +    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
    1.46      done
    1.47    then have a: "[setprod id A * (-1)^(card E) =
    1.48        ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
    1.49 @@ -357,7 +357,7 @@
    1.50    then have "[setprod id A * (-1)^(card E) = setprod id A *
    1.51        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
    1.52      apply (rule cong_trans_int)
    1.53 -    apply (simp add: a mult_commute mult_left_commute)
    1.54 +    apply (simp add: a mult.commute mult.left_commute)
    1.55      done
    1.56    then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
    1.57      apply (rule cong_trans_int)