From cbd63ef5fef1f70c441c21859e2182b8d18e60c7 Mon Sep 17 00:00:00 2001
From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Date: Fri, 22 Mar 2024 12:34:59 +1100
Subject: [PATCH 1/3] More arguments (ABS, REP) of newtypeTools.rich_new_type

---
 examples/bnf-datatypes/bnfAlgebraScript.sml   | 11 ++-
 examples/bnf-datatypes/concreteBNFScript.sml  | 15 ++--
 .../context-free/sexpcodeScript.sml           |  5 +-
 .../genericGraphScript.sml                    | 68 ++++++++++++------
 src/1/newtypeTools.sig                        | 20 +++++-
 src/1/newtypeTools.sml                        |  8 +--
 src/num/theories/cvScript.sml                 |  9 ++-
 .../src/more_theories/ordinalScript.sml       |  2 +-
 .../src/more_theories/wellorderScript.sml     | 72 +++++++++----------
 9 files changed, 128 insertions(+), 82 deletions(-)

diff --git a/examples/bnf-datatypes/bnfAlgebraScript.sml b/examples/bnf-datatypes/bnfAlgebraScript.sml
index b09e8a5ee3..3305156e41 100644
--- a/examples/bnf-datatypes/bnfAlgebraScript.sml
+++ b/examples/bnf-datatypes/bnfAlgebraScript.sml
@@ -196,14 +196,13 @@ Type alg[local,pp] = “:α set # ((β,α)F -> α)”
 val idx_tydef as
               {absrep_id, newty, repabs_pseudo_id, termP, termP_exists,
                termP_term_REP, ...} =
-  newtypeTools.rich_new_type(
-  "idx",
+  newtypeTools.rich_new_type{
+  tyname = "idx",
   prove(“∃i : (α,β) alg. alg i”,
         simp[EXISTS_PROD] >> qexists_tac ‘UNIV’ >>
-        simp[alg_def]));
-Overload dIx = (#term_REP_t idx_tydef)
-Overload mkIx = (#term_ABS_t idx_tydef)
-
+        simp[alg_def]),
+  ABS = "mkIx",
+  REP = "dIx"};
 
 Definition bigprod_def:
   bigprod : ((α,β)idx -> α, β) alg =
diff --git a/examples/bnf-datatypes/concreteBNFScript.sml b/examples/bnf-datatypes/concreteBNFScript.sml
index 52b7855883..ee75f529a6 100644
--- a/examples/bnf-datatypes/concreteBNFScript.sml
+++ b/examples/bnf-datatypes/concreteBNFScript.sml
@@ -401,14 +401,13 @@ Type alg[local,pp] = “:α set # ((β,α)F -> α)”
 val idx_tydef as
               {absrep_id, newty, repabs_pseudo_id, termP, termP_exists,
                termP_term_REP, ...} =
-  newtypeTools.rich_new_type(
-  "idx",
-  prove(“∃i : (α,β) alg. alg i”,
-        simp[EXISTS_PROD] >> qexists_tac ‘UNIV’ >>
-        simp[alg_def]));
-Overload dIx = (#term_REP_t idx_tydef)
-Overload mkIx = (#term_ABS_t idx_tydef)
-
+  newtypeTools.rich_new_type{
+  tyname = "idx",
+  exthm = prove(“∃i : (α,β) alg. alg i”,
+           simp[EXISTS_PROD] >> qexists_tac ‘UNIV’ >>
+           simp[alg_def]),
+  ABS = "mkIx",
+  REP = "dIx"};
 
 Definition bigprod_def:
   bigprod : ((α,β)idx -> α, β) alg =
diff --git a/examples/formal-languages/context-free/sexpcodeScript.sml b/examples/formal-languages/context-free/sexpcodeScript.sml
index d5bb185aee..8280e4748f 100644
--- a/examples/formal-languages/context-free/sexpcodeScript.sml
+++ b/examples/formal-languages/context-free/sexpcodeScript.sml
@@ -28,7 +28,10 @@ QED
 
 val {absrep_id, newty, repabs_pseudo_id, termP, termP_exists, termP_term_REP,
      term_ABS_t, term_ABS_pseudo11, term_REP_t, term_REP_11} =
-    newtypeTools.rich_new_type("sexpcode", decencs_exist);
+    newtypeTools.rich_new_type{tyname = "sexpcode",
+                               exthm = decencs_exist,
+                               ABS = "sexpcode_ABS",
+                               REP = "sexpcode_REP"};
 
 Definition encode_def[nocompute]:
   encode sc = SND (^term_REP_t sc)
diff --git a/examples/generic_finite_graphs/genericGraphScript.sml b/examples/generic_finite_graphs/genericGraphScript.sml
index f086d2e6f8..8513418fe1 100644
--- a/examples/generic_finite_graphs/genericGraphScript.sml
+++ b/examples/generic_finite_graphs/genericGraphScript.sml
@@ -125,23 +125,47 @@ Definition edge_cst_def:
      (dirp ⇒ ∀m n. CARD {(m,n,l) | l | (m,n,l) ∈ es} ≤ 1))
 End
 
-val SL_OK_tydefrec = newtypeTools.rich_new_type("SL_OK",
-  prove(“∃x:unit. (λx. T) x”, simp[]));
-val noSL_tydefrec = newtypeTools.rich_new_type("noSL",
-  prove(“∃x:num. (λx. T) x”, simp[]));
-
-val INF_OK_tydefrec = newtypeTools.rich_new_type("INF_OK",
-  prove(“∃x:num. (λx. T) x”, simp[]));
-val finiteG_tydefrec = newtypeTools.rich_new_type("finiteG",
-  prove(“∃x:unit. (λx. T) x”, simp[]));
-
-val undirectedG_tydefrec = newtypeTools.rich_new_type("undirectedG",
-  prove(“∃x:num. (λx. T) x”, simp[]));
-val directedG_tydefrec = newtypeTools.rich_new_type("directedG",
-  prove(“∃x:unit. (λx. T) x”, simp[]));
-
-val allEdgesOK_tydefrec = newtypeTools.rich_new_type("allEdgesOK",
-  prove(“∃x:num. (λx. T) x”, simp[]));
+val SL_OK_tydefrec = newtypeTools.rich_new_type
+   {tyname = "SL_OK",
+    exthm  = prove(“∃x:unit. (λx. T) x”, simp[]),
+    ABS    = "SL_OK_ABS",
+    REP    = "SL_OK_REP"};
+
+val noSL_tydefrec = newtypeTools.rich_new_type
+   {tyname = "noSL",
+    exthm  = prove(“∃x:num. (λx. T) x”, simp[]),
+    ABS    = "noSL_ABS",
+    REP    = "noSL_REP"};
+
+val INF_OK_tydefrec = newtypeTools.rich_new_type
+   {tyname = "INF_OK",
+    exthm  = prove(“∃x:num. (λx. T) x”, simp[]),
+    ABS    = "INF_OK_ABS",
+    REP    = "INF_OK_REP"};
+
+val finiteG_tydefrec = newtypeTools.rich_new_type
+   {tyname = "finiteG",
+    exthm  = prove(“∃x:unit. (λx. T) x”, simp[]),
+    ABS    = "finiteG_ABS",
+    REP    = "finiteG_REP"};
+
+val undirectedG_tydefrec = newtypeTools.rich_new_type
+   {tyname = "undirectedG",
+    exthm  = prove(“∃x:num. (λx. T) x”, simp[]),
+    ABS    = "undirectedG_ABS",
+    REP    = "undirectedG_REP"};
+
+val directedG_tydefrec = newtypeTools.rich_new_type
+   {tyname = "directedG",
+    exthm  = prove(“∃x:unit. (λx. T) x”, simp[]),
+    ABS    = "directedG_ABS",
+    REP    = "directedG_REP"};
+
+val allEdgesOK_tydefrec = newtypeTools.rich_new_type
+   {tyname = "allEdgesOK",
+    exthm  = prove(“∃x:num. (λx. T) x”, simp[]),
+    ABS    = "allEdgesOK_ABS",
+    REP    = "allEdgesOK_REP"};
 
 Definition itself2set_def[simp]:
   itself2set (:'a) = univ(:'a)
@@ -351,12 +375,15 @@ Proof
   qexists ‘{}’ >> simp[]
 QED
 
-val tydefrec = newtypeTools.rich_new_type("graph", graphs_exist)
+val tydefrec = newtypeTools.rich_new_type
+   {tyname = "graph",
+    exthm  = graphs_exist,
+    ABS    = "graph_ABS",
+    REP    = "graph_REP"};
 
 (* any undirected graph *)
 Type udgraph[pp] = “:('a,undirectedG,'ec,'el,'nf,'nl,'sl)graph”
 
-
 (* finite directed graph with labels on nodes and edges, possibility of
    multiple, but finitely many edges, and with self-loops allowed *)
 Type fdirgraph[pp] = “:('NodeEnum,
@@ -1886,4 +1913,5 @@ Proof
   simp[DELETE_COMM, DIFF_COMM]
 QED
 
-val  _ = export_theory();
+val _ = export_theory();
+val _ = html_theory "genericGraph";
diff --git a/src/1/newtypeTools.sig b/src/1/newtypeTools.sig
index 4934b7a77e..2b61562e71 100644
--- a/src/1/newtypeTools.sig
+++ b/src/1/newtypeTools.sig
@@ -1,8 +1,26 @@
+(*---------------------------------------------------------------------------*
+ *       New routines supporting the definition of types                     *
+ *                                                                           *
+ * USAGE: rich_new_type {tyname, exthm, ABS, REP}                            *
+ *                                                                           *
+ * ARGUMENTS: tyname -- the name of the new type                             *
+ *                                                                           *
+ *            exthm --- the existence theorem of the new type (|- ?x. P x)   *
+ *                                                                           *
+ *            ABS  --- the name of the required abstraction function         *
+ *                                                                           *
+ *            REP  --- the name of the required representation function      *
+ *---------------------------------------------------------------------------*)
+
 signature newtypeTools =
 sig
 
   include Abbrev
-  val rich_new_type : string * thm ->
+  val rich_new_type : {tyname: string,
+                       exthm: thm,
+                       ABS: string,
+                       REP: string}
+                       ->
                       {absrep_id: thm,
                        newty: hol_type,
                        repabs_pseudo_id: thm,
diff --git a/src/1/newtypeTools.sml b/src/1/newtypeTools.sml
index c1662be5a5..11f2bf06c6 100644
--- a/src/1/newtypeTools.sml
+++ b/src/1/newtypeTools.sml
@@ -10,8 +10,7 @@ fun t1 /\ t2 = mk_conj(t1, t2)
 fun t1 ==> t2 = mk_imp (t1,t2)
 fun t1 == t2 = mk_eq(t1,t2)
 
-
-fun rich_new_type (tyname, exthm) = let
+fun rich_new_type {tyname, exthm, ABS, REP} = let
   val bij_ax = new_type_definition(tyname, exthm)
   val (termP, oldty) = let
     val (bvar, exthm_body) = exthm |> concl |> dest_exists
@@ -23,8 +22,8 @@ fun rich_new_type (tyname, exthm) = let
   val x = mk_var("x", oldty) and y = mk_var("y", oldty)
   val newty = bij_ax |> concl |> dest_exists |> #1 |> type_of |> dom_rng |> #1
   val term_ABSREP =
-      define_new_type_bijections { ABS = tyname ^ "_ABS", REP = tyname ^ "_REP",
-                                   name = tyname ^ "_ABSREP", tyax = bij_ax}
+      define_new_type_bijections { ABS = ABS, REP = REP,
+                                   name = tyname ^ "_ABSREP", tyax = bij_ax }
   val absrep_id = term_ABSREP |> CONJUNCT1
   val (term_ABS_t, term_REP_t) = let
     val eqn1_lhs = absrep_id|> concl |> strip_forall |> #2 |> lhs
@@ -74,5 +73,4 @@ in
    term_REP_t = term_REP_t, term_ABS_t = term_ABS_t}
 end
 
-
 end (* struct *)
diff --git a/src/num/theories/cvScript.sml b/src/num/theories/cvScript.sml
index 3aa7486985..940c85ff9b 100644
--- a/src/num/theories/cvScript.sml
+++ b/src/num/theories/cvScript.sml
@@ -59,9 +59,12 @@ Inductive iscv:
 [~pair:] (!c d. iscv c /\ iscv d ==> iscv (P0 c d))
 End
 
-val cv_tydefrec = newtypeTools.rich_new_type("cv",
-  prove(“?cv. iscv cv”,
-        Q.EXISTS_TAC ‘N0 0’ >> REWRITE_TAC[iscv_num]))
+val cv_tydefrec = newtypeTools.rich_new_type
+   {tyname = "cv",
+    exthm  = prove(“?cv. iscv cv”,
+                   Q.EXISTS_TAC ‘N0 0’ >> REWRITE_TAC[iscv_num]),
+    ABS    = "cv_ABS",
+    REP    = "cv_REP"};
 
 val Pair_def = new_definition("Pair_def",
   “Pair c d = cv_ABS (P0 (cv_REP c) (cv_REP d))”);
diff --git a/src/pred_set/src/more_theories/ordinalScript.sml b/src/pred_set/src/more_theories/ordinalScript.sml
index b64ab707b2..707807d4f7 100644
--- a/src/pred_set/src/more_theories/ordinalScript.sml
+++ b/src/pred_set/src/more_theories/ordinalScript.sml
@@ -51,7 +51,7 @@ val _ = save_thm ("ordlt_trichotomy", ordlt_trichotomy)
 val _ = overload_on ("mkOrdinal", ``ordinal_ABS``)
 
 val allOrds_def = Define`
-  allOrds = wellorder_ABS { (x,y) | (x = y) \/ ordlt x y }
+  allOrds = mkWO { (x,y) | (x = y) \/ ordlt x y }
 `;
 val EXISTS_PROD = pairTheory.EXISTS_PROD
 val EXISTS_SUM = sumTheory.EXISTS_SUM
diff --git a/src/pred_set/src/more_theories/wellorderScript.sml b/src/pred_set/src/more_theories/wellorderScript.sml
index d89f1a5533..f717f178f7 100644
--- a/src/pred_set/src/more_theories/wellorderScript.sml
+++ b/src/pred_set/src/more_theories/wellorderScript.sml
@@ -74,28 +74,26 @@ val wellfounded_subset = store_thm(
   `?min. min IN s /\ !w. (w,min) IN r ==> w NOTIN s` by metis_tac [] >>
   metis_tac [SUBSET_DEF])
 
-val wellorder_results = newtypeTools.rich_new_type(
-  "wellorder",
-  prove(``?x. wellorder x``, qexists_tac `{}` >> simp[wellorder_EMPTY]))
+val wellorder_results = newtypeTools.rich_new_type
+   {tyname = "wellorder",
+    exthm  = prove(``?x. wellorder x``, qexists_tac `{}` >> simp[wellorder_EMPTY]),
+    ABS    = "mkWO",
+    REP    = "destWO"};
 
-val _ = overload_on ("mkWO", ``wellorder_ABS``)
-val _ = overload_on ("destWO", ``wellorder_REP``)
-
-val _ = save_thm("mkWO_destWO", #absrep_id wellorder_results)
-val _ = export_rewrites ["mkWO_destWO"]
-val destWO_mkWO = save_thm("destWO_mkWO", #repabs_pseudo_id wellorder_results)
+Theorem mkWO_destWO[simp] = #absrep_id wellorder_results
+Theorem destWO_mkWO = #repabs_pseudo_id wellorder_results
 
 val termP_term_REP = #termP_term_REP wellorder_results
 
 val elsOf_def = Define`
-  elsOf w = domain (wellorder_REP w) UNION range (wellorder_REP w)
+  elsOf w = domain (destWO w) UNION range (destWO w)
 `;
 
-val _ = overload_on("WIN", ``\p w. p IN strict (wellorder_REP w)``)
+val _ = overload_on("WIN", ``\p w. p IN strict (destWO w)``)
 val _ = set_fixity "WIN" (Infix(NONASSOC, 425))
-val _ = overload_on("WLE", ``\p w. p IN wellorder_REP w``)
+val _ = overload_on("WLE", ``\p w. p IN destWO w``)
 val _ = set_fixity "WLE" (Infix(NONASSOC, 425))
-val _ = overload_on ("wrange", ``\w. range (wellorder_REP w)``)
+val _ = overload_on ("wrange", ``\w. range (destWO w)``)
 
 val WIN_elsOf = store_thm(
   "WIN_elsOf",
@@ -112,13 +110,13 @@ val WIN_trichotomy = store_thm(
   ``!x y. x IN elsOf w /\ y IN elsOf w ==>
           (x,y) WIN w \/ (x = y) \/ (y,x) WIN w``,
   rpt strip_tac >>
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[elsOf_def, wellorder_def, strict_def, linear_order_def] >> metis_tac[]);
 
 val WIN_REFL = store_thm(
   "WIN_REFL",
   ``(x,x) WIN w <=> F``,
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def, strict_def]);
 val _ = export_rewrites ["WIN_REFL"]
 
@@ -126,14 +124,14 @@ val WLE_TRANS = store_thm(
   "WLE_TRANS",
   ``(x,y) WLE w /\ (y,z) WLE w ==> (x,z) WLE w``,
   strip_tac >>
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def, linear_order_def, transitive_def] >> metis_tac[]);
 
 val WLE_ANTISYM = store_thm(
   "WLE_ANTISYM",
   ``(x,y) WLE w /\ (y,x) WLE w ==> (x = y)``,
   strip_tac >>
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def, linear_order_def, antisym_def]);
 
 val WIN_WLE = store_thm(
@@ -144,7 +142,7 @@ val WIN_WLE = store_thm(
 val elsOf_WLE = store_thm(
   "elsOf_WLE",
   ``x IN elsOf w <=> (x,x) WLE w``,
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def, elsOf_def, reflexive_def, in_domain, in_range] >>
   metis_tac[]);
 
@@ -156,16 +154,16 @@ val transitive_strict = store_thm(
 val WIN_TRANS = store_thm(
   "WIN_TRANS",
   ``(x,y) WIN w /\ (y,z) WIN w ==> (x,z) WIN w``,
-  `transitive (wellorder_REP w) /\ antisym (wellorder_REP w)`
+  `transitive (destWO w) /\ antisym (destWO w)`
      by metis_tac [termP_term_REP, wellorder_def, linear_order_def] >>
   metis_tac [transitive_def, transitive_strict]);
 
 val WIN_WF = store_thm(
   "WIN_WF",
   ``wellfounded (\p. p WIN w)``,
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def] >>
-  qsuff_tac `(\p. p WIN w) = strict (wellorder_REP w)` >- simp[] >>
+  qsuff_tac `(\p. p WIN w) = strict (destWO w)` >- simp[] >>
   simp[FUN_EQ_THM, SPECIFICATION]);
 
 val CURRY_def = pairTheory.CURRY_DEF |> SPEC_ALL |> ABS ``y:'b``
@@ -211,16 +209,16 @@ val reflexive_rrestrict = store_thm(
 
 val wellorder_rrestrict = store_thm(
   "wellorder_rrestrict",
-  ``wellorder (rrestrict (wellorder_REP w) s)``,
-  `wellorder (wellorder_REP w)` by metis_tac [termP_term_REP] >>
+  ``wellorder (rrestrict (destWO w) s)``,
+  `wellorder (destWO w)` by metis_tac [termP_term_REP] >>
   fs[wellorder_def] >>
   rw[linear_order_rrestrict, reflexive_rrestrict] >>
   match_mp_tac wellfounded_subset >>
-  qexists_tac `strict(wellorder_REP w)` >>
+  qexists_tac `strict(destWO w)` >>
   rw[rrestrict_SUBSET, strict_subset]);
 
 val wobound_def = Define`
-  wobound x w = wellorder_ABS (rrestrict (wellorder_REP w) (iseg w x))
+  wobound x w = mkWO (rrestrict (destWO w) (iseg w x))
 `;
 
 val WIN_wobound = store_thm(
@@ -240,7 +238,7 @@ val localDefine = with_flag (computeLib.auto_import_definitions, false) Define
 
 val wellorder_cases = store_thm(
   "wellorder_cases",
-  ``!w. ?s. wellorder s /\ (w = wellorder_ABS s)``,
+  ``!w. ?s. wellorder s /\ (w = mkWO s)``,
   rw[Once (#termP_exists wellorder_results)] >>
   simp_tac (srw_ss() ++ DNF_ss)[#absrep_id wellorder_results]);
 
@@ -352,7 +350,7 @@ val wellorder_fromNat_SUM = store_thm(
   simp[]);
 
 val fromNatWO_def = Define`
-  fromNatWO n = wellorder_ABS { (INL i, INL j) | i <= j /\ j < n }
+  fromNatWO n = mkWO { (INL i, INL j) | i <= j /\ j < n }
 `
 
 val fromNatWO_11 = store_thm(
@@ -759,7 +757,7 @@ val orderlt_trichotomy = store_thm(
     metis_tac [wo2wo_mono, THE_DEF, WIN_elsOf, option_CASES]
   ]);
 
-val wZERO_def = Define`wZERO = wellorder_ABS {}`
+val wZERO_def = Define`wZERO = mkWO {}`
 
 val elsOf_wZERO = store_thm(
   "elsOf_wZERO",
@@ -892,7 +890,7 @@ val orderiso_unique = store_thm(
     (!x y. (x,y) WIN w1 ==> (f2 x, f2 y) WIN w2) ==>
     !x. x IN elsOf w1 ==> (f1 x = f2 x)``,
   rpt strip_tac >> spose_not_then strip_assume_tac >>
-  `wellorder (wellorder_REP w1)` by rw[termP_term_REP] >>
+  `wellorder (destWO w1)` by rw[termP_term_REP] >>
   fs[wellorder_def, wellfounded_def] >>
   first_x_assum (qspec_then `elsOf w1 INTER {x | f1 x <> f2 x}` mp_tac) >>
   asm_simp_tac (srw_ss() ++ SatisfySimps.SATISFY_ss) [] >>
@@ -939,7 +937,7 @@ val WLE_WIN_EQ = store_thm(
   metis_tac [elsOf_WLE, WLE_WIN, WIN_WLE]);
 
 val remove_def = Define`
-  remove e w = wellorder_ABS { (x,y) | x <> e /\ y <> e /\ (x,y) WLE w }
+  remove e w = mkWO { (x,y) | x <> e /\ y <> e /\ (x,y) WLE w }
 `;
 
 val wellorder_remove = store_thm(
@@ -947,7 +945,7 @@ val wellorder_remove = store_thm(
   ``wellorder { (x,y) | x <> e /\ y <> e /\ (x,y) WLE w }``,
   qspec_then `w` assume_tac (GEN_ALL termP_term_REP) >>
   qmatch_abbrev_tac `wellorder r` >>
-  `r = rrestrict (wellorder_REP w) (elsOf w DELETE e)`
+  `r = rrestrict (destWO w) (elsOf w DELETE e)`
      by (simp[EXTENSION, Abbr`r`, rrestrict_def, FORALL_PROD] >>
          metis_tac [WLE_elsOf]) >>
   simp[wellorder_rrestrict]);
@@ -988,11 +986,11 @@ val wellorder_ADD1 = store_thm(
       qexists_tac `a` >> metis_tac [WLE_elsOf]
     ],
     fs[linear_order_def, wellorder_def] >>
-    `domain (wellorder_REP w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
+    `domain (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
      e INSERT elsOf w`
        by (rw[EXTENSION, in_domain, in_range, EQ_IMP_THM] >>
            metis_tac [WLE_elsOf]) >>
-    `range (wellorder_REP w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
+    `range (destWO w UNION {(x,e) | x IN elsOf w} UNION {(e,e)}) =
      e INSERT elsOf w`
        by (rw[EXTENSION, in_domain, in_range] >>
            metis_tac [elsOf_WLE, WLE_elsOf]) >>
@@ -1028,16 +1026,16 @@ val elsOf_cardeq_iso = store_thm(
   ``INJ f (elsOf (wo:'b wellorder)) univ(:'a) ==>
     ?wo':'a wellorder. orderiso wo wo'``,
   simp[elsOf_def] >> strip_tac >>
-  `wellorder (wellorder_REP wo)` by simp[#termP_term_REP wellorder_results] >>
-  qexists_tac `wellorder_ABS (IMAGE (f ## f) (wellorder_REP wo))` >>
+  `wellorder (destWO wo)` by simp[#termP_term_REP wellorder_results] >>
+  qexists_tac `mkWO (IMAGE (f ## f) (destWO wo))` >>
   simp[orderiso_thm] >>
-  `wellorder (IMAGE (f ## f) (wellorder_REP wo))`
+  `wellorder (IMAGE (f ## f) (destWO wo))`
     by imp_res_tac INJ_preserves_wellorder >>
   qexists_tac `f` >>
   simp[destWO_mkWO, elsOf_def, domain_IMAGE_ff, range_IMAGE_ff] >>
   simp_tac bool_ss [GSYM IMAGE_UNION] >>
   qabbrev_tac `
-    els = domain (wellorder_REP wo) UNION range (wellorder_REP wo)` >>
+    els = domain (destWO wo) UNION range (destWO wo)` >>
   simp[BIJ_DEF, SURJ_IMAGE] >>
   simp[strict_def, EXISTS_PROD] >>
   fs[INJ_DEF] >>

From 5e52861f53e4888155609dcacfa51152bf137bee Mon Sep 17 00:00:00 2001
From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Date: Fri, 22 Mar 2024 12:56:37 +1100
Subject: [PATCH 2/3] FTBFS rich_new_type{} in nomdatatype.ml

---
 examples/lambda/basics/nomdatatype.sml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/examples/lambda/basics/nomdatatype.sml b/examples/lambda/basics/nomdatatype.sml
index 03319d7e35..932a964218 100644
--- a/examples/lambda/basics/nomdatatype.sml
+++ b/examples/lambda/basics/nomdatatype.sml
@@ -131,7 +131,9 @@ fun new_type_step1 tyname n {vp, lp} = let
   val {absrep_id, newty, repabs_pseudo_id, termP, termP_exists, termP_term_REP,
        term_ABS_t, term_ABS_pseudo11,
        term_REP_t, term_REP_11} =
-      newtypeTools.rich_new_type (tyname, term_exists)
+      newtypeTools.rich_new_type {tyname = tyname, exthm = term_exists,
+                                  ABS = tyname ^ "_ABS",
+                                  REP = tyname ^ "_REP"}
 in
   {term_ABS_pseudo11 = term_ABS_pseudo11, term_REP_11 = term_REP_11,
    term_REP_t = term_REP_t, term_ABS_t = term_ABS_t, absrep_id = absrep_id,

From 250529c22b93a1585bd38efd974bf889923a5c2f Mon Sep 17 00:00:00 2001
From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Date: Sat, 23 Mar 2024 17:38:45 +1100
Subject: [PATCH 3/3] Fix uses of newtypeTools.rich_new_type in newly committed
 work

---
 examples/algebra/aat/aatmonoidScript.sml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/examples/algebra/aat/aatmonoidScript.sml b/examples/algebra/aat/aatmonoidScript.sml
index 51966684de..07ca5b424b 100644
--- a/examples/algebra/aat/aatmonoidScript.sml
+++ b/examples/algebra/aat/aatmonoidScript.sml
@@ -35,7 +35,10 @@ Proof
 QED
 
 val mrec as {absrep_id,...} =
-       newtypeTools.rich_new_type ("monoid", fullmonoids_exist)
+       newtypeTools.rich_new_type {tyname = "monoid",
+                                   exthm = fullmonoids_exist,
+                                   ABS = "monoid_ABS",
+                                   REP = "monoid_REP"};
 
 Overload mkmonoid = “monoid_ABS”