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