1signature FinalThm = 2sig 3 type thm 4 type tag 5 type term 6 type hol_type 7 type 'a set = 'a HOLset.set 8 type depdisk = (string * int) * ((string * int list) list) 9 10 val kernelid : string 11 12 (* Simple operations on the type of theorems *) 13 14 val tag : thm -> tag 15 val hyp : thm -> term list 16 val hypset : thm -> term set 17 val concl : thm -> term 18 val dest_thm : thm -> term list * term 19 val thm_frees : thm -> term list 20 val hyp_frees : thm -> term set 21 val hyp_tyvars : thm -> hol_type set 22 23 24 (* The primitive rules of inference *) 25 26 val ASSUME : term -> thm 27 val REFL : term -> thm 28 val BETA_CONV : term -> thm 29 val ABS : term -> thm -> thm 30 val DISCH : term -> thm -> thm 31 val MP : thm -> thm -> thm 32 val SUBST : (term,thm)Lib.subst -> term -> thm -> thm 33 val INST_TYPE : (hol_type,hol_type)Lib.subst -> thm -> thm 34 35 36 (* Now some derivable-but-primitive rules of inference *) 37 38 39 (* Lambda calculus rules *) 40 41 val ALPHA : term -> term -> thm 42 val MK_COMB : thm * thm -> thm 43 val AP_TERM : term -> thm -> thm 44 val AP_THM : thm -> term -> thm 45 46 47 (* Equality *) 48 49 val SYM : thm -> thm 50 val TRANS : thm -> thm -> thm 51 val EQ_MP : thm -> thm -> thm 52 val EQ_IMP_RULE : thm -> thm * thm 53 54 55 (* Free variable instantiation *) 56 57 val INST : (term,term)Lib.subst -> thm -> thm 58 59 60 (* Universal quantification *) 61 62 val SPEC : term -> thm -> thm 63 val GEN : term -> thm -> thm 64 val GENL : term list -> thm -> thm 65 66 67 (* Existential quantification *) 68 69 val EXISTS : term * term -> thm -> thm 70 val CHOOSE : term * thm -> thm -> thm 71 72 73 (* Conjunction *) 74 75 val CONJ : thm -> thm -> thm 76 val CONJUNCT1 : thm -> thm 77 val CONJUNCT2 : thm -> thm 78 79 80 (* Disjunction *) 81 82 val DISJ1 : thm -> term -> thm 83 val DISJ2 : term -> thm -> thm 84 val DISJ_CASES : thm -> thm -> thm -> thm 85 86 87 (* Negation *) 88 89 val NOT_INTRO : thm -> thm 90 val NOT_ELIM : thm -> thm 91 val CCONTR : term -> thm -> thm 92 93 94 (* Computing with explicit substitutions *) 95 96 val Beta : thm -> thm 97 val Mk_comb : thm -> thm * thm * (thm -> thm -> thm) 98 val Mk_abs : thm -> term * thm * (thm -> thm) 99 val Specialize : term -> thm -> thm 100 101 (* Multiple binders *) 102 103 val GEN_ABS : term option -> term list -> thm -> thm 104 105 (* Oracle invocation *) 106 107 val mk_thm : term list * term -> thm 108 val mk_oracle_thm : string -> term list * term -> thm 109 val mk_axiom_thm : (string Nonce.t * term) -> thm 110 val add_tag : tag * thm -> thm 111 112 (* definitional rules of inference *) 113 val prim_type_definition : {Thy : string, Tyop : string} * thm -> thm 114 val prim_specification : string -> string list -> thm -> thm 115 val gen_prim_specification : string -> thm -> string list * thm 116 117 (* Fetching theorems from disk *) 118 119 val disk_thm : (depdisk * string list) * term list -> thm 120 121 (* Saving proof dependencies *) 122 123 val save_dep : string -> thm -> thm 124 125end; 126