Make the theorems used by the progress tactic persistent

8 files changed, 285 insertions, 186 deletions

diff --git a/backends/hol4/evalLib.sig b/backends/hol4/evalLib.sig
index f44cff13..40183af8 100644
--- a/backends/hol4/evalLib.sig
+++ b/backends/hol4/evalLib.sig
@@ -8,6 +8,14 @@ sig
 
   include Abbrev
 
+  (* The following functions allow to *persistently* register custom rewriting theorems.
+
+     Remark: it is important that we allow to save rewriting theorems without forcing
+     the user to save them in, say, srw_ss.
+   *)
+  val add_rewrite_thm : thm -> unit
+  val add_rewrite_thms : thm list -> unit
+
   (* The following functions allow to *persistently* register custom unfolding theorems *)
   val add_unfold_thm : thm -> unit
   val add_unfold_thms : thm list -> unit
diff --git a/backends/hol4/evalLib.sml b/backends/hol4/evalLib.sml
index 85a6b94a..f9e758c9 100644
--- a/backends/hol4/evalLib.sml
+++ b/backends/hol4/evalLib.sml
@@ -27,61 +27,113 @@ fun get_const_name (tm : term) : const_name =
     (thy, name)
   end
 
-(* Create the persistent collection, which is a pair:
+(* Create the persistent collection of rewrite theorems - TODO: more efficient
+   collection than a list? *)
+val (add_rewrite_thm, get_rewrite_thms) =
+  let
+    (* Small helper *)
+    fun add_to_state (th : thm) s = th :: s
+
+    (* Persistently update the maps given a delta  *)
+    fun apply_delta (delta : ThmSetData.setdelta) st =
+      case delta of
+        ThmSetData.ADD (_, th) => add_to_state th st
+      | ThmSetData.REMOVE _ =>
+        raise mk_HOL_ERR "evalLib" "apply_delta" ("Unexpected REMOVE")
+
+    (* Initialize the collection *)
+    val init_state = []
+    val {update_global_value, (* Local update *)
+         record_delta, (* Global update *)
+         get_global_value = get_rewrite_thms,
+         ...} =
+        ThmSetData.export_with_ancestry {
+          settype = "evalLib_rewrite_theorems",
+          delta_ops = {apply_to_global = apply_delta,
+                       uptodate_delta = K true,
+                       thy_finaliser = NONE,
+                       initial_value = init_state,
+                       apply_delta = apply_delta}
+        }
+
+    fun add_rewrite_thm (s : string) : unit =
+      let
+        val th = saveThmsLib.lookup_thm s
+      in
+        (* Record the delta - for persistence for the future sessions *)
+        record_delta (ThmSetData.ADD th);
+        (* Update the global value - for the current session: record_delta
+           doesn't update the state of the current session *)
+        update_global_value (add_to_state (snd th))
+      end
+  in
+    (add_rewrite_thm, get_rewrite_thms)
+  end
+
+fun add_rewrite_thms (ls : string list) : unit =
+  app add_rewrite_thm ls
+
+
+(* Create the persistent collection of unfolding theorems, which is a pair:
    (set of constants, map from constant name to theorem)
  *)
-type state = term Redblackset.set * (const_name, thm) Redblackmap.dict
+type unfold_state = term Redblackset.set * (const_name, thm) Redblackmap.dict
 fun get_custom_unfold_const (th : thm) : term = (fst o strip_comb o lhs o snd o strip_forall o concl) th
 
-(* Small helper *)
-fun add_to_state (th : thm) (s, m) =
+val (add_unfold_thm, get_unfold_thms_map) =
   let
-    val k = get_custom_unfold_const th
-    val name = get_const_name k
-    val s = Redblackset.add (s, k)
-    val m = Redblackmap.insert (m, name, th)
-  in
-    (s, m)
-  end
+    (* Small helper *)
+    fun add_to_state (th : thm) (s, m) =
+      let
+        val k = get_custom_unfold_const th
+        val name = get_const_name k
+        val s = Redblackset.add (s, k)
+        val m = Redblackmap.insert (m, name, th)
+      in
+        (s, m)
+      end
 
-(* Persistently update the maps given a delta  *)
-fun apply_delta (delta : ThmSetData.setdelta) st =
-  case delta of
-    ThmSetData.ADD (_, th) => add_to_state th st
-  | ThmSetData.REMOVE _ =>
-    raise mk_HOL_ERR "saveThmsLib" "create_map" ("Unexpected REMOVE")
-
-(* Initialize the collection *)
-val init_state = (Redblackset.empty compare, Redblackmap.mkDict const_name_compare)
-val {update_global_value, (* Local update *)
-     record_delta, (* Global update *)
-     get_global_value,
-     ...} =
-    ThmSetData.export_with_ancestry {
-      settype = "custom_unfold_theorems",
-      delta_ops = {apply_to_global = apply_delta,
-                   uptodate_delta = K true,
-                   thy_finaliser = NONE,
-                   initial_value = init_state,
-                   apply_delta = apply_delta}
-    }
-
-fun add_unfold_thm (s : string) : unit =
-  let
-    val th = saveThmsLib.lookup_thm s
+    (* Persistently update the maps given a delta  *)
+    fun apply_delta (delta : ThmSetData.setdelta) st =
+      case delta of
+        ThmSetData.ADD (_, th) => add_to_state th st
+      | ThmSetData.REMOVE _ =>
+        raise mk_HOL_ERR "evalLib" "apply_delta" ("Unexpected REMOVE")
+
+    (* Initialize the collection *)
+    val init_state = (Redblackset.empty compare, Redblackmap.mkDict const_name_compare)
+    val {update_global_value, (* Local update *)
+         record_delta, (* Global update *)
+         get_global_value = get_unfold_thms_map,
+         ...} =
+        ThmSetData.export_with_ancestry {
+          settype = "evalLib_unfold_theorems",
+          delta_ops = {apply_to_global = apply_delta,
+                       uptodate_delta = K true,
+                       thy_finaliser = NONE,
+                       initial_value = init_state,
+                       apply_delta = apply_delta}
+        }
+
+    fun add_unfold_thm (s : string) : unit =
+      let
+        val th = saveThmsLib.lookup_thm s
+      in
+        (* Record the delta - for persistence for the future sessions *)
+        record_delta (ThmSetData.ADD th);
+        (* Update the global value - for the current session: record_delta
+           doesn't update the state of the current session *)
+        update_global_value (add_to_state (snd th))
+      end
   in
-    (* Record the delta - for persistence for the future sessions *)
-      record_delta (ThmSetData.ADD th);
-    (* Update the global value - for the current session: record_delta
-       doesn't update the state of the current session *)
-    update_global_value (add_to_state (snd th))
+    (add_unfold_thm, get_unfold_thms_map)
   end
 
 fun add_unfold_thms (ls : string list) : unit =
   app add_unfold_thm ls
 
 fun get_unfold_thms () : thm list =
-  map snd (Redblackmap.listItems (snd (get_global_value ())))
+  map snd (Redblackmap.listItems (snd (get_unfold_thms_map ())))
 
 (* Apply a custom unfolding to the term, if possible.
 
@@ -90,7 +142,7 @@ fun get_unfold_thms () : thm list =
 fun apply_custom_unfold (tm : term) : thm =
   let
     (* Retrieve the custom unfoldings *)
-    val custom_unfolds = snd (get_global_value ())
+    val custom_unfolds = snd (get_unfold_thms_map ())
 
     (* Remove all the matches to find the top-most scrutinee *)
     val scrut = strip_all_cases_get_scrutinee tm
@@ -148,7 +200,7 @@ fun apply_custom_unfold (tm : term) : thm =
 fun eval_conv tm =
   let
     (* TODO: optimize: we recompute the list each time... *)
-    val restr_tms = Redblackset.listItems (fst (get_global_value ()))
+    val restr_tms = Redblackset.listItems (fst (get_unfold_thms_map ()))
     (* We do the following:
        - use the standard EVAL conv, but restrains it from unfolding terms for
          which we have custom unfolding theorems
@@ -156,7 +208,7 @@ fun eval_conv tm =
        - simplify
      *)
     val standard_eval = RESTR_EVAL_CONV restr_tms
-    val simp_no_fail_conv = (fn x => SIMP_CONV (srw_ss ()) [] x handle UNCHANGED => REFL x)
+    val simp_no_fail_conv = (fn x => SIMP_CONV (srw_ss ()) (get_rewrite_thms ()) x handle UNCHANGED => REFL x)
     val one_step_conv = standard_eval THENC (apply_custom_unfold THENC simp_no_fail_conv)
     (* Wrap the conversion such that it fails if the term is unchanged *)
     fun one_step_changed_conv tm = (CHANGED_CONV one_step_conv) tm
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 776843bf..5339dec9 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -183,34 +183,6 @@ val massage : tactic =
   assume_bounds_for_all_int_vars >>
   rewrite_with_dep_int_lemmas
 
-(* The registered spec theorems, that {!progress} will automatically apply.
-
-   The keys are the function names (it is a pair, because constant names
-   are made of the theory name and the name of the constant itself).
-
-   Also note that we can store several specs per definition (in practice, when
-   looking up specs, we will try them all one by one, in a LIFO order).
-
-   We store theorems where all the premises are in the goal, with implications
-   (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not  [H0, ..., Hn ⊢ H]).
-
-   We do this because, when doing proofs by induction, {!progress} might have to
-   handle *unregistered* theorems coming the current goal assumptions and of the shape
-   (the conclusion of the theorem is an assumption, and we want to ignore this assumption):
-   {[
-     [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
-         case nth ls i of
-           Return x => ...
-         | ...      => ...]
-     ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
-         case nth ls i of
-           Return x => ...
-         | ...      => ...
-   ]}
- *)
-val reg_spec_thms: (const_name, thm) Redblackmap.dict ref =
-  ref (Redblackmap.mkDict const_name_compare)
-
 (* Retrieve the specified application in a spec theorem.
 
    A spec theorem for a function [f] typically has the shape:
@@ -249,11 +221,33 @@ fun get_spec_app (t : term) : term =
       else (fst o dest_eq) t;
   in t end
 
-(* Register a spec theorem in the spec database.
+(* Create the persistent collection of spec theorems, that {!progress} will automatically apply.
 
-   For the shape of spec theorems, see {!get_spec_thm_app}.
+   The keys are the function names (it is a pair, because constant names
+   are made of the theory name and the name of the constant itself).
+
+   Also note that we can store several specs per definition (in practice, when
+   looking up specs, we will try them all one by one, in a LIFO order).
+
+   We store theorems where all the premises are in the goal, with implications
+   (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not  [H0, ..., Hn ⊢ H]).
+
+   We do this because, when doing proofs by induction, {!progress} might have to
+   handle *unregistered* theorems coming from the current goal assumptions and of the shape
+   (the conclusion of the theorem is also present as an assumption, and we want to ignore
+    this assumption):
+   {[
+     [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
+         case nth ls i of
+           Return x => ...
+         | ...      => ...]
+     ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
+         case nth ls i of
+           Return x => ...
+         | ...      => ...
+   ]}
  *)
-fun register_spec_thm (th: thm) : unit =
+fun get_key_normalize_thm (th : thm) : const_name * thm =
   let
     (* Transform the theroem a bit before storing it *)
     val th = SPEC_ALL th;
@@ -262,95 +256,110 @@ fun register_spec_thm (th: thm) : unit =
     (* Retrieve the function name *)
     val cn = get_fun_name_from_app f;
   in
-    (* Store *)
-    reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th)
+    (* Return *)
+    (cn, th)
   end
 
+val { save_thm = save_spec_thm,
+      delete_thm = delete_spec_thm,
+      temp_save_thm = temp_save_spec_thm,
+      temp_delete_thm = temp_delete_spec_thm,
+      get_map = get_spec_thms, ... } =
+  saveThmsLib.create_map {
+    compare = const_name_compare,
+    get_key_normalize_thm = get_key_normalize_thm
+  } "spec_theorems"
+
+val save_spec_thms = app save_spec_thm
+
 val all_add_eqs = [
-  isize_add_eq,
-  i8_add_eq,
-  i16_add_eq,
-  i32_add_eq,
-  i64_add_eq,
-  i128_add_eq,
-  usize_add_eq,
-  u8_add_eq,
-  u16_add_eq,
-  u32_add_eq,
-  u64_add_eq,
-  u128_add_eq
+  "primitives.isize_add_eq",
+  "primitives.i8_add_eq",
+  "primitives.i16_add_eq",
+  "primitives.i32_add_eq",
+  "primitives.i64_add_eq",
+  "primitives.i128_add_eq",
+  "primitives.usize_add_eq",
+  "primitives.u8_add_eq",
+  "primitives.u16_add_eq",
+  "primitives.u32_add_eq",
+  "primitives.u64_add_eq",
+  "primitives.u128_add_eq"
 ]
-val _ = app register_spec_thm all_add_eqs
+val _ = save_spec_thms all_add_eqs
 
 val all_sub_eqs = [
-  isize_sub_eq,
-  i8_sub_eq,
-  i16_sub_eq,
-  i32_sub_eq,
-  i64_sub_eq,
-  i128_sub_eq,
-  usize_sub_eq,
-  u8_sub_eq,
-  u16_sub_eq,
-  u32_sub_eq,
-  u64_sub_eq,
-  u128_sub_eq
+  "primitives.isize_sub_eq",
+  "primitives.i8_sub_eq",
+  "primitives.i16_sub_eq",
+  "primitives.i32_sub_eq",
+  "primitives.i64_sub_eq",
+  "primitives.i128_sub_eq",
+  "primitives.usize_sub_eq",
+  "primitives.u8_sub_eq",
+  "primitives.u16_sub_eq",
+  "primitives.u32_sub_eq",
+  "primitives.u64_sub_eq",
+  "primitives.u128_sub_eq"
 ]
-val _ = app register_spec_thm all_sub_eqs
+val _ = save_spec_thms all_sub_eqs
 
 val all_mul_eqs = [
-  isize_mul_eq,
-  i8_mul_eq,
-  i16_mul_eq,
-  i32_mul_eq,
-  i64_mul_eq,
-  i128_mul_eq,
-  usize_mul_eq,
-  u8_mul_eq,
-  u16_mul_eq,
-  u32_mul_eq,
-  u64_mul_eq,
-  u128_mul_eq
+  "primitives.isize_mul_eq",
+  "primitives.i8_mul_eq",
+  "primitives.i16_mul_eq",
+  "primitives.i32_mul_eq",
+  "primitives.i64_mul_eq",
+  "primitives.i128_mul_eq",
+  "primitives.usize_mul_eq",
+  "primitives.u8_mul_eq",
+  "primitives.u16_mul_eq",
+  "primitives.u32_mul_eq",
+  "primitives.u64_mul_eq",
+  "primitives.u128_mul_eq"
 ]
-val _ = app register_spec_thm all_mul_eqs
+val _ = save_spec_thms all_mul_eqs
 
 val all_div_eqs = [
-  isize_div_eq,
-  i8_div_eq,
-  i16_div_eq,
-  i32_div_eq,
-  i64_div_eq,
-  i128_div_eq,
-  usize_div_eq,
-  u8_div_eq,
-  u16_div_eq,
-  u32_div_eq,
-  u64_div_eq,
-  u128_div_eq
+  "primitives.isize_div_eq",
+  "primitives.i8_div_eq",
+  "primitives.i16_div_eq",
+  "primitives.i32_div_eq",
+  "primitives.i64_div_eq",
+  "primitives.i128_div_eq",
+  "primitives.usize_div_eq",
+  "primitives.u8_div_eq",
+  "primitives.u16_div_eq",
+  "primitives.u32_div_eq",
+  "primitives.u64_div_eq",
+  "primitives.u128_div_eq"
 ]
-val _ = app register_spec_thm all_div_eqs
+val _ = save_spec_thms all_div_eqs
 
 val all_rem_eqs = [
-  isize_rem_eq,
-  i8_rem_eq,
-  i16_rem_eq,
-  i32_rem_eq,
-  i64_rem_eq,
-  i128_rem_eq,
-  usize_rem_eq,
-  u8_rem_eq,
-  u16_rem_eq,
-  u32_rem_eq,
-  u64_rem_eq,
-  u128_rem_eq
+  "primitives.isize_rem_eq",
+  "primitives.i8_rem_eq",
+  "primitives.i16_rem_eq",
+  "primitives.i32_rem_eq",
+  "primitives.i64_rem_eq",
+  "primitives.i128_rem_eq",
+  "primitives.usize_rem_eq",
+  "primitives.u8_rem_eq",
+  "primitives.u16_rem_eq",
+  "primitives.u32_rem_eq",
+  "primitives.u64_rem_eq",
+  "primitives.u128_rem_eq"
 ]
-val _ = app register_spec_thm all_rem_eqs
-
-val all_vec_lems = [
-  vec_len_spec,
-  vec_insert_back_spec
+val _ = save_spec_thms all_rem_eqs
+
+val _ = save_spec_thms [
+  "primitives.vec_index_fwd_spec",
+  "primitives.vec_index_back_spec",
+  "primitives.vec_index_mut_fwd_spec",
+  "primitives.vec_index_mut_back_spec",
+  "primitives.vec_insert_back_spec",
+  "primitives.vec_push_back_spec"
 ]
-val _ = app register_spec_thm all_vec_lems
 
 (* Provided the goal contains a call to a monadic function, return this function call.
 
@@ -499,7 +508,7 @@ val progress : tactic =
     val asms_thl = mapfilter asm_to_spec asms;
     (* Lookup a spec in the database *)
     val thl =
-      case Redblackmap.peek (!reg_spec_thms, fname) of
+      case Redblackmap.peek (get_spec_thms (), fname) of
         NONE => asms_thl
       | SOME spec => spec :: asms_thl;
     val _ =
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 8cd54f33..7920454b 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1624,8 +1624,8 @@ Proof
   prove_scalar_eq_equiv_tac
 QED
 
-(* Remark.: don't move this up, it will break some proofs *)
-val _ = BasicProvers.export_rewrites [
+
+val _ = evalLib.add_rewrite_thms [
   "isize_eq_equiv",
   "i8_eq_equiv",
   "i16_eq_equiv",
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 2407e2f2..e4051212 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -2388,24 +2388,20 @@ sig
    
    [vec_len_spec]  Theorem
       
-      [oracles: DISK_THM]
-      [axioms: int_to_usize_usize_to_int, usize_bounds,
-       vec_to_list_num_bounds] []
+      [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
             0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
    
    [vec_len_vec_new]  Theorem
       
-      [oracles: DISK_THM]
-      [axioms: mk_vec_axiom, int_to_usize_usize_to_int,
-       usize_to_int_int_to_usize, usize_bounds] []
+      [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
       ⊢ vec_len vec_new = int_to_usize 0
    
    [vec_push_back_spec]  Theorem
       
       [oracles: DISK_THM]
-      [axioms: usize_to_int_int_to_usize, mk_vec_axiom,
-       int_to_usize_usize_to_int, usize_bounds, vec_to_list_num_bounds] []
+      [axioms: usize_to_int_int_to_usize, mk_vec_axiom, usize_bounds,
+       vec_to_list_num_bounds] []
       ⊢ ∀v x.
           usize_to_int (vec_len v) < usize_max ⇒
           ∃nv.
@@ -2438,8 +2434,7 @@ sig
       
       [oracles: DISK_THM]
       [axioms: vec_to_list_num_bounds, usize_bounds,
-       int_to_usize_usize_to_int, usize_to_int_bounds,
-       usize_to_int_int_to_usize, mk_vec_axiom] []
+       usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] []
       ⊢ ∀v i x.
           usize_to_int i < usize_to_int (vec_len v) ⇒
           (let
diff --git a/backends/hol4/saveThmsLib.sig b/backends/hol4/saveThmsLib.sig
index 9cbac1c7..bbdc080b 100644
--- a/backends/hol4/saveThmsLib.sig
+++ b/backends/hol4/saveThmsLib.sig
@@ -25,15 +25,20 @@ sig
   (* The user-provided functions *)
   type 'key key_fns = {
     compare : 'key * 'key -> order,
-    get_key_from_thm : thm -> 'key
+    (* Retrieve the key from the theorem and normalize it at the same time *)
+    get_key_normalize_thm : thm -> ('key * thm)
   }
 
   (* The functions we return to the user to manipulate the map *)
   type 'key map_fns = {
     (* Persistently save a theorem *)
     save_thm : string -> unit,
+    (* Persistently delete a theorem *)
+    delete_thm : string -> unit,
     (* Temporarily save a theorem *)
     temp_save_thm : thm -> unit,
+    (* Temporarily delete a theorem *)
+    temp_delete_thm : thm -> unit,
     (* Get the key set *)
     get_keys : unit -> 'key Redblackset.set,
     (* Get the theorems map *)
diff --git a/backends/hol4/saveThmsLib.sml b/backends/hol4/saveThmsLib.sml
index 76b428cf..e7b20055 100644
--- a/backends/hol4/saveThmsLib.sml
+++ b/backends/hol4/saveThmsLib.sml
@@ -8,32 +8,35 @@ type thname = KernelSig.kernelname
 (* The user-provided functions *)
 type 'key key_fns = {
   compare : 'key * 'key -> order,
-  get_key_from_thm : thm -> 'key
+  get_key_normalize_thm : thm -> ('key * thm)
 }
 
 (* The functions we return to the user to manipulate the map *)
 type 'key map_fns = {
   (* Persistently save a theorem *)
   save_thm : string -> unit,
+  (* Persistently delete a theorem *)
+  delete_thm : string -> unit,
   (* Temporarily save a theorem *)
   temp_save_thm : thm -> unit,
+  (* Temporarily delete a theorem *)
+  temp_delete_thm : thm -> unit,
   (* Get the key set *)
   get_keys : unit -> 'key Redblackset.set,
   (* Get the theorems map *)
   get_map : unit -> ('key, thm) Redblackmap.dict
 }
 
-(* This function is adapted from ThmSetData.sml.
+(* This function is adapted from ThmSetData.sml *)
+fun get_Kname (s : string) : thname =
+  case String.fields (equal #".") s of
+    [s0] => {Thy = current_theory(), Name = s}
+  | [s1,s2] => {Thy = s1, Name = s2}
+  | _ => raise mk_HOL_ERR "saveThmsLib" "get_Kname" ("Malformed name: " ^ s)
 
-   It raises an exception if it can't find a theorem.
- *)
 fun lookup_thm (s : string) : thname * thm =
   let
-    val name =
-     case String.fields (equal #".") s of
-         [s0] => {Thy = current_theory(), Name = s}
-       | [s1,s2] => {Thy = s1, Name = s2}
-       | _ => raise mk_HOL_ERR "saveThmsLib" "lookup_thm" ("Malformed name: " ^ s)
+    val name = get_Kname s
     fun lookup_exn {Thy,Name} = DB.fetch Thy Name
   in
     (name, lookup_exn name)
@@ -45,24 +48,40 @@ type 'key state = 'key Redblackset.set * ('key, thm) Redblackmap.dict
 (* Initialize a persistent map *)
 fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns =
   let
-     val { compare, get_key_from_thm } = kf
+     val { compare, get_key_normalize_thm } = kf
      
      (* Small helper *)
-     fun add_to_state (th : thm) (s, m) =
+     fun add_to_state (th : thm) (s, m) : 'key state =
        let
-         val k = get_key_from_thm th
+         val (k, th) = get_key_normalize_thm th
          val s = Redblackset.add (s, k)
          val m = Redblackmap.insert (m, k, th)
        in
          (s, m)
        end
+
+     (* Small helper *)
+     fun remove_from_state (th : thm) ((s, m) : 'key state) : 'key state =
+       let
+         val (k, _) = get_key_normalize_thm th
+         (* For deletion: we have to test whether the element/key is there or not,
+            because otherwise the functions raise the exception NotFound *)
+         val s = if Redblackset.member (s, k) then Redblackset.delete (s, k) else s
+         val m = if Option.isSome (Redblackmap.peek (m, k)) then fst (Redblackmap.remove (m, k)) else m
+       in
+         (s, m)
+       end
   
      (* Persistently update the map given a delta  *)
      fun apply_delta (delta : ThmSetData.setdelta) st =
        case delta of
          ThmSetData.ADD (_, th) => add_to_state th st
-       | ThmSetData.REMOVE _ =>
-         raise mk_HOL_ERR "saveThmsLib" "create_map" ("Unexpected REMOVE")
+       | ThmSetData.REMOVE th_name =>
+         let
+           val (_, th) = lookup_thm th_name
+         in
+           remove_from_state th st
+         end
 
      (* Initialize the dictionary *)
      val init_state = (Redblackset.empty compare, Redblackmap.mkDict compare)
@@ -85,6 +104,10 @@ fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns =
      fun temp_save_thm (th : thm) : unit =
        update_global_value (add_to_state th)
 
+     (* Temporarily delete theorem *)
+     fun temp_delete_thm (th : thm) : unit =
+       update_global_value (remove_from_state th)
+
      (* Persistently save a theorem *)
      fun save_thm (s : string) : unit =
        let
@@ -96,11 +119,22 @@ fun create_map (kf : 'key key_fns) (name : string) : 'key map_fns =
            temp_save_thm (snd th)
        end
 
+     (* Persistently delete a theorem *)
+     fun delete_thm (s : string) : unit =
+       let
+         val (_, th) = lookup_thm s
+       in
+         (* Similar to [save_thm] *)
+         record_delta (ThmSetData.REMOVE s);
+         temp_delete_thm th
+       end
+
      (* *)
      val get_keys = fst o get_global_value
      val get_map = snd o get_global_value
   in
-    { save_thm = save_thm, temp_save_thm = temp_save_thm,
+    { save_thm = save_thm, delete_thm = delete_thm,
+      temp_save_thm = temp_save_thm, temp_delete_thm = temp_delete_thm,
       get_keys = get_keys, get_map = get_map }
   end
 
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
index 79026376..c3f04cca 100644
--- a/backends/hol4/testHashmapScript.sml
+++ b/backends/hol4/testHashmapScript.sml
@@ -51,7 +51,7 @@ Proof
   progress >> progress
 QED
 
-val _ = register_spec_thm nth_mut_fwd_spec
+val _ = save_spec_thm "nth_mut_fwd_spec"
 
 val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
 val insert_def = new_axiom ("insert_def", “
@@ -177,9 +177,7 @@ Proof
     Cases_on ‘q' = k’ >> rw []
     >- (fs [list_t_v_def, index_eq]) >>
     Cases_on ‘insert k v ls0’ >> fs [] >>
-    (* TODO: would be good to have a tactic which inverts equalities of the
-       shape ‘ListCons (q',r) a = ls1’ *)
-    sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >>
+    gvs [list_t_v_def, index_eq] >>
     first_x_assum (qspec_assume ‘0’) >>
     fs [len_def] >>
     strip_tac >>
@@ -193,7 +191,7 @@ Proof
     fs [list_t_v_def, index_eq, len_def] >>
     first_x_assum (qspec_assume ‘i’) >> rfs []) >>
   Cases_on ‘insert k v ls0’ >> fs [] >>
-  sg ‘ls1 = ListCons (q',r) a’ >- fs [] >> fs [list_t_v_def, index_eq] >>
+  gvs [list_t_v_def, index_eq] >>
   last_x_assum (qspec_assume ‘i - 1’) >>
   fs [len_def] >>
   sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >>
@@ -250,13 +248,11 @@ Proof
     last_x_assum (qspecl_assume [‘i’, ‘j’]) >>
     rfs [list_t_v_def, len_def] >>
     sg ‘0 < j’ >- int_tac >>
-    Cases_on ‘i = 0’ >> fs [index_eq] >>
-    sg ‘0 < i’ >- int_tac >> fs []) >>
+    Cases_on ‘i = 0’ >> gvs [index_eq]) >>
   (* k ≠ q: recursion *)
   Cases_on ‘insert k v ls0’ >> fs [bind_def] >>
   last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >>
-  rfs [] >>
-  sg ‘ls1 = ListCons (q,r) a’ >- fs [] >> fs [list_t_v_def] >>
+  gvs [list_t_v_def] >>
   imp_res_tac distinct_keys_tail >> fs [] >>
   irule distinct_keys_cons >> rw [] >>
   metis_tac [distinct_keys_insert_index_neq]