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