diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy
index c74541b24c..16525f3fa2 100644
--- a/proof/crefine/AARCH64/ADT_C.thy
+++ b/proof/crefine/AARCH64/ADT_C.thy
@@ -161,17 +161,6 @@ where
   "getContext_C thread \<equiv>
    \<lambda>s. from_user_context_C (tcbContext_C (the (clift (t_hrs_' (globals s)) (Ptr &(thread\<rightarrow>[''tcbArch_C''])))))"
 
-(* FIXME AARCH64 move, this is very specific and rather ugly, is it possible to generalise? *)
-lemma size_64_less_64:
-  "size (r::64) < (64::nat)"
-  apply (induct r rule: bit0.plus_induct, simp)
-  apply (frule bit0.Suc_size)
-  apply (case_tac "x = 64 - 1"; clarsimp)
-  apply (prop_tac "size x \<noteq> size (64 - 1 :: 64)")
-   apply (subst bit0.size_inj, simp)
-  apply simp
-  done
-
 lemma from_user_context_C:
   "ccontext_relation uc uc' \<Longrightarrow> from_user_context_C uc' = uc"
   unfolding ccontext_relation_def cregs_relation_def
@@ -944,9 +933,6 @@ lemma option_to_ctcb_ptr_inj:
   apply (erule is_aligned_no_overflow_0; simp)
   done
 
-(* FIXME AARCH64 this is bad news, we need the alignment constraints to use option_to_ctcb_ptr_inj,
-   and we used to be able to say that if there's a non-null tcb pointer in a vcpu, then it's aligned,
-   but on AARCH64 we don't have anything like that in vcpu validity, so we are stuck *)
 lemma cpspace_vcpu_relation_unique:
   assumes "cpspace_vcpu_relation ah ch" "cpspace_vcpu_relation ah' ch"
   assumes "\<forall>x \<in> ran (map_to_vcpus ah). is_aligned_opt (vcpuTCBPtr x) tcbBlockSizeBits"
@@ -1064,19 +1050,6 @@ lemma cpspace_asidpool_relation_unique:
    apply (clarsimp simp: non_dom_eval_eq)
   apply force
   done
-(* FIXME AARCH64 old proof for reference, remove if not needed after rest of ADT_H is fixed
-   apply clarsimp
-   apply (case_tac "i \<le> mask asid_low_bits", simp)
-    apply (drule sym[where s="option_to_ptr _"], simp)
-    apply (simp add: option_to_ptr_def option_to_0_def ran_def split: option.splits)
-   apply clarsimp
-   apply (drule_tac c=i in contra_subsetD, simp)+
-   apply (clarsimp simp: non_dom_eval_eq)
-  apply clarsimp
-  apply (rule ccontr)
-  apply clarsimp
-  apply blast
-  done *)
 
 lemma cpspace_user_data_relation_unique:
   "\<lbrakk>cmap_relation (heap_to_user_data ah bh) (clift ch) Ptr cuser_user_data_relation;
@@ -1308,12 +1281,6 @@ lemma ksPSpace_eq_imp_valid_tcb'_eq:
                  valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def valid_arch_tcb'_def
           split: thread_state.splits option.splits)
 
-(* FIXME AARCH64 we don't have valid_vcpu' on AARCH64
-lemma ksPSpace_eq_imp_valid_vcpu'_eq:
-  assumes ksPSpace: "ksPSpace s' = ksPSpace s"
-  shows "valid_vcpu' vcpu s' = valid_vcpu' vcpu s"
-  by (auto simp: valid_vcpu'_def ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace] split: option.splits) *)
-
 lemma ksPSpace_eq_imp_valid_objs'_eq:
   assumes ksPSpace: "ksPSpace s' = ksPSpace s"
   shows "valid_objs' s' = valid_objs' s"
diff --git a/proof/crefine/AARCH64/ArchMove_C.thy b/proof/crefine/AARCH64/ArchMove_C.thy
index 64d093f547..82a56f5720 100644
--- a/proof/crefine/AARCH64/ArchMove_C.thy
+++ b/proof/crefine/AARCH64/ArchMove_C.thy
@@ -462,7 +462,6 @@ crunch ko_at'[wp]: readVCPUReg "\<lambda>s. P (ko_at' a p s)"
 
 crunch obj_at'[wp]: readVCPUReg "\<lambda>s. P (obj_at' a p s)"
 
-(* FIXME AARCH64 this might not be needed, but currently proved version doesn't have the P
 crunch pred_tcb_at'[wp]: readVCPUReg "\<lambda>s. P (pred_tcb_at' a b p s)"  *)
 
 crunch ksCurThread[wp]: readVCPUReg "\<lambda>s. P (ksCurThread s)"
diff --git a/proof/crefine/AARCH64/Arch_C.thy b/proof/crefine/AARCH64/Arch_C.thy
index 57f6efd6bf..bd27a30ae5 100644
--- a/proof/crefine/AARCH64/Arch_C.thy
+++ b/proof/crefine/AARCH64/Arch_C.thy
@@ -745,7 +745,6 @@ lemma ccap_relation_VSpaceCap_IsMapped:
   apply (simp add: to_bool_def)
   done
 
-(* FIXME AARCH64 do we also want VSRootPT_T/cap_vspace_cap_lift? *)
 lemma ccap_relation_PageTableCap_BasePtr:
   "\<lbrakk> ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap p NormalPT_T m)) ccap \<rbrakk>
    \<Longrightarrow> capPTBasePtr_CL (cap_page_table_cap_lift ccap) = p"
@@ -754,7 +753,6 @@ lemma ccap_relation_PageTableCap_BasePtr:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits)
   done
 
-(* FIXME AARCH64 do we also want VSRootPT_T/cap_vspace_cap_lift? *)
 lemma ccap_relation_PageTableCap_MappedASID:
   "\<lbrakk> ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap p NormalPT_T (Some (a,b))))
                    ccap \<rbrakk>
@@ -888,7 +886,7 @@ lemma slotcap_in_mem_VSpace:
   apply (simp add: cap_get_tag_isCap_ArchObject2)
   done
 
-lemma pptrUserTop_val: (* FIXME AARCH64: need value spelled out for C code *)
+lemma pptrUserTop_val: (* FIXME AARCH64: need value spelled out for C code, make schematic *)
   "pptrUserTop = 0xFFFFFFFFFFF"
   by (simp add: pptrUserTop_def mask_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
 
@@ -898,11 +896,6 @@ lemma ccap_relation_vspace_base: (* FIXME AARCH64: move up if needed in VSpace_R
   by (frule cap_get_tag_isCap_unfolded_H_cap)
      (clarsimp simp: cap_vspace_cap_lift ccap_relation_def cap_to_H_def split: if_splits)
 
-(* The magic 4 comes out of the bitfield generator *)
-lemma ThreadState_Restart_mask[simp]: (* FIXME AARCH64: move far up *)
-  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
-  by (simp add: ThreadState_Restart_def mask_def)
-
 lemma Restart_valid[simp]:
   "valid_tcb_state' Restart s"
   by (simp add: valid_tcb_state'_def)
@@ -1297,11 +1290,6 @@ definition
                             (pde_range_C.length_C pde_ran))
           \<and> 1 \<le> pde_range_C.length_C pde_ran"
 
-(* FIXME AARCH64 do we want an analogue for AARCH64?
-definition
- "vm_attribs_relation attr attr' \<equiv>
-       riscvExecuteNever_CL (vm_attributes_lift attr') = from_bool (riscvExecuteNever attr)" *)
-
 lemma framesize_from_H_eqs:
   "(framesize_from_H vsz = scast Kernel_C.ARMSmallPage) = (vsz = ARMSmallPage)"
   "(framesize_from_H vsz = scast Kernel_C.ARMLargePage) = (vsz = ARMLargePage)"
@@ -1348,7 +1336,7 @@ lemma cpte_relation_pte_invalid_eq:
   "cpte_relation pte pte' \<Longrightarrow> (pte_lift pte' = Some Pte_pte_invalid) = (pte = InvalidPTE)"
   by (clarsimp simp: cpte_relation_def Let_def split: if_splits pte.splits)
 
-lemma from_bool_inj[simp]: (* FIXME AARCH64: move up *)
+lemma from_bool_inj[simp]: (* FIXME AARCH64: move to Word_Lib *)
   "(from_bool x = from_bool y) = (x = y)"
   unfolding from_bool_def
   by (auto split: bool.splits)
@@ -1415,24 +1403,6 @@ lemma performPageInvocationMap_ccorres:
                          ccap_relation_FrameCap_MappedAddress)
   done
 
-lemma vaddr_segment_nonsense3_folded: (* FIXME AARCH64: remove if unused, also in RISCV64 and X64 *)
-  "is_aligned (p :: machine_word) pageBits \<Longrightarrow>
-   (p + ((vaddr >> pageBits) && mask ((pt_bits pt_t) - word_size_bits) << word_size_bits) &&
-     ~~ mask (pt_bits pt_t)) = p"
-  apply (rule is_aligned_add_helper[THEN conjunct2])
-   apply (simp add: bit_simps mask_def)+
-   (* FIXME AARCH64 abstraction violation *)
-   apply (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
-  (* FIXME AARCH64 consider cleanup *)
-  apply (cases pt_t; clarsimp simp: bit_simps mask_def split: if_splits)
-   apply (simp_all add: shiftl_less_t2n[where m=12 and n=3, simplified,
-                                        OF and_mask_less'[where n=9, unfolded mask_def, simplified]])
-  apply clarsimp
-  apply (rule shiftl_less_t2n[where m=13, simplified]; simp)
-  apply (rule and_mask_less'[where n=10, simplified mask_def, simplified])
-  apply simp
-  done
-
 lemma performPageGetAddress_ccorres:
   "ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' ((=) Restart))
@@ -1556,18 +1526,6 @@ lemma slotcap_in_mem_valid:
   apply (erule(1) ctes_of_valid')
   done
 
-lemma unat_less_iff64: (* FIXME AARCH64: remove if unused *)
-  "\<lbrakk>unat (a::machine_word) = b;c < 2^word_bits\<rbrakk>
-   \<Longrightarrow> (a < of_nat c) = (b < c)"
-  apply (rule iffI)
-    apply (drule unat_less_helper)
-    apply simp
-  apply (simp add:unat64_eq_of_nat)
-  apply (rule of_nat_mono_maybe)
-   apply (simp add:word_bits_def)
-  apply simp
-  done
-
 lemma injection_handler_if_returnOk:
   "injection_handler Inl (if a then b else returnOk c)
   = (if a then (injection_handler Inl b) else returnOk c)"
@@ -1580,11 +1538,6 @@ lemma injection_handler_if_returnOk:
 lemma pbfs_less: "pageBitsForSize sz < 31"
   by (case_tac sz,simp_all add: bit_simps)
 
-definition
-  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option" (* FIXME AARCH64: remove if unused, also in X64 and RISCV64 *)
-where
-  "to_option f x \<equiv> if f x then Some x else None"
-
 lemma cte_wp_at_eq_gsMaxObjectSize:
   "cte_wp_at' ((=) cap o cteCap) slot s
     \<Longrightarrow> valid_global_refs' s
@@ -1673,8 +1626,7 @@ lemma ccap_relation_FrameCap_IsMapped:
   apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits)
   done
 
-(* FIXME AARCH64: move *)
-lemma and_1_0_not_bit_0:
+lemma and_1_0_not_bit_0: (* FIXME AARCH64: move to Word_Lib *)
   "(w && 1 = 0) = (\<not> (w::'a::len word) !! 0)"
   using to_bool_and_1[simplified to_bool_def, where x=w]
   by auto
diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy
index 744853ef91..494fe0de8a 100644
--- a/proof/crefine/AARCH64/CSpace_C.thy
+++ b/proof/crefine/AARCH64/CSpace_C.thy
@@ -1902,8 +1902,7 @@ lemma clearUntypedFreeIndex_noop_ccorres:
   apply simp
   done
 
-(* FIXME AARCH64 move *)
-lemma mask_shiftl_le_mask:
+lemma mask_shiftl_le_mask: (* FIXME AARCH64 move to Word_Lib *)
   "mask n << m \<le> (mask (n+m) :: 'a::len word)"
   by (subst add.commute)
      (rule leq_high_bits_shiftr_low_bits_leq_bits, simp)
diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy
index f8eb3cfb28..1e88f94e17 100644
--- a/proof/crefine/AARCH64/Finalise_C.thy
+++ b/proof/crefine/AARCH64/Finalise_C.thy
@@ -1118,7 +1118,7 @@ lemma deleteASIDPool_ccorres:
              apply (rule ccorres_move_c_guard_ap)
              apply (rule_tac ccorres_symb_exec_r2)
                apply csymbr
-               apply (rule ccorres_guard_imp) (* FIXME AARCH64: csymbr messes up C precond *)
+               apply (rule ccorres_guard_imp)
                  apply (rule_tac R="\<lambda>_. True" and
                                  R'="\<lbrace>(inv asidpool.ASIDPool poolKO (of_nat n) \<noteq> None) \<longleftrightarrow>
                                       (asid_map_get_tag \<acute>asid_map = scast asid_map_asid_map_vspace)\<rbrace> \<inter>
@@ -1131,7 +1131,6 @@ lemma deleteASIDPool_ccorres:
                  apply (rule ccorres_return_Skip)
                 apply clarsimp
                 apply assumption
-               (* FIXME AARCH64: repairing broken csymbr C precond matching *)
                apply (clarsimp split: if_split simp: upto_enum_word simp del: upt.simps)
                apply (drule CollectD, assumption)
               apply clarsimp
@@ -1905,9 +1904,6 @@ lemma Zombie_new_spec:
   apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified])
   done
 
-(* FIXME AARCH64 move? retire? revisit *)
-lemmas upcast_ucast_id = More_Word.ucast_up_inj
-
 lemma ccap_relation_IRQHandler_mask:
   "\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk>
     \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 9
@@ -2618,7 +2614,7 @@ lemma Arch_finaliseCap_ccorres:
                        F="\<lambda>asid'. asid' = asid" and
                        R=\<top> and
                        R'=UNIV
-                       in ccorres_symb_exec_r_abstract_UNIV) (* FIXME AARCH64: csymbr fails *)
+                       in ccorres_symb_exec_r_abstract_UNIV)
           apply vcg
           apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 dest!: cap_to_H_VSCap)
           apply (clarsimp simp: cap_vspace_cap_lift_def cap_vspace_cap_lift)
@@ -2655,7 +2651,7 @@ lemma Arch_finaliseCap_ccorres:
                       F="\<lambda>asid'. asid' = asid" and
                       R=\<top> and
                       R'=UNIV
-                      in ccorres_symb_exec_r_abstract_UNIV) (* FIXME AARCH64: csymbr fails *)
+                      in ccorres_symb_exec_r_abstract_UNIV)
          apply vcg
          apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 dest!: cap_to_H_PTCap)
          apply (clarsimp simp: cap_page_table_cap_lift_def cap_page_table_cap_lift)
diff --git a/proof/crefine/AARCH64/IpcCancel_C.thy b/proof/crefine/AARCH64/IpcCancel_C.thy
index 1c95b3caad..ae15dd14ba 100644
--- a/proof/crefine/AARCH64/IpcCancel_C.thy
+++ b/proof/crefine/AARCH64/IpcCancel_C.thy
@@ -144,7 +144,7 @@ lemma tcbEPDequeue_spec:
    apply simp
   apply (frule c_guard_clift)
   apply (simp add: typ_heap_simps')
-  apply (intro allI conjI impI) (* FIXME AARCH64 different number of goals, not sure why *)
+  apply (intro allI conjI impI)
                apply (clarsimp simp add: typ_heap_simps h_t_valid_clift_Some_iff)
               apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff
                               cong: if_weak_cong)
diff --git a/proof/crefine/AARCH64/Machine_C.thy b/proof/crefine/AARCH64/Machine_C.thy
index 11b815ff0a..1e02ad82ad 100644
--- a/proof/crefine/AARCH64/Machine_C.thy
+++ b/proof/crefine/AARCH64/Machine_C.thy
@@ -62,7 +62,7 @@ assumes maskInterrupt_ccorres:
            (doMachineOp (maskInterrupt m irq))
            (Call maskInterrupt_'proc)"
 
-(* FIXME AARCH64 this is a simplification until complete FPU handling is added at a future date *)
+(* This is a simplification until complete FPU handling is added at a future date *)
 assumes fpuThreadDelete_ccorres:
   "ccorres dc xfdc (tcb_at' thread) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
      (fpuThreadDelete thread)
@@ -265,14 +265,6 @@ assumes vcpu_hw_write_reg_ccorres:
            (doMachineOp (writeVCPUHardwareReg r v))
            (Call vcpu_hw_write_reg_'proc)"
 
-(* FIXME AARCH64 these were RISCV64 machine op ccorres assumptions, remove after we have new ones
-assumes hwASIDFlush_ccorres:
-  "ccorres dc xfdc \<top> (\<lbrace>\<acute>asid___unsigned_long = asid\<rbrace>) []
-           (doMachineOp (AARCH64.hwASIDFlush asid))
-           (Call hwASIDFlush_'proc)"
-
-*)
-
 (* The following are fastpath specific assumptions.
    We might want to move them somewhere else. *)
 
diff --git a/proof/crefine/AARCH64/Recycle_C.thy b/proof/crefine/AARCH64/Recycle_C.thy
index 99e23c225a..19648fe9be 100644
--- a/proof/crefine/AARCH64/Recycle_C.thy
+++ b/proof/crefine/AARCH64/Recycle_C.thy
@@ -571,59 +571,6 @@ lemma page_table_at_rf_sr_dom_s:
   apply (auto simp add: intvl_def shiftl_t2n pte_bits_def word_size_bits_def)[1]
   done
 
-(* FIXME AARCH64 this currently doesn't make sense, update when going through Arch_C so that it's at
-   least useful
-   clearMemory corresponds to clearMemory on the Haskell side, and that contains a cleanCacheRange_RAM
-lemma clearMemory_setObject_PTE_ccorres:
-  "ccorres dc xfdc (page_table_at' pt_t ptr
-                and (\<lambda>s. 2 ^ (ptBits pt_t) \<le> gsMaxObjectSize s)
-                and (\<lambda>_. is_aligned ptr (ptBits pt_t) \<and> ptr \<noteq> 0 \<and> pstart = addrFromPPtr ptr))
-            (UNIV \<inter> {s. ptr___ptr_to_unsigned_long_' s = Ptr ptr} \<inter> {s. bits_' s = of_nat (ptBits pt_t)}) []
-       (do mapM_x (\<lambda>a. setObject a AARCH64_H.InvalidPTE)
-                        [ptr , ptr + 2 ^ objBits AARCH64_H.InvalidPTE .e. ptr + 2 ^ (ptBits pt_t) - 1];
-           cleanCacheRange_RAM ???
-        od)
-       (Call clearMemory_'proc)"
-  apply (rule ccorres_gen_asm)+
-  apply (cinit' lift: ptr___ptr_to_unsigned_long_' bits_')
-   apply (rule ccorres_Guard_Seq)
-
-
-   apply (rule_tac P="page_table_at' pt_t ptr and (\<lambda>s. 2 ^ (ptBits pt_t) \<le> gsMaxObjectSize s)"
-               in ccorres_from_vcg_nofail[where P'=UNIV])
-   apply (rule allI, rule conseqPre, vcg)
-   apply clarsimp
-   apply (subst ghost_assertion_size_logic[unfolded o_def])
-     apply (simp add: bit_simps)
-    apply assumption
-   apply (clarsimp simp: replicateHider_def[symmetric] bit_simps)
-   apply (frule is_aligned_no_overflow', simp)
-   apply (intro conjI)
-      apply (erule is_aligned_weaken, simp)
-     apply (clarsimp simp: is_aligned_def)
-    using page_table_at_rf_sr_dom_s
-    apply (simp add: bit_simps)
-   apply (clarsimp simp add: bit_simps
-                      cong: StateSpace.state.fold_congs globals.fold_congs)
-   apply (simp add: upto_enum_step_def objBits_simps bit_simps add.commute[where b=ptr]
-                    linorder_not_less[symmetric] archObjSize_def
-                    upto_enum_word split_def)
-  apply (erule mapM_x_store_memset_ccorres_assist
-                      [unfolded split_def, OF _ _ _ _ _ _ subset_refl],
-         simp_all add: shiftl_t2n hd_map objBits_simps archObjSize_def bit_simps)[1]
-   apply (rule cmap_relationE1, erule rf_sr_cpte_relation, erule ko_at_projectKO_opt)
-   apply (subst coerce_memset_to_heap_update_pte)
-   apply (clarsimp simp: rf_sr_def Let_def cstate_relation_def typ_heap_simps)
-   apply (rule conjI)
-    apply (simp add: cpspace_relation_def typ_heap_simps update_pte_map_tos
-                     update_pte_map_to_ptes carray_map_relation_upd_triv)
-    apply (rule cmap_relation_updI, simp_all)[1]
-    apply (simp add: cpte_relation_def Let_def pte_lift_def)
-   apply (simp add: carch_state_relation_def cmachine_state_relation_def
-                    update_pte_map_tos)
-  apply simp
-  done *)
-
 lemma ccorres_make_xfdc:
   "ccorresG rf_sr \<Gamma> r xf P P' h a c \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc P P' h a c"
   apply (erule ccorres_rel_imp)
diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy
index ddfb5e532f..2f97581052 100644
--- a/proof/crefine/AARCH64/Retype_C.thy
+++ b/proof/crefine/AARCH64/Retype_C.thy
@@ -35,14 +35,6 @@ lemma sle_positive: "\<lbrakk> b < 0x8000000000000000; (a :: machine_word) \<le>
   apply (clarsimp simp:word_le_def)
   done
 
-lemma sless_positive: "\<lbrakk> b < 0x8000000000000000; (a :: machine_word) < b \<rbrakk> \<Longrightarrow> a <s b"
-  apply (clarsimp simp: word_sless_def)
-  apply (rule conjI)
-   apply (erule sle_positive)
-   apply simp
-  apply simp
-  done
-
 lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x8000000000000000 \<rbrakk> \<Longrightarrow> 0 \<le> sint a"
   apply (subst sint_eq_uint)
    apply (simp add:unat_less_helper)
@@ -51,7 +43,6 @@ lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x80000000000000
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-(* FIXME AARCH64 we have multiple page table index sizes *)
 lemma map_option_byte_to_word_heap:
   assumes disj: "\<And>(off :: 9 word) x. x<8 \<Longrightarrow> p + ucast off * 8 + x \<notin> S " (*9=page table index*)
   shows "byte_to_word_heap (\<lambda>x. if x \<in> S then 0 else mem x) p
@@ -5844,8 +5835,6 @@ lemma updatePTType_ccorres:
   apply (clarsimp simp: cvariable_array_map_relation_def split: if_splits)
   done
 
-(* FIXME AARCH64 multiple issues in vspace objects, possibly missing ghost state updates, and
-   page table ghost state in state relation *)
 lemma Arch_createObject_ccorres:
   assumes t: "toAPIType newType = None"
   shows "ccorres (\<lambda>a b. ccap_relation (ArchObjectCap a) b) ret__struct_cap_C_'
@@ -5856,7 +5845,6 @@ lemma Arch_createObject_ccorres:
      (Call Arch_createObject_'proc)"
 proof -
   note if_cong[cong]
-  (* FIXME AARCH64 note sign_extend_canonical_address[simp] *)
 
   show ?thesis
     apply (clarsimp simp: createObject_c_preconds_def
diff --git a/proof/crefine/AARCH64/StateRelation_C.thy b/proof/crefine/AARCH64/StateRelation_C.thy
index 04be4b1c68..a949af4312 100644
--- a/proof/crefine/AARCH64/StateRelation_C.thy
+++ b/proof/crefine/AARCH64/StateRelation_C.thy
@@ -444,7 +444,6 @@ lemma pte_0:
    pte_lift cpte = Some (Pte_pte_invalid)"
   by (simp add: pte_lift_def pte_get_tag_def pte_tag_defs)
 
-(* FIXME AARCH64 review *)
 (* with hypervisor support enabled, use stage-2 translation format for PTE *)
 (* see makeUserPage in C *)
 definition cpte_relation :: "pte \<Rightarrow> pte_C \<Rightarrow> bool" where
@@ -461,8 +460,7 @@ definition cpte_relation :: "pte \<Rightarrow> pte_C \<Rightarrow> bool" where
         then cpte' = Some (Pte_pte_4k_page
                              \<lparr> pte_pte_4k_page_CL.UXN_CL = of_bool xn,
                                page_base_address_CL = baseaddr,
-                               nG_CL = from_bool global, \<comment> \<open>flipped in hyp mode
-                                 (* FIXME AARCH64 check manual for what this really means *)\<close>
+                               nG_CL = from_bool global, \<comment> \<open>flipped in hyp mode\<close>
                                AF_CL = 1,
                                SH_CL = 0,
                                AP_CL = ap_from_vm_rights vmrights,
diff --git a/proof/crefine/AARCH64/Syscall_C.thy b/proof/crefine/AARCH64/Syscall_C.thy
index 2b463dcc08..7932ce9289 100644
--- a/proof/crefine/AARCH64/Syscall_C.thy
+++ b/proof/crefine/AARCH64/Syscall_C.thy
@@ -1718,7 +1718,6 @@ lemma word_ctz_upcast_id:
   unfolding word_ctz_def
   by (simp add: ucast_up_app source_size_def target_size_def eq_zero_set_bl)
 
-(* FIXME AARCH64 stated to use machine_word on ARM_HYP, which works there by coincidence *)
 (* folded calculation of eisr used in vgicMaintenance *)
 definition
   eisr_calc :: "32 word \<Rightarrow> 32 word \<Rightarrow> nat"
diff --git a/proof/crefine/AARCH64/TcbQueue_C.thy b/proof/crefine/AARCH64/TcbQueue_C.thy
index 8d14299465..55e295aa36 100644
--- a/proof/crefine/AARCH64/TcbQueue_C.thy
+++ b/proof/crefine/AARCH64/TcbQueue_C.thy
@@ -894,45 +894,6 @@ lemma tcb_queue_relation'_prev_mask:
   shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)"
   by (rule tcb_queue_relation_prev_mask [OF tcb_queue_relation'_queue_rel], fact+)
 
-(* FIXME AARCH64 sign-extensions and pspace_canonical' are gone, leaving these in case we end up
-   needing something analogous to demonstrate validity of pointers
-lemma tcb_queue_relation_next_sign:
-  assumes
-    "tcb_queue_relation getNext getPrev mp queue NULL qhead" and
-    valid_ep: "\<forall>t\<in>set queue. tcb_at' t s"
-    "distinct queue"
-    "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
-    "tcbp \<in> set queue"  and
-    canon: "pspace_canonical' s"
-  shows "sign_extend canonical_bit (ptr_val (getNext tcb)) = ptr_val (getNext tcb)"
-proof (cases "(getNext tcb) = NULL")
-  case True
-  thus ?thesis by simp
-next
-  case False
-
-  hence "ctcb_ptr_to_tcb_ptr (getNext tcb) \<in> set queue" using assms
-    apply -
-    apply (drule (3) tcb_queueD)
-    apply (clarsimp split: if_split_asm)
-    done
-
-  with valid_ep(1) have tcb: "tcb_at' (ctcb_ptr_to_tcb_ptr (getNext tcb)) s" ..
-  with canon have "canonical_address (ctcb_ptr_to_tcb_ptr (getNext tcb))" by (simp add: obj_at'_is_canonical)
-  moreover
-  have "is_aligned (ctcb_ptr_to_tcb_ptr (getNext tcb)) tcbBlockSizeBits" using tcb by (rule tcb_aligned')
-  ultimately
-  have "canonical_address (ptr_val (getNext tcb))" by (rule canonical_address_ctcb_ptr)
-  thus ?thesis
-    by (simp add: sign_extend_canonical_address[symmetric] canonical_bit_def)
-qed
-
-lemma tcb_queue_relation'_next_sign:
-  "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>t\<in>set queue. tcb_at' t s;
-     distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \<in> set queue; pspace_canonical' s\<rbrakk>
-\<Longrightarrow> sign_extend canonical_bit (ptr_val (getNext tcb)) = ptr_val (getNext tcb)"
-  by (rule tcb_queue_relation_next_sign [OF tcb_queue_relation'_queue_rel])
-
 lemma tcb_queue_relation_prev_sign:
   assumes
     "tcb_queue_relation getNext getPrev mp queue NULL qhead" and
@@ -1477,10 +1438,5 @@ lemma rf_sr_tcb_update_not_in_queue:
   apply (simp add: carch_state_relation_def)
   by (simp add: cmachine_state_relation_def)
 
-(* FIXME AARCH64 unused on all arches, remove: rf_sr_tcb_update_not_in_queue2,
-   rf_sr_tcb_update_not_in_queue *)
-lemmas rf_sr_tcb_update_not_in_queue2
-    = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified]
-
 end
 end
diff --git a/proof/crefine/AARCH64/Tcb_C.thy b/proof/crefine/AARCH64/Tcb_C.thy
index 50808a7288..445ce17692 100644
--- a/proof/crefine/AARCH64/Tcb_C.thy
+++ b/proof/crefine/AARCH64/Tcb_C.thy
@@ -536,13 +536,6 @@ lemma threadSet_ipcbuffer_invs:
   apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong)
   done
 
-(* FIXME AARCH64 this likely needs to be something with make_canonical
-lemma canonical_address_bitfield_extract_tcb:
-  "\<lbrakk>canonical_address t; is_aligned t tcbBlockSizeBits\<rbrakk> \<Longrightarrow>
-     t = ctcb_ptr_to_tcb_ptr (tcb_Ptr (sign_extend canonical_bit (ptr_val (tcb_ptr_to_ctcb_ptr t))))"
-  apply (drule (1) canonical_address_tcb_ptr)
-  by (fastforce simp: sign_extended_iff_sign_extend canonical_address_sign_extended) *)
-
 (* FIXME AARCH64 move to SR_Lemmas where the RISCV64 version is *)
 lemma canonical_address_tcb_ptr:
   "\<lbrakk> canonical_address t; is_aligned t tcbBlockSizeBits \<rbrakk>
diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy
index fa04396e57..f25894bc9f 100644
--- a/proof/crefine/AARCH64/VSpace_C.thy
+++ b/proof/crefine/AARCH64/VSpace_C.thy
@@ -63,45 +63,6 @@ lemma unat_of_nat_pageBitsForSize[simp]:
   apply simp
   done
 
-(* FIXME AARCH64 checkVPAlignment has gone missing in C, it is used in decodeRISCVFrameInvocation
-   for RISCVPageMap, and on ARM_HYP for decodeARMFrameInvocation/ARMPageMap
-   For AARCH64 it does the calculation inline via a macro: IS_PAGE_ALIGNED(vaddr, frameSize)
-   TODO: re-introduce checkVPAlignment in C
-lemma checkVPAlignment_ccorres:
-  "ccorres (\<lambda>a c. if to_bool c then a = Inr () else a = Inl AlignmentError) ret__unsigned_long_'
-           \<top>
-           (\<lbrace>sz = framesize_to_H \<acute>sz \<and> \<acute>sz < 3\<rbrace> \<inter> \<lbrace>\<acute>w = w\<rbrace>)
-           []
-           (checkVPAlignment sz w)
-           (Call checkVPAlignment_'proc)"
-  apply (cinit lift: sz_' w_')
-   apply (csymbr)
-   apply clarsimp
-   apply (rule ccorres_Guard [where A=\<top> and C'=UNIV])
-   apply (simp split: if_split)
-   apply (rule conjI)
-    apply (clarsimp simp: mask_def unlessE_def returnOk_def)
-    apply (rule ccorres_guard_imp)
-      apply (rule ccorres_return_C)
-        apply simp
-       apply simp
-      apply simp
-     apply simp
-    apply (simp split: if_split)
-   apply (clarsimp simp: mask_def unlessE_def throwError_def split: if_split)
-   apply (rule ccorres_guard_imp)
-     apply (rule ccorres_return_C)
-       apply simp
-      apply simp
-     apply simp
-    apply simp
-   apply (simp split: if_split)
-  apply (clarsimp split: if_split)
-  apply (simp add: word_less_nat_alt)
-  apply (rule order_le_less_trans, rule pageBitsForSize_le)
-  apply simp
-  done *)
-
 lemma rf_asidTable:
   "\<lbrakk> (\<sigma>, x) \<in> rf_sr; valid_arch_state' \<sigma>; idx \<le> mask asid_high_bits \<rbrakk>
      \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>)
@@ -200,35 +161,6 @@ lemma no_fail_seL4_Fault_VMFault_new':
   apply terminates_trivial
   done
 
-(* FIXME AARCH64 this doesn't make much sense currently with hyp, but was a helper used by
-     handleVMFault_ccorres, so possibly could still have that role once updated *)
-lemma returnVMFault_corres:
-  "\<lbrakk> addr = addr'; i = i' && mask 1; fault = fault' && mask 32 \<rbrakk> \<Longrightarrow>
-   corres_underlying
-     {(x, y). cstate_relation x y} True True
-     (lift_rv id (\<lambda>y. ()) (\<lambda>e. e) (\<lambda>_ _. False)
-                 (\<lambda>e f e'. f = SCAST(32 signed \<rightarrow> 64) EXCEPTION_FAULT \<and>
-                           (\<exists>vf. e = ArchFault (VMFault (address_CL vf) [instructionFault_CL vf, FSR_CL vf])
-                                       \<and> errfault e' = Some (SeL4_Fault_VMFault vf))))
-     \<top> \<top>
-     (throwError (Fault_H.fault.ArchFault (VMFault addr [i, fault])))
-     (do f <- seL4_Fault_VMFault_new' addr' fault' i';
-         _ <- modify (current_fault_'_update (\<lambda>_. f));
-         e <- gets errglobals;
-         return (scast EXCEPTION_FAULT, e)
-      od)"
-  apply (rule corres_symb_exec_r)
-     apply (rename_tac vmf)
-     apply (rule_tac F="seL4_Fault_VMFault_lift vmf = \<lparr>address_CL = addr, FSR_CL = fault && mask 32, instructionFault_CL = i && mask 1\<rparr>
-                         \<and> seL4_Fault_get_tag vmf = scast seL4_Fault_VMFault"
-              in corres_gen_asm2)
-     apply (rule lift_rv_throwError;
-            clarsimp simp: exception_defs seL4_Fault_VMFault_lift)
-    apply (wpsimp wp: valid_spec_to_wp'[OF seL4_Fault_VMFault_new'_spec]
-                      no_fail_seL4_Fault_VMFault_new'
-                simp: mask_twice)+
-  done
-
 lemma handleVMFault_ccorres:
   "ccorres ((\<lambda>f ex v. ex = scast EXCEPTION_FAULT
                       \<and> (\<exists>vf. f = ArchFault (VMFault (address_CL vf)
@@ -410,47 +342,6 @@ lemma isPageTablePTE_def2:
   "isPageTablePTE pte = (\<exists>ppn. pte = PageTablePTE ppn)"
   by (simp add: isPageTablePTE_def split: pte.splits)
 
-(* FIXME AARCH64 no longer present on this arch, but be wary of analogues
-lemma getPPtrFromHWPTE_spec':
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>pte___ptr_to_struct_pte_C \<rbrace>
-           Call getPPtrFromHWPTE_'proc
-           \<lbrace> \<acute>ret__ptr_to_struct_pte_C =
-               pte_Ptr (ptrFromPAddr (pte_CL.ppn_CL (pte_lift
-                            (the (clift \<^bsup>s\<^esup>t_hrs \<^bsup>s\<^esup>pte___ptr_to_struct_pte_C))) << pageBits)) \<rbrace>"
-  by vcg (simp add: bit_simps)
-
-lemma getPPtrFromHWPTE_corres:
-  "ccorres (\<lambda>_ ptr. ptr = pte_Ptr (getPPtrFromHWPTE pte))
-     ret__ptr_to_struct_pte_C_'
-     (ko_at' pte ptePtr and K (isPageTablePTE pte))
-     \<lbrace> \<acute>pte___ptr_to_struct_pte_C = pte_Ptr ptePtr \<rbrace>
-     hs
-     (return ())
-     (Call getPPtrFromHWPTE_'proc)"
-  apply (rule ccorres_from_vcg)
-  apply (rule allI, rule conseqPre, vcg)
-  apply (clarsimp simp: return_def rf_sr_def cstate_relation_def Let_def cpspace_relation_def)
-  apply (drule (1) cmap_relation_ko_atD)
-  apply (clarsimp simp: typ_heap_simps getPPtrFromHWPTE_def cpte_relation_def Let_def
-                        isPageTablePTE_def2 bit_simps)
-  done
-
-lemma isPTEPageTable_spec':
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t \<acute>pte___ptr_to_struct_pte_C \<rbrace>
-           Call isPTEPageTable_'proc
-           \<lbrace> \<forall>cpte pte. clift \<^bsup>s\<^esup>t_hrs \<^bsup>s\<^esup>pte___ptr_to_struct_pte_C = Some cpte \<longrightarrow>
-                        cpte_relation pte cpte \<longrightarrow>
-             \<acute>ret__unsigned_long = from_bool (isPageTablePTE pte) \<rbrace>"
-  by vcg
-     (auto simp: cpte_relation_def isPageTablePTE_def2 Let_def
-                 readable_from_vm_rights_def writable_from_vm_rights_def bit_simps
-           split: bool.split if_split pte.splits vmrights.splits)
-
-lemma readable_from_vm_rights0:
-  "(readable_from_vm_rights vm = (0::machine_word)) = (vm = VMKernelOnly)"
-  by (auto simp add: readable_from_vm_rights_def split: vmrights.splits)
-*)
-
 lemma ccorres_checkPTAt:
   "ccorres_underlying srel Ga rrel xf arrel axf P P' hs (a ()) c \<Longrightarrow>
    ccorres_underlying srel Ga rrel xf arrel axf
@@ -635,7 +526,7 @@ lemma levelType_maxPTLevel[simp]: (* FIXME AARCH64: move *)
   "levelType maxPTLevel = VSRootPT_T"
   by (simp add: levelType_def)
 
-lemma unat_le_fold: (* FIXME AARCH64: move *)
+lemma unat_le_fold: (* FIXME AARCH64: move to Word_Lib *)
   "n < 2 ^ LENGTH('a) \<Longrightarrow> (unat x \<le> n) = (x \<le> of_nat n)" for x::"'a::len word"
   by (simp add: word_le_nat_alt unat_of_nat_eq)
 
@@ -1818,10 +1709,6 @@ lemma setVMRoot_ccorres:
               elim!: ccap_relationE
               split: if_split_asm cap_CL.splits)
 
-lemma ccorres_seq_IF_False: (* FIXME AARCH64: move, check if used *)
-  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
-  by simp
-
 lemma add_mask_ignore: (* FIXME AARCH64: move to WordLib *)
   "x && mask n = 0 \<Longrightarrow> v + x && mask n = v && mask n"
   by (metis arith_simps(50) mask_eqs(2))
diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy
index 463cc7b405..efacfd9a1c 100644
--- a/proof/crefine/AARCH64/Wellformed_C.thy
+++ b/proof/crefine/AARCH64/Wellformed_C.thy
@@ -171,8 +171,6 @@ definition
   Cap_notification_cap aec \<Rightarrow> True
   | _ \<Rightarrow> False"
 
-(* FIXME AARCH64: unclear why there aren't isBlahCap_C functions for arch objects in Wellformed_C *)
-
 definition
   ep_at_C' :: "word64 \<Rightarrow> heap_raw_state \<Rightarrow> bool"
 where
@@ -638,6 +636,11 @@ where
 definition cacheLineSize :: nat where
   "cacheLineSize \<equiv> 6"
 
+(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
+lemma ThreadState_Restart_mask[simp]:
+  "(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
+  by (simp add: ThreadState_Restart_def mask_def)
+
 (* generic lemmas with arch-specific consequences *)
 
 schematic_goal size_gpRegisters:
diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy
index 516e609e78..5caca99996 100644
--- a/proof/crefine/ARM/Arch_C.thy
+++ b/proof/crefine/ARM/Arch_C.thy
@@ -2157,7 +2157,7 @@ lemma pte_get_tag_alt:
   by (auto simp add: pte_lift_def Let_def split: if_split_asm)
 
 definition
-  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option"
+  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option" (* FIXME: consider moving to Lib *)
 where
   "to_option f x \<equiv> if f x then Some x else None"
 
diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy
index 31b8baa885..0e8f182846 100644
--- a/proof/crefine/ARM_HYP/Finalise_C.thy
+++ b/proof/crefine/ARM_HYP/Finalise_C.thy
@@ -1669,8 +1669,6 @@ lemma irq_opt_relation_Some_ucast:
   apply (simp only: unat_arith_simps)
   by (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def)
 
-lemmas upcast_ucast_id = More_Word.ucast_up_inj
-
 lemma irq_opt_relation_Some_ucast':
   "\<lbrakk> x && mask 10 = x; ucast x \<le> (ucast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (ucast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
     \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)"
diff --git a/proof/crefine/ARM_HYP/TcbQueue_C.thy b/proof/crefine/ARM_HYP/TcbQueue_C.thy
index 853d4615e5..5b6dba4499 100644
--- a/proof/crefine/ARM_HYP/TcbQueue_C.thy
+++ b/proof/crefine/ARM_HYP/TcbQueue_C.thy
@@ -1199,8 +1199,5 @@ lemma rf_sr_tcb_update_not_in_queue:
                          typ_heap_simps')
   by (simp add: cmachine_state_relation_def)
 
-lemmas rf_sr_tcb_update_not_in_queue2
-    = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified]
-
 end
 end
diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy
index 16f86c76cc..36160c1267 100644
--- a/proof/crefine/ARM_HYP/VSpace_C.thy
+++ b/proof/crefine/ARM_HYP/VSpace_C.thy
@@ -2669,10 +2669,6 @@ definition
   | ARM_HYP_H.flush_type.CleanInvalidate \<Rightarrow> (label = Kernel_C.ARMPageCleanInvalidate_Data \<or> label = Kernel_C.ARMPDCleanInvalidate_Data)
   | ARM_HYP_H.flush_type.Unify \<Rightarrow> (label = Kernel_C.ARMPageUnify_Instruction \<or> label = Kernel_C.ARMPDUnify_Instruction)"
 
-lemma ccorres_seq_IF_False:
-  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
-  by simp
-
 lemma doFlush_ccorres:
   "ccorres dc xfdc (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 6 = ps && mask 6
         \<comment> \<open>ahyp version translates ps into kernel virtual before flushing\<close>
diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy
index 647c647f23..08697a656b 100644
--- a/proof/crefine/Move_C.thy
+++ b/proof/crefine/Move_C.thy
@@ -1493,4 +1493,15 @@ lemma from_to_bool_le_1_idem:
   apply (simp add: word_le_1_and_idem)
   done
 
+(* FIXME AARCH64: this is very specific and rather ugly, is it possible to generalise? *)
+lemma size_64_less_64:
+  "size (r::64) < (64::nat)"
+  apply (induct r rule: bit0.plus_induct, simp)
+  apply (frule bit0.Suc_size)
+  apply (case_tac "x = 64 - 1"; clarsimp)
+  apply (prop_tac "size x \<noteq> size (64 - 1 :: 64)")
+   apply (subst bit0.size_inj, simp)
+  apply simp
+  done
+
 end
diff --git a/proof/crefine/RISCV64/Arch_C.thy b/proof/crefine/RISCV64/Arch_C.thy
index 589d99d21b..b96179f21a 100644
--- a/proof/crefine/RISCV64/Arch_C.thy
+++ b/proof/crefine/RISCV64/Arch_C.thy
@@ -1402,15 +1402,6 @@ lemma performPageGetAddress_ccorres:
                      pred_tcb_at'_def obj_at'_def ct_in_state'_def)
   done
 
-lemma vaddr_segment_nonsense3_folded:
-  "is_aligned (p :: machine_word) pageBits \<Longrightarrow>
-   (p + ((vaddr >> pageBits) && mask (pt_bits - word_size_bits) << word_size_bits) && ~~ mask pt_bits) = p"
-  apply (rule is_aligned_add_helper[THEN conjunct2])
-   apply (simp add: bit_simps mask_def)+
-  apply (rule shiftl_less_t2n[where m=12 and n=3, simplified, OF and_mask_less'[where n=9, unfolded mask_def, simplified]])
-   apply simp+
-  done
-
 lemma vmsz_aligned_addrFromPPtr':
   "vmsz_aligned (addrFromPPtr p) sz
        = vmsz_aligned p sz"
@@ -1453,18 +1444,6 @@ lemma slotcap_in_mem_valid:
   apply (erule(1) ctes_of_valid')
   done
 
-lemma unat_less_iff64:
-  "\<lbrakk>unat (a::machine_word) = b;c < 2^word_bits\<rbrakk>
-   \<Longrightarrow> (a < of_nat c) = (b < c)"
-  apply (rule iffI)
-    apply (drule unat_less_helper)
-    apply simp
-  apply (simp add:unat64_eq_of_nat)
-  apply (rule of_nat_mono_maybe)
-   apply (simp add:word_bits_def)
-  apply simp
-  done
-
 lemma injection_handler_if_returnOk:
   "injection_handler Inl (if a then b else returnOk c)
   = (if a then (injection_handler Inl b) else returnOk c)"
@@ -1477,11 +1456,6 @@ lemma injection_handler_if_returnOk:
 lemma pbfs_less: "pageBitsForSize sz < 31"
   by (case_tac sz,simp_all add: bit_simps)
 
-definition
-  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option"
-where
-  "to_option f x \<equiv> if f x then Some x else None"
-
 lemma cte_wp_at_eq_gsMaxObjectSize:
   "cte_wp_at' ((=) cap o cteCap) slot s
     \<Longrightarrow> valid_global_refs' s
diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
index 7456e4fd20..a6af450eb3 100644
--- a/proof/crefine/RISCV64/Finalise_C.thy
+++ b/proof/crefine/RISCV64/Finalise_C.thy
@@ -1633,8 +1633,6 @@ lemma Zombie_new_spec:
   apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified])
   done
 
-lemmas upcast_ucast_id = More_Word.ucast_up_inj
-
 lemma irq_opt_relation_Some_ucast:
   "\<lbrakk> x && mask 6 = x; ucast x \<noteq> irqInvalid;
     ucast x \<le> (scast Kernel_C.maxIRQ :: 6 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
diff --git a/proof/crefine/RISCV64/TcbQueue_C.thy b/proof/crefine/RISCV64/TcbQueue_C.thy
index 60ca67b668..55b52ed358 100644
--- a/proof/crefine/RISCV64/TcbQueue_C.thy
+++ b/proof/crefine/RISCV64/TcbQueue_C.thy
@@ -1474,8 +1474,5 @@ lemma rf_sr_tcb_update_not_in_queue:
   apply (simp add: carch_state_relation_def)
   by (simp add: cmachine_state_relation_def)
 
-lemmas rf_sr_tcb_update_not_in_queue2
-    = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified]
-
 end
 end
diff --git a/proof/crefine/RISCV64/VSpace_C.thy b/proof/crefine/RISCV64/VSpace_C.thy
index 2dc48c1fe7..e5daa78946 100644
--- a/proof/crefine/RISCV64/VSpace_C.thy
+++ b/proof/crefine/RISCV64/VSpace_C.thy
@@ -969,10 +969,6 @@ lemma setVMRoot_ccorres:
               elim!: ccap_relationE
               split: if_split_asm cap_CL.splits)
 
-lemma ccorres_seq_IF_False:
-  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
-  by simp
-
 (* FIXME x64: needed? *)
 lemma ptrFromPAddr_mask6_simp[simp]:
   "ptrFromPAddr ps && mask 6 = ps && mask 6"
diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy
index 26f4689aad..e8e87ada5a 100644
--- a/proof/crefine/X64/Arch_C.thy
+++ b/proof/crefine/X64/Arch_C.thy
@@ -1589,15 +1589,6 @@ lemma pde_align_ptBits:
   apply (simp add: bit_simps)
   done
 
-lemma vaddr_segment_nonsense3_folded:
-  "is_aligned (p :: machine_word) pageBits \<Longrightarrow>
-   (p + ((vaddr >> pageBits) && mask (pt_bits - word_size_bits) << word_size_bits) && ~~ mask pt_bits) = p"
-  apply (rule is_aligned_add_helper[THEN conjunct2])
-   apply (simp add: bit_simps mask_def)+
-  apply (rule shiftl_less_t2n[where m=12 and n=3, simplified, OF and_mask_less'[where n=9, unfolded mask_def, simplified]])
-   apply simp+
-  done
-
 lemma storePDE_Basic_ccorres'':
   "ccorres dc xfdc
      (\<lambda>_. True)
@@ -1913,7 +1904,7 @@ lemma shiftr_asid_low_bits_mask_eq_0:
   apply (rule iffI[rotated])
    apply simp
   apply (rule asid_low_high_bits)
-     apply (rule upcast_ucast_id[where 'b=machine_word_len]; simp add: asid_low_bits_of_mask_eq)
+     apply (rule More_Word.ucast_up_inj[where 'b=machine_word_len]; simp add: asid_low_bits_of_mask_eq)
     apply (simp add: ucast_asid_high_bits_is_shift)
    apply (simp add: asid_wf_def mask_def)
   apply (rule asid_wf_0)
@@ -1926,18 +1917,6 @@ lemma slotcap_in_mem_valid:
   apply (erule(1) ctes_of_valid')
   done
 
-lemma unat_less_iff64:
-  "\<lbrakk>unat (a::machine_word) = b;c < 2^word_bits\<rbrakk>
-   \<Longrightarrow> (a < of_nat c) = (b < c)"
-  apply (rule iffI)
-    apply (drule unat_less_helper)
-    apply simp
-  apply (simp add:unat64_eq_of_nat)
-  apply (rule of_nat_mono_maybe)
-   apply (simp add:word_bits_def)
-  apply simp
-  done
-
 lemma injection_handler_if_returnOk:
   "injection_handler Inl (if a then b else returnOk c)
   = (if a then (injection_handler Inl b) else returnOk c)"
@@ -1950,11 +1929,6 @@ lemma injection_handler_if_returnOk:
 lemma pbfs_less: "pageBitsForSize sz < 31"
   by (case_tac sz,simp_all add: bit_simps)
 
-definition
-  to_option :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a option"
-where
-  "to_option f x \<equiv> if f x then Some x else None"
-
 lemma cte_wp_at_eq_gsMaxObjectSize:
   "cte_wp_at' ((=) cap o cteCap) slot s
     \<Longrightarrow> valid_global_refs' s
diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy
index 7425df66fc..2172200432 100644
--- a/proof/crefine/X64/Finalise_C.thy
+++ b/proof/crefine/X64/Finalise_C.thy
@@ -1701,8 +1701,6 @@ lemma irq_opt_relation_Some_ucast:
   apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def)
   done
 
-lemmas upcast_ucast_id = More_Word.ucast_up_inj
-
 lemma irq_opt_relation_Some_ucast':
   "\<lbrakk> x && mask 8 = x; ucast x \<le> (scast Kernel_C.maxIRQ :: 8 word) \<or> x \<le> (scast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
     \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast x)"
diff --git a/proof/crefine/X64/TcbQueue_C.thy b/proof/crefine/X64/TcbQueue_C.thy
index 0e1843dd58..a35c839555 100644
--- a/proof/crefine/X64/TcbQueue_C.thy
+++ b/proof/crefine/X64/TcbQueue_C.thy
@@ -1557,8 +1557,5 @@ lemma rf_sr_tcb_update_not_in_queue:
                               global_ioport_bitmap_heap_update_tag_disj_simps obj_at'_def projectKOs)
   by (simp add: cmachine_state_relation_def)
 
-lemmas rf_sr_tcb_update_not_in_queue2
-    = rf_sr_tcb_update_no_queue_helper [OF rf_sr_tcb_update_not_in_queue, simplified]
-
 end
 end
diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy
index 5d9a5cc38f..de28b2a0ac 100644
--- a/proof/crefine/X64/VSpace_C.thy
+++ b/proof/crefine/X64/VSpace_C.thy
@@ -1296,10 +1296,6 @@ lemma setVMRoot_ccorres:
   apply (match premises in H: \<open>cr3_C.words_C _.[0] && _ = 0\<close> \<Rightarrow> \<open>insert H; word_bitwise\<close>)
   done
 
-lemma ccorres_seq_IF_False:
-  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)"
-  by simp
-
 (* FIXME x64: needed? *)
 lemma ptrFromPAddr_mask6_simp[simp]:
   "ptrFromPAddr ps && mask 6 = ps && mask 6"