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