1signature TypeBase = 2sig 3 4 type hol_type = Type.hol_type 5 type term = Term.term 6 type thm = Thm.thm 7 type tyinfo = TypeBasePure.tyinfo 8 type typeBase = TypeBasePure.typeBase 9 type shared_thm = TypeBasePure.shared_thm 10 type rcd_fieldinfo = TypeBasePure.rcd_fieldinfo 11 12 (* Imperative database of datatype facts and associated operations. *) 13 14 val theTypeBase : unit -> typeBase 15 val thy_typebase : {thyname : string} -> typeBase option 16 val thy_updates : {thyname : string} -> tyinfo list 17 val merge_typebases : string list -> typeBase option 18 val write : tyinfo list -> unit 19 val export : tyinfo list -> unit (* includes write action *) 20 val fetch : hol_type -> tyinfo option 21 val read : {Thy :string, Tyop: string} -> tyinfo option 22 val elts : unit -> tyinfo list 23 val register_update_fn : (tyinfo -> tyinfo) -> unit 24 25 val axiom_of : hol_type -> thm 26 val induction_of : hol_type -> thm 27 val constructors_of : hol_type -> term list 28 val destructors_of : hol_type -> thm list 29 val recognizers_of : hol_type -> thm list 30 val case_const_of : hol_type -> term 31 val case_cong_of : hol_type -> thm 32 val case_def_of : hol_type -> thm 33 val case_eq_of : hol_type -> thm 34 val nchotomy_of : hol_type -> thm 35 val distinct_of : hol_type -> thm 36 val fields_of : hol_type -> (string * rcd_fieldinfo) list 37 val accessors_of : hol_type -> thm list 38 val updates_of : hol_type -> thm list 39 val one_one_of : hol_type -> thm 40 val simpls_of : hol_type -> simpfrag.simpfrag 41 val size_of : hol_type -> term * thm 42 val encode_of : hol_type -> term * thm 43 44 val axiom_of0 : hol_type -> shared_thm 45 val induction_of0 : hol_type -> shared_thm 46 val size_of0 : hol_type -> (term * shared_thm) option 47 val encode_of0 : hol_type -> (term * shared_thm) option 48 49 val is_constructor : term -> bool 50 51 val mk_case : term * (term * term) list -> term 52 val dest_case : term -> term * term * (term * term) list 53 val is_case : term -> bool 54 val strip_case : term -> term * (term * term) list 55 val mk_pattern_fn : (term * term) list -> term 56 57 val mk_record : hol_type * (string * term) list -> term 58 val dest_record : term -> hol_type * (string * term) list 59 val is_record : term -> bool 60 61 val dest_record_type : hol_type -> (string * rcd_fieldinfo) list 62 val is_record_type : hol_type -> bool 63 64 val CaseEq : string -> thm 65 val CaseEqs : string list -> thm 66 val AllCaseEqs : unit -> thm 67 68 val update_induction : thm -> unit 69 val update_axiom : thm -> unit 70end 71