examples/elliptic/fieldScript.sml

56 (* The subtype context.                                                      *)
59 val context = group_context;
60 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
204 val context = subtypeTools.add_rewrite2'' field_sub_def context;
205 (*val context = subtypeTools.add_rewrite2'' field_div_def context;*)
206 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
465 val context = subtypeTools.add_judgement2 FiniteField_Field context;
466 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
473 val context = subtypeTools.add_judgement2 field_nonzero_carrier context;
474 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
494 val context = subtypeTools.add_reduction2 field_zero_carrier context;
495 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
516 val context = subtypeTools.add_rewrite2 field_one_zero context;
517 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
530 val context = subtypeTools.add_reduction2 field_one_nonzero context;
531 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
539 val context = subtypeTools.add_reduction2 field_neg_carrier context;
540 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
548 val context = subtypeTools.add_reduction2 field_add_carrier context;
549 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
559 val context = subtypeTools.add_rewrite2'' field_add_assoc context;
560 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
581 val context = subtypeTools.add_rewrite2 field_num_zero context;
582 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
593 val context = subtypeTools.add_rewrite2 field_add_lzero context;
594 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
602 val context = subtypeTools.add_rewrite2'' (GSYM field_num_one) context;
603 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
610 val context = subtypeTools.add_rewrite2 field_add_lzero' context;
611 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
618 val context = subtypeTools.add_rewrite2 field_add_rzero context;
619 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
626 val context = subtypeTools.add_rewrite2 field_add_rzero' context;
627 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
639 val context = subtypeTools.add_rewrite2 field_lneg context;
640 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
649 val context = subtypeTools.add_rewrite2 field_lneg' context;
650 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
658 val context = subtypeTools.add_rewrite2 field_rneg context;
659 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
668 val context = subtypeTools.add_rewrite2 field_rneg' context;
669 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
687 val context = subtypeTools.add_rewrite2' field_add_lcancel context;
688 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
702 val context = subtypeTools.add_rewrite2' field_add_rcancel context;
703 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
718 val context = subtypeTools.add_reduction2 field_inv_nonzero context;
719 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
727 val context = subtypeTools.add_rewrite2 field_mult_lzero context;
728 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
736 val context = subtypeTools.add_rewrite2 field_mult_lzero' context;
737 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
747 val context = subtypeTools.add_rewrite2'' field_distrib_ladd context;
748 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
814 val context = subtypeTools.add_rewrite2 field_mult_rzero context;
815 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
823 val context = subtypeTools.add_rewrite2 field_mult_rzero' context;
824 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
838 val context = subtypeTools.add_reduction2 field_mult_nonzero context;
839 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
854 val context = subtypeTools.add_reduction2 field_mult_carrier context;
855 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
875 val context = subtypeTools.add_rewrite2'' field_mult_assoc context;
876 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
921 val context = subtypeTools.add_rewrite2' field_entire context;
922 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
937 val context = subtypeTools.add_rewrite2 field_mult_lone context;
938 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
945 val context = subtypeTools.add_rewrite2 field_mult_lone' context;
946 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
953 val context = subtypeTools.add_rewrite2 field_mult_rone context;
954 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
961 val context = subtypeTools.add_rewrite2 field_mult_rone' context;
962 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
974 val context = subtypeTools.add_rewrite2 field_linv context;
975 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
984 val context = subtypeTools.add_rewrite2 field_linv' context;
985 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
994 val context = subtypeTools.add_rewrite2 field_rinv context;
995 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1004 val context = subtypeTools.add_rewrite2 field_rinv' context;
1005 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1032 val context = subtypeTools.add_rewrite2' field_mult_lcancel context;
1033 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1047 val context = subtypeTools.add_rewrite2' field_mult_rcancel context;
1048 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1056 val context = subtypeTools.add_rewrite2 field_neg_neg context;
1057 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1066 val context = subtypeTools.add_rewrite2 field_neg_cancel context;
1067 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1123 val context = subtypeTools.add_rewrite2 field_neg_zero context;
1124 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1141 val context = subtypeTools.add_rewrite2'' field_distrib_radd context;
1142 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1159 val context = subtypeTools.add_rewrite2 field_mult_lneg context;
1160 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1168 val context = subtypeTools.add_rewrite2 field_mult_rneg context;
1169 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1190 val context = subtypeTools.add_rewrite2'' field_inv_mult context;
1191 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1200 val context = subtypeTools.add_reduction2 field_exp_carrier context;
1201 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1211 val context = subtypeTools.add_reduction2 field_exp_nonzero context;
1212 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1221 val context = subtypeTools.add_reduction2 field_num_carrier context;
1222 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1257 val context = subtypeTools.add_rewrite2 field_inv_one context;
1258 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1265 val context = subtypeTools.add_rewrite2 field_exp_zero context;
1266 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1274 val context = subtypeTools.add_rewrite2 field_exp_one context;
1275 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1295 val context = subtypeTools.add_rewrite2'' field_neg_add context;
1296 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1321 val context = subtypeTools.add_rewrite2 field_num_add context;
1322 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1331 val context = subtypeTools.add_rewrite2'' field_num_add' context;
1332 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1343 val context = subtypeTools.add_rewrite2 field_num_mult context;
1344 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1353 val context = subtypeTools.add_rewrite2'' field_num_mult' context;
1354 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1364 val context = subtypeTools.add_rewrite2 field_num_exp context;
1365 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1373 val context = subtypeTools.add_rewrite2'' field_single_add_single context;
1374 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1383 val context = subtypeTools.add_rewrite2'' field_single_add_single' context;
1384 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1394 val context = subtypeTools.add_rewrite2'' field_single_add_mult context;
1395 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1404 val context = subtypeTools.add_rewrite2'' field_single_add_mult' context;
1405 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1420 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult context;
1421 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1435 val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult' context;
1436 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1451 val context = subtypeTools.add_rewrite2'' field_mult_add_mult context;
1452 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1462 val context = subtypeTools.add_rewrite2'' field_mult_add_mult' context;
1463 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1477 val context = subtypeTools.add_rewrite2'' field_mult_add_neg context;
1478 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1491 val context = subtypeTools.add_rewrite2'' field_mult_add_neg' context;
1492 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1528 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult context;
1529 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1543 val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult' context;
1544 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1553 val context = subtypeTools.add_rewrite2'' field_neg_add_neg context;
1554 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1563 val context = subtypeTools.add_rewrite2'' field_neg_add_neg' context;
1564 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1575 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult context;
1576 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1586 val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult' context;
1587 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1602 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult context;
1603 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1613 val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult' context;
1614 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1621 val context = subtypeTools.add_rewrite2'' field_single_mult_single context;
1622 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1630 val context = subtypeTools.add_rewrite2'' field_single_mult_single' context;
1631 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1639 val context = subtypeTools.add_rewrite2'' field_single_mult_exp context;
1640 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1649 val context = subtypeTools.add_rewrite2'' field_single_mult_exp' context;
1650 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1663 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp context;
1664 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1676 val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp' context;
1677 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1691 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp context;
1692 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1701 val context = subtypeTools.add_rewrite2'' field_exp_mult_exp' context;
1702 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1715 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv context;
1716 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1728 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv' context;
1729 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1762 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp context;
1763 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1776 val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp' context;
1777 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1786 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv context;
1787 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1796 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv' context;
1797 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1807 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp context;
1808 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1818 val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp' context;
1819 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1834 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp context;
1835 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1845 val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp' context;
1846 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1855 val context = subtypeTools.add_rewrite2 field_one_exp context;
1856 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1869 val context = subtypeTools.add_rewrite2 field_zero_exp context;
1870 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1882 val context = subtypeTools.add_rewrite2 field_exp_eq_zero context;
1883 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1894 val context = subtypeTools.add_rewrite2'' field_exp_neg context;
1895 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1908 val context = subtypeTools.add_rewrite2'' field_exp_exp context;
1909 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1958 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_r_conv context;
1959 val context = subtypeTools.add_conversion2'' field_sub_eq_zero_l_conv context;
1960 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1976 val context = subtypeTools.add_rewrite2 field_inv_inv context;
1977 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1985 val context = subtypeTools.add_reduction2 field_sub_carrier context;
1986 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2004 val context = subtypeTools.add_reduction2 field_neg_nonzero context;
2005 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2023 val context = subtypeTools.add_rewrite2'' field_inv_neg context;
2024 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2042 val context = subtypeTools.add_rewrite2'' field_exp_mult context;
2043 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2055 val context = subtypeTools.add_rewrite2'' field_exp_inv context;
2056 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2111 val context = subtypeTools.add_conversion2'' field_add_ac_conv context;
2112 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2163 val context = subtypeTools.add_conversion2'' field_mult_ac_conv context;
2164 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2215 val context = subtypeTools.add_reduction2 field_div_carrier context;
2216 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2224 val context = subtypeTools.add_reduction2 field_div_nonzero context;
2225 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2380 val context = subtypeTools.add_rewrite2 field_inv_eq_zero context;
2381 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2390 val context = subtypeTools.add_rewrite2 field_div_eq_zero context;
2391 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2552 val context = subtypeTools.add_judgement2 GF_in_carrier_imp context;
2553 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
2684 val context = subtypeTools.add_reduction2 GF context;
2685 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;