Update the HOL4 proofs for the last *release* version of HOL4

6 files changed, 327 insertions, 325 deletions

diff --git a/tests/hol4/betree/betreeMain_TypesTheory.sig b/tests/hol4/betree/betreeMain_TypesTheory.sig
index 5cbe4c6b..a451eae9 100644
--- a/tests/hol4/betree/betreeMain_TypesTheory.sig
+++ b/tests/hol4/betree/betreeMain_TypesTheory.sig
@@ -4,11 +4,29 @@ sig
   
   (*  Definitions  *)
     val betree_be_tree_t_TY_DEF : thm
+    val betree_be_tree_t_betree_be_tree_node_id_cnt : thm
+    val betree_be_tree_t_betree_be_tree_node_id_cnt_fupd : thm
+    val betree_be_tree_t_betree_be_tree_params : thm
+    val betree_be_tree_t_betree_be_tree_params_fupd : thm
+    val betree_be_tree_t_betree_be_tree_root : thm
+    val betree_be_tree_t_betree_be_tree_root_fupd : thm
     val betree_be_tree_t_case_def : thm
     val betree_be_tree_t_size_def : thm
     val betree_internal_t_TY_DEF : thm
+    val betree_internal_t_betree_internal_id : thm
+    val betree_internal_t_betree_internal_id_fupd : thm
+    val betree_internal_t_betree_internal_left : thm
+    val betree_internal_t_betree_internal_left_fupd : thm
+    val betree_internal_t_betree_internal_pivot : thm
+    val betree_internal_t_betree_internal_pivot_fupd : thm
+    val betree_internal_t_betree_internal_right : thm
+    val betree_internal_t_betree_internal_right_fupd : thm
     val betree_internal_t_case_def : thm
     val betree_leaf_t_TY_DEF : thm
+    val betree_leaf_t_betree_leaf_id : thm
+    val betree_leaf_t_betree_leaf_id_fupd : thm
+    val betree_leaf_t_betree_leaf_size : thm
+    val betree_leaf_t_betree_leaf_size_fupd : thm
     val betree_leaf_t_case_def : thm
     val betree_leaf_t_size_def : thm
     val betree_list_t_TY_DEF : thm
@@ -18,41 +36,23 @@ sig
     val betree_message_t_case_def : thm
     val betree_message_t_size_def : thm
     val betree_node_id_counter_t_TY_DEF : thm
+    val betree_node_id_counter_t_betree_node_id_counter_next_node_id : thm
+    val betree_node_id_counter_t_betree_node_id_counter_next_node_id_fupd : thm
     val betree_node_id_counter_t_case_def : thm
     val betree_node_id_counter_t_size_def : thm
     val betree_node_t_TY_DEF : thm
     val betree_node_t_case_def : thm
     val betree_node_t_size_def : thm
     val betree_params_t_TY_DEF : thm
+    val betree_params_t_betree_params_min_flush_size : thm
+    val betree_params_t_betree_params_min_flush_size_fupd : thm
+    val betree_params_t_betree_params_split_size : thm
+    val betree_params_t_betree_params_split_size_fupd : thm
     val betree_params_t_case_def : thm
     val betree_params_t_size_def : thm
     val betree_upsert_fun_state_t_TY_DEF : thm
     val betree_upsert_fun_state_t_case_def : thm
     val betree_upsert_fun_state_t_size_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def : thm
-    val recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_id_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_left_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_pivot_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_right_def : thm
-    val recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def : thm
-    val recordtype_betree_leaf_t_seldef_betree_leaf_id_def : thm
-    val recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def : thm
-    val recordtype_betree_leaf_t_seldef_betree_leaf_size_def : thm
-    val recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def : thm
-    val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def : thm
-    val recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def : thm
-    val recordtype_betree_params_t_seldef_betree_params_min_flush_size_def : thm
-    val recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def : thm
-    val recordtype_betree_params_t_seldef_betree_params_split_size_def : thm
-    val recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def : thm
   
   (*  Theorems  *)
     val EXISTS_betree_be_tree_t : thm
@@ -204,6 +204,38 @@ sig
                       $var$('betree_be_tree_t') a0') ⇒
                    $var$('betree_be_tree_t') a0') rep
    
+   [betree_be_tree_t_betree_be_tree_node_id_cnt]  Definition
+      
+      ⊢ ∀b b0 b1.
+          (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0
+   
+   [betree_be_tree_t_betree_be_tree_node_id_cnt_fupd]  Definition
+      
+      ⊢ ∀f b b0 b1.
+          betree_be_tree_t b b0 b1 with
+          betree_be_tree_node_id_cnt updated_by f =
+          betree_be_tree_t b (f b0) b1
+   
+   [betree_be_tree_t_betree_be_tree_params]  Definition
+      
+      ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b
+   
+   [betree_be_tree_t_betree_be_tree_params_fupd]  Definition
+      
+      ⊢ ∀f b b0 b1.
+          betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f =
+          betree_be_tree_t (f b) b0 b1
+   
+   [betree_be_tree_t_betree_be_tree_root]  Definition
+      
+      ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1
+   
+   [betree_be_tree_t_betree_be_tree_root_fupd]  Definition
+      
+      ⊢ ∀f b b0 b1.
+          betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f =
+          betree_be_tree_t b b0 (f b1)
+   
    [betree_be_tree_t_case_def]  Definition
       
       ⊢ ∀a0 a1 a2 f.
@@ -246,6 +278,51 @@ sig
                       $var$('betree_internal_t') a1') ⇒
                    $var$('betree_internal_t') a1') rep
    
+   [betree_internal_t_betree_internal_id]  Definition
+      
+      ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u
+   
+   [betree_internal_t_betree_internal_id_fupd]  Definition
+      
+      ⊢ ∀f u u0 b b0.
+          betree_internal_t u u0 b b0 with betree_internal_id updated_by f =
+          betree_internal_t (f u) u0 b b0
+   
+   [betree_internal_t_betree_internal_left]  Definition
+      
+      ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b
+   
+   [betree_internal_t_betree_internal_left_fupd]  Definition
+      
+      ⊢ ∀f u u0 b b0.
+          betree_internal_t u u0 b b0 with
+          betree_internal_left updated_by f =
+          betree_internal_t u u0 (f b) b0
+   
+   [betree_internal_t_betree_internal_pivot]  Definition
+      
+      ⊢ ∀u u0 b b0.
+          (betree_internal_t u u0 b b0).betree_internal_pivot = u0
+   
+   [betree_internal_t_betree_internal_pivot_fupd]  Definition
+      
+      ⊢ ∀f u u0 b b0.
+          betree_internal_t u u0 b b0 with
+          betree_internal_pivot updated_by f =
+          betree_internal_t u (f u0) b b0
+   
+   [betree_internal_t_betree_internal_right]  Definition
+      
+      ⊢ ∀u u0 b b0.
+          (betree_internal_t u u0 b b0).betree_internal_right = b0
+   
+   [betree_internal_t_betree_internal_right_fupd]  Definition
+      
+      ⊢ ∀f u u0 b b0.
+          betree_internal_t u u0 b b0 with
+          betree_internal_right updated_by f =
+          betree_internal_t u u0 b (f b0)
+   
    [betree_internal_t_case_def]  Definition
       
       ⊢ ∀a0 a1 a2 a3 f.
@@ -267,6 +344,26 @@ sig
                       $var$('betree_leaf_t') a0') ⇒
                    $var$('betree_leaf_t') a0') rep
    
+   [betree_leaf_t_betree_leaf_id]  Definition
+      
+      ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_id = u
+   
+   [betree_leaf_t_betree_leaf_id_fupd]  Definition
+      
+      ⊢ ∀f u u0.
+          betree_leaf_t u u0 with betree_leaf_id updated_by f =
+          betree_leaf_t (f u) u0
+   
+   [betree_leaf_t_betree_leaf_size]  Definition
+      
+      ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0
+   
+   [betree_leaf_t_betree_leaf_size_fupd]  Definition
+      
+      ⊢ ∀f u u0.
+          betree_leaf_t u u0 with betree_leaf_size updated_by f =
+          betree_leaf_t u (f u0)
+   
    [betree_leaf_t_case_def]  Definition
       
       ⊢ ∀a0 a1 f. betree_leaf_t_CASE (betree_leaf_t a0 a1) f = f a0 a1
@@ -355,6 +452,19 @@ sig
                       $var$('betree_node_id_counter_t') a0) ⇒
                    $var$('betree_node_id_counter_t') a0) rep
    
+   [betree_node_id_counter_t_betree_node_id_counter_next_node_id]  Definition
+      
+      ⊢ ∀u. (betree_node_id_counter_t u).
+            betree_node_id_counter_next_node_id =
+            u
+   
+   [betree_node_id_counter_t_betree_node_id_counter_next_node_id_fupd]  Definition
+      
+      ⊢ ∀f u.
+          betree_node_id_counter_t u with
+          betree_node_id_counter_next_node_id updated_by f =
+          betree_node_id_counter_t (f u)
+   
    [betree_node_id_counter_t_case_def]  Definition
       
       ⊢ ∀a f.
@@ -424,6 +534,27 @@ sig
                       $var$('betree_params_t') a0') ⇒
                    $var$('betree_params_t') a0') rep
    
+   [betree_params_t_betree_params_min_flush_size]  Definition
+      
+      ⊢ ∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u
+   
+   [betree_params_t_betree_params_min_flush_size_fupd]  Definition
+      
+      ⊢ ∀f u u0.
+          betree_params_t u u0 with
+          betree_params_min_flush_size updated_by f =
+          betree_params_t (f u) u0
+   
+   [betree_params_t_betree_params_split_size]  Definition
+      
+      ⊢ ∀u u0. (betree_params_t u u0).betree_params_split_size = u0
+   
+   [betree_params_t_betree_params_split_size_fupd]  Definition
+      
+      ⊢ ∀f u u0.
+          betree_params_t u u0 with betree_params_split_size updated_by f =
+          betree_params_t u (f u0)
+   
    [betree_params_t_case_def]  Definition
       
       ⊢ ∀a0 a1 f. betree_params_t_CASE (betree_params_t a0 a1) f = f a0 a1
@@ -463,137 +594,6 @@ sig
       ⊢ (∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateAdd a) = 1) ∧
         ∀a. betree_upsert_fun_state_t_size (BetreeUpsertFunStateSub a) = 1
    
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_def]  Definition
-      
-      ⊢ ∀b b0 b1.
-          (betree_be_tree_t b b0 b1).betree_be_tree_node_id_cnt = b0
-   
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_node_id_cnt_fupd_def]  Definition
-      
-      ⊢ ∀f b b0 b1.
-          betree_be_tree_t b b0 b1 with
-          betree_be_tree_node_id_cnt updated_by f =
-          betree_be_tree_t b (f b0) b1
-   
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_def]  Definition
-      
-      ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_params = b
-   
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_params_fupd_def]  Definition
-      
-      ⊢ ∀f b b0 b1.
-          betree_be_tree_t b b0 b1 with betree_be_tree_params updated_by f =
-          betree_be_tree_t (f b) b0 b1
-   
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_def]  Definition
-      
-      ⊢ ∀b b0 b1. (betree_be_tree_t b b0 b1).betree_be_tree_root = b1
-   
-   [recordtype_betree_be_tree_t_seldef_betree_be_tree_root_fupd_def]  Definition
-      
-      ⊢ ∀f b b0 b1.
-          betree_be_tree_t b b0 b1 with betree_be_tree_root updated_by f =
-          betree_be_tree_t b b0 (f b1)
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_id_def]  Definition
-      
-      ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_id = u
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_id_fupd_def]  Definition
-      
-      ⊢ ∀f u u0 b b0.
-          betree_internal_t u u0 b b0 with betree_internal_id updated_by f =
-          betree_internal_t (f u) u0 b b0
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_left_def]  Definition
-      
-      ⊢ ∀u u0 b b0. (betree_internal_t u u0 b b0).betree_internal_left = b
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_left_fupd_def]  Definition
-      
-      ⊢ ∀f u u0 b b0.
-          betree_internal_t u u0 b b0 with
-          betree_internal_left updated_by f =
-          betree_internal_t u u0 (f b) b0
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_pivot_def]  Definition
-      
-      ⊢ ∀u u0 b b0.
-          (betree_internal_t u u0 b b0).betree_internal_pivot = u0
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_pivot_fupd_def]  Definition
-      
-      ⊢ ∀f u u0 b b0.
-          betree_internal_t u u0 b b0 with
-          betree_internal_pivot updated_by f =
-          betree_internal_t u (f u0) b b0
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_right_def]  Definition
-      
-      ⊢ ∀u u0 b b0.
-          (betree_internal_t u u0 b b0).betree_internal_right = b0
-   
-   [recordtype_betree_internal_t_seldef_betree_internal_right_fupd_def]  Definition
-      
-      ⊢ ∀f u u0 b b0.
-          betree_internal_t u u0 b b0 with
-          betree_internal_right updated_by f =
-          betree_internal_t u u0 b (f b0)
-   
-   [recordtype_betree_leaf_t_seldef_betree_leaf_id_def]  Definition
-      
-      ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_id = u
-   
-   [recordtype_betree_leaf_t_seldef_betree_leaf_id_fupd_def]  Definition
-      
-      ⊢ ∀f u u0.
-          betree_leaf_t u u0 with betree_leaf_id updated_by f =
-          betree_leaf_t (f u) u0
-   
-   [recordtype_betree_leaf_t_seldef_betree_leaf_size_def]  Definition
-      
-      ⊢ ∀u u0. (betree_leaf_t u u0).betree_leaf_size = u0
-   
-   [recordtype_betree_leaf_t_seldef_betree_leaf_size_fupd_def]  Definition
-      
-      ⊢ ∀f u u0.
-          betree_leaf_t u u0 with betree_leaf_size updated_by f =
-          betree_leaf_t u (f u0)
-   
-   [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_def]  Definition
-      
-      ⊢ ∀u. (betree_node_id_counter_t u).
-            betree_node_id_counter_next_node_id =
-            u
-   
-   [recordtype_betree_node_id_counter_t_seldef_betree_node_id_counter_next_node_id_fupd_def]  Definition
-      
-      ⊢ ∀f u.
-          betree_node_id_counter_t u with
-          betree_node_id_counter_next_node_id updated_by f =
-          betree_node_id_counter_t (f u)
-   
-   [recordtype_betree_params_t_seldef_betree_params_min_flush_size_def]  Definition
-      
-      ⊢ ∀u u0. (betree_params_t u u0).betree_params_min_flush_size = u
-   
-   [recordtype_betree_params_t_seldef_betree_params_min_flush_size_fupd_def]  Definition
-      
-      ⊢ ∀f u u0.
-          betree_params_t u u0 with
-          betree_params_min_flush_size updated_by f =
-          betree_params_t (f u) u0
-   
-   [recordtype_betree_params_t_seldef_betree_params_split_size_def]  Definition
-      
-      ⊢ ∀u u0. (betree_params_t u u0).betree_params_split_size = u0
-   
-   [recordtype_betree_params_t_seldef_betree_params_split_size_fupd_def]  Definition
-      
-      ⊢ ∀f u u0.
-          betree_params_t u u0 with betree_params_split_size updated_by f =
-          betree_params_t u (f u0)
-   
    [EXISTS_betree_be_tree_t]  Theorem
       
       ⊢ ∀P. (∃b. P b) ⇔
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index c8e87f07..7259f2f5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1040,7 +1040,7 @@ QED
 
 (* TODO: the names introduced by progress are random, which is confusing.
    It also makes the proofs less stable.
-   Try to use the names given by the let-bindings. *)
+   Update the progress tactic to use the names given by the let-bindings. *)
 
 Theorem hash_map_move_elements_loop_fwd_back_spec_aux:
   ∀ hm slots i n.
@@ -1138,16 +1138,17 @@ Proof
     fs [])
   >-(
     (* Prove that index j (update slots i) = index j slots *)
-    pop_assum (qspec_assume ‘int_to_usize j’) >> gvs [] >> massage >> gvs [] >>
+    first_x_assum (qspec_assume ‘int_to_usize j’) >> gvs [] >> massage >> gvs [] >>
     fs [vec_len_def] >>
     massage >> gvs [] >>
     sg ‘j ≠ usize_to_int i’ >- int_tac >> gvs [vec_index_def, vec_update_def] >>
     massage >>
     (* Use the fact that slot_t_lookup k (index i ... slots) = NONE *)
-    last_x_assum (qspec_assume ‘k’) >>
+    first_x_assum (qspec_assume ‘k’) >>
     first_assum sg_premise_tac
     >- (
       sg ‘usize_to_int i < j’ >- int_tac >> fs [] >>
+      sg ‘usize_to_int i ≤ j’ >- int_tac >> fs [] >>
       (* TODO: we have to rewrite key_MEM_j_lookup_i_is_NONE before applying
          metis_tac *)
       assume_tac key_MEM_j_lookup_i_is_NONE >> fs [] >>
@@ -1156,7 +1157,8 @@ Proof
     (* Use the fact that as the key is in the slots after i, it can't be in “hm” (yet) *)
     last_x_assum (qspec_assume ‘j’) >> gvs [] >>
     first_x_assum sg_premise_tac >- (int_tac) >> gvs [] >>
-    first_x_assum imp_res_tac) >>
+    first_x_assum imp_res_tac >>
+    metis_tac []) >>
   (* The conclusion of the theorem (the post-condition) *)
   conj_tac
   >-(
diff --git a/tests/hol4/hashmap/hashmap_TypesTheory.sig b/tests/hol4/hashmap/hashmap_TypesTheory.sig
index 4ad77ac5..a8839fa4 100644
--- a/tests/hol4/hashmap/hashmap_TypesTheory.sig
+++ b/tests/hol4/hashmap/hashmap_TypesTheory.sig
@@ -5,18 +5,18 @@ sig
   (*  Definitions  *)
     val hash_map_t_TY_DEF : thm
     val hash_map_t_case_def : thm
+    val hash_map_t_hash_map_max_load : thm
+    val hash_map_t_hash_map_max_load_factor : thm
+    val hash_map_t_hash_map_max_load_factor_fupd : thm
+    val hash_map_t_hash_map_max_load_fupd : thm
+    val hash_map_t_hash_map_num_entries : thm
+    val hash_map_t_hash_map_num_entries_fupd : thm
+    val hash_map_t_hash_map_slots : thm
+    val hash_map_t_hash_map_slots_fupd : thm
     val hash_map_t_size_def : thm
     val list_t_TY_DEF : thm
     val list_t_case_def : thm
     val list_t_size_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_max_load_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_max_load_factor_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_num_entries_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_slots_def : thm
-    val recordtype_hash_map_t_seldef_hash_map_slots_fupd_def : thm
   
   (*  Theorems  *)
     val EXISTS_hash_map_t : thm
@@ -72,6 +72,46 @@ sig
       ⊢ ∀a0 a1 a2 a3 f.
           hash_map_t_CASE (hash_map_t a0 a1 a2 a3) f = f a0 a1 a2 a3
    
+   [hash_map_t_hash_map_max_load]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0
+   
+   [hash_map_t_hash_map_max_load_factor]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p
+   
+   [hash_map_t_hash_map_max_load_factor_fupd]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
+          hash_map_t u (f p) u0 v
+   
+   [hash_map_t_hash_map_max_load_fupd]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_max_load updated_by f =
+          hash_map_t u p (f u0) v
+   
+   [hash_map_t_hash_map_num_entries]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u
+   
+   [hash_map_t_hash_map_num_entries_fupd]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_num_entries updated_by f =
+          hash_map_t (f u) p u0 v
+   
+   [hash_map_t_hash_map_slots]  Definition
+      
+      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
+   
+   [hash_map_t_hash_map_slots_fupd]  Definition
+      
+      ⊢ ∀f u p u0 v.
+          hash_map_t u p u0 v with hash_map_slots updated_by f =
+          hash_map_t u p u0 (f v)
+   
    [hash_map_t_size_def]  Definition
       
       ⊢ ∀f a0 a1 a2 a3.
@@ -108,46 +148,6 @@ sig
            list_t_size f (ListCons a0 a1 a2) =
            1 + (f a1 + list_t_size f a2)) ∧ ∀f. list_t_size f ListNil = 0
    
-   [recordtype_hash_map_t_seldef_hash_map_max_load_def]  Definition
-      
-      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load = u0
-   
-   [recordtype_hash_map_t_seldef_hash_map_max_load_factor_def]  Definition
-      
-      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_max_load_factor = p
-   
-   [recordtype_hash_map_t_seldef_hash_map_max_load_factor_fupd_def]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hash_map_t u p u0 v with hash_map_max_load_factor updated_by f =
-          hash_map_t u (f p) u0 v
-   
-   [recordtype_hash_map_t_seldef_hash_map_max_load_fupd_def]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hash_map_t u p u0 v with hash_map_max_load updated_by f =
-          hash_map_t u p (f u0) v
-   
-   [recordtype_hash_map_t_seldef_hash_map_num_entries_def]  Definition
-      
-      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_num_entries = u
-   
-   [recordtype_hash_map_t_seldef_hash_map_num_entries_fupd_def]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hash_map_t u p u0 v with hash_map_num_entries updated_by f =
-          hash_map_t (f u) p u0 v
-   
-   [recordtype_hash_map_t_seldef_hash_map_slots_def]  Definition
-      
-      ⊢ ∀u p u0 v. (hash_map_t u p u0 v).hash_map_slots = v
-   
-   [recordtype_hash_map_t_seldef_hash_map_slots_fupd_def]  Definition
-      
-      ⊢ ∀f u p u0 v.
-          hash_map_t u p u0 v with hash_map_slots updated_by f =
-          hash_map_t u p u0 (f v)
-   
    [EXISTS_hash_map_t]  Theorem
       
       ⊢ ∀P. (∃h. P h) ⇔
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
index bea7eb76..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
@@ -5,18 +5,18 @@ sig
   (*  Definitions  *)
     val hashmap_hash_map_t_TY_DEF : thm
     val hashmap_hash_map_t_case_def : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_max_load_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_num_entries : thm
+    val hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd : thm
+    val hashmap_hash_map_t_hashmap_hash_map_slots : thm
+    val hashmap_hash_map_t_hashmap_hash_map_slots_fupd : thm
     val hashmap_hash_map_t_size_def : thm
     val hashmap_list_t_TY_DEF : thm
     val hashmap_list_t_case_def : thm
     val hashmap_list_t_size_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def : thm
-    val recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def : thm
   
   (*  Theorems  *)
     val EXISTS_hashmap_hash_map_t : thm
@@ -73,92 +73,92 @@ sig
           hashmap_hash_map_t_CASE (hashmap_hash_map_t a0 a1 a2 a3) f =
           f a0 a1 a2 a3
    
-   [hashmap_hash_map_t_size_def]  Definition
-      
-      ⊢ ∀f a0 a1 a2 a3.
-          hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
-          1 + pair_size (λv. 0) (λv. 0) a1
-   
-   [hashmap_list_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('hashmap_list_t').
-                   (∀a0'.
-                      (∃a0 a1 a2.
-                         a0' =
-                         (λa0 a1 a2.
-                              ind_type$CONSTR 0 (a0,a1)
-                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
-                           a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) (ARB,ARB)
-                        (λn. ind_type$BOTTOM) ⇒
-                      $var$('hashmap_list_t') a0') ⇒
-                   $var$('hashmap_list_t') a0') rep
-   
-   [hashmap_list_t_case_def]  Definition
-      
-      ⊢ (∀a0 a1 a2 f v.
-           hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
-        ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
-   
-   [hashmap_list_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1 a2.
-           hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
-           1 + (f a1 + hashmap_list_t_size f a2)) ∧
-        ∀f. hashmap_list_t_size f HashmapListNil = 0
-   
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load = u0
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_max_load_factor =
           p
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_factor_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_factor_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_max_load_factor updated_by f =
           hashmap_hash_map_t u (f p) u0 v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_max_load_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_max_load_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_max_load updated_by f =
           hashmap_hash_map_t u p (f u0) v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_num_entries]  Definition
       
       ⊢ ∀u p u0 v.
           (hashmap_hash_map_t u p u0 v).hashmap_hash_map_num_entries = u
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_num_entries_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_num_entries_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_num_entries updated_by f =
           hashmap_hash_map_t (f u) p u0 v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_slots]  Definition
       
       ⊢ ∀u p u0 v. (hashmap_hash_map_t u p u0 v).hashmap_hash_map_slots = v
    
-   [recordtype_hashmap_hash_map_t_seldef_hashmap_hash_map_slots_fupd_def]  Definition
+   [hashmap_hash_map_t_hashmap_hash_map_slots_fupd]  Definition
       
       ⊢ ∀f u p u0 v.
           hashmap_hash_map_t u p u0 v with
           hashmap_hash_map_slots updated_by f =
           hashmap_hash_map_t u p u0 (f v)
    
+   [hashmap_hash_map_t_size_def]  Definition
+      
+      ⊢ ∀f a0 a1 a2 a3.
+          hashmap_hash_map_t_size f (hashmap_hash_map_t a0 a1 a2 a3) =
+          1 + pair_size (λv. 0) (λv. 0) a1
+   
+   [hashmap_list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('hashmap_list_t').
+                   (∀a0'.
+                      (∃a0 a1 a2.
+                         a0' =
+                         (λa0 a1 a2.
+                              ind_type$CONSTR 0 (a0,a1)
+                                (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
+                           a0 a1 a2 ∧ $var$('hashmap_list_t') a2) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) (ARB,ARB)
+                        (λn. ind_type$BOTTOM) ⇒
+                      $var$('hashmap_list_t') a0') ⇒
+                   $var$('hashmap_list_t') a0') rep
+   
+   [hashmap_list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 a2 f v.
+           hashmap_list_t_CASE (HashmapListCons a0 a1 a2) f v = f a0 a1 a2) ∧
+        ∀f v. hashmap_list_t_CASE HashmapListNil f v = v
+   
+   [hashmap_list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1 a2.
+           hashmap_list_t_size f (HashmapListCons a0 a1 a2) =
+           1 + (f a1 + hashmap_list_t_size f a2)) ∧
+        ∀f. hashmap_list_t_size f HashmapListNil = 0
+   
    [EXISTS_hashmap_hash_map_t]  Theorem
       
       ⊢ ∀P. (∃h. P h) ⇔
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 6148221f..149d7e22 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -23,6 +23,10 @@ sig
     val p3_c_def : thm
     val pair_t_TY_DEF : thm
     val pair_t_case_def : thm
+    val pair_t_pair_x : thm
+    val pair_t_pair_x_fupd : thm
+    val pair_t_pair_y : thm
+    val pair_t_pair_y_fupd : thm
     val pair_t_size_def : thm
     val q1_body_def : thm
     val q1_c_def : thm
@@ -30,12 +34,6 @@ sig
     val q2_c_def : thm
     val q3_body_def : thm
     val q3_c_def : thm
-    val recordtype_pair_t_seldef_pair_x_def : thm
-    val recordtype_pair_t_seldef_pair_x_fupd_def : thm
-    val recordtype_pair_t_seldef_pair_y_def : thm
-    val recordtype_pair_t_seldef_pair_y_fupd_def : thm
-    val recordtype_wrap_t_seldef_wrap_val_def : thm
-    val recordtype_wrap_t_seldef_wrap_val_fupd_def : thm
     val s1_body_def : thm
     val s1_c_def : thm
     val s2_body_def : thm
@@ -49,6 +47,8 @@ sig
     val wrap_t_TY_DEF : thm
     val wrap_t_case_def : thm
     val wrap_t_size_def : thm
+    val wrap_t_wrap_val : thm
+    val wrap_t_wrap_val_fupd : thm
     val x0_body_def : thm
     val x0_c_def : thm
     val x1_body_def : thm
@@ -198,6 +198,22 @@ sig
       
       ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1
    
+   [pair_t_pair_x]  Definition
+      
+      ⊢ ∀t t0. (pair_t t t0).pair_x = t
+   
+   [pair_t_pair_x_fupd]  Definition
+      
+      ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0
+   
+   [pair_t_pair_y]  Definition
+      
+      ⊢ ∀t t0. (pair_t t t0).pair_y = t0
+   
+   [pair_t_pair_y_fupd]  Definition
+      
+      ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
+   
    [pair_t_size_def]  Definition
       
       ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1)
@@ -226,30 +242,6 @@ sig
       
       ⊢ q3_c = get_return_value q3_body
    
-   [recordtype_pair_t_seldef_pair_x_def]  Definition
-      
-      ⊢ ∀t t0. (pair_t t t0).pair_x = t
-   
-   [recordtype_pair_t_seldef_pair_x_fupd_def]  Definition
-      
-      ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0
-   
-   [recordtype_pair_t_seldef_pair_y_def]  Definition
-      
-      ⊢ ∀t t0. (pair_t t t0).pair_y = t0
-   
-   [recordtype_pair_t_seldef_pair_y_fupd_def]  Definition
-      
-      ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
-   
-   [recordtype_wrap_t_seldef_wrap_val_def]  Definition
-      
-      ⊢ ∀t. (wrap_t t).wrap_val = t
-   
-   [recordtype_wrap_t_seldef_wrap_val_fupd_def]  Definition
-      
-      ⊢ ∀f t. wrap_t t with wrap_val updated_by f = wrap_t (f t)
-   
    [s1_body_def]  Definition
       
       ⊢ s1_body = Return (int_to_u32 6)
@@ -311,6 +303,14 @@ sig
       
       ⊢ ∀f a. wrap_t_size f (wrap_t a) = 1 + f a
    
+   [wrap_t_wrap_val]  Definition
+      
+      ⊢ ∀t. (wrap_t t).wrap_val = t
+   
+   [wrap_t_wrap_val_fupd]  Definition
+      
+      ⊢ ∀f t. wrap_t t with wrap_val updated_by f = wrap_t (f t)
+   
    [x0_body_def]  Definition
       
       ⊢ x0_body = Return (int_to_u32 0)
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
index 82c842be..c0ff4e09 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
+++ b/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
@@ -53,15 +53,11 @@ sig
     val one_t_size_def : thm
     val pair_t_TY_DEF : thm
     val pair_t_case_def : thm
+    val pair_t_pair_x : thm
+    val pair_t_pair_x_fupd : thm
+    val pair_t_pair_y : thm
+    val pair_t_pair_y_fupd : thm
     val pair_t_size_def : thm
-    val recordtype_pair_t_seldef_pair_x_def : thm
-    val recordtype_pair_t_seldef_pair_x_fupd_def : thm
-    val recordtype_pair_t_seldef_pair_y_def : thm
-    val recordtype_pair_t_seldef_pair_y_fupd_def : thm
-    val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def : thm
-    val recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def : thm
-    val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def : thm
-    val recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def : thm
     val refs_test1_fwd_def : thm
     val refs_test2_fwd_def : thm
     val rem_test_fwd_def : thm
@@ -69,9 +65,13 @@ sig
     val struct_with_pair_t_TY_DEF : thm
     val struct_with_pair_t_case_def : thm
     val struct_with_pair_t_size_def : thm
+    val struct_with_pair_t_struct_with_pair_p : thm
+    val struct_with_pair_t_struct_with_pair_p_fupd : thm
     val struct_with_tuple_t_TY_DEF : thm
     val struct_with_tuple_t_case_def : thm
     val struct_with_tuple_t_size_def : thm
+    val struct_with_tuple_t_struct_with_tuple_p : thm
+    val struct_with_tuple_t_struct_with_tuple_p_fupd : thm
     val subs_test_fwd_def : thm
     val sum_t_TY_DEF : thm
     val sum_t_case_def : thm
@@ -577,45 +577,25 @@ sig
       
       ⊢ ∀a0 a1 f. pair_t_CASE (pair_t a0 a1) f = f a0 a1
    
-   [pair_t_size_def]  Definition
-      
-      ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1)
-   
-   [recordtype_pair_t_seldef_pair_x_def]  Definition
+   [pair_t_pair_x]  Definition
       
       ⊢ ∀t t0. (pair_t t t0).pair_x = t
    
-   [recordtype_pair_t_seldef_pair_x_fupd_def]  Definition
+   [pair_t_pair_x_fupd]  Definition
       
       ⊢ ∀f t t0. pair_t t t0 with pair_x updated_by f = pair_t (f t) t0
    
-   [recordtype_pair_t_seldef_pair_y_def]  Definition
+   [pair_t_pair_y]  Definition
       
       ⊢ ∀t t0. (pair_t t t0).pair_y = t0
    
-   [recordtype_pair_t_seldef_pair_y_fupd_def]  Definition
+   [pair_t_pair_y_fupd]  Definition
       
       ⊢ ∀f t t0. pair_t t t0 with pair_y updated_by f = pair_t t (f t0)
    
-   [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_def]  Definition
-      
-      ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
-   
-   [recordtype_struct_with_pair_t_seldef_struct_with_pair_p_fupd_def]  Definition
-      
-      ⊢ ∀f p.
-          struct_with_pair_t p with struct_with_pair_p updated_by f =
-          struct_with_pair_t (f p)
-   
-   [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_def]  Definition
-      
-      ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
-   
-   [recordtype_struct_with_tuple_t_seldef_struct_with_tuple_p_fupd_def]  Definition
+   [pair_t_size_def]  Definition
       
-      ⊢ ∀f p.
-          struct_with_tuple_t p with struct_with_tuple_p updated_by f =
-          struct_with_tuple_t (f p)
+      ⊢ ∀f f1 a0 a1. pair_t_size f f1 (pair_t a0 a1) = 1 + (f a0 + f1 a1)
    
    [refs_test1_fwd_def]  Definition
       
@@ -665,6 +645,16 @@ sig
           struct_with_pair_t_size f f1 (struct_with_pair_t a) =
           1 + pair_t_size f f1 a
    
+   [struct_with_pair_t_struct_with_pair_p]  Definition
+      
+      ⊢ ∀p. (struct_with_pair_t p).struct_with_pair_p = p
+   
+   [struct_with_pair_t_struct_with_pair_p_fupd]  Definition
+      
+      ⊢ ∀f p.
+          struct_with_pair_t p with struct_with_pair_p updated_by f =
+          struct_with_pair_t (f p)
+   
    [struct_with_tuple_t_TY_DEF]  Definition
       
       ⊢ ∃rep.
@@ -688,6 +678,16 @@ sig
           struct_with_tuple_t_size f f1 (struct_with_tuple_t a) =
           1 + pair_size f f1 a
    
+   [struct_with_tuple_t_struct_with_tuple_p]  Definition
+      
+      ⊢ ∀p. (struct_with_tuple_t p).struct_with_tuple_p = p
+   
+   [struct_with_tuple_t_struct_with_tuple_p_fupd]  Definition
+      
+      ⊢ ∀f p.
+          struct_with_tuple_t p with struct_with_tuple_p updated_by f =
+          struct_with_tuple_t (f p)
+   
    [subs_test_fwd_def]  Definition
       
       ⊢ ∀x y. subs_test_fwd x y = u32_sub x y