examples/elliptic/groupScript.sml

49 (* The subtype context.                                                      *)
52 val context = subtypeTools.empty2;
53 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
551 val context = subtypeTools.add_judgement2 AbelianGroup_Group context;
552 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
559 val context = subtypeTools.add_judgement2 FiniteGroup_Group context;
560 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
567 val context = subtypeTools.add_judgement2 FiniteAbelianGroup_FiniteGroup context;
568 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
575 val context =
576     subtypeTools.add_judgement2 FiniteAbelianGroup_AbelianGroup context;
577 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
596 val context = subtypeTools.add_reduction2 group_id_carrier context;
597 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
604 val context = subtypeTools.add_reduction2 group_inv_carrier context;
605 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
612 val context = subtypeTools.add_reduction2 group_mult_carrier context;
613 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
620 val context = subtypeTools.add_rewrite2 group_lid context;
621 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
628 val context = subtypeTools.add_rewrite2 group_linv context;
629 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
637 val context = subtypeTools.add_rewrite2'' group_assoc context;
638 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
697 val context = subtypeTools.add_rewrite2 group_rinv context;
698 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
724 val context = subtypeTools.add_rewrite2 group_rid context;
725 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
747 val context = subtypeTools.add_rewrite2' group_lcancel context;
748 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
767 val context = subtypeTools.add_rewrite2' group_lcancel_id context;
768 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
800 val context = subtypeTools.add_rewrite2' group_rcancel context;
801 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
820 val context = subtypeTools.add_rewrite2' group_rcancel_id context;
821 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
848 val context = subtypeTools.add_rewrite2' group_inv_cancel context;
849 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
861 val context = subtypeTools.add_rewrite2 group_inv_inv context;
862 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
889 val context = subtypeTools.add_rewrite2 group_inv_id context;
890 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
931 val context = subtypeTools.add_rewrite2'' group_inv_mult context;
932 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
942 val context = subtypeTools.add_reduction2 group_exp_carrier context;
943 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
952 val context = subtypeTools.add_rewrite2 group_id_exp context;
953 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1073 val context = subtypeTools.add_conversion2'' group_ac_conv context;
1074 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1135 val context = subtypeTools.add_reduction2 trivial_group context;
1136 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1426 val context = subtypeTools.add_reduction2 add_mod context;
1427 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1448 val context = subtypeTools.add_judgement2 Prime_Nonzero context;
1449 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
1514 val context = subtypeTools.add_reduction2 mult_mod context;
1515 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;