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