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