More arguments for newtypeTools.rich_new_type

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”
 

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 =

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 =

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)

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";

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,

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,

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 *)

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))”);

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