# Structure DefnBase

signature DefnBase =
sig
type term = Term.term
type thm = Thm.thm
datatype defn
= ABBREV of {eqn:thm, bind:string}
| PRIMREC of {eqs:thm, ind:thm, bind:string}
| NONREC of {eqs:thm, ind:thm, SV:term list, stem:string}
| STDREC of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string}
| MUTREC of {eqs:thm list, ind:thm, R:term,SV:term list,
stem:string,union:defn}
| NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list,
stem:string,aux:defn}
| TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string}
val pp_defn : defn Parse.pprinter
val all_terms : defn -> term list
(* conclusions of theorems, SV variables, R *)
(* Used to control context tracking during termination
condition extraction *)
val read_congs : unit -> thm list
val write_congs : thm list -> unit
val add_cong : thm -> unit
val drop_cong : term -> thm
val export_cong : string -> unit
(* record various flavours of definition, keyed by constant and a
"tag", which is a user-choosable string. Assume that "user" and
"compute" exist for example.
Another might be "PMATCH", which would be the definition with
case constants translated into PMATCH versions.
*)
val register_defn : string -> thm -> unit
val lookup_defn : term -> string -> thm option
val register_indn : thm * term list -> unit
val lookup_indn : term -> (thm * term list) option
(* register_defn is given a tag and a theorem which is a conjunction of
possibly universally quantified equations. The machinery here
will create a sub-conjunction of the clauses per constant (and this is
what is returned by lookup_defn).
Induction theorems have some number of induction variables (P1,
P2, ..) where each corresponds to a defined constant. This list
of constants is what is passed into register_indn alongside the
induction theorem. When a term is looked up, if lookup_indn t
returns SOME (th, ts), then t will be among the ts.
*)
val const_eq_ref : Abbrev.conv ref
val elim_triv_literal_CONV : Abbrev.conv
val one_line_ify : PmatchHeuristics.pmatch_heuristic option -> thm -> thm
end

*HOL 4, Kananaskis-14*