src/HOL/NumberTheory/Gauss.thy
 author paulson Fri Mar 05 11:43:55 2004 +0100 (2004-03-05) changeset 14434 5f14c1207499 parent 14353 79f9fbef9106 child 14981 e73f8140af78 permissions -rw-r--r--
patch to NumberTheory problems caused by Parity
```     1 (*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
```
```     2     Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
```
```     3     License:    GPL (GNU GENERAL PUBLIC LICENSE)
```
```     4 *)
```
```     5
```
```     6 header {* Gauss' Lemma *}
```
```     7
```
```     8 theory Gauss = Euler:;
```
```     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((gsetprod 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: "gsetprod id E * gsetprod id D = gsetprod id C";
```
```   307   apply (insert D_E_disj finite_D finite_E C_eq)
```
```   308   apply (frule gsetprod_Un_disjoint [of D E id])
```
```   309 by auto
```
```   310
```
```   311 lemma (in GAUSS) C_B_zcong_prod: "[gsetprod id C = gsetprod id B] (mod p)";
```
```   312 thm gsetprod_same_function_zcong;
```
```   313   apply (auto simp add: C_def)
```
```   314   apply (insert finite_B SR_B_inj)
```
```   315   apply (frule_tac f = "StandardRes p" in prod_prop_id, auto)
```
```   316   apply (rule gsetprod_same_function_zcong)
```
```   317 by (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
```
```   318
```
```   319 lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A";
```
```   320   apply (rule Un_least)
```
```   321 by (auto simp add: A_def F_subset D_subset)
```
```   322
```
```   323 lemma two_eq: "2 * (x::int) = x + x";
```
```   324   by arith
```
```   325
```
```   326 lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}";
```
```   327   apply (simp add: F_eq D_eq)
```
```   328   apply (auto simp add: F_eq D_eq)
```
```   329   proof -;
```
```   330     fix y; fix ya;
```
```   331     assume "p - StandardRes p (y * a) = StandardRes p (ya * a)";
```
```   332     then have "p = StandardRes p (y * a) + StandardRes p (ya * a)";
```
```   333       by arith
```
```   334     moreover have "p dvd p";
```
```   335       by auto
```
```   336     ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))";
```
```   337       by auto
```
```   338     then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)";
```
```   339       by (auto simp add: zcong_def)
```
```   340     have "[y * a = StandardRes p (y * a)] (mod p)";
```
```   341       by (simp only: zcong_sym StandardRes_prop1)
```
```   342     moreover have "[ya * a = StandardRes p (ya * a)] (mod p)";
```
```   343       by (simp only: zcong_sym StandardRes_prop1)
```
```   344     ultimately have "[y * a + ya * a =
```
```   345         StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)";
```
```   346       by (rule zcong_zadd)
```
```   347     with a have "[y * a + ya * a = 0] (mod p)";
```
```   348       apply (elim zcong_trans)
```
```   349       by (simp only: zcong_refl)
```
```   350     also have "y * a + ya * a = a * (y + ya)";
```
```   351       by (simp add: zadd_zmult_distrib2 zmult_commute)
```
```   352     finally have "[a * (y + ya) = 0] (mod p)";.;
```
```   353     with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
```
```   354         p_a_relprime
```
```   355         have a: "[y + ya = 0] (mod p)";
```
```   356       by auto
```
```   357     assume b: "y \<in> A" and c: "ya: A";
```
```   358     with A_def have "0 < y + ya";
```
```   359       by auto
```
```   360     moreover from b c A_def have "y + ya \<le> (p - 1) div 2 + (p - 1) div 2";
```
```   361       by auto
```
```   362     moreover from b c p_eq2 A_def have "y + ya < p";
```
```   363       by auto
```
```   364     ultimately show False;
```
```   365       apply simp
```
```   366       apply (frule_tac m = p in zcong_not_zero)
```
```   367       by (auto simp add: a)
```
```   368 qed;
```
```   369
```
```   370 lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)";
```
```   371   apply (insert F_D_disj finite_F finite_D)
```
```   372   proof -;
```
```   373     have "card (F \<union> D) = card E + card D";
```
```   374       by (auto simp add: finite_F finite_D F_D_disj
```
```   375                          card_Un_disjoint F_card_eq_E)
```
```   376     then have "card (F \<union> D) = card C";
```
```   377       by (simp add: C_card_eq_D_plus_E)
```
```   378     from this show "card (F \<union> D) = nat ((p - 1) div 2)";
```
```   379       by (simp add: C_card_eq_B B_card_eq)
```
```   380 qed;
```
```   381
```
```   382 lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A";
```
```   383   apply (insert finite_A F_Un_D_subset A_card_eq F_Un_D_card)
```
```   384 by (auto simp add: card_seteq)
```
```   385
```
```   386 lemma (in GAUSS) prod_D_F_eq_prod_A:
```
```   387     "(gsetprod id D) * (gsetprod id F) = gsetprod id A";
```
```   388   apply (insert F_D_disj finite_D finite_F)
```
```   389   apply (frule gsetprod_Un_disjoint [of F D id])
```
```   390 by (auto simp add: F_Un_D_eq_A)
```
```   391
```
```   392 lemma (in GAUSS) prod_F_zcong:
```
```   393     "[gsetprod id F = ((-1) ^ (card E)) * (gsetprod id E)] (mod p)";
```
```   394   proof -;
```
```   395     have "gsetprod id F = gsetprod id (op - p ` E)";
```
```   396       by (auto simp add: F_def)
```
```   397     then have "gsetprod id F = gsetprod (op - p) E";
```
```   398       apply simp
```
```   399       apply (insert finite_E inj_on_pminusx_E)
```
```   400       by (frule_tac f = "op - p" in prod_prop_id, auto)
```
```   401     then have one:
```
```   402       "[gsetprod id F = gsetprod (StandardRes p o (op - p)) E] (mod p)";
```
```   403       apply simp
```
```   404       apply (insert p_g_0 finite_E)
```
```   405       by (auto simp add: StandardRes_prod)
```
```   406     moreover have a: "\<forall>x \<in> E. [p - x = 0 - x] (mod p)";
```
```   407       apply clarify
```
```   408       apply (insert zcong_id [of p])
```
```   409       by (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto)
```
```   410     moreover have b: "\<forall>x \<in> E. [StandardRes p (p - x) = p - x](mod p)";
```
```   411       apply clarify
```
```   412       by (simp add: StandardRes_prop1 zcong_sym)
```
```   413     moreover have "\<forall>x \<in> E. [StandardRes p (p - x) = - x](mod p)";
```
```   414       apply clarify
```
```   415       apply (insert a b)
```
```   416       by (rule_tac b = "p - x" in zcong_trans, auto)
```
```   417     ultimately have c:
```
```   418       "[gsetprod (StandardRes p o (op - p)) E = gsetprod (uminus) E](mod p)";
```
```   419       apply simp
```
```   420       apply (insert finite_E p_g_0)
```
```   421       by (frule gsetprod_same_function_zcong [of E "StandardRes p o (op - p)"
```
```   422                                                      uminus p], auto);
```
```   423     then have two: "[gsetprod id F = gsetprod (uminus) E](mod p)";
```
```   424       apply (insert one c)
```
```   425       by (rule zcong_trans [of "gsetprod id F"
```
```   426                                "gsetprod (StandardRes p o op - p) E" p
```
```   427                                "gsetprod uminus E"], auto);
```
```   428     also have "gsetprod uminus E = (gsetprod id E) * (-1)^(card E)";
```
```   429       apply (insert finite_E)
```
```   430       by (induct set: Finites, auto)
```
```   431     then have "gsetprod uminus E = (-1) ^ (card E) * (gsetprod id E)";
```
```   432       by (simp add: zmult_commute)
```
```   433     with two show ?thesis
```
```   434       by simp
```
```   435 qed;
```
```   436
```
```   437 subsection {* Gauss' Lemma *}
```
```   438
```
```   439 lemma (in GAUSS) aux: "gsetprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = gsetprod id A * a ^ card A";
```
```   440   by (auto simp add: finite_E neg_one_special)
```
```   441
```
```   442 theorem (in GAUSS) pre_gauss_lemma:
```
```   443     "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)";
```
```   444   proof -;
```
```   445     have "[gsetprod id A = gsetprod id F * gsetprod id D](mod p)";
```
```   446       by (auto simp add: prod_D_F_eq_prod_A zmult_commute)
```
```   447     then have "[gsetprod id A = ((-1)^(card E) * gsetprod id E) *
```
```   448         gsetprod id D] (mod p)";
```
```   449       apply (rule zcong_trans)
```
```   450       by (auto simp add: prod_F_zcong zcong_scalar)
```
```   451     then have "[gsetprod id A = ((-1)^(card E) * gsetprod id C)] (mod p)";
```
```   452       apply (rule zcong_trans)
```
```   453       apply (insert C_prod_eq_D_times_E, erule subst)
```
```   454       by (subst zmult_assoc, auto)
```
```   455     then have "[gsetprod id A = ((-1)^(card E) * gsetprod id B)] (mod p)"
```
```   456       apply (rule zcong_trans)
```
```   457       by (simp add: C_B_zcong_prod zcong_scalar2)
```
```   458     then have "[gsetprod id A = ((-1)^(card E) *
```
```   459         (gsetprod id ((%x. x * a) ` A)))] (mod p)";
```
```   460       by (simp add: B_def)
```
```   461     then have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. x * a) A))]
```
```   462         (mod p)";
```
```   463       apply (rule zcong_trans)
```
```   464       by (simp add: finite_A inj_on_xa_A prod_prop_id zcong_scalar2)
```
```   465     moreover have "gsetprod (%x. x * a) A =
```
```   466         gsetprod (%x. a) A * gsetprod id A";
```
```   467       by (insert finite_A, induct set: Finites, auto)
```
```   468     ultimately have "[gsetprod id A = ((-1)^(card E) * (gsetprod (%x. a) A *
```
```   469         gsetprod id A))] (mod p)";
```
```   470       by simp
```
```   471     then have "[gsetprod id A = ((-1)^(card E) * a^(card A) *
```
```   472         gsetprod id A)](mod p)";
```
```   473       apply (rule zcong_trans)
```
```   474       by (simp add: zcong_scalar2 zcong_scalar finite_A gsetprod_const
```
```   475         zmult_assoc)
```
```   476     then have a: "[gsetprod id A * (-1)^(card E) =
```
```   477         ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)";
```
```   478       by (rule zcong_scalar)
```
```   479     then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
```
```   480         (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)";
```
```   481       apply (rule zcong_trans)
```
```   482       by (simp add: a mult_commute mult_left_commute)
```
```   483     then have "[gsetprod id A * (-1)^(card E) = gsetprod id A *
```
```   484         a^(card A)](mod p)";
```
```   485       apply (rule zcong_trans)
```
```   486       by (simp add: aux)
```
```   487     with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"]
```
```   488          p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)";
```
```   489        by (simp add: order_less_imp_le)
```
```   490     from this show ?thesis
```
```   491       by (simp add: A_card_eq zcong_sym)
```
```   492 qed;
```
```   493
```
```   494 theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)";
```
```   495 proof -;
```
```   496   from Euler_Criterion p_prime p_g_2 have
```
```   497     "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)";
```
```   498     by auto
```
```   499   moreover note pre_gauss_lemma;
```
```   500   ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)";
```
```   501     by (rule zcong_trans)
```
```   502   moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)";
```
```   503     by (auto simp add: Legendre_def)
```
```   504   moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1";
```
```   505     by (rule neg_one_power)
```
```   506   ultimately show ?thesis;
```
```   507     by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
```
```   508 qed;
```
```   509
```
`   510 end;`