1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -239,12 +239,13 @@
     1.4    by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
     1.5  
     1.6  lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
     1.7 -  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute)
     1.8 +  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
     1.9  
    1.10  lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
    1.11    apply (auto simp add: C_def)
    1.12    apply (insert finite_B SR_B_inj)
    1.13 -  apply (frule_tac f = "\<lambda>x. x mod int p" in setprod_reindex_id [symmetric], auto)
    1.14 +  apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
    1.15 +  apply auto
    1.16    apply (rule cong_setprod_int)
    1.17    apply (auto simp add: cong_int_def)
    1.18    done
    1.19 @@ -291,14 +292,14 @@
    1.20    by (auto simp add: card_seteq)
    1.21  
    1.22  lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
    1.23 -  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint)
    1.24 +  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
    1.25  
    1.26  lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
    1.27  proof -
    1.28    have FE: "setprod id F = setprod (op - p) E"
    1.29      apply (auto simp add: F_def)
    1.30      apply (insert finite_E inj_on_pminusx_E)
    1.31 -    apply (frule setprod_reindex_id, auto)
    1.32 +    apply (drule setprod.reindex, auto)
    1.33      done
    1.34    then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
    1.35      by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
    1.36 @@ -324,7 +325,7 @@
    1.37    "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
    1.38  proof -
    1.39    have "[setprod id A = setprod id F * setprod id D](mod p)"
    1.40 -    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
    1.41 +    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong)
    1.42    then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
    1.43      apply (rule cong_trans_int)
    1.44      apply (metis cong_scalar_int prod_F_zcong)
    1.45 @@ -338,7 +339,7 @@
    1.46      by (simp add: B_def)
    1.47    then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
    1.48      (mod p)"
    1.49 -    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
    1.50 +    by (simp add: inj_on_xa_A setprod.reindex)
    1.51    moreover have "setprod (\<lambda>x. x * a) A =
    1.52      setprod (\<lambda>x. a) A * setprod id A"
    1.53      using finite_A by (induct set: finite) auto
    1.54 @@ -360,7 +361,7 @@
    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)
    1.58 -    apply (simp add: aux cong del:setprod_cong)
    1.59 +    apply (simp add: aux cong del:setprod.cong)
    1.60      done
    1.61    with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
    1.62      by (metis cong_mult_lcancel_int)