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 11 (* Imperative database of datatype facts and associated operations. *) 12 13 val theTypeBase : unit -> typeBase 14 val write : tyinfo list -> tyinfo list 15 val export : tyinfo list -> unit 16 val fetch : hol_type -> tyinfo option 17 val read : {Thy :string, Tyop: string} -> tyinfo option 18 val elts : unit -> tyinfo list 19 val register_update_fn : (tyinfo list -> tyinfo list) -> unit 20 21 val axiom_of : hol_type -> thm 22 val induction_of : hol_type -> thm 23 val constructors_of : hol_type -> term list 24 val destructors_of : hol_type -> thm list 25 val recognizers_of : hol_type -> thm list 26 val case_const_of : hol_type -> term 27 val case_cong_of : hol_type -> thm 28 val case_def_of : hol_type -> thm 29 val case_eq_of : hol_type -> thm 30 val nchotomy_of : hol_type -> thm 31 val distinct_of : hol_type -> thm 32 val fields_of : hol_type -> (string * hol_type) list 33 val accessors_of : hol_type -> thm list 34 val updates_of : hol_type -> thm list 35 val one_one_of : hol_type -> thm 36 val simpls_of : hol_type -> simpfrag.simpfrag 37 val size_of : hol_type -> term * thm 38 val encode_of : hol_type -> term * thm 39 40 val axiom_of0 : hol_type -> shared_thm 41 val induction_of0 : hol_type -> shared_thm 42 val size_of0 : hol_type -> (term * shared_thm) option 43 val encode_of0 : hol_type -> (term * shared_thm) option 44 45 val is_constructor : term -> bool 46 47 val mk_case : term * (term * term) list -> term 48 val dest_case : term -> term * term * (term * term) list 49 val is_case : term -> bool 50 val strip_case : term -> term * (term * term) list 51 val mk_pattern_fn : (term * term) list -> term 52 53 val mk_record : hol_type * (string * term) list -> term 54 val dest_record : term -> hol_type * (string * term) list 55 val is_record : term -> bool 56 57 val dest_record_type : hol_type -> (string * hol_type) list 58 val is_record_type : hol_type -> bool 59 60 val CaseEq : string -> thm 61 val CaseEqs : string list -> thm 62 val AllCaseEqs : unit -> thm 63end 64