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