1(* ========================================================================= *) 2(* ELLIPTIC CURVE THEORY TOOLS *) 3(* ========================================================================= *) 4 5structure ellipticTools :> ellipticTools = 6struct 7 8open HolKernel Parse boolLib bossLib fieldTools ellipticTheory; 9 10(* ------------------------------------------------------------------------- *) 11(* Syntax operations. *) 12(* ------------------------------------------------------------------------- *) 13 14(* ------------------------------------------------------------------------- *) 15(* Pretty printing. *) 16(* ------------------------------------------------------------------------- *) 17 18(* ------------------------------------------------------------------------- *) 19(* AC normalization. *) 20(* ------------------------------------------------------------------------- *) 21 22(* ------------------------------------------------------------------------- *) 23(* Proof tools. *) 24(* ------------------------------------------------------------------------- *) 25 26(* ------------------------------------------------------------------------- *) 27(* Subtype context. *) 28(* ------------------------------------------------------------------------- *) 29 30val context = field_context; 31val context = subtypeTools.add_reduction2 curve_field context; 32val context = subtypeTools.add_reduction2 curve_a1_carrier context; 33val context = subtypeTools.add_reduction2 curve_a2_carrier context; 34val context = subtypeTools.add_reduction2 curve_a3_carrier context; 35val context = subtypeTools.add_reduction2 curve_a4_carrier context; 36val context = subtypeTools.add_reduction2 curve_a6_carrier context; 37val context = subtypeTools.add_reduction2 curve_zero_carrier context; 38val context = subtypeTools.add_reduction2 curve_neg_carrier context; 39val context = subtypeTools.add_reduction2 curve_double_carrier context; 40val context = subtypeTools.add_reduction2 curve_add_carrier context; 41val context = subtypeTools.add_rewrite2 curve_double_zero context; 42val context = subtypeTools.add_rewrite2 curve_add_lzero context; 43val context = subtypeTools.add_rewrite2 curve_add_lneg context; 44val context = subtypeTools.add_rewrite2 curve_add_rzero context; 45val context = subtypeTools.add_rewrite2 curve_add_rneg context; 46(*** 47val context = subtypeTools.add_reduction2 curve_group context; 48val context = subtypeTools.add_rewrite2 example_prime_def context; 49val context = subtypeTools.add_rewrite2 example_field_def context; 50val context = subtypeTools.add_reduction2 example_curve context; 51***) 52 53val elliptic_context = context; 54 55end 56