3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
4 *) |
4 *) |
5 |
5 |
6 header {*Integers: Divisibility and Congruences*} |
6 header {*Integers: Divisibility and Congruences*} |
7 |
7 |
8 theory Int2 imports Finite2 WilsonRuss begin; |
8 theory Int2 imports Finite2 WilsonRuss begin |
9 |
9 |
10 text{*Note. This theory is being revised. See the web page |
10 text{*Note. This theory is being revised. See the web page |
11 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
11 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
12 |
12 |
13 constdefs |
13 constdefs |
14 MultInv :: "int => int => int" |
14 MultInv :: "int => int => int" |
15 "MultInv p x == x ^ nat (p - 2)"; |
15 "MultInv p x == x ^ nat (p - 2)" |
16 |
16 |
17 (*****************************************************************) |
17 (*****************************************************************) |
18 (* *) |
18 (* *) |
19 (* Useful lemmas about dvd and powers *) |
19 (* Useful lemmas about dvd and powers *) |
20 (* *) |
20 (* *) |
21 (*****************************************************************) |
21 (*****************************************************************) |
22 |
22 |
23 lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) --> |
23 lemma zpower_zdvd_prop1: |
24 p dvd ((y::int) ^ n)"; |
24 "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)" |
25 by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y]) |
25 by (induct n) (auto simp add: zdvd_zmult zdvd_zmult2 [of p y]) |
26 |
26 |
27 lemma zdvd_bounds: "n dvd m ==> (m \<le> (0::int) | n \<le> m)"; |
27 lemma zdvd_bounds: "n dvd m ==> m \<le> (0::int) | n \<le> m" |
28 proof -; |
28 proof - |
29 assume "n dvd m"; |
29 assume "n dvd m" |
30 then have "~(0 < m & m < n)"; |
30 then have "~(0 < m & m < n)" |
31 apply (insert zdvd_not_zless [of m n]) |
31 using zdvd_not_zless [of m n] by auto |
32 by (rule contrapos_pn, auto) |
|
33 then have "(~0 < m | ~m < n)" by auto |
|
34 then show ?thesis by auto |
32 then show ?thesis by auto |
35 qed; |
33 qed |
36 |
34 |
37 lemma aux4: " -(m * n) = (-m) * (n::int)"; |
35 lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==> |
|
36 (p dvd m) | (p dvd n)" |
|
37 apply (cases "0 \<le> m") |
|
38 apply (simp add: zprime_zdvd_zmult) |
|
39 apply (insert zprime_zdvd_zmult [of "-m" p n]) |
|
40 apply auto |
|
41 done |
|
42 |
|
43 lemma zpower_zdvd_prop2: |
|
44 "zprime p \<Longrightarrow> p dvd ((y::int) ^ n) \<Longrightarrow> 0 < n \<Longrightarrow> p dvd y" |
|
45 apply (induct n) |
|
46 apply simp |
|
47 apply (frule zprime_zdvd_zmult_better) |
|
48 apply simp |
|
49 apply force |
|
50 done |
|
51 |
|
52 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y" |
|
53 proof - |
|
54 assume "0 < z" |
|
55 then have "(x div z) * z \<le> (x div z) * z + x mod z" |
|
56 by arith |
|
57 also have "... = x" |
|
58 by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac) |
|
59 also assume "x < y * z" |
|
60 finally show ?thesis |
|
61 by (auto simp add: prems mult_less_cancel_right, insert prems, arith) |
|
62 qed |
|
63 |
|
64 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y" |
|
65 proof - |
|
66 assume "0 < z" and "x < (y * z) + z" |
|
67 then have "x < (y + 1) * z" by (auto simp add: int_distrib) |
|
68 then have "x div z < y + 1" |
|
69 apply - |
|
70 apply (rule_tac y = "y + 1" in div_prop1) |
|
71 apply (auto simp add: prems) |
|
72 done |
|
73 then show ?thesis by auto |
|
74 qed |
|
75 |
|
76 lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)" |
|
77 proof- |
|
78 assume "0 < y" |
|
79 from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto |
|
80 moreover have "0 \<le> x mod y" |
|
81 by (auto simp add: prems pos_mod_sign) |
|
82 ultimately show ?thesis |
|
83 by arith |
|
84 qed |
|
85 |
|
86 (*****************************************************************) |
|
87 (* *) |
|
88 (* Useful properties of congruences *) |
|
89 (* *) |
|
90 (*****************************************************************) |
|
91 |
|
92 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)" |
|
93 by (auto simp add: zcong_def) |
|
94 |
|
95 lemma zcong_id: "[m = 0] (mod m)" |
|
96 by (auto simp add: zcong_def zdvd_0_right) |
|
97 |
|
98 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)" |
|
99 by (auto simp add: zcong_refl zcong_zadd) |
|
100 |
|
101 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)" |
|
102 by (induct z) (auto simp add: zcong_zmult) |
|
103 |
|
104 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
|
105 [a = d](mod m)" |
|
106 apply (erule zcong_trans) |
|
107 apply simp |
|
108 done |
|
109 |
|
110 lemma aux1: "a - b = (c::int) ==> a = c + b" |
38 by auto |
111 by auto |
39 |
112 |
40 lemma zprime_zdvd_zmult_better: "[| zprime p; p dvd (m * n) |] ==> |
|
41 (p dvd m) | (p dvd n)"; |
|
42 apply (case_tac "0 \<le> m") |
|
43 apply (simp add: zprime_zdvd_zmult) |
|
44 by (insert zprime_zdvd_zmult [of "-m" p n], auto) |
|
45 |
|
46 lemma zpower_zdvd_prop2 [rule_format]: "zprime p --> p dvd ((y::int) ^ n) |
|
47 --> 0 < n --> p dvd y"; |
|
48 apply (induct_tac n, auto) |
|
49 apply (frule zprime_zdvd_zmult_better, auto) |
|
50 done |
|
51 |
|
52 lemma stupid: "(0 :: int) \<le> y ==> x \<le> x + y"; |
|
53 by arith |
|
54 |
|
55 lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"; |
|
56 proof -; |
|
57 assume "0 < z"; |
|
58 then have "(x div z) * z \<le> (x div z) * z + x mod z"; |
|
59 apply (rule_tac x = "x div z * z" in stupid) |
|
60 by (simp add: pos_mod_sign) |
|
61 also have "... = x"; |
|
62 by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac) |
|
63 also assume "x < y * z"; |
|
64 finally show ?thesis; |
|
65 by (auto simp add: prems mult_less_cancel_right, insert prems, arith) |
|
66 qed; |
|
67 |
|
68 lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"; |
|
69 proof -; |
|
70 assume "0 < z" and "x < (y * z) + z"; |
|
71 then have "x < (y + 1) * z" by (auto simp add: int_distrib) |
|
72 then have "x div z < y + 1"; |
|
73 by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems) |
|
74 then show ?thesis by auto |
|
75 qed; |
|
76 |
|
77 lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"; |
|
78 proof-; |
|
79 assume "0 < y"; |
|
80 from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto |
|
81 moreover have "0 \<le> x mod y"; |
|
82 by (auto simp add: prems pos_mod_sign) |
|
83 ultimately show ?thesis; |
|
84 by arith |
|
85 qed; |
|
86 |
|
87 (*****************************************************************) |
|
88 (* *) |
|
89 (* Useful properties of congruences *) |
|
90 (* *) |
|
91 (*****************************************************************) |
|
92 |
|
93 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"; |
|
94 by (auto simp add: zcong_def) |
|
95 |
|
96 lemma zcong_id: "[m = 0] (mod m)"; |
|
97 by (auto simp add: zcong_def zdvd_0_right) |
|
98 |
|
99 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"; |
|
100 by (auto simp add: zcong_refl zcong_zadd) |
|
101 |
|
102 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"; |
|
103 by (induct_tac z, auto simp add: zcong_zmult) |
|
104 |
|
105 lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> |
|
106 [a = d](mod m)"; |
|
107 by (auto, rule_tac b = c in zcong_trans) |
|
108 |
|
109 lemma aux1: "a - b = (c::int) ==> a = c + b"; |
|
110 by auto |
|
111 |
|
112 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
113 lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = |
113 [c = b * d] (mod m))"; |
114 [c = b * d] (mod m))" |
114 apply (auto simp add: zcong_def dvd_def) |
115 apply (auto simp add: zcong_def dvd_def) |
115 apply (rule_tac x = "ka + k * d" in exI) |
116 apply (rule_tac x = "ka + k * d" in exI) |
116 apply (drule aux1)+; |
117 apply (drule aux1)+ |
117 apply (auto simp add: int_distrib) |
118 apply (auto simp add: int_distrib) |
118 apply (rule_tac x = "ka - k * d" in exI) |
119 apply (rule_tac x = "ka - k * d" in exI) |
119 apply (drule aux1)+; |
120 apply (drule aux1)+ |
120 apply (auto simp add: int_distrib) |
121 apply (auto simp add: int_distrib) |
121 done |
122 done |
122 |
123 |
123 lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
124 lemma zcong_zmult_prop2: "[a = b](mod m) ==> |
124 ([c = d * a](mod m) = [c = d * b] (mod m))"; |
125 ([c = d * a](mod m) = [c = d * b] (mod m))" |
125 by (auto simp add: zmult_ac zcong_zmult_prop1) |
126 by (auto simp add: zmult_ac zcong_zmult_prop1) |
126 |
127 |
127 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
128 lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); |
128 ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"; |
129 ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)" |
129 apply (auto simp add: zcong_def) |
130 apply (auto simp add: zcong_def) |
130 apply (drule zprime_zdvd_zmult_better, auto) |
131 apply (drule zprime_zdvd_zmult_better, auto) |
131 done |
132 done |
132 |
133 |
133 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
134 lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); |
134 x < m; y < m |] ==> x = y"; |
135 x < m; y < m |] ==> x = y" |
135 apply (simp add: zcong_zmod_eq) |
136 apply (simp add: zcong_zmod_eq) |
136 apply (subgoal_tac "(x mod m) = x"); |
137 apply (subgoal_tac "(x mod m) = x") |
137 apply (subgoal_tac "(y mod m) = y"); |
138 apply (subgoal_tac "(y mod m) = y") |
138 apply simp |
139 apply simp |
139 apply (rule_tac [1-2] mod_pos_pos_trivial) |
140 apply (rule_tac [1-2] mod_pos_pos_trivial) |
140 by auto |
141 apply auto |
|
142 done |
141 |
143 |
142 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> |
144 lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> |
143 ~([x = 1] (mod p))"; |
145 ~([x = 1] (mod p))" |
144 proof; |
146 proof |
145 assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)" |
147 assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)" |
146 then have "[1 = -1] (mod p)"; |
148 then have "[1 = -1] (mod p)" |
147 apply (auto simp add: zcong_sym) |
149 apply (auto simp add: zcong_sym) |
148 apply (drule zcong_trans, auto) |
150 apply (drule zcong_trans, auto) |
149 done |
151 done |
150 then have "[1 + 1 = -1 + 1] (mod p)"; |
152 then have "[1 + 1 = -1 + 1] (mod p)" |
151 by (simp only: zcong_shift) |
153 by (simp only: zcong_shift) |
152 then have "[2 = 0] (mod p)"; |
154 then have "[2 = 0] (mod p)" |
153 by auto |
155 by auto |
154 then have "p dvd 2"; |
156 then have "p dvd 2" |
155 by (auto simp add: dvd_def zcong_def) |
157 by (auto simp add: dvd_def zcong_def) |
156 with prems show False; |
158 with prems show False |
157 by (auto simp add: zdvd_not_zless) |
159 by (auto simp add: zdvd_not_zless) |
158 qed; |
160 qed |
159 |
161 |
160 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"; |
162 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)" |
161 by (auto simp add: zcong_def) |
163 by (auto simp add: zcong_def) |
162 |
164 |
163 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
165 lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> |
164 [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"; |
166 [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" |
165 by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
167 by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult) |
166 |
168 |
167 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
169 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==> |
168 ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"; |
170 ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)" |
169 apply auto |
171 apply auto |
170 apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
172 apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero) |
171 by auto |
173 apply auto |
172 |
174 done |
173 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"; |
175 |
|
176 lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" |
174 by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
177 by (auto simp add: zcong_zero_equiv_div zdvd_not_zless) |
175 |
178 |
176 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"; |
179 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0" |
177 apply (drule order_le_imp_less_or_eq, auto) |
180 apply (drule order_le_imp_less_or_eq, auto) |
178 by (frule_tac m = m in zcong_not_zero, auto) |
181 apply (frule_tac m = m in zcong_not_zero) |
|
182 apply auto |
|
183 done |
179 |
184 |
180 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
185 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. (zgcd(x,y) = 1) |] |
181 ==> zgcd (setprod id A,y) = 1"; |
186 ==> zgcd (setprod id A,y) = 1" |
182 by (induct set: Finites, auto simp add: zgcd_zgcd_zmult) |
187 by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult) |
183 |
188 |
184 (*****************************************************************) |
189 (*****************************************************************) |
185 (* *) |
190 (* *) |
186 (* Some properties of MultInv *) |
191 (* Some properties of MultInv *) |
187 (* *) |
192 (* *) |
188 (*****************************************************************) |
193 (*****************************************************************) |
189 |
194 |
190 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
195 lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> |
191 [(MultInv p x) = (MultInv p y)] (mod p)"; |
196 [(MultInv p x) = (MultInv p y)] (mod p)" |
192 by (auto simp add: MultInv_def zcong_zpower) |
197 by (auto simp add: MultInv_def zcong_zpower) |
193 |
198 |
194 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
199 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
195 [(x * (MultInv p x)) = 1] (mod p)"; |
200 [(x * (MultInv p x)) = 1] (mod p)" |
196 proof (simp add: MultInv_def zcong_eq_zdvd_prop); |
201 proof (simp add: MultInv_def zcong_eq_zdvd_prop) |
197 assume "2 < p" and "zprime p" and "~ p dvd x"; |
202 assume "2 < p" and "zprime p" and "~ p dvd x" |
198 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"; |
203 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)" |
199 by auto |
204 by auto |
200 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"; |
205 also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)" |
201 by (simp only: nat_add_distrib, auto) |
206 by (simp only: nat_add_distrib, auto) |
202 also have "p - 2 + 1 = p - 1" by arith |
207 also have "p - 2 + 1 = p - 1" by arith |
203 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"; |
208 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)" |
204 by (rule ssubst, auto) |
209 by (rule ssubst, auto) |
205 also from prems have "[x ^ nat (p - 1) = 1] (mod p)"; |
210 also from prems have "[x ^ nat (p - 1) = 1] (mod p)" |
206 by (auto simp add: Little_Fermat) |
211 by (auto simp add: Little_Fermat) |
207 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.; |
212 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" . |
208 qed; |
213 qed |
209 |
214 |
210 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
215 lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
211 [(MultInv p x) * x = 1] (mod p)"; |
216 [(MultInv p x) * x = 1] (mod p)" |
212 by (auto simp add: MultInv_prop2 zmult_ac) |
217 by (auto simp add: MultInv_prop2 zmult_ac) |
213 |
218 |
214 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"; |
219 lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))" |
215 by (simp add: nat_diff_distrib) |
220 by (simp add: nat_diff_distrib) |
216 |
221 |
217 lemma aux_2: "2 < p ==> 0 < nat (p - 2)"; |
222 lemma aux_2: "2 < p ==> 0 < nat (p - 2)" |
218 by auto |
223 by auto |
219 |
224 |
220 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
225 lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
221 ~([MultInv p x = 0](mod p))"; |
226 ~([MultInv p x = 0](mod p))" |
222 apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
227 apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1) |
223 apply (drule aux_2) |
228 apply (drule aux_2) |
224 apply (drule zpower_zdvd_prop2, auto) |
229 apply (drule zpower_zdvd_prop2, auto) |
225 done |
230 done |
226 |
231 |
227 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
232 lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
228 [(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
233 [(MultInv p (MultInv p x)) = (x * (MultInv p x) * |
229 (MultInv p (MultInv p x)))] (mod p)"; |
234 (MultInv p (MultInv p x)))] (mod p)" |
230 apply (drule MultInv_prop2, auto) |
235 apply (drule MultInv_prop2, auto) |
231 apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto); |
236 apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto) |
232 apply (auto simp add: zcong_sym) |
237 apply (auto simp add: zcong_sym) |
233 done |
238 done |
234 |
239 |
235 lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
240 lemma aux__2: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> |
236 [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)"; |
241 [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)" |
237 apply (frule MultInv_prop3, auto) |
242 apply (frule MultInv_prop3, auto) |
238 apply (insert MultInv_prop2 [of p "MultInv p x"], auto) |
243 apply (insert MultInv_prop2 [of p "MultInv p x"], auto) |
239 apply (drule MultInv_prop2, auto) |
244 apply (drule MultInv_prop2, auto) |
240 apply (drule_tac k = x in zcong_scalar2, auto) |
245 apply (drule_tac k = x in zcong_scalar2, auto) |
241 apply (auto simp add: zmult_ac) |
246 apply (auto simp add: zmult_ac) |
242 done |
247 done |
243 |
248 |
244 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
249 lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> |
245 [(MultInv p (MultInv p x)) = x] (mod p)"; |
250 [(MultInv p (MultInv p x)) = x] (mod p)" |
246 apply (frule aux__1, auto) |
251 apply (frule aux__1, auto) |
247 apply (drule aux__2, auto) |
252 apply (drule aux__2, auto) |
248 apply (drule zcong_trans, auto) |
253 apply (drule zcong_trans, auto) |
249 done |
254 done |
250 |
255 |
251 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
256 lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); |
252 ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
257 ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> |
253 [x = y] (mod p)"; |
258 [x = y] (mod p)" |
254 apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
259 apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and |
255 m = p and k = x in zcong_scalar) |
260 m = p and k = x in zcong_scalar) |
256 apply (insert MultInv_prop2 [of p x], simp) |
261 apply (insert MultInv_prop2 [of p x], simp) |
257 apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
262 apply (auto simp only: zcong_sym [of "MultInv p x * x"]) |
258 apply (auto simp add: zmult_ac) |
263 apply (auto simp add: zmult_ac) |
259 apply (drule zcong_trans, auto) |
264 apply (drule zcong_trans, auto) |
260 apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto) |
265 apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto) |
261 apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac) |
266 apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac) |
262 apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
267 apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x]) |
263 apply (auto simp add: zcong_sym) |
268 apply (auto simp add: zcong_sym) |
264 done |
269 done |
265 |
270 |
266 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
271 lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> |
267 [a * MultInv p j = a * MultInv p k] (mod p)"; |
272 [a * MultInv p j = a * MultInv p k] (mod p)" |
268 by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
273 by (drule MultInv_prop1, auto simp add: zcong_scalar2) |
269 |
274 |
270 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
275 lemma aux___1: "[j = a * MultInv p k] (mod p) ==> |
271 [j * k = a * MultInv p k * k] (mod p)"; |
276 [j * k = a * MultInv p k * k] (mod p)" |
272 by (auto simp add: zcong_scalar) |
277 by (auto simp add: zcong_scalar) |
273 |
278 |
274 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
279 lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); |
275 [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"; |
280 [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)" |
276 apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
281 apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 |
277 [of "MultInv p k * k" 1 p "j * k" a]) |
282 [of "MultInv p k * k" 1 p "j * k" a]) |
278 apply (auto simp add: zmult_ac) |
283 apply (auto simp add: zmult_ac) |
279 done |
284 done |
280 |
285 |
281 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
286 lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = |
282 (MultInv p j) * a] (mod p)"; |
287 (MultInv p j) * a] (mod p)" |
283 by (auto simp add: zmult_assoc zcong_scalar2) |
288 by (auto simp add: zmult_assoc zcong_scalar2) |
284 |
289 |
285 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
290 lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); |
286 [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
291 [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |] |
287 ==> [k = a * (MultInv p j)] (mod p)"; |
292 ==> [k = a * (MultInv p j)] (mod p)" |
288 apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
293 apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 |
289 [of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
294 [of "MultInv p j * j" 1 p "MultInv p j * a" k]) |
290 apply (auto simp add: zmult_ac zcong_sym) |
295 apply (auto simp add: zmult_ac zcong_sym) |
291 done |
296 done |
292 |
297 |
293 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
298 lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); |
294 ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
299 ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> |
295 [k = a * MultInv p j] (mod p)"; |
300 [k = a * MultInv p j] (mod p)" |
296 apply (drule aux___1) |
301 apply (drule aux___1) |
297 apply (frule aux___2, auto) |
302 apply (frule aux___2, auto) |
298 by (drule aux___3, drule aux___4, auto) |
303 by (drule aux___3, drule aux___4, auto) |
299 |
304 |
300 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
305 lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); |
301 ~([k = 0](mod p)); ~([j = 0](mod p)); |
306 ~([k = 0](mod p)); ~([j = 0](mod p)); |
302 [a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
307 [a * MultInv p j = a * MultInv p k] (mod p) |] ==> |
303 [j = k] (mod p)"; |
308 [j = k] (mod p)" |
304 apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
309 apply (auto simp add: zcong_eq_zdvd_prop [of a p]) |
305 apply (frule zprime_imp_zrelprime, auto) |
310 apply (frule zprime_imp_zrelprime, auto) |
306 apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
311 apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto) |
307 apply (drule MultInv_prop5, auto) |
312 apply (drule MultInv_prop5, auto) |
308 done |
313 done |
309 |
314 |
310 end |
315 end |