author | nipkow |
Mon, 17 Oct 2016 11:46:22 +0200 | |
changeset 64267 | b9a1486e79be |
parent 61382 | efac889fccbc |
child 64272 | f76b6dda2e56 |
permissions | -rw-r--r-- |
38159 | 1 |
(* Title: HOL/Old_Number_Theory/Residues.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>Residue Sets\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
6 |
|
38159 | 7 |
theory Residues |
8 |
imports Int2 |
|
9 |
begin |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
10 |
|
61382 | 11 |
text \<open> |
19670 | 12 |
\medskip Define the residue of a set, the standard residue, |
61382 | 13 |
quadratic residues, and prove some basic properties.\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
14 |
|
38159 | 15 |
definition ResSet :: "int => int set => bool" |
16 |
where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
17 |
|
38159 | 18 |
definition StandardRes :: "int => int => int" |
19 |
where "StandardRes m x = x mod m" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
20 |
|
38159 | 21 |
definition QuadRes :: "int => int => bool" |
53077 | 22 |
where "QuadRes m x = (\<exists>y. ([y\<^sup>2 = x] (mod m)))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
23 |
|
38159 | 24 |
definition Legendre :: "int => int => int" where |
19670 | 25 |
"Legendre a p = (if ([a = 0] (mod p)) then 0 |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
26 |
else if (QuadRes p a) then 1 |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
27 |
else -1)" |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
28 |
|
38159 | 29 |
definition SR :: "int => int set" |
30 |
where "SR p = {x. (0 \<le> x) & (x < p)}" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
31 |
|
38159 | 32 |
definition SRStar :: "int => int set" |
33 |
where "SRStar p = {x. (0 < x) & (x < p)}" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
34 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
35 |
|
61382 | 36 |
subsection \<open>Some useful properties of StandardRes\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
37 |
|
18369 | 38 |
lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
39 |
by (auto simp add: StandardRes_def zcong_zmod) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
40 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
41 |
lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2) |
18369 | 42 |
= ([x1 = x2] (mod m))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
43 |
by (auto simp add: StandardRes_def zcong_zmod_eq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
44 |
|
18369 | 45 |
lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))" |
30042 | 46 |
by (auto simp add: StandardRes_def zcong_def dvd_eq_mod_eq_0) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
47 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
48 |
lemma StandardRes_prop4: "2 < m |
18369 | 49 |
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
50 |
by (auto simp add: StandardRes_def zcong_zmod_eq |
29948 | 51 |
mod_mult_eq [of x y m]) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
52 |
|
18369 | 53 |
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x" |
41541 | 54 |
by (auto simp add: StandardRes_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
55 |
|
18369 | 56 |
lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p" |
41541 | 57 |
by (auto simp add: StandardRes_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
58 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
59 |
lemma StandardRes_eq_zcong: |
18369 | 60 |
"(StandardRes m x = 0) = ([x = 0](mod m))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
61 |
by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
62 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
63 |
|
61382 | 64 |
subsection \<open>Relations between StandardRes, SRStar, and SR\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
65 |
|
18369 | 66 |
lemma SRStar_SR_prop: "x \<in> SRStar p ==> x \<in> SR p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
67 |
by (auto simp add: SRStar_def SR_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
68 |
|
18369 | 69 |
lemma StandardRes_SR_prop: "x \<in> SR p ==> StandardRes p x = x" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
70 |
by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
71 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
72 |
lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p) |
18369 | 73 |
= (~[x = 0] (mod p))" |
41541 | 74 |
apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
75 |
apply (subgoal_tac "0 < p") |
18369 | 76 |
apply (drule_tac a = x in pos_mod_sign, arith, simp) |
77 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
78 |
|
18369 | 79 |
lemma StandardRes_SRStar_prop1a: "x \<in> SRStar p ==> ~([x = 0] (mod p))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
80 |
by (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
81 |
|
16663 | 82 |
lemma StandardRes_SRStar_prop2: "[| 2 < p; zprime p; x \<in> SRStar p |] |
18369 | 83 |
==> StandardRes p (MultInv p x) \<in> SRStar p" |
84 |
apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp) |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
85 |
apply (rule MultInv_prop3) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
86 |
apply (auto simp add: SRStar_def zcong_def zdvd_not_zless) |
18369 | 87 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
88 |
|
18369 | 89 |
lemma StandardRes_SRStar_prop3: "x \<in> SRStar p ==> StandardRes p x = x" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
90 |
by (auto simp add: SRStar_SR_prop StandardRes_SR_prop) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
91 |
|
16663 | 92 |
lemma StandardRes_SRStar_prop4: "[| zprime p; 2 < p; x \<in> SRStar p |] |
18369 | 93 |
==> StandardRes p x \<in> SRStar p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
94 |
by (frule StandardRes_SRStar_prop3, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
95 |
|
16663 | 96 |
lemma SRStar_mult_prop1: "[| zprime p; 2 < p; x \<in> SRStar p; y \<in> SRStar p|] |
18369 | 97 |
==> (StandardRes p (x * y)):SRStar p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
98 |
apply (frule_tac x = x in StandardRes_SRStar_prop4, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
99 |
apply (frule_tac x = y in StandardRes_SRStar_prop4, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
100 |
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |
18369 | 101 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
102 |
|
16663 | 103 |
lemma SRStar_mult_prop2: "[| 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
|
104 |
x \<in> SRStar p |] |
18369 | 105 |
==> StandardRes p (a * MultInv p x) \<in> SRStar p" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
106 |
apply (frule_tac x = x in StandardRes_SRStar_prop2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
107 |
apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
108 |
apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3) |
18369 | 109 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
110 |
|
18369 | 111 |
lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
112 |
by (auto simp add: SRStar_def int_card_bdd_int_set_l_l) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
113 |
|
18369 | 114 |
lemma SRStar_finite: "2 < p ==> finite( SRStar p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
115 |
by (auto simp add: SRStar_def bdd_int_set_l_l_finite) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
116 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
117 |
|
61382 | 118 |
subsection \<open>Properties relating ResSets with StandardRes\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
119 |
|
18369 | 120 |
lemma aux: "x mod m = y mod m ==> [x = y] (mod m)" |
121 |
apply (subgoal_tac "x = y ==> [x = y](mod m)") |
|
122 |
apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)") |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
123 |
apply (auto simp add: zcong_zmod [of x y m]) |
18369 | 124 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
125 |
|
18369 | 126 |
lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
127 |
apply (auto simp add: ResSet_def StandardRes_def inj_on_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
128 |
apply (drule_tac m = m in aux, auto) |
18369 | 129 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
130 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
131 |
lemma StandardRes_Sum: "[| finite X; 0 < m |] |
64267 | 132 |
==> [sum f X = sum (StandardRes m o f) X](mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
133 |
apply (rule_tac F = X in finite_induct) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
134 |
apply (auto intro!: zcong_zadd simp add: StandardRes_prop1) |
18369 | 135 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
136 |
|
18369 | 137 |
lemma SR_pos: "0 < m ==> (StandardRes m ` X) \<subseteq> {x. 0 \<le> x & x < m}" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
138 |
by (auto simp add: StandardRes_ubound StandardRes_lbound) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
139 |
|
18369 | 140 |
lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
141 |
apply (rule_tac f = "StandardRes m" in finite_imageD) |
18369 | 142 |
apply (rule_tac B = "{x. (0 :: int) \<le> x & x < m}" in finite_subset) |
143 |
apply (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos) |
|
144 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
145 |
|
18369 | 146 |
lemma mod_mod_is_mod: "[x = x mod m](mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
147 |
by (auto simp add: zcong_zmod) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
148 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
149 |
lemma StandardRes_prod: "[| finite X; 0 < m |] |
18369 | 150 |
==> [setprod f X = setprod (StandardRes m o f) X] (mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
151 |
apply (rule_tac F = X in finite_induct) |
18369 | 152 |
apply (auto intro!: zcong_zmult simp add: StandardRes_prop1) |
153 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
154 |
|
19670 | 155 |
lemma ResSet_image: |
156 |
"[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> |
|
157 |
ResSet m (f ` A)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
158 |
by (auto simp add: ResSet_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
159 |
|
19670 | 160 |
|
61382 | 161 |
subsection \<open>Property for SRStar\<close> |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
162 |
|
18369 | 163 |
lemma ResSet_SRStar_prop: "ResSet p (SRStar p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
164 |
by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
165 |
|
18369 | 166 |
end |