Remove some redundant (repeated) theorems

jonsterling · Mar 3, 2018 · 6131c9b · 6131c9b
1 parent 3525c49
commit 6131c9b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 14 deletions.
diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml
@@ -1340,14 +1340,6 @@ val FromList_thm = Q.store_thm("FromList_thm",
   \\ match_mp_tac memory_rel_rearrange
   \\ fs [] \\ rw [] \\ fs []);
 
-val cut_env_adjust_set_insert_1 = Q.store_thm("cut_env_adjust_set_insert_1",
-  `cut_env (adjust_set x) (insert 1 w l) =
-    cut_env (adjust_set x) l`,
-  fs [wordSemTheory.cut_env_def] \\ rw []
-  \\ fs [lookup_inter_alt,lookup_insert]
-  \\ rw [] \\ fs [SUBSET_DEF]
-  \\ res_tac \\ fs [NOT_1_domain]);
-
 val get_var_get_real_addr_lemma =
     GEN_ALL(CONV_RULE(LAND_CONV(move_conj_left(
                                    same_const``wordSem$get_var`` o #1 o

diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml
@@ -5921,12 +5921,6 @@ val memory_rel_any_Number_IMP = store_thm("memory_rel_any_Number_IMP",
   \\ simp_tac std_ss [fcpTheory.FCP_BETA,DIMINDEX_GT_0,word_1comp_def]
   \\ EVAL_TAC);
 
-val Smallnum_i2w = store_thm("Smallnum_i2w",
-  ``Smallnum i = i2w (4 * i)``,
-  Cases_on `i` \\ fs [Smallnum_def,integer_wordTheory.i2w_def]
-  \\ reverse IF_CASES_TAC THEN1 (`F` by intLib.COOPER_TAC)
-  \\ ntac 2 AP_TERM_TAC \\ intLib.COOPER_TAC);
-
 val memory_rel_Number_IMP = store_thm("memory_rel_Number_IMP",
   ``good_dimindex (:'a) /\ small_int (:'a) i /\
     memory_rel c be refs sp st m dm ((Number i,v:'a word_loc)::vars) ==>