author  paulson <lp15@cam.ac.uk> 
Fri, 13 Nov 2015 12:27:13 +0000  
changeset 61649  268d88ec9087 
parent 61382  efac889fccbc 
child 61952  546958347e05 
permissions  rwrr 
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 

61382  5 
section \<open>Euler's criterion\<close> 
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 

61382  18 
subsection \<open>Property for MultInvPair\<close> 
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 numberrepresentationspecific 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 

61382  92 
subsection \<open>Properties of SetS\<close> 
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 

61382  226 
text \<open>\medskip Prove the first part of Euler's Criterion:\<close> 
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 numberrepresentationspecific 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 

61382  233 
text \<open>\medskip Prove another part of Euler Criterion:\<close> 
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) 
61382  254 
with \<open>2 < p\<close> 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 

61382  271 
text \<open>\medskip Prove the final part of Euler's Criterion:\<close> 
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 numberrepresentationspecific 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) 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61382
diff
changeset

287 
apply (auto simp add: power_mult [symmetric]) 
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 numberrepresentationspecific 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 

61382  294 
text \<open>\medskip Finally show Euler's Criterion:\<close> 
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 