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