src/HOL/Number_Theory/Gauss.thy
author eberlm <eberlm@in.tum.de>
Mon Oct 17 15:20:06 2016 +0200 (2016-10-17)
changeset 64282 261d42f0bfac
parent 64272 f76b6dda2e56
child 64631 7705926ee595
permissions -rw-r--r--
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
lp15@55730
     1
(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
lp15@55730
     2
lp15@55730
     3
Ported by lcp but unfinished
lp15@55730
     4
*)
lp15@55730
     5
wenzelm@60526
     6
section \<open>Gauss' Lemma\<close>
lp15@55730
     7
lp15@55730
     8
theory Gauss
eberlm@64282
     9
imports Euler_Criterion
lp15@55730
    10
begin
lp15@55730
    11
lp15@55730
    12
lemma cong_prime_prod_zero_nat: 
lp15@55730
    13
  fixes a::nat
lp15@55730
    14
  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
lp15@55730
    15
  by (auto simp add: cong_altdef_nat)
lp15@55730
    16
lp15@55730
    17
lemma cong_prime_prod_zero_int: 
lp15@55730
    18
  fixes a::int
lp15@55730
    19
  shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
lp15@55730
    20
  by (auto simp add: cong_altdef_int)
lp15@55730
    21
lp15@55730
    22
lp15@55730
    23
locale GAUSS =
lp15@55730
    24
  fixes p :: "nat"
lp15@55730
    25
  fixes a :: "int"
lp15@55730
    26
lp15@55730
    27
  assumes p_prime: "prime p"
lp15@55730
    28
  assumes p_ge_2: "2 < p"
lp15@55730
    29
  assumes p_a_relprime: "[a \<noteq> 0](mod p)"
lp15@55730
    30
  assumes a_nonzero:    "0 < a"
lp15@55730
    31
begin
lp15@55730
    32
lp15@55730
    33
definition "A = {0::int <.. ((int p - 1) div 2)}"
lp15@55730
    34
definition "B = (\<lambda>x. x * a) ` A"
lp15@55730
    35
definition "C = (\<lambda>x. x mod p) ` B"
lp15@55730
    36
definition "D = C \<inter> {.. (int p - 1) div 2}"
lp15@55730
    37
definition "E = C \<inter> {(int p - 1) div 2 <..}"
lp15@55730
    38
definition "F = (\<lambda>x. (int p - x)) ` E"
lp15@55730
    39
lp15@55730
    40
wenzelm@60526
    41
subsection \<open>Basic properties of p\<close>
lp15@55730
    42
lp15@55730
    43
lemma odd_p: "odd p"
lp15@55730
    44
by (metis p_prime p_ge_2 prime_odd_nat)
lp15@55730
    45
lp15@55730
    46
lemma p_minus_one_l: "(int p - 1) div 2 < p"
lp15@55730
    47
proof -
lp15@55730
    48
  have "(p - 1) div 2 \<le> (p - 1) div 1"
lp15@55730
    49
    by (metis div_by_1 div_le_dividend)
lp15@55730
    50
  also have "\<dots> = p - 1" by simp
lp15@55730
    51
  finally show ?thesis using p_ge_2 by arith
lp15@55730
    52
qed
lp15@55730
    53
lp15@55730
    54
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
haftmann@64240
    55
  using odd_p p_ge_2 nonzero_mult_div_cancel_left [of 2 "p - 1"]   
haftmann@58834
    56
  by simp
lp15@55730
    57
lp15@55730
    58
lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
lp15@55730
    59
  using odd_p p_ge_2
haftmann@58645
    60
  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
lp15@55730
    61
lp15@55730
    62
wenzelm@60526
    63
subsection \<open>Basic Properties of the Gauss Sets\<close>
lp15@55730
    64
lp15@55730
    65
lemma finite_A: "finite (A)"
lp15@55730
    66
by (auto simp add: A_def)
lp15@55730
    67
lp15@55730
    68
lemma finite_B: "finite (B)"
lp15@55730
    69
by (auto simp add: B_def finite_A)
lp15@55730
    70
lp15@55730
    71
lemma finite_C: "finite (C)"
lp15@55730
    72
by (auto simp add: C_def finite_B)
lp15@55730
    73
lp15@55730
    74
lemma finite_D: "finite (D)"
lp15@55730
    75
by (auto simp add: D_def finite_C)
lp15@55730
    76
lp15@55730
    77
lemma finite_E: "finite (E)"
lp15@55730
    78
by (auto simp add: E_def finite_C)
lp15@55730
    79
lp15@55730
    80
lemma finite_F: "finite (F)"
lp15@55730
    81
by (auto simp add: F_def finite_E)
lp15@55730
    82
lp15@55730
    83
lemma C_eq: "C = D \<union> E"
lp15@55730
    84
by (auto simp add: C_def D_def E_def)
lp15@55730
    85
lp15@55730
    86
lemma A_card_eq: "card A = nat ((int p - 1) div 2)"
lp15@55730
    87
  by (auto simp add: A_def)
lp15@55730
    88
lp15@55730
    89
lemma inj_on_xa_A: "inj_on (\<lambda>x. x * a) A"
lp15@55730
    90
  using a_nonzero by (simp add: A_def inj_on_def)
lp15@55730
    91
lp15@55730
    92
definition ResSet :: "int => int set => bool"
lp15@55730
    93
  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
lp15@55730
    94
lp15@55730
    95
lemma ResSet_image:
lp15@55730
    96
  "\<lbrakk> 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) \<rbrakk> \<Longrightarrow>
lp15@55730
    97
    ResSet m (f ` A)"
lp15@55730
    98
  by (auto simp add: ResSet_def)
lp15@55730
    99
lp15@55730
   100
lemma A_res: "ResSet p A"
lp15@55730
   101
  using p_ge_2
lp15@55730
   102
  by (auto simp add: A_def ResSet_def intro!: cong_less_imp_eq_int)
lp15@55730
   103
lp15@55730
   104
lemma B_res: "ResSet p B"
lp15@55730
   105
proof -
lp15@55730
   106
  {fix x fix y
lp15@55730
   107
    assume a: "[x * a = y * a] (mod p)"
lp15@55730
   108
    assume b: "0 < x"
lp15@55730
   109
    assume c: "x \<le> (int p - 1) div 2"
lp15@55730
   110
    assume d: "0 < y"
lp15@55730
   111
    assume e: "y \<le> (int p - 1) div 2"
eberlm@63534
   112
    from p_a_relprime have "\<not>p dvd a"
eberlm@63534
   113
      by (simp add: cong_altdef_int)
eberlm@63534
   114
    with p_prime have "coprime a (int p)" 
eberlm@63633
   115
       by (subst gcd.commute, intro prime_imp_coprime) auto
eberlm@63534
   116
    with a cong_mult_rcancel_int [of a "int p" x y]
eberlm@63534
   117
      have "[x = y] (mod p)" by simp
lp15@55730
   118
    with cong_less_imp_eq_int [of x y p] p_minus_one_l
lp15@55730
   119
        order_le_less_trans [of x "(int p - 1) div 2" p]
lp15@55730
   120
        order_le_less_trans [of y "(int p - 1) div 2" p] 
lp15@55730
   121
    have "x = y"
haftmann@62348
   122
      by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
lp15@55730
   123
    } note xy = this
lp15@55730
   124
  show ?thesis
lp15@55730
   125
    apply (insert p_ge_2 p_a_relprime p_minus_one_l)
lp15@55730
   126
    apply (auto simp add: B_def)
lp15@55730
   127
    apply (rule ResSet_image)
lp15@55730
   128
    apply (auto simp add: A_res)
lp15@55730
   129
    apply (auto simp add: A_def xy)
lp15@55730
   130
    done
lp15@55730
   131
  qed
lp15@55730
   132
lp15@55730
   133
lemma SR_B_inj: "inj_on (\<lambda>x. x mod p) B"
lp15@55730
   134
proof -
lp15@55730
   135
{ fix x fix y
lp15@55730
   136
  assume a: "x * a mod p = y * a mod p"
lp15@55730
   137
  assume b: "0 < x"
lp15@55730
   138
  assume c: "x \<le> (int p - 1) div 2"
lp15@55730
   139
  assume d: "0 < y"
lp15@55730
   140
  assume e: "y \<le> (int p - 1) div 2"
lp15@55730
   141
  assume f: "x \<noteq> y"
eberlm@63534
   142
  from a have a': "[x * a = y * a](mod p)" 
lp15@55730
   143
    by (metis cong_int_def)
eberlm@63534
   144
  from p_a_relprime have "\<not>p dvd a"
eberlm@63534
   145
    by (simp add: cong_altdef_int)
eberlm@63534
   146
  with p_prime have "coprime a (int p)" 
eberlm@63633
   147
     by (subst gcd.commute, intro prime_imp_coprime) auto
eberlm@63534
   148
  with a' cong_mult_rcancel_int [of a "int p" x y]
eberlm@63534
   149
    have "[x = y] (mod p)" by simp
lp15@55730
   150
  with cong_less_imp_eq_int [of x y p] p_minus_one_l
lp15@55730
   151
    order_le_less_trans [of x "(int p - 1) div 2" p]
lp15@55730
   152
    order_le_less_trans [of y "(int p - 1) div 2" p] 
lp15@55730
   153
  have "x = y"
haftmann@62348
   154
    by (metis b c cong_less_imp_eq_int d e zero_less_imp_eq_int of_nat_0_le_iff)
lp15@55730
   155
  then have False
lp15@55730
   156
    by (simp add: f)}
lp15@55730
   157
  then show ?thesis
lp15@55730
   158
    by (auto simp add: B_def inj_on_def A_def) metis
lp15@55730
   159
qed
lp15@55730
   160
lp15@55730
   161
lemma inj_on_pminusx_E: "inj_on (\<lambda>x. p - x) E"
lp15@55730
   162
  apply (auto simp add: E_def C_def B_def A_def)
lp15@55730
   163
  apply (rule_tac g = "(op - (int p))" in inj_on_inverseI)
lp15@55730
   164
  apply auto
lp15@55730
   165
  done
lp15@55730
   166
lp15@55730
   167
lemma nonzero_mod_p:
lp15@55730
   168
  fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
haftmann@59545
   169
  by (simp add: cong_int_def)
lp15@55730
   170
lp15@55730
   171
lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
lp15@55730
   172
  by (rule nonzero_mod_p) (auto simp add: A_def)
lp15@55730
   173
lp15@55730
   174
lemma A_greater_zero: "x \<in> A \<Longrightarrow> 0 < x"
lp15@55730
   175
  by (auto simp add: A_def)
lp15@55730
   176
lp15@55730
   177
lemma B_ncong_p: "x \<in> B \<Longrightarrow> [x \<noteq> 0](mod p)"
eberlm@63534
   178
  by (auto simp: B_def p_prime p_a_relprime A_ncong_p dest: cong_prime_prod_zero_int) 
lp15@55730
   179
lp15@55730
   180
lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
nipkow@56544
   181
  using a_nonzero by (auto simp add: B_def A_greater_zero)
lp15@55730
   182
lp15@55730
   183
lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
lp15@55730
   184
proof (auto simp add: C_def)
lp15@55730
   185
  fix x :: int
lp15@55730
   186
  assume a1: "x \<in> B"
lp15@55730
   187
  have f2: "\<And>x\<^sub>1. int x\<^sub>1 = 0 \<or> 0 < int x\<^sub>1" by linarith
lp15@55730
   188
  have "x mod int p \<noteq> 0" using a1 B_ncong_p cong_int_def by simp
lp15@55730
   189
  thus "0 < x mod int p" using a1 f2 
lp15@55730
   190
    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
lp15@55730
   191
qed
lp15@55730
   192
lp15@55730
   193
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((int p - 1) div 2)}"
lp15@55730
   194
  apply (auto simp add: F_def E_def C_def)
lp15@55730
   195
  apply (metis p_ge_2 Divides.pos_mod_bound less_diff_eq nat_int plus_int_code(2) zless_nat_conj)
lp15@55730
   196
  apply (auto intro: p_odd_int)
lp15@55730
   197
  done
lp15@55730
   198
lp15@55730
   199
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
lp15@55730
   200
  by (auto simp add: D_def C_greater_zero)
lp15@55730
   201
lp15@55730
   202
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - ((y*a) mod p) & (int p - 1) div 2 < (y*a) mod p)}"
lp15@55730
   203
  by (auto simp add: F_def E_def D_def C_def B_def A_def)
lp15@55730
   204
lp15@55730
   205
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = (y*a) mod p & (y*a) mod p \<le> (int p - 1) div 2)}"
lp15@55730
   206
  by (auto simp add: D_def C_def B_def A_def)
lp15@55730
   207
lp15@55730
   208
lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
lp15@55730
   209
  using p_prime A_ncong_p [OF assms]
eberlm@63633
   210
  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
lp15@55730
   211
nipkow@64272
   212
lemma A_prod_relprime: "gcd (prod id A) p = 1"
nipkow@64272
   213
  by (metis id_def all_A_relprime prod_coprime)
lp15@55730
   214
lp15@55730
   215
wenzelm@60526
   216
subsection \<open>Relationships Between Gauss Sets\<close>
lp15@55730
   217
lp15@55730
   218
lemma StandardRes_inj_on_ResSet: "ResSet m X \<Longrightarrow> (inj_on (\<lambda>b. b mod m) X)"
lp15@55730
   219
  by (auto simp add: ResSet_def inj_on_def cong_int_def)
lp15@55730
   220
lp15@55730
   221
lemma B_card_eq_A: "card B = card A"
lp15@55730
   222
  using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
lp15@55730
   223
lp15@55730
   224
lemma B_card_eq: "card B = nat ((int p - 1) div 2)"
lp15@55730
   225
  by (simp add: B_card_eq_A A_card_eq)
lp15@55730
   226
lp15@55730
   227
lemma F_card_eq_E: "card F = card E"
lp15@55730
   228
  using finite_E 
lp15@55730
   229
  by (simp add: F_def inj_on_pminusx_E card_image)
lp15@55730
   230
lp15@55730
   231
lemma C_card_eq_B: "card C = card B"
lp15@55730
   232
proof -
lp15@55730
   233
  have "inj_on (\<lambda>x. x mod p) B"
lp15@55730
   234
    by (metis SR_B_inj) 
lp15@55730
   235
  then show ?thesis
lp15@55730
   236
    by (metis C_def card_image)
lp15@55730
   237
qed
lp15@55730
   238
lp15@55730
   239
lemma D_E_disj: "D \<inter> E = {}"
lp15@55730
   240
  by (auto simp add: D_def E_def)
lp15@55730
   241
lp15@55730
   242
lemma C_card_eq_D_plus_E: "card C = card D + card E"
lp15@55730
   243
  by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
lp15@55730
   244
nipkow@64272
   245
lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
nipkow@64272
   246
  by (metis C_eq D_E_disj finite_D finite_E inf_commute prod.union_disjoint sup_commute)
lp15@55730
   247
nipkow@64272
   248
lemma C_B_zcong_prod: "[prod id C = prod id B] (mod p)"
lp15@55730
   249
  apply (auto simp add: C_def)
lp15@55730
   250
  apply (insert finite_B SR_B_inj)
nipkow@64272
   251
  apply (drule prod.reindex [of "\<lambda>x. x mod int p" B id])
haftmann@57418
   252
  apply auto
nipkow@64272
   253
  apply (rule cong_prod_int)
lp15@55730
   254
  apply (auto simp add: cong_int_def)
lp15@55730
   255
  done
lp15@55730
   256
lp15@55730
   257
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
lp15@55730
   258
  apply (intro Un_least subset_trans [OF F_subset] subset_trans [OF D_subset])
lp15@55730
   259
  apply (auto simp add: A_def)
lp15@55730
   260
  done
lp15@55730
   261
lp15@55730
   262
lemma F_D_disj: "(F \<inter> D) = {}"
lp15@55730
   263
proof (auto simp add: F_eq D_eq)
lp15@55730
   264
  fix y::int and z::int
lp15@55730
   265
  assume "p - (y*a) mod p = (z*a) mod p"
lp15@55730
   266
  then have "[(y*a) mod p + (z*a) mod p = 0] (mod p)"
haftmann@57512
   267
    by (metis add.commute diff_eq_eq dvd_refl cong_int_def dvd_eq_mod_eq_0 mod_0)
lp15@55730
   268
  moreover have "[y * a = (y*a) mod p] (mod p)"
lp15@55730
   269
    by (metis cong_int_def mod_mod_trivial)
lp15@55730
   270
  ultimately have "[a * (y + z) = 0] (mod p)"
haftmann@57512
   271
    by (metis cong_int_def mod_add_left_eq mod_add_right_eq mult.commute ring_class.ring_distribs(1))
lp15@55730
   272
  with p_prime a_nonzero p_a_relprime
lp15@55730
   273
  have a: "[y + z = 0] (mod p)"
eberlm@63534
   274
    by (auto dest!: cong_prime_prod_zero_int)
lp15@55730
   275
  assume b: "y \<in> A" and c: "z \<in> A"
lp15@55730
   276
  with A_def have "0 < y + z"
lp15@55730
   277
    by auto
lp15@55730
   278
  moreover from b c p_eq2 A_def have "y + z < p"
lp15@55730
   279
    by auto
lp15@55730
   280
  ultimately show False
lp15@55730
   281
    by (metis a nonzero_mod_p)
lp15@55730
   282
qed
lp15@55730
   283
lp15@55730
   284
lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
lp15@55730
   285
proof -
lp15@55730
   286
  have "card (F \<union> D) = card E + card D"
lp15@55730
   287
    by (auto simp add: finite_F finite_D F_D_disj card_Un_disjoint F_card_eq_E)
lp15@55730
   288
  then have "card (F \<union> D) = card C"
lp15@55730
   289
    by (simp add: C_card_eq_D_plus_E)
lp15@55730
   290
  then show "card (F \<union> D) = nat ((p - 1) div 2)"
lp15@55730
   291
    by (simp add: C_card_eq_B B_card_eq)
lp15@55730
   292
qed
lp15@55730
   293
lp15@55730
   294
lemma F_Un_D_eq_A: "F \<union> D = A"
lp15@55730
   295
  using finite_A F_Un_D_subset A_card_eq F_Un_D_card 
lp15@55730
   296
  by (auto simp add: card_seteq)
lp15@55730
   297
nipkow@64272
   298
lemma prod_D_F_eq_prod_A: "(prod id D) * (prod id F) = prod id A"
nipkow@64272
   299
  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F prod.union_disjoint)
lp15@55730
   300
nipkow@64272
   301
lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
lp15@55730
   302
proof -
nipkow@64272
   303
  have FE: "prod id F = prod (op - p) E"
lp15@55730
   304
    apply (auto simp add: F_def)
lp15@55730
   305
    apply (insert finite_E inj_on_pminusx_E)
nipkow@64272
   306
    apply (drule prod.reindex, auto)
lp15@55730
   307
    done
lp15@55730
   308
  then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
lp15@55730
   309
    by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
nipkow@64272
   310
  then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
lp15@55730
   311
    using finite_E p_ge_2
nipkow@64272
   312
          cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
lp15@55730
   313
    by auto
nipkow@64272
   314
  then have two: "[prod id F = prod (uminus) E](mod p)"
nipkow@64272
   315
    by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
nipkow@64272
   316
  have "prod uminus E = (-1) ^ (card E) * (prod id E)"
lp15@55730
   317
    using finite_E by (induct set: finite) auto
lp15@55730
   318
  with two show ?thesis
lp15@55730
   319
    by simp
lp15@55730
   320
qed
lp15@55730
   321
lp15@55730
   322
wenzelm@60526
   323
subsection \<open>Gauss' Lemma\<close>
lp15@55730
   324
nipkow@64272
   325
lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
haftmann@57512
   326
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
lp15@55730
   327
lp15@55730
   328
theorem pre_gauss_lemma:
lp15@55730
   329
  "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
lp15@55730
   330
proof -
nipkow@64272
   331
  have "[prod id A = prod id F * prod id D](mod p)"
nipkow@64272
   332
    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
nipkow@64272
   333
  then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
lp15@55730
   334
    apply (rule cong_trans_int)
lp15@55730
   335
    apply (metis cong_scalar_int prod_F_zcong)
lp15@55730
   336
    done
nipkow@64272
   337
  then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
haftmann@57512
   338
    by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
nipkow@64272
   339
  then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
lp15@55730
   340
    by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
nipkow@64272
   341
  then have "[prod id A = ((-1)^(card E) *
nipkow@64272
   342
    (prod id ((\<lambda>x. x * a) ` A)))] (mod p)"
lp15@55730
   343
    by (simp add: B_def)
nipkow@64272
   344
  then have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. x * a) A))]
lp15@55730
   345
    (mod p)"
nipkow@64272
   346
    by (simp add: inj_on_xa_A prod.reindex)
nipkow@64272
   347
  moreover have "prod (\<lambda>x. x * a) A =
nipkow@64272
   348
    prod (\<lambda>x. a) A * prod id A"
lp15@55730
   349
    using finite_A by (induct set: finite) auto
nipkow@64272
   350
  ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A *
nipkow@64272
   351
    prod id A))] (mod p)"
lp15@55730
   352
    by simp
nipkow@64272
   353
  then have "[prod id A = ((-1)^(card E) * a^(card A) *
nipkow@64272
   354
      prod id A)](mod p)"
lp15@55730
   355
    apply (rule cong_trans_int)
nipkow@64272
   356
    apply (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
lp15@55730
   357
    done
nipkow@64272
   358
  then have a: "[prod id A * (-1)^(card E) =
nipkow@64272
   359
      ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
lp15@55730
   360
    by (rule cong_scalar_int)
nipkow@64272
   361
  then have "[prod id A * (-1)^(card E) = prod id A *
lp15@55730
   362
      (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
lp15@55730
   363
    apply (rule cong_trans_int)
haftmann@57512
   364
    apply (simp add: a mult.commute mult.left_commute)
lp15@55730
   365
    done
nipkow@64272
   366
  then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
lp15@55730
   367
    apply (rule cong_trans_int)
nipkow@64272
   368
    apply (simp add: aux cong del: prod.strong_cong)
lp15@55730
   369
    done
haftmann@58410
   370
  with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
lp15@55730
   371
    by (metis cong_mult_lcancel_int)
lp15@55730
   372
  then show ?thesis
lp15@55730
   373
    by (simp add: A_card_eq cong_sym_int)
lp15@55730
   374
qed
lp15@55730
   375
lp15@55730
   376
theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
lp15@55730
   377
proof -
eberlm@64282
   378
  from euler_criterion p_prime p_ge_2 have
lp15@55730
   379
      "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
lp15@55730
   380
    by auto
eberlm@64282
   381
  moreover have "int ((p - 1) div 2) =(int p - 1) div 2" using p_eq2 by linarith
eberlm@64282
   382
    hence "[a ^ nat (int ((p - 1) div 2)) = a ^ nat ((int p - 1) div 2)] (mod int p)" by force
lp15@55730
   383
  moreover note pre_gauss_lemma
eberlm@64282
   384
  ultimately have "[(Legendre a p) = (-1) ^ (card E)] (mod p)" using cong_trans_int by blast
lp15@55730
   385
  moreover from p_a_relprime have "(Legendre a p) = 1 | (Legendre a p) = (-1)"
lp15@55730
   386
    by (auto simp add: Legendre_def)
lp15@55730
   387
  moreover have "(-1::int) ^ (card E) = 1 | (-1::int) ^ (card E) = -1"
eberlm@64282
   388
    using neg_one_even_power neg_one_odd_power by blast
eberlm@64282
   389
  moreover have "[1 \<noteq> - 1] (mod int p)"
eberlm@64282
   390
    using cong_altdef_int nonzero_mod_p[of 2] p_odd_int by fastforce
lp15@55730
   391
  ultimately show ?thesis
eberlm@64282
   392
    by (auto simp add: cong_sym_int)
lp15@55730
   393
qed
lp15@55730
   394
lp15@55730
   395
end
lp15@55730
   396
lp15@55730
   397
end