Structure DefnBaseCore

signature DefnBaseCore =
sig
  type term = Term.term
  type thm  = Thm.thm
  type kname = KernelSig.kernelname

  (* 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.

     For the moment, as per all the names that talk of "userdefs", the
     only useful tag is "user".
  *)
  datatype defn_thm = STDEQNS of thm | OTHER of thm
  type defn_presentation = {const: term, thmname: kname, thm : defn_thm}
  exception nonstdform
  val constants_of_defn : thm -> kname list                (* EXN: nonstdform *)
  val defn_eqns : thm -> (kname * thm) list                (* EXN: nonstdform *)
  val register_defn : {tag: string, thmname:string} -> unit
  val lookup_userdef : term -> defn_presentation option
  val current_userdefs : unit -> defn_presentation list
  val thy_userdefs : {thyname:string} -> defn_presentation list

  val register_indn : thm * kname list -> unit
  val lookup_indn : term -> (thm * kname 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.
   *)

end

HOL 4, Trindemossen-1