diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy
index d3fa7a4f0b..59a4ed1ed7 100644
--- a/proof/crefine/X64/ADT_C.thy
+++ b/proof/crefine/X64/ADT_C.thy
@@ -102,7 +102,7 @@ lemma setTCBContext_C_corres:
   apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def
                         carch_state_relation_def cmachine_state_relation_def
                         typ_heap_simps' update_tcb_map_tos)
-  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def
+  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def tcb_cte_cases_neqs
                    cvariable_relation_upd_const ko_at_projectKO_opt)
   apply (simp add: cep_relations_drop_fun_upd)
   apply (apply_conjunct \<open>match conclusion in \<open>fpu_null_state_relation _\<close> \<Rightarrow>
@@ -352,7 +352,7 @@ lemma unat_ucast_mask_pageBits_shift:
 lemma mask_pageBits_shift_sum:
   "unat n = unat (p && mask 3) \<Longrightarrow>
   (p && ~~ mask pageBits) + (p && mask pageBits >> 3) * 8 + n = (p::machine_word)"
-  apply (clarsimp simp: ArchMove_C.word_shift_by_3)
+  apply (clarsimp simp: X64.word_shift_by_3)
   apply (subst word_plus_and_or_coroll)
    apply (rule word_eqI)
    apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size)
@@ -756,6 +756,7 @@ lemma map_to_ctes_tcb_ctes:
   "ctes_of s' = ctes_of s \<Longrightarrow>
    ko_at' tcb p s \<Longrightarrow> ko_at' tcb' p s' \<Longrightarrow>
    \<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb"
+  supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *)
   apply (clarsimp simp add: ran_tcb_cte_cases)
   apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb
                  split: kernel_object.splits)
@@ -1327,7 +1328,7 @@ lemma ksPSpace_eq_imp_typ_at'_eq:
 lemma ksPSpace_eq_imp_valid_cap'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_cap' c s' = valid_cap' c s"
-  by (auto simp: valid_cap'_def page_table_at'_def page_directory_at'_def
+  by (auto simp: valid_cap'_def valid_arch_cap'_def page_table_at'_def page_directory_at'_def
                  valid_untyped'_def pd_pointer_table_at'_def page_map_l4_at'_def
                  ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
                  ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace]
@@ -1340,7 +1341,7 @@ lemma ksPSpace_eq_imp_valid_tcb'_eq:
   by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
                  ksPSpace_eq_imp_valid_cap'_eq[OF ksPSpace]
                  ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace]
-                 valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def valid_bound_tcb'_def
+                 valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def valid_arch_tcb'_def
           split: thread_state.splits option.splits)
 
 lemma ksPSpace_eq_imp_valid_arch_obj'_eq:
diff --git a/proof/crefine/X64/ArchMove_C.thy b/proof/crefine/X64/ArchMove_C.thy
index 3a3f492568..1a3f9a916c 100644
--- a/proof/crefine/X64/ArchMove_C.thy
+++ b/proof/crefine/X64/ArchMove_C.thy
@@ -31,6 +31,8 @@ lemma ps_clear_is_aligned_ksPSpace_None:
                     power_overflow)
   by assumption
 
+context Arch begin arch_global_naming
+
 lemma ps_clear_is_aligned_ctes_None:
   assumes "ps_clear p tcbBlockSizeBits s"
       and "is_aligned p tcbBlockSizeBits"
@@ -170,8 +172,6 @@ lemma addToBitmap_sets_L1Bitmap_same_dom:
                         prioToL1Index_max[simplified wordRadix_def, simplified])
   done
 
-context begin interpretation Arch .
-
 lemma vmsz_aligned_aligned_pageBits:
   "vmsz_aligned ptr sz \<Longrightarrow> is_aligned ptr pageBits"
   apply (simp add: vmsz_aligned_def)
@@ -422,6 +422,7 @@ lemma valid_untyped':
   apply (frule pspace_distinctD'[OF _ pspace_distinct'])
   apply simp
   apply (frule aligned_ranges_subset_or_disjoint[OF al])
+  apply (simp only: add_mask_fold)
   apply (fold obj_range'_def)
   apply (rule iffI)
    apply auto[1]
@@ -429,14 +430,15 @@ lemma valid_untyped':
    apply (rule ccontr, simp)
    apply (simp add: Set.psubset_eq)
    apply (erule conjE)
-   apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp)
+   apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp)
    apply (cut_tac is_aligned_no_overflow[OF al])
-   apply (auto simp add: obj_range'_def)[1]
+   apply (auto simp add: obj_range'_def add_mask_fold)[1]
   apply (clarsimp simp add: usableUntypedRange.simps Int_commute)
-  apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp+)
+  apply (case_tac "obj_range' ptr' ko \<inter> mask_range ptr bits \<noteq> {}", simp)
   apply (cut_tac is_aligned_no_overflow[OF al])
   apply (clarsimp simp add: obj_range'_def)
   apply (frule is_aligned_no_overflow)
+  apply (simp add: mask_def add_diff_eq)
   by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1
                nat_le_linear power_overflow sub_wrap add_0
                add_0_right word_add_increasing word_less_1 word_less_sub_1)
@@ -509,4 +511,10 @@ lemma cap_case_isPML4Cap:
 
 end
 
+(* these will need to be requalified when moved *)
+arch_requalify_facts
+  empty_fail_loadWordUser
+
+lemmas [intro!, simp] = empty_fail_loadWordUser
+
 end
diff --git a/proof/crefine/X64/Detype_C.thy b/proof/crefine/X64/Detype_C.thy
index eae4571c82..0f6134a024 100644
--- a/proof/crefine/X64/Detype_C.thy
+++ b/proof/crefine/X64/Detype_C.thy
@@ -396,13 +396,14 @@ proof -
       using vu unfolding valid_cap'_def valid_untyped'_def
       apply clarsimp
       apply (drule_tac x = x in spec)
-      apply (clarsimp simp:ko_wp_at'_def)
+      apply (clarsimp simp:ko_wp_at'_def add_mask_fold)
       done
 
     with koat have "\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}"
       apply -
       apply (erule obj_atE')+
-      apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject)
+      apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject
+                       add_mask_fold)
       done
 
     thus ?thesis using subset1
@@ -570,7 +571,7 @@ proof -
      apply simp
     apply clarsimp
     apply (drule_tac y = n in aligned_add_aligned [where m = cte_level_bits, simplified cte_level_bits_def])
-     apply (simp add: tcb_cte_cases_def is_aligned_def split: if_split_asm)
+     apply (simp add: tcb_cte_cases_def  cteSizeBits_def is_aligned_def split: if_split_asm)
     apply (simp add: word_bits_conv)
     apply simp
     done
@@ -1786,7 +1787,7 @@ proof -
     apply (frule pspace_distinctD'[OF _ pspace_distinct'])
     apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def)
     apply (drule_tac x=x in spec)
-    apply (simp add: obj_range'_def objBitsKO_def)
+    apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq)
     apply (simp only: not_le)
     apply (cut_tac is_aligned_no_overflow[OF al])
     apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1",
@@ -1839,7 +1840,7 @@ proof -
     apply (frule pspace_distinctD'[OF _ pspace_distinct'])
     apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def)
     apply (drule_tac x=x in spec)
-    apply (simp add: obj_range'_def objBitsKO_def)
+    apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq)
     apply (simp only: not_le)
     apply (cut_tac is_aligned_no_overflow[OF al])
     apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1",
@@ -1865,9 +1866,9 @@ proof -
         \<Longrightarrow> {p ..+ 2 ^ objBitsT TCBT} \<inter> {ptr..+2 ^ bits} = {}"
       apply (clarsimp simp: valid_cap'_def)
       apply (drule(1) map_to_ko_atI')
-      apply (clarsimp simp: obj_at'_def valid_untyped'_def2)
+      apply (clarsimp simp: obj_at'_def valid_untyped'_def2 mask_2pm1 add_diff_eq)
       apply (elim allE, drule(1) mp)
-      apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al)
+      apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al add_mask_fold[symmetric])
       apply (subgoal_tac "objBitsKO ko = objBitsT TCBT")
        apply (subgoal_tac "p \<in> {p ..+ 2 ^ objBitsT TCBT}")
         apply simp
diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy
index 0c878db8ed..be10a8d977 100644
--- a/proof/crefine/X64/Finalise_C.thy
+++ b/proof/crefine/X64/Finalise_C.thy
@@ -839,7 +839,7 @@ lemma doUnbindNotification_ccorres:
       apply simp
       apply (erule(1) rf_sr_tcb_update_no_queue2)
               apply (simp add: typ_heap_simps')+
-       apply (simp add: tcb_cte_cases_def)
+       apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
       apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
      apply (simp add: invs'_def valid_state'_def)
      apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+
@@ -891,7 +891,7 @@ lemma doUnbindNotification_ccorres':
       apply simp
       apply (erule(1) rf_sr_tcb_update_no_queue2)
               apply (simp add: typ_heap_simps')+
-       apply (simp add: tcb_cte_cases_def)
+       apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
       apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def)
      apply (simp add: invs'_def valid_state'_def)
      apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+
diff --git a/proof/crefine/X64/Ipc_C.thy b/proof/crefine/X64/Ipc_C.thy
index 15040668c2..9917e66d8d 100644
--- a/proof/crefine/X64/Ipc_C.thy
+++ b/proof/crefine/X64/Ipc_C.thy
@@ -187,7 +187,7 @@ crunch getSanitiseRegisterInfo
 
 lemma empty_fail_getSanitiseRegisterInfo[wp, simp]:
   "empty_fail (getSanitiseRegisterInfo t)"
-  by (wpsimp simp: getSanitiseRegisterInfo_def wp: ArchMove_C.empty_fail_archThreadGet)
+  by (wpsimp simp: getSanitiseRegisterInfo_def wp: X64.empty_fail_archThreadGet)
 
 lemma asUser_getRegister_getSanitiseRegisterInfo_comm:
   "do
@@ -4576,7 +4576,7 @@ lemma sendIPC_block_ccorres_helper:
                               rf_sr_tcb_update_twice)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen,
           (simp add: typ_heap_simps')+)[1]
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def cteSizeBits_def)
         apply (simp add: ctcb_relation_def cthread_state_relation_def
                          ThreadState_defs mask_def)
         apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend
@@ -4588,7 +4588,7 @@ lemma sendIPC_block_ccorres_helper:
                threadSet_valid_objs')
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
-                         tcb_cte_cases_def)
+                         tcb_cte_cases_def cteSizeBits_def)
    apply (drule obj_at'_is_canonical, simp, simp)
   apply clarsimp
   done
@@ -5165,7 +5165,7 @@ lemma receiveIPC_block_ccorres_helper:
         apply (frule h_t_valid_c_guard)
         apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice cap_get_tag_isCap)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps)+)
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def cteSizeBits_def)
         apply (simp add: ctcb_relation_def cthread_state_relation_def ccap_relation_ep_helpers
                          ThreadState_defs mask_def cap_get_tag_isCap)
         apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend)
@@ -5176,7 +5176,7 @@ lemma receiveIPC_block_ccorres_helper:
                threadSet_weak_sch_act_wf_runnable')
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
-                         tcb_cte_cases_def obj_at'_is_canonical)
+                         tcb_cte_cases_def obj_at'_is_canonical cteSizeBits_def)
   apply clarsimp
   done
 
@@ -6217,7 +6217,7 @@ lemma receiveSignal_block_ccorres_helper:
         apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice)
         apply (erule(1) rf_sr_tcb_update_no_queue_gen,
           (simp add: typ_heap_simps')+)
-         apply (simp add: tcb_cte_cases_def)
+         apply (simp add: tcb_cte_cases_def cteSizeBits_def)
         apply (simp add: ctcb_relation_def cthread_state_relation_def
                          ThreadState_defs mask_def)
         apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend)
@@ -6228,7 +6228,7 @@ lemma receiveSignal_block_ccorres_helper:
                threadSet_weak_sch_act_wf_runnable')
     apply (clarsimp simp: guard_is_UNIV_def)
    apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def
-                     valid_tcb_state'_def obj_at'_is_canonical)
+                     valid_tcb_state'_def obj_at'_is_canonical cteSizeBits_def)
   done
 
 lemma cpspace_relation_ntfn_update_ntfn':
diff --git a/proof/crefine/X64/IsolatedThreadAction.thy b/proof/crefine/X64/IsolatedThreadAction.thy
index 20c7c11bde..53b98565d6 100644
--- a/proof/crefine/X64/IsolatedThreadAction.thy
+++ b/proof/crefine/X64/IsolatedThreadAction.thy
@@ -148,11 +148,11 @@ end
 
 lemmas getObject_return_tcb
     = getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb,
-                       unfolded objBits_simps, simplified]
+                       unfolded gen_objBits_simps, simplified]
 
 lemmas setObject_modify_tcb
     = setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb,
-                       unfolded objBits_simps, simplified]
+                       unfolded gen_objBits_simps, simplified]
 
 lemma partial_overwrite_fun_upd:
   "inj idx \<Longrightarrow>
diff --git a/proof/crefine/X64/Recycle_C.thy b/proof/crefine/X64/Recycle_C.thy
index 7eb8d1c6aa..e8b2013c84 100644
--- a/proof/crefine/X64/Recycle_C.thy
+++ b/proof/crefine/X64/Recycle_C.thy
@@ -546,10 +546,10 @@ lemma heap_to_user_data_in_user_mem'[simp]:
    apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 3])
      apply (erule aligned_add_aligned)
       apply (simp add: is_aligned_mult_triv2[where n = 3,simplified])
-     apply  (clarsimp simp: objBits_simps X64.pageBits_def)
+     apply  (clarsimp simp: X64.objBits_simps X64.pageBits_def)
     apply simp
    apply (rule is_aligned_add_helper[THEN conjunct2])
-    apply (simp add: X64.pageBits_def objBits_simps)
+    apply (simp add: X64.pageBits_def X64.objBits_simps)
    apply (rule word_less_power_trans2[where k = 3,simplified])
      apply (rule less_le_trans[OF ucast_less])
       apply simp+
diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy
index 480e13078d..e36a7dceeb 100644
--- a/proof/crefine/X64/Refine_C.thy
+++ b/proof/crefine/X64/Refine_C.thy
@@ -642,7 +642,7 @@ lemma threadSet_all_invs_triv':
         apply (simp add: tcb_relation_def arch_tcb_context_set_def
                          atcbContextSet_def arch_tcb_relation_def)
        apply (simp add: tcb_cap_cases_def)
-      apply (simp add: tcb_cte_cases_def)
+      apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs)
      apply (simp add: exst_same_def)
     apply (wp thread_set_invs_trivial thread_set_ct_running thread_set_not_state_valid_sched
               threadSet_invs_trivial threadSet_ct_running' hoare_weak_lift_imp
diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy
index 122be6b735..2db2859a8d 100644
--- a/proof/crefine/X64/Retype_C.thy
+++ b/proof/crefine/X64/Retype_C.thy
@@ -1428,7 +1428,7 @@ lemma zero_ranges_ptr_retyps:
   apply (erule disjoint_subset[rotated])
   apply (subst intvl_plus_unat_eq)
     apply clarsimp
-   apply clarsimp
+   apply (clarsimp simp: mask_def add_diff_eq)
    apply (clarsimp simp: word_unat.Rep_inject[symmetric]
                          valid_cap_simps' capAligned_def
                          unat_of_nat
@@ -6147,7 +6147,7 @@ lemma threadSet_domain_ccorres [corres]:
   apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def
                         fpu_null_state_heap_update_tag_disj_simps)
   apply (clarsimp simp: update_tcb_map_tos typ_heap_simps')
-  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def)
+  apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def cteSizeBits_def)
   apply (simp add: cep_relations_drop_fun_upd
                    cvariable_relation_upd_const ko_at_projectKO_opt)
   apply (drule ko_at_projectKO_opt)
@@ -6578,7 +6578,7 @@ lemma ctes_of_ko_at_strong:
    apply (subst intvl_range_conv[where bits = cteSizeBits,simplified])
      apply simp
     apply (simp add:word_bits_def objBits_simps')
-   apply (simp add:field_simps)
+   apply (simp add:field_simps mask_def)
   apply (intro exI conjI,assumption)
   apply (clarsimp simp:objBits_simps obj_range'_def word_and_le2)
   apply (cut_tac intvl_range_conv[where bits = cteSizeBits and ptr = p, simplified])
@@ -6592,37 +6592,11 @@ lemma ctes_of_ko_at_strong:
   apply (thin_tac "P \<or> Q" for P Q)
   apply (erule order_trans)
   apply (subst word_plus_and_or_coroll2[where x = p and w = "mask tcbBlockSizeBits",symmetric])
-  apply (clarsimp simp:tcb_cte_cases_def field_simps split:if_split_asm)
-      apply (subst p_assoc_help)
-      apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'])
-        apply (simp add: objBits_simps')
-       apply (rule Aligned.is_aligned_neg_mask)
-       apply (rule le_refl,simp)
-      apply (simp add: objBits_simps')
-     apply (subst p_assoc_help)
-     apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'])
-       apply (simp add: objBits_simps')
-      apply (rule Aligned.is_aligned_neg_mask)
-      apply (rule le_refl,simp)
-     apply (simp add: objBits_simps')
-    apply (subst p_assoc_help)
-    apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'])
-    apply (simp add:objBits_simps')
-     apply (rule Aligned.is_aligned_neg_mask)
-     apply (rule le_refl,simp)
-    apply (simp add: objBits_simps')
-   apply (subst p_assoc_help)
-   apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'])
-     apply (simp add: objBits_simps')
-    apply (rule Aligned.is_aligned_neg_mask)
-    apply (rule le_refl,simp)
-   apply (simp add: objBits_simps')
-  apply (subst p_assoc_help)+
-  apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap'])
-    apply (simp add: objBits_simps')
-   apply (rule Aligned.is_aligned_neg_mask)
-   apply (rule le_refl,simp)
-  apply (simp add: objBits_simps')
+  apply (clarsimp simp: tcb_cte_cases_def field_simps cteSizeBits_def tcbBlockSizeBits_def
+                  split:if_split_asm)
+      apply (subst add.commute)
+      apply (rule word_plus_mono_left[OF _ is_aligned_no_wrap']
+             , simp add: mask_def, rule is_aligned_neg_mask2, simp add: mask_def)+
   done
 
 lemma pspace_no_overlap_induce_cte:
@@ -6651,7 +6625,7 @@ lemma pspace_no_overlap_induce_cte:
   apply (subst intvl_range_conv)
     apply simp
    apply (simp add: word_bits_def)
-  apply (simp add: obj_range'_def)
+  apply (simp add: obj_range'_def ptr_range_mask_range del: Int_atLeastAtMost)
   done
 
 lemma pspace_no_overlap_induce_asidpool:
@@ -7188,7 +7162,7 @@ lemma tcb_ctes_typ_region_bytes:
                         pspace_no_overlap'_def is_aligned_neg_mask_weaken
                         field_simps upto_intvl_eq[symmetric])
   apply (elim allE, drule(1) mp)
-  apply simp
+  apply (simp add: mask_def add_diff_eq upto_intvl_eq[symmetric] del: Int_atLeastAtMost)
   apply (drule(1) pspace_alignedD')
   apply (erule disjoint_subset[rotated])
   apply (simp add: upto_intvl_eq[symmetric])
diff --git a/proof/crefine/X64/SR_lemmas_C.thy b/proof/crefine/X64/SR_lemmas_C.thy
index 0aa1b29c1a..44386556a3 100644
--- a/proof/crefine/X64/SR_lemmas_C.thy
+++ b/proof/crefine/X64/SR_lemmas_C.thy
@@ -906,9 +906,9 @@ proof -
     apply (rule is_aligned_weaken[OF _ bits])
     apply (erule cte_wp_atE')
      apply assumption
-    apply (simp add: tcb_cte_cases_def field_simps split: if_split_asm)
+    apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs field_simps split: if_split_asm)
         apply (fastforce elim: aligned_add_aligned[OF _ _ cte_bits_le_tcb_bits]
-                         simp: is_aligned_def cte_level_bits_def)+
+                         simp: is_aligned_def cte_level_bits_def cteSizeBits_def)+
     apply (erule is_aligned_weaken[OF _  cte_bits_le_tcb_bits])
     done
 qed
diff --git a/proof/crefine/X64/Schedule_C.thy b/proof/crefine/X64/Schedule_C.thy
index cab2a5ab7e..9cbf7e7ddf 100644
--- a/proof/crefine/X64/Schedule_C.thy
+++ b/proof/crefine/X64/Schedule_C.thy
@@ -738,7 +738,7 @@ lemma threadSet_timeSlice_ccorres [corres]:
   apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def
                         fpu_null_state_heap_update_tag_disj_simps)
   apply (clarsimp simp: update_tcb_map_tos typ_heap_simps')
-  apply (simp add: map_to_ctes_upd_tcb_no_ctes tcb_cte_cases_def
+  apply (simp add: map_to_ctes_upd_tcb_no_ctes tcb_cte_cases_def tcb_cte_cases_neqs
                    map_to_tcbs_upd)
   apply (simp add: cep_relations_drop_fun_upd cvariable_relation_upd_const
                    ko_at_projectKO_opt)
diff --git a/proof/crefine/X64/Syscall_C.thy b/proof/crefine/X64/Syscall_C.thy
index adda71099e..7ab6425772 100644
--- a/proof/crefine/X64/Syscall_C.thy
+++ b/proof/crefine/X64/Syscall_C.thy
@@ -562,7 +562,7 @@ done
 lemma tcb_cte_cases_tcbFault_update_simp:
   "(f, u) \<in> ran tcb_cte_cases \<Longrightarrow> f (tcbFault_update (\<lambda>_. Some fault) tcb) = f tcb"
   unfolding tcb_cte_cases_def
-  by auto
+  by (auto simp: tcb_cte_cases_neqs)
 
 lemma hrs_mem_update_use_hrs_mem:
   "hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)"
diff --git a/proof/crefine/X64/TcbQueue_C.thy b/proof/crefine/X64/TcbQueue_C.thy
index 7a79843bdf..ad0dbd68bf 100644
--- a/proof/crefine/X64/TcbQueue_C.thy
+++ b/proof/crefine/X64/TcbQueue_C.thy
@@ -1150,7 +1150,7 @@ lemma tcb_at'_non_kernel_data_ref:
   apply (drule map_to_tcbs_from_tcb_at)
   apply (clarsimp simp: pspace_domain_valid_def map_comp_def split: option.splits)
   apply (drule spec, drule spec, drule (1) mp)
-  apply (simp add: projectKOs objBits_simps)
+  apply (simp add: projectKOs objBits_simps add_mask_fold)
   done
 
 lemmas tcb_at'_non_kernel_data_ref'
diff --git a/proof/crefine/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy
index 7c4f2dbae3..d05900a400 100644
--- a/proof/crefine/X64/Tcb_C.thy
+++ b/proof/crefine/X64/Tcb_C.thy
@@ -115,6 +115,7 @@ lemma getObject_state:
    apply clarsimp
    apply (erule impE)
     apply simp
+   apply (simp flip: add_mask_fold)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow, simp add: word_bits_def)
@@ -135,6 +136,7 @@ lemma getObject_state:
    apply clarsimp
    apply (erule impE)
     apply simp
+   apply (simp flip: add_mask_fold)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
@@ -145,6 +147,7 @@ lemma getObject_state:
    apply fastforce
   apply clarsimp
   apply (erule impE)
+   apply (simp flip: add_mask_fold)
    apply (rule word_diff_ls'(3))
    apply unat_arith
    apply (drule is_aligned_no_overflow)
@@ -210,6 +213,7 @@ lemma asUser_state:
      apply fastforce
     apply clarsimp
     apply (erule impE, simp)
+    apply (simp flip: add_mask_fold)
     apply (erule notE, rule word_diff_ls'(3))
      apply unat_arith
     apply (drule is_aligned_no_overflow)
@@ -237,6 +241,7 @@ lemma asUser_state:
      apply fastforce
     apply clarsimp
     apply (erule impE, simp)
+    apply (simp flip: add_mask_fold)
     apply (erule notE, rule word_diff_ls'(3))
      apply unat_arith
     apply (drule is_aligned_no_overflow)
@@ -248,6 +253,7 @@ lemma asUser_state:
     apply fastforce
    apply clarsimp
    apply (erule impE)
+    apply (simp flip: add_mask_fold)
     apply (rule word_diff_ls'(3))
      apply unat_arith
     apply (drule is_aligned_no_overflow)
@@ -979,6 +985,7 @@ lemma invokeTCB_ThreadControl_ccorres:
    apply (clarsimp simp: cte_level_bits_def Kernel_C.tcbCTable_def Kernel_C.tcbVTable_def
                          tcbCTableSlot_def tcbVTableSlot_def size_of_def
                          tcb_cte_cases_def isCap_simps tcb_aligned' obj_at'_is_canonical
+                         cteSizeBits_def
                   split: option.split_asm
                   dest!: isValidVTableRootD invs_pspace_canonical')
   apply (clarsimp simp: valid_cap'_def capAligned_def word_bits_conv
@@ -1312,6 +1319,7 @@ lemma getObject_context:
    apply clarsimp
    apply (erule impE)
     apply simp
+   apply (simp flip: add_mask_fold)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
@@ -1333,6 +1341,7 @@ lemma getObject_context:
    apply clarsimp
    apply (erule impE)
     apply simp
+   apply (simp flip: add_mask_fold)
    apply (erule notE, rule word_diff_ls'(3))
     apply unat_arith
    apply (drule is_aligned_no_overflow)
@@ -1343,6 +1352,7 @@ lemma getObject_context:
    apply fastforce
   apply clarsimp
   apply (erule impE)
+   apply (simp flip: add_mask_fold)
    apply (rule word_diff_ls'(3))
    apply unat_arith
    apply (drule is_aligned_no_overflow)
@@ -1408,6 +1418,7 @@ lemma asUser_context:
      apply fastforce
     apply clarsimp
     apply (erule impE, simp)
+    apply (simp flip: add_mask_fold)
     apply (erule notE, rule word_diff_ls'(3))
      apply unat_arith
     apply (drule is_aligned_no_overflow)
@@ -1419,6 +1430,7 @@ lemma asUser_context:
     apply fastforce
    apply clarsimp
    apply (erule impE)
+    apply (simp flip: add_mask_fold)
     apply (rule word_diff_ls'(3))
      apply unat_arith
     apply (drule is_aligned_no_overflow)