word_lib internal + crefine: remove duplicate lemma

seL4 · Nov 15, 2019 · 1970ed0 · 1970ed0
1 parent c390ba7
commit 1970ed0
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 4 deletions.
diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy
@@ -348,8 +348,6 @@ lemma two_bits_cases:
   apply (frule and_mask_cases[where n=2 and x=x, simplified mask_def])
   using upt_conv_Cons by auto[1]
 
-lemmas mask_1_eq_1 = mask_1
-
 lemma zero_OR_eq:
   "y = 0 \<Longrightarrow> (x || y) = x"
   by simp

diff --git a/proof/crefine/ARM/CSpace_C.thy b/proof/crefine/ARM/CSpace_C.thy
@@ -612,7 +612,7 @@ lemma cteInsert_ccorres_mdb_helper:
   apply (rule allI)
   apply (rule conseqPre)
   apply vcg
-  apply (clarsimp simp: return_def mask_1_eq_1[simplified])
+  apply (clarsimp simp: return_def mask_Suc_0)
   apply (simp add: cmdbnode_relation_def)
   done
 

diff --git a/proof/crefine/ARM_HYP/CSpace_C.thy b/proof/crefine/ARM_HYP/CSpace_C.thy
@@ -618,7 +618,7 @@ lemma cteInsert_ccorres_mdb_helper:
   apply (rule allI)
   apply (rule conseqPre)
   apply vcg
-  apply (clarsimp simp: return_def mask_1_eq_1[simplified])
+  apply (clarsimp simp: return_def mask_Suc_0)
   apply (simp add: cmdbnode_relation_def)
   done