src/HOL/NumberTheory/Gauss.thy

 
 lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
 
 lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
-  using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
+by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
 
 
 subsection {* Relationships Between Gauss Sets *}
 
 lemma B_card_eq_A: "card B = card A"

     apply (frule_tac f = "op - p" in setprod_reindex_id, auto)
     done
   then have one:
     "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
     apply simp
-    apply (insert p_g_0 finite_E)
-    by (auto simp add: StandardRes_prod)
+    apply (insert p_g_0 finite_E StandardRes_prod)
+    by (auto)
   moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
     apply clarify
     apply (insert zcong_id [of p])
     apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
     done

     apply (rule_tac b = "p - x" in zcong_trans, auto)
     done
   ultimately have c:
     "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
     apply simp
-    apply (insert finite_E p_g_0)
-    apply (rule setprod_same_function_zcong
-      [of E "StandardRes p o (op - p)" uminus p], auto)
-    done
+    using finite_E p_g_0
+      setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+    by auto
   then have two: "[setprod id F = setprod (uminus) E](mod p)"
     apply (insert one c)
     apply (rule zcong_trans [of "setprod id F"
                                "setprod (StandardRes p o op - p) E" p
                                "setprod uminus E"], auto)

 
 theorem pre_gauss_lemma:
   "[a ^ nat((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 zmult_commute)
+    by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
   then have "[setprod id A = ((-1)^(card E) * setprod id E) *
       setprod id D] (mod p)"
     apply (rule zcong_trans)
-    apply (auto simp add: prod_F_zcong zcong_scalar)
+    apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod_cong)
     done
   then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
     apply (rule zcong_trans)
     apply (insert C_prod_eq_D_times_E, erule subst)
     apply (subst zmult_assoc, auto)
     done
   then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
     apply (rule zcong_trans)
-    apply (simp add: C_B_zcong_prod zcong_scalar2)
+    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod_cong)
     done
   then have "[setprod id A = ((-1)^(card E) *
     (setprod id ((%x. x * a) ` A)))] (mod p)"
     by (simp add: B_def)
   then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
     (mod p)"
-    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
+    by (simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric] cong del:setprod_cong)
   moreover have "setprod (%x. x * a) A =
     setprod (%x. a) A * setprod id A"
     using finite_A by (induct set: finite) auto
   ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
     setprod id A))] (mod p)"

     apply (simp add: a mult_commute mult_left_commute)
     done
   then have "[setprod id A * (-1)^(card E) = setprod id A *
       a^(card A)](mod p)"
     apply (rule zcong_trans)
-    apply (simp add: aux)
+    apply (simp add: aux cong del:setprod_cong)
     done
   with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
       p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
     by (simp add: order_less_imp_le)
   from this show ?thesis