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