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/Int2.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 {*Integers: Divisibility and Congruences*} |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
6 |
|
27556 | 7 |
theory Int2 |
8 |
imports Finite2 WilsonRuss |
|
9 |
begin |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
10 |
|
38159 | 11 |
definition MultInv :: "int => int => int" |
12 |
where "MultInv p x = x ^ nat (p - 2)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
13 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
14 |
|
19670 | 15 |
subsection {* Useful lemmas about dvd and powers *} |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
16 |
|
18369 | 17 |
lemma zpower_zdvd_prop1: |
18 |
"0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)" |
|
30042 | 19 |
by (induct n) (auto simp add: dvd_mult2 [of p y]) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
20 |
|
18369 | 21 |
lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m" |
22 |
proof - |
|
23 |
assume "n dvd m" |
|
24 |
then have "~(0 < m & m < n)" |
|
25 |
using zdvd_not_zless [of m n] by auto |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
26 |
then show ?thesis by auto |
18369 | 27 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
28 |
|
19670 | 29 |
lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==> |
18369 | 30 |
(p dvd m) | (p dvd n)" |
31 |
apply (cases "0 \<le> m") |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
32 |
apply (simp add: zprime_zdvd_zmult) |
18369 | 33 |
apply (insert zprime_zdvd_zmult [of "-m" p n]) |
34 |
apply auto |
|
35 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
36 |
|
18369 | 37 |
lemma zpower_zdvd_prop2: |
38 |
"zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y" |
|
39 |
apply (induct n) |
|
40 |
apply simp |
|
41 |
apply (frule zprime_zdvd_zmult_better) |
|
42 |
apply simp |
|
30042 | 43 |
apply (force simp del:dvd_mult) |
18369 | 44 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
45 |
|
41541 | 46 |
lemma div_prop1: |
47 |
assumes "0 < z" and "(x::int) < y * z" |
|
48 |
shows "x div z < y" |
|
18369 | 49 |
proof - |
41541 | 50 |
from `0 < z` have modth: "x mod z \<ge> 0" by simp |
23315 | 51 |
have "(x div z) * z \<le> (x div z) * z" by simp |
52 |
then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith |
|
53 |
also have "\<dots> = x" |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
54 |
by (auto simp add: zmod_zdiv_equality [symmetric] ac_simps) |
41541 | 55 |
also note `x < y * z` |
18369 | 56 |
finally show ?thesis |
41541 | 57 |
apply (auto simp add: mult_less_cancel_right) |
58 |
using assms apply arith |
|
59 |
done |
|
18369 | 60 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
61 |
|
41541 | 62 |
lemma div_prop2: |
63 |
assumes "0 < z" and "(x::int) < (y * z) + z" |
|
64 |
shows "x div z \<le> y" |
|
18369 | 65 |
proof - |
41541 | 66 |
from assms have "x < (y + 1) * z" by (auto simp add: int_distrib) |
18369 | 67 |
then have "x div z < y + 1" |
68 |
apply (rule_tac y = "y + 1" in div_prop1) |
|
41541 | 69 |
apply (auto simp add: `0 < z`) |
18369 | 70 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
71 |
then show ?thesis by auto |
18369 | 72 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
73 |
|
41541 | 74 |
lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)" |
18369 | 75 |
proof- |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
76 |
from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto |
41541 | 77 |
moreover have "0 \<le> x mod y" by (auto simp add: assms) |
78 |
ultimately show ?thesis by arith |
|
18369 | 79 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
80 |
|
19670 | 81 |
|
82 |
subsection {* Useful properties of congruences *} |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
83 |
|
18369 | 84 |
lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
85 |
by (auto simp add: zcong_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
86 |
|
18369 | 87 |
lemma zcong_id: "[m = 0] (mod m)" |
30042 | 88 |
by (auto simp add: zcong_def) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
89 |
|
18369 | 90 |
lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)" |
41541 | 91 |
by (auto simp add: zcong_zadd) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
92 |
|
18369 | 93 |
lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)" |
94 |
by (induct z) (auto simp add: zcong_zmult) |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
95 |
|
19670 | 96 |
lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
18369 | 97 |
[a = d](mod m)" |
98 |
apply (erule zcong_trans) |
|
99 |
apply simp |
|
100 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
101 |
|
18369 | 102 |
lemma aux1: "a - b = (c::int) ==> a = c + b" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
103 |
by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
104 |
|
19670 | 105 |
lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
18369 | 106 |
[c = b * d] (mod m))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
107 |
apply (auto simp add: zcong_def dvd_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
108 |
apply (rule_tac x = "ka + k * d" in exI) |
18369 | 109 |
apply (drule aux1)+ |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
110 |
apply (auto simp add: int_distrib) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
111 |
apply (rule_tac x = "ka - k * d" in exI) |
18369 | 112 |
apply (drule aux1)+ |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
113 |
apply (auto simp add: int_distrib) |
18369 | 114 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
115 |
|
19670 | 116 |
lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
18369 | 117 |
([c = d * a](mod m) = [c = d * b] (mod m))" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
118 |
by (auto simp add: ac_simps zcong_zmult_prop1) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
119 |
|
19670 | 120 |
lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
18369 | 121 |
~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
122 |
apply (auto simp add: zcong_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
123 |
apply (drule zprime_zdvd_zmult_better, auto) |
18369 | 124 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
125 |
|
19670 | 126 |
lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
18369 | 127 |
x < m; y < m |] ==> x = y" |
44766 | 128 |
by (metis zcong_not zcong_sym less_linear) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
129 |
|
41541 | 130 |
lemma zcong_neg_1_impl_ne_1: |
131 |
assumes "2 < p" and "[x = -1] (mod p)" |
|
132 |
shows "~([x = 1] (mod p))" |
|
18369 | 133 |
proof |
41541 | 134 |
assume "[x = 1] (mod p)" |
135 |
with assms have "[1 = -1] (mod p)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
136 |
apply (auto simp add: zcong_sym) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
137 |
apply (drule zcong_trans, auto) |
18369 | 138 |
done |
139 |
then have "[1 + 1 = -1 + 1] (mod p)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
140 |
by (simp only: zcong_shift) |
18369 | 141 |
then have "[2 = 0] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
142 |
by auto |
18369 | 143 |
then have "p dvd 2" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
144 |
by (auto simp add: dvd_def zcong_def) |
41541 | 145 |
with `2 < p` show False |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
146 |
by (auto simp add: zdvd_not_zless) |
18369 | 147 |
qed |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
148 |
|
18369 | 149 |
lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
150 |
by (auto simp add: zcong_def) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
151 |
|
19670 | 152 |
lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
153 |
[a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
154 |
by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
155 |
|
16663 | 156 |
lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
18369 | 157 |
~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)" |
19670 | 158 |
apply auto |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
159 |
apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
18369 | 160 |
apply auto |
161 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
162 |
|
19670 | 163 |
lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
164 |
by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
165 |
|
18369 | 166 |
lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
167 |
apply (drule order_le_imp_less_or_eq, auto) |
18369 | 168 |
apply (frule_tac m = m in zcong_not_zero) |
169 |
apply auto |
|
170 |
done |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
171 |
|
27556 | 172 |
lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |] |
173 |
==> zgcd (setprod id A) y = 1" |
|
22274 | 174 |
by (induct set: finite) (auto simp add: zgcd_zgcd_zmult) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
175 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
176 |
|
19670 | 177 |
subsection {* Some properties of MultInv *} |
178 |
||
179 |
lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
|
18369 | 180 |
[(MultInv p x) = (MultInv p y)] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
181 |
by (auto simp add: MultInv_def zcong_zpower) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
182 |
|
19670 | 183 |
lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
18369 | 184 |
[(x * (MultInv p x)) = 1] (mod p)" |
185 |
proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
|
41541 | 186 |
assume 1: "2 < p" and 2: "zprime p" and 3: "~ p dvd x" |
18369 | 187 |
have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
188 |
by auto |
41541 | 189 |
also from 1 have "nat (p - 2) + 1 = nat (p - 2 + 1)" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19670
diff
changeset
|
190 |
by (simp only: nat_add_distrib) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
191 |
also have "p - 2 + 1 = p - 1" by arith |
18369 | 192 |
finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
193 |
by (rule ssubst, auto) |
41541 | 194 |
also from 2 3 have "[x ^ nat (p - 1) = 1] (mod p)" |
19670 | 195 |
by (auto simp add: Little_Fermat) |
18369 | 196 |
finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" . |
197 |
qed |
|
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
198 |
|
19670 | 199 |
lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
18369 | 200 |
[(MultInv p x) * x = 1] (mod p)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
201 |
by (auto simp add: MultInv_prop2 ac_simps) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
202 |
|
18369 | 203 |
lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
204 |
by (simp add: nat_diff_distrib) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
205 |
|
18369 | 206 |
lemma aux_2: "2 < p ==> 0 < nat (p - 2)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
207 |
by auto |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
208 |
|
19670 | 209 |
lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
18369 | 210 |
~([MultInv p x = 0](mod p))" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
211 |
apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
212 |
apply (drule aux_2) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
213 |
apply (drule zpower_zdvd_prop2, auto) |
18369 | 214 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
215 |
|
19670 | 216 |
lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
217 |
[(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
|
18369 | 218 |
(MultInv p (MultInv p x)))] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
219 |
apply (drule MultInv_prop2, auto) |
18369 | 220 |
apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
221 |
apply (auto simp add: zcong_sym) |
18369 | 222 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
223 |
|
16663 | 224 |
lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
18369 | 225 |
[(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
226 |
apply (frule MultInv_prop3, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
227 |
apply (insert MultInv_prop2 [of p "MultInv p x"], auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
228 |
apply (drule MultInv_prop2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
229 |
apply (drule_tac k = x in zcong_scalar2, auto) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
230 |
apply (auto simp add: ac_simps) |
18369 | 231 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
232 |
|
19670 | 233 |
lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
18369 | 234 |
[(MultInv p (MultInv p x)) = x] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
235 |
apply (frule aux__1, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
236 |
apply (drule aux__2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
237 |
apply (drule zcong_trans, auto) |
18369 | 238 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
239 |
|
19670 | 240 |
lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
241 |
~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
|
18369 | 242 |
[x = y] (mod p)" |
19670 | 243 |
apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
244 |
m = p and k = x in zcong_scalar) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
245 |
apply (insert MultInv_prop2 [of p x], simp) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
246 |
apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
247 |
apply (auto simp add: ac_simps) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
248 |
apply (drule zcong_trans, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
249 |
apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
250 |
apply (insert MultInv_prop2a [of p y], auto simp add: ac_simps) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
251 |
apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
252 |
apply (auto simp add: zcong_sym) |
18369 | 253 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
254 |
|
19670 | 255 |
lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
18369 | 256 |
[a * MultInv p j = a * MultInv p k] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
257 |
by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
258 |
|
19670 | 259 |
lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
18369 | 260 |
[j * k = a * MultInv p k * k] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
261 |
by (auto simp add: zcong_scalar) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
262 |
|
19670 | 263 |
lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
18369 | 264 |
[j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)" |
19670 | 265 |
apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
266 |
[of "MultInv p k * k" 1 p "j * k" a]) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
267 |
apply (auto simp add: ac_simps) |
18369 | 268 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
269 |
|
19670 | 270 |
lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
18369 | 271 |
(MultInv p j) * a] (mod p)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
44766
diff
changeset
|
272 |
by (auto simp add: mult.assoc zcong_scalar2) |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
273 |
|
19670 | 274 |
lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
275 |
[(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
18369 | 276 |
==> [k = a * (MultInv p j)] (mod p)" |
19670 | 277 |
apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
278 |
[of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
279 |
apply (auto simp add: ac_simps zcong_sym) |
18369 | 280 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
281 |
|
19670 | 282 |
lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
283 |
~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
|
18369 | 284 |
[k = a * MultInv p j] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
285 |
apply (drule aux___1) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
286 |
apply (frule aux___2, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
287 |
by (drule aux___3, drule aux___4, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
288 |
|
19670 | 289 |
lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
290 |
~([k = 0](mod p)); ~([j = 0](mod p)); |
19670 | 291 |
[a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
18369 | 292 |
[j = k] (mod p)" |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
293 |
apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
294 |
apply (frule zprime_imp_zrelprime, auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
295 |
apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
296 |
apply (drule MultInv_prop5, auto) |
18369 | 297 |
done |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
298 |
|
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
diff
changeset
|
299 |
end |