1signature Defn = 2sig 3 include Abbrev 4 5 type thry = TypeBasePure.typeBase 6 type proofs = Manager.proofs 7 type absyn = Absyn.absyn 8 type pattern = Pmatch.pattern 9 10 val monitoring : bool ref 11 12 val ind_suffix : string ref 13 val def_suffix : string ref 14 val const_eq_ref : conv ref 15 16 val wfrec_eqns : thry -> term -> 17 {SV : term list, 18 WFR : term, 19 extracta : (thm * term list * bool) list, 20 pats : pattern list, 21 proto_def : term} 22 23 val mk_defn : string -> term -> defn 24 val mk_Rdefn : string -> term -> term -> defn 25 val Hol_defn : string -> term quotation -> defn 26 val Hol_Rdefn : string -> term quotation -> term quotation -> defn 27 val mk_defns : string list -> term list -> defn list 28 val Hol_defns : string list -> term quotation -> defn list 29 val Hol_multi_defns : term quotation -> defn list 30 31 val name_of : defn -> string 32 val eqns_of : defn -> thm list 33 val ind_of : defn -> thm option 34 val tcs_of : defn -> term list 35 val reln_of : defn -> term option 36 val params_of : defn -> term list 37 38 val aux_defn : defn -> defn option 39 val union_defn : defn -> defn option 40 41 val inst_defn : defn -> (term,term)subst * (hol_type,hol_type)subst -> defn 42 val set_reln : defn -> term -> defn 43 44 val elim_tcs : defn -> thm list -> defn 45 val simp_tcs : defn -> conv -> defn 46 val prove_tcs : defn -> tactic -> defn 47 48 val triv_defn : defn -> bool 49 val fetch_eqns : defn -> thm 50 51 val been_stored: string * thm -> unit 52 val store : string * thm * thm -> unit 53 val save_defn : defn -> unit 54 55 val parse_absyn : absyn -> term * string list 56 val parse_quote : term quotation -> term list 57 58 val tgoal : defn -> proofs 59 val tprove0 : defn * tactic -> thm * thm 60 val tprove : defn * tactic -> thm * thm 61 val tstore_defn : defn * tactic -> thm * thm 62 63 (* Do a termination proof without the DefnBase.defn object around. The 64 first theorem should be the equations and the second the induction 65 principle, e.g., as written by Defn.save_defn. *) 66 val tgoal_no_defn : (thm * thm) -> proofs 67 val tprove_no_defn : (thm * thm) * tactic -> thm * thm 68 69 val SUC_TO_NUMERAL_DEFN_CONV_hook : (term -> thm) ref 70 71end 72