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