More arguments for newtypeTools.rich_new_type

[binghe]

Hi,

The (undocumented) tool newtypeTools.rich_new_type currently lacks the ability to specify the newly created function constants for converting between the abstraction and representation types (ABS and REP). The current workaround is to do overloading after calling it, e.g., in wellorderScript.sml:

val wellorder_results = newtypeTools.rich_new_type(
  "wellorder",
  prove(``?x. wellorder x``, qexists_tac `{}` >> simp[wellorder_EMPTY]))

val _ = overload_on ("mkWO", ``wellorder_ABS``)
val _ = overload_on ("destWO", ``wellorder_REP``)

In this PR, per our offline discussions, I have modified the signature of rich_new_type to allow providing ABS and REP constant names. The new signature is the following:

  val rich_new_type : {tyname: string,
                       exthm: thm,
                       ABS: string,
                       REP: string}
                       ->
                      {absrep_id: thm,
                       newty: hol_type,
                       repabs_pseudo_id: thm,
                       termP: term,
                       termP_exists: thm,
                       termP_term_REP: thm,
                       term_ABS_t: term,
                       term_ABS_pseudo11: thm,
                       term_REP_t: term,
                       term_REP_11: thm}

All existing uses in core theories and examples are updated with the extra ABS and REP parameters (NOTE: SML doesn't support optional record slot values).

NOTE: in wellorderScript.sml, although the two constants wellorder_ABS and wellorder_REP were overloaded, they are still used in many places. I have updated them all.

--Chun

[mn200]

Many thanks! (I should get around to documenting this...)