src/HOL/NumberTheory/Euler.thy
author nipkow
Fri Jul 01 17:41:10 2005 +0200 (2005-07-01)
changeset 16663 13e9c402308b
parent 16417 9bc16273c2d4
child 16733 236dfafbeb63
permissions -rw-r--r--
prime is a predicate now.
paulson@13871
     1
(*  Title:      HOL/Quadratic_Reciprocity/Euler.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 {* Euler's criterion *}
paulson@13871
     7
haftmann@16417
     8
theory Euler imports Residues EvenOdd begin;
paulson@13871
     9
paulson@13871
    10
constdefs
paulson@13871
    11
  MultInvPair :: "int => int => int => int set"
paulson@13871
    12
  "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
paulson@13871
    13
  SetS        :: "int => int => int set set"
paulson@13871
    14
  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))";
paulson@13871
    15
paulson@13871
    16
(****************************************************************)
paulson@13871
    17
(*                                                              *)
paulson@13871
    18
(* Property for MultInvPair                                     *)
paulson@13871
    19
(*                                                              *)
paulson@13871
    20
(****************************************************************)
paulson@13871
    21
nipkow@16663
    22
lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
paulson@13871
    23
                              X \<in> (SetS a p); Y \<in> (SetS a p);
paulson@13871
    24
                              ~((X \<inter> Y) = {}) |] ==> 
paulson@13871
    25
                           X = Y";
paulson@13871
    26
  apply (auto simp add: SetS_def)
paulson@13871
    27
  apply (drule StandardRes_SRStar_prop1a)+; defer 1;
paulson@13871
    28
  apply (drule StandardRes_SRStar_prop1a)+;
paulson@13871
    29
  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
paulson@13871
    30
  apply (drule notE, rule MultInv_zcong_prop1, auto)
paulson@13871
    31
  apply (drule notE, rule MultInv_zcong_prop2, auto)
paulson@13871
    32
  apply (drule MultInv_zcong_prop2, auto)
paulson@13871
    33
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
paulson@13871
    34
  apply (drule MultInv_zcong_prop1, auto)
paulson@13871
    35
  apply (drule MultInv_zcong_prop2, auto)
paulson@13871
    36
  apply (drule MultInv_zcong_prop2, auto)
paulson@13871
    37
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
paulson@13871
    38
done
paulson@13871
    39
nipkow@16663
    40
lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
paulson@13871
    41
                              X \<in> (SetS a p); Y \<in> (SetS a p);
paulson@13871
    42
                              X \<noteq> Y |] ==>
paulson@13871
    43
                              X \<inter> Y = {}";
paulson@13871
    44
  apply (rule notnotD)
paulson@13871
    45
  apply (rule notI)
paulson@13871
    46
  apply (drule MultInvPair_prop1a, auto)
paulson@13871
    47
done
paulson@13871
    48
nipkow@16663
    49
lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
paulson@13871
    50
    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
paulson@13871
    51
  by (auto simp add: MultInvPair_prop1b)
paulson@13871
    52
nipkow@16663
    53
lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
paulson@13871
    54
                          Union ( SetS a p) = SRStar p";
paulson@13871
    55
  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
paulson@13871
    56
    SRStar_mult_prop2)
paulson@13871
    57
  apply (frule StandardRes_SRStar_prop3)
paulson@13871
    58
  apply (rule bexI, auto)
paulson@13871
    59
done
paulson@13871
    60
nipkow@16663
    61
lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
paulson@13871
    62
                                ~([j = 0] (mod p)); 
paulson@13871
    63
                                ~(QuadRes p a) |]  ==> 
paulson@13871
    64
                             ~([j = a * MultInv p j] (mod p))";
paulson@13871
    65
  apply auto
paulson@13871
    66
proof -;
nipkow@16663
    67
  assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and 
paulson@13871
    68
    "~([j = 0] (mod p))" and "~(QuadRes p a)";
paulson@13871
    69
  assume "[j = a * MultInv p j] (mod p)";
paulson@13871
    70
  then have "[j * j = (a * MultInv p j) * j] (mod p)";
paulson@13871
    71
    by (auto simp add: zcong_scalar)
paulson@13871
    72
  then have a:"[j * j = a * (MultInv p j * j)] (mod p)";
paulson@13871
    73
    by (auto simp add: zmult_ac)
paulson@13871
    74
  have "[j * j = a] (mod p)";
paulson@13871
    75
    proof -;
paulson@13871
    76
      from prems have b: "[MultInv p j * j = 1] (mod p)";
paulson@13871
    77
        by (simp add: MultInv_prop2a)
paulson@13871
    78
      from b a show ?thesis;
paulson@13871
    79
        by (auto simp add: zcong_zmult_prop2)
paulson@13871
    80
    qed;
paulson@13871
    81
  then have "[j^2 = a] (mod p)";
paulson@13871
    82
    apply(subgoal_tac "2 = Suc(Suc(0))");
paulson@13871
    83
    apply (erule ssubst)
paulson@13871
    84
    apply (auto simp only: power_Suc power_0)
paulson@13871
    85
    by auto
paulson@13871
    86
  with prems show False;
paulson@13871
    87
    by (simp add: QuadRes_def)
paulson@13871
    88
qed;
paulson@13871
    89
nipkow@16663
    90
lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
paulson@13871
    91
                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
paulson@13871
    92
                             card (MultInvPair a p j) = 2";
paulson@13871
    93
  apply (auto simp add: MultInvPair_def)
paulson@13871
    94
  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))");
paulson@13871
    95
  apply auto
paulson@13871
    96
  apply (simp only: StandardRes_prop2)
paulson@13871
    97
  apply (drule MultInvPair_distinct)
paulson@13871
    98
by auto
paulson@13871
    99
paulson@13871
   100
(****************************************************************)
paulson@13871
   101
(*                                                              *)
paulson@13871
   102
(* Properties of SetS                                           *)
paulson@13871
   103
(*                                                              *)
paulson@13871
   104
(****************************************************************)
paulson@13871
   105
paulson@13871
   106
lemma SetS_finite: "2 < p ==> finite (SetS a p)";
paulson@13871
   107
  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
paulson@13871
   108
paulson@13871
   109
lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X";
paulson@13871
   110
  by (auto simp add: SetS_def MultInvPair_def)
paulson@13871
   111
nipkow@16663
   112
lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
paulson@13871
   113
                        ~(QuadRes p a) |]  ==>
paulson@13871
   114
                        \<forall>X \<in> SetS a p. card X = 2";
paulson@13871
   115
  apply (auto simp add: SetS_def)
paulson@13871
   116
  apply (frule StandardRes_SRStar_prop1a)
paulson@13871
   117
  apply (rule MultInvPair_card_two, auto)
paulson@13871
   118
done
paulson@13871
   119
paulson@13871
   120
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))";
nipkow@15402
   121
  by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
paulson@13871
   122
paulson@13871
   123
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
paulson@13871
   124
    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S";
paulson@13871
   125
by (induct set: Finites, auto)
paulson@13871
   126
nipkow@16663
   127
lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> 
paulson@13871
   128
                  int(card(SetS a p)) = (p - 1) div 2";
paulson@13871
   129
proof -;
nipkow@16663
   130
  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)";
paulson@13871
   131
  then have "(p - 1) = 2 * int(card(SetS a p))";
paulson@13871
   132
  proof -;
paulson@13871
   133
    have "p - 1 = int(card(Union (SetS a p)))";
paulson@13871
   134
      by (auto simp add: prems MultInvPair_prop2 SRStar_card)
paulson@13871
   135
    also have "... = int (setsum card (SetS a p))";
paulson@13871
   136
      by (auto simp add: prems SetS_finite SetS_elems_finite
nipkow@15402
   137
                         MultInvPair_prop1c [of p a] card_Union_disjoint)
paulson@13871
   138
    also have "... = int(setsum (%x.2) (SetS a p))";
paulson@13871
   139
      apply (insert prems)
paulson@13871
   140
      apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
paulson@15047
   141
        card_setsum_aux simp del: setsum_constant)
paulson@13871
   142
    done
paulson@13871
   143
    also have "... = 2 * int(card( SetS a p))";
paulson@13871
   144
      by (auto simp add: prems SetS_finite setsum_const2)
paulson@13871
   145
    finally show ?thesis .;
paulson@13871
   146
  qed;
paulson@13871
   147
  from this show ?thesis;
paulson@13871
   148
    by auto
paulson@13871
   149
qed;
paulson@13871
   150
nipkow@16663
   151
lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
paulson@13871
   152
                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
nipkow@15392
   153
                          [\<Prod>x = a] (mod p)";
paulson@13871
   154
  apply (auto simp add: SetS_def MultInvPair_def)
paulson@13871
   155
  apply (frule StandardRes_SRStar_prop1a)
paulson@13871
   156
  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)");
paulson@13871
   157
  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
paulson@13871
   158
  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
paulson@13871
   159
    StandardRes_prop4);
paulson@13871
   160
  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)");
paulson@13871
   161
  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
paulson@13871
   162
                   b = "x * (a * MultInv p x)" and
paulson@13871
   163
                   c = "a * (x * MultInv p x)" in  zcong_trans, force);
paulson@13871
   164
  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
paulson@13871
   165
  apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
paulson@13871
   166
  apply (auto simp add: zmult_ac)
paulson@13871
   167
done
paulson@13871
   168
paulson@13871
   169
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1";
paulson@13871
   170
  by arith
paulson@13871
   171
paulson@13871
   172
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)";
paulson@13871
   173
  by auto
paulson@13871
   174
paulson@13871
   175
lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
paulson@13871
   176
    (d22set (p - 1))";
paulson@13871
   177
  apply (induct p rule: d22set.induct, auto)
paulson@13871
   178
  apply (simp add: SRStar_def d22set.simps, arith)
paulson@13871
   179
  apply (simp add: SRStar_def d22set.simps, clarify)
paulson@13871
   180
  apply (frule aux1)
paulson@13871
   181
  apply (frule aux2, auto)
paulson@13871
   182
  apply (simp_all add: SRStar_def)
paulson@13871
   183
  apply (simp add: d22set.simps)
paulson@13871
   184
  apply (frule d22set_le)
paulson@13871
   185
  apply (frule d22set_g_1, auto)
paulson@13871
   186
done
paulson@13871
   187
nipkow@16663
   188
lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
nipkow@15392
   189
                                 [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
nipkow@15392
   190
proof -
nipkow@16663
   191
  assume "zprime p" and "2 < p" and  "~([a = 0] (mod p))" and "~(QuadRes p a)"
nipkow@15392
   192
  then have "[\<Prod>(Union (SetS a p)) = 
nipkow@15392
   193
      setprod (setprod (%x. x)) (SetS a p)] (mod p)"
paulson@13871
   194
    by (auto simp add: SetS_finite SetS_elems_finite
nipkow@15392
   195
                       MultInvPair_prop1c setprod_Union_disjoint)
nipkow@15392
   196
  also have "[setprod (setprod (%x. x)) (SetS a p) = 
nipkow@15392
   197
      setprod (%x. a) (SetS a p)] (mod p)"
nipkow@15392
   198
    apply (rule setprod_same_function_zcong)
paulson@13871
   199
    by (auto simp add: prems SetS_setprod_prop SetS_finite)
nipkow@15392
   200
  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
nipkow@15392
   201
      a^(card (SetS a p))] (mod p)"
nipkow@15392
   202
    by (auto simp add: prems SetS_finite setprod_constant)
nipkow@15392
   203
  finally (zcong_trans) show ?thesis
paulson@13871
   204
    apply (rule zcong_trans)
nipkow@15392
   205
    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
nipkow@15392
   206
    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
paulson@13871
   207
    apply (auto simp add: prems SetS_card)
paulson@13871
   208
  done
nipkow@15392
   209
qed
paulson@13871
   210
nipkow@16663
   211
lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
nipkow@15392
   212
                                    \<Prod>(Union (SetS a p)) = zfact (p - 1)";
paulson@13871
   213
proof -;
nipkow@16663
   214
  assume "zprime p" and "2 < p" and "~([a = 0](mod p))";
nipkow@15392
   215
  then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
paulson@13871
   216
    by (auto simp add: MultInvPair_prop2)
nipkow@15392
   217
  also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
paulson@13871
   218
    by (auto simp add: prems SRStar_d22set_prop)
nipkow@15392
   219
  also have "... = zfact(p - 1)"
nipkow@15392
   220
  proof -
nipkow@15392
   221
     have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
paulson@13871
   222
      apply (insert prems, auto)
paulson@13871
   223
      apply (drule d22set_g_1)
paulson@13871
   224
      apply (auto simp add: d22set_fin)
paulson@13871
   225
     done
nipkow@15392
   226
     then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))";
paulson@13871
   227
       by auto
paulson@13871
   228
     then show ?thesis
paulson@13871
   229
       by (auto simp add: d22set_prod_zfact)
paulson@13871
   230
  qed;
nipkow@15392
   231
  finally show ?thesis .
paulson@13871
   232
qed;
paulson@13871
   233
nipkow@16663
   234
lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
paulson@13871
   235
                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)";
paulson@13871
   236
  apply (frule Union_SetS_setprod_prop1) 
paulson@13871
   237
  apply (auto simp add: Union_SetS_setprod_prop2)
paulson@13871
   238
done
paulson@13871
   239
paulson@13871
   240
(****************************************************************)
paulson@13871
   241
(*                                                              *)
paulson@13871
   242
(*  Prove the first part of Euler's Criterion:                  *)
paulson@13871
   243
(*    ~(QuadRes p x) |] ==>                                     *)
paulson@13871
   244
(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
paulson@13871
   245
(*                                                              *)
paulson@13871
   246
(****************************************************************)
paulson@13871
   247
nipkow@16663
   248
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
paulson@13871
   249
    ~(QuadRes p x) |] ==> 
paulson@13871
   250
      [x^(nat (((p) - 1) div 2)) = -1](mod p)";
paulson@13871
   251
  apply (frule zfact_prop, auto)
paulson@13871
   252
  apply (frule Wilson_Russ)
paulson@13871
   253
  apply (auto simp add: zcong_sym)
paulson@13871
   254
  apply (rule zcong_trans, auto)
paulson@13871
   255
done
paulson@13871
   256
paulson@13871
   257
(********************************************************************)
paulson@13871
   258
(*                                                                  *)
paulson@13871
   259
(* Prove another part of Euler Criterion:                           *)
paulson@13871
   260
(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
paulson@13871
   261
(*                                                                  *)
paulson@13871
   262
(********************************************************************)
paulson@13871
   263
paulson@13871
   264
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)";
paulson@13871
   265
proof -;
paulson@13871
   266
  assume "0 < p";
paulson@13871
   267
  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))";
paulson@13871
   268
    by (auto simp add: diff_add_assoc)
paulson@13871
   269
  also have "... = (a ^ 1) * a ^ (nat(p) - 1)";
paulson@13871
   270
    by (simp only: zpower_zadd_distrib)
paulson@13871
   271
  also have "... = a * a ^ (nat(p) - 1)";
paulson@13871
   272
    by auto
paulson@13871
   273
  finally show ?thesis .;
paulson@13871
   274
qed;
paulson@13871
   275
paulson@13871
   276
lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)";
paulson@13871
   277
proof -;
paulson@13871
   278
  assume "2 < p" and "p \<in> zOdd";
paulson@13871
   279
  then have "(p - 1):zEven";
paulson@13871
   280
    by (auto simp add: zEven_def zOdd_def)
paulson@13871
   281
  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)";
paulson@13871
   282
    by (auto simp add: even_div_2_prop2)
paulson@13871
   283
  then have "1 < (p - 1)"
paulson@13871
   284
    by auto
paulson@13871
   285
  then have " 1 < (2 * ((p - 1) div 2))";
paulson@13871
   286
    by (auto simp add: aux_1)
paulson@13871
   287
  then have "0 < (2 * ((p - 1) div 2)) div 2";
paulson@13871
   288
    by auto
paulson@13871
   289
  then show ?thesis by auto
paulson@13871
   290
qed;
paulson@13871
   291
nipkow@16663
   292
lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)";
paulson@13871
   293
  apply (frule zprime_zOdd_eq_grt_2)
paulson@13871
   294
  apply (frule aux_2, auto)
paulson@13871
   295
  apply (frule_tac a = a in aux_1, auto)
paulson@13871
   296
  apply (frule zcong_zmult_prop1, auto)
paulson@13871
   297
done
paulson@13871
   298
paulson@13871
   299
(****************************************************************)
paulson@13871
   300
(*                                                              *)
paulson@13871
   301
(* Prove the final part of Euler's Criterion:                   *)
paulson@13871
   302
(*           QuadRes p x |] ==>                                 *)
paulson@13871
   303
(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
paulson@13871
   304
(*                                                              *)
paulson@13871
   305
(****************************************************************)
paulson@13871
   306
paulson@13871
   307
lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)";
paulson@13871
   308
  apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> 
paulson@13871
   309
    ~([y ^ 2 = 0] (mod p))");
paulson@13871
   310
  apply (auto simp add: zcong_sym [of "y^2" x p] intro: zcong_trans)
paulson@13871
   311
  apply (auto simp add: zcong_eq_zdvd_prop intro: zpower_zdvd_prop1)
paulson@13871
   312
done
paulson@13871
   313
paulson@13871
   314
lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))";
paulson@13871
   315
  by (auto simp add: nat_mult_distrib)
paulson@13871
   316
nipkow@16663
   317
lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> 
paulson@13871
   318
                      [x^(nat (((p) - 1) div 2)) = 1](mod p)";
paulson@13871
   319
  apply (subgoal_tac "p \<in> zOdd")
paulson@13871
   320
  apply (auto simp add: QuadRes_def)
paulson@13871
   321
  apply (frule aux__1, auto)
paulson@13871
   322
  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower);
paulson@13871
   323
  apply (auto simp add: zpower_zpower)
paulson@13871
   324
  apply (rule zcong_trans)
paulson@13871
   325
  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"]);
paulson@13871
   326
  apply (simp add: aux__2)
paulson@13871
   327
  apply (frule odd_minus_one_even)
paulson@13871
   328
  apply (frule even_div_2_prop2)
paulson@13871
   329
  apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
paulson@13871
   330
done
paulson@13871
   331
paulson@13871
   332
(********************************************************************)
paulson@13871
   333
(*                                                                  *)
paulson@13871
   334
(* Finally show Euler's Criterion                                   *)
paulson@13871
   335
(*                                                                  *)
paulson@13871
   336
(********************************************************************)
paulson@13871
   337
nipkow@16663
   338
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
paulson@13871
   339
    a^(nat (((p) - 1) div 2))] (mod p)";
paulson@13871
   340
  apply (auto simp add: Legendre_def Euler_part2)
paulson@13871
   341
  apply (frule Euler_part3, auto simp add: zcong_sym)
paulson@13871
   342
  apply (frule Euler_part1, auto simp add: zcong_sym)
paulson@13871
   343
done
paulson@13871
   344
paulson@14485
   345
end