1 2open HolKernel Parse boolLib bossLib listTheory rich_listTheory bitTheory 3 markerTheory pairTheory arithmeticTheory numSyntax wordsTheory 4 Serpent_Reference_UtilityTheory wordsLib; 5 6val _ = new_theory "Serpent_Reference_Transformation"; 7 8(*---------------------------------------------------------------------------*) 9(* linear transformation table used in encryption *) 10(*---------------------------------------------------------------------------*) 11 12(*---------------------------------------------------------------------------*) 13(* for efficient evaluation in the place of BOUNDED_FORALL_THM *) 14(*---------------------------------------------------------------------------*) 15 16val row_conv = 17 REPEATC (numLib.BOUNDED_FORALL_CONV EVAL) THENC REWRITE_CONV []; 18 19val LTTable_def = Define 20`LTTable = 21[ 22[16;52;56;70;83;94;105]; 23[72;114;125]; 24[2;9;15;30;76;84;126]; 25[36;90;103]; 26[20;56;60;74;87;98;109]; 27[1;76;118]; 28[2;6;13;19;34;80;88]; 29[40;94;107]; 30[24;60;64;78;91;102;113]; 31[5;80;122]; 32[6;10;17;23;38;84;92]; 33[44;98;111]; 34[28;64;68;82;95;106;117]; 35[9;84;126]; 36[10;14;21;27;42;88;96]; 37[48;102;115]; 38[32;68;72;86;99;110;121]; 39[2;13;88]; 40[14;18;25;31;46;92;100]; 41[52;106;119]; 42[36;72;76;90;103;114;125]; 43[6;17;92]; 44[18;22;29;35;50;96;104]; 45[56;110;123]; 46[1;40;76;80;94;107;118]; 47[10;21;96]; 48[22;26;33;39;54;100;108]; 49[60;114;127]; 50[5;44;80;84;98;111;122]; 51[14;25;100]; 52[26;30;37;43;58;104;112]; 53[3;118]; 54[9;48;84;88;102;115;126]; 55[18;29;104]; 56[30;34;41;47;62;108;116]; 57[7;122]; 58[2;13;52;88;92;106;119]; 59[22;33;108]; 60[34;38;45;51;66;112;120]; 61[11;126]; 62[6;17;56;92;96;110;123]; 63[26;37;112]; 64[38;42;49;55;70;116;124]; 65[2;15;76]; 66[10;21;60;96;100;114;127]; 67[30;41;116]; 68[0;42;46;53;59;74;120]; 69[6;19;80]; 70[3;14;25;100;104;118]; 71[34;45;120]; 72[4;46;50;57;63;78;124]; 73[10;23;84]; 74[7;18;29;104;108;122]; 75[38;49;124]; 76[0;8;50;54;61;67;82]; 77[14;27;88]; 78[11;22;33;108;112;126]; 79[0;42;53]; 80[4;12;54;58;65;71;86]; 81[18;31;92]; 82[2;15;26;37;76;112;116]; 83[4;46;57]; 84[8;16;58;62;69;75;90]; 85[22;35;96]; 86[6;19;30;41;80;116;120]; 87[8;50;61]; 88[12;20;62;66;73;79;94]; 89[26;39;100]; 90[10;23;34;45;84;120;124]; 91[12;54;65]; 92[16;24;66;70;77;83;98]; 93[30;43;104]; 94[0;14;27;38;49;88;124]; 95[16;58;69]; 96[20;28;70;74;81;87;102]; 97[34;47;108]; 98[0;4;18;31;42;53;92]; 99[20;62;73]; 100[24;32;74;78;85;91;106]; 101[38;51;112]; 102[4;8;22;35;46;57;96]; 103[24;66;77]; 104[28;36;78;82;89;95;110]; 105[42;55;116]; 106[8;12;26;39;50;61;100]; 107[28;70;81]; 108[32;40;82;86;93;99;114]; 109[46;59;120]; 110[12;16;30;43;54;65;104]; 111[32;74;85]; 112[36;90;103;118]; 113[50;63;124]; 114[16;20;34;47;58;69;108]; 115[36;78;89]; 116[40;94;107;122]; 117[0;54;67]; 118[20;24;38;51;62;73;112]; 119[40;82;93]; 120[44;98;111;126]; 121[4;58;71]; 122[24;28;42;55;66;77;116]; 123[44;86;97]; 124[2;48;102;115]; 125[8;62;75]; 126[28;32;46;59;70;81;120]; 127[48;90;101]; 128[6;52;106;119]; 129[12;66;79]; 130[32;36;50;63;74;85;124]; 131[52;94;105]; 132[10;56;110;123]; 133[16;70;83]; 134[0;36;40;54;67;78;89]; 135[56;98;109]; 136[14;60;114;127]; 137[20;74;87]; 138[4;40;44;58;71;82;93]; 139[60;102;113]; 140[3;18;72;114;118;125]; 141[24;78;91]; 142[8;44;48;62;75;86;97]; 143[64;106;117]; 144[1;7;22;76;118;122]; 145[28;82;95]; 146[12;48;52;66;79;90;101]; 147[68;110;121]; 148[5;11;26;80;122;126]; 149[32;86;99] 150]`; 151 152(* linear transformation table used in decryption *) 153 154val InvLTTable_def = Define 155`InvLTTable = 156[ 157[53;55;72]; 158[1;5;20;90]; 159[15;102]; 160[3;31;90]; 161[57;59;76]; 162[5;9;24;94]; 163[19;106]; 164[7;35;94]; 165[61;63;80]; 166[9;13;28;98]; 167[23;110]; 168[11;39;98]; 169[65;67;84]; 170[13;17;32;102]; 171[27;114]; 172[1;3;15;20;43;102]; 173[69;71;88]; 174[17;21;36;106]; 175[1;31;118]; 176[5;7;19;24;47;106]; 177[73;75;92]; 178[21;25;40;110]; 179[5;35;122]; 180[9;11;23;28;51;110]; 181[77;79;96]; 182[25;29;44;114]; 183[9;39;126]; 184[13;15;27;32;55;114]; 185[81;83;100]; 186[1;29;33;48;118]; 187[2;13;43]; 188[1;17;19;31;36;59;118]; 189[85;87;104]; 190[5;33;37;52;122]; 191[6;17;47]; 192[5;21;23;35;40;63;122]; 193[89;91;108]; 194[9;37;41;56;126]; 195[10;21;51]; 196[9;25;27;39;44;67;126]; 197[93;95;112]; 198[2;13;41;45;60]; 199[14;25;55]; 200[2;13;29;31;43;48;71]; 201[97;99;116]; 202[6;17;45;49;64]; 203[18;29;59]; 204[6;17;33;35;47;52;75]; 205[101;103;120]; 206[10;21;49;53;68]; 207[22;33;63]; 208[10;21;37;39;51;56;79]; 209[105;107;124]; 210[14;25;53;57;72]; 211[26;37;67]; 212[14;25;41;43;55;60;83]; 213[0;109;111]; 214[18;29;57;61;76]; 215[30;41;71]; 216[18;29;45;47;59;64;87]; 217[4;113;115]; 218[22;33;61;65;80]; 219[34;45;75]; 220[22;33;49;51;63;68;91]; 221[8;117;119]; 222[26;37;65;69;84]; 223[38;49;79]; 224[26;37;53;55;67;72;95]; 225[12;121;123]; 226[30;41;69;73;88]; 227[42;53;83]; 228[30;41;57;59;71;76;99]; 229[16;125;127]; 230[34;45;73;77;92]; 231[46;57;87]; 232[34;45;61;63;75;80;103]; 233[1;3;20]; 234[38;49;77;81;96]; 235[50;61;91]; 236[38;49;65;67;79;84;107]; 237[5;7;24]; 238[42;53;81;85;100]; 239[54;65;95]; 240[42;53;69;71;83;88;111]; 241[9;11;28]; 242[46;57;85;89;104]; 243[58;69;99]; 244[46;57;73;75;87;92;115]; 245[13;15;32]; 246[50;61;89;93;108]; 247[62;73;103]; 248[50;61;77;79;91;96;119]; 249[17;19;36]; 250[54;65;93;97;112]; 251[66;77;107]; 252[54;65;81;83;95;100;123]; 253[21;23;40]; 254[58;69;97;101;116]; 255[70;81;111]; 256[58;69;85;87;99;104;127]; 257[25;27;44]; 258[62;73;101;105;120]; 259[74;85;115]; 260[3;62;73;89;91;103;108]; 261[29;31;48]; 262[66;77;105;109;124]; 263[78;89;119]; 264[7;66;77;93;95;107;112]; 265[33;35;52]; 266[0;70;81;109;113]; 267[82;93;123]; 268[11;70;81;97;99;111;116]; 269[37;39;56]; 270[4;74;85;113;117]; 271[86;97;127]; 272[15;74;85;101;103;115;120]; 273[41;43;60]; 274[8;78;89;117;121]; 275[3;90]; 276[19;78;89;105;107;119;124]; 277[45;47;64]; 278[12;82;93;121;125]; 279[7;94]; 280[0;23;82;93;109;111;123]; 281[49;51;68]; 282[1;16;86;97;125]; 283[11;98]; 284[4;27;86;97;113;115;127] 285]`; 286 287val LTFun_def = Define `LTFun x = EL x LTTable`; 288 289val invLTFun_def = Define `invLTFun x = EL x InvLTTable`; 290 291val LTFunVal = Q.store_thm( 292"LTFunVal", 293` 294(LTFun 0 = [ 16;52;56;70;83;94;105]) /\ 295(LTFun 1 = [ 72;114;125]) /\ 296(LTFun 2 = [ 2;9;15;30;76;84;126]) /\ 297(LTFun 3 = [ 36;90;103]) /\ 298(LTFun 4 = [ 20;56;60;74;87;98;109]) /\ 299(LTFun 5 = [ 1;76;118]) /\ 300(LTFun 6 = [ 2;6;13;19;34;80;88]) /\ 301(LTFun 7 = [ 40;94;107]) /\ 302(LTFun 8 = [ 24;60;64;78;91;102;113]) /\ 303(LTFun 9 = [ 5;80;122]) /\ 304(LTFun 10 = [ 6;10;17;23;38;84;92]) /\ 305(LTFun 11 = [ 44;98;111]) /\ 306(LTFun 12 = [ 28;64;68;82;95;106;117]) /\ 307(LTFun 13 = [ 9;84;126]) /\ 308(LTFun 14 = [ 10;14;21;27;42;88;96]) /\ 309(LTFun 15 = [ 48;102;115]) /\ 310(LTFun 16 = [ 32;68;72;86;99;110;121]) /\ 311(LTFun 17 = [ 2;13;88]) /\ 312(LTFun 18 = [ 14;18;25;31;46;92;100]) /\ 313(LTFun 19 = [ 52;106;119]) /\ 314(LTFun 20 = [ 36;72;76;90;103;114;125]) /\ 315(LTFun 21 = [ 6;17;92]) /\ 316(LTFun 22 = [ 18;22;29;35;50;96;104]) /\ 317(LTFun 23 = [ 56;110;123]) /\ 318(LTFun 24 = [ 1;40;76;80;94;107;118]) /\ 319(LTFun 25 = [ 10;21;96]) /\ 320(LTFun 26 = [ 22;26;33;39;54;100;108]) /\ 321(LTFun 27 = [ 60;114;127]) /\ 322(LTFun 28 = [ 5;44;80;84;98;111;122]) /\ 323(LTFun 29 = [ 14;25;100]) /\ 324(LTFun 30 = [ 26;30;37;43;58;104;112]) /\ 325(LTFun 31 = [ 3;118]) /\ 326(LTFun 32 = [ 9;48;84;88;102;115;126]) /\ 327(LTFun 33 = [ 18;29;104]) /\ 328(LTFun 34 = [ 30;34;41;47;62;108;116]) /\ 329(LTFun 35 = [ 7;122]) /\ 330(LTFun 36 = [ 2;13;52;88;92;106;119]) /\ 331(LTFun 37 = [ 22;33;108]) /\ 332(LTFun 38 = [ 34;38;45;51;66;112;120]) /\ 333(LTFun 39 = [ 11;126]) /\ 334(LTFun 40 = [ 6;17;56;92;96;110;123]) /\ 335(LTFun 41 = [ 26;37;112]) /\ 336(LTFun 42 = [ 38;42;49;55;70;116;124]) /\ 337(LTFun 43 = [ 2;15;76]) /\ 338(LTFun 44 = [ 10;21;60;96;100;114;127]) /\ 339(LTFun 45 = [ 30;41;116]) /\ 340(LTFun 46 = [ 0;42;46;53;59;74;120]) /\ 341(LTFun 47 = [ 6;19;80]) /\ 342(LTFun 48 = [ 3;14;25;100;104;118]) /\ 343(LTFun 49 = [ 34;45;120]) /\ 344(LTFun 50 = [ 4;46;50;57;63;78;124]) /\ 345(LTFun 51 = [ 10;23;84]) /\ 346(LTFun 52 = [ 7;18;29;104;108;122]) /\ 347(LTFun 53 = [ 38;49;124]) /\ 348(LTFun 54 = [ 0;8;50;54;61;67;82]) /\ 349(LTFun 55 = [ 14;27;88]) /\ 350(LTFun 56 = [ 11;22;33;108;112;126]) /\ 351(LTFun 57 = [ 0;42;53]) /\ 352(LTFun 58 = [ 4;12;54;58;65;71;86]) /\ 353(LTFun 59 = [ 18;31;92]) /\ 354(LTFun 60 = [ 2;15;26;37;76;112;116]) /\ 355(LTFun 61 = [ 4;46;57]) /\ 356(LTFun 62 = [ 8;16;58;62;69;75;90]) /\ 357(LTFun 63 = [ 22;35;96]) /\ 358(LTFun 64 = [ 6;19;30;41;80;116;120]) /\ 359(LTFun 65 = [ 8;50;61]) /\ 360(LTFun 66 = [ 12;20;62;66;73;79;94]) /\ 361(LTFun 67 = [ 26;39;100]) /\ 362(LTFun 68 = [ 10;23;34;45;84;120;124]) /\ 363(LTFun 69 = [ 12;54;65]) /\ 364(LTFun 70 = [ 16;24;66;70;77;83;98]) /\ 365(LTFun 71 = [ 30;43;104]) /\ 366(LTFun 72 = [ 0;14;27;38;49;88;124]) /\ 367(LTFun 73 = [ 16;58;69]) /\ 368(LTFun 74 = [ 20;28;70;74;81;87;102]) /\ 369(LTFun 75 = [ 34;47;108]) /\ 370(LTFun 76 = [ 0;4;18;31;42;53;92]) /\ 371(LTFun 77 = [ 20;62;73]) /\ 372(LTFun 78 = [ 24;32;74;78;85;91;106]) /\ 373(LTFun 79 = [ 38;51;112]) /\ 374(LTFun 80 = [ 4;8;22;35;46;57;96]) /\ 375(LTFun 81 = [ 24;66;77]) /\ 376(LTFun 82 = [ 28;36;78;82;89;95;110]) /\ 377(LTFun 83 = [ 42;55;116]) /\ 378(LTFun 84 = [ 8;12;26;39;50;61;100]) /\ 379(LTFun 85 = [ 28;70;81]) /\ 380(LTFun 86 = [ 32;40;82;86;93;99;114]) /\ 381(LTFun 87 = [ 46;59;120]) /\ 382(LTFun 88 = [ 12;16;30;43;54;65;104]) /\ 383(LTFun 89 = [ 32;74;85]) /\ 384(LTFun 90 = [ 36;90;103;118]) /\ 385(LTFun 91 = [ 50;63;124]) /\ 386(LTFun 92 = [ 16;20;34;47;58;69;108]) /\ 387(LTFun 93 = [ 36;78;89]) /\ 388(LTFun 94 = [ 40;94;107;122]) /\ 389(LTFun 95 = [ 0;54;67]) /\ 390(LTFun 96 = [ 20;24;38;51;62;73;112]) /\ 391(LTFun 97 = [ 40;82;93]) /\ 392(LTFun 98 = [ 44;98;111;126]) /\ 393(LTFun 99 = [ 4;58;71]) /\ 394(LTFun 100 = [ 24;28;42;55;66;77;116]) /\ 395(LTFun 101 = [ 44;86;97]) /\ 396(LTFun 102 = [ 2;48;102;115]) /\ 397(LTFun 103 = [ 8;62;75]) /\ 398(LTFun 104 = [ 28;32;46;59;70;81;120]) /\ 399(LTFun 105 = [ 48;90;101]) /\ 400(LTFun 106 = [ 6;52;106;119]) /\ 401(LTFun 107 = [ 12;66;79]) /\ 402(LTFun 108 = [ 32;36;50;63;74;85;124]) /\ 403(LTFun 109 = [ 52;94;105]) /\ 404(LTFun 110 = [ 10;56;110;123]) /\ 405(LTFun 111 = [ 16;70;83]) /\ 406(LTFun 112 = [ 0;36;40;54;67;78;89]) /\ 407(LTFun 113 = [ 56;98;109]) /\ 408(LTFun 114 = [ 14;60;114;127]) /\ 409(LTFun 115 = [ 20;74;87]) /\ 410(LTFun 116 = [ 4;40;44;58;71;82;93]) /\ 411(LTFun 117 = [ 60;102;113]) /\ 412(LTFun 118 = [ 3;18;72;114;118;125]) /\ 413(LTFun 119 = [ 24;78;91]) /\ 414(LTFun 120 = [ 8;44;48;62;75;86;97]) /\ 415(LTFun 121 = [ 64;106;117]) /\ 416(LTFun 122 = [ 1;7;22;76;118;122]) /\ 417(LTFun 123 = [ 28;82;95]) /\ 418(LTFun 124 = [ 12;48;52;66;79;90;101]) /\ 419(LTFun 125 = [ 68;110;121]) /\ 420(LTFun 126 = [ 5;11;26;80;122;126]) /\ 421(LTFun 127 = [ 32;86;99])`, 422REPEAT STRIP_TAC THEN EVAL_TAC); 423 424(* linear transformation table used in decryption *) 425 426val invLTFunVal = Q.store_thm( 427"invLTFunVal", 428` 429(invLTFun 0 = [53;55;72]) /\ 430(invLTFun 1 = [1;5;20;90]) /\ 431(invLTFun 2 = [15;102]) /\ 432(invLTFun 3 = [3;31;90]) /\ 433(invLTFun 4 = [57;59;76]) /\ 434(invLTFun 5 = [5;9;24;94]) /\ 435(invLTFun 6 = [19;106]) /\ 436(invLTFun 7 = [7;35;94]) /\ 437(invLTFun 8 = [61;63;80]) /\ 438(invLTFun 9 = [9;13;28;98]) /\ 439(invLTFun 10 = [23;110]) /\ 440(invLTFun 11 = [11;39;98]) /\ 441(invLTFun 12 = [65;67;84]) /\ 442(invLTFun 13 = [13;17;32;102]) /\ 443(invLTFun 14 = [27;114]) /\ 444(invLTFun 15 = [1;3;15;20;43;102]) /\ 445(invLTFun 16 = [69;71;88]) /\ 446(invLTFun 17 = [17;21;36;106]) /\ 447(invLTFun 18 = [1;31;118]) /\ 448(invLTFun 19 = [5;7;19;24;47;106]) /\ 449(invLTFun 20 = [73;75;92]) /\ 450(invLTFun 21 = [21;25;40;110]) /\ 451(invLTFun 22 = [5;35;122]) /\ 452(invLTFun 23 = [9;11;23;28;51;110]) /\ 453(invLTFun 24 = [77;79;96]) /\ 454(invLTFun 25 = [25;29;44;114]) /\ 455(invLTFun 26 = [9;39;126]) /\ 456(invLTFun 27 = [13;15;27;32;55;114]) /\ 457(invLTFun 28 = [81;83;100]) /\ 458(invLTFun 29 = [1;29;33;48;118]) /\ 459(invLTFun 30 = [2;13;43]) /\ 460(invLTFun 31 = [1;17;19;31;36;59;118]) /\ 461(invLTFun 32 = [85;87;104]) /\ 462(invLTFun 33 = [5;33;37;52;122]) /\ 463(invLTFun 34 = [6;17;47]) /\ 464(invLTFun 35 = [5;21;23;35;40;63;122]) /\ 465(invLTFun 36 = [89;91;108]) /\ 466(invLTFun 37 = [9;37;41;56;126]) /\ 467(invLTFun 38 = [10;21;51]) /\ 468(invLTFun 39 = [9;25;27;39;44;67;126]) /\ 469(invLTFun 40 = [93;95;112]) /\ 470(invLTFun 41 = [2;13;41;45;60]) /\ 471(invLTFun 42 = [14;25;55]) /\ 472(invLTFun 43 = [2;13;29;31;43;48;71]) /\ 473(invLTFun 44 = [97;99;116]) /\ 474(invLTFun 45 = [6;17;45;49;64]) /\ 475(invLTFun 46 = [18;29;59]) /\ 476(invLTFun 47 = [6;17;33;35;47;52;75]) /\ 477(invLTFun 48 = [101;103;120]) /\ 478(invLTFun 49 = [10;21;49;53;68]) /\ 479(invLTFun 50 = [22;33;63]) /\ 480(invLTFun 51 = [10;21;37;39;51;56;79]) /\ 481(invLTFun 52 = [105;107;124]) /\ 482(invLTFun 53 = [14;25;53;57;72]) /\ 483(invLTFun 54 = [26;37;67]) /\ 484(invLTFun 55 = [14;25;41;43;55;60;83]) /\ 485(invLTFun 56 = [0;109;111]) /\ 486(invLTFun 57 = [18;29;57;61;76]) /\ 487(invLTFun 58 = [30;41;71]) /\ 488(invLTFun 59 = [18;29;45;47;59;64;87]) /\ 489(invLTFun 60 = [4;113;115]) /\ 490(invLTFun 61 = [22;33;61;65;80]) /\ 491(invLTFun 62 = [34;45;75]) /\ 492(invLTFun 63 = [22;33;49;51;63;68;91]) /\ 493(invLTFun 64 = [8;117;119]) /\ 494(invLTFun 65 = [26;37;65;69;84]) /\ 495(invLTFun 66 = [38;49;79]) /\ 496(invLTFun 67 = [26;37;53;55;67;72;95]) /\ 497(invLTFun 68 = [12;121;123]) /\ 498(invLTFun 69 = [30;41;69;73;88]) /\ 499(invLTFun 70 = [42;53;83]) /\ 500(invLTFun 71 = [30;41;57;59;71;76;99]) /\ 501(invLTFun 72 = [16;125;127]) /\ 502(invLTFun 73 = [34;45;73;77;92]) /\ 503(invLTFun 74 = [46;57;87]) /\ 504(invLTFun 75 = [34;45;61;63;75;80;103]) /\ 505(invLTFun 76 = [1;3;20]) /\ 506(invLTFun 77 = [38;49;77;81;96]) /\ 507(invLTFun 78 = [50;61;91]) /\ 508(invLTFun 79 = [38;49;65;67;79;84;107]) /\ 509(invLTFun 80 = [5;7;24]) /\ 510(invLTFun 81 = [42;53;81;85;100]) /\ 511(invLTFun 82 = [54;65;95]) /\ 512(invLTFun 83 = [42;53;69;71;83;88;111]) /\ 513(invLTFun 84 = [9;11;28]) /\ 514(invLTFun 85 = [46;57;85;89;104]) /\ 515(invLTFun 86 = [58;69;99]) /\ 516(invLTFun 87 = [46;57;73;75;87;92;115]) /\ 517(invLTFun 88 = [13;15;32]) /\ 518(invLTFun 89 = [50;61;89;93;108]) /\ 519(invLTFun 90 = [62;73;103]) /\ 520(invLTFun 91 = [50;61;77;79;91;96;119]) /\ 521(invLTFun 92 = [17;19;36]) /\ 522(invLTFun 93 = [54;65;93;97;112]) /\ 523(invLTFun 94 = [66;77;107]) /\ 524(invLTFun 95 = [54;65;81;83;95;100;123]) /\ 525(invLTFun 96 = [21;23;40]) /\ 526(invLTFun 97 = [58;69;97;101;116]) /\ 527(invLTFun 98 = [70;81;111]) /\ 528(invLTFun 99 = [58;69;85;87;99;104;127]) /\ 529(invLTFun 100 = [25;27;44]) /\ 530(invLTFun 101 = [62;73;101;105;120]) /\ 531(invLTFun 102 = [74;85;115]) /\ 532(invLTFun 103 = [3;62;73;89;91;103;108]) /\ 533(invLTFun 104 = [29;31;48]) /\ 534(invLTFun 105 = [66;77;105;109;124]) /\ 535(invLTFun 106 = [78;89;119]) /\ 536(invLTFun 107 = [7;66;77;93;95;107;112]) /\ 537(invLTFun 108 = [33;35;52]) /\ 538(invLTFun 109 = [0;70;81;109;113]) /\ 539(invLTFun 110 = [82;93;123]) /\ 540(invLTFun 111 = [11;70;81;97;99;111;116]) /\ 541(invLTFun 112 = [37;39;56]) /\ 542(invLTFun 113 = [4;74;85;113;117]) /\ 543(invLTFun 114 = [86;97;127]) /\ 544(invLTFun 115 = [15;74;85;101;103;115;120]) /\ 545(invLTFun 116 = [41;43;60]) /\ 546(invLTFun 117 = [8;78;89;117;121]) /\ 547(invLTFun 118 = [3;90]) /\ 548(invLTFun 119 = [19;78;89;105;107;119;124]) /\ 549(invLTFun 120 = [45;47;64]) /\ 550(invLTFun 121 = [12;82;93;121;125]) /\ 551(invLTFun 122 = [7;94]) /\ 552(invLTFun 123 = [0;23;82;93;109;111;123]) /\ 553(invLTFun 124 = [49;51;68]) /\ 554(invLTFun 125 = [1;16;86;97;125]) /\ 555(invLTFun 126 = [11;98]) /\ 556(invLTFun 127 = [4;27;86;97;113;115;127])`, 557REPEAT STRIP_TAC THEN EVAL_TAC); 558 559 560(* compute the parity on select bits *) 561 562val selParity_def = Define 563`(selParity (w:word128) [] = F) /\ 564 (selParity w (pos::t) = boolXor (w ' pos) (selParity w t))`; 565 566val selParityAppend = Q.store_thm( 567 "selParityAppend", 568 `!w l1 l2. selParity w (l1++l2) = boolXor (selParity w l1) (selParity w l2)`, 569 Induct_on `l1` THEN 570 RW_TAC list_ss [selParity_def] THEN 571 METIS_TAC [boolXorFacts,boolXorComm,boolXorAssoc,selParity_def]); 572 573(*linear transform*) 574 575val transform_def = Define 576`(transform transFun 0 (w:word128) 577 = let newBit = selParity w (transFun 0) 578 in 579 if newBit 580 then (1w:word128) 581 else (0w:word128)) 582 /\ 583 (transform transFun (SUC i) w 584 = let newBit = selParity w (transFun (SUC i)) 585 in 586 let newWord = if newBit 587 then ((1w:word128)<<(SUC i)) 588 else (0w:word128) 589 in 590 newWord || transform transFun i w)`; 591 592val transformEval = Q.store_thm( 593 "transformEval", 594 `!n transFun (w:word128). 595 transform transFun n w = 596 if n = 0 597 then let newBit = selParity w (transFun 0) 598 in 599 if newBit 600 then (1w:word128) 601 else (0w:word128) 602 else let newBit = selParity w (transFun n) 603 in 604 let newWord = if newBit 605 then ((1w:word128)<<n) 606 else (0w:word128) 607 in 608 newWord || transform transFun (n-1) w`, 609 RW_TAC std_ss [transform_def,LET_THM] THEN 610 (Cases_on `n` THENL [ 611 METIS_TAC [], 612 FULL_SIMP_TAC arith_ss [transform_def,LET_THM]])); 613 614val LT_def = Define `LT w = transform LTFun 127 w`; 615 616val invLT_def = Define `invLT w = transform invLTFun 127 w`; 617 618(*desired properties of transform*) 619 620val transform_inv1_w128 = Q.store_thm( 621 "transform_inv1_w128", 622 `!to d w transFun. 623 to < 128 /\ 624 d < 128 /\ 625 to > d 626 ==> 627 ~((transform transFun d w) ' to)`, 628 Induct_on `d` THEN 629 SRW_TAC [WORD_BIT_EQ_ss,BIT_ss] [n2w_def,transform_def,LET_THM]); 630 631val transform_inv2_w128 = Q.store_thm( 632 "transform_inv2_w128", 633 `!to d w transFun. 634 to < 128 /\ 635 d < 128 /\ 636 to <= d 637 ==> 638 ((transform transFun d w) ' to = selParity w (transFun to))`, 639 Induct_on `d` THEN 640 SRW_TAC [WORD_BIT_EQ_ss] [transform_def,LET_THM] THEN 641 `d < 128` by DECIDE_TAC THEN 642 Cases_on `to <= d` THEN 643 ASM_SIMP_TAC arith_ss [] THEN 644 `to = SUC d` by DECIDE_TAC THEN 645 SRW_TAC [WORD_BIT_EQ_ss,BIT_ss] [n2w_def,transform_inv1_w128]); 646 647(* the composite of two linear transformations *) 648 649val transCompose_def = Define `transCompose f1 f2 = \x. FLAT (MAP f1 (f2 x))`; 650 651(* a transform function is legal *) 652 653val transInRange_def = Define 654 `transInRange transFun = 655 !i. i < 128 ==> ALL_EL (\x. x < 128) (transFun i)`; 656 657val LTFunInRange = Q.store_thm( 658 "LTFunInRange", 659 `transInRange LTFun`, 660 SIMP_TAC std_ss [transInRange_def] THEN CONV_TAC (time row_conv)); 661 662val invLTFunInRange = Q.store_thm( 663 "invLTFunInRange", 664 `transInRange invLTFun`, 665 SIMP_TAC std_ss [transInRange_def] THEN CONV_TAC (time row_conv)); 666 667(* desired properties of composite of linear transformations *) 668 669val transformComposeLemma = Q.store_thm( 670 "transformComposeLemma", 671 `!transFun1 transL2 w. 672 transInRange transFun1 /\ 673 ALL_EL (\x. x < 128) transL2 674 ==> 675 (selParity (transform transFun1 127 w) transL2 676 = selParity w (FLAT (MAP transFun1 transL2)))`, 677 Induct_on `transL2` THEN 678 FULL_SIMP_TAC list_ss 679 [MAP,FLAT,selParity_def,transform_def,selParityAppend,transform_inv2_w128]); 680 681val transformComposeBit = Q.store_thm( 682 "transformComposeBit", 683 `!i transFun1 transFun2 w. 684 i < 128 /\ 685 transInRange transFun1 /\ 686 transInRange transFun2 687 ==> 688 ((transform transFun2 127 (transform transFun1 127 w)) ' i = 689 (transform (transCompose transFun1 transFun2) 127 w) ' i)`, 690 RW_TAC arith_ss [transCompose_def,transInRange_def,transform_inv2_w128, 691 transformComposeLemma]); 692 693val transformComposeWord = Q.store_thm( 694 "transformComposeWord", 695 `!transFun1 transFun2 w. 696 transInRange transFun1 /\ 697 transInRange transFun2 698 ==> 699 (transform transFun2 127 (transform transFun1 127 w) = 700 transform (transCompose transFun1 transFun2) 127 w)`, 701 SRW_TAC [WORD_BIT_EQ_ss] [transformComposeBit]); 702 703val TL128_eq_makeTL128 = save_thm( 704 "TL128_eq_makeTL128", SYM (EVAL ``makeTL 128``)); 705 706(* the intermediate values of the composite of the two given linear 707 transformation functions, used to speed up the verification *) 708 709val Res_def = Define `Res i = FLAT (MAP LTFun (invLTFun i))`; 710 711(*load "numSyntax"; 712quietdec := true; 713open numSyntax; 714quietdec := false;*) 715 716val ResTable = 717 LIST_CONJ (map EVAL (map (fn i => ``Res ^(term_of_int i)``) (upto 0 127))); 718 719val _ = computeLib.add_thms [ResTable] computeLib.the_compset; 720 721(* parity check is the same as counting EVEN or ODD. 722 countEvenL and countEven is the two equivalent description, 723 while countEvenL reduce a layer of loop *) 724 725val countL_def = Define 726`(countL l []= l) /\ 727 (countL l (h::t) = let x = makeL h 728 in 729 let tmp = zipXor x l 730 in 731 countL tmp t)`; 732 733val countEvenL_def = Define` 734 countEvenL tl = 735 countL 736 [T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; 737 T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; 738 T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; 739 T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; 740 T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; 741 T; T; T; T; T; T; T; T; T; T; T; T; T] tl`; 742 743val countEvenL_LT_facts = Q.store_thm( 744 "countEvenL_LT_facts", 745 `!i. 746 i < 128 747 ==> 748 (countEvenL (Res i) = countEvenL [i]) `, 749 SIMP_TAC std_ss [] THEN CONV_TAC (time row_conv) THEN REWRITE_TAC []); 750 751val countEven_def = Define` 752 (countEven x [] = T) /\ 753 (countEven x (h::t) = boolXor (x = h) (countEven x t))`; 754 755val countL_fact = Q.store_thm( 756 "countL_fact", 757 `!i al h tl. 758 i < LENGTH al /\ 759 h < LENGTH al /\ 760 ALL_EL (\x. x < LENGTH al) tl 761 ==> 762 (EL i (countL (zipXor (makeL h) al) tl) = 763 boolXor (i = h) (EL i (countL al tl)))`, 764 Induct_on `tl` THEN 765 RW_TAC list_ss [countL_def,LET_THM,zipXor_makeL, 766 zipXor_makeL_COMM,LENGTH_zipXor,boolXorComm3]); 767 768val Res_fact = Q.store_thm( 769 "Res_fact", 770 `!i. 771 i < 128 772 ==> 773 ALL_EL (\x. x < 128) (Res i)`, 774 SIMP_TAC std_ss [] THEN CONV_TAC (time row_conv)); 775 776(* equivalence between countEven and countEvenL *) 777 778val countEvenL_countEven_eq = Q.store_thm( 779 "countEvenL_countEven_eq", 780 `!i tl. 781 i < 128 /\ 782 ALL_EL (\x. x < 128) tl 783 ==> 784 (EL i (countEvenL tl) = countEven i tl)`, 785 SIMP_TAC std_ss [] THEN 786 Induct_on `tl` THENL [ 787 FULL_SIMP_TAC arith_ss [countEvenL_def,countEven_def,countL_def, 788 TL128_eq_makeTL128,makeTL_fact], 789 790 FULL_SIMP_TAC std_ss [ALL_EL,countEvenL_def,countEven_def,countL_def, 791 LET_THM,TL128_eq_makeTL128,makeTL_fact, 792 zipXor_makeL_COMM,LENGTH_zipXor,boolXorComm3, 793 LENGTH_makeTL] THEN 794 FULL_SIMP_TAC std_ss [countEven_def,countL_fact,countEvenL_def, 795 TL128_eq_makeTL128,LENGTH_makeTL]]); 796 797val LTFun_invLTFun_fact = Q.store_thm( 798 "LTFun_invLTFun_fact", 799 `!i. 800 i < 128 801 ==> 802 !j. 803 j < 128 804 ==> 805 (countEven j ((transCompose LTFun invLTFun) i) 806 = countEven j [i])`, 807 RW_TAC std_ss [GSYM Res_def, transCompose_def, GSYM countEvenL_countEven_eq, 808 countEvenL_LT_facts,Res_fact,ALL_EL]); 809 810(* desired properties of countEven *) 811 812val countEven_filter1 = Q.store_thm( 813 "countEven_filter1", 814 `!i L d transL. 815 LENGTH transL <= L /\ 816 i < d+1 /\ 817 ALL_EL (\x. x < d+1) transL 818 819 ==> 820 countEven i (FILTER (\x. ~(x = i)) transL)`, 821 Induct_on `L` THEN 822 RW_TAC arith_ss [countEven_def,ALL_EL,LENGTH_NIL,FILTER] THEN 823 Cases_on `transL` THEN 824 RW_TAC arith_ss [countEven_def,ALL_EL,LENGTH_NIL,FILTER] THEN 825 FULL_SIMP_TAC list_ss [boolXor_def] THEN 826 METIS_TAC []); 827 828 829val countEven_filter2 = Q.store_thm( 830 "countEven_filter2", 831 `!i k L d transL. 832 LENGTH transL <= L /\ 833 i < d+1 /\ 834 k < d+1 /\ 835 ALL_EL (\x. x < d+1) transL 836 ==> 837 (countEven k (FILTER (\x. ~(x = i)) transL) 838 = if k = i 839 then T 840 else countEven k transL)`, 841 Induct_on `L` THEN 842 RW_TAC arith_ss [countEven_def,ALL_EL,LENGTH_NIL,FILTER] THEN 843 Cases_on `transL` THEN 844 FULL_SIMP_TAC list_ss [countEven_def,ALL_EL,LENGTH_NIL,FILTER]THEN 845 Cases_on `k = i` THEN Cases_on `h = i` THEN 846 RW_TAC std_ss [boolXor_def,countEven_def] THEN 847 METIS_TAC []); 848 849val countEven_filter3 = Q.store_thm( 850 "countEven_filter3", 851 `!i k L d transL1 transL2. 852 LENGTH transL1 <= L /\ 853 LENGTH transL2 <= L /\ 854 (!j. j < d+1 ==> (countEven j transL1 = countEven j transL2)) /\ 855 i < d+1 /\ 856 k < d+1 /\ 857 ALL_EL (\x. x < d+1) transL1 /\ 858 ALL_EL (\x. x < d+1) transL2 859 ==> 860 (countEven k (FILTER (\x. ~(x = i)) transL1) = 861 countEven k (FILTER (\x. ~(x = i)) transL2))`, 862 RW_TAC std_ss [] THEN METIS_TAC [countEven_filter2]); 863 864(* desired properties of selParity *) 865 866val selParity_filter = Q.store_thm( 867 "selParity_filter", 868 `!i transL w. 869 i < 128 /\ 870 ALL_EL (\x. x < 128) transL 871 ==> 872 (selParity w transL 873 = if countEven i transL 874 then selParity w (FILTER (\x. ~(x = i)) transL) 875 else boolXor (w ' i) (selParity w (FILTER (\x. ~(x = i)) transL)))`, 876 Induct_on `transL` THEN1 METIS_TAC [FILTER,countEven_def] THEN 877 SRW_TAC [] [selParity_def,countEven_def,FILTER,ALL_EL] THEN 878 FULL_SIMP_TAC std_ss [boolXor_def] THEN METIS_TAC []); 879 880(*equivalence between two position list used in selParity*) 881 882val selParity_eq1 = Q.store_thm( 883 "selParity_eq1", 884 `!L transL1 transL2 w. 885 ALL_EL (\x. x < 128) transL1 /\ 886 ALL_EL (\x. x < 128) transL2 /\ 887 LENGTH transL1 <= L /\ 888 LENGTH transL2 <= L /\ 889 (!j. j < 128 ==> (countEven j transL1 = countEven j transL2 )) 890 ==> 891 (selParity w transL1 = selParity w transL2)`, 892 Induct_on `L` THEN 893 RW_TAC arith_ss [boolXor_def,countEven_def,selParity_def,LENGTH_NIL] THEN 894 Cases_on `transL1` THEN Cases_on `transL2` THENL [ 895 RW_TAC arith_ss [selParity_def], 896 `h < 128` by FULL_SIMP_TAC list_ss [ALL_EL] THEN 897 `!j. j < 128 ==> 898 countEven j (FILTER (\x. ~(x = h)) (h::t)) = countEven h (h::t)` 899 by METIS_TAC [countEven_def, countEven_filter2, 900 numLib.num_CONV ``128``, ADD1] THEN 901 `!j:num. countEven j []` by METIS_TAC [countEven_def] THEN 902 `!j. j < 128 ==> countEven j (FILTER (\x. ~(x = h)) (h::t))` 903 by METIS_TAC [countEven_def] THEN 904 FULL_SIMP_TAC bool_ss [FILTER] THEN 905 `LENGTH (FILTER (\x. ~(x = h)) t) <= L` 906 by (FULL_SIMP_TAC list_ss [] THEN 907 METIS_TAC [LENGTH_FILTER, LESS_EQ_TRANS]) THEN 908 `LENGTH ([]:num list) <= L` by RW_TAC arith_ss [LENGTH] THEN 909 `ALL_EL (\x. x < 128) t` by FULL_SIMP_TAC list_ss [ALL_EL] THEN 910 `!j. j < 128 ==> (countEven j [] = countEven j (FILTER (\x. ~(x = h)) t))` 911 by METIS_TAC [] THEN 912 `ALL_EL (\x. x < 128) (FILTER (\x. ~(x = h)) t)` 913 by METIS_TAC [ALL_EL_FILTER] THEN 914 `selParity w [] = selParity w (FILTER (\x. ~(x = h)) t)` 915 by METIS_TAC [] THEN 916 `countEven h (h::t)` by METIS_TAC [] THEN 917 `~countEven h t` 918 by FULL_SIMP_TAC std_ss [countEven_def,boolXor_def] THEN 919 METIS_TAC [selParity_filter, boolXor_def, selParity_def, countEven_def], 920 `h < 128` by FULL_SIMP_TAC list_ss [ALL_EL] THEN 921 `!j. j < 128 ==> 922 countEven j (FILTER (\x. ~(x = h)) (h::t)) = countEven h (h::t)` 923 by METIS_TAC [countEven_def, countEven_filter2, 924 numLib.num_CONV ``128``, ADD1] THEN 925 `!j:num. countEven j []` by METIS_TAC [countEven_def] THEN 926 `!j. j < 128 ==> countEven j (FILTER (\x. ~(x = h)) (h::t))` 927 by METIS_TAC [countEven_def] THEN 928 FULL_SIMP_TAC bool_ss [FILTER] THEN 929 `LENGTH (FILTER (\x. ~(x = h)) t) <= L` 930 by (FULL_SIMP_TAC list_ss [] THEN 931 METIS_TAC [LENGTH_FILTER, LESS_EQ_TRANS]) THEN 932 `LENGTH ([]:num list) <= L` by RW_TAC arith_ss [LENGTH] THEN 933 `ALL_EL (\x. x < 128) t` by FULL_SIMP_TAC list_ss [ALL_EL] THEN 934 `!j. j < 128 ==> (countEven j [] = countEven j (FILTER (\x. ~(x = h)) t))` 935 by METIS_TAC [] THEN 936 `ALL_EL (\x. x < 128) (FILTER (\x. ~(x = h)) t)` 937 by METIS_TAC [ALL_EL_FILTER] THEN 938 `selParity w [] = selParity w (FILTER (\x. ~(x = h)) t)` 939 by METIS_TAC [] THEN 940 `countEven h (h::t)` by METIS_TAC [] THEN 941 `~countEven h t` 942 by FULL_SIMP_TAC std_ss [countEven_def,boolXor_def] THEN 943 METIS_TAC [selParity_filter, boolXor_def, selParity_def, countEven_def], 944 `(h < 128) /\ (h' < 128)` by FULL_SIMP_TAC std_ss [ALL_EL] THEN 945 `!j. j < 128 ==> 946 (countEven j (FILTER (\x. ~(x = h')) (h::t)) = 947 countEven j (FILTER (\x. ~(x = h')) (h'::t')))` 948 by METIS_TAC [countEven_def, numLib.num_CONV ``128``, ADD1, 949 countEven_filter3] THEN 950 `ALL_EL (\x. x < 128) (FILTER (\x. ~(x = h')) (h::t)) /\ 951 ALL_EL (\x. x < 128) (FILTER (\x. ~(x = h')) (h'::t'))` 952 by METIS_TAC [ALL_EL_FILTER] THEN 953 `LENGTH (FILTER (\x. ~(x = h')) (h::t)) <= LENGTH (h::t) /\ 954 LENGTH (FILTER (\x. ~(x = h')) (h'::t')) <= LENGTH (h'::t')` 955 by FULL_SIMP_TAC arith_ss [LENGTH_FILTER] THEN 956 `LENGTH (FILTER (\x. ~(x = h')) (h'::t')) <= SUC L /\ 957 LENGTH (FILTER (\x. ~(x = h')) (h::t)) <= SUC L` 958 by FULL_SIMP_TAC arith_ss [] THEN 959 `!j. j < 128 ==> 960 (countEven j (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t))) = 961 countEven j (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h'::t'))))` 962 by METIS_TAC [countEven_filter3,ADD1,numLib.num_CONV ``128``] THEN 963 `(FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t)) = 964 FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) t)) /\ 965 (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h'::t')) = 966 FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) t'))` 967 by RW_TAC list_ss [FILTER_COMM, FILTER] THEN 968 `ALL_EL (\x. x < 128) 969 (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h'::t'))) /\ 970 ALL_EL (\x. x < 128) 971 (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t)))` 972 by METIS_TAC [ALL_EL_FILTER] THEN 973 `LENGTH (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) t)) <= L /\ 974 LENGTH (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) t')) <= L` 975 by (FULL_SIMP_TAC list_ss [] THEN 976 METIS_TAC [LENGTH_FILTER, LESS_EQ_TRANS]) THEN 977 `selParity w (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t))) = 978 selParity w (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h'::t')))` 979 by METIS_TAC [] THEN 980 `(selParity w (h::t) = 981 if countEven h' (h::t) 982 then selParity w (FILTER (\x. ~(x = h')) (h::t)) 983 else boolXor (w ' h') (selParity w (FILTER (\x. ~(x = h')) (h::t)))) /\ 984 (selParity w (h'::t') = 985 if countEven h' (h'::t') 986 then selParity w (FILTER (\x. ~(x = h')) (h'::t')) 987 else boolXor (w ' h') (selParity w (FILTER (\x. ~(x = h')) (h'::t'))))` 988 by METIS_TAC [selParity_filter] THEN 989 `(selParity w (FILTER (\x. ~(x = h')) (h::t)) = 990 if countEven h (FILTER (\x. ~(x = h')) (h::t)) 991 then selParity w (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t))) 992 else boolXor (w ' h) (selParity w 993 (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h::t))))) /\ 994 (selParity w (FILTER (\x. ~(x = h')) (h'::t')) = 995 if countEven h (FILTER (\x. ~(x = h')) (h'::t')) 996 then selParity w (FILTER (\x. ~(x = h)) 997 (FILTER (\x. ~(x = h')) (h'::t'))) 998 else boolXor (w ' h) (selParity w 999 (FILTER (\x. ~(x = h)) (FILTER (\x. ~(x = h')) (h'::t')))))` 1000 by METIS_TAC [selParity_filter] THEN 1001 Cases_on `countEven h' (h::t)` THEN 1002 Cases_on `countEven h (h::t)` THEN 1003 Cases_on `countEven h' (h'::t')` THEN 1004 Cases_on `countEven h (h'::t')` THEN 1005 FULL_SIMP_TAC std_ss [] THEN 1006 METIS_TAC []]); 1007 1008val selParity_eq2 = Q.store_thm( 1009 "selParity_eq2", 1010 `!transL1 transL2 w. 1011 ALL_EL (\x. x < 128) transL1 /\ 1012 ALL_EL (\x. x < 128) transL2 /\ 1013 (!j. 1014 j < 128 1015 ==> 1016 (countEven j transL1 = countEven j transL2 )) 1017 ==> 1018 (selParity w transL1 = selParity w transL2)`, 1019 RW_TAC std_ss [] THEN 1020 Cases_on `LENGTH transL1 < LENGTH transL2` THENL [ 1021 `LENGTH transL1 <= LENGTH transL2` by RW_TAC arith_ss [] THEN 1022 `LENGTH transL2 <= LENGTH transL2` by RW_TAC arith_ss [] THEN 1023 METIS_TAC [selParity_eq1], 1024 `LENGTH transL1 <= LENGTH transL1` by RW_TAC arith_ss [] THEN 1025 `LENGTH transL2 <= LENGTH transL1` by RW_TAC arith_ss [] THEN 1026 METIS_TAC [selParity_eq1]]); 1027 1028(* given linear transformations cancel each other *) 1029 1030val invLT_LT_cancel = Q.store_thm( 1031 "invLT_LT_cancel", 1032 `!w. invLT (LT w) = w`, 1033 SRW_TAC [fcpLib.FCP_ss] 1034 [invLT_def,LT_def,transformComposeWord,LTFunInRange,invLTFunInRange] THEN 1035 `w ' i = selParity w [i]` by RW_TAC std_ss [selParity_def,boolXor_def] THEN 1036 FULL_SIMP_TAC arith_ss [transform_inv2_w128] THEN 1037 `ALL_EL (\x. x < 128) (transCompose LTFun invLTFun i)` 1038 by (FULL_SIMP_TAC arith_ss [GSYM Res_def,transCompose_def] THEN 1039 `!i. i < 128 ==> ALL_EL (\x. x < 128) (Res i)` 1040 by METIS_TAC [Res_fact] THEN 1041 FULL_SIMP_TAC arith_ss []) THEN 1042 `ALL_EL (\x. x < 128) [i]` by RW_TAC list_ss [ALL_EL] THEN 1043 RW_TAC arith_ss [LTFun_invLTFun_fact,selParity_eq2]); 1044 1045val _ = export_theory(); 1046