From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/betree/betreeMain_FunsScript.sml | 12 ++----------
 tests/hol4/betree/betreeMain_FunsTheory.sig | 14 ++------------
 2 files changed, 4 insertions(+), 22 deletions(-)

(limited to 'tests/hol4/betree')

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 ()
-- 
cgit v1.2.3