src/HOL/NumberTheory/Gauss.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 16663 13e9c402308b
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
     2     ID:         $Id$
     3     Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
     4 *)
     5 
     6 header {* Gauss' Lemma *}
     7 
     8 theory Gauss imports Euler begin;
     9 
    10 locale GAUSS =
    11   fixes p :: "int"
    12   fixes a :: "int"
    13   fixes A :: "int set"
    14   fixes B :: "int set"
    15   fixes C :: "int set"
    16   fixes D :: "int set"
    17   fixes E :: "int set"
    18   fixes F :: "int set"
    19 
    20   assumes p_prime: "p \<in> zprime"
    21   assumes p_g_2: "2 < p"
    22   assumes p_a_relprime: "~[a = 0](mod p)"
    23   assumes a_nonzero:    "0 < a"
    24 
    25   defines A_def: "A == {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    26   defines B_def: "B == (%x. x * a) ` A"
    27   defines C_def: "C == (StandardRes p) ` B"
    28   defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
    29   defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
    30   defines F_def: "F == (%x. (p - x)) ` E";
    31 
    32 subsection {* Basic properties of p *}
    33 
    34 lemma (in GAUSS) p_odd: "p \<in> zOdd";
    35   by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    36 
    37 lemma (in GAUSS) p_g_0: "0 < p";
    38   by (insert p_g_2, auto)
    39 
    40 lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2";
    41   by (insert p_g_2, auto simp add: pos_imp_zdiv_nonneg_iff)
    42 
    43 lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p";
    44   proof -;
    45     have "p - 1 = (p - 1) div 1" by auto
    46     then have "(p - 1) div 2 \<le> p - 1"
    47       apply (rule ssubst) back;
    48       apply (rule zdiv_mono2)
    49       by (auto simp add: p_g_0)
    50     then have "(p - 1) div 2 \<le> p - 1";
    51       by auto
    52     then show ?thesis by simp
    53 qed;
    54 
    55 lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1";
    56   apply (insert zdiv_zmult_self2 [of 2 "p - 1"])
    57 by auto
    58 
    59 lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)";
    60   apply (frule odd_minus_one_even)
    61   apply (simp add: zEven_def)
    62   apply (subgoal_tac "2 \<noteq> 0")
    63   apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)  
    64 by (auto simp add: even_div_2_prop2)
    65 
    66 lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1";
    67   apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    68 by (frule zodd_imp_zdiv_eq, auto)
    69 
    70 subsection {* Basic Properties of the Gauss Sets *}
    71 
    72 lemma (in GAUSS) finite_A: "finite (A)";
    73   apply (auto simp add: A_def) 
    74 thm bdd_int_set_l_finite;
    75   apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}"); 
    76 by (auto simp add: bdd_int_set_l_finite finite_subset)
    77 
    78 lemma (in GAUSS) finite_B: "finite (B)";
    79   by (auto simp add: B_def finite_A finite_imageI)
    80 
    81 lemma (in GAUSS) finite_C: "finite (C)";
    82   by (auto simp add: C_def finite_B finite_imageI)
    83 
    84 lemma (in GAUSS) finite_D: "finite (D)";
    85   by (auto simp add: D_def finite_Int finite_C)
    86 
    87 lemma (in GAUSS) finite_E: "finite (E)";
    88   by (auto simp add: E_def finite_Int finite_C)
    89 
    90 lemma (in GAUSS) finite_F: "finite (F)";
    91   by (auto simp add: F_def finite_E finite_imageI)
    92 
    93 lemma (in GAUSS) C_eq: "C = D \<union> E";
    94   by (auto simp add: C_def D_def E_def)
    95 
    96 lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)";
    97   apply (auto simp add: A_def) 
    98   apply (insert int_nat)
    99   apply (erule subst)
   100   by (auto simp add: card_bdd_int_set_l_le)
   101 
   102 lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A";
   103   apply (insert a_nonzero)
   104 by (simp add: A_def inj_on_def)
   105 
   106 lemma (in GAUSS) A_res: "ResSet p A";
   107   apply (auto simp add: A_def ResSet_def) 
   108   apply (rule_tac m = p in zcong_less_eq) 
   109   apply (insert p_g_2, auto) 
   110   apply (subgoal_tac [1-2] "(p - 1) div 2 < p");
   111 by (auto, auto simp add: p_minus_one_l)
   112 
   113 lemma (in GAUSS) B_res: "ResSet p B";
   114   apply (insert p_g_2 p_a_relprime p_minus_one_l)
   115   apply (auto simp add: B_def) 
   116   apply (rule ResSet_image)
   117   apply (auto simp add: A_res) 
   118   apply (auto simp add: A_def)
   119   proof -;
   120     fix x fix y
   121     assume a: "[x * a = y * a] (mod p)"
   122     assume b: "0 < x"
   123     assume c: "x \<le> (p - 1) div 2"
   124     assume d: "0 < y"
   125     assume e: "y \<le> (p - 1) div 2"
   126     from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   127         have "[x = y](mod p)";
   128       by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   129     with zcong_less_eq [of x y p] p_minus_one_l 
   130          order_le_less_trans [of x "(p - 1) div 2" p]
   131          order_le_less_trans [of y "(p - 1) div 2" p] show "x = y";
   132       by (simp add: prems p_minus_one_l p_g_0)
   133 qed;
   134 
   135 lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B";
   136   apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
   137   proof -;
   138     fix x fix y
   139     assume a: "x * a mod p = y * a mod p"
   140     assume b: "0 < x"
   141     assume c: "x \<le> (p - 1) div 2"
   142     assume d: "0 < y"
   143     assume e: "y \<le> (p - 1) div 2"
   144     assume f: "x \<noteq> y"
   145     from a have "[x * a = y * a](mod p)";
   146       by (simp add: zcong_zmod_eq p_g_0)
   147     with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 
   148         have "[x = y](mod p)";
   149       by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 
   150     with zcong_less_eq [of x y p] p_minus_one_l 
   151          order_le_less_trans [of x "(p - 1) div 2" p]
   152          order_le_less_trans [of y "(p - 1) div 2" p] have "x = y";
   153       by (simp add: prems p_minus_one_l p_g_0)
   154     then have False;
   155       by (simp add: f)
   156     then show "a = 0";
   157       by simp
   158 qed;
   159 
   160 lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E";
   161   apply (auto simp add: E_def C_def B_def A_def)
   162   apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI);
   163 by auto
   164 
   165 lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)";
   166   apply (auto simp add: A_def)
   167   apply (frule_tac m = p in zcong_not_zero)
   168   apply (insert p_minus_one_l)
   169 by auto
   170 
   171 lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x";
   172   by (auto simp add: A_def)
   173 
   174 lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)";
   175   apply (auto simp add: B_def)
   176   apply (frule A_ncong_p) 
   177   apply (insert p_a_relprime p_prime a_nonzero)
   178   apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
   179 by (auto simp add: A_greater_zero)
   180 
   181 lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
   182   apply (insert a_nonzero)
   183 by (auto simp add: B_def mult_pos A_greater_zero)
   184 
   185 lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
   186   apply (auto simp add: C_def)
   187   apply (frule B_ncong_p)
   188   apply (subgoal_tac "[x = StandardRes p x](mod p)");
   189   defer; apply (simp add: StandardRes_prop1)
   190   apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
   191 by auto
   192 
   193 lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y";
   194   apply (auto simp add: C_def)
   195   proof -;
   196     fix x;
   197     assume a: "x \<in> B";
   198     from p_g_0 have "0 \<le> StandardRes p x";
   199       by (simp add: StandardRes_lbound)
   200     moreover have "~[x = 0] (mod p)";
   201       by (simp add: a B_ncong_p)
   202     then have "StandardRes p x \<noteq> 0";
   203       by (simp add: StandardRes_prop3)
   204     ultimately show "0 < StandardRes p x";
   205       by (simp add: order_le_less)
   206 qed;
   207 
   208 lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)";
   209   by (auto simp add: D_def C_ncong_p)
   210 
   211 lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)";
   212   by (auto simp add: E_def C_ncong_p)
   213 
   214 lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)";
   215   apply (auto simp add: F_def) 
   216   proof -;
   217     fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   218     from E_ncong_p have "~[x = 0] (mod p)";
   219       by (simp add: a)
   220     moreover from a have "0 < x";
   221       by (simp add: a E_def C_greater_zero)
   222     moreover from a have "x < p";
   223       by (auto simp add: E_def C_def p_g_0 StandardRes_ubound)
   224     ultimately have "~[p - x = 0] (mod p)";
   225       by (simp add: zcong_not_zero)
   226     from this show False by (simp add: b)
   227 qed;
   228 
   229 lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   230   apply (auto simp add: F_def E_def) 
   231   apply (insert p_g_0)
   232   apply (frule_tac x = xa in StandardRes_ubound)
   233   apply (frule_tac x = x in StandardRes_ubound)
   234   apply (subgoal_tac "xa = StandardRes p xa")
   235   apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1)
   236   proof -;
   237     from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have 
   238         "2 * (p - 1) div 2 = 2 * ((p - 1) div 2)";
   239       by simp
   240     with p_eq2 show " !!x. [| (p - 1) div 2 < StandardRes p x; x \<in> B |]
   241          ==> p - StandardRes p x \<le> (p - 1) div 2";
   242       by simp
   243 qed;
   244 
   245 lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}";
   246   by (auto simp add: D_def C_greater_zero)
   247 
   248 lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}";
   249   by (auto simp add: F_def E_def D_def C_def B_def A_def)
   250 
   251 lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}";
   252   by (auto simp add: D_def C_def B_def A_def)
   253 
   254 lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2";
   255   by (auto simp add: D_eq)
   256 
   257 lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2";
   258   apply (auto simp add: F_eq A_def)
   259   proof -;
   260     fix y;
   261     assume "(p - 1) div 2 < StandardRes p (y * a)";
   262     then have "p - StandardRes p (y * a) < p - ((p - 1) div 2)";
   263       by arith
   264     also from p_eq2 have "... = 2 * ((p - 1) div 2) + 1 - ((p - 1) div 2)"; 
   265       by (rule subst, auto)
   266     also; have "2 * ((p - 1) div 2) + 1 - (p - 1) div 2 = (p - 1) div 2 + 1";
   267       by arith
   268     finally show "p - StandardRes p (y * a) \<le> (p - 1) div 2";
   269       by (insert zless_add1_eq [of "p - StandardRes p (y * a)" 
   270           "(p - 1) div 2"],auto);
   271 qed;
   272 
   273 lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x,p) = 1";
   274   apply (insert p_prime p_minus_one_l)
   275 by (auto simp add: A_def zless_zprime_imp_zrelprime)
   276 
   277 lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1";
   278   by (insert all_A_relprime finite_A, simp add: all_relprime_prod_relprime)
   279 
   280 subsection {* Relationships Between Gauss Sets *}
   281 
   282 lemma (in GAUSS) B_card_eq_A: "card B = card A";
   283   apply (insert finite_A)
   284 by (simp add: finite_A B_def inj_on_xa_A card_image)
   285 
   286 lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)";
   287   by (auto simp add: B_card_eq_A A_card_eq)
   288 
   289 lemma (in GAUSS) F_card_eq_E: "card F = card E";
   290   apply (insert finite_E)
   291 by (simp add: F_def inj_on_pminusx_E card_image)
   292 
   293 lemma (in GAUSS) C_card_eq_B: "card C = card B";
   294   apply (insert finite_B)
   295   apply (subgoal_tac "inj_on (StandardRes p) B");
   296   apply (simp add: B_def C_def card_image)
   297   apply (rule StandardRes_inj_on_ResSet)
   298 by (simp add: B_res)
   299 
   300 lemma (in GAUSS) D_E_disj: "D \<inter> E = {}";
   301   by (auto simp add: D_def E_def)
   302 
   303 lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E";
   304   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   305 
   306 lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C";
   307   apply (insert D_E_disj finite_D finite_E C_eq)
   308   apply (frule setprod_Un_disjoint [of D E id])
   309 by auto
   310 
   311 lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)";
   312   apply (auto simp add: C_def)
   313   apply (insert finite_B SR_B_inj) 
   314   apply (frule_tac f1 = "StandardRes p" in setprod_reindex_id[THEN sym], auto)
   315   apply (rule setprod_same_function_zcong)
   316 by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   317 
   318 lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
   319   apply (rule Un_least)
   320 by (auto simp add: A_def F_subset D_subset)
   321 
   322 lemma two_eq: "2 * (x::int) = x + x";
   323   by arith
   324 
   325 lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
   326   apply (simp add: F_eq D_eq)
   327   apply (auto simp add: F_eq D_eq)
   328   proof -;
   329     fix y; fix ya;
   330     assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
   331     then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
   332       by arith
   333     moreover have "p dvd p";
   334       by auto
   335     ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
   336       by auto
   337     then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
   338       by (auto simp add: zcong_def)
   339     have "[y * a = StandardRes p (y * a)] (mod p)";
   340       by (simp only: zcong_sym StandardRes_prop1)
   341     moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
   342       by (simp only: zcong_sym StandardRes_prop1)
   343     ultimately have "[y * a + ya * a = 
   344         StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
   345       by (rule zcong_zadd)
   346     with a have "[y * a + ya * a = 0] (mod p)";
   347       apply (elim zcong_trans)
   348       by (simp only: zcong_refl)
   349     also have "y * a + ya * a = a * (y + ya)";
   350       by (simp add: zadd_zmult_distrib2 zmult_commute)
   351     finally have "[a * (y + ya) = 0] (mod p)";.;
   352     with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   353         p_a_relprime
   354         have a: "[y + ya = 0] (mod p)";
   355       by auto
   356     assume b: "y \<in> A" and c: "ya: A";
   357     with A_def have "0 < y + ya";
   358       by auto
   359     moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
   360       by auto 
   361     moreover from b c p_eq2 A_def have "y + ya < p";
   362       by auto
   363     ultimately show False;
   364       apply simp
   365       apply (frule_tac m = p in zcong_not_zero)
   366       by (auto simp add: a)
   367 qed;
   368 
   369 lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
   370   apply (insert F_D_disj finite_F finite_D)
   371   proof -;
   372     have "card (F \<union> D) = card E + card D";
   373       by (auto simp add: finite_F finite_D F_D_disj 
   374                          card_Un_disjoint F_card_eq_E)
   375     then have "card (F \<union> D) = card C";
   376       by (simp add: C_card_eq_D_plus_E)
   377     from this show "card (F \<union> D) = nat ((p - 1) div 2)"; 
   378       by (simp add: C_card_eq_B B_card_eq)
   379 qed;
   380 
   381 lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
   382   apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card) 
   383 by (auto simp add: card_seteq)
   384 
   385 lemma (in GAUSS) prod_D_F_eq_prod_A: 
   386     "(setprod id D) * (setprod id F) = setprod id A";
   387   apply (insert F_D_disj finite_D finite_F)
   388   apply (frule setprod_Un_disjoint [of F D id])
   389 by (auto simp add: F_Un_D_eq_A)
   390 
   391 lemma (in GAUSS) prod_F_zcong:
   392     "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   393   proof -
   394     have "setprod id F = setprod id (op - p ` E)"
   395       by (auto simp add: F_def)
   396     then have "setprod id F = setprod (op - p) E"
   397       apply simp
   398       apply (insert finite_E inj_on_pminusx_E)
   399       by (frule_tac f = "op - p" in setprod_reindex_id, auto)
   400     then have one: 
   401       "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
   402       apply simp
   403       apply (insert p_g_0 finite_E)
   404       by (auto simp add: StandardRes_prod)
   405     moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)"
   406       apply clarify
   407       apply (insert zcong_id [of p])
   408       by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
   409     moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)"
   410       apply clarify
   411       by (simp add: StandardRes_prop1 zcong_sym)
   412     moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)"
   413       apply clarify
   414       apply (insert a b)
   415       by (rule_tac b = "p - x" in zcong_trans, auto)
   416     ultimately have c:
   417       "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
   418       apply simp
   419       apply (insert finite_E p_g_0)
   420       by (rule setprod_same_function_zcong [of E "StandardRes p o (op - p)"
   421                                                      uminus p], auto)
   422     then have two: "[setprod id F = setprod (uminus) E](mod p)"
   423       apply (insert one c)
   424       by (rule zcong_trans [of "setprod id F" 
   425                                "setprod (StandardRes p o op - p) E" p
   426                                "setprod uminus E"], auto) 
   427     also have "setprod uminus E = (setprod id E) * (-1)^(card E)" 
   428       apply (insert finite_E)
   429       by (induct set: Finites, auto)
   430     then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   431       by (simp add: zmult_commute)
   432     with two show ?thesis
   433       by simp
   434 qed
   435 
   436 subsection {* Gauss' Lemma *}
   437 
   438 lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   439   by (auto simp add: finite_E neg_one_special)
   440 
   441 theorem (in GAUSS) pre_gauss_lemma:
   442     "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   443   proof -
   444     have "[setprod id A = setprod id F * setprod id D](mod p)"
   445       by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
   446     then have "[setprod id A = ((-1)^(card E) * setprod id E) * 
   447         setprod id D] (mod p)"
   448       apply (rule zcong_trans)
   449       by (auto simp add: prod_F_zcong zcong_scalar)
   450     then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   451       apply (rule zcong_trans)
   452       apply (insert C_prod_eq_D_times_E, erule subst)
   453       by (subst zmult_assoc, auto)
   454     then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   455       apply (rule zcong_trans)
   456       by (simp add: C_B_zcong_prod zcong_scalar2)
   457     then have "[setprod id A = ((-1)^(card E) *
   458         (setprod id ((%x. x * a) ` A)))] (mod p)"
   459       by (simp add: B_def)
   460     then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] 
   461         (mod p)"
   462       apply (rule zcong_trans)
   463       by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2)
   464     moreover have "setprod (%x. x * a) A = 
   465         setprod (%x. a) A * setprod id A"
   466       by (insert finite_A, induct set: Finites, auto)
   467     ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * 
   468         setprod id A))] (mod p)"
   469       by simp 
   470     then have "[setprod id A = ((-1)^(card E) * a^(card A) * 
   471         setprod id A)](mod p)"
   472       apply (rule zcong_trans)
   473       by (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant
   474         zmult_assoc)
   475     then have a: "[setprod id A * (-1)^(card E) = 
   476         ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
   477       by (rule zcong_scalar)
   478     then have "[setprod id A * (-1)^(card E) = setprod id A * 
   479         (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   480       apply (rule zcong_trans)
   481       by (simp add: a mult_commute mult_left_commute)
   482     then have "[setprod id A * (-1)^(card E) = setprod id A * 
   483         a^(card A)](mod p)"
   484       apply (rule zcong_trans)
   485       by (simp add: aux)
   486     with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   487          p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   488        by (simp add: order_less_imp_le)
   489     from this show ?thesis
   490       by (simp add: A_card_eq zcong_sym)
   491 qed
   492 
   493 theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   494 proof -
   495   from Euler_Criterion p_prime p_g_2 have
   496     "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   497     by auto
   498   moreover note pre_gauss_lemma
   499   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)"
   500     by (rule zcong_trans)
   501   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
   502     by (auto simp add: Legendre_def)
   503   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
   504     by (rule neg_one_power)
   505   ultimately show ?thesis
   506     by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   507 qed
   508 
   509 end