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