src/HOL/Old_Number_Theory/Euler.thy
author wenzelm
Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409 b7cfe12acf2e
parent 58889 5b7a9633cfa8
child 61382 efac889fccbc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
     1
(*  Title:      HOL/Old_Number_Theory/Euler.thy
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     2
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     3
*)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     4
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 57514
diff changeset
     5
section {* Euler's criterion *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
     6
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
     7
theory Euler
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
     8
imports Residues EvenOdd
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
     9
begin
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    10
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
    11
definition MultInvPair :: "int => int => int => int set"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
    12
  where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    13
38159
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
    14
definition SetS :: "int => int => int set set"
e9b4835a54ee modernized specifications;
wenzelm
parents: 35544
diff changeset
    15
  where "SetS a p = MultInvPair a p ` SRStar p"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    16
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    17
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    18
subsection {* Property for MultInvPair *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    19
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    20
lemma MultInvPair_prop1a:
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    21
  "[| zprime p; 2 < p; ~([a = 0](mod p));
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    22
      X \<in> (SetS a p); Y \<in> (SetS a p);
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    23
      ~((X \<inter> Y) = {}) |] ==> X = Y"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    24
  apply (auto simp add: SetS_def)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    25
  apply (drule StandardRes_SRStar_prop1a)+ defer 1
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    26
  apply (drule StandardRes_SRStar_prop1a)+
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    27
  apply (auto simp add: MultInvPair_def StandardRes_prop2 zcong_sym)
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    28
  apply (drule notE, rule MultInv_zcong_prop1, auto)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    29
  apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    30
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    31
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    32
  apply (drule MultInv_zcong_prop1, auto)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    33
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    34
  apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    35
  apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[]
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    36
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    37
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    38
lemma MultInvPair_prop1b:
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    39
  "[| zprime p; 2 < p; ~([a = 0](mod p));
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    40
      X \<in> (SetS a p); Y \<in> (SetS a p);
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    41
      X \<noteq> Y |] ==> X \<inter> Y = {}"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    42
  apply (rule notnotD)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    43
  apply (rule notI)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    44
  apply (drule MultInvPair_prop1a, auto)
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    45
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    46
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
    47
lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    48
    \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    49
  by (auto simp add: MultInvPair_prop1b)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    50
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
    51
lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    52
                          Union ( SetS a p) = SRStar p"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    53
  apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    54
    SRStar_mult_prop2)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    55
  apply (frule StandardRes_SRStar_prop3)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    56
  apply (rule bexI, auto)
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    57
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    58
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    59
lemma MultInvPair_distinct:
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    60
  assumes "zprime p" and "2 < p" and
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    61
    "~([a = 0] (mod p))" and
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    62
    "~([j = 0] (mod p))" and
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    63
    "~(QuadRes p a)"
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    64
  shows "~([j = a * MultInv p j] (mod p))"
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    65
proof
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    66
  assume "[j = a * MultInv p j] (mod p)"
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    67
  then have "[j * j = (a * MultInv p j) * j] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    68
    by (auto simp add: zcong_scalar)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    69
  then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
    70
    by (auto simp add: ac_simps)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    71
  have "[j * j = a] (mod p)"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    72
  proof -
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    73
    from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    74
      by (simp add: MultInv_prop2a)
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    75
    from this and a show ?thesis
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    76
      by (auto simp add: zcong_zmult_prop2)
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    77
  qed
53077
a1b3784f8129 more symbols;
wenzelm
parents: 45480
diff changeset
    78
  then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square)
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
    79
  with assms show False by (simp add: QuadRes_def)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    80
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    81
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
    82
lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    83
                                ~(QuadRes p a); ~([j = 0] (mod p)) |]  ==> 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    84
                             card (MultInvPair a p j) = 2"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    85
  apply (auto simp add: MultInvPair_def)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    86
  apply (subgoal_tac "~ (StandardRes p j = StandardRes p (a * MultInv p j))")
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    87
  apply auto
45480
a39bb6d42ace remove unnecessary number-representation-specific rules from metis calls;
huffman
parents: 44766
diff changeset
    88
  apply (metis MultInvPair_distinct StandardRes_def aux)
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
    89
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    90
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    91
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
    92
subsection {* Properties of SetS *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    93
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    94
lemma SetS_finite: "2 < p ==> finite (SetS a p)"
40786
0a54cfc9add3 gave more standard finite set rules simp and intro attribute
nipkow
parents: 38159
diff changeset
    95
  by (auto simp add: SetS_def SRStar_finite [of p])
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    96
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
    97
lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    98
  by (auto simp add: SetS_def MultInvPair_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
    99
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   100
lemma SetS_elems_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   101
                        ~(QuadRes p a) |]  ==>
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   102
                        \<forall>X \<in> SetS a p. card X = 2"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   103
  apply (auto simp add: SetS_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   104
  apply (frule StandardRes_SRStar_prop1a)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   105
  apply (rule MultInvPair_card_two, auto)
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   106
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   107
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   108
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   109
  by (auto simp add: SetS_finite SetS_elems_finite)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   110
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   111
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set); 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   112
    \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
22274
ce1459004c8d Adapted to changes in Finite_Set theory.
berghofe
parents: 21404
diff changeset
   113
  by (induct set: finite) auto
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   114
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   115
lemma SetS_card:
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   116
  assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   117
  shows "int(card(SetS a p)) = (p - 1) div 2"
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   118
proof -
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   119
  have "(p - 1) = 2 * int(card(SetS a p))"
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   120
  proof -
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   121
    have "p - 1 = int(card(Union (SetS a p)))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   122
      by (auto simp add: assms MultInvPair_prop2 SRStar_card)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   123
    also have "... = int (setsum card (SetS a p))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   124
      by (auto simp add: assms SetS_finite SetS_elems_finite
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   125
        MultInvPair_prop1c [of p a] card_Union_disjoint)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   126
    also have "... = int(setsum (%x.2) (SetS a p))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   127
      using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
15047
fa62de5862b9 redefining sumr to be a translation to setsum
paulson
parents: 14981
diff changeset
   128
        card_setsum_aux simp del: setsum_constant)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   129
    also have "... = 2 * int(card( SetS a p))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   130
      by (auto simp add: assms SetS_finite setsum_const2)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   131
    finally show ?thesis .
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   132
  qed
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   133
  then show ?thesis by auto
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   134
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   135
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   136
lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   137
                              ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   138
                          [\<Prod>x = a] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   139
  apply (auto simp add: SetS_def MultInvPair_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   140
  apply (frule StandardRes_SRStar_prop1a)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 57418
diff changeset
   141
  apply hypsubst_thin
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   142
  apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   143
  apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   144
  apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   145
    StandardRes_prop4)
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   146
  apply (subgoal_tac "[x * (a * MultInv p x) = a * (x * MultInv p x)] (mod p)")
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   147
  apply (drule_tac a = "StandardRes p x * StandardRes p (a * MultInv p x)" and
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   148
                   b = "x * (a * MultInv p x)" and
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   149
                   c = "a * (x * MultInv p x)" in  zcong_trans, force)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   150
  apply (frule_tac p = p and x = x in MultInv_prop2, auto)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   151
apply (metis StandardRes_SRStar_prop3 mult_1_right mult.commute zcong_sym zcong_zmult_prop1)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   152
  apply (auto simp add: ac_simps)
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   153
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   154
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   155
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   156
  by arith
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   157
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   158
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   159
  by auto
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   160
35544
342a448ae141 fix fragile proof using old induction rule (cf. bdf8ad377877)
krauss
parents: 32479
diff changeset
   161
lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"
342a448ae141 fix fragile proof using old induction rule (cf. bdf8ad377877)
krauss
parents: 32479
diff changeset
   162
using d22set.induct by blast
342a448ae141 fix fragile proof using old induction rule (cf. bdf8ad377877)
krauss
parents: 32479
diff changeset
   163
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   164
lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
35544
342a448ae141 fix fragile proof using old induction rule (cf. bdf8ad377877)
krauss
parents: 32479
diff changeset
   165
  apply (induct p rule: d22set_induct_old)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   166
  apply auto
16733
236dfafbeb63 linear arithmetic now takes "&" in assumptions apart.
nipkow
parents: 16663
diff changeset
   167
  apply (simp add: SRStar_def d22set.simps)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   168
  apply (simp add: SRStar_def d22set.simps, clarify)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   169
  apply (frule aux1)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   170
  apply (frule aux2, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   171
  apply (simp_all add: SRStar_def)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   172
  apply (simp add: d22set.simps)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   173
  apply (frule d22set_le)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   174
  apply (frule d22set_g_1, auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   175
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   176
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   177
lemma Union_SetS_setprod_prop1:
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   178
  assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   179
    "~(QuadRes p a)"
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   180
  shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   181
proof -
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   182
  from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   183
    by (auto simp add: SetS_finite SetS_elems_finite
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 53077
diff changeset
   184
      MultInvPair_prop1c setprod.Union_disjoint)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   185
  also have "[setprod (setprod (%x. x)) (SetS a p) = 
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   186
      setprod (%x. a) (SetS a p)] (mod p)"
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   187
    by (rule setprod_same_function_zcong)
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   188
      (auto simp add: assms SetS_setprod_prop SetS_finite)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   189
  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   190
      a^(card (SetS a p))] (mod p)"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   191
    by (auto simp add: assms SetS_finite setprod_constant)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   192
  finally (zcong_trans) show ?thesis
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   193
    apply (rule zcong_trans)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   194
    apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   195
    apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   196
    apply (auto simp add: assms SetS_card)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   197
    done
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   198
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   199
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   200
lemma Union_SetS_setprod_prop2:
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   201
  assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   202
  shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   203
proof -
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   204
  from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   205
    by (auto simp add: MultInvPair_prop2)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   206
  also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
41541
1fa4725c4656 eliminated global prems;
wenzelm
parents: 40786
diff changeset
   207
    by (auto simp add: assms SRStar_d22set_prop)
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   208
  also have "... = zfact(p - 1)"
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   209
  proof -
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   210
    have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
25760
6d947d7a5ae8 new metis proofs
paulson
parents: 25675
diff changeset
   211
      by (metis d22set_fin d22set_g_1 linorder_neq_iff)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   212
    then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))"
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   213
      by auto
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   214
    then show ?thesis
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   215
      by (auto simp add: d22set_prod_zfact)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   216
  qed
15392
290bc97038c7 First step in reorganizing Finite_Set
nipkow
parents: 15047
diff changeset
   217
  finally show ?thesis .
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   218
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   219
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   220
lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   221
                   [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   222
  apply (frule Union_SetS_setprod_prop1) 
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   223
  apply (auto simp add: Union_SetS_setprod_prop2)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   224
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   225
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   226
text {* \medskip Prove the first part of Euler's Criterion: *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   227
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   228
lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   229
    ~(QuadRes p x) |] ==> 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   230
      [x^(nat (((p) - 1) div 2)) = -1](mod p)"
45480
a39bb6d42ace remove unnecessary number-representation-specific rules from metis calls;
huffman
parents: 44766
diff changeset
   231
  by (metis Wilson_Russ zcong_sym zcong_trans zfact_prop)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   232
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   233
text {* \medskip Prove another part of Euler Criterion: *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   234
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   235
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   236
proof -
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   237
  assume "0 < p"
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   238
  then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   239
    by (auto simp add: diff_add_assoc)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   240
  also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 41541
diff changeset
   241
    by (simp only: power_add)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   242
  also have "... = a * a ^ (nat(p) - 1)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   243
    by auto
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   244
  finally show ?thesis .
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   245
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   246
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   247
lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)"
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   248
proof -
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   249
  assume "2 < p" and "p \<in> zOdd"
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   250
  then have "(p - 1):zEven"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   251
    by (auto simp add: zEven_def zOdd_def)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   252
  then have aux_1: "2 * ((p - 1) div 2) = (p - 1)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   253
    by (auto simp add: even_div_2_prop2)
23373
ead82c82da9e tuned proofs: avoid implicit prems;
wenzelm
parents: 22274
diff changeset
   254
  with `2 < p` have "1 < (p - 1)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   255
    by auto
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   256
  then have " 1 < (2 * ((p - 1) div 2))"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   257
    by (auto simp add: aux_1)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   258
  then have "0 < (2 * ((p - 1) div 2)) div 2"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   259
    by auto
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   260
  then show ?thesis by auto
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   261
qed
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   262
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   263
lemma Euler_part2:
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   264
    "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   265
  apply (frule zprime_zOdd_eq_grt_2)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   266
  apply (frule aux_2, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   267
  apply (frule_tac a = a in aux_1, auto)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   268
  apply (frule zcong_zmult_prop1, auto)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   269
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   270
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   271
text {* \medskip Prove the final part of Euler's Criterion: *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   272
53077
a1b3784f8129 more symbols;
wenzelm
parents: 45480
diff changeset
   273
lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)"
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 26510
diff changeset
   274
  by (metis dvdI power2_eq_square zcong_sym zcong_trans zcong_zero_equiv_div dvd_trans)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   275
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   276
lemma aux__2: "2 * nat((p - 1) div 2) =  nat (2 * ((p - 1) div 2))"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   277
  by (auto simp add: nat_mult_distrib)
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   278
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   279
lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> 
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   280
                      [x^(nat (((p) - 1) div 2)) = 1](mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   281
  apply (subgoal_tac "p \<in> zOdd")
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   282
  apply (auto simp add: QuadRes_def)
25675
2488fc510178 tidied some messy proofs
paulson
parents: 23373
diff changeset
   283
   prefer 2 
45480
a39bb6d42ace remove unnecessary number-representation-specific rules from metis calls;
huffman
parents: 44766
diff changeset
   284
   apply (metis zprime_zOdd_eq_grt_2)
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   285
  apply (frule aux__1, auto)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   286
  apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
25675
2488fc510178 tidied some messy proofs
paulson
parents: 23373
diff changeset
   287
  apply (auto simp add: zpower_zpower) 
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   288
  apply (rule zcong_trans)
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   289
  apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
45480
a39bb6d42ace remove unnecessary number-representation-specific rules from metis calls;
huffman
parents: 44766
diff changeset
   290
  apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   291
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   292
19670
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   293
2e4a143c73c5 prefer 'definition' over low-level defs;
wenzelm
parents: 18369
diff changeset
   294
text {* \medskip Finally show Euler's Criterion: *}
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   295
16663
13e9c402308b prime is a predicate now.
nipkow
parents: 16417
diff changeset
   296
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
16974
0f8ebabf3163 more zcong_sym;
wenzelm
parents: 16733
diff changeset
   297
    a^(nat (((p) - 1) div 2))] (mod p)"
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   298
  apply (auto simp add: Legendre_def Euler_part2)
20369
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
   299
  apply (frule Euler_part3, auto simp add: zcong_sym)[]
7e03c3ed1a18 tuned proofs;
wenzelm
parents: 19670
diff changeset
   300
  apply (frule Euler_part1, auto simp add: zcong_sym)[]
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   301
  done
13871
26e5f5e624f6 Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff changeset
   302
18369
694ea14ab4f2 tuned sources and proofs
wenzelm
parents: 16974
diff changeset
   303
end