author  wenzelm 
Sat, 10 Oct 2015 16:26:23 +0200  
changeset 61382  efac889fccbc 
parent 58889  5b7a9633cfa8 
child 63566  e5abbdee461a 
permissions  rwrr 
38159  1 
(* Title: HOL/Old_Number_Theory/Gauss.thy 
2 
Authors: Jeremy Avigad, David Gray, and Adam Kramer 

13871
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>Gauss' Lemma\<close> 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

6 

27556  7 
theory Gauss 
8 
imports Euler 

9 
begin 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

10 

26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

11 
locale GAUSS = 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

12 
fixes p :: "int" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

13 
fixes a :: "int" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

14 

16663  15 
assumes p_prime: "zprime p" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

16 
assumes p_g_2: "2 < p" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

17 
assumes p_a_relprime: "~[a = 0](mod p)" 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

18 
assumes a_nonzero: "0 < a" 
21233  19 
begin 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

20 

38159  21 
definition "A = {(x::int). 0 < x & x \<le> ((p  1) div 2)}" 
22 
definition "B = (%x. x * a) ` A" 

23 
definition "C = StandardRes p ` B" 

24 
definition "D = C \<inter> {x. x \<le> ((p  1) div 2)}" 

25 
definition "E = C \<inter> {x. ((p  1) div 2) < x}" 

26 
definition "F = (%x. (p  x)) ` E" 

21233  27 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

28 

61382  29 
subsection \<open>Basic properties of p\<close> 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

30 

21233  31 
lemma p_odd: "p \<in> zOdd" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

32 
by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

33 

21233  34 
lemma p_g_0: "0 < p" 
18369  35 
using p_g_2 by auto 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

36 

21233  37 
lemma int_nat: "int (nat ((p  1) div 2)) = (p  1) div 2" 
26289  38 
using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

39 

21233  40 
lemma p_minus_one_l: "(p  1) div 2 < p" 
18369  41 
proof  
42 
have "(p  1) div 2 \<le> (p  1) div 1" 

43 
by (rule zdiv_mono2) (auto simp add: p_g_0) 

44 
also have "\<dots> = p  1" by simp 

45 
finally show ?thesis by simp 

46 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

47 

21233  48 
lemma p_eq: "p = (2 * (p  1) div 2) + 1" 
30034  49 
using div_mult_self1_is_id [of 2 "p  1"] by auto 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

50 

21233  51 

21288  52 
lemma (in ) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x  1) div 2 = 2 * ((x  1) div 2)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

53 
apply (frule odd_minus_one_even) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

54 
apply (simp add: zEven_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

55 
apply (subgoal_tac "2 \<noteq> 0") 
30034  56 
apply (frule_tac b = "2 :: int" and a = "x  1" in div_mult_self1_is_id) 
18369  57 
apply (auto simp add: even_div_2_prop2) 
58 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

59 

21233  60 

61 
lemma p_eq2: "p = (2 * ((p  1) div 2)) + 1" 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

62 
apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto) 
18369  63 
apply (frule zodd_imp_zdiv_eq, auto) 
64 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

65 

21233  66 

61382  67 
subsection \<open>Basic Properties of the Gauss Sets\<close> 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

68 

21233  69 
lemma finite_A: "finite (A)" 
46756
faf62905cd53
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents:
44766
diff
changeset

70 
by (auto simp add: A_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

71 

21233  72 
lemma finite_B: "finite (B)" 
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset

73 
by (auto simp add: B_def finite_A) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

74 

21233  75 
lemma finite_C: "finite (C)" 
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset

76 
by (auto simp add: C_def finite_B) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

77 

21233  78 
lemma finite_D: "finite (D)" 
41541  79 
by (auto simp add: D_def finite_C) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

80 

21233  81 
lemma finite_E: "finite (E)" 
41541  82 
by (auto simp add: E_def finite_C) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

83 

21233  84 
lemma finite_F: "finite (F)" 
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset

85 
by (auto simp add: F_def finite_E) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

86 

21233  87 
lemma C_eq: "C = D \<union> E" 
40786
0a54cfc9add3
gave more standard finite set rules simp and intro attribute
nipkow
parents:
38159
diff
changeset

88 
by (auto simp add: C_def D_def E_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

89 

21233  90 
lemma A_card_eq: "card A = nat ((p  1) div 2)" 
18369  91 
apply (auto simp add: A_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

92 
apply (insert int_nat) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

93 
apply (erule subst) 
18369  94 
apply (auto simp add: card_bdd_int_set_l_le) 
95 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

96 

21233  97 
lemma inj_on_xa_A: "inj_on (%x. x * a) A" 
18369  98 
using a_nonzero by (simp add: A_def inj_on_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

99 

21233  100 
lemma A_res: "ResSet p A" 
18369  101 
apply (auto simp add: A_def ResSet_def) 
102 
apply (rule_tac m = p in zcong_less_eq) 

103 
apply (insert p_g_2, auto) 

104 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

105 

21233  106 
lemma B_res: "ResSet p B" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

107 
apply (insert p_g_2 p_a_relprime p_minus_one_l) 
18369  108 
apply (auto simp add: B_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

109 
apply (rule ResSet_image) 
18369  110 
apply (auto simp add: A_res) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

111 
apply (auto simp add: A_def) 
18369  112 
proof  
113 
fix x fix y 

114 
assume a: "[x * a = y * a] (mod p)" 

115 
assume b: "0 < x" 

116 
assume c: "x \<le> (p  1) div 2" 

117 
assume d: "0 < y" 

118 
assume e: "y \<le> (p  1) div 2" 

119 
from a p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 

120 
have "[x = y](mod p)" 

121 
by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 

122 
with zcong_less_eq [of x y p] p_minus_one_l 

123 
order_le_less_trans [of x "(p  1) div 2" p] 

124 
order_le_less_trans [of y "(p  1) div 2" p] show "x = y" 

41541  125 
by (simp add: b c d e p_minus_one_l p_g_0) 
18369  126 
qed 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

127 

21233  128 
lemma SR_B_inj: "inj_on (StandardRes p) B" 
41541  129 
apply (auto simp add: B_def StandardRes_def inj_on_def A_def) 
18369  130 
proof  
131 
fix x fix y 

132 
assume a: "x * a mod p = y * a mod p" 

133 
assume b: "0 < x" 

134 
assume c: "x \<le> (p  1) div 2" 

135 
assume d: "0 < y" 

136 
assume e: "y \<le> (p  1) div 2" 

137 
assume f: "x \<noteq> y" 

138 
from a have "[x * a = y * a](mod p)" 

139 
by (simp add: zcong_zmod_eq p_g_0) 

140 
with p_a_relprime p_prime a_nonzero zcong_cancel [of p a x y] 

141 
have "[x = y](mod p)" 

142 
by (simp add: zprime_imp_zrelprime zcong_def p_g_0 order_le_less) 

143 
with zcong_less_eq [of x y p] p_minus_one_l 

144 
order_le_less_trans [of x "(p  1) div 2" p] 

145 
order_le_less_trans [of y "(p  1) div 2" p] have "x = y" 

41541  146 
by (simp add: b c d e p_minus_one_l p_g_0) 
18369  147 
then have False 
148 
by (simp add: f) 

149 
then show "a = 0" 

150 
by simp 

151 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

152 

21233  153 
lemma inj_on_pminusx_E: "inj_on (%x. p  x) E" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

154 
apply (auto simp add: E_def C_def B_def A_def) 
18369  155 
apply (rule_tac g = "%x. 1 * (x  p)" in inj_on_inverseI) 
156 
apply auto 

157 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

158 

21233  159 
lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

160 
apply (auto simp add: A_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

161 
apply (frule_tac m = p in zcong_not_zero) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

162 
apply (insert p_minus_one_l) 
18369  163 
apply auto 
164 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

165 

21233  166 
lemma A_greater_zero: "x \<in> A ==> 0 < x" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

167 
by (auto simp add: A_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

168 

21233  169 
lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

170 
apply (auto simp add: B_def) 
18369  171 
apply (frule A_ncong_p) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

172 
apply (insert p_a_relprime p_prime a_nonzero) 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
57418
diff
changeset

173 
apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra) 
18369  174 
apply (auto simp add: A_greater_zero) 
175 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

176 

21233  177 
lemma B_greater_zero: "x \<in> B ==> 0 < x" 
56544  178 
using a_nonzero by (auto simp add: B_def A_greater_zero) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

179 

21233  180 
lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

181 
apply (auto simp add: C_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

182 
apply (frule B_ncong_p) 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
57418
diff
changeset

183 
apply (subgoal_tac "[xa = StandardRes p xa](mod p)") 
18369  184 
defer apply (simp add: StandardRes_prop1) 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
57418
diff
changeset

185 
apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans) 
18369  186 
apply auto 
187 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

188 

21233  189 
lemma C_greater_zero: "y \<in> C ==> 0 < y" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

190 
apply (auto simp add: C_def) 
18369  191 
proof  
192 
fix x 

193 
assume a: "x \<in> B" 

194 
from p_g_0 have "0 \<le> StandardRes p x" 

195 
by (simp add: StandardRes_lbound) 

196 
moreover have "~[x = 0] (mod p)" 

197 
by (simp add: a B_ncong_p) 

198 
then have "StandardRes p x \<noteq> 0" 

199 
by (simp add: StandardRes_prop3) 

200 
ultimately show "0 < StandardRes p x" 

201 
by (simp add: order_le_less) 

202 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

203 

21233  204 
lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

205 
by (auto simp add: D_def C_ncong_p) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

206 

21233  207 
lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

208 
by (auto simp add: E_def C_ncong_p) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

209 

21233  210 
lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)" 
18369  211 
apply (auto simp add: F_def) 
212 
proof  

213 
fix x assume a: "x \<in> E" assume b: "[p  x = 0] (mod p)" 

214 
from E_ncong_p have "~[x = 0] (mod p)" 

215 
by (simp add: a) 

216 
moreover from a have "0 < x" 

217 
by (simp add: a E_def C_greater_zero) 

218 
moreover from a have "x < p" 

219 
by (auto simp add: E_def C_def p_g_0 StandardRes_ubound) 

220 
ultimately have "~[p  x = 0] (mod p)" 

221 
by (simp add: zcong_not_zero) 

222 
from this show False by (simp add: b) 

223 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

224 

21233  225 
lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p  1) div 2)}" 
18369  226 
apply (auto simp add: F_def E_def) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

227 
apply (insert p_g_0) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

228 
apply (frule_tac x = xa in StandardRes_ubound) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

229 
apply (frule_tac x = x in StandardRes_ubound) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

230 
apply (subgoal_tac "xa = StandardRes p xa") 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

231 
apply (auto simp add: C_def StandardRes_prop2 StandardRes_prop1) 
18369  232 
proof  
233 
from zodd_imp_zdiv_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 have 

234 
"2 * (p  1) div 2 = 2 * ((p  1) div 2)" 

235 
by simp 

236 
with p_eq2 show " !!x. [ (p  1) div 2 < StandardRes p x; x \<in> B ] 

237 
==> p  StandardRes p x \<le> (p  1) div 2" 

238 
by simp 

239 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

240 

21233  241 
lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p  1) div 2)}" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

242 
by (auto simp add: D_def C_greater_zero) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

243 

21233  244 
lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p  (StandardRes p (y*a)) & (p  1) div 2 < StandardRes p (y*a))}" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

245 
by (auto simp add: F_def E_def D_def C_def B_def A_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

246 

21233  247 
lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p  1) div 2)}" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

248 
by (auto simp add: D_def C_def B_def A_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

249 

21233  250 
lemma D_leq: "x \<in> D ==> x \<le> (p  1) div 2" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

251 
by (auto simp add: D_eq) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

252 

21233  253 
lemma F_ge: "x \<in> F ==> x \<le> (p  1) div 2" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

254 
apply (auto simp add: F_eq A_def) 
18369  255 
proof  
256 
fix y 

257 
assume "(p  1) div 2 < StandardRes p (y * a)" 

258 
then have "p  StandardRes p (y * a) < p  ((p  1) div 2)" 

259 
by arith 

260 
also from p_eq2 have "... = 2 * ((p  1) div 2) + 1  ((p  1) div 2)" 

261 
by auto 

262 
also have "2 * ((p  1) div 2) + 1  (p  1) div 2 = (p  1) div 2 + 1" 

263 
by arith 

264 
finally show "p  StandardRes p (y * a) \<le> (p  1) div 2" 

265 
using zless_add1_eq [of "p  StandardRes p (y * a)" "(p  1) div 2"] by auto 

266 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

267 

27556  268 
lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1" 
18369  269 
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

270 

27556  271 
lemma A_prod_relprime: "zgcd (setprod id A) p = 1" 
30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

272 
by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime]) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

273 

21233  274 

61382  275 
subsection \<open>Relationships Between Gauss Sets\<close> 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

276 

21233  277 
lemma B_card_eq_A: "card B = card A" 
18369  278 
using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

279 

21233  280 
lemma B_card_eq: "card B = nat ((p  1) div 2)" 
18369  281 
by (simp add: B_card_eq_A A_card_eq) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

282 

21233  283 
lemma F_card_eq_E: "card F = card E" 
18369  284 
using finite_E by (simp add: F_def inj_on_pminusx_E card_image) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

285 

21233  286 
lemma C_card_eq_B: "card C = card B" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

287 
apply (insert finite_B) 
18369  288 
apply (subgoal_tac "inj_on (StandardRes p) B") 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

289 
apply (simp add: B_def C_def card_image) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

290 
apply (rule StandardRes_inj_on_ResSet) 
18369  291 
apply (simp add: B_res) 
292 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

293 

21233  294 
lemma D_E_disj: "D \<inter> E = {}" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

295 
by (auto simp add: D_def E_def) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

296 

21233  297 
lemma C_card_eq_D_plus_E: "card C = card D + card E" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

298 
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

299 

21233  300 
lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

301 
apply (insert D_E_disj finite_D finite_E C_eq) 
57418  302 
apply (frule setprod.union_disjoint [of D E id]) 
18369  303 
apply auto 
304 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

305 

21233  306 
lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

307 
apply (auto simp add: C_def) 
18369  308 
apply (insert finite_B SR_B_inj) 
57418  309 
apply (frule setprod.reindex [of "StandardRes p" B id]) 
310 
apply auto 

15392  311 
apply (rule setprod_same_function_zcong) 
18369  312 
apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0) 
313 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

314 

21233  315 
lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

316 
apply (rule Un_least) 
18369  317 
apply (auto simp add: A_def F_subset D_subset) 
318 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

319 

21233  320 
lemma F_D_disj: "(F \<inter> D) = {}" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

321 
apply (simp add: F_eq D_eq) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

322 
apply (auto simp add: F_eq D_eq) 
18369  323 
proof  
324 
fix y fix ya 

325 
assume "p  StandardRes p (y * a) = StandardRes p (ya * a)" 

326 
then have "p = StandardRes p (y * a) + StandardRes p (ya * a)" 

327 
by arith 

328 
moreover have "p dvd p" 

329 
by auto 

330 
ultimately have "p dvd (StandardRes p (y * a) + StandardRes p (ya * a))" 

331 
by auto 

332 
then have a: "[StandardRes p (y * a) + StandardRes p (ya * a) = 0] (mod p)" 

333 
by (auto simp add: zcong_def) 

334 
have "[y * a = StandardRes p (y * a)] (mod p)" 

335 
by (simp only: zcong_sym StandardRes_prop1) 

336 
moreover have "[ya * a = StandardRes p (ya * a)] (mod p)" 

337 
by (simp only: zcong_sym StandardRes_prop1) 

338 
ultimately have "[y * a + ya * a = 

339 
StandardRes p (y * a) + StandardRes p (ya * a)] (mod p)" 

340 
by (rule zcong_zadd) 

341 
with a have "[y * a + ya * a = 0] (mod p)" 

342 
apply (elim zcong_trans) 

343 
by (simp only: zcong_refl) 

344 
also have "y * a + ya * a = a * (y + ya)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

345 
by (simp add: distrib_left mult.commute) 
18369  346 
finally have "[a * (y + ya) = 0] (mod p)" . 
347 
with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"] 

348 
p_a_relprime 

349 
have a: "[y + ya = 0] (mod p)" 

350 
by auto 

351 
assume b: "y \<in> A" and c: "ya: A" 

352 
with A_def have "0 < y + ya" 

353 
by auto 

354 
moreover from b c A_def have "y + ya \<le> (p  1) div 2 + (p  1) div 2" 

355 
by auto 

356 
moreover from b c p_eq2 A_def have "y + ya < p" 

357 
by auto 

358 
ultimately show False 

359 
apply simp 

360 
apply (frule_tac m = p in zcong_not_zero) 

361 
apply (auto simp add: a) 

362 
done 

363 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

364 

21233  365 
lemma F_Un_D_card: "card (F \<union> D) = nat ((p  1) div 2)" 
18369  366 
proof  
367 
have "card (F \<union> D) = card E + card D" 

368 
by (auto simp add: finite_F finite_D F_D_disj 

369 
card_Un_disjoint F_card_eq_E) 

370 
then have "card (F \<union> D) = card C" 

371 
by (simp add: C_card_eq_D_plus_E) 

372 
from this show "card (F \<union> D) = nat ((p  1) div 2)" 

373 
by (simp add: C_card_eq_B B_card_eq) 

374 
qed 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

375 

21233  376 
lemma F_Un_D_eq_A: "F \<union> D = A" 
18369  377 
using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq) 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

378 

21233  379 
lemma prod_D_F_eq_prod_A: 
18369  380 
"(setprod id D) * (setprod id F) = setprod id A" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

381 
apply (insert F_D_disj finite_D finite_F) 
57418  382 
apply (frule setprod.union_disjoint [of F D id]) 
18369  383 
apply (auto simp add: F_Un_D_eq_A) 
384 
done 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

385 

21233  386 
lemma prod_F_zcong: 
18369  387 
"[setprod id F = ((1) ^ (card E)) * (setprod id E)] (mod p)" 
388 
proof  

389 
have "setprod id F = setprod id (op  p ` E)" 

390 
by (auto simp add: F_def) 

391 
then have "setprod id F = setprod (op  p) E" 

392 
apply simp 

393 
apply (insert finite_E inj_on_pminusx_E) 

57418  394 
apply (frule setprod.reindex [of "minus p" E id]) 
395 
apply auto 

18369  396 
done 
397 
then have one: 

398 
"[setprod id F = setprod (StandardRes p o (op  p)) E] (mod p)" 

399 
apply simp 

30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

400 
apply (insert p_g_0 finite_E StandardRes_prod) 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

401 
by (auto) 
18369  402 
moreover have a: "\<forall>x \<in> E. [p  x = 0  x] (mod p)" 
403 
apply clarify 

404 
apply (insert zcong_id [of p]) 

405 
apply (rule_tac a = p and m = p and c = x and d = x in zcong_zdiff, auto) 

406 
done 

407 
moreover have b: "\<forall>x \<in> E. [StandardRes p (p  x) = p  x](mod p)" 

408 
apply clarify 

409 
apply (simp add: StandardRes_prop1 zcong_sym) 

410 
done 

411 
moreover have "\<forall>x \<in> E. [StandardRes p (p  x) =  x](mod p)" 

412 
apply clarify 

413 
apply (insert a b) 

414 
apply (rule_tac b = "p  x" in zcong_trans, auto) 

415 
done 

416 
ultimately have c: 

417 
"[setprod (StandardRes p o (op  p)) E = setprod (uminus) E](mod p)" 

418 
apply simp 

30837
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

419 
using finite_E p_g_0 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

420 
setprod_same_function_zcong [of E "StandardRes p o (op  p)" uminus p] 
3d4832d9f7e4
added strong_setprod_cong[cong] (in analogy with setsum)
nipkow
parents:
30034
diff
changeset

421 
by auto 
18369  422 
then have two: "[setprod id F = setprod (uminus) E](mod p)" 
423 
apply (insert one c) 

424 
apply (rule zcong_trans [of "setprod id F" 

15392  425 
"setprod (StandardRes p o op  p) E" p 
18369  426 
"setprod uminus E"], auto) 
427 
done 

428 
also have "setprod uminus E = (setprod id E) * (1)^(card E)" 

22274  429 
using finite_E by (induct set: finite) auto 
18369  430 
then have "setprod uminus E = (1) ^ (card E) * (setprod id E)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

431 
by (simp add: mult.commute) 
18369  432 
with two show ?thesis 
433 
by simp 

15392  434 
qed 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

435 

21233  436 

61382  437 
subsection \<open>Gauss' Lemma\<close> 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

438 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57512
diff
changeset

439 
lemma aux: "setprod id A * ( 1) ^ card E * a ^ card A * ( 1) ^ card E = setprod id A * a ^ card A" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

440 
by (auto simp add: finite_E neg_one_special) 
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

441 

21233  442 
theorem pre_gauss_lemma: 
18369  443 
"[a ^ nat((p  1) div 2) = (1) ^ (card E)] (mod p)" 
444 
proof  

445 
have "[setprod id A = setprod id F * setprod id D](mod p)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

446 
by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del:setprod.cong) 
18369  447 
then have "[setprod id A = ((1)^(card E) * setprod id E) * 
448 
setprod id D] (mod p)" 

449 
apply (rule zcong_trans) 

57418  450 
apply (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.cong) 
18369  451 
done 
452 
then have "[setprod id A = ((1)^(card E) * setprod id C)] (mod p)" 

453 
apply (rule zcong_trans) 

454 
apply (insert C_prod_eq_D_times_E, erule subst) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

455 
apply (subst mult.assoc, auto) 
18369  456 
done 
457 
then have "[setprod id A = ((1)^(card E) * setprod id B)] (mod p)" 

458 
apply (rule zcong_trans) 

57418  459 
apply (simp add: C_B_zcong_prod zcong_scalar2 cong del:setprod.cong) 
18369  460 
done 
461 
then have "[setprod id A = ((1)^(card E) * 

462 
(setprod id ((%x. x * a) ` A)))] (mod p)" 

463 
by (simp add: B_def) 

464 
then have "[setprod id A = ((1)^(card E) * (setprod (%x. x * a) A))] 

465 
(mod p)" 

57418  466 
by (simp add:finite_A inj_on_xa_A setprod.reindex cong del:setprod.cong) 
18369  467 
moreover have "setprod (%x. x * a) A = 
468 
setprod (%x. a) A * setprod id A" 

22274  469 
using finite_A by (induct set: finite) auto 
18369  470 
ultimately have "[setprod id A = ((1)^(card E) * (setprod (%x. a) A * 
471 
setprod id A))] (mod p)" 

472 
by simp 

473 
then have "[setprod id A = ((1)^(card E) * a^(card A) * 

474 
setprod id A)](mod p)" 

475 
apply (rule zcong_trans) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

476 
apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc) 
18369  477 
done 
478 
then have a: "[setprod id A * (1)^(card E) = 

479 
((1)^(card E) * a^(card A) * setprod id A * (1)^(card E))](mod p)" 

480 
by (rule zcong_scalar) 

481 
then have "[setprod id A * (1)^(card E) = setprod id A * 

482 
(1)^(card E) * a^(card A) * (1)^(card E)](mod p)" 

483 
apply (rule zcong_trans) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

484 
apply (simp add: a mult.commute mult.left_commute) 
18369  485 
done 
486 
then have "[setprod id A * (1)^(card E) = setprod id A * 

487 
a^(card A)](mod p)" 

488 
apply (rule zcong_trans) 

57418  489 
apply (simp add: aux cong del:setprod.cong) 
18369  490 
done 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57512
diff
changeset

491 
with this zcong_cancel2 [of p "setprod id A" "( 1) ^ card E" "a ^ card A"] 
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57512
diff
changeset

492 
p_g_0 A_prod_relprime have "[( 1) ^ card E = a ^ card A](mod p)" 
18369  493 
by (simp add: order_less_imp_le) 
494 
from this show ?thesis 

495 
by (simp add: A_card_eq zcong_sym) 

15392  496 
qed 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

497 

21233  498 
theorem gauss_lemma: "(Legendre a p) = (1) ^ (card E)" 
15392  499 
proof  
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

500 
from Euler_Criterion p_prime p_g_2 have 
18369  501 
"[(Legendre a p) = 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

502 
by auto 
15392  503 
moreover note pre_gauss_lemma 
504 
ultimately have "[(Legendre a p) = (1) ^ (card E)] (mod p)" 

13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

505 
by (rule zcong_trans) 
15392  506 
moreover from p_a_relprime have "(Legendre a p) = 1  (Legendre a p) = (1)" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

507 
by (auto simp add: Legendre_def) 
15392  508 
moreover have "(1::int) ^ (card E) = 1  (1::int) ^ (card E) = 1" 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

509 
by (rule neg_one_power) 
15392  510 
ultimately show ?thesis 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

511 
by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym) 
15392  512 
qed 
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset

513 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16733
diff
changeset

514 
end 
21233  515 

516 
end 