src/HOL/Number_Theory/Gauss.thy
changeset 57418 6ab1c7cb0b8d
parent 56544 b60d5d119489
child 57512 cc97b347b301
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Jun 27 22:08:55 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sat Jun 28 09:16:42 2014 +0200
@@ -239,12 +239,13 @@
   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
 
 lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
-  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod_Un_disjoint sup_commute)
+  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
 
 lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   apply (auto simp add: C_def)
   apply (insert finite_B SR_B_inj)
-  apply (frule_tac f = "\<lambda>x. x mod int p" in setprod_reindex_id [symmetric], auto)
+  apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
+  apply auto
   apply (rule cong_setprod_int)
   apply (auto simp add: cong_int_def)
   done
@@ -291,14 +292,14 @@
   by (auto simp add: card_seteq)
 
 lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
-  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod_Un_disjoint)
+  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
 
 lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
 proof -
   have FE: "setprod id F = setprod (op - p) E"
     apply (auto simp add: F_def)
     apply (insert finite_E inj_on_pminusx_E)
-    apply (frule setprod_reindex_id, auto)
+    apply (drule setprod.reindex, auto)
     done
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
@@ -324,7 +325,7 @@
   "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
   have "[setprod id A = setprod id F * setprod id D](mod p)"
-    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
+    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod.cong)
   then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
     apply (rule cong_trans_int)
     apply (metis cong_scalar_int prod_F_zcong)
@@ -338,7 +339,7 @@
     by (simp add: B_def)
   then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
     (mod p)"
-    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
+    by (simp add: inj_on_xa_A setprod.reindex)
   moreover have "setprod (\<lambda>x. x * a) A =
     setprod (\<lambda>x. a) A * setprod id A"
     using finite_A by (induct set: finite) auto
@@ -360,7 +361,7 @@
     done
   then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
     apply (rule cong_trans_int)
-    apply (simp add: aux cong del:setprod_cong)
+    apply (simp add: aux cong del:setprod.cong)
     done
   with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
     by (metis cong_mult_lcancel_int)