1(* ========================================================================= *)
2(* FIELD THEORY TOOLS                                                        *)
3(* ========================================================================= *)
4
5signature fieldTools =
6sig
7
8(* ------------------------------------------------------------------------- *)
9(* Syntax operations.                                                        *)
10(* ------------------------------------------------------------------------- *)
11
12val field_ty_op : string
13
14val field_inv_tm : Term.term
15val dest_field_inv : Term.term -> Term.term * Term.term
16val is_field_inv : Term.term -> bool
17
18val field_mult_tm : Term.term
19val dest_field_mult : Term.term -> Term.term * Term.term * Term.term
20val is_field_mult : Term.term -> bool
21
22val field_exp_tm : Term.term
23val dest_field_exp : Term.term -> Term.term * Term.term * Term.term
24val is_field_exp : Term.term -> bool
25
26(* ------------------------------------------------------------------------- *)
27(* AC normalization.                                                         *)
28(* ------------------------------------------------------------------------- *)
29
30val field_add_ac_conv : subtypeTools.named_conv
31
32val field_mult_ac_conv : subtypeTools.named_conv
33
34(* ------------------------------------------------------------------------- *)
35(* Proof tools.                                                              *)
36(* ------------------------------------------------------------------------- *)
37
38val ORACLE_field_poly : bool ref
39
40val field_div_elim_ss : subtypeTools.context2 -> simpLib.simpset
41
42val field_poly_ss : subtypeTools.context2 -> Thm.thm list -> simpLib.simpset
43
44val field_poly_basis_ss : subtypeTools.context2 -> simpLib.simpset
45
46(* ------------------------------------------------------------------------- *)
47(* Subtype context.                                                          *)
48(* ------------------------------------------------------------------------- *)
49
50val field_context : subtypeTools.context2
51
52(* ------------------------------------------------------------------------- *)
53(* Pretty printing.                                                          *)
54(* ------------------------------------------------------------------------- *)
55
56val field_pretty_print : bool ref
57
58val field_pretty_print_max_size : int ref
59
60end
61