author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58889 | 5b7a9633cfa8 |
child 61382 | efac889fccbc |
permissions | -rw-r--r-- |
38159 | 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 | 5 |
section {* Euler's criterion *} |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
6 |
|
38159 | 7 |
theory Euler |
8 |
imports Residues EvenOdd |
|
9 |
begin |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
10 |
|
38159 | 11 |
definition MultInvPair :: "int => int => int => int set" |
12 |
where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}" |
|
19670 | 13 |
|
38159 | 14 |
definition SetS :: "int => int => int set set" |
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 | 17 |
|
18 |
subsection {* Property for MultInvPair *} |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
19 |
|
19670 | 20 |
lemma MultInvPair_prop1a: |
21 |
"[| zprime p; 2 < p; ~([a = 0](mod p)); |
|
22 |
X \<in> (SetS a p); Y \<in> (SetS a p); |
|
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 | 25 |
apply (drule StandardRes_SRStar_prop1a)+ defer 1 |
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 | 28 |
apply (drule notE, rule MultInv_zcong_prop1, auto)[] |
29 |
apply (drule notE, rule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
30 |
apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
31 |
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] |
|
32 |
apply (drule MultInv_zcong_prop1, auto)[] |
|
33 |
apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
34 |
apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)[] |
|
35 |
apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)[] |
|
19670 | 36 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
37 |
|
19670 | 38 |
lemma MultInvPair_prop1b: |
39 |
"[| zprime p; 2 < p; ~([a = 0](mod p)); |
|
40 |
X \<in> (SetS a p); Y \<in> (SetS a p); |
|
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 | 45 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
46 |
|
16663 | 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 | 51 |
lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==> |
16974 | 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 | 57 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
58 |
|
41541 | 59 |
lemma MultInvPair_distinct: |
60 |
assumes "zprime p" and "2 < p" and |
|
61 |
"~([a = 0] (mod p))" and |
|
62 |
"~([j = 0] (mod p))" and |
|
63 |
"~(QuadRes p a)" |
|
64 |
shows "~([j = a * MultInv p j] (mod p))" |
|
20369 | 65 |
proof |
16974 | 66 |
assume "[j = a * MultInv p j] (mod p)" |
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 | 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 | 71 |
have "[j * j = a] (mod p)" |
41541 | 72 |
proof - |
73 |
from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)" |
|
74 |
by (simp add: MultInv_prop2a) |
|
75 |
from this and a show ?thesis |
|
76 |
by (auto simp add: zcong_zmult_prop2) |
|
77 |
qed |
|
53077 | 78 |
then have "[j\<^sup>2 = a] (mod p)" by (simp add: power2_eq_square) |
41541 | 79 |
with assms show False by (simp add: QuadRes_def) |
16974 | 80 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
81 |
|
16663 | 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 | 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 | 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 | 89 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
90 |
|
19670 | 91 |
|
92 |
subsection {* Properties of SetS *} |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
93 |
|
16974 | 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 | 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 | 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 | 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 | 106 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
107 |
|
16974 | 108 |
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))" |
41541 | 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 | 112 |
\<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S" |
22274 | 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 | 115 |
lemma SetS_card: |
116 |
assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)" |
|
117 |
shows "int(card(SetS a p)) = (p - 1) div 2" |
|
16974 | 118 |
proof - |
41541 | 119 |
have "(p - 1) = 2 * int(card(SetS a p))" |
16974 | 120 |
proof - |
121 |
have "p - 1 = int(card(Union (SetS a p)))" |
|
41541 | 122 |
by (auto simp add: assms MultInvPair_prop2 SRStar_card) |
16974 | 123 |
also have "... = int (setsum card (SetS a p))" |
41541 | 124 |
by (auto simp add: assms SetS_finite SetS_elems_finite |
125 |
MultInvPair_prop1c [of p a] card_Union_disjoint) |
|
16974 | 126 |
also have "... = int(setsum (%x.2) (SetS a p))" |
41541 | 127 |
using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite |
15047 | 128 |
card_setsum_aux simp del: setsum_constant) |
16974 | 129 |
also have "... = 2 * int(card( SetS a p))" |
41541 | 130 |
by (auto simp add: assms SetS_finite setsum_const2) |
16974 | 131 |
finally show ?thesis . |
132 |
qed |
|
41541 | 133 |
then show ?thesis by auto |
16974 | 134 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
135 |
|
16663 | 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 | 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 | 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 | 145 |
StandardRes_prop4) |
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 | 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 | 153 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
154 |
|
16974 | 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 | 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 | 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 | 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 | 175 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
176 |
|
41541 | 177 |
lemma Union_SetS_setprod_prop1: |
178 |
assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and |
|
179 |
"~(QuadRes p a)" |
|
180 |
shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)" |
|
15392 | 181 |
proof - |
41541 | 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 | 184 |
MultInvPair_prop1c setprod.Union_disjoint) |
15392 | 185 |
also have "[setprod (setprod (%x. x)) (SetS a p) = |
186 |
setprod (%x. a) (SetS a p)] (mod p)" |
|
18369 | 187 |
by (rule setprod_same_function_zcong) |
41541 | 188 |
(auto simp add: assms SetS_setprod_prop SetS_finite) |
15392 | 189 |
also (zcong_trans) have "[setprod (%x. a) (SetS a p) = |
190 |
a^(card (SetS a p))] (mod p)" |
|
41541 | 191 |
by (auto simp add: assms SetS_finite setprod_constant) |
15392 | 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 | 194 |
apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto) |
195 |
apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force) |
|
41541 | 196 |
apply (auto simp add: assms SetS_card) |
18369 | 197 |
done |
15392 | 198 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
199 |
|
41541 | 200 |
lemma Union_SetS_setprod_prop2: |
201 |
assumes "zprime p" and "2 < p" and "~([a = 0](mod p))" |
|
202 |
shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)" |
|
16974 | 203 |
proof - |
41541 | 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 | 206 |
also have "... = \<Prod>({1} \<union> (d22set (p - 1)))" |
41541 | 207 |
by (auto simp add: assms SRStar_d22set_prop) |
15392 | 208 |
also have "... = zfact(p - 1)" |
209 |
proof - |
|
18369 | 210 |
have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))" |
25760 | 211 |
by (metis d22set_fin d22set_g_1 linorder_neq_iff) |
18369 | 212 |
then have "\<Prod>({1} \<union> (d22set (p - 1))) = \<Prod>(d22set (p - 1))" |
213 |
by auto |
|
214 |
then show ?thesis |
|
215 |
by (auto simp add: d22set_prod_zfact) |
|
16974 | 216 |
qed |
15392 | 217 |
finally show ?thesis . |
16974 | 218 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
|
16663 | 220 |
lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==> |
16974 | 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 | 224 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
225 |
|
19670 | 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 | 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 | 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 | 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 | 235 |
lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)" |
236 |
proof - |
|
237 |
assume "0 < p" |
|
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 | 240 |
also have "... = (a ^ 1) * a ^ (nat(p) - 1)" |
44766 | 241 |
by (simp only: power_add) |
16974 | 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 | 244 |
finally show ?thesis . |
245 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
246 |
|
16974 | 247 |
lemma aux_2: "[| (2::int) < p; p \<in> zOdd |] ==> 0 < ((p - 1) div 2)" |
248 |
proof - |
|
249 |
assume "2 < p" and "p \<in> zOdd" |
|
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 | 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 | 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 | 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 | 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 | 261 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
262 |
|
19670 | 263 |
lemma Euler_part2: |
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 | 269 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
270 |
|
19670 | 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 | 273 |
lemma aux__1: "[| ~([x = 0] (mod p)); [y\<^sup>2 = x] (mod p)|] ==> ~(p dvd y)" |
30042 | 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 | 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 | 279 |
lemma Euler_part3: "[| 2 < p; zprime p; ~([x = 0](mod p)); QuadRes p x |] ==> |
16974 | 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 | 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 | 286 |
apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower) |
25675 | 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 | 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 | 291 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
292 |
|
19670 | 293 |
|
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 | 296 |
theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) = |
16974 | 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 | 299 |
apply (frule Euler_part3, auto simp add: zcong_sym)[] |
300 |
apply (frule Euler_part1, auto simp add: zcong_sym)[] |
|
18369 | 301 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
302 |
|
18369 | 303 |
end |