1signature FinalTerm = 2sig 3 4 eqtype term 5 eqtype hol_type 6 type ('a,'b)subst = ('a,'b)Lib.subst 7 type 'a set = 'a HOLset.set 8 9 val equality : term 10 11 val type_of : term -> hol_type 12 val free_vars : term -> term list 13 val free_vars_lr : term -> term list 14 val FVL : term list -> term set -> term set 15 val free_in : term -> term -> bool 16 val all_vars : term -> term list 17 val all_atoms : term -> term set 18 val all_atomsl : term list -> term set -> term set 19 val free_varsl : term list -> term list 20 val all_varsl : term list -> term list 21 val type_vars_in_term : term -> hol_type list 22 val var_occurs : term -> term -> bool 23 24 val genvar : hol_type -> term 25 val genvars : hol_type -> int -> term list 26 val variant : term list -> term -> term 27 val prim_variant : term list -> term -> term 28 val gen_variant : (string -> bool) -> string -> term list -> term -> term 29 30 val mk_var : string * hol_type -> term 31 val mk_primed_var : string * hol_type -> term 32 val decls : string -> term list 33 val all_consts : unit -> term list 34 val mk_const : string * hol_type -> term 35 val prim_mk_const : {Thy:string, Name:string} -> term 36 val mk_thy_const : {Thy:string, Name:string, Ty:hol_type} -> term 37 val list_mk_comb : term * term list -> term 38 val mk_comb : term * term -> term 39 val mk_abs : term * term -> term 40 val list_mk_binder : term option -> term list * term -> term 41 val list_mk_abs : term list * term -> term 42 val dest_var : term -> string * hol_type 43 val dest_const : term -> string * hol_type 44 val dest_thy_const : term -> {Thy:string, Name:string, Ty:hol_type} 45 val dest_comb : term -> term * term 46 val strip_binder : term option -> term -> term list * term 47 val strip_abs : term -> term list * term 48 val dest_abs : term -> term * term 49 val is_var : term -> bool 50 val is_genvar : term -> bool 51 val is_const : term -> bool 52 val is_comb : term -> bool 53 val is_abs : term -> bool 54 val rator : term -> term 55 val rand : term -> term 56 val bvar : term -> term 57 val body : term -> term 58 val rename_bvar : string -> term -> term 59 60 val same_const : term -> term -> bool 61 val aconv : term -> term -> bool 62 val beta_conv : term -> term 63 val eta_conv : term -> term 64 val subst : (term,term) subst -> term -> term 65 val inst : (hol_type,hol_type) subst -> term -> term 66 67 val raw_match : hol_type list -> term set 68 -> term -> term 69 -> (term,term)subst * (hol_type,hol_type)subst 70 -> ((term,term)subst * term set) * 71 ((hol_type,hol_type)subst * hol_type list) 72 val match_terml : hol_type list -> term set -> term -> term 73 -> (term,term)subst * (hol_type,hol_type)subst 74 val match_term : term -> term -> (term,term)subst*(hol_type,hol_type)subst 75 val norm_subst : ((term,term)subst * term set) * 76 ((hol_type,hol_type)subst * hol_type list) 77 -> ((term,term)subst * (hol_type,hol_type)subst) 78 79 val var_compare : term * term -> order 80 val compare : term * term -> order 81 val term_eq : term -> term -> bool 82 val fast_term_eq : term -> term -> bool 83 84 val empty_tmset : term set 85 val empty_varset : term set 86 87 val term_size : term -> int 88 89 (* theory segment related functionality *) 90 val uptodate_term : term -> bool 91 92 val thy_consts : string -> term list 93 val del_segment : string -> unit 94 95 val prim_new_const : KernelSig.kernelname -> hol_type -> term 96 val prim_delete_const : KernelSig.kernelname -> unit 97 98 (* printed theory functionality *) 99 val read_raw : term vector -> string -> term 100 val write_raw : (term -> int) -> term -> string 101 102 datatype lambda = 103 VAR of string * hol_type 104 | CONST of {Name : string, Thy : string, Ty : hol_type} 105 | COMB of term * term 106 | LAMB of term * term 107 val dest_term : term -> lambda 108 val identical : term -> term -> bool 109 110 111end 112