1signature nomdatatype =
2sig
3
4  include Abbrev
5  type coninfo = {con_termP : thm, con_def : thm}
6
7  val new_type_step1 : string -> int -> {vp:term,lp:term} ->
8                       {term_ABS_pseudo11 : thm,
9                        term_REP_11 : thm,
10                        term_REP_t : term,
11                        term_ABS_t : term,
12                        absrep_id : thm,
13                        repabs_pseudo_id : thm,
14                        genind_term_REP : thm,
15                        genind_exists : thm,
16                        newty : hol_type,
17                        termP : term}
18
19  val termP_removal :
20      {elimth : thm, absrep_id : thm, tpm_def : thm, termP : term,
21       repty : hol_type} ->
22      term -> thm
23      (* tpm_def should be a theorem of the form
24           pm pi t = ABS (gtpm pi (REP t))
25         where pm is the term that the user expects to see as the
26         permutation action for the new type.  I.e., this will presumably
27         be something like ``pmact something``. *)
28
29
30  val define_permutation : { name_pfx : string, name : string,
31                             term_REP_t : term, term_ABS_t : term,
32                             absrep_id : thm, repabs_pseudo_id : thm,
33                             cons_info : coninfo list, newty : hol_type,
34                             genind_term_REP : thm} ->
35                           { tpm_thm : thm, term_REP_tpm : thm,
36                             t_pmact_t : term, tpm_t : term}
37
38  (* datatype utility functions *)
39  val rpt_hyp_dest_conj : thm -> thm
40  val elim_unnecessary_atoms : {finite_fv:thm} -> thm list -> thm -> thm
41  val sort_uvars : conv
42  val rename_vars : (string * string) list -> conv
43  val lift_exfunction : {repabs_pseudo_id : thm, term_REP_t : term,
44                         cons_info : coninfo list} ->
45                        thm -> thm
46  val prove_alpha_fcbhyp : {ppm:term, alphas: thm list, rwts: thm list} ->
47                           thm -> thm
48  val defined_const : thm -> term
49
50end
51
52
53