Regenerate the test files and fix a proof

9 files changed, 11 insertions, 83 deletions

diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 5e604f8c..bd16c16c 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -88,14 +88,6 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘
     od
 ’
 
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body_def:
-  core_num_u64_max_body : u64 result = Return (int_to_u64 18446744073709551615)
-End
-Definition core_num_u64_max_c_def:
-  core_num_u64_max_c : u64 = get_return_value core_num_u64_max_body
-End
-
 val betree_upsert_update_fwd_def = Define ‘
   (** [betree_main::betree::upsert_update]: forward function *)
   betree_upsert_update_fwd
@@ -109,8 +101,8 @@ val betree_upsert_update_fwd_def = Define ‘
       (case st of
       | BetreeUpsertFunStateAdd v =>
         do
-        margin <- u64_sub core_num_u64_max_c prev0;
-        if u64_ge margin v then u64_add prev0 v else Return core_num_u64_max_c
+        margin <- u64_sub core_u64_max prev0;
+        if u64_ge margin v then u64_add prev0 v else Return core_u64_max
         od
       | BetreeUpsertFunStateSub v =>
         if u64_ge prev0 v then u64_sub prev0 v else Return (int_to_u64 0)))
diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betreeMain_FunsTheory.sig
index 6c249f70..c922ca9f 100644
--- a/tests/hol4/betree/betreeMain_FunsTheory.sig
+++ b/tests/hol4/betree/betreeMain_FunsTheory.sig
@@ -58,8 +58,6 @@ sig
     val betree_store_internal_node_fwd_def : thm
     val betree_store_leaf_node_fwd_def : thm
     val betree_upsert_update_fwd_def : thm
-    val core_num_u64_max_body_def : thm
-    val core_num_u64_max_c_def : thm
     val main_fwd_def : thm
   
   val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1215,22 +1213,14 @@ sig
             case st of
               BetreeUpsertFunStateAdd v =>
                 do
-                  margin <- u64_sub core_num_u64_max_c prev0;
+                  margin <- u64_sub core_u64_max prev0;
                   if u64_ge margin v then u64_add prev0 v
-                  else Return core_num_u64_max_c
+                  else Return core_u64_max
                 od
             | BetreeUpsertFunStateSub v' =>
               if u64_ge prev0 v' then u64_sub prev0 v'
               else Return (int_to_u64 0)
    
-   [core_num_u64_max_body_def]  Definition
-      
-      ⊢ core_num_u64_max_body = Return (int_to_u64 18446744073709551615)
-   
-   [core_num_u64_max_c_def]  Definition
-      
-      ⊢ core_num_u64_max_c = get_return_value core_num_u64_max_body
-   
    [main_fwd_def]  Definition
       
       ⊢ main_fwd = Return ()
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
index e3c3d2a5..682c5760 100644
--- a/tests/hol4/hashmap/hashmap_FunsScript.sml
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -170,14 +170,6 @@ val hash_map_insert_no_resize_fwd_back_def = Define ‘
     od
 ’
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
   (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
       (there is a single backward function, and the forward function returns ()) *)
@@ -241,7 +233,7 @@ val hash_map_try_resize_fwd_back_def = Define ‘
       (there is a single backward function, and the forward function returns ()) *)
   hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
     do
-    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    max_usize <- mk_usize (u32_to_int core_u32_max);
     let capacity = vec_len self.hash_map_slots in
     do
     n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig
index 50482547..bb3e192b 100644
--- a/tests/hol4/hashmap/hashmap_FunsTheory.sig
+++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
   type thm = Thm.thm
   
   (*  Definitions  *)
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val hash_key_fwd_def : thm
     val hash_map_allocate_slots_fwd_def : thm
     val hash_map_allocate_slots_loop_fwd_def : thm
@@ -48,14 +46,6 @@ sig
 (*
    [hashmap_Types] Parent theory of "hashmap_Funs"
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [hash_key_fwd_def]  Definition
       
       ⊢ ∀k. hash_key_fwd k = Return k
@@ -472,7 +462,7 @@ sig
       ⊢ ∀self.
           hash_map_try_resize_fwd_back self =
           do
-            max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+            max_usize <- mk_usize (u32_to_int core_u32_max);
             capacity <<- vec_len self.hash_map_slots;
             n1 <- usize_div max_usize (int_to_usize 2);
             (i,i0) <<- self.hash_map_max_load_factor;
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 7259f2f5..8bc12fa5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1296,7 +1296,7 @@ Proof
   rw [hash_map_try_resize_fwd_back_def] >>
   (* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *)
   assume_tac usize_u32_bounds >>
-  fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >>
+  fs [core_u32_max_def, u32_max_def] >>
   massage >> fs [mk_usize_def, u32_max_def] >>
   (* / 2 *)
   progress >>
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
index b21c4f58..c1e30aa6 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
@@ -193,14 +193,6 @@ val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘
     od
 ’
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
   (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
       (there is a single backward function, and the forward function returns ()) *)
@@ -271,7 +263,7 @@ val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
   hashmap_hash_map_try_resize_fwd_back
     (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
     do
-    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    max_usize <- mk_usize (u32_to_int core_u32_max);
     let capacity = vec_len self.hashmap_hash_map_slots in
     do
     n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
index 1d24cb26..d4e43d9a 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
   type thm = Thm.thm
   
   (*  Definitions  *)
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val hashmap_hash_key_fwd_def : thm
     val hashmap_hash_map_allocate_slots_fwd_def : thm
     val hashmap_hash_map_allocate_slots_loop_fwd_def : thm
@@ -50,14 +48,6 @@ sig
 (*
    [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs"
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [hashmap_hash_key_fwd_def]  Definition
       
       ⊢ ∀k. hashmap_hash_key_fwd k = Return k
@@ -506,7 +496,7 @@ sig
       ⊢ ∀self.
           hashmap_hash_map_try_resize_fwd_back self =
           do
-            max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+            max_usize <- mk_usize (u32_to_int core_u32_max);
             capacity <<- vec_len self.hashmap_hash_map_slots;
             n1 <- usize_div max_usize (int_to_usize 2);
             (i,i0) <<- self.hashmap_hash_map_max_load_factor;
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/misc-constants/constantsScript.sml
index d589d348..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/misc-constants/constantsScript.sml
@@ -13,17 +13,9 @@ Definition x0_c_def:
   x0_c : u32 = get_return_value x0_body
 End
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 (** [constants::X1] *)
 Definition x1_body_def:
-  x1_body : u32 result = Return core_num_u32_max_c
+  x1_body : u32 result = Return core_u32_max
 End
 Definition x1_c_def:
   x1_c : u32 = get_return_value x1_body
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 149d7e22..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -4,8 +4,6 @@ sig
   
   (*  Definitions  *)
     val add_fwd_def : thm
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val get_z1_fwd_def : thm
     val get_z1_z1_body_def : thm
     val get_z1_z1_c_def : thm
@@ -110,14 +108,6 @@ sig
       
       ⊢ ∀a b. add_fwd a b = i32_add a b
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [get_z1_fwd_def]  Definition
       
       ⊢ get_z1_fwd = Return get_z1_z1_c
@@ -321,7 +311,7 @@ sig
    
    [x1_body_def]  Definition
       
-      ⊢ x1_body = Return core_num_u32_max_c
+      ⊢ x1_body = Return core_u32_max
    
    [x1_c_def]  Definition