1(* For interactive use
2app load ["gcdTheory", "wordsLib", "intLib", "ExtendedEuclidTheory"];
3quietdec := true;
4open gcdTheory dividesTheory arithmeticTheory
5     pairTheory intLib integerTheory
6     wordsTheory wordsLib
7     ExtendedEuclidTheory;
8quietdec := false;
9*)
10
11open HolKernel Parse boolLib bossLib ExtendedEuclidTheory
12   gcdTheory dividesTheory arithmeticTheory
13   pairTheory wordsTheory wordsLib intLib integerTheory;
14
15val _ = new_theory "ideaMult";
16
17val ARW = RW_TAC arith_ss;
18val ASP = FULL_SIMP_TAC arith_ss;
19
20(*---------------------------------------------------------------------------*)
21(* To be proved, or assumed, but will assert this well-known fact for now.   *)
22(*---------------------------------------------------------------------------*)
23
24val _ = intLib.prefer_int();
25
26val prime_axiom = new_axiom("prime_axiom", ``prime 65537n``);
27
28val minv_Lemma1 = Q.store_thm
29("minv_Lemma1",
30 ` !a b. b < a ==> ~(0 < b) \/ ~divides a b`,
31 ARW [] THEN `!a b. ~(a <= b) ==> ~(0 < b /\ divides a b)`
32   by METIS_TAC [MONO_NOT,DIVIDES_LE] THEN
33 `~(0 < b /\ divides a b) = ~(0 < b) \/ ~(divides a b)`
34   by METIS_TAC [DE_MORGAN_THM] THEN
35 `(b < a) ==> (~(0 < b) \/ ~divides a b)`
36   by METIS_TAC [NOT_LESS_EQUAL] THEN METIS_TAC []);
37
38val minv_Lemma2 = Q.store_thm
39("minv_Lemma2",
40 `!x:num. ((0 < x) /\ (x < 65537)) ==> ~(divides 65537 x)`,
41 ARW [] THEN IMP_RES_TAC minv_Lemma1);
42
43val minv_Lemma3 = Q.store_thm
44("minv_Lemma3",
45 `!x:num. ((0 < x) /\ (x < 65537)) ==> ((gcd x 65537) = 1)`,
46 ARW [] THEN ASSUME_TAC prime_axiom THEN IMP_RES_TAC PRIME_GCD THEN
47 `divides 65537 x \/ (gcd 65537 x = 1)` by  METIS_TAC [] THENL
48 [METIS_TAC [minv_Lemma2], METIS_TAC [GCD_SYM]]);
49
50val gcd_Lemma1 = Q.store_thm
51("gcd_Lemma1",
52 `!a b. b <= a ==> (gcd (a-b) b = gcd a b)`,
53 ARW [] THEN `is_gcd (a-b) b (gcd (a-b) b)` by ARW [GCD_IS_GCD] THEN
54 IMP_RES_TAC IS_GCD_MINUS_L THEN
55 `is_gcd a b (gcd a b)` by ARW [GCD_IS_GCD] THEN
56 IMP_RES_TAC IS_GCD_UNIQUE);
57
58val gcd_Lemma2 = Q.store_thm
59("gcd_Lemma2",
60 `!a b. a <= b ==> (gcd a (b-a) = gcd a b)`,
61 ARW [] THEN `is_gcd a (b-a) (gcd a (b-a))` by ARW [GCD_IS_GCD] THEN
62 IMP_RES_TAC IS_GCD_MINUS_R THEN
63 `is_gcd a b (gcd a b)` by ARW [GCD_IS_GCD] THEN
64 IMP_RES_TAC IS_GCD_UNIQUE);
65
66val minv_Lemma4 = Q.store_thm
67("minv_Lemma4",
68 `!r1:num r2:num u1:int u2:int v1:int v2:int. gcd r1 r2 =
69   gcd (FST(dec(r1, r2, u1, u2, v1, v2)))
70       (FST(SND(dec(r1, r2, u1, u2,v1, v2))))`,
71  ARW [dec_def] THENL [METIS_TAC [LESS_IMP_LESS_OR_EQ, gcd_Lemma2],
72  METIS_TAC [NOT_LESS, gcd_Lemma1]]);
73
74val minv_Lemma5 = Q.store_thm
75("minv_Lemma5",
76`!r1 r2 u1 u2 v1 v2.
77   (~((FST (dec (r1,r2,u1,u2,v1,v2)) = 1) \/
78      (FST (SND (dec (r1,r2,u1,u2,v1,v2))) = 1) \/
79      (FST (dec (r1,r2,u1,u2,v1,v2)) = 0) \/
80      (FST (SND (dec (r1,r2,u1,u2,v1,v2))) = 0)))
81  ==> (inv (dec (r1,r2,u1,u2,v1,v2)) = inv (dec (dec (r1,r2,u1,u2,v1,v2))))`,
82  REWRITE_TAC [dec_def] THEN RW_TAC arith_ss [inv_def]);
83
84val minv_Lemma6 = Q.store_thm
85("minv_Lemma6",
86 `!r1:num r2:num u1:int u2:int v1:int v2:int. gcd r1 r2 =
87  gcd (FST(inv(r1, r2, u1, u2, v1, v2)))
88      (FST(SND(inv(r1, r2, u1, u2,v1, v2))))`,
89  FULL_SIMP_TAC arith_ss [inv_def] THEN
90  recInduct inv_ind THEN ARW [] THENL[
91    UNDISCH_TAC ``FST (dec (r1,r2,u1,u2,v1,v2)) = 1`` THEN
92    ARW [dec_def] THEN ARW [inv_def] THEN
93    IMP_RES_TAC NOT_LESS THEN METIS_TAC [gcd_Lemma1],
94    UNDISCH_TAC ``FST (SND (dec (r1,r2,u1,u2,v1,v2))) = 1`` THEN
95    ARW [dec_def] THEN ARW [inv_def] THEN
96    IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN
97    METIS_TAC [gcd_Lemma2],
98    UNDISCH_TAC ``FST (dec (r1,r2,u1,u2,v1,v2)) = 0`` THEN
99    ARW [dec_def] THEN IMP_RES_TAC NOT_LESS THEN
100    IMP_RES_TAC LESS_EQUAL_ANTISYM THEN
101    `r1-r2=0` by DECIDE_TAC THEN
102    `inv (r1 - r2,r2,u1 - u2,u2,v1 - v2,v2) = inv (0,r2,u1 - u2,u2,v1 - v2,v2)`
103     by METIS_TAC [] THEN
104    ARW [inv_def] THEN METIS_TAC [gcd_Lemma1],
105    UNDISCH_TAC ``FST (SND (dec (r1,r2,u1,u2,v1,v2))) = 0`` THEN ARW [dec_def],
106    `inv (dec (r1,r2,u1,u2,v1,v2))=inv (dec (dec (r1,r2,u1,u2,v1,v2)))`
107     by ARW [minv_Lemma5] THEN
108    `gcd (FST (inv (dec (dec (r1,r2,u1,u2,v1,v2)))))
109         (FST (SND (inv (dec (dec (r1,r2,u1,u2,v1,v2)))))) =
110     gcd (FST (inv (dec (r1,r2,u1,u2,v1,v2))))
111         (FST (SND (inv (dec (r1,r2,u1,u2,v1,v2)))))` by METIS_TAC [] THEN
112    `gcd (FST (dec (r1,r2,u1,u2,v1,v2)))
113         (FST (SND (dec (r1,r2,u1,u2,v1,v2)))) =
114     gcd (FST (inv (dec (r1,r2,u1,u2,v1,v2))))
115            (FST (SND (inv (dec (r1,r2,u1,u2,v1,v2)))))` by METIS_TAC [] THEN
116    METIS_TAC [minv_Lemma4]]);
117
118val minv_Lemma7 = Q.store_thm
119("minv_Lemma7",
120 `!x. gcd (ir1 x) (ir2 x) = gcd x 65537`,
121  ARW [ir1_def, ir2_def] THEN ARW [minv_Lemma6]);
122
123val minv_Lemma8 = Q.store_thm
124("minv_Lemma8",
125 `!x. ((0 < x) /\ (x < 65537)) ==> (((ir1 x) = 1) \/ ((ir2 x) = 1))`,
126 ARW [] THEN `gcd (ir1 x) (ir2 x) = 1` by ARW [minv_Lemma7, minv_Lemma3] THEN
127 `((ir1 x) = 1) \/ ((ir1 x) = 0) \/ ((ir2 x) = 1) \/ ((ir2 x) =0)`
128    by ARW [i16_Lemma6] THENL[
129   ARW [],
130   `gcd 0 (ir2 x) = 1` by METIS_TAC [] THEN METIS_TAC [GCD_0L],
131   ARW [],
132   ` gcd (ir1 x) 0 = 1` by METIS_TAC [] THEN
133   METIS_TAC [GCD_0R]]);
134
135val minv_Lemma9 = Q.store_thm
136("minv_Lemma9",
137 `!x. ((0 < x) /\ (x < 65537)) ==>
138   (((int_of_num x) * (iu1 x)) % 65537 = 1) \/
139   (((int_of_num x) * (iu2 x)) % 65537 = 1)`,
140 `~(65537i = 0)`
141      by intLib.ARITH_TAC THEN ARW [] THEN
142 `($& (ir1 x) % 65537 = (iu1 x * $& x) % 65537) /\
143  ($& (ir2 x) % 65537 = (iu2 x * $& x) % 65537)`
144      by RW_TAC arith_ss [i16_Lemma8] THEN
145 `(((ir1 x) = 1) \/ ((ir2 x) = 1))`
146      by ARW [minv_Lemma8] THENL
147 [`$& 1 % 65537 = (iu1 x * $& x) % 65537`
148      by METIS_TAC [] THEN
149  `1 % 65537 = $& (1 MOD 65537)`
150      by METIS_TAC [INT_MOD_CALCULATE] THEN
151  `1n < 65537n`
152      by ARW [] THEN
153  `1 MOD 65537 = 1`
154      by METIS_TAC [LESS_MOD] THEN
155  `1 = (iu1 x * $& x) % 65537`
156      by METIS_TAC [] THEN
157  `$& x * iu1 x = iu1 x * $& x`
158      by RW_TAC arith_ss [INT_MUL_COMM],
159  `$&1 % 65537 = (iu2 x * $& x) % 65537`
160      by METIS_TAC [] THEN
161  `$&1 % 65537 = $& (1 MOD 65537)`
162      by METIS_TAC [INT_MOD_CALCULATE] THEN
163  `1n < 65537n`
164      by ARW [] THEN
165  `1 MOD 65537 = 1`
166      by METIS_TAC [LESS_MOD] THEN
167  `1 = (iu2 x * $& x) % 65537`
168      by METIS_TAC [] THEN
169  `$& x * iu2 x = iu2 x * $& x`
170      by RW_TAC arith_ss [INT_MUL_COMM]] THEN
171   ARW []);
172
173val mode_Lemma1 = Q.store_thm
174("mode_Lemma1",
175 `!a c. (~(c=0) /\ (a % c = 0)) ==> (~a % c = 0)`,
176 ARW [] THEN IMP_RES_TAC INT_MOD_EQ0 THEN
177 `~a = ~(k *c)` by METIS_TAC [] THEN
178 `~a = ~k * c` by METIS_TAC [INT_NEG_LMUL] THEN
179 METIS_TAC [INT_MOD_COMMON_FACTOR]);
180
181val mode_Lemma2 = Q.store_thm
182("mode_Lemma2",
183`!a b c. ~(c=0) ==> ((a * b % c) % c = (a * b) % c)`,
184RW_TAC arith_ss [int_mod] THEN ARW [INT_SUB_LDISTRIB] THEN
185`a * (b / c * c) = a * (b / c) * c` by METIS_TAC [INT_MUL_ASSOC] THEN
186 ARW [] THEN
187`(a * (b / c) * c) % c = 0` by METIS_TAC [INT_MOD_COMMON_FACTOR] THEN
188`(a * b - a * (b / c) * c) / c = a * b / c - a * (b / c) * c / c`
189 by (ARW [INT_SUB_CALCULATE, INT_ADD_DIV] THEN
190     `~(a * (b / c) * c) % c = 0` by METIS_TAC [mode_Lemma1] THEN
191     ARW [INT_ADD_DIV] THEN ARW [INT_NEG_LMUL, INT_DIV_RMUL]) THEN
192ARW [INT_DIV_RMUL] THEN ARW [INT_SUB_RDISTRIB] THEN
193ARW [INT_SUB_CALCULATE] THEN
194`~(a * b / c * c + ~(a * (b / c) * c)) =
195 ~(a * b / c * c) - ( ~(a * (b / c) * c))` by ARW [INT_SUB_LNEG] THEN
196ARW [] THEN ARW [INT_SUB_RNEG] THEN ARW [INT_ADD_ASSOC] THEN
197`a * b + ~(a * (b / c) * c) + ~(a * b / c * c) + a * (b / c) * c =
198 a * b + (~(a * (b / c) * c) + ~(a * b / c * c) + a * (b / c) * c)`
199by METIS_TAC [INT_ADD_ASSOC] THEN ARW [] THEN
200`~(a * (b / c) * c) + ~(a * b / c * c) + a * (b / c) * c =
201 ~(a * (b / c) * c) + (~(a * b / c * c) + a * (b / c) * c)`
202by METIS_TAC [INT_ADD_ASSOC] THEN ARW [] THEN
203`~(a * (b / c) * c) + (~(a * b / c * c) + a * (b / c) * c) =
204(~(a * b / c * c) + a * (b / c) * c) + ~(a * (b / c) * c)`
205by METIS_TAC [INT_ADD_COMM] THEN ARW [] THEN
206`~(a * b / c * c) + a * (b / c) * c + ~(a * (b / c) * c) =
207 ~(a * b / c * c) + (a * (b / c) * c + ~(a * (b / c) * c))`
208by METIS_TAC [INT_ADD_ASSOC] THEN ARW [] THEN
209`a * (b / c) * c + ~(a * (b / c) * c) = 0` by METIS_TAC [INT_ADD_RINV] THEN
210ARW [] THEN
211METIS_TAC [INT_ADD_RID]);
212
213val piu1_def = Define `piu1 x = (iu1 x) % 65537`;
214val piu2_def = Define `piu2 x = (iu2 x) % 65537`;
215
216val minv_Lemma10 = Q.store_thm
217("minv_Lemma10",
218 `!x. ((0 < x) /\ (x < 65537)) ==>
219  (((int_of_num x) * (piu1 x)) % 65537 = 1) \/
220  (((int_of_num x) * (piu2 x)) % 65537 = 1)`,
221 RW_TAC arith_ss [piu1_def, piu2_def] THEN
222 `~(65537i = 0)` by intLib.ARITH_TAC THEN
223 ASSUME_TAC minv_Lemma9 THEN
224 METIS_TAC [mode_Lemma2]);
225
226val minv_def =
227  Define `minv x =
228    if ((int_of_num x) * (piu1 x)) % 65537 = 1
229        then piu1 x
230        else if ((int_of_num x) * (piu2 x)) % 65537 = 1
231          then piu2 x
232          else 0`;
233
234val minv_Theorem = Q.store_thm
235("minv_Theorem",
236 `!x. ((0 < x) /\ (x < 65537)) ==> (((int_of_num x) * (minv x)) % 65537 = 1)`,
237 ARW [minv_def] THEN
238 IMP_RES_TAC minv_Lemma10);
239
240val piu_Lemma1 = Q.store_thm
241("piu_Lemma1",
242 `!x. (0 <= piu1 x) /\ (piu1 x < 65537)`,
243 ASP [piu1_def] THEN
244 `~(65537 < 0)` by intLib.ARITH_TAC THEN
245 `~(65537i = 0)` by intLib.ARITH_TAC THEN
246 STRIP_TAC THEN METIS_TAC [INT_MOD_BOUNDS]);
247
248val piu_Lemma2 = Q.store_thm
249("piu_Lemma2",
250 `!x. (0 <= piu2 x) /\ (piu2 x < 65537)`,
251 ASP [piu2_def] THEN
252 `~(65537 < 0)` by intLib.ARITH_TAC THEN
253 `~(65537i = 0)` by intLib.ARITH_TAC THEN
254 STRIP_TAC THEN METIS_TAC [INT_MOD_BOUNDS]);
255
256val minv_Corollary1 = Q.store_thm
257("minv_Corollary1",
258`!x. ((0 < x) /\ (x < 65537)) ==> ((0 <= (minv x)) /\ ((minv x) < 65537))`,
259 STRIP_TAC THEN STRIP_TAC THEN
260 `((minv x = piu1 x) \/ (minv x = piu2 x))`
261   by METIS_TAC [minv_def, minv_Lemma10]
262 THENL [ARW [piu_Lemma1], ARW [piu_Lemma2]]);
263
264val minv_Corollary2 = Q.store_thm
265("minv_Corollary2",
266 `!x. ((0 < x) /\ (x < 65537)) ==> ~((minv x) = 0)`,
267 `~(65537i = 0)` by intLib.ARITH_TAC THEN
268 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
269 IMP_RES_TAC minv_Theorem THEN
270 `($& x * 0) % 65537 = 1` by METIS_TAC [] THEN
271 `$& x * 0 = 0` by METIS_TAC [INT_MUL_RZERO] THEN
272 `0 % 65537 = 1` by METIS_TAC [] THEN
273 `0 % 65537 = 0` by METIS_TAC [INT_MOD0] THEN
274 `0 = 1` by METIS_TAC [] THEN
275 `~(1n = 0n)` by ARW [] THEN
276 METIS_TAC [INT_INJ]);
277
278val minv_Corollary3 = Q.store_thm
279("minv_Corollary3",
280 `!x. ((0 < x) /\ (x < 65537)) ==> ((0 < (minv x)) /\ ((minv x) < 65537))`,
281 STRIP_TAC THEN STRIP_TAC THEN
282 IMP_RES_TAC minv_Corollary1 THEN
283 IMP_RES_TAC minv_Corollary2 THEN ARW [] THEN
284 `(0 < (minv x)) \/ (0 = (minv x))` by METIS_TAC [INT_LE_LT] THEN
285 `minv x = 0` by METIS_TAC []);
286
287val encode_def = Define `encode x:num = if x = 0n then 65536n else x`;
288val decode_def = Define `decode x:num = if x = 65536n then 0n else x`;
289
290val encode_Lemma1 = Q.store_thm
291("encode_Lemma1",
292 `!x. (x < 65536) ==> ((0 < (encode x)) /\ ((encode x) < 65537))`,
293 ARW [encode_def]);
294
295val encode_Lemma2 = Q.store_thm
296("encode_Lemma2",
297 `!x. (x < 65536) ==>
298   (((int_of_num (encode x)) * (minv (encode x))) % 65537 = 1)`,
299 ARW [encode_Lemma1, minv_Theorem]);
300
301val decode_Lemma1 = Q.store_thm
302("decode_Lemma1",
303 `!x. ((0 < x) /\ (x < 65537)) ==> ((decode x) < 65536)`,
304 ARW [decode_def]);
305
306val decode_Lemma2 = Q.store_thm
307("decode_Lemma2",
308 `!x. ((0 < x) /\ (x < 65537)) ==> ((encode (decode x)) = x)`,
309 ARW [encode_def, decode_def]);
310
311val decode_Lemma3 = Q.store_thm
312("decode_Lemma3",
313 `!x. (x < 65536) ==> ((decode (encode x)) = x)`,
314 ARW [encode_def, decode_def]);
315
316(*---------------------------------------------------------------------------*)
317(* Now phrase in terms of word16                                             *)
318(*---------------------------------------------------------------------------*)
319
320val encode_Lemma3 = Q.store_thm
321("encode_Lemma3",
322 `!w:word16. ((0 < (encode (w2n w))) /\ ((encode (w2n w)) < 65537))`,
323 STRIP_TAC THEN
324 `w2n w < 65536n` by WORD_DECIDE_TAC THEN
325 ARW [encode_Lemma1]);
326
327val wmul_Lemma1 = Q.store_thm
328("wmul_Lemma1",
329 `!w:word16.
330   (int_of_num (encode (w2n w)) * minv (encode (w2n w))) % 65537 = 1`,
331 ARW [] THEN
332 `w2n w < 65536n` by WORD_DECIDE_TAC THEN
333 METIS_TAC [encode_Lemma2]);
334
335val winv_def =
336 Define
337   `winv (w:word16) = n2w (decode (Num (minv (encode (w2n w))))) : word16`;
338
339val wmul_def =
340 Define
341   `wmul (x:word16) (y:word16) =
342      n2w (decode (Num (((int_of_num (encode (w2n x))) *
343                       (int_of_num (encode (w2n y)))) % 65537))) : word16`;
344
345val _ = set_fixity "wmul"  (Infixr 350);
346
347val Num_Lemma1 = Q.store_thm
348("Num_Lemma1",
349 `!x y. ((0 <= x) /\ (0 <= y) /\ (x < y)) ==> ((Num x) < (Num y))`,
350 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
351 `Num y <= Num x` by METIS_TAC [NOT_LESS] THEN
352 `(int_of_num (Num y)) <= (int_of_num (Num x))` by METIS_TAC [INT_LE] THEN
353 IMP_RES_TAC INT_OF_NUM THEN
354 `y <= x` by METIS_TAC [] THEN
355 METIS_TAC [INT_NOT_LT]);
356
357val wmul_Lemma2 = Q.store_thm
358("wmul_Lemma2",
359 `!x. ((0 < x) /\ (x < 65537)) ==>
360      (int_of_num (encode (w2n (n2w (decode (Num x)) : word16))) = x)`,
361 SRW_TAC [] [] THEN
362 `0 <= x` by METIS_TAC [INT_LT_IMP_LE] THEN
363 `0i <= 0i` by ARITH_TAC THEN
364 `0i <= 65537i` by ARITH_TAC THEN
365 `(Num 0) < (Num x)` by METIS_TAC [Num_Lemma1] THEN
366 `(Num x) < (Num 65537)` by METIS_TAC [Num_Lemma1] THEN
367 `Num ($& 0) = 0` by METIS_TAC [NUM_OF_INT] THEN
368 `Num ($& 65537) = 65537` by METIS_TAC [NUM_OF_INT] THEN
369 `0 < Num x` by METIS_TAC [] THEN
370 `Num x < 65537` by METIS_TAC [] THEN
371 `decode (Num x) MOD 65536 = decode (Num x)`
372    by (RES_TAC THEN
373        `decode (Num x) < 65536n` by METIS_TAC [decode_Lemma1] THEN
374        METIS_TAC [LESS_MOD]) THEN
375 ARW [decode_Lemma2, INT_OF_NUM]);
376
377val wmul_Theorem = Q.store_thm
378("wmul_Theorem",
379 `!w:word16. w wmul winv(w) = 1w`,
380 ARW [wmul_def, winv_def] THEN
381 `w2n w < 65536n` by WORD_DECIDE_TAC THEN
382 `(0 < (encode (w2n w))) /\ ((encode (w2n w)) < 65537)`
383    by METIS_TAC [encode_Lemma1] THEN
384 `(0 < (minv (encode (w2n w)))) /\ ((minv (encode (w2n w))) < 65537)`
385    by METIS_TAC [minv_Corollary3] THEN
386 `($& (encode (w2n (n2w (decode (Num (minv (encode (w2n w))))):word16)))) =
387  (minv (encode (w2n w)))`
388    by METIS_TAC [wmul_Lemma2] THEN ARW [] THEN
389 `(($& (encode (w2n w)) * minv (encode (w2n w))) % 65537) = 1`
390    by METIS_TAC [wmul_Lemma1] THEN ARW [] THEN
391 `Num ($& 1) = 1` by METIS_TAC [NUM_OF_INT] THEN ARW [] THEN ARW [decode_def]);
392
393val wmul_Lemma3 = Q.store_thm
394("wmul_Lemma3",
395 `!x:word16. ~(($& (encode (w2n x))) = 0)`,
396 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
397 `encode (w2n x) = 0n` by METIS_TAC [INT_INJ] THEN
398 `w2n x < 65536n` by WORD_DECIDE_TAC THEN
399 `0 < encode (w2n x)` by METIS_TAC [encode_Lemma1] THEN
400 ARW []);
401
402val MOD_EQ0 =
403  SIMP_RULE arith_ss [] (BETA_RULE (Q.SPEC `\x. x=0` MOD_P));
404(* !p q. 0 < q ==> ((p MOD q = 0) = ?k. p = k * q) *)
405
406val wmul_Lemma4 = Q.store_thm
407("wmul_Lemma4",
408 `!x:word16 y:word16.
409     ~((($& (encode (w2n x)) * $& (encode (w2n y))) % 65537) = 0)`,
410 `~(65537i = 0)` by intLib.ARITH_TAC THEN
411 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
412 `($& (encode (w2n x)) * $& (encode (w2n y))) =
413   $&((encode (w2n x)) * (encode (w2n y)))` by METIS_TAC [INT_MUL] THEN
414 `($& (encode (w2n x) * encode (w2n y))) % 65537 = 0` by METIS_TAC [] THEN
415 `$& (encode (w2n x) * encode (w2n y)) % 65537 =
416  $& ((encode (w2n x) * encode (w2n y)) MOD 65537)` by METIS_TAC [INT_MOD] THEN
417 `$& ((encode (w2n x) * encode (w2n y)) MOD 65537) = 0` by METIS_TAC [] THEN
418 `(encode (w2n x) * encode (w2n y)) MOD 65537 = 0` by METIS_TAC [INT_INJ] THEN
419 `0n < 65537n`  by ARW [] THEN
420 IMP_RES_TAC MOD_EQ0 THEN
421 `divides 65537 (encode (w2n x) * encode (w2n y))`
422    by METIS_TAC [divides_def] THEN
423 `((0 < (encode (w2n x))) /\ ((encode (w2n x)) < 65537))`
424    by METIS_TAC [encode_Lemma3] THEN
425 `gcd (encode (w2n x)) 65537 = 1` by METIS_TAC [minv_Lemma3] THEN
426 `divides 65537 (encode (w2n y))` by METIS_TAC [L_EUCLIDES] THEN
427 `((0 < (encode (w2n y))) /\ ((encode (w2n y)) < 65537))`
428    by METIS_TAC [encode_Lemma3] THEN
429 `65537 <= (encode (w2n y))` by METIS_TAC [DIVIDES_LE] THEN
430 ARW [NOT_LESS]);
431
432val wmul_ASSOC = Q.store_thm
433("wmul_ASSOC",
434 `!x:word16 y:word16 z:word16. (x wmul y) wmul z = x wmul (y wmul z)`,
435 ARW [wmul_def] THEN
436 `~(65537 < 0)` by intLib.ARITH_TAC THEN
437 `~(65537i = 0)` by intLib.ARITH_TAC THEN
438 `(0 <= (($& (encode (w2n x)) * $& (encode (w2n y))) % 65537)) /\
439  ((($& (encode (w2n x)) * $& (encode (w2n y))) % 65537) < 65537)`
440    by METIS_TAC [INT_MOD_BOUNDS] THEN
441 `(0 <= (($& (encode (w2n y)) * $& (encode (w2n z))) % 65537)) /\
442  ((($& (encode (w2n y)) * $& (encode (w2n z))) % 65537) < 65537)`
443    by METIS_TAC [INT_MOD_BOUNDS] THEN
444 `~((($& (encode (w2n x)) * $& (encode (w2n y))) % 65537) = 0)`
445    by METIS_TAC [wmul_Lemma4] THEN
446 `~((($& (encode (w2n y)) * $& (encode (w2n z))) % 65537) = 0)`
447    by METIS_TAC [wmul_Lemma4] THEN
448 `0 < (($& (encode (w2n x)) * $& (encode (w2n y))) % 65537)`
449    by METIS_TAC [INT_LE_LT] THEN
450 `0 < (($& (encode (w2n y)) * $& (encode (w2n z))) % 65537)`
451    by METIS_TAC [INT_LE_LT] THEN
452 `($& (encode (w2n (n2w (decode
453    (Num (($& (encode (w2n x)) * $& (encode (w2n y))) % 65537))):word16)))) =
454  (($& (encode (w2n x)) * $& (encode (w2n y))) % 65537)`
455    by METIS_TAC [wmul_Lemma2] THEN
456 ARW [] THEN
457 `($& (encode (w2n (n2w (decode
458    (Num (($& (encode (w2n y)) * $& (encode (w2n z))) % 65537))):word16)))) =
459  (($& (encode (w2n y)) * $& (encode (w2n z))) % 65537)`
460    by METIS_TAC [wmul_Lemma2] THEN
461 ARW [] THEN
462 `(($& (encode (w2n x)) * ($& (encode (w2n y)) *
463    $& (encode (w2n z))) % 65537) % 65537) =
464 (($& (encode (w2n x)) * ($& (encode (w2n y)) * $& (encode (w2n z)))) % 65537)`
465    by METIS_TAC [mode_Lemma2] THEN
466 ARW [] THEN
467 `($& (encode (w2n x)) * $& (encode (w2n y))) % 65537 * $& (encode (w2n z)) =
468   $& (encode (w2n z)) * ($& (encode (w2n x)) * $& (encode (w2n y))) % 65537`
469    by METIS_TAC [INT_MUL_COMM] THEN
470 ARW [] THEN
471 `(($& (encode (w2n z)) * ($& (encode (w2n x)) *
472    $& (encode (w2n y))) % 65537) % 65537) =
473  (($& (encode (w2n z)) * ($& (encode (w2n x)) * $& (encode (w2n y)))) % 65537)`
474    by METIS_TAC [mode_Lemma2] THEN
475 ARW [] THEN
476 METIS_TAC [INT_MUL_COMM, INT_MUL_ASSOC]);
477
478val wmul_Mul1 = Q.store_thm
479("wmul_Mul1",
480 `!w:word16. w wmul 1w = w`,
481 `~(65537i = 0)` by intLib.ARITH_TAC THEN ARW [wmul_def] THEN
482 `($& (encode (w2n w)) * $& (encode (w2n (1w:word16)))) =
483   $&((encode (w2n w)) * (encode (w2n (1w:word16))))`
484 by METIS_TAC [INT_MUL] THEN ARW [] THEN
485 `$& (encode (w2n w) * encode (w2n (1w:word16))) % 65537 =
486  $& ((encode (w2n w) * encode (w2n (1w:word16))) MOD 65537)`
487    by METIS_TAC [INT_MOD] THEN ARW [] THEN
488 ARW [word_1_n2w] THEN
489 `encode 1 = 1` by ARW [encode_def] THEN ARW [] THEN
490 `(encode (w2n w)) < 65537` by METIS_TAC [encode_Lemma3] THEN
491 `(encode (w2n w) MOD 65537) = (encode (w2n w))`
492    by METIS_TAC [LESS_MOD] THEN ARW [NUM_OF_INT] THEN
493 `w2n w < 65536n` by WORD_DECIDE_TAC THEN
494 SRW_TAC [] [decode_Lemma3]);
495
496val () = export_theory();
497