1signature TotalDefn = 2sig 3 4 include Abbrev 5 6 (* Support for automated termination proofs *) 7 8 val guessR : defn -> term list 9 val proveTotal : tactic -> defn -> defn * thm option 10 11 12 (* Support for interactive termination proofs *) 13 14 val WF_thms : thm list ref 15 val termination_simps : thm list ref 16 17 val PRIM_WF_TAC : thm list -> tactic 18 val PRIM_TC_SIMP_CONV : thm list -> conv 19 val PRIM_TC_SIMP_TAC : thm list -> tactic 20 val PRIM_WF_REL_TAC : term quotation -> thm list -> thm list -> tactic 21 22 val WF_TAC : tactic 23 val TC_SIMP_CONV : conv 24 val TC_SIMP_TAC : tactic 25 val STD_TERM_TAC : tactic 26 val WF_REL_TAC : term quotation -> tactic 27 28 (* Definitions with automated termination proof support *) 29 30 val defnDefine : tactic -> defn -> thm * thm option * thm option 31 val primDefine : defn -> thm * thm option * thm option 32 val tDefine : string -> term quotation -> tactic -> thm 33 val xDefine : string -> term quotation -> thm 34 val Define : term quotation -> thm 35 val multiDefine : term quotation -> thm list 36 datatype phase 37 = PARSE of term quotation 38 | BUILD of term 39 | TERMINATION of defn 40 41 type apidefn = (defn * thm option, phase * exn) Lib.verdict 42 43 val apiDefine : (defn->term list) -> tactic -> string * term -> apidefn 44 val apiDefineq : (defn->term list) -> tactic -> term quotation -> apidefn 45 val std_apiDefine : string * term -> apidefn 46 val std_apiDefineq : term quotation -> apidefn 47 48 val xDefineSchema : string -> term quotation -> thm 49 val DefineSchema : term quotation -> thm 50 51end 52